Step
*
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])
⊢ altWind(h;w) ∈ P[w]
BY
{ ((Assert ⌜(λn,s. if (n =z 0) then altWind(h;w)
if bdd-all(n;i.(copath-length(s i) =z i)) then altWind(h;copath-at(w;s (n - 1)))
else ⋅
fi )
0
⋅ ∈ (λn,s. if (n =z 0) then P[w]
if bdd-all(n;i.(copath-length(s i) =z i)) then P[copath-at(w;s (n - 1))]
else Unit
fi )
0
⋅⌝⋅
THENM (Reduce -1 THEN Auto)
)
THEN Strong_Bar_Induction ⌜copath(a.B[a];w)⌝ ⌜λn,p,x. (0 < n
⇒ (copath-length(p (n - 1)) = (n - 1) ∈ ℤ)
⇒ (copath-length(x) = n ∈ ℤ)
⇒ copathAgree(a.B[a];w;p (n - 1);x))⌝ ⌜λn,p. ∃i:ℕn
(¬(copath-length(p i)
= i
∈ ℤ))⌝⋅
THEN All Reduce
THEN Try (Complete (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. alpha : ℕ ⟶ copath(a.B[a];w)
7. ∀n:ℕ
(0 < n
⇒ (copath-length(alpha (n - 1)) = (n - 1) ∈ ℤ)
⇒ (copath-length(alpha n) = n ∈ ℤ)
⇒ copathAgree(a.B[a];w;alpha (n - 1);alpha n))
⊢ ↓∃n:ℕ. ∃i:ℕn. (¬(copath-length(alpha i) = i ∈ ℤ))
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 : ℕ
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. m : ∃i:ℕn. (¬(copath-length(s i) = i ∈ ℤ))
⊢ if (n =z 0) then altWind(h;w)
if bdd-all(n;i.(copath-length(s i) =z i)) then altWind(h;copath-at(w;s (n - 1)))
else ⋅
fi ∈ if (n =z 0) then P[w]
if bdd-all(n;i.(copath-length(s i) =z i)) then P[copath-at(w;s (n - 1))]
else Unit
fi
3
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 : ℕ
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 )
⊢ if (n =z 0) then altWind(h;w)
if bdd-all(n;i.(copath-length(s i) =z i)) then altWind(h;copath-at(w;s (n - 1)))
else ⋅
fi ∈ if (n =z 0) then P[w]
if bdd-all(n;i.(copath-length(s i) =z i)) then P[copath-at(w;s (n - 1))]
else Unit
fi
Latex:
Latex:
1. A : \mBbbU{}'
2. B : A {}\mrightarrow{} Type
3. P : altW(A;a.B[a]) {}\mrightarrow{} \mBbbP{}
4. h : \mforall{}w:altW(A;a.B[a]). ((\mforall{}b:coW-dom(a.B[a];w). P[altW-item(w;b)]) {}\mRightarrow{} P[w])
5. w : altW(A;a.B[a])
\mvdash{} altWind(h;w) \mmember{} P[w]
By
Latex:
((Assert \mkleeneopen{}(\mlambda{}n,s. if (n =\msubz{} 0) then altWind(h;w)
if bdd-all(n;i.(copath-length(s i) =\msubz{} i)) then altWind(h;copath-at(w;s (n - 1)))
else \mcdot{}
fi )
0
\mcdot{} \mmember{} (\mlambda{}n,s. if (n =\msubz{} 0) then P[w]
if bdd-all(n;i.(copath-length(s i) =\msubz{} i)) then P[copath-at(w;s (n - 1))]
else Unit
fi )
0
\mcdot{}\mkleeneclose{}\mcdot{}
THENM (Reduce -1 THEN Auto)
)
THEN Strong\_Bar\_Induction \mkleeneopen{}copath(a.B[a];w)\mkleeneclose{} \mkleeneopen{}\mlambda{}n,p,x. (0 < n
{}\mRightarrow{} (copath-length(p (n - 1)) = (n - 1))
{}\mRightarrow{} (copath-length(x) = n)
{}\mRightarrow{} copathAgree(a.B[a];w;p (n - 1);x))\mkleeneclose{}
\mkleeneopen{}\mlambda{}n,p. \mexists{}i:\mBbbN{}n. (\mneg{}(copath-length(p i) = i))\mkleeneclose{}\mcdot{}
THEN All Reduce
THEN Try (Complete (Auto)))
Home
Index