Theorems · Definition · logic and foundations
StateTransition.Reaches
{σ : Type u_1} → (σ → Option σ) → σ → σ → PropThe reflexive transitive closure of a state transition function. Reaches f a b means
there is a finite sequence of steps f a = some a₁, f a₁ = some a₂, ... such that aₙ = b.
This relation permits zero steps of the state transition function.
- Defined in
- Mathlib.Computability.StateTransition
- Cited by
- 15 results in Mathlib
- Foundations
- Depth 4 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites1
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Relation.ReflTransGenproof · cited by 104
Cited by15
Results whose statement or proof uses this declaration.
- StateTransition.mem_evalstatement and proof · cited by 8
- StateTransition.reaches_evalstatement and proof · cited by 4
- StateTransition.tr_evalproof · cited by 4
- StateTransition.tr_eval_revproof · cited by 3
- Turing.ToPartrec.cont_eval_fixproof · cited by 2
- Turing.TM2to1.tr_respectsproof · cited by 2
- StateTransition.tr_reachesstatement and proof · cited by 1
- StateTransition.tr_reaches_revstatement and proof · cited by 1
- Turing.TM2to1.tr_respects_auxstatement and proof · cited by 1
- StateTransition.eval_maximalstatement and proof · cited by 1
- StateTransition.reaches_totalstatement and proof · cited by 1
- Turing.TM1to1.tr_respectsproof · cited by 0