(46steps total)
PrintForm
Definitions
hol
num
Sections
HOLlib
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
num
iso
2
1
2
1
1
1
2
f
:(
). one_one(
;
;
f
) &
onto(
;
;
f
)
By:
((DTerm (
m
:
.
m
+1) 0) THEN (Unab [`one_one`;`onto`;`not`])) THEN Simp
THEN
StrongAuto
Generated subgoal:
1
1.
y
:
.
x
:
.
y
=
x
+1
False
1
step
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(46steps total)
PrintForm
Definitions
hol
num
Sections
HOLlib
Doc
f:(
). one_one(;;f) & 
onto(;;f) f:(). one_one(;;f) & onto(;;f)
m:. m+1) 0) THEN (Unab [`one_one`;`onto`;`not`])) THEN Simp
y:. x:. y = x+1 
False
