Nuprl - Proof: fpf-join wf 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

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:A| (a

1of(f) @ filter(

dom(f);1of(g))) }
7. f

a:A fp-> B(a)
8. g

a:A fp-> B(a)

f(a)?g(a)

B(a)

By:	Analyze -3 THEN Unfold `fpf-cap` 0 THEN SplitOnConclITE

Generated subgoals:

1 6. a : A
7. (a  1of(f) @ filter(a.a  dom(f);1of(g)))
8. f  a:A fp-> B(a)
9. g  a:A fp-> B(a)
10. a  dom(f)
  f(a)  B(a)
1 step

2 6. a : A
7. (a  1of(f) @ filter(a.a  dom(f);1of(g)))
8. f  a:A fp-> B(a)
9. g  a:A fp-> B(a)
10. a  dom(f)
  g(a)  B(a)
8 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

1	6. a : A 7. (a 1of(f) @ filter(a.a dom(f);1of(g))) 8. f a:A fp-> B(a) 9. g a:A fp-> B(a) 10. a dom(f) f(a) B(a)	1 step
2	6. a : A 7. (a 1of(f) @ filter(a.a dom(f);1of(g))) 8. f a:A fp-> B(a) 9. g a:A fp-> B(a) 10. a dom(f) g(a) B(a)	8 steps