Step
*
of Lemma
ulinorder_functionality_wrt_iff
∀[T:Type]. ∀[R,R':T ⟶ T ⟶ ℙ].
((∀[x,y:T]. uiff(R[x;y];R'[x;y]))
⇒ (UniformLinorder(T;x,y.R[x;y])
⇐⇒ UniformLinorder(T;x,y.R'[x;y])))
BY
{ ((RepD THENA Auto)
THEN Unfold `ulinorder` 0
THEN RepeatFor 2 ((D 0 THENA Auto))
THEN Repeat (ParallelLast)
THEN Auto) }
Latex:
Latex:
\mforall{}[T:Type]. \mforall{}[R,R':T {}\mrightarrow{} T {}\mrightarrow{} \mBbbP{}].
((\mforall{}[x,y:T]. uiff(R[x;y];R'[x;y]))
{}\mRightarrow{} (UniformLinorder(T;x,y.R[x;y]) \mLeftarrow{}{}\mRightarrow{} UniformLinorder(T;x,y.R'[x;y])))
By
Latex:
((RepD THENA Auto)
THEN Unfold `ulinorder` 0
THEN RepeatFor 2 ((D 0 THENA Auto))
THEN Repeat (ParallelLast)
THEN Auto)
Home
Index