---

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

.....falsecase..... 
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 ∈ ℤ)
⊢ (λi,g. f o g) (n - 1) primrec(n - 1;f o p-id();λi,g. f o g) x ~ (λi,g. f o g) (n - 1) primrec(n - 1;p-id();λi,g. f o g\000C) outl(f x)
BY
{ (Reduce 0 THEN RW (SubC (AddrC [1] (UnfoldTopAbC))) 0 THEN RepUR ``can-apply do-apply`` 0 THEN ProveSqEq) }

---

Latex:

---

Latex:
.....falsecase..... 
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.  \mneg{}(n  =  0)
\mvdash{}  (\mlambda{}i,g.  f  o  g)  (n  -  1)  primrec(n  -  1;f  o  p-id();\mlambda{}i,g.  f  o  g)  x  \msim{}  (\mlambda{}i,g.  f  o  g)  (n  -  1) 
                                                                                                                    primrec(n  -  1;p-id();\mlambda{}i,g.  f  o  g) 
                                                                                                                    outl(f  x)


By

---

Latex:
(Reduce  0
  THEN  RW  (SubC  (AddrC  [1]  (UnfoldTopAbC)))  0
  THEN  RepUR  ``can-apply  do-apply``  0
  THEN  ProveSqEq)

---

Home Index