Step * of Lemma non-forking-wellfounded-linorder

`∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].`
`  (decidable-non-minimal(T;x,y.R[x;y])`
`  `` WellFnd{i}(T;x,y.R[x;y])`
`  `` (∀m:T. (unique-minimal(T;x,y.R[x;y];m) `` non-forking(T;x,y.R[x;y]) `` WeakLinorder(T;x,y.x (R^*) y))))`
BY
`{ (Auto`
`   THEN (InstLemma `unique-minimal-wellfounded-implies` [⌜T⌝;⌜R⌝;⌜m⌝]⋅ THENA Auto)`
`   THEN D 0`
`   THEN FLemma `rel_star_order` [4] `
`   THEN Auto) }`

1
`1. [T] : Type`
`2. [R] : T ⟶ T ⟶ ℙ`
`3. decidable-non-minimal(T;x,y.R[x;y])`
`4. WellFnd{i}(T;x,y.R[x;y])`
`5. m : T`
`6. unique-minimal(T;x,y.R[x;y];m)`
`7. non-forking(T;x,y.R[x;y])`
`8. ∀y:T. (↓m ((λx,y. R[x;y])^*) y)`
`9. Order(T;x,y.x (R^*) y)`
`⊢ weak-connex(T; x,y.x (R^*) y)`

Latex:

Latex:
\mforall{}[T:Type].  \mforall{}[R:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].
(decidable-non-minimal(T;x,y.R[x;y])
{}\mRightarrow{}  WellFnd\{i\}(T;x,y.R[x;y])
{}\mRightarrow{}  (\mforall{}m:T
(unique-minimal(T;x,y.R[x;y];m)
{}\mRightarrow{}  non-forking(T;x,y.R[x;y])
{}\mRightarrow{}  WeakLinorder(T;x,y.x  rel\_star(T;  R)  y))))

By

Latex:
(Auto
THEN  (InstLemma  `unique-minimal-wellfounded-implies`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}R\mkleeneclose{};\mkleeneopen{}m\mkleeneclose{}]\mcdot{}  THENA  Auto)
THEN  D  0
THEN  FLemma  `rel\_star\_order`  [4]
THEN  Auto)

Home Index