Nuprl - Proof: fpf-join-is-empty

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: fpf-join-is-empty

A:Type, eq:EqDecider(A), f,g:x:A fp-> Top.

fpf-is-empty(f

g) ~ (fpf-is-empty(f)

fpf-is-empty(g))

By:	Auto THEN Analyze -2 THEN Analyze -1 THEN Repeat (Unfolds [`fpf-is-empty`;`fpf-join`;`fpf-dom`] 0 THEN Reduce 0) THEN All Thin

Generated subgoal:

1 1. A : Type
2. eq : EqDecider(A)
3. d : A List
4. d1 : A List
(||d @ filter(a.deq-member(eq;a;d);d1)||=0) = ((||d||=0)(||d1||=0))
4 steps

About:

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