%------------------------------------------------------------------------------ % File : cocATP---0.2.0 % Problem : SEU665^2 : TPTP v6.1.0. Released v3.7.0. % Transfm : none % Format : tptp:raw % Command : python CASC.py /export/starexec/sandbox/benchmark/theBenchmark.p % Computer : n188.star.cs.uiowa.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2609 0 2.40GHz % Memory : 32286.75MB % OS : Linux 2.6.32-431.20.3.el6.x86_64 % CPULimit : 300s % DateTime : Thu Jul 17 13:32:45 EDT 2014 % Result : Theorem 3.58s % Output : Proof 3.58s % Verified : % SZS Type : None (Parsing solution fails) % Syntax : Number of formulae : 0 % Comments : %------------------------------------------------------------------------------ %----ERROR: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % % Problem : SEU665^2 : TPTP v6.1.0. Released v3.7.0. % % Command : python CASC.py /export/starexec/sandbox/benchmark/theBenchmark.p % % Computer : n188.star.cs.uiowa.edu % % Model : x86_64 x86_64 % % CPU : Intel(R) Xeon(R) CPU E5-2609 0 @ 2.40GHz % % Memory : 32286.75MB % % OS : Linux 2.6.32-431.20.3.el6.x86_64 % % CPULimit : 300 % % DateTime : Thu Jul 17 11:05:56 CDT 2014 % % CPUTime : 3.58 % Python 2.7.5 % Using paths ['/home/cristobal/cocATP/CASC/TPTP/', '/export/starexec/sandbox/benchmark/', '/export/starexec/sandbox/benchmark/'] % FOF formula (<kernel.Constant object at 0xc9de60>, <kernel.DependentProduct object at 0xc9d488>) of role type named in_type % Using role type % Declaring in:(fofType->(fofType->Prop)) % FOF formula (<kernel.Constant object at 0xc9f098>, <kernel.DependentProduct object at 0xc9d200>) of role type named dsetconstr_type % Using role type % Declaring dsetconstr:(fofType->((fofType->Prop)->fofType)) % FOF formula (<kernel.Constant object at 0xc9d908>, <kernel.Sort object at 0x72b368>) of role type named dsetconstrI_type % Using role type % Declaring dsetconstrI:Prop % FOF formula (((eq Prop) dsetconstrI) (forall (A:fofType) (Xphi:(fofType->Prop)) (Xx:fofType), (((in Xx) A)->((Xphi Xx)->((in Xx) ((dsetconstr A) (fun (Xy:fofType)=> (Xphi Xy)))))))) of role definition named dsetconstrI % A new definition: (((eq Prop) dsetconstrI) (forall (A:fofType) (Xphi:(fofType->Prop)) (Xx:fofType), (((in Xx) A)->((Xphi Xx)->((in Xx) ((dsetconstr A) (fun (Xy:fofType)=> (Xphi Xy)))))))) % Defined: dsetconstrI:=(forall (A:fofType) (Xphi:(fofType->Prop)) (Xx:fofType), (((in Xx) A)->((Xphi Xx)->((in Xx) ((dsetconstr A) (fun (Xy:fofType)=> (Xphi Xy))))))) % FOF formula (<kernel.Constant object at 0x72b830>, <kernel.Sort object at 0x72b368>) of role type named setext_type % Using role type % Declaring setext:Prop % FOF formula (((eq Prop) setext) (forall (A:fofType) (B:fofType), ((forall (Xx:fofType), (((in Xx) A)->((in Xx) B)))->((forall (Xx:fofType), (((in Xx) B)->((in Xx) A)))->(((eq fofType) A) B))))) of role definition named setext % A new definition: (((eq Prop) setext) (forall (A:fofType) (B:fofType), ((forall (Xx:fofType), (((in Xx) A)->((in Xx) B)))->((forall (Xx:fofType), (((in Xx) B)->((in Xx) A)))->(((eq fofType) A) B))))) % Defined: setext:=(forall (A:fofType) (B:fofType), ((forall (Xx:fofType), (((in Xx) A)->((in Xx) B)))->((forall (Xx:fofType), (((in Xx) B)->((in Xx) A)))->(((eq fofType) A) B)))) % FOF formula (<kernel.Constant object at 0xc3ee18>, <kernel.DependentProduct object at 0xc9d200>) of role type named kpair_type % Using role type % Declaring kpair:(fofType->(fofType->fofType)) % FOF formula (<kernel.Constant object at 0xc3ebd8>, <kernel.DependentProduct object at 0xc9dc68>) of role type named cartprod_type % Using role type % Declaring cartprod:(fofType->(fofType->fofType)) % FOF formula (<kernel.Constant object at 0xc3ee18>, <kernel.Sort object at 0x72b368>) of role type named cartprodpairin_type % Using role type % Declaring cartprodpairin:Prop % FOF formula (((eq Prop) cartprodpairin) (forall (A:fofType) (B:fofType) (Xx:fofType), (((in Xx) A)->(forall (Xy:fofType), (((in Xy) B)->((in ((kpair Xx) Xy)) ((cartprod A) B))))))) of role definition named cartprodpairin % A new definition: (((eq Prop) cartprodpairin) (forall (A:fofType) (B:fofType) (Xx:fofType), (((in Xx) A)->(forall (Xy:fofType), (((in Xy) B)->((in ((kpair Xx) Xy)) ((cartprod A) B))))))) % Defined: cartprodpairin:=(forall (A:fofType) (B:fofType) (Xx:fofType), (((in Xx) A)->(forall (Xy:fofType), (((in Xy) B)->((in ((kpair Xx) Xy)) ((cartprod A) B)))))) % FOF formula (<kernel.Constant object at 0xc9d908>, <kernel.DependentProduct object at 0xc9d488>) of role type named dpsetconstr_type % Using role type % Declaring dpsetconstr:(fofType->(fofType->((fofType->(fofType->Prop))->fofType))) % FOF formula (((eq (fofType->(fofType->((fofType->(fofType->Prop))->fofType)))) dpsetconstr) (fun (A:fofType) (B:fofType) (Xphi:(fofType->(fofType->Prop)))=> ((dsetconstr ((cartprod A) B)) (fun (Xu:fofType)=> ((ex fofType) (fun (Xx:fofType)=> ((and ((in Xx) A)) ((ex fofType) (fun (Xy:fofType)=> ((and ((and ((in Xy) B)) ((Xphi Xx) Xy))) (((eq fofType) Xu) ((kpair Xx) Xy)))))))))))) of role definition named dpsetconstr % A new definition: (((eq (fofType->(fofType->((fofType->(fofType->Prop))->fofType)))) dpsetconstr) (fun (A:fofType) (B:fofType) (Xphi:(fofType->(fofType->Prop)))=> ((dsetconstr ((cartprod A) B)) (fun (Xu:fofType)=> ((ex fofType) (fun (Xx:fofType)=> ((and ((in Xx) A)) ((ex fofType) (fun (Xy:fofType)=> ((and ((and ((in Xy) B)) ((Xphi Xx) Xy))) (((eq fofType) Xu) ((kpair Xx) Xy)))))))))))) % Defined: dpsetconstr:=(fun (A:fofType) (B:fofType) (Xphi:(fofType->(fofType->Prop)))=> ((dsetconstr ((cartprod A) B)) (fun (Xu:fofType)=> ((ex fofType) (fun (Xx:fofType)=> ((and ((in Xx) A)) ((ex fofType) (fun (Xy:fofType)=> ((and ((and ((in Xy) B)) ((Xphi Xx) Xy))) (((eq fofType) Xu) ((kpair Xx) Xy))))))))))) % FOF formula (dsetconstrI->(setext->(cartprodpairin->(forall (A:fofType) (B:fofType) (Xphi:(fofType->(fofType->Prop))) (Xx:fofType), (((in Xx) A)->(forall (Xy:fofType), (((in Xy) B)->(((Xphi Xx) Xy)->((in ((kpair Xx) Xy)) (((dpsetconstr A) B) (fun (Xz:fofType) (Xu:fofType)=> ((Xphi Xz) Xu)))))))))))) of role conjecture named dpsetconstrI % Conjecture to prove = (dsetconstrI->(setext->(cartprodpairin->(forall (A:fofType) (B:fofType) (Xphi:(fofType->(fofType->Prop))) (Xx:fofType), (((in Xx) A)->(forall (Xy:fofType), (((in Xy) B)->(((Xphi Xx) Xy)->((in ((kpair Xx) Xy)) (((dpsetconstr A) B) (fun (Xz:fofType) (Xu:fofType)=> ((Xphi Xz) Xu)))))))))))):Prop % Parameter fofType_DUMMY:fofType. % We need to prove ['(dsetconstrI->(setext->(cartprodpairin->(forall (A:fofType) (B:fofType) (Xphi:(fofType->(fofType->Prop))) (Xx:fofType), (((in Xx) A)->(forall (Xy:fofType), (((in Xy) B)->(((Xphi Xx) Xy)->((in ((kpair Xx) Xy)) (((dpsetconstr A) B) (fun (Xz:fofType) (Xu:fofType)=> ((Xphi Xz) Xu))))))))))))'] % Parameter fofType:Type. % Parameter in:(fofType->(fofType->Prop)). % Parameter dsetconstr:(fofType->((fofType->Prop)->fofType)). % Definition dsetconstrI:=(forall (A:fofType) (Xphi:(fofType->Prop)) (Xx:fofType), (((in Xx) A)->((Xphi Xx)->((in Xx) ((dsetconstr A) (fun (Xy:fofType)=> (Xphi Xy))))))):Prop. % Definition setext:=(forall (A:fofType) (B:fofType), ((forall (Xx:fofType), (((in Xx) A)->((in Xx) B)))->((forall (Xx:fofType), (((in Xx) B)->((in Xx) A)))->(((eq fofType) A) B)))):Prop. % Parameter kpair:(fofType->(fofType->fofType)). % Parameter cartprod:(fofType->(fofType->fofType)). % Definition cartprodpairin:=(forall (A:fofType) (B:fofType) (Xx:fofType), (((in Xx) A)->(forall (Xy:fofType), (((in Xy) B)->((in ((kpair Xx) Xy)) ((cartprod A) B)))))):Prop. % Definition dpsetconstr:=(fun (A:fofType) (B:fofType) (Xphi:(fofType->(fofType->Prop)))=> ((dsetconstr ((cartprod A) B)) (fun (Xu:fofType)=> ((ex fofType) (fun (Xx:fofType)=> ((and ((in Xx) A)) ((ex fofType) (fun (Xy:fofType)=> ((and ((and ((in Xy) B)) ((Xphi Xx) Xy))) (((eq fofType) Xu) ((kpair Xx) Xy))))))))))):(fofType->(fofType->((fofType->(fofType->Prop))->fofType))). % Trying to prove (dsetconstrI->(setext->(cartprodpairin->(forall (A:fofType) (B:fofType) (Xphi:(fofType->(fofType->Prop))) (Xx:fofType), (((in Xx) A)->(forall (Xy:fofType), (((in Xy) B)->(((Xphi Xx) Xy)->((in ((kpair Xx) Xy)) (((dpsetconstr A) B) (fun (Xz:fofType) (Xu:fofType)=> ((Xphi Xz) Xu)))))))))))) % Found x1000000:=(x100000 x3):((in ((kpair Xx) Xy)) ((cartprod A) B)) % Found (x100000 x3) as proof of ((in ((kpair Xx) Xy)) ((cartprod A) B)) % Found ((x10000 Xy) x3) as proof of ((in ((kpair Xx) Xy)) ((cartprod A) B)) % Found (((x1000 x2) Xy) x3) as proof of ((in ((kpair Xx) Xy)) ((cartprod A) B)) % Found ((((x100 Xx) x2) Xy) x3) as proof of ((in ((kpair Xx) Xy)) ((cartprod A) B)) % Found (((((x10 B) Xx) x2) Xy) x3) as proof of ((in ((kpair Xx) Xy)) ((cartprod A) B)) % Found ((((((x1 A) B) Xx) x2) Xy) x3) as proof of ((in ((kpair Xx) Xy)) ((cartprod A) B)) % Found ((((((x1 A) B) Xx) x2) Xy) x3) as proof of ((in ((kpair Xx) Xy)) ((cartprod A) B)) % Found x2:((in Xx) A) % Instantiate: x6:=Xx:fofType % Found x2 as proof of ((in x6) A) % Found x5:((in Xx0) A0) % Instantiate: A0:=((dsetconstr ((cartprod A) B)) (fun (Xu:fofType)=> ((ex fofType) (fun (Xx:fofType)=> ((and ((in Xx) A)) ((ex fofType) (fun (Xy:fofType)=> ((and ((and ((in Xy) B)) (((fun (Xz:fofType) (Xu:fofType)=> ((Xphi Xz) Xu)) Xx) Xy))) (((eq fofType) Xu) ((kpair Xx) Xy)))))))))):fofType % Found (fun (x5:((in Xx0) A0))=> x5) as proof of ((in Xx0) (((dpsetconstr A) B) (fun (Xz:fofType) (Xu:fofType)=> ((Xphi Xz) Xu)))) % Found (fun (Xx0:fofType) (x5:((in Xx0) A0))=> x5) as proof of (((in Xx0) A0)->((in Xx0) (((dpsetconstr A) B) (fun (Xz:fofType) (Xu:fofType)=> ((Xphi Xz) Xu))))) % Found (fun (Xx0:fofType) (x5:((in Xx0) A0))=> x5) as proof of (forall (Xx:fofType), (((in Xx) A0)->((in Xx) (((dpsetconstr A) B) (fun (Xz:fofType) (Xu:fofType)=> ((Xphi Xz) Xu)))))) % Found x5:((in Xx0) (((dpsetconstr A) B) (fun (Xz:fofType) (Xu:fofType)=> ((Xphi Xz) Xu)))) % Instantiate: A0:=(((dpsetconstr A) B) (fun (Xz:fofType) (Xu:fofType)=> ((Xphi Xz) Xu))):fofType % Found (fun (x5:((in Xx0) (((dpsetconstr A) B) (fun (Xz:fofType) (Xu:fofType)=> ((Xphi Xz) Xu)))))=> x5) as proof of ((in Xx0) A0) % Found (fun (Xx0:fofType) (x5:((in Xx0) (((dpsetconstr A) B) (fun (Xz:fofType) (Xu:fofType)=> ((Xphi Xz) Xu)))))=> x5) as proof of (((in Xx0) (((dpsetconstr A) B) (fun (Xz:fofType) (Xu:fofType)=> ((Xphi Xz) Xu))))->((in Xx0) A0)) % Found (fun (Xx0:fofType) (x5:((in Xx0) (((dpsetconstr A) B) (fun (Xz:fofType) (Xu:fofType)=> ((Xphi Xz) Xu)))))=> x5) as proof of (forall (Xx:fofType), (((in Xx) (((dpsetconstr A) B) (fun (Xz:fofType) (Xu:fofType)=> ((Xphi Xz) Xu))))->((in Xx) A0))) % Found eta_expansion000:=(eta_expansion00 (fun (Xx1:fofType)=> ((and ((in Xx1) A)) ((ex fofType) (fun (Xy0:fofType)=> ((and ((and ((in Xy0) B)) ((Xphi Xx1) Xy0))) (((eq fofType) ((kpair Xx) Xy)) ((kpair Xx1) Xy0)))))))):(((eq (fofType->Prop)) (fun (Xx1:fofType)=> ((and ((in Xx1) A)) ((ex fofType) (fun (Xy0:fofType)=> ((and ((and ((in Xy0) B)) ((Xphi Xx1) Xy0))) (((eq fofType) ((kpair Xx) Xy)) ((kpair Xx1) Xy0)))))))) (fun (x:fofType)=> ((and ((in x) A)) ((ex fofType) (fun (Xy0:fofType)=> ((and ((and ((in Xy0) B)) ((Xphi x) Xy0))) (((eq fofType) ((kpair Xx) Xy)) ((kpair x) Xy0)))))))) % Found (eta_expansion00 (fun (Xx1:fofType)=> ((and ((in Xx1) A)) ((ex fofType) (fun (Xy0:fofType)=> ((and ((and ((in Xy0) B)) ((Xphi Xx1) Xy0))) (((eq fofType) ((kpair Xx) Xy)) ((kpair Xx1) Xy0)))))))) as proof of (((eq (fofType->Prop)) (fun (Xx1:fofType)=> ((and ((in Xx1) A)) ((ex fofType) (fun (Xy0:fofType)=> ((and ((and ((in Xy0) B)) ((Xphi Xx1) Xy0))) (((eq fofType) ((kpair Xx) Xy)) ((kpair Xx1) Xy0)))))))) b) % Found ((eta_expansion0 Prop) (fun (Xx1:fofType)=> ((and ((in Xx1) A)) ((ex fofType) (fun (Xy0:fofType)=> ((and ((and ((in Xy0) B)) ((Xphi Xx1) Xy0))) (((eq fofType) ((kpair Xx) Xy)) ((kpair Xx1) Xy0)))))))) as proof of (((eq (fofType->Prop)) (fun (Xx1:fofType)=> ((and ((in Xx1) A)) ((ex fofType) (fun (Xy0:fofType)=> ((and ((and ((in Xy0) B)) ((Xphi Xx1) Xy0))) (((eq fofType) ((kpair Xx) Xy)) ((kpair Xx1) Xy0)))))))) b) % Found (((eta_expansion fofType) Prop) (fun (Xx1:fofType)=> ((and ((in Xx1) A)) ((ex fofType) (fun (Xy0:fofType)=> ((and ((and ((in Xy0) B)) ((Xphi Xx1) Xy0))) (((eq fofType) ((kpair Xx) Xy)) ((kpair Xx1) Xy0)))))))) as proof of (((eq (fofType->Prop)) (fun (Xx1:fofType)=> ((and ((in Xx1) A)) ((ex fofType) (fun (Xy0:fofType)=> ((and ((and ((in Xy0) B)) ((Xphi Xx1) Xy0))) (((eq fofType) ((kpair Xx) Xy)) ((kpair Xx1) Xy0)))))))) b) % Found (((eta_expansion fofType) Prop) (fun (Xx1:fofType)=> ((and ((in Xx1) A)) ((ex fofType) (fun (Xy0:fofType)=> ((and ((and ((in Xy0) B)) ((Xphi Xx1) Xy0))) (((eq fofType) ((kpair Xx) Xy)) ((kpair Xx1) Xy0)))))))) as proof of (((eq (fofType->Prop)) (fun (Xx1:fofType)=> ((and ((in Xx1) A)) ((ex fofType) (fun (Xy0:fofType)=> ((and ((and ((in Xy0) B)) ((Xphi Xx1) Xy0))) (((eq fofType) ((kpair Xx) Xy)) ((kpair Xx1) Xy0)))))))) b) % Found (((eta_expansion fofType) Prop) (fun (Xx1:fofType)=> ((and ((in Xx1) A)) ((ex fofType) (fun (Xy0:fofType)=> ((and ((and ((in Xy0) B)) ((Xphi Xx1) Xy0))) (((eq fofType) ((kpair Xx) Xy)) ((kpair Xx1) Xy0)))))))) as proof of (((eq (fofType->Prop)) (fun (Xx1:fofType)=> ((and ((in Xx1) A)) ((ex fofType) (fun (Xy0:fofType)=> ((and ((and ((in Xy0) B)) ((Xphi Xx1) Xy0))) (((eq fofType) ((kpair Xx) Xy)) ((kpair Xx1) Xy0)))))))) b) % Found eq_ref00:=(eq_ref0 (f x6)):(((eq Prop) (f x6)) (f x6)) % Found (eq_ref0 (f x6)) as proof of (((eq Prop) (f x6)) ((and ((in x6) A)) ((ex fofType) (fun (Xy0:fofType)=> ((and ((and ((in Xy0) B)) ((Xphi x6) Xy0))) (((eq fofType) ((kpair Xx) Xy)) ((kpair x6) Xy0))))))) % Found ((eq_ref Prop) (f x6)) as proof of (((eq Prop) (f x6)) ((and ((in x6) A)) ((ex fofType) (fun (Xy0:fofType)=> ((and ((and ((in Xy0) B)) ((Xphi x6) Xy0))) (((eq fofType) ((kpair Xx) Xy)) ((kpair x6) Xy0))))))) % Found ((eq_ref Prop) (f x6)) as proof of (((eq Prop) (f x6)) ((and ((in x6) A)) ((ex fofType) (fun (Xy0:fofType)=> ((and ((and ((in Xy0) B)) ((Xphi x6) Xy0))) (((eq fofType) ((kpair Xx) Xy)) ((kpair x6) Xy0))))))) % Found (fun (x6:fofType)=> ((eq_ref Prop) (f x6))) as proof of (((eq Prop) (f x6)) ((and ((in x6) A)) ((ex fofType) (fun (Xy0:fofType)=> ((and ((and ((in Xy0) B)) ((Xphi x6) Xy0))) (((eq fofType) ((kpair Xx) Xy)) ((kpair x6) Xy0))))))) % Found (fun (x6:fofType)=> ((eq_ref Prop) (f x6))) as proof of (forall (x:fofType), (((eq Prop) (f x)) ((and ((in x) A)) ((ex fofType) (fun (Xy0:fofType)=> ((and ((and ((in Xy0) B)) ((Xphi x) Xy0))) (((eq fofType) ((kpair Xx) Xy)) ((kpair x) Xy0)))))))) % Found eq_ref00:=(eq_ref0 (f x6)):(((eq Prop) (f x6)) (f x6)) % Found (eq_ref0 (f x6)) as proof of (((eq Prop) (f x6)) ((and ((in x6) A)) ((ex fofType) (fun (Xy0:fofType)=> ((and ((and ((in Xy0) B)) ((Xphi x6) Xy0))) (((eq fofType) ((kpair Xx) Xy)) ((kpair x6) Xy0))))))) % Found ((eq_ref Prop) (f x6)) as proof of (((eq Prop) (f x6)) ((and ((in x6) A)) ((ex fofType) (fun (Xy0:fofType)=> ((and ((and ((in Xy0) B)) ((Xphi x6) Xy0))) (((eq fofType) ((kpair Xx) Xy)) ((kpair x6) Xy0))))))) % Found ((eq_ref Prop) (f x6)) as proof of (((eq Prop) (f x6)) ((and ((in x6) A)) ((ex fofType) (fun (Xy0:fofType)=> ((and ((and ((in Xy0) B)) ((Xphi x6) Xy0))) (((eq fofType) ((kpair Xx) Xy)) ((kpair x6) Xy0))))))) % Found (fun (x6:fofType)=> ((eq_ref Prop) (f x6))) as proof of (((eq Prop) (f x6)) ((and ((in x6) A)) ((ex fofType) (fun (Xy0:fofType)=> ((and ((and ((in Xy0) B)) ((Xphi x6) Xy0))) (((eq fofType) ((kpair Xx) Xy)) ((kpair x6) Xy0))))))) % Found (fun (x6:fofType)=> ((eq_ref Prop) (f x6))) as proof of (forall (x:fofType), (((eq Prop) (f x)) ((and ((in x) A)) ((ex fofType) (fun (Xy0:fofType)=> ((and ((and ((in Xy0) B)) ((Xphi x) Xy0))) (((eq fofType) ((kpair Xx) Xy)) ((kpair x) Xy0)))))))) % Found x1000000:=(x100000 x3):((in ((kpair Xx) Xy)) ((cartprod A) B)) % Found (x100000 x3) as proof of ((in ((kpair Xx) Xy)) ((cartprod A) B)) % Found ((x10000 Xy) x3) as proof of ((in ((kpair Xx) Xy)) ((cartprod A) B)) % Found (((x1000 x2) Xy) x3) as proof of ((in ((kpair Xx) Xy)) ((cartprod A) B)) % Found ((((x100 Xx) x2) Xy) x3) as proof of ((in ((kpair Xx) Xy)) ((cartprod A) B)) % Found (((((x10 B) Xx) x2) Xy) x3) as proof of ((in ((kpair Xx) Xy)) ((cartprod A) B)) % Found ((((((x1 A) B) Xx) x2) Xy) x3) as proof of ((in ((kpair Xx) Xy)) ((cartprod A) B)) % Found ((((((x1 A) B) Xx) x2) Xy) x3) as proof of ((in ((kpair Xx) Xy)) ((cartprod A) B)) % Found x1000000:=(x100000 x3):((in ((kpair Xx) Xy)) ((cartprod A) B)) % Found (x100000 x3) as proof of ((in ((kpair Xx) Xy)) ((cartprod A) B)) % Found ((x10000 Xy) x3) as proof of ((in ((kpair Xx) Xy)) ((cartprod A) B)) % Found (((x1000 x2) Xy) x3) as proof of ((in ((kpair Xx) Xy)) ((cartprod A) B)) % Found ((((x100 Xx) x2) Xy) x3) as proof of ((in ((kpair Xx) Xy)) ((cartprod A) B)) % Found (((((x10 B) Xx) x2) Xy) x3) as proof of ((in ((kpair Xx) Xy)) ((cartprod A) B)) % Found ((((((x1 A) B) Xx) x2) Xy) x3) as proof of ((in ((kpair Xx) Xy)) ((cartprod A) B)) % Found ((((((x1 A) B) Xx) x2) Xy) x3) as proof of ((in ((kpair Xx) Xy)) ((cartprod A) B)) % Found eq_ref00:=(eq_ref0 ((kpair Xx) Xy)):(((eq fofType) ((kpair Xx) Xy)) ((kpair Xx) Xy)) % Found (eq_ref0 ((kpair Xx) Xy)) as proof of (((eq fofType) ((kpair Xx) Xy)) ((kpair x6) x7)) % Found ((eq_ref fofType) ((kpair Xx) Xy)) as proof of (((eq fofType) ((kpair Xx) Xy)) ((kpair x6) x7)) % Found ((eq_ref fofType) ((kpair Xx) Xy)) as proof of (((eq fofType) ((kpair Xx) Xy)) ((kpair x6) x7)) % Found ((eq_ref fofType) ((kpair Xx) Xy)) as proof of (((eq fofType) ((kpair Xx) Xy)) ((kpair x6) x7)) % Found eq_ref00:=(eq_ref0 ((kpair Xx) Xy)):(((eq fofType) ((kpair Xx) Xy)) ((kpair Xx) Xy)) % Found (eq_ref0 ((kpair Xx) Xy)) as proof of (((eq fofType) ((kpair Xx) Xy)) ((kpair x6) x7)) % Found ((eq_ref fofType) ((kpair Xx) Xy)) as proof of (((eq fofType) ((kpair Xx) Xy)) ((kpair x6) x7)) % Found ((eq_ref fofType) ((kpair Xx) Xy)) as proof of (((eq fofType) ((kpair Xx) Xy)) ((kpair x6) x7)) % Found ((eq_ref fofType) ((kpair Xx) Xy)) as proof of (((eq fofType) ((kpair Xx) Xy)) ((kpair x6) x7)) % Found ((eq_ref fofType) ((kpair Xx) Xy)) as proof of (((eq fofType) ((kpair Xx) Xy)) ((kpair x6) x7)) % Found conj2000:=(conj200 x4):((and ((in x7) B)) ((Xphi x6) x7)) % Found (conj200 x4) as proof of ((and ((in x7) B)) ((Xphi x6) x7)) % Found ((conj20 ((Xphi x6) x7)) x4) as proof of ((and ((in x7) B)) ((Xphi x6) x7)) % Found (((fun (B0:Prop)=> ((conj2 B0) x3)) ((Xphi x6) x7)) x4) as proof of ((and ((in x7) B)) ((Xphi x6) x7)) % Found (((fun (B0:Prop)=> (((conj ((in x7) B)) B0) x3)) ((Xphi x6) x7)) x4) as proof of ((and ((in x7) B)) ((Xphi x6) x7)) % Found (((fun (B0:Prop)=> (((conj ((in x7) B)) B0) x3)) ((Xphi x6) x7)) x4) as proof of ((and ((in x7) B)) ((Xphi x6) x7)) % Found ((conj10 (((fun (B0:Prop)=> (((conj ((in x7) B)) B0) x3)) ((Xphi x6) x7)) x4)) ((eq_ref fofType) ((kpair Xx) Xy))) as proof of ((and ((and ((in x7) B)) ((Xphi x6) x7))) (((eq fofType) ((kpair Xx) Xy)) ((kpair x6) x7))) % Found (((conj1 (((eq fofType) ((kpair Xx) Xy)) ((kpair x6) x7))) (((fun (B0:Prop)=> (((conj ((in x7) B)) B0) x3)) ((Xphi x6) x7)) x4)) ((eq_ref fofType) ((kpair Xx) Xy))) as proof of ((and ((and ((in x7) B)) ((Xphi x6) x7))) (((eq fofType) ((kpair Xx) Xy)) ((kpair x6) x7))) % Found ((((conj ((and ((in x7) B)) ((Xphi x6) x7))) (((eq fofType) ((kpair Xx) Xy)) ((kpair x6) x7))) (((fun (B0:Prop)=> (((conj ((in x7) B)) B0) x3)) ((Xphi x6) x7)) x4)) ((eq_ref fofType) ((kpair Xx) Xy))) as proof of ((and ((and ((in x7) B)) ((Xphi x6) x7))) (((eq fofType) ((kpair Xx) Xy)) ((kpair x6) x7))) % Found ((((conj ((and ((in x7) B)) ((Xphi x6) x7))) (((eq fofType) ((kpair Xx) Xy)) ((kpair x6) x7))) (((fun (B0:Prop)=> (((conj ((in x7) B)) B0) x3)) ((Xphi x6) x7)) x4)) ((eq_ref fofType) ((kpair Xx) Xy))) as proof of ((and ((and ((in x7) B)) ((Xphi x6) x7))) (((eq fofType) ((kpair Xx) Xy)) ((kpair x6) x7))) % Found (ex_intro010 ((((conj ((and ((in x7) B)) ((Xphi x6) x7))) (((eq fofType) ((kpair Xx) Xy)) ((kpair x6) x7))) (((fun (B0:Prop)=> (((conj ((in x7) B)) B0) x3)) ((Xphi x6) x7)) x4)) ((eq_ref fofType) ((kpair Xx) Xy)))) as proof of ((ex fofType) (fun (Xy0:fofType)=> ((and ((and ((in Xy0) B)) ((Xphi x6) Xy0))) (((eq fofType) ((kpair Xx) Xy)) ((kpair x6) Xy0))))) % Found ((ex_intro01 Xy) ((((conj ((and ((in Xy) B)) ((Xphi x6) Xy))) (((eq fofType) ((kpair Xx) Xy)) ((kpair x6) Xy))) (((fun (B0:Prop)=> (((conj ((in Xy) B)) B0) x3)) ((Xphi x6) Xy)) x4)) ((eq_ref fofType) ((kpair Xx) Xy)))) as proof of ((ex fofType) (fun (Xy0:fofType)=> ((and ((and ((in Xy0) B)) ((Xphi x6) Xy0))) (((eq fofType) ((kpair Xx) Xy)) ((kpair x6) Xy0))))) % Found (((ex_intro0 (fun (Xy0:fofType)=> ((and ((and ((in Xy0) B)) ((Xphi x6) Xy0))) (((eq fofType) ((kpair Xx) Xy)) ((kpair x6) Xy0))))) Xy) ((((conj ((and ((in Xy) B)) ((Xphi x6) Xy))) (((eq fofType) ((kpair Xx) Xy)) ((kpair x6) Xy))) (((fun (B0:Prop)=> (((conj ((in Xy) B)) B0) x3)) ((Xphi x6) Xy)) x4)) ((eq_ref fofType) ((kpair Xx) Xy)))) as proof of ((ex fofType) (fun (Xy0:fofType)=> ((and ((and ((in Xy0) B)) ((Xphi x6) Xy0))) (((eq fofType) ((kpair Xx) Xy)) ((kpair x6) Xy0))))) % Found (((ex_intro0 (fun (Xy0:fofType)=> ((and ((and ((in Xy0) B)) ((Xphi x6) Xy0))) (((eq fofType) ((kpair Xx) Xy)) ((kpair x6) Xy0))))) Xy) ((((conj ((and ((in Xy) B)) ((Xphi x6) Xy))) (((eq fofType) ((kpair Xx) Xy)) ((kpair x6) Xy))) (((fun (B0:Prop)=> (((conj ((in Xy) B)) B0) x3)) ((Xphi x6) Xy)) x4)) ((eq_ref fofType) ((kpair Xx) Xy)))) as proof of ((ex fofType) (fun (Xy0:fofType)=> ((and ((and ((in Xy0) B)) ((Xphi x6) Xy0))) (((eq fofType) ((kpair Xx) Xy)) ((kpair x6) Xy0))))) % Found ((conj00 x2) (((ex_intro0 (fun (Xy0:fofType)=> ((and ((and ((in Xy0) B)) ((Xphi x6) Xy0))) (((eq fofType) ((kpair Xx) Xy)) ((kpair x6) Xy0))))) Xy) ((((conj ((and ((in Xy) B)) ((Xphi x6) Xy))) (((eq fofType) ((kpair Xx) Xy)) ((kpair x6) Xy))) (((fun (B0:Prop)=> (((conj ((in Xy) B)) B0) x3)) ((Xphi x6) Xy)) x4)) ((eq_ref fofType) ((kpair Xx) Xy))))) as proof of ((and ((in x6) A)) ((ex fofType) (fun (Xy0:fofType)=> ((and ((and ((in Xy0) B)) ((Xphi x6) Xy0))) (((eq fofType) ((kpair Xx) Xy)) ((kpair x6) Xy0)))))) % Found (((conj0 ((ex fofType) (fun (Xy0:fofType)=> ((and ((and ((in Xy0) B)) ((Xphi x6) Xy0))) (((eq fofType) ((kpair Xx) Xy)) ((kpair x6) Xy0)))))) x2) (((ex_intro0 (fun (Xy0:fofType)=> ((and ((and ((in Xy0) B)) ((Xphi x6) Xy0))) (((eq fofType) ((kpair Xx) Xy)) ((kpair x6) Xy0))))) Xy) ((((conj ((and ((in Xy) B)) ((Xphi x6) Xy))) (((eq fofType) ((kpair Xx) Xy)) ((kpair x6) Xy))) (((fun (B0:Prop)=> (((conj ((in Xy) B)) B0) x3)) ((Xphi x6) Xy)) x4)) ((eq_ref fofType) ((kpair Xx) Xy))))) as proof of ((and ((in x6) A)) ((ex fofType) (fun (Xy0:fofType)=> ((and ((and ((in Xy0) B)) ((Xphi x6) Xy0))) (((eq fofType) ((kpair Xx) Xy)) ((kpair x6) Xy0)))))) % Found ((((conj ((in x6) A)) ((ex fofType) (fun (Xy0:fofType)=> ((and ((and ((in Xy0) B)) ((Xphi x6) Xy0))) (((eq fofType) ((kpair Xx) Xy)) ((kpair x6) Xy0)))))) x2) (((ex_intro0 (fun (Xy0:fofType)=> ((and ((and ((in Xy0) B)) ((Xphi x6) Xy0))) (((eq fofType) ((kpair Xx) Xy)) ((kpair x6) Xy0))))) Xy) ((((conj ((and ((in Xy) B)) ((Xphi x6) Xy))) (((eq fofType) ((kpair Xx) Xy)) ((kpair x6) Xy))) (((fun (B0:Prop)=> (((conj ((in Xy) B)) B0) x3)) ((Xphi x6) Xy)) x4)) ((eq_ref fofType) ((kpair Xx) Xy))))) as proof of ((and ((in x6) A)) ((ex fofType) (fun (Xy0:fofType)=> ((and ((and ((in Xy0) B)) ((Xphi x6) Xy0))) (((eq fofType) ((kpair Xx) Xy)) ((kpair x6) Xy0)))))) % Found ((((conj ((in x6) A)) ((ex fofType) (fun (Xy0:fofType)=> ((and ((and ((in Xy0) B)) ((Xphi x6) Xy0))) (((eq fofType) ((kpair Xx) Xy)) ((kpair x6) Xy0)))))) x2) (((ex_intro0 (fun (Xy0:fofType)=> ((and ((and ((in Xy0) B)) ((Xphi x6) Xy0))) (((eq fofType) ((kpair Xx) Xy)) ((kpair x6) Xy0))))) Xy) ((((conj ((and ((in Xy) B)) ((Xphi x6) Xy))) (((eq fofType) ((kpair Xx) Xy)) ((kpair x6) Xy))) (((fun (B0:Prop)=> (((conj ((in Xy) B)) B0) x3)) ((Xphi x6) Xy)) x4)) ((eq_ref fofType) ((kpair Xx) Xy))))) as proof of ((and ((in x6) A)) ((ex fofType) (fun (Xy0:fofType)=> ((and ((and ((in Xy0) B)) ((Xphi x6) Xy0))) (((eq fofType) ((kpair Xx) Xy)) ((kpair x6) Xy0)))))) % Found (ex_intro000 ((((conj ((in x6) A)) ((ex fofType) (fun (Xy0:fofType)=> ((and ((and ((in Xy0) B)) ((Xphi x6) Xy0))) (((eq fofType) ((kpair Xx) Xy)) ((kpair x6) Xy0)))))) x2) (((ex_intro0 (fun (Xy0:fofType)=> ((and ((and ((in Xy0) B)) ((Xphi x6) Xy0))) (((eq fofType) ((kpair Xx) Xy)) ((kpair x6) Xy0))))) Xy) ((((conj ((and ((in Xy) B)) ((Xphi x6) Xy))) (((eq fofType) ((kpair Xx) Xy)) ((kpair x6) Xy))) (((fun (B0:Prop)=> (((conj ((in Xy) B)) B0) x3)) ((Xphi x6) Xy)) x4)) ((eq_ref fofType) ((kpair Xx) Xy)))))) as proof of ((ex fofType) (fun (Xx1:fofType)=> ((and ((in Xx1) A)) ((ex fofType) (fun (Xy0:fofType)=> ((and ((and ((in Xy0) B)) ((Xphi Xx1) Xy0))) (((eq fofType) ((kpair Xx) Xy)) ((kpair Xx1) Xy0)))))))) % Found ((ex_intro00 Xx) ((((conj ((in Xx) A)) ((ex fofType) (fun (Xy0:fofType)=> ((and ((and ((in Xy0) B)) ((Xphi Xx) Xy0))) (((eq fofType) ((kpair Xx) Xy)) ((kpair Xx) Xy0)))))) x2) (((ex_intro0 (fun (Xy0:fofType)=> ((and ((and ((in Xy0) B)) ((Xphi Xx) Xy0))) (((eq fofType) ((kpair Xx) Xy)) ((kpair Xx) Xy0))))) Xy) ((((conj ((and ((in Xy) B)) ((Xphi Xx) Xy))) (((eq fofType) ((kpair Xx) Xy)) ((kpair Xx) Xy))) (((fun (B0:Prop)=> (((conj ((in Xy) B)) B0) x3)) ((Xphi Xx) Xy)) x4)) ((eq_ref fofType) ((kpair Xx) Xy)))))) as proof of ((ex fofType) (fun (Xx1:fofType)=> ((and ((in Xx1) A)) ((ex fofType) (fun (Xy0:fofType)=> ((and ((and ((in Xy0) B)) ((Xphi Xx1) Xy0))) (((eq fofType) ((kpair Xx) Xy)) ((kpair Xx1) Xy0)))))))) % Found (((ex_intro0 (fun (Xx1:fofType)=> ((and ((in Xx1) A)) ((ex fofType) (fun (Xy0:fofType)=> ((and ((and ((in Xy0) B)) ((Xphi Xx1) Xy0))) (((eq fofType) ((kpair Xx) Xy)) ((kpair Xx1) Xy0)))))))) Xx) ((((conj ((in Xx) A)) ((ex fofType) (fun (Xy0:fofType)=> ((and ((and ((in Xy0) B)) ((Xphi Xx) Xy0))) (((eq fofType) ((kpair Xx) Xy)) ((kpair Xx) Xy0)))))) x2) (((ex_intro0 (fun (Xy0:fofType)=> ((and ((and ((in Xy0) B)) ((Xphi Xx) Xy0))) (((eq fofType) ((kpair Xx) Xy)) ((kpair Xx) Xy0))))) Xy) ((((conj ((and ((in Xy) B)) ((Xphi Xx) Xy))) (((eq fofType) ((kpair Xx) Xy)) ((kpair Xx) Xy))) (((fun (B0:Prop)=> (((conj ((in Xy) B)) B0) x3)) ((Xphi Xx) Xy)) x4)) ((eq_ref fofType) ((kpair Xx) Xy)))))) as proof of ((ex fofType) (fun (Xx1:fofType)=> ((and ((in Xx1) A)) ((ex fofType) (fun (Xy0:fofType)=> ((and ((and ((in Xy0) B)) ((Xphi Xx1) Xy0))) (((eq fofType) ((kpair Xx) Xy)) ((kpair Xx1) Xy0)))))))) % Found ((((ex_intro fofType) (fun (Xx1:fofType)=> ((and ((in Xx1) A)) ((ex fofType) (fun (Xy0:fofType)=> ((and ((and ((in Xy0) B)) ((Xphi Xx1) Xy0))) (((eq fofType) ((kpair Xx) Xy)) ((kpair Xx1) Xy0)))))))) Xx) ((((conj ((in Xx) A)) ((ex fofType) (fun (Xy0:fofType)=> ((and ((and ((in Xy0) B)) ((Xphi Xx) Xy0))) (((eq fofType) ((kpair Xx) Xy)) ((kpair Xx) Xy0)))))) x2) ((((ex_intro fofType) (fun (Xy0:fofType)=> ((and ((and ((in Xy0) B)) ((Xphi Xx) Xy0))) (((eq fofType) ((kpair Xx) Xy)) ((kpair Xx) Xy0))))) Xy) ((((conj ((and ((in Xy) B)) ((Xphi Xx) Xy))) (((eq fofType) ((kpair Xx) Xy)) ((kpair Xx) Xy))) (((fun (B0:Prop)=> (((conj ((in Xy) B)) B0) x3)) ((Xphi Xx) Xy)) x4)) ((eq_ref fofType) ((kpair Xx) Xy)))))) as proof of ((ex fofType) (fun (Xx1:fofType)=> ((and ((in Xx1) A)) ((ex fofType) (fun (Xy0:fofType)=> ((and ((and ((in Xy0) B)) ((Xphi Xx1) Xy0))) (((eq fofType) ((kpair Xx) Xy)) ((kpair Xx1) Xy0)))))))) % Found ((((ex_intro fofType) (fun (Xx1:fofType)=> ((and ((in Xx1) A)) ((ex fofType) (fun (Xy0:fofType)=> ((and ((and ((in Xy0) B)) ((Xphi Xx1) Xy0))) (((eq fofType) ((kpair Xx) Xy)) ((kpair Xx1) Xy0)))))))) Xx) ((((conj ((in Xx) A)) ((ex fofType) (fun (Xy0:fofType)=> ((and ((and ((in Xy0) B)) ((Xphi Xx) Xy0))) (((eq fofType) ((kpair Xx) Xy)) ((kpair Xx) Xy0)))))) x2) ((((ex_intro fofType) (fun (Xy0:fofType)=> ((and ((and ((in Xy0) B)) ((Xphi Xx) Xy0))) (((eq fofType) ((kpair Xx) Xy)) ((kpair Xx) Xy0))))) Xy) ((((conj ((and ((in Xy) B)) ((Xphi Xx) Xy))) (((eq fofType) ((kpair Xx) Xy)) ((kpair Xx) Xy))) (((fun (B0:Prop)=> (((conj ((in Xy) B)) B0) x3)) ((Xphi Xx) Xy)) x4)) ((eq_ref fofType) ((kpair Xx) Xy)))))) as proof of ((ex fofType) (fun (Xx1:fofType)=> ((and ((in Xx1) A)) ((ex fofType) (fun (Xy0:fofType)=> ((and ((and ((in Xy0) B)) ((Xphi Xx1) Xy0))) (((eq fofType) ((kpair Xx) Xy)) ((kpair Xx1) Xy0)))))))) % Found ((x500 ((((((x1 A) B) Xx) x2) Xy) x3)) ((((ex_intro fofType) (fun (Xx1:fofType)=> ((and ((in Xx1) A)) ((ex fofType) (fun (Xy0:fofType)=> ((and ((and ((in Xy0) B)) ((Xphi Xx1) Xy0))) (((eq fofType) ((kpair Xx) Xy)) ((kpair Xx1) Xy0)))))))) Xx) ((((conj ((in Xx) A)) ((ex fofType) (fun (Xy0:fofType)=> ((and ((and ((in Xy0) B)) ((Xphi Xx) Xy0))) (((eq fofType) ((kpair Xx) Xy)) ((kpair Xx) Xy0)))))) x2) ((((ex_intro fofType) (fun (Xy0:fofType)=> ((and ((and ((in Xy0) B)) ((Xphi Xx) Xy0))) (((eq fofType) ((kpair Xx) Xy)) ((kpair Xx) Xy0))))) Xy) ((((conj ((and ((in Xy) B)) ((Xphi Xx) Xy))) (((eq fofType) ((kpair Xx) Xy)) ((kpair Xx) Xy))) (((fun (B0:Prop)=> (((conj ((in Xy) B)) B0) x3)) ((Xphi Xx) Xy)) x4)) ((eq_ref fofType) ((kpair Xx) Xy))))))) as proof of ((in ((kpair Xx) Xy)) (((dpsetconstr A) B) (fun (Xz:fofType) (Xu:fofType)=> ((Xphi Xz) Xu)))) % Found (((x50 ((kpair Xx) Xy)) ((((((x1 A) B) Xx) x2) Xy) x3)) ((((ex_intro fofType) (fun (Xx1:fofType)=> ((and ((in Xx1) A)) ((ex fofType) (fun (Xy0:fofType)=> ((and ((and ((in Xy0) B)) ((Xphi Xx1) Xy0))) (((eq fofType) ((kpair Xx) Xy)) ((kpair Xx1) Xy0)))))))) Xx) ((((conj ((in Xx) A)) ((ex fofType) (fun (Xy0:fofType)=> ((and ((and ((in Xy0) B)) ((Xphi Xx) Xy0))) (((eq fofType) ((kpair Xx) Xy)) ((kpair Xx) Xy0)))))) x2) ((((ex_intro fofType) (fun (Xy0:fofType)=> ((and ((and ((in Xy0) B)) ((Xphi Xx) Xy0))) (((eq fofType) ((kpair Xx) Xy)) ((kpair Xx) Xy0))))) Xy) ((((conj ((and ((in Xy) B)) ((Xphi Xx) Xy))) (((eq fofType) ((kpair Xx) Xy)) ((kpair Xx) Xy))) (((fun (B0:Prop)=> (((conj ((in Xy) B)) B0) x3)) ((Xphi Xx) Xy)) x4)) ((eq_ref fofType) ((kpair Xx) Xy))))))) as proof of ((in ((kpair Xx) Xy)) (((dpsetconstr A) B) (fun (Xz:fofType) (Xu:fofType)=> ((Xphi Xz) Xu)))) % Found ((((x5 (fun (x9:fofType)=> ((ex fofType) (fun (Xx1:fofType)=> ((and ((in Xx1) A)) ((ex fofType) (fun (Xy0:fofType)=> ((and ((and ((in Xy0) B)) ((Xphi Xx1) Xy0))) (((eq fofType) x9) ((kpair Xx1) Xy0)))))))))) ((kpair Xx) Xy)) ((((((x1 A) B) Xx) x2) Xy) x3)) ((((ex_intro fofType) (fun (Xx1:fofType)=> ((and ((in Xx1) A)) ((ex fofType) (fun (Xy0:fofType)=> ((and ((and ((in Xy0) B)) ((Xphi Xx1) Xy0))) (((eq fofType) ((kpair Xx) Xy)) ((kpair Xx1) Xy0)))))))) Xx) ((((conj ((in Xx) A)) ((ex fofType) (fun (Xy0:fofType)=> ((and ((and ((in Xy0) B)) ((Xphi Xx) Xy0))) (((eq fofType) ((kpair Xx) Xy)) ((kpair Xx) Xy0)))))) x2) ((((ex_intro fofType) (fun (Xy0:fofType)=> ((and ((and ((in Xy0) B)) ((Xphi Xx) Xy0))) (((eq fofType) ((kpair Xx) Xy)) ((kpair Xx) Xy0))))) Xy) ((((conj ((and ((in Xy) B)) ((Xphi Xx) Xy))) (((eq fofType) ((kpair Xx) Xy)) ((kpair Xx) Xy))) (((fun (B0:Prop)=> (((conj ((in Xy) B)) B0) x3)) ((Xphi Xx) Xy)) x4)) ((eq_ref fofType) ((kpair Xx) Xy))))))) as proof of ((in ((kpair Xx) Xy)) (((dpsetconstr A) B) (fun (Xz:fofType) (Xu:fofType)=> ((Xphi Xz) Xu)))) % Found (((((x ((cartprod A) B)) (fun (x9:fofType)=> ((ex fofType) (fun (Xx1:fofType)=> ((and ((in Xx1) A)) ((ex fofType) (fun (Xy0:fofType)=> ((and ((and ((in Xy0) B)) ((Xphi Xx1) Xy0))) (((eq fofType) x9) ((kpair Xx1) Xy0)))))))))) ((kpair Xx) Xy)) ((((((x1 A) B) Xx) x2) Xy) x3)) ((((ex_intro fofType) (fun (Xx1:fofType)=> ((and ((in Xx1) A)) ((ex fofType) (fun (Xy0:fofType)=> ((and ((and ((in Xy0) B)) ((Xphi Xx1) Xy0))) (((eq fofType) ((kpair Xx) Xy)) ((kpair Xx1) Xy0)))))))) Xx) ((((conj ((in Xx) A)) ((ex fofType) (fun (Xy0:fofType)=> ((and ((and ((in Xy0) B)) ((Xphi Xx) Xy0))) (((eq fofType) ((kpair Xx) Xy)) ((kpair Xx) Xy0)))))) x2) ((((ex_intro fofType) (fun (Xy0:fofType)=> ((and ((and ((in Xy0) B)) ((Xphi Xx) Xy0))) (((eq fofType) ((kpair Xx) Xy)) ((kpair Xx) Xy0))))) Xy) ((((conj ((and ((in Xy) B)) ((Xphi Xx) Xy))) (((eq fofType) ((kpair Xx) Xy)) ((kpair Xx) Xy))) (((fun (B0:Prop)=> (((conj ((in Xy) B)) B0) x3)) ((Xphi Xx) Xy)) x4)) ((eq_ref fofType) ((kpair Xx) Xy))))))) as proof of ((in ((kpair Xx) Xy)) (((dpsetconstr A) B) (fun (Xz:fofType) (Xu:fofType)=> ((Xphi Xz) Xu)))) % Found (fun (x4:((Xphi Xx) Xy))=> (((((x ((cartprod A) B)) (fun (x9:fofType)=> ((ex fofType) (fun (Xx1:fofType)=> ((and ((in Xx1) A)) ((ex fofType) (fun (Xy0:fofType)=> ((and ((and ((in Xy0) B)) ((Xphi Xx1) Xy0))) (((eq fofType) x9) ((kpair Xx1) Xy0)))))))))) ((kpair Xx) Xy)) ((((((x1 A) B) Xx) x2) Xy) x3)) ((((ex_intro fofType) (fun (Xx1:fofType)=> ((and ((in Xx1) A)) ((ex fofType) (fun (Xy0:fofType)=> ((and ((and ((in Xy0) B)) ((Xphi Xx1) Xy0))) (((eq fofType) ((kpair Xx) Xy)) ((kpair Xx1) Xy0)))))))) Xx) ((((conj ((in Xx) A)) ((ex fofType) (fun (Xy0:fofType)=> ((and ((and ((in Xy0) B)) ((Xphi Xx) Xy0))) (((eq fofType) ((kpair Xx) Xy)) ((kpair Xx) Xy0)))))) x2) ((((ex_intro fofType) (fun (Xy0:fofType)=> ((and ((and ((in Xy0) B)) ((Xphi Xx) Xy0))) (((eq fofType) ((kpair Xx) Xy)) ((kpair Xx) Xy0))))) Xy) ((((conj ((and ((in Xy) B)) ((Xphi Xx) Xy))) (((eq fofType) ((kpair Xx) Xy)) ((kpair Xx) Xy))) (((fun (B0:Prop)=> (((conj ((in Xy) B)) B0) x3)) ((Xphi Xx) Xy)) x4)) ((eq_ref fofType) ((kpair Xx) Xy)))))))) as proof of ((in ((kpair Xx) Xy)) (((dpsetconstr A) B) (fun (Xz:fofType) (Xu:fofType)=> ((Xphi Xz) Xu)))) % Found (fun (x3:((in Xy) B)) (x4:((Xphi Xx) Xy))=> (((((x ((cartprod A) B)) (fun (x9:fofType)=> ((ex fofType) (fun (Xx1:fofType)=> ((and ((in Xx1) A)) ((ex fofType) (fun (Xy0:fofType)=> ((and ((and ((in Xy0) B)) ((Xphi Xx1) Xy0))) (((eq fofType) x9) ((kpair Xx1) Xy0)))))))))) ((kpair Xx) Xy)) ((((((x1 A) B) Xx) x2) Xy) x3)) ((((ex_intro fofType) (fun (Xx1:fofType)=> ((and ((in Xx1) A)) ((ex fofType) (fun (Xy0:fofType)=> ((and ((and ((in Xy0) B)) ((Xphi Xx1) Xy0))) (((eq fofType) ((kpair Xx) Xy)) ((kpair Xx1) Xy0)))))))) Xx) ((((conj ((in Xx) A)) ((ex fofType) (fun (Xy0:fofType)=> ((and ((and ((in Xy0) B)) ((Xphi Xx) Xy0))) (((eq fofType) ((kpair Xx) Xy)) ((kpair Xx) Xy0)))))) x2) ((((ex_intro fofType) (fun (Xy0:fofType)=> ((and ((and ((in Xy0) B)) ((Xphi Xx) Xy0))) (((eq fofType) ((kpair Xx) Xy)) ((kpair Xx) Xy0))))) Xy) ((((conj ((and ((in Xy) B)) ((Xphi Xx) Xy))) (((eq fofType) ((kpair Xx) Xy)) ((kpair Xx) Xy))) (((fun (B0:Prop)=> (((conj ((in Xy) B)) B0) x3)) ((Xphi Xx) Xy)) x4)) ((eq_ref fofType) ((kpair Xx) Xy)))))))) as proof of (((Xphi Xx) Xy)->((in ((kpair Xx) Xy)) (((dpsetconstr A) B) (fun (Xz:fofType) (Xu:fofType)=> ((Xphi Xz) Xu))))) % Found (fun (Xy:fofType) (x3:((in Xy) B)) (x4:((Xphi Xx) Xy))=> (((((x ((cartprod A) B)) (fun (x9:fofType)=> ((ex fofType) (fun (Xx1:fofType)=> ((and ((in Xx1) A)) ((ex fofType) (fun (Xy0:fofType)=> ((and ((and ((in Xy0) B)) ((Xphi Xx1) Xy0))) (((eq fofType) x9) ((kpair Xx1) Xy0)))))))))) ((kpair Xx) Xy)) ((((((x1 A) B) Xx) x2) Xy) x3)) ((((ex_intro fofType) (fun (Xx1:fofType)=> ((and ((in Xx1) A)) ((ex fofType) (fun (Xy0:fofType)=> ((and ((and ((in Xy0) B)) ((Xphi Xx1) Xy0))) (((eq fofType) ((kpair Xx) Xy)) ((kpair Xx1) Xy0)))))))) Xx) ((((conj ((in Xx) A)) ((ex fofType) (fun (Xy0:fofType)=> ((and ((and ((in Xy0) B)) ((Xphi Xx) Xy0))) (((eq fofType) ((kpair Xx) Xy)) ((kpair Xx) Xy0)))))) x2) ((((ex_intro fofType) (fun (Xy0:fofType)=> ((and ((and ((in Xy0) B)) ((Xphi Xx) Xy0))) (((eq fofType) ((kpair Xx) Xy)) ((kpair Xx) Xy0))))) Xy) ((((conj ((and ((in Xy) B)) ((Xphi Xx) Xy))) (((eq fofType) ((kpair Xx) Xy)) ((kpair Xx) Xy))) (((fun (B0:Prop)=> (((conj ((in Xy) B)) B0) x3)) ((Xphi Xx) Xy)) x4)) ((eq_ref fofType) ((kpair Xx) Xy)))))))) as proof of (((in Xy) B)->(((Xphi Xx) Xy)->((in ((kpair Xx) Xy)) (((dpsetconstr A) B) (fun (Xz:fofType) (Xu:fofType)=> ((Xphi Xz) Xu)))))) % Found (fun (x2:((in Xx) A)) (Xy:fofType) (x3:((in Xy) B)) (x4:((Xphi Xx) Xy))=> (((((x ((cartprod A) B)) (fun (x9:fofType)=> ((ex fofType) (fun (Xx1:fofType)=> ((and ((in Xx1) A)) ((ex fofType) (fun (Xy0:fofType)=> ((and ((and ((in Xy0) B)) ((Xphi Xx1) Xy0))) (((eq fofType) x9) ((kpair Xx1) Xy0)))))))))) ((kpair Xx) Xy)) ((((((x1 A) B) Xx) x2) Xy) x3)) ((((ex_intro fofType) (fun (Xx1:fofType)=> ((and ((in Xx1) A)) ((ex fofType) (fun (Xy0:fofType)=> ((and ((and ((in Xy0) B)) ((Xphi Xx1) Xy0))) (((eq fofType) ((kpair Xx) Xy)) ((kpair Xx1) Xy0)))))))) Xx) ((((conj ((in Xx) A)) ((ex fofType) (fun (Xy0:fofType)=> ((and ((and ((in Xy0) B)) ((Xphi Xx) Xy0))) (((eq fofType) ((kpair Xx) Xy)) ((kpair Xx) Xy0)))))) x2) ((((ex_intro fofType) (fun (Xy0:fofType)=> ((and ((and ((in Xy0) B)) ((Xphi Xx) Xy0))) (((eq fofType) ((kpair Xx) Xy)) ((kpair Xx) Xy0))))) Xy) ((((conj ((and ((in Xy) B)) ((Xphi Xx) Xy))) (((eq fofType) ((kpair Xx) Xy)) ((kpair Xx) Xy))) (((fun (B0:Prop)=> (((conj ((in Xy) B)) B0) x3)) ((Xphi Xx) Xy)) x4)) ((eq_ref fofType) ((kpair Xx) Xy)))))))) as proof of (forall (Xy:fofType), (((in Xy) B)->(((Xphi Xx) Xy)->((in ((kpair Xx) Xy)) (((dpsetconstr A) B) (fun (Xz:fofType) (Xu:fofType)=> ((Xphi Xz) Xu))))))) % Found (fun (Xx:fofType) (x2:((in Xx) A)) (Xy:fofType) (x3:((in Xy) B)) (x4:((Xphi Xx) Xy))=> (((((x ((cartprod A) B)) (fun (x9:fofType)=> ((ex fofType) (fun (Xx1:fofType)=> ((and ((in Xx1) A)) ((ex fofType) (fun (Xy0:fofType)=> ((and ((and ((in Xy0) B)) ((Xphi Xx1) Xy0))) (((eq fofType) x9) ((kpair Xx1) Xy0)))))))))) ((kpair Xx) Xy)) ((((((x1 A) B) Xx) x2) Xy) x3)) ((((ex_intro fofType) (fun (Xx1:fofType)=> ((and ((in Xx1) A)) ((ex fofType) (fun (Xy0:fofType)=> ((and ((and ((in Xy0) B)) ((Xphi Xx1) Xy0))) (((eq fofType) ((kpair Xx) Xy)) ((kpair Xx1) Xy0)))))))) Xx) ((((conj ((in Xx) A)) ((ex fofType) (fun (Xy0:fofType)=> ((and ((and ((in Xy0) B)) ((Xphi Xx) Xy0))) (((eq fofType) ((kpair Xx) Xy)) ((kpair Xx) Xy0)))))) x2) ((((ex_intro fofType) (fun (Xy0:fofType)=> ((and ((and ((in Xy0) B)) ((Xphi Xx) Xy0))) (((eq fofType) ((kpair Xx) Xy)) ((kpair Xx) Xy0))))) Xy) ((((conj ((and ((in Xy) B)) ((Xphi Xx) Xy))) (((eq fofType) ((kpair Xx) Xy)) ((kpair Xx) Xy))) (((fun (B0:Prop)=> (((conj ((in Xy) B)) B0) x3)) ((Xphi Xx) Xy)) x4)) ((eq_ref fofType) ((kpair Xx) Xy)))))))) as proof of (((in Xx) A)->(forall (Xy:fofType), (((in Xy) B)->(((Xphi Xx) Xy)->((in ((kpair Xx) Xy)) (((dpsetconstr A) B) (fun (Xz:fofType) (Xu:fofType)=> ((Xphi Xz) Xu)))))))) % Found (fun (Xphi:(fofType->(fofType->Prop))) (Xx:fofType) (x2:((in Xx) A)) (Xy:fofType) (x3:((in Xy) B)) (x4:((Xphi Xx) Xy))=> (((((x ((cartprod A) B)) (fun (x9:fofType)=> ((ex fofType) (fun (Xx1:fofType)=> ((and ((in Xx1) A)) ((ex fofType) (fun (Xy0:fofType)=> ((and ((and ((in Xy0) B)) ((Xphi Xx1) Xy0))) (((eq fofType) x9) ((kpair Xx1) Xy0)))))))))) ((kpair Xx) Xy)) ((((((x1 A) B) Xx) x2) Xy) x3)) ((((ex_intro fofType) (fun (Xx1:fofType)=> ((and ((in Xx1) A)) ((ex fofType) (fun (Xy0:fofType)=> ((and ((and ((in Xy0) B)) ((Xphi Xx1) Xy0))) (((eq fofType) ((kpair Xx) Xy)) ((kpair Xx1) Xy0)))))))) Xx) ((((conj ((in Xx) A)) ((ex fofType) (fun (Xy0:fofType)=> ((and ((and ((in Xy0) B)) ((Xphi Xx) Xy0))) (((eq fofType) ((kpair Xx) Xy)) ((kpair Xx) Xy0)))))) x2) ((((ex_intro fofType) (fun (Xy0:fofType)=> ((and ((and ((in Xy0) B)) ((Xphi Xx) Xy0))) (((eq fofType) ((kpair Xx) Xy)) ((kpair Xx) Xy0))))) Xy) ((((conj ((and ((in Xy) B)) ((Xphi Xx) Xy))) (((eq fofType) ((kpair Xx) Xy)) ((kpair Xx) Xy))) (((fun (B0:Prop)=> (((conj ((in Xy) B)) B0) x3)) ((Xphi Xx) Xy)) x4)) ((eq_ref fofType) ((kpair Xx) Xy)))))))) as proof of (forall (Xx:fofType), (((in Xx) A)->(forall (Xy:fofType), (((in Xy) B)->(((Xphi Xx) Xy)->((in ((kpair Xx) Xy)) (((dpsetconstr A) B) (fun (Xz:fofType) (Xu:fofType)=> ((Xphi Xz) Xu))))))))) % Found (fun (B:fofType) (Xphi:(fofType->(fofType->Prop))) (Xx:fofType) (x2:((in Xx) A)) (Xy:fofType) (x3:((in Xy) B)) (x4:((Xphi Xx) Xy))=> (((((x ((cartprod A) B)) (fun (x9:fofType)=> ((ex fofType) (fun (Xx1:fofType)=> ((and ((in Xx1) A)) ((ex fofType) (fun (Xy0:fofType)=> ((and ((and ((in Xy0) B)) ((Xphi Xx1) Xy0))) (((eq fofType) x9) ((kpair Xx1) Xy0)))))))))) ((kpair Xx) Xy)) ((((((x1 A) B) Xx) x2) Xy) x3)) ((((ex_intro fofType) (fun (Xx1:fofType)=> ((and ((in Xx1) A)) ((ex fofType) (fun (Xy0:fofType)=> ((and ((and ((in Xy0) B)) ((Xphi Xx1) Xy0))) (((eq fofType) ((kpair Xx) Xy)) ((kpair Xx1) Xy0)))))))) Xx) ((((conj ((in Xx) A)) ((ex fofType) (fun (Xy0:fofType)=> ((and ((and ((in Xy0) B)) ((Xphi Xx) Xy0))) (((eq fofType) ((kpair Xx) Xy)) ((kpair Xx) Xy0)))))) x2) ((((ex_intro fofType) (fun (Xy0:fofType)=> ((and ((and ((in Xy0) B)) ((Xphi Xx) Xy0))) (((eq fofType) ((kpair Xx) Xy)) ((kpair Xx) Xy0))))) Xy) ((((conj ((and ((in Xy) B)) ((Xphi Xx) Xy))) (((eq fofType) ((kpair Xx) Xy)) ((kpair Xx) Xy))) (((fun (B0:Prop)=> (((conj ((in Xy) B)) B0) x3)) ((Xphi Xx) Xy)) x4)) ((eq_ref fofType) ((kpair Xx) Xy)))))))) as proof of (forall (Xphi:(fofType->(fofType->Prop))) (Xx:fofType), (((in Xx) A)->(forall (Xy:fofType), (((in Xy) B)->(((Xphi Xx) Xy)->((in ((kpair Xx) Xy)) (((dpsetconstr A) B) (fun (Xz:fofType) (Xu:fofType)=> ((Xphi Xz) Xu))))))))) % Found (fun (A:fofType) (B:fofType) (Xphi:(fofType->(fofType->Prop))) (Xx:fofType) (x2:((in Xx) A)) (Xy:fofType) (x3:((in Xy) B)) (x4:((Xphi Xx) Xy))=> (((((x ((cartprod A) B)) (fun (x9:fofType)=> ((ex fofType) (fun (Xx1:fofType)=> ((and ((in Xx1) A)) ((ex fofType) (fun (Xy0:fofType)=> ((and ((and ((in Xy0) B)) ((Xphi Xx1) Xy0))) (((eq fofType) x9) ((kpair Xx1) Xy0)))))))))) ((kpair Xx) Xy)) ((((((x1 A) B) Xx) x2) Xy) x3)) ((((ex_intro fofType) (fun (Xx1:fofType)=> ((and ((in Xx1) A)) ((ex fofType) (fun (Xy0:fofType)=> ((and ((and ((in Xy0) B)) ((Xphi Xx1) Xy0))) (((eq fofType) ((kpair Xx) Xy)) ((kpair Xx1) Xy0)))))))) Xx) ((((conj ((in Xx) A)) ((ex fofType) (fun (Xy0:fofType)=> ((and ((and ((in Xy0) B)) ((Xphi Xx) Xy0))) (((eq fofType) ((kpair Xx) Xy)) ((kpair Xx) Xy0)))))) x2) ((((ex_intro fofType) (fun (Xy0:fofType)=> ((and ((and ((in Xy0) B)) ((Xphi Xx) Xy0))) (((eq fofType) ((kpair Xx) Xy)) ((kpair Xx) Xy0))))) Xy) ((((conj ((and ((in Xy) B)) ((Xphi Xx) Xy))) (((eq fofType) ((kpair Xx) Xy)) ((kpair Xx) Xy))) (((fun (B0:Prop)=> (((conj ((in Xy) B)) B0) x3)) ((Xphi Xx) Xy)) x4)) ((eq_ref fofType) ((kpair Xx) Xy)))))))) as proof of (forall (B:fofType) (Xphi:(fofType->(fofType->Prop))) (Xx:fofType), (((in Xx) A)->(forall (Xy:fofType), (((in Xy) B)->(((Xphi Xx) Xy)->((in ((kpair Xx) Xy)) (((dpsetconstr A) B) (fun (Xz:fofType) (Xu:fofType)=> ((Xphi Xz) Xu))))))))) % Found (fun (x1:cartprodpairin) (A:fofType) (B:fofType) (Xphi:(fofType->(fofType->Prop))) (Xx:fofType) (x2:((in Xx) A)) (Xy:fofType) (x3:((in Xy) B)) (x4:((Xphi Xx) Xy))=> (((((x ((cartprod A) B)) (fun (x9:fofType)=> ((ex fofType) (fun (Xx1:fofType)=> ((and ((in Xx1) A)) ((ex fofType) (fun (Xy0:fofType)=> ((and ((and ((in Xy0) B)) ((Xphi Xx1) Xy0))) (((eq fofType) x9) ((kpair Xx1) Xy0)))))))))) ((kpair Xx) Xy)) ((((((x1 A) B) Xx) x2) Xy) x3)) ((((ex_intro fofType) (fun (Xx1:fofType)=> ((and ((in Xx1) A)) ((ex fofType) (fun (Xy0:fofType)=> ((and ((and ((in Xy0) B)) ((Xphi Xx1) Xy0))) (((eq fofType) ((kpair Xx) Xy)) ((kpair Xx1) Xy0)))))))) Xx) ((((conj ((in Xx) A)) ((ex fofType) (fun (Xy0:fofType)=> ((and ((and ((in Xy0) B)) ((Xphi Xx) Xy0))) (((eq fofType) ((kpair Xx) Xy)) ((kpair Xx) Xy0)))))) x2) ((((ex_intro fofType) (fun (Xy0:fofType)=> ((and ((and ((in Xy0) B)) ((Xphi Xx) Xy0))) (((eq fofType) ((kpair Xx) Xy)) ((kpair Xx) Xy0))))) Xy) ((((conj ((and ((in Xy) B)) ((Xphi Xx) Xy))) (((eq fofType) ((kpair Xx) Xy)) ((kpair Xx) Xy))) (((fun (B0:Prop)=> (((conj ((in Xy) B)) B0) x3)) ((Xphi Xx) Xy)) x4)) ((eq_ref fofType) ((kpair Xx) Xy)))))))) as proof of (forall (A:fofType) (B:fofType) (Xphi:(fofType->(fofType->Prop))) (Xx:fofType), (((in Xx) A)->(forall (Xy:fofType), (((in Xy) B)->(((Xphi Xx) Xy)->((in ((kpair Xx) Xy)) (((dpsetconstr A) B) (fun (Xz:fofType) (Xu:fofType)=> ((Xphi Xz) Xu))))))))) % Found (fun (x0:setext) (x1:cartprodpairin) (A:fofType) (B:fofType) (Xphi:(fofType->(fofType->Prop))) (Xx:fofType) (x2:((in Xx) A)) (Xy:fofType) (x3:((in Xy) B)) (x4:((Xphi Xx) Xy))=> (((((x ((cartprod A) B)) (fun (x9:fofType)=> ((ex fofType) (fun (Xx1:fofType)=> ((and ((in Xx1) A)) ((ex fofType) (fun (Xy0:fofType)=> ((and ((and ((in Xy0) B)) ((Xphi Xx1) Xy0))) (((eq fofType) x9) ((kpair Xx1) Xy0)))))))))) ((kpair Xx) Xy)) ((((((x1 A) B) Xx) x2) Xy) x3)) ((((ex_intro fofType) (fun (Xx1:fofType)=> ((and ((in Xx1) A)) ((ex fofType) (fun (Xy0:fofType)=> ((and ((and ((in Xy0) B)) ((Xphi Xx1) Xy0))) (((eq fofType) ((kpair Xx) Xy)) ((kpair Xx1) Xy0)))))))) Xx) ((((conj ((in Xx) A)) ((ex fofType) (fun (Xy0:fofType)=> ((and ((and ((in Xy0) B)) ((Xphi Xx) Xy0))) (((eq fofType) ((kpair Xx) Xy)) ((kpair Xx) Xy0)))))) x2) ((((ex_intro fofType) (fun (Xy0:fofType)=> ((and ((and ((in Xy0) B)) ((Xphi Xx) Xy0))) (((eq fofType) ((kpair Xx) Xy)) ((kpair Xx) Xy0))))) Xy) ((((conj ((and ((in Xy) B)) ((Xphi Xx) Xy))) (((eq fofType) ((kpair Xx) Xy)) ((kpair Xx) Xy))) (((fun (B0:Prop)=> (((conj ((in Xy) B)) B0) x3)) ((Xphi Xx) Xy)) x4)) ((eq_ref fofType) ((kpair Xx) Xy)))))))) as proof of (cartprodpairin->(forall (A:fofType) (B:fofType) (Xphi:(fofType->(fofType->Prop))) (Xx:fofType), (((in Xx) A)->(forall (Xy:fofType), (((in Xy) B)->(((Xphi Xx) Xy)->((in ((kpair Xx) Xy)) (((dpsetconstr A) B) (fun (Xz:fofType) (Xu:fofType)=> ((Xphi Xz) Xu)))))))))) % Found (fun (x:dsetconstrI) (x0:setext) (x1:cartprodpairin) (A:fofType) (B:fofType) (Xphi:(fofType->(fofType->Prop))) (Xx:fofType) (x2:((in Xx) A)) (Xy:fofType) (x3:((in Xy) B)) (x4:((Xphi Xx) Xy))=> (((((x ((cartprod A) B)) (fun (x9:fofType)=> ((ex fofType) (fun (Xx1:fofType)=> ((and ((in Xx1) A)) ((ex fofType) (fun (Xy0:fofType)=> ((and ((and ((in Xy0) B)) ((Xphi Xx1) Xy0))) (((eq fofType) x9) ((kpair Xx1) Xy0)))))))))) ((kpair Xx) Xy)) ((((((x1 A) B) Xx) x2) Xy) x3)) ((((ex_intro fofType) (fun (Xx1:fofType)=> ((and ((in Xx1) A)) ((ex fofType) (fun (Xy0:fofType)=> ((and ((and ((in Xy0) B)) ((Xphi Xx1) Xy0))) (((eq fofType) ((kpair Xx) Xy)) ((kpair Xx1) Xy0)))))))) Xx) ((((conj ((in Xx) A)) ((ex fofType) (fun (Xy0:fofType)=> ((and ((and ((in Xy0) B)) ((Xphi Xx) Xy0))) (((eq fofType) ((kpair Xx) Xy)) ((kpair Xx) Xy0)))))) x2) ((((ex_intro fofType) (fun (Xy0:fofType)=> ((and ((and ((in Xy0) B)) ((Xphi Xx) Xy0))) (((eq fofType) ((kpair Xx) Xy)) ((kpair Xx) Xy0))))) Xy) ((((conj ((and ((in Xy) B)) ((Xphi Xx) Xy))) (((eq fofType) ((kpair Xx) Xy)) ((kpair Xx) Xy))) (((fun (B0:Prop)=> (((conj ((in Xy) B)) B0) x3)) ((Xphi Xx) Xy)) x4)) ((eq_ref fofType) ((kpair Xx) Xy)))))))) as proof of (setext->(cartprodpairin->(forall (A:fofType) (B:fofType) (Xphi:(fofType->(fofType->Prop))) (Xx:fofType), (((in Xx) A)->(forall (Xy:fofType), (((in Xy) B)->(((Xphi Xx) Xy)->((in ((kpair Xx) Xy)) (((dpsetconstr A) B) (fun (Xz:fofType) (Xu:fofType)=> ((Xphi Xz) Xu))))))))))) % Found (fun (x:dsetconstrI) (x0:setext) (x1:cartprodpairin) (A:fofType) (B:fofType) (Xphi:(fofType->(fofType->Prop))) (Xx:fofType) (x2:((in Xx) A)) (Xy:fofType) (x3:((in Xy) B)) (x4:((Xphi Xx) Xy))=> (((((x ((cartprod A) B)) (fun (x9:fofType)=> ((ex fofType) (fun (Xx1:fofType)=> ((and ((in Xx1) A)) ((ex fofType) (fun (Xy0:fofType)=> ((and ((and ((in Xy0) B)) ((Xphi Xx1) Xy0))) (((eq fofType) x9) ((kpair Xx1) Xy0)))))))))) ((kpair Xx) Xy)) ((((((x1 A) B) Xx) x2) Xy) x3)) ((((ex_intro fofType) (fun (Xx1:fofType)=> ((and ((in Xx1) A)) ((ex fofType) (fun (Xy0:fofType)=> ((and ((and ((in Xy0) B)) ((Xphi Xx1) Xy0))) (((eq fofType) ((kpair Xx) Xy)) ((kpair Xx1) Xy0)))))))) Xx) ((((conj ((in Xx) A)) ((ex fofType) (fun (Xy0:fofType)=> ((and ((and ((in Xy0) B)) ((Xphi Xx) Xy0))) (((eq fofType) ((kpair Xx) Xy)) ((kpair Xx) Xy0)))))) x2) ((((ex_intro fofType) (fun (Xy0:fofType)=> ((and ((and ((in Xy0) B)) ((Xphi Xx) Xy0))) (((eq fofType) ((kpair Xx) Xy)) ((kpair Xx) Xy0))))) Xy) ((((conj ((and ((in Xy) B)) ((Xphi Xx) Xy))) (((eq fofType) ((kpair Xx) Xy)) ((kpair Xx) Xy))) (((fun (B0:Prop)=> (((conj ((in Xy) B)) B0) x3)) ((Xphi Xx) Xy)) x4)) ((eq_ref fofType) ((kpair Xx) Xy)))))))) as proof of (dsetconstrI->(setext->(cartprodpairin->(forall (A:fofType) (B:fofType) (Xphi:(fofType->(fofType->Prop))) (Xx:fofType), (((in Xx) A)->(forall (Xy:fofType), (((in Xy) B)->(((Xphi Xx) Xy)->((in ((kpair Xx) Xy)) (((dpsetconstr A) B) (fun (Xz:fofType) (Xu:fofType)=> ((Xphi Xz) Xu)))))))))))) % Got proof (fun (x:dsetconstrI) (x0:setext) (x1:cartprodpairin) (A:fofType) (B:fofType) (Xphi:(fofType->(fofType->Prop))) (Xx:fofType) (x2:((in Xx) A)) (Xy:fofType) (x3:((in Xy) B)) (x4:((Xphi Xx) Xy))=> (((((x ((cartprod A) B)) (fun (x9:fofType)=> ((ex fofType) (fun (Xx1:fofType)=> ((and ((in Xx1) A)) ((ex fofType) (fun (Xy0:fofType)=> ((and ((and ((in Xy0) B)) ((Xphi Xx1) Xy0))) (((eq fofType) x9) ((kpair Xx1) Xy0)))))))))) ((kpair Xx) Xy)) ((((((x1 A) B) Xx) x2) Xy) x3)) ((((ex_intro fofType) (fun (Xx1:fofType)=> ((and ((in Xx1) A)) ((ex fofType) (fun (Xy0:fofType)=> ((and ((and ((in Xy0) B)) ((Xphi Xx1) Xy0))) (((eq fofType) ((kpair Xx) Xy)) ((kpair Xx1) Xy0)))))))) Xx) ((((conj ((in Xx) A)) ((ex fofType) (fun (Xy0:fofType)=> ((and ((and ((in Xy0) B)) ((Xphi Xx) Xy0))) (((eq fofType) ((kpair Xx) Xy)) ((kpair Xx) Xy0)))))) x2) ((((ex_intro fofType) (fun (Xy0:fofType)=> ((and ((and ((in Xy0) B)) ((Xphi Xx) Xy0))) (((eq fofType) ((kpair Xx) Xy)) ((kpair Xx) Xy0))))) Xy) ((((conj ((and ((in Xy) B)) ((Xphi Xx) Xy))) (((eq fofType) ((kpair Xx) Xy)) ((kpair Xx) Xy))) (((fun (B0:Prop)=> (((conj ((in Xy) B)) B0) x3)) ((Xphi Xx) Xy)) x4)) ((eq_ref fofType) ((kpair Xx) Xy)))))))) % Time elapsed = 3.210251s % node=456 cost=1963.000000 depth=37 % :::::::::::::::::::::: % % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p % (fun (x:dsetconstrI) (x0:setext) (x1:cartprodpairin) (A:fofType) (B:fofType) (Xphi:(fofType->(fofType->Prop))) (Xx:fofType) (x2:((in Xx) A)) (Xy:fofType) (x3:((in Xy) B)) (x4:((Xphi Xx) Xy))=> (((((x ((cartprod A) B)) (fun (x9:fofType)=> ((ex fofType) (fun (Xx1:fofType)=> ((and ((in Xx1) A)) ((ex fofType) (fun (Xy0:fofType)=> ((and ((and ((in Xy0) B)) ((Xphi Xx1) Xy0))) (((eq fofType) x9) ((kpair Xx1) Xy0)))))))))) ((kpair Xx) Xy)) ((((((x1 A) B) Xx) x2) Xy) x3)) ((((ex_intro fofType) (fun (Xx1:fofType)=> ((and ((in Xx1) A)) ((ex fofType) (fun (Xy0:fofType)=> ((and ((and ((in Xy0) B)) ((Xphi Xx1) Xy0))) (((eq fofType) ((kpair Xx) Xy)) ((kpair Xx1) Xy0)))))))) Xx) ((((conj ((in Xx) A)) ((ex fofType) (fun (Xy0:fofType)=> ((and ((and ((in Xy0) B)) ((Xphi Xx) Xy0))) (((eq fofType) ((kpair Xx) Xy)) ((kpair Xx) Xy0)))))) x2) ((((ex_intro fofType) (fun (Xy0:fofType)=> ((and ((and ((in Xy0) B)) ((Xphi Xx) Xy0))) (((eq fofType) ((kpair Xx) Xy)) ((kpair Xx) Xy0))))) Xy) ((((conj ((and ((in Xy) B)) ((Xphi Xx) Xy))) (((eq fofType) ((kpair Xx) Xy)) ((kpair Xx) Xy))) (((fun (B0:Prop)=> (((conj ((in Xy) B)) B0) x3)) ((Xphi Xx) Xy)) x4)) ((eq_ref fofType) ((kpair Xx) Xy)))))))) % % SZS output end Proof for /export/starexec/sandbox/benchmark/theBenchmark.p % EOF %------------------------------------------------------------------------------