Step
*
of Lemma
rel-immediate-exists
∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].
(SWellFounded(R x y)
⇒ (∀x,y:T. Dec(∃z:T. ((R x z) ∧ (R z y))))
⇒ (∀y:T. ((∃x:T. (R x y))
⇒ (∃x:T. (R! x y)))))
BY
{ (Auto THEN ((InstLemma `rel-immediate-rel-plus` [⌜T⌝; ⌜R⌝])⋅ THENA Auto)) }
1
1. [T] : Type
2. [R] : T ⟶ T ⟶ ℙ
3. SWellFounded(R x y)@i
4. ∀x,y:T. Dec(∃z:T. ((R x z) ∧ (R z y)))@i
5. y : T@i
6. ∃x:T. (R x y)@i
7. R+ => R!+
⊢ ∃x:T. (R! x y)
Latex:
Latex:
\mforall{}[T:Type]. \mforall{}[R:T {}\mrightarrow{} T {}\mrightarrow{} \mBbbP{}].
(SWellFounded(R x y)
{}\mRightarrow{} (\mforall{}x,y:T. Dec(\mexists{}z:T. ((R x z) \mwedge{} (R z y))))
{}\mRightarrow{} (\mforall{}y:T. ((\mexists{}x:T. (R x y)) {}\mRightarrow{} (\mexists{}x:T. (R! x y)))))
By
Latex:
(Auto THEN ((InstLemma `rel-immediate-rel-plus` [\mkleeneopen{}T\mkleeneclose{}; \mkleeneopen{}R\mkleeneclose{}])\mcdot{} THENA Auto))
Home
Index