Nuprl - Proof: hsuc def 1

(9steps total) PrintForm Definitions Lemmas hol num Sections HOLlib Doc

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: hsuc def 1

1. m :

m+1 = abs_num(suc_rep(rep_num(m)))

By:	Inst Thm* 'a,'b:S, P:('b), rep:('a'b), abs:('b'a), a:'a, r:'b. Thm* iso_pair('a;'b;P;rep;abs) rep(a) = r a = abs(r) [;;is_num_rep;rep_num;abs_num] THEN StrongAuto THEN BackThru -1 THEN StrongAuto

Generated subgoals:

1 2. a,r:.
2. iso_pair(;;is_num_rep;rep_num;abs_num)
2.
2. rep_num(a) = r    a = abs_num(r)
  iso_pair(;;is_num_rep;rep_num;abs_num)
1 step

2 2. a,r:.
2. iso_pair(;;is_num_rep;rep_num;abs_num)
2.
2. rep_num(a) = r    a = abs_num(r)
  rep_num(m+1) = suc_rep(rep_num(m))
6 steps

About:

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

(9steps total) PrintForm Definitions Lemmas hol num Sections HOLlib Doc

1	2. a,r:. 2. iso_pair(;;is_num_rep;rep_num;abs_num) 2. 2. rep_num(a) = r a = abs_num(r) iso_pair(;;is_num_rep;rep_num;abs_num)	1 step
2	2. a,r:. 2. iso_pair(;;is_num_rep;rep_num;abs_num) 2. 2. rep_num(a) = r a = abs_num(r) rep_num(m+1) = suc_rep(rep_num(m))	6 steps