Theorems · Theorem · logic and foundations
Turing.ListBlank.cons_head_tail
∀ {Γ : Type u_1} [inst : Inhabited Γ] (l : Turing.ListBlank Γ), Turing.ListBlank.cons l.head l.tail = lThe cons and head/tail functions are mutually inverse, unlike in the case of List where
this only holds for nonempty lists.
- Defined in
- Mathlib.Computability.TuringMachine.Tape
- Cited by
- 13 results in Mathlib
- Foundations
- Depth 73 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- Inhabited
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites7
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Turing.ListBlankstatement · cited by 68
- Turing.ListBlank.consstatement · cited by 31
- Quotient.sound'proof · cited by 30
- Turing.ListBlank.headstatement · cited by 27
- Turing.ListBlank.tailstatement · cited by 27
- Quotient.ind'proof · cited by 13
- Turing.BlankExtends.reflproof · cited by 2
Cited by13
Results whose statement or proof uses this declaration.
- Turing.ListBlank.nth_succproof · cited by 5
- Turing.ListBlank.nth_zeroproof · cited by 4
- Turing.ListBlank.tail_mapproof · cited by 4
- Turing.ListBlank.head_mapproof · cited by 4
- Turing.ListBlank.map_consproof · cited by 3
- Turing.Tape.mk'_right₀proof · cited by 3
- Turing.Tape.move_left_mk'proof · cited by 3
- Turing.Tape.move_right_leftproof · cited by 3
- Turing.ListBlank.exists_consproof · cited by 3
- Turing.Tape.move_left_rightproof · cited by 2
- Turing.TM1to1.trTape'_move_rightproof · cited by 1
- Turing.TM2to1.addBottom_mapproof · cited by 1