Step
*
1
1
1
1
2
1
of Lemma
pW-sup_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 : 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)
18. n : ℕ
19. Barred(pcw-partial(λx.(path (x + 1));n))
⊢ Barred(pcw-partial(path;n + 1))
BY
{ TACTIC:TACTIC:(RepUR ``pcw-pp-barred pcw-partial`` -1
                 THEN RepUR ``pcw-pp-barred pcw-partial`` 0
                 THEN ParallelLast
                 THEN Try ((NthHypSq (-1) THEN RepeatFor 2 (EqCD) THEN CompleteAuto))
                 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.  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>
18.  n  :  \mBbbN{}
19.  Barred(pcw-partial(\mlambda{}x.(path  (x  +  1));n))
\mvdash{}  Barred(pcw-partial(path;n  +  1))
By
Latex:
TACTIC:TACTIC:(RepUR  ``pcw-pp-barred  pcw-partial``  -1
                              THEN  RepUR  ``pcw-pp-barred  pcw-partial``  0
                              THEN  ParallelLast
                              THEN  Try  ((NthHypSq  (-1)  THEN  RepeatFor  2  (EqCD)  THEN  CompleteAuto))
                              THEN  Auto)
Home
Index