---

Step * 1 1 1 of Lemma canonicalizable-baire-direct

.....assertion..... 
1. f : Base
2. f1 : Base
3. f = f1 ∈ (ℕ ⟶ ℕ)
⊢ λn.if (n) < (0)  then ⊥  else (f n) ~ λn.if (n) < (0)  then ⊥  else (f1 n)
BY
{ (SqEqCD
   THEN SqequalSqle
   THEN AssumeHasValue
   THEN Try (HasValueD (-1))
   THEN Try (ExceptionCases (-1))
   THEN Try (Complete (SameException))
   THEN Try (Complete ((AutoSplit
                        THEN (Assert ⌜(f n) = (f1 n) ∈ ℕ⌝⋅ THENA EquationFromSomeHyp Auto)
                        THEN HypSubst' (-1) 0
                        THEN Auto)))) }

---

Latex:

---

Latex:
.....assertion..... 
1.  f  :  Base
2.  f1  :  Base
3.  f  =  f1
\mvdash{}  \mlambda{}n.if  (n)  <  (0)    then  \mbot{}    else  (f  n)  \msim{}  \mlambda{}n.if  (n)  <  (0)    then  \mbot{}    else  (f1  n)


By

---

Latex:
(SqEqCD
  THEN  SqequalSqle
  THEN  AssumeHasValue
  THEN  Try  (HasValueD  (-1))
  THEN  Try  (ExceptionCases  (-1))
  THEN  Try  (Complete  (SameException))
  THEN  Try  (Complete  ((AutoSplit
                                            THEN  (Assert  \mkleeneopen{}(f  n)  =  (f1  n)\mkleeneclose{}\mcdot{}  THENA  EquationFromSomeHyp  Auto)
                                            THEN  HypSubst'  (-1)  0
                                            THEN  Auto))))

---

Home Index