Tape

📁 Source: Mathlib/Computability/Tape.lean

Statistics

Metric	Count
Definitions `BlankExtends`, `above`, `BlankRel`, `above`, `below`, `setoid`, `Dir`, `ListBlank`, `append`, `cons`, `flatMap`, `hasEmptyc`, `head`, `inhabited`, `liftOn`, `map`, `mk`, `modifyNth`, `nth`, `tail`, `PointedMap`, `f`, `Tape`, `Tape`, `Tape`, `head`, `inhabited`, `left`, `left₀`, `map`, `mk'`, `mk₁`, `mk₂`, `move`, `nth`, `right`, `right₀`, `write`, `instCoeFunPointedMapForall`, `instDecidableEqDir`, `instInhabitedDir`, `default`, `instInhabitedPointedMap`, `proj`	44
Theorems `above_of_le`, `below_of_le`, `refl`, `trans`, `equivalence`, `refl`, `trans`, `append_assoc`, `append_mk`, `cons_flatMap`, `cons_head_tail`, `cons_mk`, `exists_cons`, `ext`, `ext_iff`, `flatMap_mk`, `head_cons`, `head_map`, `head_mk`, `induction_on`, `map_cons`, `map_mk`, `map_modifyNth`, `nth_map`, `nth_mk`, `nth_modifyNth`, `nth_succ`, `nth_zero`, `tail_cons`, `tail_map`, `tail_mk`, `headI_map`, `map_pt`, `map_pt'`, `mk_val`, `exists_mk'`, `map_fst`, `map_mk'`, `map_mk₁`, `map_mk₂`, `map_move`, `map_write`, `mk'_head`, `mk'_left`, `mk'_left_right₀`, `mk'_nth_nat`, `mk'_right`, `mk'_right₀`, `move_left_mk'`, `move_left_nth`, `move_left_right`, `move_right_left`, `move_right_mk'`, `move_right_n_head`, `move_right_nth`, `nth_zero`, `right₀_nth`, `write_mk`, `write_mk'`, `write_move_right_n`, `write_nth`, `write_self`, `proj_map_nth`	63
Total	107

Turing

Definitions

Name	Category	Theorems
`BlankExtends` 📖	MathDef	1 math math: `BlankExtends.refl`
`BlankRel` 📖	MathDef	2 math math: `BlankRel.equivalence`, `BlankRel.refl`
`Dir` 📖	CompData	—
`ListBlank` 📖	CompOp	4 math math: `TM2to1.tr_respects_aux₁`, `TM2to1.tr_respects_aux₃`, `TM2to1.tr_eval_dom`, `TM2to1.tr_respects_aux₂`
`PointedMap` 📖	CompData	—
`Tape` 📖	CompData	8 math math: `TM2to1.tr_respects_aux₁`, `Tape.move_right_n_head`, `TM2to1.tr_respects_aux₃`, `Tape.write_move_right_n`, `TM1to1.trTape'_move_left`, `TM1to1.stepAux_move`, `TM1to1.trTape'_move_right`, `TM2to1.tr_respects_aux₂`
`instCoeFunPointedMapForall` 📖	CompOp	—
`instDecidableEqDir` 📖	CompOp	—
`instInhabitedDir` 📖	CompOp	—
`instInhabitedPointedMap` 📖	CompOp	—
`proj` 📖	CompOp	2 math math: `TM2to1.tr_eval`, `proj_map_nth`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`proj_map_nth` 📖	mathematical	—	`ListBlank.nth` `ListBlank.map` `proj`	—	`ListBlank.nth_map`

Turing.BlankExtends

Definitions

Name	Category	Theorems
`above` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`above_of_le` 📖	—	`Turing.BlankExtends`	—	—	`List.replicate_add`
`below_of_le` 📖	—	`Turing.BlankExtends`	—	—	—
`refl` 📖	mathematical	—	`Turing.BlankExtends`	—	—
`trans` 📖	—	`Turing.BlankExtends`	—	—	—

Turing.BlankRel

Definitions

Name	Category	Theorems
`above` 📖	CompOp	—
`below` 📖	CompOp	—
`setoid` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`equivalence` 📖	mathematical	—	`Turing.BlankRel`	—	`refl` `symm` `trans`
`refl` 📖	mathematical	—	`Turing.BlankRel`	—	`Turing.BlankExtends.refl`
`trans` 📖	—	`Turing.BlankRel`	—	—	—

Turing.ListBlank

Definitions

Name	Category	Theorems
`append` 📖	CompOp	3 math math: `append_mk`, `append_assoc`, `cons_flatMap`
`cons` 📖	CompOp	13 math math: `Turing.Tape.move_left_mk'`, `Turing.TM1to1.stepAux_write`, `exists_cons`, `head_cons`, `map_cons`, `Turing.Tape.write_mk'`, `tail_cons`, `cons_flatMap`, `Turing.TM1to1.trTape'_move_left`, `cons_mk`, `Turing.Tape.move_right_mk'`, `Turing.TM1to1.trTape'_move_right`, `cons_head_tail`
`flatMap` 📖	CompOp	2 math math: `flatMap_mk`, `cons_flatMap`
`hasEmptyc` 📖	CompOp	3 math math: `Turing.TM2to1.tr_respects_aux₁`, `Turing.TM2to1.tr_respects_aux₃`, `Turing.TM2to1.tr_respects_aux₂`
`head` 📖	CompOp	12 math math: `nth_zero`, `head_map`, `Turing.Tape.move_left_mk'`, `Turing.TM1to1.stepAux_read`, `head_cons`, `Turing.Tape.mk'_head`, `head_mk`, `Turing.TM1to1.trTape'_move_left`, `Turing.TM2to1.addBottom_head_fst`, `Turing.Tape.move_right_mk'`, `Turing.TM1to1.trTape'_move_right`, `cons_head_tail`
`inhabited` 📖	CompOp	—
`liftOn` 📖	CompOp	—
`map` 📖	CompOp	10 math math: `head_map`, `map_mk`, `map_modifyNth`, `map_cons`, `tail_map`, `Turing.Tape.map_mk'`, `Turing.TM2to1.tr_eval`, `Turing.TM2to1.addBottom_map`, `nth_map`, `Turing.proj_map_nth`
`mk` 📖	CompOp	—
`modifyNth` 📖	CompOp	4 math math: `Turing.TM2to1.addBottom_modifyNth`, `nth_modifyNth`, `map_modifyNth`, `Turing.Tape.write_move_right_n`
`nth` 📖	CompOp	13 math math: `Turing.TM2to1.addBottom_nth_succ_fst`, `nth_zero`, `ext_iff`, `nth_modifyNth`, `Turing.TM2to1.stk_nth_val`, `nth_succ`, `Turing.Tape.write_move_right_n`, `Turing.Tape.mk'_nth_nat`, `Turing.Tape.right₀_nth`, `nth_map`, `nth_mk`, `Turing.TM2to1.addBottom_nth_snd`, `Turing.proj_map_nth`
`tail` 📖	CompOp	11 math math: `Turing.Tape.move_left_mk'`, `tail_mk`, `nth_succ`, `Turing.Tape.write_mk'`, `tail_cons`, `tail_map`, `Turing.TM1to1.trTape'_move_left`, `Turing.Tape.move_right_mk'`, `Turing.TM1to1.trTape'_move_right`, `cons_head_tail`, `Turing.Tape.mk'_right`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`append_assoc` 📖	mathematical	—	`append`	—	`induction_on`
`append_mk` 📖	mathematical	—	`append`	—	—
`cons_flatMap` 📖	mathematical	—	`flatMap` `cons` `append`	—	`induction_on`
`cons_head_tail` 📖	mathematical	—	`cons` `head` `tail`	—	`Quotient.ind'` `Quotient.sound'` `Turing.BlankExtends.refl`
`cons_mk` 📖	mathematical	—	`cons`	—	—
`exists_cons` 📖	mathematical	—	`cons`	—	`cons_head_tail`
`ext` 📖	—	`nth`	—	—	`induction_on` `Quotient.sound'` `lt_or_ge` `List.getI_eq_getElem` `List.getI_eq_default` `le_total`
`ext_iff` 📖	mathematical	—	`nth`	—	`ext`
`flatMap_mk` 📖	mathematical	—	`flatMap`	—	—
`head_cons` 📖	mathematical	—	`head` `cons`	—	`Quotient.ind'`
`head_map` 📖	mathematical	—	`head` `map` `Turing.PointedMap.f`	—	`cons_head_tail` `Quotient.inductionOn'`
`head_mk` 📖	mathematical	—	`head` `List.headI`	—	—
`induction_on` 📖	—	—	—	—	`Quotient.inductionOn'`
`map_cons` 📖	mathematical	—	`map` `cons` `Turing.PointedMap.f`	—	`cons_head_tail` `head_map` `head_cons` `tail_map` `tail_cons`
`map_mk` 📖	mathematical	—	`map` `Turing.PointedMap.f`	—	—
`map_modifyNth` 📖	mathematical	`Turing.PointedMap.f`	`map` `modifyNth`	—	`map_cons` `head_map` `tail_map`
`nth_map` 📖	mathematical	—	`nth` `map` `Turing.PointedMap.f`	—	`induction_on` `List.getD_map` `Turing.PointedMap.map_pt`
`nth_mk` 📖	mathematical	—	`nth` `List.getI`	—	—
`nth_modifyNth` 📖	mathematical	—	`nth` `modifyNth`	—	`nth_zero` `head_cons` `nth_succ` `tail_cons`
`nth_succ` 📖	mathematical	—	`nth` `tail`	—	`cons_head_tail` `Quotient.inductionOn'`
`nth_zero` 📖	mathematical	—	`nth` `head`	—	`cons_head_tail` `Quotient.inductionOn'`
`tail_cons` 📖	mathematical	—	`tail` `cons`	—	`Quotient.ind'`
`tail_map` 📖	mathematical	—	`tail` `map`	—	`cons_head_tail` `Quotient.inductionOn'`
`tail_mk` 📖	mathematical	—	`tail`	—	—

Turing.PointedMap

Definitions

Name	Category	Theorems
`f` 📖	CompOp	13 math math: `headI_map`, `Turing.ListBlank.head_map`, `Turing.ListBlank.map_mk`, `map_pt'`, `Turing.TM0.map_init`, `Turing.ListBlank.map_cons`, `Turing.Tape.map_fst`, `Turing.Tape.map_mk₁`, `Turing.Tape.map_mk₂`, `Turing.Tape.map_write`, `Turing.ListBlank.nth_map`, `mk_val`, `map_pt`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`headI_map` 📖	mathematical	—	`List.headI` `f`	—	`map_pt`
`map_pt` 📖	mathematical	—	`f`	—	`map_pt'`
`map_pt'` 📖	mathematical	—	`f`	—	—
`mk_val` 📖	mathematical	—	`f`	—	—

Turing.TM0.Cfg

Definitions

Name	Category	Theorems
`Tape` 📖	CompOp	—

Turing.TM1.Cfg

Definitions

Name	Category	Theorems
`Tape` 📖	CompOp	—

Turing.Tape

Definitions

Name	Category	Theorems
`head` 📖	CompOp	5 math math: `move_right_n_head`, `nth_zero`, `write_self`, `mk'_head`, `map_fst`
`inhabited` 📖	CompOp	—
`left` 📖	CompOp	2 math math: `mk'_left_right₀`, `mk'_left`
`left₀` 📖	CompOp	—
`map` 📖	CompOp	6 math math: `map_fst`, `map_mk₁`, `map_mk'`, `map_mk₂`, `map_write`, `map_move`
`mk'` 📖	CompOp	16 math math: `Turing.TM2to1.tr_respects_aux₁`, `move_left_mk'`, `Turing.TM1to1.trTape_mk'`, `mk'_left_right₀`, `mk'_left`, `Turing.TM2to1.tr_respects_aux₃`, `write_move_right_n`, `exists_mk'`, `write_mk'`, `mk'_head`, `mk'_right₀`, `map_mk'`, `mk'_nth_nat`, `move_right_mk'`, `Turing.TM2to1.tr_respects_aux₂`, `mk'_right`
`mk₁` 📖	CompOp	1 math math: `map_mk₁`
`mk₂` 📖	CompOp	1 math math: `map_mk₂`
`move` 📖	CompOp	15 math math: `Turing.TM2to1.tr_respects_aux₁`, `move_right_n_head`, `move_left_mk'`, `Turing.TM2to1.tr_respects_aux₃`, `write_move_right_n`, `move_right_nth`, `move_left_right`, `move_right_left`, `move_left_nth`, `Turing.TM1to1.trTape'_move_left`, `Turing.TM1to1.stepAux_move`, `map_move`, `move_right_mk'`, `Turing.TM1to1.trTape'_move_right`, `Turing.TM2to1.tr_respects_aux₂`
`nth` 📖	CompOp	7 math math: `move_right_n_head`, `nth_zero`, `move_right_nth`, `move_left_nth`, `mk'_nth_nat`, `right₀_nth`, `write_nth`
`right` 📖	CompOp	1 math math: `mk'_right`
`right₀` 📖	CompOp	3 math math: `mk'_left_right₀`, `mk'_right₀`, `right₀_nth`
`write` 📖	CompOp	6 math math: `write_move_right_n`, `write_self`, `write_mk'`, `write_mk`, `map_write`, `write_nth`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_mk'` 📖	mathematical	—	`mk'`	—	`mk'_left_right₀`
`map_fst` 📖	mathematical	—	`head` `map` `Turing.PointedMap.f`	—	—
`map_mk'` 📖	mathematical	—	`map` `mk'` `Turing.ListBlank.map`	—	`Turing.ListBlank.head_map` `Turing.ListBlank.tail_map`
`map_mk₁` 📖	mathematical	—	`map` `mk₁` `Turing.PointedMap.f`	—	`map_mk₂`
`map_mk₂` 📖	mathematical	—	`map` `mk₂` `Turing.PointedMap.f`	—	`map_mk'`
`map_move` 📖	mathematical	—	`map` `move`	—	`Turing.ListBlank.map_cons` `Turing.ListBlank.head_map` `Turing.ListBlank.tail_map`
`map_write` 📖	mathematical	—	`map` `write` `Turing.PointedMap.f`	—	—
`mk'_head` 📖	mathematical	—	`head` `mk'` `Turing.ListBlank.head`	—	—
`mk'_left` 📖	mathematical	—	`left` `mk'`	—	—
`mk'_left_right₀` 📖	mathematical	—	`mk'` `left` `right₀`	—	`Turing.ListBlank.head_cons` `Turing.ListBlank.tail_cons`
`mk'_nth_nat` 📖	mathematical	—	`nth` `mk'` `Turing.ListBlank.nth`	—	`right₀_nth` `mk'_right₀`
`mk'_right` 📖	mathematical	—	`right` `mk'` `Turing.ListBlank.tail`	—	—
`mk'_right₀` 📖	mathematical	—	`right₀` `mk'`	—	`Turing.ListBlank.cons_head_tail`
`move_left_mk'` 📖	mathematical	—	`move` `Turing.Dir.left` `mk'` `Turing.ListBlank.tail` `Turing.ListBlank.cons` `Turing.ListBlank.head`	—	`Turing.ListBlank.cons_head_tail` `Turing.ListBlank.head_cons` `Turing.ListBlank.tail_cons`
`move_left_nth` 📖	mathematical	—	`nth` `move` `Turing.Dir.left`	—	`Turing.ListBlank.nth_succ` `Turing.ListBlank.nth_zero` `Turing.ListBlank.head_cons` `add_sub_cancel_right` `Turing.ListBlank.tail_cons`
`move_left_right` 📖	mathematical	—	`move` `Turing.Dir.right` `Turing.Dir.left`	—	`Turing.ListBlank.head_cons` `Turing.ListBlank.cons_head_tail` `Turing.ListBlank.tail_cons`
`move_right_left` 📖	mathematical	—	`move` `Turing.Dir.left` `Turing.Dir.right`	—	`Turing.ListBlank.head_cons` `Turing.ListBlank.tail_cons` `Turing.ListBlank.cons_head_tail`
`move_right_mk'` 📖	mathematical	—	`move` `Turing.Dir.right` `mk'` `Turing.ListBlank.cons` `Turing.ListBlank.head` `Turing.ListBlank.tail`	—	—
`move_right_n_head` 📖	mathematical	—	`head` `Nat.iterate` `Turing.Tape` `move` `Turing.Dir.right` `nth`	—	`move_right_nth`
`move_right_nth` 📖	mathematical	—	`nth` `move` `Turing.Dir.right`	—	`move_right_left` `move_left_nth` `add_sub_cancel_right`
`nth_zero` 📖	mathematical	—	`nth` `head`	—	—
`right₀_nth` 📖	mathematical	—	`Turing.ListBlank.nth` `right₀` `nth`	—	`Turing.ListBlank.nth_zero` `Turing.ListBlank.head_cons` `Turing.ListBlank.nth_succ` `Turing.ListBlank.tail_cons`
`write_mk` 📖	mathematical	—	`write`	—	—
`write_mk'` 📖	mathematical	—	`write` `mk'` `Turing.ListBlank.cons` `Turing.ListBlank.tail`	—	`Turing.ListBlank.head_cons` `Turing.ListBlank.tail_cons`
`write_move_right_n` 📖	mathematical	—	`write` `Turing.ListBlank.nth` `Nat.iterate` `Turing.Tape` `move` `Turing.Dir.right` `mk'` `Turing.ListBlank.modifyNth`	—	`Turing.ListBlank.nth_zero` `write_mk'` `Turing.ListBlank.nth_succ` `move_right_mk'` `Turing.ListBlank.head_cons` `Turing.ListBlank.tail_cons`
`write_nth` 📖	mathematical	—	`nth` `write`	—	—
`write_self` 📖	mathematical	—	`write` `head`	—	—

Turing.instInhabitedDir

Definitions

Name	Category	Theorems
`default` 📖	CompOp	—

---

← Back to Index