Step
*
1
3
2
1
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. ∀i:ℕn. (copath-length(s i) = 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)]
BY
{ ((D -5 With ⌜copath-extend(s (n - 1);b)⌝ THENA Auto)
THEN (Subst' (n + 1 =z 0) ~ ff -1 THENA Auto)
THEN Reduce -1
THEN (Subst' (n + 1) - 1 ~ n -1 THENA Auto)
THEN (Reduce -1 THENA Auto)
THEN SplitOnHypITE -1
THEN Auto) }
1
.....truecase.....
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. ff ∈ 𝔹
10. bdd-all(n;i.(copath-length(s i) =z i)) ∈ 𝔹
11. ∀i:ℕn. (copath-length(s i) = i ∈ ℤ)
12. b : coW-dom(a.B[a];copath-at(w;s (n - 1)))
13. altWind(h;copath-at(w;copath-extend(s (n - 1);b))) ∈ P[copath-at(w;copath-extend(s (n - 1);b))]
14. ↑bdd-all(n + 1;i.(copath-length(if i=n then copath-extend(s (n - 1);b) else (s i)) =z i))
⊢ altWind(h;coW-item(copath-at(w;s (n - 1));b)) ∈ P[altW-item(copath-at(w;s (n - 1));b)]
2
.....falsecase.....
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. ff ∈ 𝔹
10. bdd-all(n;i.(copath-length(s i) =z i)) ∈ 𝔹
11. ∀i:ℕn. (copath-length(s i) = i ∈ ℤ)
12. b : coW-dom(a.B[a];copath-at(w;s (n - 1)))
13. ⋅ ∈ Unit
14. ¬↑bdd-all(n + 1;i.(copath-length(if i=n then copath-extend(s (n - 1);b) else (s i)) =z i))
⊢ 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. \mforall{}i:\mBbbN{}n. (copath-length(s i) = i)
13. b : coW-dom(a.B[a];copath-at(w;s (n - 1)))
\mvdash{} altWind(h;coW-item(copath-at(w;s (n - 1));b)) \mmember{} P[altW-item(copath-at(w;s (n - 1));b)]
By
Latex:
((D -5 With \mkleeneopen{}copath-extend(s (n - 1);b)\mkleeneclose{} THENA Auto)
THEN (Subst' (n + 1 =\msubz{} 0) \msim{} ff -1 THENA Auto)
THEN Reduce -1
THEN (Subst' (n + 1) - 1 \msim{} n -1 THENA Auto)
THEN (Reduce -1 THENA Auto)
THEN SplitOnHypITE -1
THEN Auto)
Home
Index