Step
*
of Lemma
cmp-le_wf
∀[T:Type]. ∀[cmp:comparison(T)]. ∀[x,y:cmp-type(T;cmp)]. (cmp-le(cmp;x;y) ∈ ℙ)
BY
{ ((Auto THEN OnVar `x' quotD THEN OnVar `y' quotD)
THEN (RepUR ``cmp-le`` 0
THEN D 2
THEN Auto
THEN (InstHyp [⌜x⌝;⌜x1⌝] 4⋅ THENA Auto)
THEN (RWO "-1" 0 THENA Auto)
THEN (RWO "3" 0 THENA Auto)
THEN (InstHyp [⌜y⌝;⌜y1⌝] 4⋅ THENA Auto)
THEN RWO "-1" 0
THEN Auto)⋅
) }
Latex:
Latex:
\mforall{}[T:Type]. \mforall{}[cmp:comparison(T)]. \mforall{}[x,y:cmp-type(T;cmp)]. (cmp-le(cmp;x;y) \mmember{} \mBbbP{})
By
Latex:
((Auto THEN OnVar `x' quotD THEN OnVar `y' quotD)
THEN (RepUR ``cmp-le`` 0
THEN D 2
THEN Auto
THEN (InstHyp [\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}x1\mkleeneclose{}] 4\mcdot{} THENA Auto)
THEN (RWO "-1" 0 THENA Auto)
THEN (RWO "3" 0 THENA Auto)
THEN (InstHyp [\mkleeneopen{}y\mkleeneclose{};\mkleeneopen{}y1\mkleeneclose{}] 4\mcdot{} THENA Auto)
THEN RWO "-1" 0
THEN Auto)\mcdot{}
)
Home
Index