Nuprl - Proof: fpf-join wf 1 2 1 1 1

(11steps total) PrintForm Definitions Lemmas mb event system 5 Sections EventSystems Doc

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: fpf-join wf 1 2 1 1 1

1. A : Type
2. B : A

Type
3. f : d:A List

a:{a:A| (a

d) }

B(a)
4. g : d:A List

a:{a:A| (a

d) }

B(a)
5. eq : EqDecider(A)
6. a : A
7. (a

1of(f))

(a

filter(

a.

deq-member(eq;a;1of(f));1of(g)))
8. f

a:A fp-> B(a)
9. g = g
10.

deq-member(eq;a;1of(f))

deq-member(eq;a;1of(g))

By:	Thin -3 THEN RWO Thm* eq:EqDecider(A), L:A List, x:A. deq-member(eq;x;L) (x L) -1 THEN Analyze -3

Generated subgoals:

1 7. (a  1of(f))
8. g = g  a:A fp-> B(a)
9. (a  1of(f))
  deq-member(eq;a;1of(g))
Auto

2 7. (a  filter(a.deq-member(eq;a;1of(f));1of(g)))
8. g = g  a:A fp-> B(a)
9. (a  1of(f))
  deq-member(eq;a;1of(g))
2 steps

About:

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

(11steps total) PrintForm Definitions Lemmas mb event system 5 Sections EventSystems Doc