Nuprl - Proof: list iso 2 2 1 1 1 2 1 2 1 1 2 1

(37steps total) PrintForm Definitions Lemmas hol list 1 Sections HOLlib Doc

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

1. 'a : S
2. x : (

'a)

3. f :

'a
4. n :

5. x = <

m:

. if m<

n then f(m) else @

x:'a. true

fi ,n>
6. ||f{

n}|| = n-0
7. m :

8.

m<n
9.

m<||f{

n}||
10.

'a:S. arb('a) = (@

x:'a. true

)

(@

x:'a. true

) = arb('a)

By:	SwapEquands 0 THEN Last BackThru THEN StrongAuto THEN Try (Complete (Unfold `label` 0))

Generated subgoals:

None

About:

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

(37steps total) PrintForm Definitions Lemmas hol list 1 Sections HOLlib Doc