Nuprl - Proof: delete fenum value is inj genW 1 1

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

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: delete fenum value is inj genW 1 1

1. P :

Prop
2. Q :

Prop
3. f : {u:

| P(u) }

{v:

| Q(v) }
4. Inj({u:

| P(u) }; {v:

| Q(v) }; f)
5. m : {u:

| P(u) }
6. k : {v:

| Q(v) }
7. (Replace value k by f(m) in f)

{u:

| P(u) &

u = m }

{v:

| Q(v) &

v = k }
8. a1 :

9. P(a1) &

a1 = m
10. a2 :

11. P(a2) &

a2 = m
12. (Replace value k by f(m) in f)(a1) = (Replace value k by f(m) in f)(a2)

a1 = a2

{u:

| P(u) &

u = m }

By:	Decide: f(a1) = k THEN Decide: f(a2) = k

Generated subgoals:

1 13. f(a1) = k
14. f(a2) = k
  a1 = a2  {u:| P(u) & u = m }
1 step

2 13. f(a1) = k
14. f(a2) = k
  a1 = a2  {u:| P(u) & u = m }
2 steps

3 13. f(a1) = k
14. f(a2) = k
  a1 = a2  {u:| P(u) & u = m }
3 steps

4 13. f(a1) = k
14. f(a2) = k
  a1 = a2  {u:| P(u) & u = m }
2 steps

About:

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

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

1	13. f(a1) = k 14. f(a2) = k a1 = a2 {u:\| P(u) & u = m }	1 step
2	13. f(a1) = k 14. f(a2) = k a1 = a2 {u:\| P(u) & u = m }	2 steps
3	13. f(a1) = k 14. f(a2) = k a1 = a2 {u:\| P(u) & u = m }	3 steps
4	13. f(a1) = k 14. f(a2) = k a1 = a2 {u:\| P(u) & u = m }	2 steps