Theorems · Theorem · logic and foundations

Turing.PartrecToTM2.codeSupp_cons

∀ (f fs : Turing.ToPartrec.Code) (k : Turing.PartrecToTM2.Cont'),
  Turing.PartrecToTM2.codeSupp (f.cons fs) k =
    Turing.PartrecToTM2.trStmts₁ (Turing.PartrecToTM2.trNormal (f.cons fs) k) ∪
      Turing.PartrecToTM2.codeSupp f (Turing.PartrecToTM2.Cont'.cons₁ fs k)

Defined in: Mathlib.Computability.TuringMachine.ToPartrec
Cited by: 2 results in Mathlib
Foundations: Depth 81 from the axioms · uses propext, Classical.choice, Quot.sound

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites13

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Finsetstatement · cited by 13,712
Turing.PartrecToTM2.Λ'statement · cited by 85
Turing.ToPartrec.Codestatement and proof · cited by 83
Turing.PartrecToTM2.Γ'proof · cited by 83
Turing.PartrecToTM2.Cont'statement and proof · cited by 51
Turing.PartrecToTM2.trNormalstatement and proof · cited by 23
Turing.PartrecToTM2.trStmts₁statement and proof · cited by 23
Turing.PartrecToTM2.contSuppproof · cited by 18
Turing.PartrecToTM2.codeSuppstatement · cited by 16
Turing.PartrecToTM2.headproof · cited by 14
Turing.PartrecToTM2.codeSupp'proof · cited by 13
Turing.PartrecToTM2.move₂proof · cited by 10

Cited by2

Results whose statement or proof uses this declaration.

Turing.PartrecToTM2.codeSupp'_supportsproof · cited by 2
Turing.PartrecToTM2.trNormal_supportsproof · cited by 2