---

Step * of Lemma canonicalizable-baire-direct

canonicalizable(ℕ ⟶ ℕ)
BY
{ TACTIC:(Unfold `canonicalizable` 0
          THEN InstConcl [⌜λf,n. if (n) < (0)  then ⊥  else (f n)⌝]⋅
          THEN Reduce 0
          THEN Try (CpltAuto)) }

1
.....wf..... 
λf,n. if (n) < (0)  then ⊥  else (f n) ∈ (ℕ ⟶ ℕ) ⟶ Base

---

Latex:

---

Latex:
canonicalizable(\mBbbN{}  {}\mrightarrow{}  \mBbbN{})


By

---

Latex:
TACTIC:(Unfold  `canonicalizable`  0
                THEN  InstConcl  [\mkleeneopen{}\mlambda{}f,n.  if  (n)  <  (0)    then  \mbot{}    else  (f  n)\mkleeneclose{}]\mcdot{}
                THEN  Reduce  0
                THEN  Try  (CpltAuto))

---

Home Index