Nuprl - Proof: num iso 2

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: num iso 2

1. x' :

2. x'' :

3. rep_num(x') = rep_num(x'')

x' = x''

By:	Assert (m,n:. m<n rep_num(m) = rep_num(n) m = n) THEN StrongAuto THEN Try (Complete (Unfold `label` 0)) THEN Try (Complete (Unfold `hnum` 0))

Generated subgoals:

1 4. m :
5. n :
6. m<n
7. rep_num(m) = rep_num(n)
  m = n
22 steps

2 4. m,n:. m<n  rep_num(m) = rep_num(n)    m = n
  x' = x''
4 steps

About:

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

1	4. m : 5. n : 6. m<n 7. rep_num(m) = rep_num(n) m = n	22 steps
2	4. m,n:. m<n rep_num(m) = rep_num(n) m = n x' = x''	4 steps