Documentation Verification Report

StateTransition

📁 Source: Mathlib/Computability/StateTransition.lean

Statistics

Metric	Count
Definitions `EvalsTo`, `refl`, `steps`, `trans`, `EvalsToInTime`, `refl`, `toEvalsTo`, `trans`, `FRespects`, `Reaches`, `Reaches₀`, `Reaches₁`, `Respects`, `eval`, `evalInduction`	15
Theorems `evals_in_steps`, `steps_le_m`, `to₀`, `head`, `refl`, `single`, `tail`, `tail'`, `trans`, `to₀`, `eval_maximal`, `eval_maximal₁`, `frespects_eq`, `fun_respects`, `mem_eval`, `reaches_eval`, `reaches_total`, `reaches₀_eq`, `reaches₁_eq`, `reaches₁_fwd`, `tr_eval`, `tr_eval'`, `tr_eval_dom`, `tr_eval_rev`, `tr_reaches`, `tr_reaches_rev`, `tr_reaches₁`	27
Total	42

StateTransition

Definitions

Name	Category	Theorems
`EvalsTo` 📖	CompData	—
`EvalsToInTime` 📖	CompData	—
`FRespects` 📖	MathDef	2 math math: `fun_respects`, `frespects_eq`
`Reaches` 📖	MathDef	7 math math: `reaches₁_fwd`, `Turing.TM2to1.tr_respects_aux`, `tr_reaches_rev`, `tr_reaches`, `mem_eval`, `eval_maximal`, `reaches_total`
`Reaches₀` 📖	MathDef	10 math math: `Turing.TM2to1.tr_respects_aux₁`, `Reaches.to₀`, `Reaches₁.to₀`, `Turing.TM2to1.tr_respects_aux₃`, `Reaches₀.trans`, `Reaches₀.tail`, `Reaches₀.single`, `Reaches₀.refl`, `reaches₀_eq`, `Reaches₀.head`
`Reaches₁` 📖	MathDef	16 math math: `Turing.PartrecToTM2.copy_ok`, `Turing.PartrecToTM2.move_ok`, `Reaches₀.tail'`, `Turing.PartrecToTM2.head_stack_ok`, `eval_maximal₁`, `tr_reaches₁`, `Turing.PartrecToTM2.succ_ok`, `Turing.PartrecToTM2.clear_ok`, `Turing.PartrecToTM2.trNormal_respects`, `Turing.PartrecToTM2.pred_ok`, `Turing.PartrecToTM2.move₂_ok`, `Turing.PartrecToTM2.tr_ret_respects`, `Turing.PartrecToTM2.tr_init`, `Turing.PartrecToTM2.unrev_ok`, `Turing.PartrecToTM2.head_main_ok`, `reaches₁_eq`
`Respects` 📖	MathDef	7 math math: `fun_respects`, `Turing.TM0to1.tr_respects`, `Turing.PartrecToTM2.tr_respects`, `Turing.TM1to1.tr_respects`, `Turing.TM1to0.tr_respects`, `Turing.TM0.Machine.map_respects`, `Turing.TM2to1.tr_respects`
`eval` 📖	CompOp	11 math math: `tr_eval'`, `Turing.ToPartrec.stepNormal_eval`, `tr_eval`, `tr_eval_dom`, `reaches_eval`, `Turing.ToPartrec.stepRet_eval`, `Turing.ToPartrec.cont_eval_fix`, `mem_eval`, `Turing.PartrecToTM2.tr_eval`, `Turing.ToPartrec.Code.Ok.zero`, `tr_eval_rev`
`evalInduction` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eval_maximal` 📖	mathematical	`Part` `Part.instMembership` `eval`	`Reaches`	—	`mem_eval` `Relation.reflTransGen_iff_eq`
`eval_maximal₁` 📖	mathematical	`Part` `Part.instMembership` `eval`	`Reaches₁`	—	`mem_eval` `Relation.TransGen.head'_iff`
`frespects_eq` 📖	mathematical	—	`FRespects`	—	`reaches₁_eq`
`fun_respects` 📖	mathematical	—	`Respects` `FRespects`	—	—
`mem_eval` 📖	mathematical	—	`Part` `Part.instMembership` `eval` `Reaches`	—	`Part.mem_unique` `PFun.mem_fix_iff` `Part.mem_some_iff` `Relation.ReflTransGen.head` `Relation.ReflTransGen.head_induction_on` `Part.mem_some`
`reaches_eval` 📖	mathematical	`Reaches`	`eval`	—	`Part.ext` `mem_eval` `eval_maximal` `reaches_total` `Relation.ReflTransGen.trans`
`reaches_total` 📖	mathematical	`Reaches`	`Reaches`	—	`Relation.ReflTransGen.total_of_right_unique`
`reaches₀_eq` 📖	mathematical	—	`Reaches₀`	—	`reaches₁_eq`
`reaches₁_eq` 📖	mathematical	—	`Reaches₁`	—	`Relation.TransGen.head'_iff`
`reaches₁_fwd` 📖	mathematical	`Reaches₁`	`Reaches`	—	`Relation.TransGen.head'_iff`
`tr_eval` 📖	mathematical	`Respects` `Part` `Part.instMembership` `eval`	`Part` `Part.instMembership` `eval`	—	`mem_eval` `tr_reaches`
`tr_eval'` 📖	mathematical	`Respects`	`eval` `Part` `Part.instMonad`	—	`Part.ext` `tr_eval_rev` `Part.mem_map_iff` `tr_eval`
`tr_eval_dom` 📖	mathematical	`Respects`	`Part.Dom` `eval`	—	`tr_eval_rev` `tr_eval`
`tr_eval_rev` 📖	mathematical	`Respects` `Part` `Part.instMembership` `eval`	`Part` `Part.instMembership` `eval`	—	`mem_eval` `tr_reaches_rev` `Relation.reflTransGen_iff_eq` `Relation.TransGen.head'_iff`
`tr_reaches` 📖	mathematical	`Respects` `Reaches`	`Reaches`	—	`Relation.reflTransGen_iff_eq_or_transGen` `tr_reaches₁` `Relation.TransGen.to_reflTransGen`
`tr_reaches_rev` 📖	mathematical	`Respects` `Reaches`	`Reaches`	—	`Relation.ReflTransGen.cases_head` `Relation.TransGen.head'_iff`
`tr_reaches₁` 📖	mathematical	`Respects` `Reaches₁`	`Reaches₁`	—	—

StateTransition.EvalsTo

Definitions

Name	Category	Theorems
`refl` 📖	CompOp	—
`steps` 📖	CompOp	2 math math: `StateTransition.EvalsToInTime.steps_le_m`, `evals_in_steps`
`trans` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`evals_in_steps` 📖	mathematical	—	`Nat.iterate` `steps`	—	—

StateTransition.EvalsToInTime

Definitions

Name	Category	Theorems
`refl` 📖	CompOp	—
`toEvalsTo` 📖	CompOp	1 math math: `steps_le_m`
`trans` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`steps_le_m` 📖	mathematical	—	`StateTransition.EvalsTo.steps` `toEvalsTo`	—	—

StateTransition.Reaches

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`to₀` 📖	mathematical	`StateTransition.Reaches`	`StateTransition.Reaches₀`	—	`Relation.TransGen.trans_right`

StateTransition.Reaches₀

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`head` 📖	mathematical	`StateTransition.Reaches₀`	`StateTransition.Reaches₀`	—	`trans` `single`
`refl` 📖	mathematical	—	`StateTransition.Reaches₀`	—	—
`single` 📖	mathematical	—	`StateTransition.Reaches₀`	—	`Relation.TransGen.head`
`tail` 📖	mathematical	`StateTransition.Reaches₀`	`StateTransition.Reaches₀`	—	`trans` `single`
`tail'` 📖	mathematical	`StateTransition.Reaches₀`	`StateTransition.Reaches₁`	—	—
`trans` 📖	mathematical	`StateTransition.Reaches₀`	`StateTransition.Reaches₀`	—	—

StateTransition.Reaches₁

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`to₀` 📖	mathematical	`StateTransition.Reaches₁`	`StateTransition.Reaches₀`	—	—

---

← Back to Index