Nuprl - Proof: card boolset vs mset 1 3 1

(22steps total) PrintForm Definitions DiscreteMath Sections DiscrMathExt Doc

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: card boolset vs mset 1 3 1

1. a :

2. k :

3. (

p,i. if p(i)

1 else 0 fi)

(

a {k}

)

a {k}

2
4. (

f,i. f(i)=

(

a {k}

5. p :

a {k}

(

i.if p(i)

1 else 0 fi=

1) = p

By:	Analyze-1 THEN ((i.if p(i) 1 else 0 fi=1) = p a Asserted THEN Analyze)

Generated subgoals:

1 5. p : a
6. size(a)(p) = k
(i.if p(i) 1 else 0 fi=1) = p
4 steps

2 5. p : a
6. size(a)(p) = k
7. (i.if p(i) 1 else 0 fi=1) = p
size(a)(i.if p(i) 1 else 0 fi=1) = k
2 steps

About:

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

(22steps total) PrintForm Definitions DiscreteMath Sections DiscrMathExt Doc

1	5. p : a 6. size(a)(p) = k (i.if p(i) 1 else 0 fi=1) = p	4 steps
2	5. p : a 6. size(a)(p) = k 7. (i.if p(i) 1 else 0 fi=1) = p size(a)(i.if p(i) 1 else 0 fi=1) = k	2 steps