Step
*
2
of Lemma
int_loset_wf
UniformLinorder(ℤ;a,b.↑(a (λx,y. x ≤z y) b))
BY
{ AbReduce 0 THEN ((RW bool_to_propC 0) THENA Auto) }
1
UniformLinorder(ℤ;a,b.a ≤ b)
Latex:
Latex:
UniformLinorder(\mBbbZ{};a,b.\muparrow{}(a (\mlambda{}x,y. x \mleq{}z y) b))
By
Latex:
AbReduce 0 THEN ((RW bool\_to\_propC 0) THENA Auto)
Home
Index