---

Step * 1 1 of Lemma canonicalizable-baire-direct


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)) ∈ Base
BY
{ (Assert ⌜λn.if (n) < (0)  then ⊥  else (f n) ~ λn.if (n) < (0)  then ⊥  else (f1 n)⌝⋅ THENM (RWO "-1" 0 THEN Auto)) }

1
.....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)

---

Latex:

---

Latex:

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


By

---

Latex:
(Assert  \mkleeneopen{}\mlambda{}n.if  (n)  <  (0)    then  \mbot{}    else  (f  n)  \msim{}  \mlambda{}n.if  (n)  <  (0)    then  \mbot{}    else  (f1  n)\mkleeneclose{}\mcdot{}
THENM  (RWO  "-1"  0  THEN  Auto)
)

---

Home Index