---

Step * 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 ⋅)
⊢ z1 ∈ b:B1[a2] ⟶ W(A1;a.B1[a])
BY
{ Assert ⌜w1 ∈ b:B1[a1] ⟶ W(A1;a.B1[a])⌝⋅ }

1
.....assertion..... 
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 ⋅)
⊢ w1 ∈ b:B1[a1] ⟶ W(A1;a.B1[a])

2
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])
⊢ z1 ∈ b:B1[a2] ⟶ W(A1;a.B1[a])

---

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>
\mvdash{}  z1  \mmember{}  b:B1[a2]  {}\mrightarrow{}  W(A1;a.B1[a])


By

---

Latex:
Assert  \mkleeneopen{}w1  \mmember{}  b:B1[a1]  {}\mrightarrow{}  W(A1;a.B1[a])\mkleeneclose{}\mcdot{}

---

Home Index