Theorems · Definition · logic and foundations
Turing.PartrecToTM2.tr
Turing.PartrecToTM2.Λ' → Turing.PartrecToTM2.Stmt'
The main program. See the section documentation for details.
- Cited by
- 33 results in Mathlib
- Foundations
- Depth 35 from the axioms · uses propext
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites14
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Turing.PartrecToTM2.Λ'statement and proof · cited by 85
- Turing.ToPartrec.Codeproof · cited by 83
- Turing.PartrecToTM2.Γ'proof · cited by 83
- Turing.PartrecToTM2.K'proof · cited by 55
- Turing.PartrecToTM2.Cont'proof · cited by 51
- Turing.PartrecToTM2.trNormalproof · cited by 23
- Turing.PartrecToTM2.Stmt'statement and proof · cited by 21
- Turing.PartrecToTM2.natEndproof · cited by 18
- Turing.PartrecToTM2.headproof · cited by 14
- Turing.PartrecToTM2.unrevproof · cited by 13
- Turing.PartrecToTM2.move₂proof · cited by 10
- Turing.PartrecToTM2.pop'proof · cited by 6
Cited by34
Results whose statement or proof uses this declaration.
- Turing.PartrecToTM2.Supportsproof · cited by 9
- Turing.PartrecToTM2.move_okstatement and proof · cited by 5
- Turing.PartrecToTM2.supports_unionproof · cited by 5
- Turing.PartrecToTM2.clear_okstatement and proof · cited by 4
- Turing.PartrecToTM2.unrev_okstatement · cited by 4
- Turing.PartrecToTM2.ret_supportsstatement · cited by 2
- Turing.PartrecToTM2.supports_singletonstatement and proof · cited by 2
- Turing.PartrecToTM2.trNormal_respectsstatement and proof · cited by 2
- Turing.PartrecToTM2.contSupp_supportsproof · cited by 1
- Turing.PartrecToTM2.copy_okstatement and proof · cited by 1
- Turing.PartrecToTM2.head_main_okstatement and proof · cited by 1
- Turing.PartrecToTM2.head_stack_okstatement and proof · cited by 1