Nuprl - Proof: hcons def 1 2 1 1 1

(17steps total) PrintForm Definitions Lemmas hol list 2 Sections HOLlib Doc

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

1. 'a : S
2. h : 'a
3. t : hlist('a)
4. n :

if n<

||t||+1 then cons(h; t)[n] else arb('a) fi

if n =

0 then h else 1of(rep_list('a;t))(pre(n)) fi

By:	BifCase THEN Simp THEN StrongAuto THEN BifCase THEN Simp THEN StrongAuto

Generated subgoals:

1 5. n<||t||+1
6. n = 0
  cons(h; t)[n] = h  'a
1 step

2 5. n<||t||+1
6. n = 0
  cons(h; t)[n] = 1of(rep_list('a;t))(pre(n))  'a
4 steps

3 5. n<||t||+1
6. n = 0
  arb('a) = h
2 steps

4 5. n<||t||+1
6. n = 0
  arb('a) = 1of(rep_list('a;t))(pre(n))
2 steps

About:

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

(17steps total) PrintForm Definitions Lemmas hol list 2 Sections HOLlib Doc

1	5. n<\|\|t\|\|+1 6. n = 0 cons(h; t)[n] = h 'a	1 step
2	5. n<\|\|t\|\|+1 6. n = 0 cons(h; t)[n] = 1of(rep_list('a;t))(pre(n)) 'a	4 steps
3	5. n<\|\|t\|\|+1 6. n = 0 arb('a) = h	2 steps
4	5. n<\|\|t\|\|+1 6. n = 0 arb('a) = 1of(rep_list('a;t))(pre(n))	2 steps