Step
*
of Lemma
no-descending-chain-implies-wellfounded
∀[T:Type]. ∀[<:T ⟶ T ⟶ ℙ].
((∀x,y,z:T. ((x < y)
⇒ (y < z)
⇒ (x < z)))
⇒ (∀x,y:T. Dec(x < y))
⇒ no-descending-chain(T;<)
⇒ WellFnd{i}(T;x,y.x < y))
BY
{ (Auto
THEN InstLemma `descending-chain-barred-implies-wellfounded`
[⌜T⌝;⌜<⌝;⌜λx,y. (¬(x < y))⌝]⋅
THEN Reduce 0
THEN Auto) }
Latex:
Latex:
\mforall{}[T:Type]. \mforall{}[<:T {}\mrightarrow{} T {}\mrightarrow{} \mBbbP{}].
((\mforall{}x,y,z:T. ((x < y) {}\mRightarrow{} (y < z) {}\mRightarrow{} (x < z)))
{}\mRightarrow{} (\mforall{}x,y:T. Dec(x < y))
{}\mRightarrow{} no-descending-chain(T;<)
{}\mRightarrow{} WellFnd\{i\}(T;x,y.x < y))
By
Latex:
(Auto
THEN InstLemma `descending-chain-barred-implies-wellfounded`
[\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}<\mkleeneclose{};\mkleeneopen{}\mlambda{}x,y. (\mneg{}(x < y))\mkleeneclose{}]\mcdot{}
THEN Reduce 0
THEN Auto)
Home
Index