---

Step * 1 of Lemma decidable__pcw-pp-barred


1. [P] : Type
2. [A] : P ⟶ Type
3. [B] : p:P ⟶ A[p] ⟶ Type
4. [C] : p:P ⟶ a:A[p] ⟶ B[p;a] ⟶ P
5. n : ℤ
6. n ≥ 0 
7. p1 : ℕn ⟶ pcw-step(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b])
8. 0 < n
⊢ Dec(0 < n ∧ let p,w,d = p1 (n - 1) in ↑isr(d))
BY
{ ((GenConclTerm ⌜p1 (n - 1)⌝⋅ THENA Auto) THEN RepeatFor 3 (D -2) THEN Reduce 0 THEN Auto) }

---

Latex:

---

Latex:

1.  [P]  :  Type
2.  [A]  :  P  {}\mrightarrow{}  Type
3.  [B]  :  p:P  {}\mrightarrow{}  A[p]  {}\mrightarrow{}  Type
4.  [C]  :  p:P  {}\mrightarrow{}  a:A[p]  {}\mrightarrow{}  B[p;a]  {}\mrightarrow{}  P
5.  n  :  \mBbbZ{}
6.  n  \mgeq{}  0 
7.  p1  :  \mBbbN{}n  {}\mrightarrow{}  pcw-step(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b])
8.  0  <  n
\mvdash{}  Dec(0  <  n  \mwedge{}  let  p,w,d  =  p1  (n  -  1)  in  \muparrow{}isr(d))


By

---

Latex:
((GenConclTerm  \mkleeneopen{}p1  (n  -  1)\mkleeneclose{}\mcdot{}  THENA  Auto)  THEN  RepeatFor  3  (D  -2)  THEN  Reduce  0  THEN  Auto)

---

Home Index