---

Step * 1 2 1 of Lemma p-fun-exp-add1-sq

.....truecase..... 
1. A : Type
2. f : A ⟶ (A + Top)
3. x : A
4. ↑isl(f x)
5. n : ℤ
6. 0 < n
7. primrec(n - 1;f o p-id();λi,g. f o g) x ~ primrec(n - 1;p-id();λi,g. f o g) outl(f x)
8. n = 0 ∈ ℤ
⊢ f o p-id() x ~ p-id() outl(f x)
BY
{ TACTIC:Auto' }

---

Latex:

---

Latex:
.....truecase..... 
1.  A  :  Type
2.  f  :  A  {}\mrightarrow{}  (A  +  Top)
3.  x  :  A
4.  \muparrow{}isl(f  x)
5.  n  :  \mBbbZ{}
6.  0  <  n
7.  primrec(n  -  1;f  o  p-id();\mlambda{}i,g.  f  o  g)  x  \msim{}  primrec(n  -  1;p-id();\mlambda{}i,g.  f  o  g)  outl(f  x)
8.  n  =  0
\mvdash{}  f  o  p-id()  x  \msim{}  p-id()  outl(f  x)


By

---

Latex:
TACTIC:Auto'

---

Home Index