Step
*
1
of Lemma
wellfounded-llex
1. [A] : Type
2. [<] : A ⟶ A ⟶ ℙ
3. ∀a,b:A. SqStable(<[a;b])
4. ∀[P:A ⟶ ℙ]. ((∀j:A. ((∀k:A. (<[k;j]
⇒ P[k]))
⇒ P[j]))
⇒ {∀n:A. P[n]})
5. [P] : Des(A;a,b.<[a;b]) ⟶ ℙ
6. ∀j:Des(A;a,b.<[a;b]). ((∀k:Des(A;a,b.<[a;b]). ((k llex(A;a,b.<[a;b]) j)
⇒ P[k]))
⇒ P[j])
7. ∀[a:A]. ∀[m,k:Des(A;a,b.<[a;b])]. (descending(a,b.<[a;b];m @ [a / k]) ∈ ℙ)
8. ∀[a:A]. ∀[m:Des(A;a,b.<[a;b])]. ({k:Des(A;a,b.<[a;b])| descending(a,b.<[a;b];m @ [a / k])} ∈ Type)
⊢ {∀n:Des(A;a,b.<[a;b]). P[n]}
BY
{ (All (Unfold `guard`)
THEN (D 0 THENA Auto)
THEN InstHyp [⌜λ2a.∀m:Des(A;a,b.<[a;b])
((∀L:Des(A;a,b.<[a;b]). ((L llex(A;a,b.<[a;b]) m)
⇒ P[L]))
⇒ (∀k:{k:Des(A;a,b.<[a;b])| descending(a,b.<[a;b];m @ [a / k])} . P[m @ [a / k]]))⌝] 4⋅) }
1
.....wf.....
1. A : Type
2. < : A ⟶ A ⟶ ℙ
3. ∀a,b:A. SqStable(<[a;b])
4. ∀[P:A ⟶ ℙ]. ((∀j:A. ((∀k:A. (<[k;j]
⇒ P[k]))
⇒ P[j]))
⇒ (∀n:A. P[n]))
5. P : Des(A;a,b.<[a;b]) ⟶ ℙ
6. ∀j:Des(A;a,b.<[a;b]). ((∀k:Des(A;a,b.<[a;b]). ((k llex(A;a,b.<[a;b]) j)
⇒ P[k]))
⇒ P[j])
7. ∀[a:A]. ∀[m,k:Des(A;a,b.<[a;b])]. (descending(a,b.<[a;b];m @ [a / k]) ∈ ℙ)
8. ∀[a:A]. ∀[m:Des(A;a,b.<[a;b])]. ({k:Des(A;a,b.<[a;b])| descending(a,b.<[a;b];m @ [a / k])} ∈ Type)
9. n : Des(A;a,b.<[a;b])
⊢ λa.∀m:Des(A;a,b.<[a;b])
((∀L:Des(A;a,b.<[a;b]). ((L llex(A;a,b.<[a;b]) m)
⇒ P[L]))
⇒ (∀k:{k:Des(A;a,b.<[a;b])| descending(a,b.<[a;b];m @ [a / k])} . P[m @ [a / k]])) ∈ A ⟶ ℙ
2
.....antecedent.....
1. [A] : Type
2. [<] : A ⟶ A ⟶ ℙ
3. ∀a,b:A. SqStable(<[a;b])
4. ∀[P:A ⟶ ℙ]. ((∀j:A. ((∀k:A. (<[k;j]
⇒ P[k]))
⇒ P[j]))
⇒ (∀n:A. P[n]))
5. [P] : Des(A;a,b.<[a;b]) ⟶ ℙ
6. ∀j:Des(A;a,b.<[a;b]). ((∀k:Des(A;a,b.<[a;b]). ((k llex(A;a,b.<[a;b]) j)
⇒ P[k]))
⇒ P[j])
7. ∀[a:A]. ∀[m,k:Des(A;a,b.<[a;b])]. (descending(a,b.<[a;b];m @ [a / k]) ∈ ℙ)
8. ∀[a:A]. ∀[m:Des(A;a,b.<[a;b])]. ({k:Des(A;a,b.<[a;b])| descending(a,b.<[a;b];m @ [a / k])} ∈ Type)
9. n : Des(A;a,b.<[a;b])
⊢ ∀j:A
((∀k:A
(<[k;j]
⇒ (∀m:Des(A;a,b.<[a;b])
((∀L:Des(A;a,b.<[a;b]). ((L llex(A;a,b.<[a;b]) m)
⇒ P[L]))
⇒ (∀k@0:{k@0:Des(A;a,b.<[a;b])| descending(a,b.<[a;b];m @ [k / k@0])} . P[m @ [k / k@0]])))))
⇒ (∀m:Des(A;a,b.<[a;b])
((∀L:Des(A;a,b.<[a;b]). ((L llex(A;a,b.<[a;b]) m)
⇒ P[L]))
⇒ (∀k:{k:Des(A;a,b.<[a;b])| descending(a,b.<[a;b];m @ [j / k])} . P[m @ [j / k]]))))
3
1. [A] : Type
2. [<] : A ⟶ A ⟶ ℙ
3. ∀a,b:A. SqStable(<[a;b])
4. ∀[P:A ⟶ ℙ]. ((∀j:A. ((∀k:A. (<[k;j]
⇒ P[k]))
⇒ P[j]))
⇒ (∀n:A. P[n]))
5. [P] : Des(A;a,b.<[a;b]) ⟶ ℙ
6. ∀j:Des(A;a,b.<[a;b]). ((∀k:Des(A;a,b.<[a;b]). ((k llex(A;a,b.<[a;b]) j)
⇒ P[k]))
⇒ P[j])
7. ∀[a:A]. ∀[m,k:Des(A;a,b.<[a;b])]. (descending(a,b.<[a;b];m @ [a / k]) ∈ ℙ)
8. ∀[a:A]. ∀[m:Des(A;a,b.<[a;b])]. ({k:Des(A;a,b.<[a;b])| descending(a,b.<[a;b];m @ [a / k])} ∈ Type)
9. n : Des(A;a,b.<[a;b])
10. ∀n:A. ∀m:Des(A;a,b.<[a;b]).
((∀L:Des(A;a,b.<[a;b]). ((L llex(A;a,b.<[a;b]) m)
⇒ P[L]))
⇒ (∀k:{k:Des(A;a,b.<[a;b])| descending(a,b.<[a;b];m @ [n / k])} . P[m @ [n / k]]))
⊢ P[n]
Latex:
Latex:
1. [A] : Type
2. [<] : A {}\mrightarrow{} A {}\mrightarrow{} \mBbbP{}
3. \mforall{}a,b:A. SqStable(<[a;b])
4. \mforall{}[P:A {}\mrightarrow{} \mBbbP{}]. ((\mforall{}j:A. ((\mforall{}k:A. (<[k;j] {}\mRightarrow{} P[k])) {}\mRightarrow{} P[j])) {}\mRightarrow{} \{\mforall{}n:A. P[n]\})
5. [P] : Des(A;a,b.<[a;b]) {}\mrightarrow{} \mBbbP{}
6. \mforall{}j:Des(A;a,b.<[a;b]). ((\mforall{}k:Des(A;a,b.<[a;b]). ((k llex(A;a,b.<[a;b]) j) {}\mRightarrow{} P[k])) {}\mRightarrow{} P[j])
7. \mforall{}[a:A]. \mforall{}[m,k:Des(A;a,b.<[a;b])]. (descending(a,b.<[a;b];m @ [a / k]) \mmember{} \mBbbP{})
8. \mforall{}[a:A]. \mforall{}[m:Des(A;a,b.<[a;b])].
(\{k:Des(A;a,b.<[a;b])| descending(a,b.<[a;b];m @ [a / k])\} \mmember{} Type)
\mvdash{} \{\mforall{}n:Des(A;a,b.<[a;b]). P[n]\}
By
Latex:
(All (Unfold `guard`)
THEN (D 0 THENA Auto)
THEN InstHyp [\mkleeneopen{}\mlambda{}\msubtwo{}a.\mforall{}m:Des(A;a,b.<[a;b])
((\mforall{}L:Des(A;a,b.<[a;b]). ((L llex(A;a,b.<[a;b]) m) {}\mRightarrow{} P[L]))
{}\mRightarrow{} (\mforall{}k:\{k:Des(A;a,b.<[a;b])| descending(a,b.<[a;b];m @ [a / k])\}
P[m @ [a / k]]))\mkleeneclose{}] 4\mcdot{})
Home
Index