---

Step * of Lemma decidable__pcw-pp-barred

∀[P:Type]. ∀[A:P ⟶ Type]. ∀[B:p:P ⟶ A[p] ⟶ Type]. ∀[C:p:P ⟶ a:A[p] ⟶ B[p;a] ⟶ P].
  ∀pp:n:ℕ × (ℕn ⟶ pcw-step(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b])). Dec(Barred(pp))
BY
{ (Auto THEN D -1 THEN D -2 THEN RepUR ``pcw-pp-barred`` 0 THEN (Decide ⌜0 < n⌝⋅ THENA Auto)) }

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

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

---

Latex:

---

Latex:
\mforall{}[P:Type].  \mforall{}[A:P  {}\mrightarrow{}  Type].  \mforall{}[B:p:P  {}\mrightarrow{}  A[p]  {}\mrightarrow{}  Type].  \mforall{}[C:p:P  {}\mrightarrow{}  a:A[p]  {}\mrightarrow{}  B[p;a]  {}\mrightarrow{}  P].
    \mforall{}pp:n:\mBbbN{}  \mtimes{}  (\mBbbN{}n  {}\mrightarrow{}  pcw-step(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b])).  Dec(Barred(pp))


By

---

Latex:
(Auto  THEN  D  -1  THEN  D  -2  THEN  RepUR  ``pcw-pp-barred``  0  THEN  (Decide  \mkleeneopen{}0  <  n\mkleeneclose{}\mcdot{}  THENA  Auto))

---

Home Index