(6steps)
PrintForm
Definitions
Lemmas
int
2
Sections
StandardLIB
Doc
At:
ndiff
ndiff
eq
imin
1
1
1
1.
a:
2.
b:
imax(imin(b;a);0) = imin(a;b)
By:
RWN 1 (LemmaC
Thm*
a,b:
. imin(a;b) = imin(b;a)) 0
THEN
Unfold `imin` 0
THEN
SplitOnConclITE
Generated subgoals:
1
3.
a
b
imax(a;0) = a
2
3.
b < a
imax(b;0) = b
About:
(6steps)
PrintForm
Definitions
Lemmas
int
2
Sections
StandardLIB
Doc
b
imax(a;0) = a imax(b;0) = b
imax(imin(b;a);0) = imin(a;b)
a,b:
. imin(a;b) = imin(b;a))
0
b imax(a;0) = a imax(b;0) = b
