Step
*
3
1
1
1
1
1
of Lemma
pW-rec_wf
.....assertion.....
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. pcw-step(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b]) ∈ Type
6. pW ∈ P ⟶ Type
7. Q : par:P ⟶ (pW par) ⟶ ℙ
8. ind : par:P
⟶ a:A[par]
⟶ f:(b:B[par;a] ⟶ (pW C[par;a;b]))
⟶ (b:B[par;a] ⟶ Q[C[par;a;b];f b])
⟶ Q[par;pW-sup(a;f)]
9. par : P
10. w : pW par
11. param-W-rel(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b];par;w) ∈ n:ℕ
⟶ (ℕn ⟶ pcw-step(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b]))
⟶ pcw-step(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b])
⟶ ℙ
12. ∀[pp:n:ℕ × (ℕn ⟶ pcw-step(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b]))]. (Barred(pp) ∈ ℙ)
13. n : ℕ
14. s : ℕn ⟶ pcw-step(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b])
15. ∀%6:ℕn. (param-W-rel(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b];par;w) %6 s (s %6))
16. ∀t:{t:pcw-step(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b])| param-W-rel(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b];par;w) n s t}
(let q,w',d = t in
case d
of inl(b) =>
let a,f = w'
in let ind(p,a,f,G) = ind[p;a;f;G] in
letrec F(p,w) = let a,f=w in
ind(p,a,f,λb.F(C[p;a;b],f(b)) in
F(C[q;a;b];f b)
| inr(z) =>
Ax ∈ let q,w',d = t in
case d of inl(b) => let a,f = w' in Q[C[q;a;b];f b] | inr(z) => True)
17. 0 < n
18. p : P
19. a : A[p]
20. w2 : b:B[p;a] ⟶ (pco-W C[p;a;b])
21. x : B[p;fst(<a, w2>)]
22. (s (n - 1)) = <p, <a, w2>, inl x> ∈ pcw-step(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b])
23. pco-W ∈ P ⟶ Type
24. v : P
25. C[p;a;x] = v ∈ P
26. a1 : A[v]
27. z1 : b:B[v;a1] ⟶ (pco-W C[v;a1;b])
28. (w2 x) = <a1, z1> ∈ (pco-W v)
⊢ z1 ∈ b:B[v;a1] ⟶ (pW C[v;a1;b])
BY
{ TACTIC:(Assert w2 ∈ b:B[p;a] ⟶ (pW C[p;a;b]) BY
((InstLemma `param-W-ext` [⌜P⌝;⌜A⌝;⌜B⌝;⌜C⌝]⋅ THENA Auto)
THEN (With ⌜p⌝ (D (-1))⋅ THENA Auto)
THEN Reduce (-1)
THEN (Assert ⌜<a, w2> ∈ a:A[p] × (b:B[p;a] ⟶ (pW C[p;a;b]))⌝⋅
THENM (MemHD (-1) THEN All Reduce THEN Auto)
)
THEN SubsumeC ⌜pW p⌝⋅)⋅) }
1
.....aux.....
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. pcw-step(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b]) ∈ Type
6. pW ∈ P ⟶ Type
7. Q : par:P ⟶ (pW par) ⟶ ℙ
8. ind : par:P
⟶ a:A[par]
⟶ f:(b:B[par;a] ⟶ (pW C[par;a;b]))
⟶ (b:B[par;a] ⟶ Q[C[par;a;b];f b])
⟶ Q[par;pW-sup(a;f)]
9. par : P
10. w : pW par
11. param-W-rel(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b];par;w) ∈ n:ℕ
⟶ (ℕn ⟶ pcw-step(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b]))
⟶ pcw-step(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b])
⟶ ℙ
12. ∀[pp:n:ℕ × (ℕn ⟶ pcw-step(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b]))]. (Barred(pp) ∈ ℙ)
13. n : ℕ
14. s : ℕn ⟶ pcw-step(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b])
15. ∀%6:ℕn. (param-W-rel(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b];par;w) %6 s (s %6))
16. ∀t:{t:pcw-step(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b])| param-W-rel(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b];par;w) n s t}
(let q,w',d = t in
case d
of inl(b) =>
let a,f = w'
in let ind(p,a,f,G) = ind[p;a;f;G] in
letrec F(p,w) = let a,f=w in
ind(p,a,f,λb.F(C[p;a;b],f(b)) in
F(C[q;a;b];f b)
| inr(z) =>
Ax ∈ let q,w',d = t in
case d of inl(b) => let a,f = w' in Q[C[q;a;b];f b] | inr(z) => True)
17. 0 < n
18. p : P
19. a : A[p]
20. w2 : b:B[p;a] ⟶ (pco-W C[p;a;b])
21. x : B[p;fst(<a, w2>)]
22. (s (n - 1)) = <p, <a, w2>, inl x> ∈ pcw-step(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b])
23. pco-W ∈ P ⟶ Type
24. v : P
25. C[p;a;x] = v ∈ P
26. a1 : A[v]
27. z1 : b:B[v;a1] ⟶ (pco-W C[v;a1;b])
28. (w2 x) = <a1, z1> ∈ (pco-W v)
29. pW p ≡ a:A[p] × (b:B[p;a] ⟶ (pW C[p;a;b]))
⊢ <a, w2> ∈ pW p
2
.....aux.....
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. pcw-step(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b]) ∈ Type
6. pW ∈ P ⟶ Type
7. Q : par:P ⟶ (pW par) ⟶ ℙ
8. ind : par:P
⟶ a:A[par]
⟶ f:(b:B[par;a] ⟶ (pW C[par;a;b]))
⟶ (b:B[par;a] ⟶ Q[C[par;a;b];f b])
⟶ Q[par;pW-sup(a;f)]
9. par : P
10. w : pW par
11. param-W-rel(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b];par;w) ∈ n:ℕ
⟶ (ℕn ⟶ pcw-step(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b]))
⟶ pcw-step(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b])
⟶ ℙ
12. ∀[pp:n:ℕ × (ℕn ⟶ pcw-step(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b]))]. (Barred(pp) ∈ ℙ)
13. n : ℕ
14. s : ℕn ⟶ pcw-step(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b])
15. ∀%6:ℕn. (param-W-rel(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b];par;w) %6 s (s %6))
16. ∀t:{t:pcw-step(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b])| param-W-rel(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b];par;w) n s t}
(let q,w',d = t in
case d
of inl(b) =>
let a,f = w'
in let ind(p,a,f,G) = ind[p;a;f;G] in
letrec F(p,w) = let a,f=w in
ind(p,a,f,λb.F(C[p;a;b],f(b)) in
F(C[q;a;b];f b)
| inr(z) =>
Ax ∈ let q,w',d = t in
case d of inl(b) => let a,f = w' in Q[C[q;a;b];f b] | inr(z) => True)
17. 0 < n
18. p : P
19. a : A[p]
20. w2 : b:B[p;a] ⟶ (pco-W C[p;a;b])
21. x : B[p;fst(<a, w2>)]
22. (s (n - 1)) = <p, <a, w2>, inl x> ∈ pcw-step(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b])
23. pco-W ∈ P ⟶ Type
24. v : P
25. C[p;a;x] = v ∈ P
26. a1 : A[v]
27. z1 : b:B[v;a1] ⟶ (pco-W C[v;a1;b])
28. (w2 x) = <a1, z1> ∈ (pco-W v)
29. pW p ≡ a:A[p] × (b:B[p;a] ⟶ (pW C[p;a;b]))
30. <a, w2> = <a, w2> ∈ (pW p)
⊢ (pW p) ⊆r (a:A[p] × (b:B[p;a] ⟶ (pW C[p;a;b])))
3
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. pcw-step(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b]) ∈ Type
6. pW ∈ P ⟶ Type
7. Q : par:P ⟶ (pW par) ⟶ ℙ
8. ind : par:P
⟶ a:A[par]
⟶ f:(b:B[par;a] ⟶ (pW C[par;a;b]))
⟶ (b:B[par;a] ⟶ Q[C[par;a;b];f b])
⟶ Q[par;pW-sup(a;f)]
9. par : P
10. w : pW par
11. param-W-rel(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b];par;w) ∈ n:ℕ
⟶ (ℕn ⟶ pcw-step(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b]))
⟶ pcw-step(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b])
⟶ ℙ
12. ∀[pp:n:ℕ × (ℕn ⟶ pcw-step(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b]))]. (Barred(pp) ∈ ℙ)
13. n : ℕ
14. s : ℕn ⟶ pcw-step(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b])
15. ∀%6:ℕn. (param-W-rel(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b];par;w) %6 s (s %6))
16. ∀t:{t:pcw-step(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b])| param-W-rel(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b];par;w) n s t}
(let q,w',d = t in
case d
of inl(b) =>
let a,f = w'
in let ind(p,a,f,G) = ind[p;a;f;G] in
letrec F(p,w) = let a,f=w in
ind(p,a,f,λb.F(C[p;a;b],f(b)) in
F(C[q;a;b];f b)
| inr(z) =>
Ax ∈ let q,w',d = t in
case d of inl(b) => let a,f = w' in Q[C[q;a;b];f b] | inr(z) => True)
17. 0 < n
18. p : P
19. a : A[p]
20. w2 : b:B[p;a] ⟶ (pco-W C[p;a;b])
21. x : B[p;fst(<a, w2>)]
22. (s (n - 1)) = <p, <a, w2>, inl x> ∈ pcw-step(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b])
23. pco-W ∈ P ⟶ Type
24. v : P
25. C[p;a;x] = v ∈ P
26. a1 : A[v]
27. z1 : b:B[v;a1] ⟶ (pco-W C[v;a1;b])
28. (w2 x) = <a1, z1> ∈ (pco-W v)
29. w2 ∈ b:B[p;a] ⟶ (pW C[p;a;b])
⊢ z1 ∈ b:B[v;a1] ⟶ (pW C[v;a1;b])
Latex:
Latex:
.....assertion.....
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. pcw-step(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b]) \mmember{} Type
6. pW \mmember{} P {}\mrightarrow{} Type
7. Q : par:P {}\mrightarrow{} (pW par) {}\mrightarrow{} \mBbbP{}
8. ind : par:P
{}\mrightarrow{} a:A[par]
{}\mrightarrow{} f:(b:B[par;a] {}\mrightarrow{} (pW C[par;a;b]))
{}\mrightarrow{} (b:B[par;a] {}\mrightarrow{} Q[C[par;a;b];f b])
{}\mrightarrow{} Q[par;pW-sup(a;f)]
9. par : P
10. w : pW par
11. param-W-rel(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b];par;w) \mmember{} n:\mBbbN{}
{}\mrightarrow{} (\mBbbN{}n {}\mrightarrow{} pcw-step(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b]))
{}\mrightarrow{} pcw-step(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b])
{}\mrightarrow{} \mBbbP{}
12. \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]))]. (Barred(pp) \mmember{} \mBbbP{})
13. n : \mBbbN{}
14. s : \mBbbN{}n {}\mrightarrow{} pcw-step(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b])
15. \mforall{}\%6:\mBbbN{}n. (param-W-rel(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b];par;w) \%6 s (s \%6))
16. \mforall{}t:\{t:pcw-step(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b])|
param-W-rel(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b];par;w) n s t\}
(let q,w',d = t in
case d
of inl(b) =>
let a,f = w'
in let ind(p,a,f,G) = ind[p;a;f;G] in
letrec F(p,w) = let a,f=w in
ind(p,a,f,\mlambda{}b.F(C[p;a;b],f(b)) in
F(C[q;a;b];f b)
| inr(z) =>
Ax \mmember{} let q,w',d = t in
case d of inl(b) => let a,f = w' in Q[C[q;a;b];f b] | inr(z) => True)
17. 0 < n
18. p : P
19. a : A[p]
20. w2 : b:B[p;a] {}\mrightarrow{} (pco-W C[p;a;b])
21. x : B[p;fst(<a, w2>)]
22. (s (n - 1)) = <p, <a, w2>, inl x>
23. pco-W \mmember{} P {}\mrightarrow{} Type
24. v : P
25. C[p;a;x] = v
26. a1 : A[v]
27. z1 : b:B[v;a1] {}\mrightarrow{} (pco-W C[v;a1;b])
28. (w2 x) = <a1, z1>
\mvdash{} z1 \mmember{} b:B[v;a1] {}\mrightarrow{} (pW C[v;a1;b])
By
Latex:
TACTIC:(Assert w2 \mmember{} b:B[p;a] {}\mrightarrow{} (pW C[p;a;b]) BY
((InstLemma `param-W-ext` [\mkleeneopen{}P\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}B\mkleeneclose{};\mkleeneopen{}C\mkleeneclose{}]\mcdot{} THENA Auto)
THEN (With \mkleeneopen{}p\mkleeneclose{} (D (-1))\mcdot{} THENA Auto)
THEN Reduce (-1)
THEN (Assert \mkleeneopen{}<a, w2> \mmember{} a:A[p] \mtimes{} (b:B[p;a] {}\mrightarrow{} (pW C[p;a;b]))\mkleeneclose{}\mcdot{}
THENM (MemHD (-1) THEN All Reduce THEN Auto)
)
THEN SubsumeC \mkleeneopen{}pW p\mkleeneclose{}\mcdot{})\mcdot{})
Home
Index