---

Step * 1 1 1 1 1 of Lemma pW-sup_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. pco-W ∈ P ⟶ Type
6. par : P
7. a : A[par]
8. f : b:B[par;a] ⟶ (pW C[par;a;b])
9. pW-sup(a;f) ∈ pco-W par
10. path : Path
11. p : P
12. a1 : A[p]
13. w1 : b:B[p;a1] ⟶ (pco-W C[p;a1;b])
14. x : B[p;a1]
15. (path 0) = <p, <a1, w1>, inl x> ∈ pcw-step(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b])
16. p = par ∈ P
17. <a1, w1> = <a, f> ∈ (pco-W par)
⊢ ↓∃n:ℕ. Barred(pcw-partial(λx.(path (x + 1));n))
BY
{ TACTIC:(DVar `path'
          THEN RenameVar `b' (-4)
          THEN (Assert pco-W par ≡ a:A[par] × (b:B[par;a] ⟶ (pco-W C[par;a;b])) BY
                      (InstLemma `param-co-W-ext` [⌜P⌝;⌜A⌝;⌜B⌝;⌜C⌝]⋅
                       THEN Auto
                       THEN (With ⌜par⌝ (D (-1))⋅ THENA Auto)
                       THEN Reduce (-1)
                       THEN Auto))
          THEN (Assert <a1, w1> = <a, f> ∈ (a:A[par] × (b:B[par;a] ⟶ (pco-W C[par;a;b]))) BY
                      Auto)
          THEN Thin (-3)
          THEN (EqHD (-1) THENA Auto)
          THEN All Reduce
          THEN (Assert b ∈ B[par;a] BY
                      Auto)
          THEN (Assert f b ∈ pW C[par;a;b] BY
                      Auto)
          THEN RepUR ``param-W`` -1
          THEN (MemTypeHD (-1) THENA Auto)
          THEN BHyp -1
          THEN Reduce 0) }

1
.....wf..... 
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. pco-W ∈ P ⟶ Type
6. par : P
7. a : A[par]
8. f : b:B[par;a] ⟶ (pW C[par;a;b])
9. pW-sup(a;f) ∈ pco-W par
10. path : ℕ ⟶ pcw-step(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b])
11. ∀i:ℕ. StepRel(path i;path (i + 1))
12. p : P
13. a1 : A[p]
14. w1 : b:B[p;a1] ⟶ (pco-W C[p;a1;b])
15. b : B[p;a1]
16. (path 0) = <p, <a1, w1>, inl b> ∈ pcw-step(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b])
17. p = par ∈ P
18. pco-W par ≡ a:A[par] × (b:B[par;a] ⟶ (pco-W C[par;a;b]))
19. a1 = a ∈ A[par]
20. w1 = f ∈ (b:B[par;a1] ⟶ (pco-W C[par;a1;b]))
21. b ∈ B[par;a]
22. (f b) = (f b) ∈ (pco-W C[par;a;b])
23. ∀path:Path. (StepAgree(path 0;C[par;a;b];f b) ⇒ (↓∃n:ℕ. Barred(pcw-partial(path;n))))
⊢ λx.(path (x + 1)) ∈ Path

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. pco-W ∈ P ⟶ Type
6. par : P
7. a : A[par]
8. f : b:B[par;a] ⟶ (pW C[par;a;b])
9. pW-sup(a;f) ∈ pco-W par
10. path : ℕ ⟶ pcw-step(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b])
11. ∀i:ℕ. StepRel(path i;path (i + 1))
12. p : P
13. a1 : A[p]
14. w1 : b:B[p;a1] ⟶ (pco-W C[p;a1;b])
15. b : B[p;a1]
16. (path 0) = <p, <a1, w1>, inl b> ∈ pcw-step(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b])
17. p = par ∈ P
18. pco-W par ≡ a:A[par] × (b:B[par;a] ⟶ (pco-W C[par;a;b]))
19. a1 = a ∈ A[par]
20. w1 = f ∈ (b:B[par;a1] ⟶ (pco-W C[par;a1;b]))
21. b ∈ B[par;a]
22. (f b) = (f b) ∈ (pco-W C[par;a;b])
23. ∀path:Path. (StepAgree(path 0;C[par;a;b];f b) ⇒ (↓∃n:ℕ. Barred(pcw-partial(path;n))))
⊢ StepAgree(path 1;C[par;a;b];f 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.  pco-W  \mmember{}  P  {}\mrightarrow{}  Type
6.  par  :  P
7.  a  :  A[par]
8.  f  :  b:B[par;a]  {}\mrightarrow{}  (pW  C[par;a;b])
9.  pW-sup(a;f)  \mmember{}  pco-W  par
10.  path  :  Path
11.  p  :  P
12.  a1  :  A[p]
13.  w1  :  b:B[p;a1]  {}\mrightarrow{}  (pco-W  C[p;a1;b])
14.  x  :  B[p;a1]
15.  (path  0)  =  <p,  <a1,  w1>,  inl  x>
16.  p  =  par
17.  <a1,  w1>  =  <a,  f>
\mvdash{}  \mdownarrow{}\mexists{}n:\mBbbN{}.  Barred(pcw-partial(\mlambda{}x.(path  (x  +  1));n))


By

---

Latex:
TACTIC:(DVar  `path'
                THEN  RenameVar  `b'  (-4)
                THEN  (Assert  pco-W  par  \mequiv{}  a:A[par]  \mtimes{}  (b:B[par;a]  {}\mrightarrow{}  (pco-W  C[par;a;b]))  BY
                                        (InstLemma  `param-co-W-ext`  [\mkleeneopen{}P\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}B\mkleeneclose{};\mkleeneopen{}C\mkleeneclose{}]\mcdot{}
                                          THEN  Auto
                                          THEN  (With  \mkleeneopen{}par\mkleeneclose{}  (D  (-1))\mcdot{}  THENA  Auto)
                                          THEN  Reduce  (-1)
                                          THEN  Auto))
                THEN  (Assert  <a1,  w1>  =  <a,  f>  BY
                                        Auto)
                THEN  Thin  (-3)
                THEN  (EqHD  (-1)  THENA  Auto)
                THEN  All  Reduce
                THEN  (Assert  b  \mmember{}  B[par;a]  BY
                                        Auto)
                THEN  (Assert  f  b  \mmember{}  pW  C[par;a;b]  BY
                                        Auto)
                THEN  RepUR  ``param-W``  -1
                THEN  (MemTypeHD  (-1)  THENA  Auto)
                THEN  BHyp  -1
                THEN  Reduce  0)

---

Home Index