---

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

.....upcase..... 
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)
⊢ primrec(n;f o p-id();λi,g. f o g) x ~ primrec(n;p-id();λi,g. f o g) outl(f x)
BY
{ TACTIC:((RWO "primrec-unroll" 0 THENA Auto) THEN (SplitOnConclITE THENA Auto)) }

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

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

---

Latex:

---

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


By

---

Latex:
TACTIC:((RWO  "primrec-unroll"  0  THENA  Auto)  THEN  (SplitOnConclITE  THENA  Auto))

---

Home Index