---

Step * 1 2 1 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. w1 ∈ b:B1[a1] ⟶ W(A1;a.B1[a])
17. <a2, z1> ∈ pW ⋅
⊢ z1 ∈ b:B1[a2] ⟶ W(A1;a.B1[a])
BY
{ ((InstLemma `param-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 (Assert <a2, z1> ∈ a:A1 × (b:B1[a] ⟶ (pW ⋅)) BY
               (SubsumeC ⌜pW ⋅⌝⋅ THEN Auto))
   THEN MemHD (-1)
   THEN All Reduce
   THEN 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.  w1  \mmember{}  b:B1[a1]  {}\mrightarrow{}  W(A1;a.B1[a])
17.  <a2,  z1>  \mmember{}  pW  \mcdot{}
\mvdash{}  z1  \mmember{}  b:B1[a2]  {}\mrightarrow{}  W(A1;a.B1[a])


By

---

Latex:
((InstLemma  `param-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)\mcdot{}
  THEN  (With  \mkleeneopen{}\mcdot{}\mkleeneclose{}  (D  (-1))\mcdot{}  THENA  Auto)
  THEN  Reduce  (-1)
  THEN  (Assert  <a2,  z1>  \mmember{}  a:A1  \mtimes{}  (b:B1[a]  {}\mrightarrow{}  (pW  \mcdot{}))  BY
                          (SubsumeC  \mkleeneopen{}pW  \mcdot{}\mkleeneclose{}\mcdot{}  THEN  Auto))
  THEN  MemHD  (-1)
  THEN  All  Reduce
  THEN  Auto)

---

Home Index