---

Step * 1 1 1 2 of Lemma W-path-lemma2


1. A1 : Type
2. B1 : A1 ⟶ Type
3. pco-W ⋅ ≡ a:A1 × (b:(B1 a) ⟶ (pco-W ⋅))
4. a : A1
5. x1 : B1[a] ⟶ W(A1;a.B1[a])
6. n : ℕ+
7. s : ℕn ⟶ cw-step(A1;a.B1[a])
8. a1 : A1
9. w1 : b:B1[a1] ⟶ (pco-W ⋅)
10. x : B1[a1]
11. a2 : A1
12. z1 : b:B1[a2] ⟶ (pco-W ⋅)
13. ∀k:ℕn. (W-rel(A1;a.B1[a];<a, x1>) k s (s k))
14. (s (n - 1)) = <⋅, <a1, w1>, inl x> ∈ cw-step(A1;a.B1[a])
15. (w1 x) = <a2, z1> ∈ (pco-W ⋅)
16. pW ⋅ ≡ a:A1 × (b:B1[a] ⟶ (pW ⋅))
17. pco-W ∈ Unit ⟶ Type
18. fst(snd((s (n - 1)))) ∈ W(A1;a.B1[a])
⊢ <a1, w1> ∈ pW ⋅
BY
{ OnMaybeHyp 13 (\h. (RepUR ``cw-step pcw-step`` h
                      THEN ((EqHD h THENA Auto) THEN All Reduce)⋅
                      THEN (((EqHD (h+1) THENA Auto) THEN All Reduce)
                            THEN skip{Try (((InstLemma `param-co-W-ext` [⌜Unit⌝;⌜λ2p.A1⌝;⌜λ2p a.B1[a]⌝;
                                             ⌜so_lambda(p,a,b.⋅)⌝]⋅
                                             THENA Auto
                                             )
                                            THEN (With ⌜⋅⌝ (D (-1))⋅ THENA Auto)
                                            THEN Reduce (-1)
                                            THEN (GenConcl ⌜w = z ∈ (a:A1 × (b:B1[a] ⟶ (pco-W ⋅)))⌝⋅ THENA Auto)
                                            THEN D -2
                                            THEN Reduce 0
                                            THEN Auto)⋅)}
                            THEN HypSubst' h (h+1)
                            THEN FLemma `equal-implies-member-param-W` [h+1]
                            THEN Try (Complete (Auto)))⋅)) }

---

Latex:

---

Latex:

1.  A1  :  Type
2.  B1  :  A1  {}\mrightarrow{}  Type
3.  pco-W  \mcdot{}  \mequiv{}  a:A1  \mtimes{}  (b:(B1  a)  {}\mrightarrow{}  (pco-W  \mcdot{}))
4.  a  :  A1
5.  x1  :  B1[a]  {}\mrightarrow{}  W(A1;a.B1[a])
6.  n  :  \mBbbN{}\msupplus{}
7.  s  :  \mBbbN{}n  {}\mrightarrow{}  cw-step(A1;a.B1[a])
8.  a1  :  A1
9.  w1  :  b:B1[a1]  {}\mrightarrow{}  (pco-W  \mcdot{})
10.  x  :  B1[a1]
11.  a2  :  A1
12.  z1  :  b:B1[a2]  {}\mrightarrow{}  (pco-W  \mcdot{})
13.  \mforall{}k:\mBbbN{}n.  (W-rel(A1;a.B1[a];<a,  x1>)  k  s  (s  k))
14.  (s  (n  -  1))  =  <\mcdot{},  <a1,  w1>,  inl  x>
15.  (w1  x)  =  <a2,  z1>
16.  pW  \mcdot{}  \mequiv{}  a:A1  \mtimes{}  (b:B1[a]  {}\mrightarrow{}  (pW  \mcdot{}))
17.  pco-W  \mmember{}  Unit  {}\mrightarrow{}  Type
18.  fst(snd((s  (n  -  1))))  \mmember{}  W(A1;a.B1[a])
\mvdash{}  <a1,  w1>  \mmember{}  pW  \mcdot{}


By

---

Latex:
OnMaybeHyp  13  (\mbackslash{}h.  (RepUR  ``cw-step  pcw-step``  h
                                        THEN  ((EqHD  h  THENA  Auto)  THEN  All  Reduce)\mcdot{}
                                        THEN  (((EqHD  (h+1)  THENA  Auto)  THEN  All  Reduce)
                                                    THEN  skip\{Try  (((InstLemma  `param-co-W-ext`  [\mkleeneopen{}Unit\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}p.A1\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}p  a.B1[a]\mkleeneclose{}
                                                                                      ;\mkleeneopen{}so\_lambda(p,a,b.\mcdot{})\mkleeneclose{}]\mcdot{}
                                                                                      THENA  Auto
                                                                                      )
                                                                                    THEN  (With  \mkleeneopen{}\mcdot{}\mkleeneclose{}  (D  (-1))\mcdot{}  THENA  Auto)
                                                                                    THEN  Reduce  (-1)
                                                                                    THEN  (GenConcl  \mkleeneopen{}w  =  z\mkleeneclose{}\mcdot{}  THENA  Auto)
                                                                                    THEN  D  -2
                                                                                    THEN  Reduce  0
                                                                                    THEN  Auto)\mcdot{})\}
                                                    THEN  HypSubst'  h  (h+1)
                                                    THEN  FLemma  `equal-implies-member-param-W`  [h+1]
                                                    THEN  Try  (Complete  (Auto)))\mcdot{}))

---

Home Index