Step
*
2
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
{ (OrRight 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. \mneg{}0 < n
\mvdash{} Dec(0 < n \mwedge{} let p,w,d = p1 (n - 1) in \muparrow{}isr(d))
By
Latex:
(OrRight THEN Auto)
Home
Index