Step
*
of Lemma
transitive-loop2
∀[T:Type]
∀L:T List
∀[R:{x:T| (x ∈ L)} ⟶ {x:T| (x ∈ L)} ⟶ ℙ]
(Trans({x:T| (x ∈ L)} ;x,y.R[x;y])
⇒ (∀i:ℕ||L|| - 1. R[L[i];L[i + 1]])
⇒ R[last(L);hd(L)] supposing ¬↑null(L)
⇒ (∀a∈L.(∀b∈L.R[a;b])))
BY
{ xxx(Auto
THEN Try ((BLemma `list-subtype` THEN Auto))
THEN Try ((DVar `L' THEN All Reduce THEN Complete (Auto')))
THEN (InstLemma `transitive-loop` [⌜{x:T| (x ∈ L)} ⌝; ⌜R⌝; ⌜L⌝])⋅
THEN Auto
THEN BLemma `list-subtype`
THEN Auto)xxx }
Latex:
Latex:
\mforall{}[T:Type]
\mforall{}L:T List
\mforall{}[R:\{x:T| (x \mmember{} L)\} {}\mrightarrow{} \{x:T| (x \mmember{} L)\} {}\mrightarrow{} \mBbbP{}]
(Trans(\{x:T| (x \mmember{} L)\} ;x,y.R[x;y])
{}\mRightarrow{} (\mforall{}i:\mBbbN{}||L|| - 1. R[L[i];L[i + 1]])
{}\mRightarrow{} R[last(L);hd(L)] supposing \mneg{}\muparrow{}null(L)
{}\mRightarrow{} (\mforall{}a\mmember{}L.(\mforall{}b\mmember{}L.R[a;b])))
By
Latex:
xxx(Auto
THEN Try ((BLemma `list-subtype` THEN Auto))
THEN Try ((DVar `L' THEN All Reduce THEN Complete (Auto')))
THEN (InstLemma `transitive-loop` [\mkleeneopen{}\{x:T| (x \mmember{} L)\} \mkleeneclose{}; \mkleeneopen{}R\mkleeneclose{}; \mkleeneopen{}L\mkleeneclose{}])\mcdot{}
THEN Auto
THEN BLemma `list-subtype`
THEN Auto)xxx
Home
Index