Nuprl - Proof: card st vs msize 1 1

(10steps total) PrintForm Definitions Lemmas DiscreteMath Sections DiscrMathExt Doc

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: card st vs msize 1 1

1. a :

2. P :

a

Prop
3. f :

a

2
4.

i:

a. P(i)

f(i) = 1

{x:

a| P(x) } ~ (i:

a

(f(i)))

By:	Witness: Wi(x.<x,0>) {x:a\| P(x) }(i:a(f(i))) \| Wi(xi.xi/x,i. x) (i:a(f(i))){x:a\| P(x) }

Generated subgoals:

1 5. x : {x:a| P(x) }
  0  (f(x))
2 steps

2 5. (x.<x,0>)  {x:a| P(x) }(i:a(f(i)))
6. xi : i:a(f(i))
7. x : a
8. i : (f(x))
9. xi = <x,i>  i:a(f(i))
  x  {x:a| P(x) }
2 steps

3 5. (x.<x,0>)  {x:a| P(x) }(i:a(f(i)))
6. (xi.xi/x,i. x)  (i:a(f(i))){x:a| P(x) }
  InvFuns({x:a| P(x) };i:a(f(i));x.<x,0>;xi.xi/x,i. x)
3 steps

About:

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

(10steps total) PrintForm Definitions Lemmas DiscreteMath Sections DiscrMathExt Doc