Theorems · Theorem · logic and foundations

Turing.ToPartrec.Code.brecOn.eq

∀ {motive : Turing.ToPartrec.Code → Sort u} (t : Turing.ToPartrec.Code)
  (F_1 : (t : Turing.ToPartrec.Code) → Turing.ToPartrec.Code.below t → motive t),
  Turing.ToPartrec.Code.brecOn t F_1 = F_1 t (Turing.ToPartrec.Code.brecOn.go t F_1).2

Defined in: Mathlib.Computability.TuringMachine.Config
Cited by: 4 results in Mathlib
Foundations: Depth 6 from the axioms · uses no axioms

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites5

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

Turing.ToPartrec.Codestatement and proof · cited by 83
Turing.ToPartrec.Code.brecOn.gostatement · cited by 5
Turing.ToPartrec.Code.belowstatement and proof · cited by 5
Turing.ToPartrec.Code.casesOnproof · cited by 2
Turing.ToPartrec.Code.brecOnstatement and proof · cited by 1

Cited by4

Results whose statement or proof uses this declaration.

Turing.ToPartrec.stepNormal.eq_defproof · cited by 0
Turing.PartrecToTM2.trNormal.eq_defproof · cited by 0
Turing.PartrecToTM2.codeSupp'.eq_defproof · cited by 0
Turing.ToPartrec.Code.eval.eq_defproof · cited by 0