Nuprl - Proof: his sum rep wd 1 1

(9steps total) PrintForm Definitions hol sum Sections HOLlib Doc

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: his sum rep wd 1 1

1. 'a : S
2. 'b : S
3. f : hbool

hbool
4.

u:'a+'b. f = rep_sum(u)

v1:'a, v2:'b.

f = (

b:hbool.

x:'a.

y:'b. (x =

v1)

(hbool

hbool)

(

b:hbool.

x@0:'a.

y:'b. (y =

v2)

(hbool

hbool)

By:	Analyze 4 THEN Analyze 4 THEN StrongAuto THEN Unab [`hrep_sum`] THEN Simp THEN StrongAuto

Generated subgoals:

1 4. x : 'a
5. f = (b:. x@0:'a. y:'b. (x@0 = x)b)  'a'b
  v1:'a, v2:'b.
  f = (b:hbool. x:'a. y:'b. (x = v1)b)  (hbool  'a  'b  hbool)
   f
   =
   (b:hbool. x@0:'a. y:'b. (y = v2)b)
    (hbool  'a  'b  hbool)
1 step

2 4. y : 'b
5. f = (b:. x:'a. y@0:'b. (y@0 = y)b)  'a'b
  v1:'a, v2:'b.
  f = (b:hbool. x:'a. y:'b. (x = v1)b)  (hbool  'a  'b  hbool)
   f
   =
   (b:hbool. x@0:'a. y:'b. (y = v2)b)
    (hbool  'a  'b  hbool)
1 step

About:

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

(9steps total) PrintForm Definitions hol sum Sections HOLlib Doc

1	4. x : 'a 5. f = (b:. x@0:'a. y:'b. (x@0 = x)b) 'a'b v1:'a, v2:'b. f = (b:hbool. x:'a. y:'b. (x = v1)b) (hbool 'a 'b hbool) f = (b:hbool. x@0:'a. y:'b. (y = v2)b) (hbool 'a 'b hbool)	1 step
2	4. y : 'b 5. f = (b:. x:'a. y@0:'b. (y@0 = y)b) 'a'b v1:'a, v2:'b. f = (b:hbool. x:'a. y:'b. (x = v1)b) (hbool 'a 'b hbool) f = (b:hbool. x@0:'a. y:'b. (y = v2)b) (hbool 'a 'b hbool)	1 step