Step
*
of Lemma
fseg-test
∀T:Type. ∀as,bs,cs:T List.
((fseg(T;as;as) ∧ (fseg(T;as;bs)
⇒ fseg(T;bs;cs)
⇒ fseg(T;as;cs))) ∧ as ≤ as ∧ (as ≤ bs
⇒ bs ≤ cs
⇒ as ≤ cs))
BY
{ Auto }
Latex:
Latex:
\mforall{}T:Type. \mforall{}as,bs,cs:T List.
((fseg(T;as;as) \mwedge{} (fseg(T;as;bs) {}\mRightarrow{} fseg(T;bs;cs) {}\mRightarrow{} fseg(T;as;cs)))
\mwedge{} as \mleq{} as
\mwedge{} (as \mleq{} bs {}\mRightarrow{} bs \mleq{} cs {}\mRightarrow{} as \mleq{} cs))
By
Latex:
Auto
Home
Index