Nuprl - Proof: num iso 2 1 2 1

(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. x' :

2. x'' :

3. rep_num(x') = rep_num(x'')
4. m :

5. 0<m
6.

. m-1<n

rep_num(m-1) = rep_num(n)

m-1 = n
7. n :

8. m<n
9. rep_num(m) = rep_num(n)

rep_num(m-1) = rep_num(n-1)

By:	Assert (0<n) THEN StrongAuto THEN Try (Complete (Unfold `label` 0)) THEN Unab [`hrep_num`] THEN Simp THEN StrongAuto THEN Try (Complete (Unfold `label` 0)) THEN Try (Complete (Unfold `label` 0))

Generated subgoal:

1 3. ncompose(suc_rep;x';zero_rep) = ncompose(suc_rep;x'';zero_rep)
4. m :
5. 0<m
6. n:.
6. m-1<n
6.
6. ncompose(suc_rep;m-1;zero_rep) = suc_rep(ncompose(suc_rep;n-1;zero_rep))
6.
6. m-1 = n
7. n :
8. m<n
9. suc_rep(ncompose(suc_rep;m-1;zero_rep))
9. =
9. suc_rep(ncompose(suc_rep;n-1;zero_rep))
9.
10. 0<n
  ncompose(suc_rep;m-1;zero_rep) = ncompose(suc_rep;n-1;zero_rep)
7 steps

About:

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

(46steps total) PrintForm Definitions hol num Sections HOLlib Doc