Step
*
1
3
2
1
of Lemma
altWind_wf
1. A : 𝕌'
2. B : A ⟶ Type
3. P : altW(A;a.B[a]) ⟶ ℙ
4. h : w:altW(A;a.B[a]) ⟶ (b:coW-dom(a.B[a];w) ⟶ P[altW-item(w;b)]) ⟶ P[w]
5. w : altW(A;a.B[a])
6. n : {1...}
7. s : ℕn ⟶ copath(a.B[a];w)
8. ∀%1:ℕn
(0 < %1
⇒ (copath-length(s (%1 - 1)) = (%1 - 1) ∈ ℤ)
⇒ (copath-length(s %1) = %1 ∈ ℤ)
⇒ copathAgree(a.B[a];w;s (%1 - 1);s %1))
9. ∀t:{t:copath(a.B[a];w)|
0 < n
⇒ (copath-length(s (n - 1)) = (n - 1) ∈ ℤ)
⇒ (copath-length(t) = n ∈ ℤ)
⇒ copathAgree(a.B[a];w;s (n - 1);t)}
(if (n + 1 =z 0) then altWind(h;w)
if bdd-all(n + 1;i.(copath-length(if i=n then t else (s i)) =z i))
then altWind(h;copath-at(w;if (n + 1) - 1=n then t else (s ((n + 1) - 1))))
else ⋅
fi ∈ if (n + 1 =z 0) then P[w]
if bdd-all(n + 1;i.(copath-length(if i=n then t else (s i)) =z i))
then P[copath-at(w;if (n + 1) - 1=n then t else (s ((n + 1) - 1)))]
else Unit
fi )
10. ff ∈ 𝔹
11. bdd-all(n;i.(copath-length(s i) =z i)) ∈ 𝔹
12. ↑bdd-all(n;i.(copath-length(s i) =z i))
⊢ h copath-at(w;s (n - 1)) (λb.altWind(h;coW-item(copath-at(w;s (n - 1));b))) ∈ P[copath-at(w;s (n - 1))]
BY
{ (MemCD THEN Auto) }
1
1. A : 𝕌'
2. B : A ⟶ Type
3. P : altW(A;a.B[a]) ⟶ ℙ
4. h : w:altW(A;a.B[a]) ⟶ (b:coW-dom(a.B[a];w) ⟶ P[altW-item(w;b)]) ⟶ P[w]
5. w : altW(A;a.B[a])
6. n : {1...}
7. s : ℕn ⟶ copath(a.B[a];w)
8. ∀%1:ℕn
(0 < %1
⇒ (copath-length(s (%1 - 1)) = (%1 - 1) ∈ ℤ)
⇒ (copath-length(s %1) = %1 ∈ ℤ)
⇒ copathAgree(a.B[a];w;s (%1 - 1);s %1))
9. ∀t:{t:copath(a.B[a];w)|
0 < n
⇒ (copath-length(s (n - 1)) = (n - 1) ∈ ℤ)
⇒ (copath-length(t) = n ∈ ℤ)
⇒ copathAgree(a.B[a];w;s (n - 1);t)}
(if (n + 1 =z 0) then altWind(h;w)
if bdd-all(n + 1;i.(copath-length(if i=n then t else (s i)) =z i))
then altWind(h;copath-at(w;if (n + 1) - 1=n then t else (s ((n + 1) - 1))))
else ⋅
fi ∈ if (n + 1 =z 0) then P[w]
if bdd-all(n + 1;i.(copath-length(if i=n then t else (s i)) =z i))
then P[copath-at(w;if (n + 1) - 1=n then t else (s ((n + 1) - 1)))]
else Unit
fi )
10. ff ∈ 𝔹
11. bdd-all(n;i.(copath-length(s i) =z i)) ∈ 𝔹
12. ↑bdd-all(n;i.(copath-length(s i) =z i))
⊢ copath-at(w;s (n - 1)) ∈ altW(A;a.B[a])
2
1. A : 𝕌'
2. B : A ⟶ Type
3. P : altW(A;a.B[a]) ⟶ ℙ
4. h : w:altW(A;a.B[a]) ⟶ (b:coW-dom(a.B[a];w) ⟶ P[altW-item(w;b)]) ⟶ P[w]
5. w : altW(A;a.B[a])
6. n : {1...}
7. s : ℕn ⟶ copath(a.B[a];w)
8. ∀%1:ℕn
(0 < %1
⇒ (copath-length(s (%1 - 1)) = (%1 - 1) ∈ ℤ)
⇒ (copath-length(s %1) = %1 ∈ ℤ)
⇒ copathAgree(a.B[a];w;s (%1 - 1);s %1))
9. ∀t:{t:copath(a.B[a];w)|
0 < n
⇒ (copath-length(s (n - 1)) = (n - 1) ∈ ℤ)
⇒ (copath-length(t) = n ∈ ℤ)
⇒ copathAgree(a.B[a];w;s (n - 1);t)}
(if (n + 1 =z 0) then altWind(h;w)
if bdd-all(n + 1;i.(copath-length(if i=n then t else (s i)) =z i))
then altWind(h;copath-at(w;if (n + 1) - 1=n then t else (s ((n + 1) - 1))))
else ⋅
fi ∈ if (n + 1 =z 0) then P[w]
if bdd-all(n + 1;i.(copath-length(if i=n then t else (s i)) =z i))
then P[copath-at(w;if (n + 1) - 1=n then t else (s ((n + 1) - 1)))]
else Unit
fi )
10. ff ∈ 𝔹
11. bdd-all(n;i.(copath-length(s i) =z i)) ∈ 𝔹
12. ↑bdd-all(n;i.(copath-length(s i) =z i))
13. b : coW-dom(a.B[a];copath-at(w;s (n - 1)))
⊢ altWind(h;coW-item(copath-at(w;s (n - 1));b)) ∈ P[altW-item(copath-at(w;s (n - 1));b)]
Latex:
Latex:
1. A : \mBbbU{}'
2. B : A {}\mrightarrow{} Type
3. P : altW(A;a.B[a]) {}\mrightarrow{} \mBbbP{}
4. h : w:altW(A;a.B[a]) {}\mrightarrow{} (b:coW-dom(a.B[a];w) {}\mrightarrow{} P[altW-item(w;b)]) {}\mrightarrow{} P[w]
5. w : altW(A;a.B[a])
6. n : \{1...\}
7. s : \mBbbN{}n {}\mrightarrow{} copath(a.B[a];w)
8. \mforall{}\%1:\mBbbN{}n
(0 < \%1
{}\mRightarrow{} (copath-length(s (\%1 - 1)) = (\%1 - 1))
{}\mRightarrow{} (copath-length(s \%1) = \%1)
{}\mRightarrow{} copathAgree(a.B[a];w;s (\%1 - 1);s \%1))
9. \mforall{}t:\{t:copath(a.B[a];w)|
0 < n
{}\mRightarrow{} (copath-length(s (n - 1)) = (n - 1))
{}\mRightarrow{} (copath-length(t) = n)
{}\mRightarrow{} copathAgree(a.B[a];w;s (n - 1);t)\}
(if (n + 1 =\msubz{} 0) then altWind(h;w)
if bdd-all(n + 1;i.(copath-length(if i=n then t else (s i)) =\msubz{} i))
then altWind(h;copath-at(w;if (n + 1) - 1=n then t else (s ((n + 1) - 1))))
else \mcdot{}
fi \mmember{} if (n + 1 =\msubz{} 0) then P[w]
if bdd-all(n + 1;i.(copath-length(if i=n then t else (s i)) =\msubz{} i))
then P[copath-at(w;if (n + 1) - 1=n then t else (s ((n + 1) - 1)))]
else Unit
fi )
10. ff \mmember{} \mBbbB{}
11. bdd-all(n;i.(copath-length(s i) =\msubz{} i)) \mmember{} \mBbbB{}
12. \muparrow{}bdd-all(n;i.(copath-length(s i) =\msubz{} i))
\mvdash{} h copath-at(w;s (n - 1)) (\mlambda{}b.altWind(h;coW-item(copath-at(w;s (n - 1));b))) \mmember{} P[copath-at(w;s
(n
- 1))]
By
Latex:
(MemCD THEN Auto)
Home
Index