Step
*
1
1
1
1
1
1
of Lemma
pcw-pp-lemma
1. P : Type@i'
2. A : P ⟶ Type@i'
3. B : p:P ⟶ A[p] ⟶ Type@i'
4. C : p:P ⟶ a:A[p] ⟶ B[p;a] ⟶ P@i
5. par : P@i
6. w : pW par@i
7. n : ℤ
8. 0 < n
9. ∀m:ℕn - 1. ∀ss:ℕn - 1 ⟶ pcw-step(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b]).
((∀x:ℕn - 1. (param-W-rel(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b];par;w) x ss (ss x)))
⇒ (fst(snd((ss m))) ∈ pW (fst((ss m)))))
10. m : ℕn@i
11. ss : ℕn ⟶ pcw-step(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b])@i
12. ∀x:ℕn. (param-W-rel(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b];par;w) x ss (ss x))
13. p : P@i
14. w1 : pco-W p@i
15. v2 : B[p;fst(w1)]?@i
16. (ss m) = <p, w1, v2> ∈ pcw-step(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b])
17. 0 < m
18. fst(snd((ss (m - 1)))) ∈ pW (fst((ss (m - 1))))
19. pW ≡ λp.(a:A[p] × (b:B[p;a] ⟶ (pW C[p;a;b])))
20. p1 : P@i
21. a : A[p1]
22. w3 : b:B[p1;a] ⟶ (pco-W C[p1;a;b])
23. x : B[p1;fst(<a, w3>)]@i
24. (ss (m - 1)) = <p1, <a, w3>, inl x> ∈ pcw-step(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b])
25. pco-W ∈ P ⟶ Type
26. True
27. p = C[p1;a;x] ∈ P
28. w1 = (w3 x) ∈ (pco-W C[p1;a;x])
⊢ <a, w3> ∈ pW p1
BY
{ TACTIC:((Assert ((ss (m - 1)) = <p1, <a, w3>, inl x> ∈ pcw-step(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b]))
∧ (fst(snd((ss (m - 1)))) ∈ pW (fst((ss (m - 1))))) BY
Auto)
THEN D -1
THEN skip{(RepUR ``param-W`` -1 THEN RepUR ``param-W`` 0 THEN (MemTypeHD (-1) THENA Auto) THEN MemTypeCD)}) }
1
1. P : Type@i'
2. A : P ⟶ Type@i'
3. B : p:P ⟶ A[p] ⟶ Type@i'
4. C : p:P ⟶ a:A[p] ⟶ B[p;a] ⟶ P@i
5. par : P@i
6. w : pW par@i
7. n : ℤ
8. 0 < n
9. ∀m:ℕn - 1. ∀ss:ℕn - 1 ⟶ pcw-step(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b]).
((∀x:ℕn - 1. (param-W-rel(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b];par;w) x ss (ss x)))
⇒ (fst(snd((ss m))) ∈ pW (fst((ss m)))))
10. m : ℕn@i
11. ss : ℕn ⟶ pcw-step(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b])@i
12. ∀x:ℕn. (param-W-rel(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b];par;w) x ss (ss x))
13. p : P@i
14. w1 : pco-W p@i
15. v2 : B[p;fst(w1)]?@i
16. (ss m) = <p, w1, v2> ∈ pcw-step(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b])
17. 0 < m
18. fst(snd((ss (m - 1)))) ∈ pW (fst((ss (m - 1))))
19. pW ≡ λp.(a:A[p] × (b:B[p;a] ⟶ (pW C[p;a;b])))
20. p1 : P@i
21. a : A[p1]
22. w3 : b:B[p1;a] ⟶ (pco-W C[p1;a;b])
23. x : B[p1;fst(<a, w3>)]@i
24. (ss (m - 1)) = <p1, <a, w3>, inl x> ∈ pcw-step(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b])
25. pco-W ∈ P ⟶ Type
26. True
27. p = C[p1;a;x] ∈ P
28. w1 = (w3 x) ∈ (pco-W C[p1;a;x])
29. (ss (m - 1)) = <p1, <a, w3>, inl x> ∈ pcw-step(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b])
30. fst(snd((ss (m - 1)))) ∈ pW (fst((ss (m - 1))))
⊢ <a, w3> ∈ pW p1
Latex:
Latex:
1. P : Type@i'
2. A : P {}\mrightarrow{} Type@i'
3. B : p:P {}\mrightarrow{} A[p] {}\mrightarrow{} Type@i'
4. C : p:P {}\mrightarrow{} a:A[p] {}\mrightarrow{} B[p;a] {}\mrightarrow{} P@i
5. par : P@i
6. w : pW par@i
7. n : \mBbbZ{}
8. 0 < n
9. \mforall{}m:\mBbbN{}n - 1. \mforall{}ss:\mBbbN{}n - 1 {}\mrightarrow{} pcw-step(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b]).
((\mforall{}x:\mBbbN{}n - 1. (param-W-rel(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b];par;w) x ss (ss x)))
{}\mRightarrow{} (fst(snd((ss m))) \mmember{} pW (fst((ss m)))))
10. m : \mBbbN{}n@i
11. ss : \mBbbN{}n {}\mrightarrow{} pcw-step(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b])@i
12. \mforall{}x:\mBbbN{}n. (param-W-rel(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b];par;w) x ss (ss x))
13. p : P@i
14. w1 : pco-W p@i
15. v2 : B[p;fst(w1)]?@i
16. (ss m) = <p, w1, v2>
17. 0 < m
18. fst(snd((ss (m - 1)))) \mmember{} pW (fst((ss (m - 1))))
19. pW \mequiv{} \mlambda{}p.(a:A[p] \mtimes{} (b:B[p;a] {}\mrightarrow{} (pW C[p;a;b])))
20. p1 : P@i
21. a : A[p1]
22. w3 : b:B[p1;a] {}\mrightarrow{} (pco-W C[p1;a;b])
23. x : B[p1;fst(<a, w3>)]@i
24. (ss (m - 1)) = <p1, <a, w3>, inl x>
25. pco-W \mmember{} P {}\mrightarrow{} Type
26. True
27. p = C[p1;a;x]
28. w1 = (w3 x)
\mvdash{} <a, w3> \mmember{} pW p1
By
Latex:
TACTIC:((Assert ((ss (m - 1)) = <p1, <a, w3>, inl x>)
\mwedge{} (fst(snd((ss (m - 1)))) \mmember{} pW (fst((ss (m - 1))))) BY
Auto)
THEN D -1
THEN skip\{(RepUR ``param-W`` -1
THEN RepUR ``param-W`` 0
THEN (MemTypeHD (-1) THENA Auto)
THEN MemTypeCD)\})
Home
Index