TMToPartrec

📁 Source: Mathlib/Computability/TMToPartrec.lean

Statistics

Metric	Count
Definitions `Cfg'`, `Cont'`, `K'`, `elim`, `Stmt'`, `Supports`, `TrCfg`, `codeSupp`, `codeSupp'`, `contStack`, `contSupp`, `halt`, `head`, `init`, `instDecidableEqCont'`, `decEq`, `instDecidableEqK'`, `instDecidableEqΓ'`, `instFintypeΓ'`, `instInhabitedCfg'`, `instInhabitedCont'`, `default`, `instInhabitedK'`, `default`, `instInhabitedStmt'`, `instInhabitedΓ'`, `default`, `moveExcl`, `move₂`, `natEnd`, `peek'`, `pop'`, `push'`, `splitAtPred`, `tr`, `trCont`, `trContStack`, `trLList`, `trList`, `trNat`, `trNormal`, `trNum`, `trPosNum`, `trStmts₁`, `unrev`, `Γ'`, `Λ'`, `Supports`, `instDecidableEq`, `instInhabited`	50
Theorems `elim_aux`, `elim_main`, `elim_rev`, `elim_stack`, `elim_update_aux`, `elim_update_main`, `elim_update_rev`, `elim_update_stack`, `clear_ok`, `codeSupp'_self`, `codeSupp'_supports`, `codeSupp_case`, `codeSupp_comp`, `codeSupp_cons`, `codeSupp_fix`, `codeSupp_self`, `codeSupp_succ`, `codeSupp_supports`, `codeSupp_tail`, `codeSupp_zero`, `contSupp_comp`, `contSupp_cons₁`, `contSupp_cons₂`, `contSupp_fix`, `contSupp_halt`, `contSupp_supports`, `copy_ok`, `default_Γ'`, `head_main_ok`, `head_stack_ok`, `head_supports`, `move_ok`, `move₂_ok`, `pred_ok`, `ret_supports`, `splitAtPred_eq`, `splitAtPred_false`, `succ_ok`, `supports_biUnion`, `supports_insert`, `supports_singleton`, `supports_union`, `trList_ne_consₗ`, `trNat_default`, `trNat_natEnd`, `trNat_zero`, `trNormal_respects`, `trNormal_supports`, `trNum_natEnd`, `trPosNum_natEnd`, `trStmts₁_self`, `trStmts₁_supports`, `trStmts₁_supports'`, `trStmts₁_trans`, `tr_clear`, `tr_copy`, `tr_eval`, `tr_init`, `tr_move`, `tr_pred`, `tr_push`, `tr_read`, `tr_respects`, `tr_ret_comp`, `tr_ret_cons₁`, `tr_ret_cons₂`, `tr_ret_fix`, `tr_ret_halt`, `tr_ret_respects`, `tr_succ`, `tr_supports`, `unrev_ok`	72
Total	122

Turing.PartrecToTM2

Definitions

Name	Category	Theorems
`Cfg'` 📖	CompOp	1 math math: `tr_eval`
`Cont'` 📖	CompData	—
`K'` 📖	CompData	34 math math: `ret_supports`, `copy_ok`, `move_ok`, `K'.elim_update_main`, `tr_push`, `tr_supports`, `supports_singleton`, `tr_ret_comp`, `head_stack_ok`, `tr_clear`, `tr_respects`, `K'.elim_update_stack`, `tr_ret_cons₂`, `tr_ret_halt`, `tr_pred`, `tr_read`, `tr_eval`, `succ_ok`, `tr_ret_fix`, `supports_insert`, `clear_ok`, `trNormal_respects`, `pred_ok`, `move₂_ok`, `tr_copy`, `tr_ret_respects`, `tr_init`, `unrev_ok`, `head_main_ok`, `K'.elim_update_rev`, `tr_ret_cons₁`, `K'.elim_update_aux`, `tr_succ`, `tr_move`
`Stmt'` 📖	CompOp	—
`Supports` 📖	MathDef	8 math math: `codeSupp_supports`, `supports_union`, `supports_singleton`, `trStmts₁_supports`, `codeSupp'_supports`, `supports_insert`, `contSupp_supports`, `supports_biUnion`
`TrCfg` 📖	MathDef	4 math math: `tr_respects`, `trNormal_respects`, `tr_ret_respects`, `tr_init`
`codeSupp` 📖	CompOp	12 math math: `contSupp_comp`, `codeSupp_self`, `codeSupp_tail`, `tr_supports`, `codeSupp_zero`, `codeSupp_fix`, `contSupp_fix`, `codeSupp_succ`, `codeSupp_case`, `codeSupp_cons`, `contSupp_cons₁`, `codeSupp_comp`
`codeSupp'` 📖	CompOp	2 math math: `codeSupp'_self`, `codeSupp'_supports`
`contStack` 📖	CompOp	—
`contSupp` 📖	CompOp	8 math math: `contSupp_comp`, `contSupp_halt`, `codeSupp_tail`, `codeSupp_zero`, `contSupp_cons₂`, `contSupp_fix`, `codeSupp_succ`, `contSupp_cons₁`
`halt` 📖	CompOp	1 math math: `tr_eval`
`head` 📖	CompOp	5 math math: `head_stack_ok`, `tr_ret_cons₂`, `contSupp_cons₂`, `head_supports`, `head_main_ok`
`init` 📖	CompOp	2 math math: `tr_eval`, `tr_init`
`instDecidableEqCont'` 📖	CompOp	—
`instDecidableEqK'` 📖	CompOp	18 math math: `copy_ok`, `move_ok`, `K'.elim_update_main`, `head_stack_ok`, `tr_respects`, `K'.elim_update_stack`, `tr_eval`, `succ_ok`, `clear_ok`, `trNormal_respects`, `pred_ok`, `move₂_ok`, `tr_ret_respects`, `tr_init`, `unrev_ok`, `head_main_ok`, `K'.elim_update_rev`, `K'.elim_update_aux`
`instDecidableEqΓ'` 📖	CompOp	4 math math: `tr_pred`, `contSupp_cons₁`, `tr_ret_cons₁`, `tr_succ`
`instFintypeΓ'` 📖	CompOp	1 math math: `supports_biUnion`
`instInhabitedCfg'` 📖	CompOp	—
`instInhabitedCont'` 📖	CompOp	—
`instInhabitedK'` 📖	CompOp	—
`instInhabitedStmt'` 📖	CompOp	—
`instInhabitedΓ'` 📖	CompOp	4 math math: `tr_push`, `default_Γ'`, `tr_pred`, `tr_ret_fix`
`moveExcl` 📖	CompOp	—
`move₂` 📖	CompOp	3 math math: `move₂_ok`, `contSupp_cons₁`, `tr_ret_cons₁`
`natEnd` 📖	CompOp	2 math, 3 bridge math: `tr_pred`, `tr_ret_fix` bridge: `trNum_natEnd`, `trPosNum_natEnd`, `trNat_natEnd`
`peek'` 📖	CompOp	1 math math: `tr_pred`
`pop'` 📖	CompOp	6 math math: `tr_clear`, `tr_pred`, `tr_ret_fix`, `tr_copy`, `tr_succ`, `tr_move`
`push'` 📖	CompOp	2 math math: `tr_copy`, `tr_move`
`splitAtPred` 📖	CompOp	2 math math: `splitAtPred_false`, `splitAtPred_eq`
`tr` 📖	CompOp	30 math math: `ret_supports`, `copy_ok`, `move_ok`, `tr_push`, `tr_supports`, `supports_singleton`, `tr_ret_comp`, `head_stack_ok`, `tr_clear`, `tr_respects`, `tr_ret_cons₂`, `tr_ret_halt`, `tr_pred`, `tr_read`, `tr_eval`, `succ_ok`, `tr_ret_fix`, `supports_insert`, `clear_ok`, `trNormal_respects`, `pred_ok`, `move₂_ok`, `tr_copy`, `tr_ret_respects`, `tr_init`, `unrev_ok`, `head_main_ok`, `tr_ret_cons₁`, `tr_succ`, `tr_move`
`trCont` 📖	CompOp	2 math math: `trNormal_respects`, `tr_ret_respects`
`trContStack` 📖	CompOp	2 math math: `trNormal_respects`, `tr_ret_respects`
`trLList` 📖	CompOp	—
`trList` 📖	CompOp	6 math math: `head_stack_ok`, `succ_ok`, `trNormal_respects`, `pred_ok`, `tr_ret_respects`, `head_main_ok`
`trNat` 📖	CompOp	2 math math: `trNat_zero`, `trNat_default`
`trNormal` 📖	CompOp	16 math math: `codeSupp_self`, `codeSupp_tail`, `tr_supports`, `trNormal_supports`, `tr_ret_comp`, `codeSupp'_self`, `codeSupp_zero`, `codeSupp_fix`, `codeSupp_succ`, `codeSupp_case`, `tr_ret_fix`, `trNormal_respects`, `codeSupp_cons`, `contSupp_cons₁`, `tr_ret_cons₁`, `codeSupp_comp`
`trNum` 📖	CompOp	—
`trPosNum` 📖	CompOp	—
`trStmts₁` 📖	CompOp	12 math math: `codeSupp_self`, `codeSupp_tail`, `codeSupp'_self`, `codeSupp_zero`, `codeSupp_fix`, `contSupp_cons₂`, `codeSupp_succ`, `codeSupp_case`, `trStmts₁_self`, `codeSupp_cons`, `contSupp_cons₁`, `codeSupp_comp`
`unrev` 📖	CompOp	3 math math: `tr_pred`, `unrev_ok`, `tr_succ`
`Γ'` 📖	CompData	36 math math: `ret_supports`, `copy_ok`, `trNat_zero`, `K'.elim_update_main`, `tr_push`, `tr_supports`, `supports_singleton`, `tr_ret_comp`, `head_stack_ok`, `tr_clear`, `tr_respects`, `K'.elim_update_stack`, `trNat_default`, `default_Γ'`, `tr_ret_cons₂`, `tr_ret_halt`, `tr_pred`, `tr_read`, `tr_eval`, `succ_ok`, `tr_ret_fix`, `supports_insert`, `trNormal_respects`, `pred_ok`, `tr_copy`, `tr_ret_respects`, `tr_init`, `unrev_ok`, `contSupp_cons₁`, `head_main_ok`, `supports_biUnion`, `K'.elim_update_rev`, `tr_ret_cons₁`, `K'.elim_update_aux`, `tr_succ`, `tr_move`
`Λ'` 📖	CompData	44 math math: `codeSupp_self`, `copy_ok`, `contSupp_halt`, `supports_union`, `move_ok`, `codeSupp_tail`, `tr_push`, `tr_supports`, `supports_singleton`, `tr_ret_comp`, `codeSupp'_self`, `codeSupp_zero`, `head_stack_ok`, `tr_clear`, `tr_respects`, `codeSupp_fix`, `tr_ret_cons₂`, `tr_ret_halt`, `contSupp_cons₂`, `tr_pred`, `tr_read`, `codeSupp_succ`, `codeSupp_case`, `tr_eval`, `succ_ok`, `tr_ret_fix`, `trStmts₁_self`, `supports_insert`, `clear_ok`, `trNormal_respects`, `pred_ok`, `move₂_ok`, `codeSupp_cons`, `tr_copy`, `tr_ret_respects`, `tr_init`, `unrev_ok`, `contSupp_cons₁`, `head_main_ok`, `supports_biUnion`, `tr_ret_cons₁`, `tr_succ`, `tr_move`, `codeSupp_comp`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`clear_ok` 📖	mathematical	`splitAtPred` `Γ'`	`Turing.Reaches₁` `Turing.TM2.Cfg` `K'` `Λ'` `Turing.TM2.step` `instDecidableEqK'` `tr` `Λ'.clear` `Function.update`	—	`Relation.TransGen.head'` `tr.eq_4` `Relation.TransGen.head` `splitAtPred.eq_1` `splitAtPred.eq_2` `Function.update_idem` `Function.update_self`
`codeSupp'_self` 📖	mathematical	—	`Finset` `Λ'` `Finset.instHasSubset` `trStmts₁` `trNormal` `codeSupp'`	—	`subset_refl` `Finset.instReflSubset` `Finset.union_subset_left`
`codeSupp'_supports` 📖	mathematical	`Finset` `Λ'` `Finset.instHasSubset` `codeSupp`	`Supports` `codeSupp'`	—	`trStmts₁_supports` `trNormal_supports` `Finset.Subset.trans` `codeSupp_self` `trStmts₁_supports'` `Finset.union_subset_left` `supports_union` `codeSupp_cons` `Finset.union_subset_right` `contSupp_cons₁` `codeSupp.eq_1` `head_supports` `codeSupp_comp` `codeSupp_case` `codeSupp_fix` `supports_singleton` `ret_supports`
`codeSupp_case` 📖	mathematical	—	`codeSupp` `Turing.ToPartrec.Code.case` `Finset` `Λ'` `Finset.instUnion` `Λ'.instDecidableEq` `trStmts₁` `trNormal`	—	`Finset.union_left_comm` `Finset.union_assoc` `Finset.union_idempotent`
`codeSupp_comp` 📖	mathematical	—	`codeSupp` `Turing.ToPartrec.Code.comp` `Finset` `Λ'` `Finset.instUnion` `Λ'.instDecidableEq` `trStmts₁` `trNormal` `Cont'.comp`	—	`Finset.union_assoc` `Finset.union_eq_right` `codeSupp'_self`
`codeSupp_cons` 📖	mathematical	—	`codeSupp` `Turing.ToPartrec.Code.cons` `Finset` `Λ'` `Finset.instUnion` `Λ'.instDecidableEq` `trStmts₁` `trNormal` `Cont'.cons₁`	—	`Finset.union_assoc`
`codeSupp_fix` 📖	mathematical	—	`codeSupp` `Turing.ToPartrec.Code.fix` `Finset` `Λ'` `Finset.instUnion` `Λ'.instDecidableEq` `trStmts₁` `trNormal` `Cont'.fix`	—	`Finset.union_singleton` `Finset.union_insert` `Finset.union_left_comm` `Finset.insert_union` `Finset.union_assoc` `Finset.union_left_idem`
`codeSupp_self` 📖	mathematical	—	`Finset` `Λ'` `Finset.instHasSubset` `trStmts₁` `trNormal` `codeSupp`	—	`Finset.Subset.trans` `codeSupp'_self` `Finset.union_subset_left`
`codeSupp_succ` 📖	mathematical	—	`codeSupp` `Turing.ToPartrec.Code.succ` `Finset` `Λ'` `Finset.instUnion` `Λ'.instDecidableEq` `trStmts₁` `trNormal` `contSupp`	—	—
`codeSupp_supports` 📖	mathematical	`Finset` `Λ'` `Finset.instHasSubset` `codeSupp`	`Supports`	—	`supports_union` `codeSupp'_supports` `contSupp_supports` `Finset.union_subset_right`
`codeSupp_tail` 📖	mathematical	—	`codeSupp` `Turing.ToPartrec.Code.tail` `Finset` `Λ'` `Finset.instUnion` `Λ'.instDecidableEq` `trStmts₁` `trNormal` `contSupp`	—	—
`codeSupp_zero` 📖	mathematical	—	`codeSupp` `Turing.ToPartrec.Code.zero'` `Finset` `Λ'` `Finset.instUnion` `Λ'.instDecidableEq` `trStmts₁` `trNormal` `contSupp`	—	—
`contSupp_comp` 📖	mathematical	—	`contSupp` `Cont'.comp` `codeSupp`	—	—
`contSupp_cons₁` 📖	mathematical	—	`contSupp` `Cont'.cons₁` `Finset` `Λ'` `Finset.instUnion` `Λ'.instDecidableEq` `trStmts₁` `move₂` `K'.main` `K'.aux` `Γ'` `Γ'.consₗ` `instDecidableEqΓ'` `K'.stack` `trNormal` `Cont'.cons₂` `codeSupp`	—	—
`contSupp_cons₂` 📖	mathematical	—	`contSupp` `Cont'.cons₂` `Finset` `Λ'` `Finset.instUnion` `Λ'.instDecidableEq` `trStmts₁` `head` `K'.stack` `Λ'.ret`	—	—
`contSupp_fix` 📖	mathematical	—	`contSupp` `Cont'.fix` `codeSupp`	—	`Finset.union_assoc`
`contSupp_halt` 📖	mathematical	—	`contSupp` `Cont'.halt` `Finset` `Λ'` `Finset.instEmptyCollection`	—	—
`contSupp_supports` 📖	mathematical	`Finset` `Λ'` `Finset.instHasSubset` `contSupp`	`Supports`	—	`instIsEmptyFalse` `Finset.union_subset_right` `contSupp_cons₁` `trStmts₁_supports'` `trNormal_supports` `supports_union` `codeSupp'_supports` `head_supports` `contSupp_cons₂` `contSupp_comp` `contSupp.eq_4`
`copy_ok` 📖	mathematical	—	`Turing.Reaches₁` `Turing.TM2.Cfg` `K'` `Γ'` `Λ'` `Turing.TM2.step` `instDecidableEqK'` `tr` `Λ'.copy` `K'.elim`	—	`K'.elim_update_rev` `K'.elim_update_main` `K'.elim_update_stack` `Relation.TransGen.head` `tr.eq_5` `Function.update.congr_simp`
`default_Γ'` 📖	mathematical	—	`Γ'` `instInhabitedΓ'` `Γ'.consₗ`	—	—
`head_main_ok` 📖	mathematical	—	`Turing.Reaches₁` `Turing.TM2.Cfg` `K'` `Γ'` `Λ'` `Turing.TM2.step` `instDecidableEqK'` `tr` `head` `K'.main` `K'.elim` `trList` `List.headI`	—	`move_ok` `splitAtPred_eq` `trNat_natEnd` `trNat_zero` `Relation.TransGen.head` `tr.eq_3` `K'.elim_update_main` `K'.elim_update_rev` `Function.update.congr_simp` `Function.update_self` `clear_ok` `Bool.decide_false` `trList_ne_consₗ` `Function.update_of_ne` `unrev_ok`
`head_stack_ok` 📖	mathematical	—	`Turing.Reaches₁` `Turing.TM2.Cfg` `K'` `Γ'` `Λ'` `Turing.TM2.step` `instDecidableEqK'` `tr` `head` `K'.stack` `K'.elim` `trList` `Γ'.consₗ` `List.headI`	—	`move_ok` `splitAtPred_eq` `Relation.TransGen.head` `tr.eq_3` `K'.elim_update_stack` `K'.elim_update_rev` `Function.update.congr_simp` `Function.update_self` `trNat_default` `K'.elim_update_main` `unrev_ok` `trNat_natEnd` `clear_ok` `Bool.decide_false` `trList_ne_consₗ` `Function.update_of_ne`
`head_supports` 📖	mathematical	`Λ'.Supports`	`head`	—	—
`move_ok` 📖	mathematical	`splitAtPred` `Γ'`	`Turing.Reaches₁` `Turing.TM2.Cfg` `K'` `Λ'` `Turing.TM2.step` `instDecidableEqK'` `tr` `Λ'.move` `Function.update`	—	`Function.update_of_ne` `Function.update_eq_self` `Relation.TransGen.head'` `Relation.TransGen.head` `tr.eq_1` `splitAtPred.eq_1` `splitAtPred.eq_2` `Function.update_self` `Function.update_comm` `Function.update_idem`
`move₂_ok` 📖	mathematical	`K'.rev` `Γ'` `splitAtPred`	`Turing.Reaches₁` `Turing.TM2.Cfg` `K'` `Λ'` `Turing.TM2.step` `instDecidableEqK'` `tr` `move₂` `Function.update`	—	`move_ok` `Relation.TransGen.head` `tr.eq_2` `Function.update_comm` `Function.update_idem` `Function.update_eq_self` `Function.update.congr_simp` `Function.update_of_ne` `Function.update_self` `splitAtPred_false`
`pred_ok` 📖	mathematical	—	`Turing.Reaches₁` `Turing.TM2.Cfg` `K'` `Γ'` `Λ'` `Turing.TM2.step` `instDecidableEqK'` `tr` `Λ'.pred` `K'.elim` `trList` `List.headI`	—	`K'.elim_update_main` `K'.elim_update_rev` `trNat_zero` `Nat.cast_succ` `Num.add_one` `Relation.TransGen.head` `tr.eq_7` `Function.update_of_ne` `unrev_ok`
`ret_supports` 📖	mathematical	`Finset` `Λ'` `Finset.instHasSubset` `contSupp`	`Turing.TM2.SupportsStmt` `K'` `Γ'` `tr` `Λ'.ret`	—	`trStmts₁_self` `Finset.union_subset_iff` `contSupp_cons₁` `contSupp_cons₂` `contSupp_comp` `codeSupp_self` `Finset.mem_union_left` `Finset.mem_union_right` `contSupp_fix` `Finset.mem_singleton_self`
`splitAtPred_eq` 📖	mathematical	`Option.elim'`	`splitAtPred`	—	`splitAtPred.eq_2`
`splitAtPred_false` 📖	mathematical	—	`splitAtPred`	—	`splitAtPred_eq`
`succ_ok` 📖	mathematical	—	`Turing.Reaches₁` `Turing.TM2.Cfg` `K'` `Γ'` `Λ'` `Turing.TM2.step` `instDecidableEqK'` `tr` `Λ'.succ` `K'.elim` `trList`	—	`Nat.cast_succ` `Num.add_one` `Relation.TransGen.head` `K'.elim_update_main` `Function.update.congr_simp` `K'.elim_update_rev` `unrev_ok` `tr.eq_6` `Function.update_self`
`supports_biUnion` 📖	mathematical	—	`Supports` `Finset.biUnion` `Γ'` `Λ'` `Λ'.instDecidableEq` `Finset.univ` `instFintypeOption` `instFintypeΓ'`	—	`forall_swap`
`supports_insert` 📖	mathematical	—	`Supports` `Λ'` `Finset` `Finset.instInsert` `Λ'.instDecidableEq` `Turing.TM2.SupportsStmt` `K'` `Γ'` `tr`	—	—
`supports_singleton` 📖	mathematical	—	`Supports` `Λ'` `Finset` `Finset.instSingleton` `Turing.TM2.SupportsStmt` `K'` `Γ'` `tr`	—	—
`supports_union` 📖	mathematical	—	`Supports` `Finset` `Λ'` `Finset.instUnion` `Λ'.instDecidableEq`	—	—
`trList_ne_consₗ` 📖	—	`Γ'` `trList`	—	—	`trNat_natEnd`
`trNat_default` 📖	mathematical	—	`trNat` `Γ'`	—	`trNat_zero`
`trNat_natEnd` 📖	bridging (complete)	`Γ'` `trNat`	`natEnd`	`natEnd`	`trNum_natEnd`
`trNat_zero` 📖	mathematical	—	`trNat` `Γ'`	—	`trNat.eq_1` `Nat.cast_zero`
`trNormal_respects` 📖	mathematical	—	`TrCfg` `Turing.ToPartrec.stepNormal` `Turing.Reaches₁` `Turing.TM2.Cfg` `K'` `Γ'` `Λ'` `Turing.TM2.step` `instDecidableEqK'` `tr` `trNormal` `trCont` `K'.elim` `trList` `trContStack`	—	`K'.elim_update_main` `trNat_zero` `head_main_ok` `succ_ok` `clear_ok` `splitAtPred_eq` `trNat_natEnd` `Relation.TransGen.head` `move_ok` `splitAtPred_false` `K'.elim_update_stack` `K'.elim_update_rev` `copy_ok` `Turing.ToPartrec.stepNormal.eq_6` `pred_ok`
`trNormal_supports` 📖	mathematical	`Finset` `Λ'` `Finset.instHasSubset` `codeSupp`	`Λ'.Supports` `trNormal`	—	`Finset.union_subset_right` `codeSupp_cons` `codeSupp_comp` `codeSupp_case` `codeSupp_fix`
`trNum_natEnd` 📖	bridging (complete)	`Γ'` `trNum`	`natEnd`	`natEnd`	`trPosNum_natEnd`
`trPosNum_natEnd` 📖	bridging (complete)	`Γ'` `trPosNum`	`natEnd`	`natEnd`	—
`trStmts₁_self` 📖	mathematical	—	`Λ'` `Finset` `Finset.instMembership` `trStmts₁`	—	`Finset.mem_insert_self` `Finset.mem_singleton_self`
`trStmts₁_supports` 📖	mathematical	`Λ'.Supports` `Finset` `Λ'` `Finset.instHasSubset` `trStmts₁`	`Supports`	—	`trStmts₁_self` `Finset.insert_subset_iff` `supports_insert` `supports_biUnion` `Finset.union_insert` `supports_union` `supports_singleton` `ret_supports`
`trStmts₁_supports'` 📖	—	`Λ'.Supports` `Finset` `Λ'` `Finset.instHasSubset` `Finset.instUnion` `Λ'.instDecidableEq` `trStmts₁` `Supports`	—	—	`supports_union` `trStmts₁_supports`
`trStmts₁_trans` 📖	mathematical	`Λ'` `Finset` `Finset.instMembership` `trStmts₁`	`Finset.instHasSubset`	—	`Finset.Subset.trans` `Finset.subset_insert` `Finset.union_insert` `Finset.mem_insert`
`tr_clear` 📖	mathematical	—	`tr` `Λ'.clear` `pop'` `Turing.TM2.Stmt.branch` `K'` `Γ'` `Λ'` `Turing.TM2.Stmt.goto`	—	—
`tr_copy` 📖	mathematical	—	`tr` `Λ'.copy` `pop'` `K'.rev` `Turing.TM2.Stmt.branch` `K'` `Γ'` `Λ'` `push'` `K'.main` `K'.stack` `Turing.TM2.Stmt.goto`	—	—
`tr_eval` 📖	mathematical	—	`Turing.eval` `Turing.TM2.Cfg` `K'` `Γ'` `Λ'` `Turing.TM2.step` `instDecidableEqK'` `tr` `init` `Part` `Part.instMonad` `Cfg'` `halt` `Turing.ToPartrec.Code.eval`	—	`tr_init` `Part.ext` `Turing.reaches_eval` `Relation.TransGen.to_reflTransGen` `Turing.tr_eval_rev` `tr_respects` `Turing.ToPartrec.stepNormal_eval` `Turing.tr_eval`
`tr_init` 📖	mathematical	—	`TrCfg` `Turing.ToPartrec.stepNormal` `Turing.ToPartrec.Cont.halt` `Turing.Reaches₁` `Turing.TM2.Cfg` `K'` `Γ'` `Λ'` `Turing.TM2.step` `instDecidableEqK'` `tr` `init`	—	`trNormal_respects`
`tr_move` 📖	mathematical	—	`tr` `Λ'.move` `pop'` `Turing.TM2.Stmt.branch` `K'` `Γ'` `Λ'` `Turing.TM2.Stmt.goto` `push'`	—	—
`tr_pred` 📖	mathematical	—	`tr` `Λ'.pred` `pop'` `K'.main` `Turing.TM2.Stmt.branch` `K'` `Γ'` `Λ'` `Γ'.bit0` `instDecidableEqΓ'` `Turing.TM2.Stmt.push` `K'.rev` `Γ'.bit1` `Turing.TM2.Stmt.goto` `natEnd` `instInhabitedΓ'` `peek'` `unrev`	—	—
`tr_push` 📖	mathematical	—	`tr` `Λ'.push` `Turing.TM2.Stmt.branch` `K'` `Γ'` `Λ'` `Turing.TM2.Stmt.push` `instInhabitedΓ'` `Turing.TM2.Stmt.goto`	—	—
`tr_read` 📖	mathematical	—	`tr` `Λ'.read` `Turing.TM2.Stmt.goto` `K'` `Γ'` `Λ'`	—	—
`tr_respects` 📖	mathematical	—	`Turing.Respects` `Turing.ToPartrec.Cfg` `Turing.TM2.Cfg` `K'` `Γ'` `Λ'` `Turing.ToPartrec.step` `Turing.TM2.step` `instDecidableEqK'` `tr` `TrCfg`	—	`tr_ret_respects`
`tr_ret_comp` 📖	mathematical	—	`tr` `Λ'.ret` `Cont'.comp` `Turing.TM2.Stmt.goto` `K'` `Γ'` `Λ'` `trNormal`	—	—
`tr_ret_cons₁` 📖	mathematical	—	`tr` `Λ'.ret` `Cont'.cons₁` `Turing.TM2.Stmt.goto` `K'` `Γ'` `Λ'` `move₂` `K'.main` `K'.aux` `Γ'.consₗ` `instDecidableEqΓ'` `K'.stack` `trNormal` `Cont'.cons₂`	—	—
`tr_ret_cons₂` 📖	mathematical	—	`tr` `Λ'.ret` `Cont'.cons₂` `Turing.TM2.Stmt.goto` `K'` `Γ'` `Λ'` `head` `K'.stack`	—	—
`tr_ret_fix` 📖	mathematical	—	`tr` `Λ'.ret` `Cont'.fix` `pop'` `K'.main` `Turing.TM2.Stmt.goto` `K'` `Γ'` `Λ'` `natEnd` `instInhabitedΓ'` `Λ'.clear` `trNormal`	—	—
`tr_ret_halt` 📖	mathematical	—	`tr` `Λ'.ret` `Cont'.halt` `Turing.TM2.Stmt.load` `K'` `Γ'` `Λ'` `Turing.TM2.Stmt.halt`	—	—
`tr_ret_respects` 📖	mathematical	—	`TrCfg` `Turing.ToPartrec.stepRet` `Turing.Reaches₁` `Turing.TM2.Cfg` `K'` `Γ'` `Λ'` `Turing.TM2.step` `instDecidableEqK'` `tr` `Λ'.ret` `trCont` `K'.elim` `trList` `trContStack`	—	`trNormal_respects` `Relation.TransGen.head` `move₂_ok` `splitAtPred_false` `K'.elim_update_main` `K'.elim_update_aux` `splitAtPred_eq` `Bool.decide_false` `trList_ne_consₗ` `K'.elim_update_stack` `Function.update.congr_simp` `head_stack_ok` `Turing.ToPartrec.stepRet.eq_5` `trNat_zero` `trList.eq_2` `List.headI.eq_2` `trNat.eq_1` `Nat.cast_succ` `Num.add_one` `Num.succ.eq_1` `List.tail.eq_2` `trCont.eq_5` `tr.eq_11` `clear_ok` `trNat_natEnd` `List.tail_subset`
`tr_succ` 📖	mathematical	—	`tr` `Λ'.succ` `pop'` `K'.main` `Turing.TM2.Stmt.branch` `K'` `Γ'` `Λ'` `Γ'.bit1` `instDecidableEqΓ'` `Turing.TM2.Stmt.push` `K'.rev` `Γ'.bit0` `Turing.TM2.Stmt.goto` `Γ'.cons` `unrev`	—	—
`tr_supports` 📖	mathematical	—	`Turing.TM2.Supports` `K'` `Γ'` `Λ'` `trNormal` `tr` `codeSupp`	—	`codeSupp_self` `trStmts₁_self` `codeSupp_supports` `Finset.Subset.refl`
`unrev_ok` 📖	mathematical	—	`Turing.Reaches₁` `Turing.TM2.Cfg` `K'` `Γ'` `Λ'` `Turing.TM2.step` `instDecidableEqK'` `tr` `unrev` `Function.update` `K'.rev` `K'.main`	—	`move_ok` `splitAtPred_false`

Turing.PartrecToTM2.K'

Definitions

Name	Category	Theorems
`elim` 📖	CompOp	15 math math: `elim_aux`, `Turing.PartrecToTM2.copy_ok`, `elim_update_main`, `elim_rev`, `elim_main`, `Turing.PartrecToTM2.head_stack_ok`, `elim_update_stack`, `Turing.PartrecToTM2.succ_ok`, `Turing.PartrecToTM2.trNormal_respects`, `Turing.PartrecToTM2.pred_ok`, `elim_stack`, `Turing.PartrecToTM2.tr_ret_respects`, `Turing.PartrecToTM2.head_main_ok`, `elim_update_rev`, `elim_update_aux`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`elim_aux` 📖	mathematical	—	`elim` `aux`	—	—
`elim_main` 📖	mathematical	—	`elim` `main`	—	—
`elim_rev` 📖	mathematical	—	`elim` `rev`	—	—
`elim_stack` 📖	mathematical	—	`elim` `stack`	—	—
`elim_update_aux` 📖	mathematical	—	`Function.update` `Turing.PartrecToTM2.K'` `Turing.PartrecToTM2.Γ'` `Turing.PartrecToTM2.instDecidableEqK'` `elim` `aux`	—	—
`elim_update_main` 📖	mathematical	—	`Function.update` `Turing.PartrecToTM2.K'` `Turing.PartrecToTM2.Γ'` `Turing.PartrecToTM2.instDecidableEqK'` `elim` `main`	—	—
`elim_update_rev` 📖	mathematical	—	`Function.update` `Turing.PartrecToTM2.K'` `Turing.PartrecToTM2.Γ'` `Turing.PartrecToTM2.instDecidableEqK'` `elim` `rev`	—	—
`elim_update_stack` 📖	mathematical	—	`Function.update` `Turing.PartrecToTM2.K'` `Turing.PartrecToTM2.Γ'` `Turing.PartrecToTM2.instDecidableEqK'` `elim` `stack`	—	—

Turing.PartrecToTM2.instDecidableEqCont'

Definitions

Name	Category	Theorems
`decEq` 📖	CompOp	—

Turing.PartrecToTM2.instInhabitedCont'

Definitions

Name	Category	Theorems
`default` 📖	CompOp	—

Turing.PartrecToTM2.instInhabitedK'

Definitions

Name	Category	Theorems
`default` 📖	CompOp	—

Turing.PartrecToTM2.instInhabitedΓ'

Definitions

Name	Category	Theorems
`default` 📖	CompOp	—

Turing.PartrecToTM2.Λ'

Definitions

Name	Category	Theorems
`Supports` 📖	MathDef	1 math math: `Turing.PartrecToTM2.trNormal_supports`
`instDecidableEq` 📖	CompOp	12 math math: `Turing.PartrecToTM2.supports_union`, `Turing.PartrecToTM2.codeSupp_tail`, `Turing.PartrecToTM2.codeSupp_zero`, `Turing.PartrecToTM2.codeSupp_fix`, `Turing.PartrecToTM2.contSupp_cons₂`, `Turing.PartrecToTM2.codeSupp_succ`, `Turing.PartrecToTM2.codeSupp_case`, `Turing.PartrecToTM2.supports_insert`, `Turing.PartrecToTM2.codeSupp_cons`, `Turing.PartrecToTM2.contSupp_cons₁`, `Turing.PartrecToTM2.supports_biUnion`, `Turing.PartrecToTM2.codeSupp_comp`
`instInhabited` 📖	CompOp	—

---

← Back to Index