:: SCHEME1 semantic presentation begin theorem :: SCHEME1:1 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "ex" (Set (Var "m")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set (Var "n")) ($#r1_hidden :::"="::: ) (Set (Num 2) ($#k4_nat_1 :::"*"::: ) (Set (Var "m")))) "or" (Bool (Set (Var "n")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Num 2) ($#k4_nat_1 :::"*"::: ) (Set (Var "m")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1))) ")" ))) ; theorem :: SCHEME1:2 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "ex" (Set (Var "m")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set (Var "n")) ($#r1_hidden :::"="::: ) (Set (Num 3) ($#k4_nat_1 :::"*"::: ) (Set (Var "m")))) "or" (Bool (Set (Var "n")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Num 3) ($#k4_nat_1 :::"*"::: ) (Set (Var "m")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1))) "or" (Bool (Set (Var "n")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Num 3) ($#k4_nat_1 :::"*"::: ) (Set (Var "m")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 2))) ")" ))) ; theorem :: SCHEME1:3 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "ex" (Set (Var "m")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set (Var "n")) ($#r1_hidden :::"="::: ) (Set (Num 4) ($#k4_nat_1 :::"*"::: ) (Set (Var "m")))) "or" (Bool (Set (Var "n")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Num 4) ($#k4_nat_1 :::"*"::: ) (Set (Var "m")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1))) "or" (Bool (Set (Var "n")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Num 4) ($#k4_nat_1 :::"*"::: ) (Set (Var "m")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 2))) "or" (Bool (Set (Var "n")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Num 4) ($#k4_nat_1 :::"*"::: ) (Set (Var "m")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 3))) ")" ))) ; theorem :: SCHEME1:4 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "ex" (Set (Var "m")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set (Var "n")) ($#r1_hidden :::"="::: ) (Set (Num 5) ($#k4_nat_1 :::"*"::: ) (Set (Var "m")))) "or" (Bool (Set (Var "n")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Num 5) ($#k4_nat_1 :::"*"::: ) (Set (Var "m")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1))) "or" (Bool (Set (Var "n")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Num 5) ($#k4_nat_1 :::"*"::: ) (Set (Var "m")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 2))) "or" (Bool (Set (Var "n")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Num 5) ($#k4_nat_1 :::"*"::: ) (Set (Var "m")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 3))) "or" (Bool (Set (Var "n")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Num 5) ($#k4_nat_1 :::"*"::: ) (Set (Var "m")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 4))) ")" ))) ; scheme :: SCHEME1:sch 1 ExRealSubseq{ F1() -> ($#m1_subset_1 :::"Real_Sequence":::), P1[ ($#m1_hidden :::"set"::: ) ] } : (Bool "ex" (Set (Var "q")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "st" (Bool "(" (Bool (Set (Var "q")) "is" ($#m2_valued_0 :::"subsequence"::: ) "of" (Set F1 "(" ")" )) & (Bool "(" "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool P1[(Set (Set (Var "q")) ($#k1_seq_1 :::"."::: ) (Set (Var "n")))]) ")" ) & (Bool "(" "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool "(" "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "r")) ($#r1_hidden :::"="::: ) (Set (Set F1 "(" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "n"))))) "holds" (Bool P1[(Set (Var "r"))]) ")" )) "holds" (Bool "ex" (Set (Var "m")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Set (Set F1 "(" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "q")) ($#k1_seq_1 :::"."::: ) (Set (Var "m"))))) ")" ) ")" )) provided (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "ex" (Set (Var "m")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "m"))) & (Bool P1[(Set (Set F1 "(" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "m")))]) ")" ))) proof end; scheme :: SCHEME1:sch 2 ExRealSeq2{ F1( ($#m1_hidden :::"set"::: ) ) -> ($#m1_subset_1 :::"Real":::), F2( ($#m1_hidden :::"set"::: ) ) -> ($#m1_subset_1 :::"Real":::) } : (Bool "ex" (Set (Var "s")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "st" (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set (Set (Var "s")) ($#k1_seq_1 :::"."::: ) (Set "(" (Num 2) ($#k4_nat_1 :::"*"::: ) (Set (Var "n")) ")" )) ($#r1_hidden :::"="::: ) (Set F1 "(" (Set (Var "n")) ")" )) & (Bool (Set (Set (Var "s")) ($#k1_seq_1 :::"."::: ) (Set "(" (Set "(" (Num 2) ($#k4_nat_1 :::"*"::: ) (Set (Var "n")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set F2 "(" (Set (Var "n")) ")" )) ")" ))) proof end; scheme :: SCHEME1:sch 3 ExRealSeq3{ F1( ($#m1_hidden :::"set"::: ) ) -> ($#m1_subset_1 :::"Real":::), F2( ($#m1_hidden :::"set"::: ) ) -> ($#m1_subset_1 :::"Real":::), F3( ($#m1_hidden :::"set"::: ) ) -> ($#m1_subset_1 :::"Real":::) } : (Bool "ex" (Set (Var "s")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "st" (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set (Set (Var "s")) ($#k1_seq_1 :::"."::: ) (Set "(" (Num 3) ($#k4_nat_1 :::"*"::: ) (Set (Var "n")) ")" )) ($#r1_hidden :::"="::: ) (Set F1 "(" (Set (Var "n")) ")" )) & (Bool (Set (Set (Var "s")) ($#k1_seq_1 :::"."::: ) (Set "(" (Set "(" (Num 3) ($#k4_nat_1 :::"*"::: ) (Set (Var "n")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set F2 "(" (Set (Var "n")) ")" )) & (Bool (Set (Set (Var "s")) ($#k1_seq_1 :::"."::: ) (Set "(" (Set "(" (Num 3) ($#k4_nat_1 :::"*"::: ) (Set (Var "n")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 2) ")" )) ($#r1_hidden :::"="::: ) (Set F3 "(" (Set (Var "n")) ")" )) ")" ))) proof end; scheme :: SCHEME1:sch 4 ExRealSeq4{ F1( ($#m1_hidden :::"set"::: ) ) -> ($#m1_subset_1 :::"Real":::), F2( ($#m1_hidden :::"set"::: ) ) -> ($#m1_subset_1 :::"Real":::), F3( ($#m1_hidden :::"set"::: ) ) -> ($#m1_subset_1 :::"Real":::), F4( ($#m1_hidden :::"set"::: ) ) -> ($#m1_subset_1 :::"Real":::) } : (Bool "ex" (Set (Var "s")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "st" (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set (Set (Var "s")) ($#k1_seq_1 :::"."::: ) (Set "(" (Num 4) ($#k4_nat_1 :::"*"::: ) (Set (Var "n")) ")" )) ($#r1_hidden :::"="::: ) (Set F1 "(" (Set (Var "n")) ")" )) & (Bool (Set (Set (Var "s")) ($#k1_seq_1 :::"."::: ) (Set "(" (Set "(" (Num 4) ($#k4_nat_1 :::"*"::: ) (Set (Var "n")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set F2 "(" (Set (Var "n")) ")" )) & (Bool (Set (Set (Var "s")) ($#k1_seq_1 :::"."::: ) (Set "(" (Set "(" (Num 4) ($#k4_nat_1 :::"*"::: ) (Set (Var "n")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 2) ")" )) ($#r1_hidden :::"="::: ) (Set F3 "(" (Set (Var "n")) ")" )) & (Bool (Set (Set (Var "s")) ($#k1_seq_1 :::"."::: ) (Set "(" (Set "(" (Num 4) ($#k4_nat_1 :::"*"::: ) (Set (Var "n")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 3) ")" )) ($#r1_hidden :::"="::: ) (Set F4 "(" (Set (Var "n")) ")" )) ")" ))) proof end; scheme :: SCHEME1:sch 5 ExRealSeq5{ F1( ($#m1_hidden :::"set"::: ) ) -> ($#m1_subset_1 :::"Real":::), F2( ($#m1_hidden :::"set"::: ) ) -> ($#m1_subset_1 :::"Real":::), F3( ($#m1_hidden :::"set"::: ) ) -> ($#m1_subset_1 :::"Real":::), F4( ($#m1_hidden :::"set"::: ) ) -> ($#m1_subset_1 :::"Real":::), F5( ($#m1_hidden :::"set"::: ) ) -> ($#m1_subset_1 :::"Real":::) } : (Bool "ex" (Set (Var "s")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "st" (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set (Set (Var "s")) ($#k1_seq_1 :::"."::: ) (Set "(" (Num 5) ($#k4_nat_1 :::"*"::: ) (Set (Var "n")) ")" )) ($#r1_hidden :::"="::: ) (Set F1 "(" (Set (Var "n")) ")" )) & (Bool (Set (Set (Var "s")) ($#k1_seq_1 :::"."::: ) (Set "(" (Set "(" (Num 5) ($#k4_nat_1 :::"*"::: ) (Set (Var "n")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set F2 "(" (Set (Var "n")) ")" )) & (Bool (Set (Set (Var "s")) ($#k1_seq_1 :::"."::: ) (Set "(" (Set "(" (Num 5) ($#k4_nat_1 :::"*"::: ) (Set (Var "n")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 2) ")" )) ($#r1_hidden :::"="::: ) (Set F3 "(" (Set (Var "n")) ")" )) & (Bool (Set (Set (Var "s")) ($#k1_seq_1 :::"."::: ) (Set "(" (Set "(" (Num 5) ($#k4_nat_1 :::"*"::: ) (Set (Var "n")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 3) ")" )) ($#r1_hidden :::"="::: ) (Set F4 "(" (Set (Var "n")) ")" )) & (Bool (Set (Set (Var "s")) ($#k1_seq_1 :::"."::: ) (Set "(" (Set "(" (Num 5) ($#k4_nat_1 :::"*"::: ) (Set (Var "n")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 4) ")" )) ($#r1_hidden :::"="::: ) (Set F5 "(" (Set (Var "n")) ")" )) ")" ))) proof end; scheme :: SCHEME1:sch 6 PartFuncExD2{ F1() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , F2() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , P1[ ($#m1_hidden :::"set"::: ) ], P2[ ($#m1_hidden :::"set"::: ) ], F3( ($#m1_hidden :::"set"::: ) ) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ), F4( ($#m1_hidden :::"set"::: ) ) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ) } : (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set F1 "(" ")" ) "," (Set F2 "(" ")" ) "st" (Bool "(" (Bool "(" "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) "holds" (Bool "(" (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) "iff" (Bool "(" (Bool P1[(Set (Var "c"))]) "or" (Bool P2[(Set (Var "c"))]) ")" ) ")" ) ")" ) & (Bool "(" "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) "st" (Bool (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool "(" "(" (Bool (Bool P1[(Set (Var "c"))])) "implies" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set F3 "(" (Set (Var "c")) ")" )) ")" & "(" (Bool (Bool P2[(Set (Var "c"))])) "implies" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set F4 "(" (Set (Var "c")) ")" )) ")" ")" ) ")" ) ")" )) provided (Bool "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) "st" (Bool (Bool P1[(Set (Var "c"))])) "holds" (Bool "not" (Bool P2[(Set (Var "c"))]))) proof end; scheme :: SCHEME1:sch 7 PartFuncExD29{ F1() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , F2() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , P1[ ($#m1_hidden :::"set"::: ) ], P2[ ($#m1_hidden :::"set"::: ) ], F3( ($#m1_hidden :::"set"::: ) ) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ), F4( ($#m1_hidden :::"set"::: ) ) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ) } : (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set F1 "(" ")" ) "," (Set F2 "(" ")" ) "st" (Bool "(" (Bool "(" "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) "holds" (Bool "(" (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) "iff" (Bool "(" (Bool P1[(Set (Var "c"))]) "or" (Bool P2[(Set (Var "c"))]) ")" ) ")" ) ")" ) & (Bool "(" "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) "st" (Bool (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool "(" "(" (Bool (Bool P1[(Set (Var "c"))])) "implies" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set F3 "(" (Set (Var "c")) ")" )) ")" & "(" (Bool (Bool P2[(Set (Var "c"))])) "implies" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set F4 "(" (Set (Var "c")) ")" )) ")" ")" ) ")" ) ")" )) provided (Bool "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) "st" (Bool (Bool P1[(Set (Var "c"))]) & (Bool P2[(Set (Var "c"))])) "holds" (Bool (Set F3 "(" (Set (Var "c")) ")" ) ($#r1_hidden :::"="::: ) (Set F4 "(" (Set (Var "c")) ")" ))) proof end; scheme :: SCHEME1:sch 8 PartFuncExD299{ F1() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , F2() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , P1[ ($#m1_hidden :::"set"::: ) ], F3( ($#m1_hidden :::"set"::: ) ) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ), F4( ($#m1_hidden :::"set"::: ) ) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ) } : (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set F1 "(" ")" ) "," (Set F2 "(" ")" ) "st" (Bool "(" (Bool (Set (Var "f")) "is" ($#v1_partfun1 :::"total"::: ) ) & (Bool "(" "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) "st" (Bool (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool "(" "(" (Bool (Bool P1[(Set (Var "c"))])) "implies" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set F3 "(" (Set (Var "c")) ")" )) ")" & "(" (Bool (Bool P1[(Set (Var "c"))])) "implies" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set F4 "(" (Set (Var "c")) ")" )) ")" ")" ) ")" ) ")" )) proof end; scheme :: SCHEME1:sch 9 PartFuncExD3{ F1() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , F2() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , P1[ ($#m1_hidden :::"set"::: ) ], P2[ ($#m1_hidden :::"set"::: ) ], P3[ ($#m1_hidden :::"set"::: ) ], F3( ($#m1_hidden :::"set"::: ) ) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ), F4( ($#m1_hidden :::"set"::: ) ) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ), F5( ($#m1_hidden :::"set"::: ) ) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ) } : (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set F1 "(" ")" ) "," (Set F2 "(" ")" ) "st" (Bool "(" (Bool "(" "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) "holds" (Bool "(" (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) "iff" (Bool "(" (Bool P1[(Set (Var "c"))]) "or" (Bool P2[(Set (Var "c"))]) "or" (Bool P3[(Set (Var "c"))]) ")" ) ")" ) ")" ) & (Bool "(" "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) "st" (Bool (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool "(" "(" (Bool (Bool P1[(Set (Var "c"))])) "implies" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set F3 "(" (Set (Var "c")) ")" )) ")" & "(" (Bool (Bool P2[(Set (Var "c"))])) "implies" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set F4 "(" (Set (Var "c")) ")" )) ")" & "(" (Bool (Bool P3[(Set (Var "c"))])) "implies" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set F5 "(" (Set (Var "c")) ")" )) ")" ")" ) ")" ) ")" )) provided (Bool "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) "holds" (Bool "(" "(" (Bool (Bool P1[(Set (Var "c"))])) "implies" (Bool "not" (Bool P2[(Set (Var "c"))])) ")" & "(" (Bool (Bool P1[(Set (Var "c"))])) "implies" (Bool "not" (Bool P3[(Set (Var "c"))])) ")" & "(" (Bool (Bool P2[(Set (Var "c"))])) "implies" (Bool "not" (Bool P3[(Set (Var "c"))])) ")" ")" )) proof end; scheme :: SCHEME1:sch 10 PartFuncExD39{ F1() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , F2() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , P1[ ($#m1_hidden :::"set"::: ) ], P2[ ($#m1_hidden :::"set"::: ) ], P3[ ($#m1_hidden :::"set"::: ) ], F3( ($#m1_hidden :::"set"::: ) ) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ), F4( ($#m1_hidden :::"set"::: ) ) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ), F5( ($#m1_hidden :::"set"::: ) ) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ) } : (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set F1 "(" ")" ) "," (Set F2 "(" ")" ) "st" (Bool "(" (Bool "(" "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) "holds" (Bool "(" (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) "iff" (Bool "(" (Bool P1[(Set (Var "c"))]) "or" (Bool P2[(Set (Var "c"))]) "or" (Bool P3[(Set (Var "c"))]) ")" ) ")" ) ")" ) & (Bool "(" "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) "st" (Bool (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool "(" "(" (Bool (Bool P1[(Set (Var "c"))])) "implies" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set F3 "(" (Set (Var "c")) ")" )) ")" & "(" (Bool (Bool P2[(Set (Var "c"))])) "implies" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set F4 "(" (Set (Var "c")) ")" )) ")" & "(" (Bool (Bool P3[(Set (Var "c"))])) "implies" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set F5 "(" (Set (Var "c")) ")" )) ")" ")" ) ")" ) ")" )) provided (Bool "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) "holds" (Bool "(" "(" (Bool (Bool P1[(Set (Var "c"))]) & (Bool P2[(Set (Var "c"))])) "implies" (Bool (Set F3 "(" (Set (Var "c")) ")" ) ($#r1_hidden :::"="::: ) (Set F4 "(" (Set (Var "c")) ")" )) ")" & "(" (Bool (Bool P1[(Set (Var "c"))]) & (Bool P3[(Set (Var "c"))])) "implies" (Bool (Set F3 "(" (Set (Var "c")) ")" ) ($#r1_hidden :::"="::: ) (Set F5 "(" (Set (Var "c")) ")" )) ")" & "(" (Bool (Bool P2[(Set (Var "c"))]) & (Bool P3[(Set (Var "c"))])) "implies" (Bool (Set F4 "(" (Set (Var "c")) ")" ) ($#r1_hidden :::"="::: ) (Set F5 "(" (Set (Var "c")) ")" )) ")" ")" )) proof end; scheme :: SCHEME1:sch 11 PartFuncExD4{ F1() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , F2() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , P1[ ($#m1_hidden :::"set"::: ) ], P2[ ($#m1_hidden :::"set"::: ) ], P3[ ($#m1_hidden :::"set"::: ) ], P4[ ($#m1_hidden :::"set"::: ) ], F3( ($#m1_hidden :::"set"::: ) ) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ), F4( ($#m1_hidden :::"set"::: ) ) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ), F5( ($#m1_hidden :::"set"::: ) ) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ), F6( ($#m1_hidden :::"set"::: ) ) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ) } : (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set F1 "(" ")" ) "," (Set F2 "(" ")" ) "st" (Bool "(" (Bool "(" "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) "holds" (Bool "(" (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) "iff" (Bool "(" (Bool P1[(Set (Var "c"))]) "or" (Bool P2[(Set (Var "c"))]) "or" (Bool P3[(Set (Var "c"))]) "or" (Bool P4[(Set (Var "c"))]) ")" ) ")" ) ")" ) & (Bool "(" "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) "st" (Bool (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool "(" "(" (Bool (Bool P1[(Set (Var "c"))])) "implies" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set F3 "(" (Set (Var "c")) ")" )) ")" & "(" (Bool (Bool P2[(Set (Var "c"))])) "implies" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set F4 "(" (Set (Var "c")) ")" )) ")" & "(" (Bool (Bool P3[(Set (Var "c"))])) "implies" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set F5 "(" (Set (Var "c")) ")" )) ")" & "(" (Bool (Bool P4[(Set (Var "c"))])) "implies" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set F6 "(" (Set (Var "c")) ")" )) ")" ")" ) ")" ) ")" )) provided (Bool "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) "holds" (Bool "(" "(" (Bool (Bool P1[(Set (Var "c"))])) "implies" (Bool "not" (Bool P2[(Set (Var "c"))])) ")" & "(" (Bool (Bool P1[(Set (Var "c"))])) "implies" (Bool "not" (Bool P3[(Set (Var "c"))])) ")" & "(" (Bool (Bool P1[(Set (Var "c"))])) "implies" (Bool "not" (Bool P4[(Set (Var "c"))])) ")" & "(" (Bool (Bool P2[(Set (Var "c"))])) "implies" (Bool "not" (Bool P3[(Set (Var "c"))])) ")" & "(" (Bool (Bool P2[(Set (Var "c"))])) "implies" (Bool "not" (Bool P4[(Set (Var "c"))])) ")" & "(" (Bool (Bool P3[(Set (Var "c"))])) "implies" (Bool "not" (Bool P4[(Set (Var "c"))])) ")" ")" )) proof end; scheme :: SCHEME1:sch 12 PartFuncExS2{ F1() -> ($#m1_hidden :::"set"::: ) , F2() -> ($#m1_hidden :::"set"::: ) , P1[ ($#m1_hidden :::"set"::: ) ], P2[ ($#m1_hidden :::"set"::: ) ], F3( ($#m1_hidden :::"set"::: ) ) -> ($#m1_hidden :::"set"::: ) , F4( ($#m1_hidden :::"set"::: ) ) -> ($#m1_hidden :::"set"::: ) } : (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set F1 "(" ")" ) "," (Set F2 "(" ")" ) "st" (Bool "(" (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) "iff" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set F1 "(" ")" )) & (Bool "(" (Bool P1[(Set (Var "x"))]) "or" (Bool P2[(Set (Var "x"))]) ")" ) ")" ) ")" ) ")" ) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool "(" "(" (Bool (Bool P1[(Set (Var "x"))])) "implies" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set F3 "(" (Set (Var "x")) ")" )) ")" & "(" (Bool (Bool P2[(Set (Var "x"))])) "implies" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set F4 "(" (Set (Var "x")) ")" )) ")" ")" ) ")" ) ")" )) provided (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set F1 "(" ")" )) & (Bool P1[(Set (Var "x"))])) "holds" (Bool "not" (Bool P2[(Set (Var "x"))]))) and (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set F1 "(" ")" )) & (Bool P1[(Set (Var "x"))])) "holds" (Bool (Set F3 "(" (Set (Var "x")) ")" ) ($#r2_hidden :::"in"::: ) (Set F2 "(" ")" ))) and (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set F1 "(" ")" )) & (Bool P2[(Set (Var "x"))])) "holds" (Bool (Set F4 "(" (Set (Var "x")) ")" ) ($#r2_hidden :::"in"::: ) (Set F2 "(" ")" ))) proof end; scheme :: SCHEME1:sch 13 PartFuncExS3{ F1() -> ($#m1_hidden :::"set"::: ) , F2() -> ($#m1_hidden :::"set"::: ) , P1[ ($#m1_hidden :::"set"::: ) ], P2[ ($#m1_hidden :::"set"::: ) ], P3[ ($#m1_hidden :::"set"::: ) ], F3( ($#m1_hidden :::"set"::: ) ) -> ($#m1_hidden :::"set"::: ) , F4( ($#m1_hidden :::"set"::: ) ) -> ($#m1_hidden :::"set"::: ) , F5( ($#m1_hidden :::"set"::: ) ) -> ($#m1_hidden :::"set"::: ) } : (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set F1 "(" ")" ) "," (Set F2 "(" ")" ) "st" (Bool "(" (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) "iff" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set F1 "(" ")" )) & (Bool "(" (Bool P1[(Set (Var "x"))]) "or" (Bool P2[(Set (Var "x"))]) "or" (Bool P3[(Set (Var "x"))]) ")" ) ")" ) ")" ) ")" ) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool "(" "(" (Bool (Bool P1[(Set (Var "x"))])) "implies" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set F3 "(" (Set (Var "x")) ")" )) ")" & "(" (Bool (Bool P2[(Set (Var "x"))])) "implies" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set F4 "(" (Set (Var "x")) ")" )) ")" & "(" (Bool (Bool P3[(Set (Var "x"))])) "implies" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set F5 "(" (Set (Var "x")) ")" )) ")" ")" ) ")" ) ")" )) provided (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set F1 "(" ")" ))) "holds" (Bool "(" "(" (Bool (Bool P1[(Set (Var "x"))])) "implies" (Bool "not" (Bool P2[(Set (Var "x"))])) ")" & "(" (Bool (Bool P1[(Set (Var "x"))])) "implies" (Bool "not" (Bool P3[(Set (Var "x"))])) ")" & "(" (Bool (Bool P2[(Set (Var "x"))])) "implies" (Bool "not" (Bool P3[(Set (Var "x"))])) ")" ")" )) and (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set F1 "(" ")" )) & (Bool P1[(Set (Var "x"))])) "holds" (Bool (Set F3 "(" (Set (Var "x")) ")" ) ($#r2_hidden :::"in"::: ) (Set F2 "(" ")" ))) and (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set F1 "(" ")" )) & (Bool P2[(Set (Var "x"))])) "holds" (Bool (Set F4 "(" (Set (Var "x")) ")" ) ($#r2_hidden :::"in"::: ) (Set F2 "(" ")" ))) and (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set F1 "(" ")" )) & (Bool P3[(Set (Var "x"))])) "holds" (Bool (Set F5 "(" (Set (Var "x")) ")" ) ($#r2_hidden :::"in"::: ) (Set F2 "(" ")" ))) proof end; scheme :: SCHEME1:sch 14 PartFuncExS4{ F1() -> ($#m1_hidden :::"set"::: ) , F2() -> ($#m1_hidden :::"set"::: ) , P1[ ($#m1_hidden :::"set"::: ) ], P2[ ($#m1_hidden :::"set"::: ) ], P3[ ($#m1_hidden :::"set"::: ) ], P4[ ($#m1_hidden :::"set"::: ) ], F3( ($#m1_hidden :::"set"::: ) ) -> ($#m1_hidden :::"set"::: ) , F4( ($#m1_hidden :::"set"::: ) ) -> ($#m1_hidden :::"set"::: ) , F5( ($#m1_hidden :::"set"::: ) ) -> ($#m1_hidden :::"set"::: ) , F6( ($#m1_hidden :::"set"::: ) ) -> ($#m1_hidden :::"set"::: ) } : (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set F1 "(" ")" ) "," (Set F2 "(" ")" ) "st" (Bool "(" (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) "iff" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set F1 "(" ")" )) & (Bool "(" (Bool P1[(Set (Var "x"))]) "or" (Bool P2[(Set (Var "x"))]) "or" (Bool P3[(Set (Var "x"))]) "or" (Bool P4[(Set (Var "x"))]) ")" ) ")" ) ")" ) ")" ) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool "(" "(" (Bool (Bool P1[(Set (Var "x"))])) "implies" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set F3 "(" (Set (Var "x")) ")" )) ")" & "(" (Bool (Bool P2[(Set (Var "x"))])) "implies" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set F4 "(" (Set (Var "x")) ")" )) ")" & "(" (Bool (Bool P3[(Set (Var "x"))])) "implies" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set F5 "(" (Set (Var "x")) ")" )) ")" & "(" (Bool (Bool P4[(Set (Var "x"))])) "implies" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set F6 "(" (Set (Var "x")) ")" )) ")" ")" ) ")" ) ")" )) provided (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set F1 "(" ")" ))) "holds" (Bool "(" "(" (Bool (Bool P1[(Set (Var "x"))])) "implies" (Bool "not" (Bool P2[(Set (Var "x"))])) ")" & "(" (Bool (Bool P1[(Set (Var "x"))])) "implies" (Bool "not" (Bool P3[(Set (Var "x"))])) ")" & "(" (Bool (Bool P1[(Set (Var "x"))])) "implies" (Bool "not" (Bool P4[(Set (Var "x"))])) ")" & "(" (Bool (Bool P2[(Set (Var "x"))])) "implies" (Bool "not" (Bool P3[(Set (Var "x"))])) ")" & "(" (Bool (Bool P2[(Set (Var "x"))])) "implies" (Bool "not" (Bool P4[(Set (Var "x"))])) ")" & "(" (Bool (Bool P3[(Set (Var "x"))])) "implies" (Bool "not" (Bool P4[(Set (Var "x"))])) ")" ")" )) and (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set F1 "(" ")" )) & (Bool P1[(Set (Var "x"))])) "holds" (Bool (Set F3 "(" (Set (Var "x")) ")" ) ($#r2_hidden :::"in"::: ) (Set F2 "(" ")" ))) and (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set F1 "(" ")" )) & (Bool P2[(Set (Var "x"))])) "holds" (Bool (Set F4 "(" (Set (Var "x")) ")" ) ($#r2_hidden :::"in"::: ) (Set F2 "(" ")" ))) and (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set F1 "(" ")" )) & (Bool P3[(Set (Var "x"))])) "holds" (Bool (Set F5 "(" (Set (Var "x")) ")" ) ($#r2_hidden :::"in"::: ) (Set F2 "(" ")" ))) and (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set F1 "(" ")" )) & (Bool P4[(Set (Var "x"))])) "holds" (Bool (Set F6 "(" (Set (Var "x")) ")" ) ($#r2_hidden :::"in"::: ) (Set F2 "(" ")" ))) proof end; scheme :: SCHEME1:sch 15 PartFuncExCD2{ F1() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , F2() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , F3() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , P1[ ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ], P2[ ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ], F4( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F3 "(" ")" ), F5( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F3 "(" ")" ) } : (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set F1 "(" ")" ) "," (Set F2 "(" ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set F3 "(" ")" ) "st" (Bool "(" (Bool "(" "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ) "holds" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "c")) "," (Set (Var "d")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) "iff" (Bool "(" (Bool P1[(Set (Var "c")) "," (Set (Var "d"))]) "or" (Bool P2[(Set (Var "c")) "," (Set (Var "d"))]) ")" ) ")" )) ")" ) & (Bool "(" "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "c")) "," (Set (Var "d")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool "(" "(" (Bool (Bool P1[(Set (Var "c")) "," (Set (Var "d"))])) "implies" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "c")) "," (Set (Var "d")) ($#k4_tarski :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Set F4 "(" (Set (Var "c")) "," (Set (Var "d")) ")" )) ")" & "(" (Bool (Bool P2[(Set (Var "c")) "," (Set (Var "d"))])) "implies" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "c")) "," (Set (Var "d")) ($#k4_tarski :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Set F5 "(" (Set (Var "c")) "," (Set (Var "d")) ")" )) ")" ")" )) ")" ) ")" )) provided (Bool "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ) "st" (Bool (Bool P1[(Set (Var "c")) "," (Set (Var "d"))])) "holds" (Bool "not" (Bool P2[(Set (Var "c")) "," (Set (Var "d"))])))) proof end; scheme :: SCHEME1:sch 16 PartFuncExCD3{ F1() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , F2() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , F3() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , P1[ ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ], P2[ ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ], P3[ ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ], F4( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F3 "(" ")" ), F5( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F3 "(" ")" ), F6( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F3 "(" ")" ) } : (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set F1 "(" ")" ) "," (Set F2 "(" ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set F3 "(" ")" ) "st" (Bool "(" (Bool "(" "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ) "holds" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "c")) "," (Set (Var "d")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) "iff" (Bool "(" (Bool P1[(Set (Var "c")) "," (Set (Var "d"))]) "or" (Bool P2[(Set (Var "c")) "," (Set (Var "d"))]) "or" (Bool P3[(Set (Var "c")) "," (Set (Var "d"))]) ")" ) ")" )) ")" ) & (Bool "(" "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "c")) "," (Set (Var "r")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool "(" "(" (Bool (Bool P1[(Set (Var "c")) "," (Set (Var "r"))])) "implies" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "c")) "," (Set (Var "r")) ($#k4_tarski :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Set F4 "(" (Set (Var "c")) "," (Set (Var "r")) ")" )) ")" & "(" (Bool (Bool P2[(Set (Var "c")) "," (Set (Var "r"))])) "implies" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "c")) "," (Set (Var "r")) ($#k4_tarski :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Set F5 "(" (Set (Var "c")) "," (Set (Var "r")) ")" )) ")" & "(" (Bool (Bool P3[(Set (Var "c")) "," (Set (Var "r"))])) "implies" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "c")) "," (Set (Var "r")) ($#k4_tarski :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Set F6 "(" (Set (Var "c")) "," (Set (Var "r")) ")" )) ")" ")" )) ")" ) ")" )) provided (Bool "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ) "holds" (Bool "(" "(" (Bool (Bool P1[(Set (Var "c")) "," (Set (Var "s"))])) "implies" (Bool "not" (Bool P2[(Set (Var "c")) "," (Set (Var "s"))])) ")" & "(" (Bool (Bool P1[(Set (Var "c")) "," (Set (Var "s"))])) "implies" (Bool "not" (Bool P3[(Set (Var "c")) "," (Set (Var "s"))])) ")" & "(" (Bool (Bool P2[(Set (Var "c")) "," (Set (Var "s"))])) "implies" (Bool "not" (Bool P3[(Set (Var "c")) "," (Set (Var "s"))])) ")" ")" ))) proof end; scheme :: SCHEME1:sch 17 PartFuncExCS2{ F1() -> ($#m1_hidden :::"set"::: ) , F2() -> ($#m1_hidden :::"set"::: ) , F3() -> ($#m1_hidden :::"set"::: ) , P1[ ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ], P2[ ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ], F4( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#m1_hidden :::"set"::: ) , F5( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#m1_hidden :::"set"::: ) } : (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set F1 "(" ")" ) "," (Set F2 "(" ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set F3 "(" ")" ) "st" (Bool "(" (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) "iff" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set F1 "(" ")" )) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set F2 "(" ")" )) & (Bool "(" (Bool P1[(Set (Var "x")) "," (Set (Var "y"))]) "or" (Bool P2[(Set (Var "x")) "," (Set (Var "y"))]) ")" ) ")" ) ")" ) ")" ) & (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool "(" "(" (Bool (Bool P1[(Set (Var "x")) "," (Set (Var "y"))])) "implies" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Set F4 "(" (Set (Var "x")) "," (Set (Var "y")) ")" )) ")" & "(" (Bool (Bool P2[(Set (Var "x")) "," (Set (Var "y"))])) "implies" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Set F5 "(" (Set (Var "x")) "," (Set (Var "y")) ")" )) ")" ")" ) ")" ) ")" )) provided (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set F1 "(" ")" )) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set F2 "(" ")" )) & (Bool P1[(Set (Var "x")) "," (Set (Var "y"))])) "holds" (Bool "not" (Bool P2[(Set (Var "x")) "," (Set (Var "y"))]))) and (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set F1 "(" ")" )) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set F2 "(" ")" )) & (Bool P1[(Set (Var "x")) "," (Set (Var "y"))])) "holds" (Bool (Set F4 "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r2_hidden :::"in"::: ) (Set F3 "(" ")" ))) and (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set F1 "(" ")" )) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set F2 "(" ")" )) & (Bool P2[(Set (Var "x")) "," (Set (Var "y"))])) "holds" (Bool (Set F5 "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r2_hidden :::"in"::: ) (Set F3 "(" ")" ))) proof end; scheme :: SCHEME1:sch 18 PartFuncExCS3{ F1() -> ($#m1_hidden :::"set"::: ) , F2() -> ($#m1_hidden :::"set"::: ) , F3() -> ($#m1_hidden :::"set"::: ) , P1[ ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ], P2[ ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ], P3[ ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ], F4( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#m1_hidden :::"set"::: ) , F5( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#m1_hidden :::"set"::: ) , F6( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#m1_hidden :::"set"::: ) } : (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set F1 "(" ")" ) "," (Set F2 "(" ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set F3 "(" ")" ) "st" (Bool "(" (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) "iff" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set F1 "(" ")" )) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set F2 "(" ")" )) & (Bool "(" (Bool P1[(Set (Var "x")) "," (Set (Var "y"))]) "or" (Bool P2[(Set (Var "x")) "," (Set (Var "y"))]) "or" (Bool P3[(Set (Var "x")) "," (Set (Var "y"))]) ")" ) ")" ) ")" ) ")" ) & (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool "(" "(" (Bool (Bool P1[(Set (Var "x")) "," (Set (Var "y"))])) "implies" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Set F4 "(" (Set (Var "x")) "," (Set (Var "y")) ")" )) ")" & "(" (Bool (Bool P2[(Set (Var "x")) "," (Set (Var "y"))])) "implies" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Set F5 "(" (Set (Var "x")) "," (Set (Var "y")) ")" )) ")" & "(" (Bool (Bool P3[(Set (Var "x")) "," (Set (Var "y"))])) "implies" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Set F6 "(" (Set (Var "x")) "," (Set (Var "y")) ")" )) ")" ")" ) ")" ) ")" )) provided (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set F1 "(" ")" )) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set F2 "(" ")" ))) "holds" (Bool "(" "(" (Bool (Bool P1[(Set (Var "x")) "," (Set (Var "y"))])) "implies" (Bool "not" (Bool P2[(Set (Var "x")) "," (Set (Var "y"))])) ")" & "(" (Bool (Bool P1[(Set (Var "x")) "," (Set (Var "y"))])) "implies" (Bool "not" (Bool P3[(Set (Var "x")) "," (Set (Var "y"))])) ")" & "(" (Bool (Bool P2[(Set (Var "x")) "," (Set (Var "y"))])) "implies" (Bool "not" (Bool P3[(Set (Var "x")) "," (Set (Var "y"))])) ")" ")" )) and (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set F1 "(" ")" )) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set F2 "(" ")" )) & (Bool P1[(Set (Var "x")) "," (Set (Var "y"))])) "holds" (Bool (Set F4 "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r2_hidden :::"in"::: ) (Set F3 "(" ")" ))) and (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set F1 "(" ")" )) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set F2 "(" ")" )) & (Bool P2[(Set (Var "x")) "," (Set (Var "y"))])) "holds" (Bool (Set F5 "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r2_hidden :::"in"::: ) (Set F3 "(" ")" ))) and (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set F1 "(" ")" )) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set F2 "(" ")" )) & (Bool P3[(Set (Var "x")) "," (Set (Var "y"))])) "holds" (Bool (Set F6 "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r2_hidden :::"in"::: ) (Set F3 "(" ")" ))) proof end; scheme :: SCHEME1:sch 19 ExFuncD3{ F1() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , F2() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , P1[ ($#m1_hidden :::"set"::: ) ], P2[ ($#m1_hidden :::"set"::: ) ], P3[ ($#m1_hidden :::"set"::: ) ], F3( ($#m1_hidden :::"set"::: ) ) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ), F4( ($#m1_hidden :::"set"::: ) ) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ), F5( ($#m1_hidden :::"set"::: ) ) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ) } : (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set F1 "(" ")" ) "," (Set F2 "(" ")" ) "st" (Bool "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) "holds" (Bool "(" "(" (Bool (Bool P1[(Set (Var "c"))])) "implies" (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set F3 "(" (Set (Var "c")) ")" )) ")" & "(" (Bool (Bool P2[(Set (Var "c"))])) "implies" (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set F4 "(" (Set (Var "c")) ")" )) ")" & "(" (Bool (Bool P3[(Set (Var "c"))])) "implies" (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set F5 "(" (Set (Var "c")) ")" )) ")" ")" ))) provided (Bool "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) "holds" (Bool "(" "(" (Bool (Bool P1[(Set (Var "c"))])) "implies" (Bool "not" (Bool P2[(Set (Var "c"))])) ")" & "(" (Bool (Bool P1[(Set (Var "c"))])) "implies" (Bool "not" (Bool P3[(Set (Var "c"))])) ")" & "(" (Bool (Bool P2[(Set (Var "c"))])) "implies" (Bool "not" (Bool P3[(Set (Var "c"))])) ")" ")" )) and (Bool "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) "holds" (Bool "(" (Bool P1[(Set (Var "c"))]) "or" (Bool P2[(Set (Var "c"))]) "or" (Bool P3[(Set (Var "c"))]) ")" )) proof end; scheme :: SCHEME1:sch 20 ExFuncD4{ F1() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , F2() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , P1[ ($#m1_hidden :::"set"::: ) ], P2[ ($#m1_hidden :::"set"::: ) ], P3[ ($#m1_hidden :::"set"::: ) ], P4[ ($#m1_hidden :::"set"::: ) ], F3( ($#m1_hidden :::"set"::: ) ) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ), F4( ($#m1_hidden :::"set"::: ) ) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ), F5( ($#m1_hidden :::"set"::: ) ) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ), F6( ($#m1_hidden :::"set"::: ) ) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ) } : (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set F1 "(" ")" ) "," (Set F2 "(" ")" ) "st" (Bool "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) "holds" (Bool "(" "(" (Bool (Bool P1[(Set (Var "c"))])) "implies" (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set F3 "(" (Set (Var "c")) ")" )) ")" & "(" (Bool (Bool P2[(Set (Var "c"))])) "implies" (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set F4 "(" (Set (Var "c")) ")" )) ")" & "(" (Bool (Bool P3[(Set (Var "c"))])) "implies" (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set F5 "(" (Set (Var "c")) ")" )) ")" & "(" (Bool (Bool P4[(Set (Var "c"))])) "implies" (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set F6 "(" (Set (Var "c")) ")" )) ")" ")" ))) provided (Bool "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) "holds" (Bool "(" "(" (Bool (Bool P1[(Set (Var "c"))])) "implies" (Bool "not" (Bool P2[(Set (Var "c"))])) ")" & "(" (Bool (Bool P1[(Set (Var "c"))])) "implies" (Bool "not" (Bool P3[(Set (Var "c"))])) ")" & "(" (Bool (Bool P1[(Set (Var "c"))])) "implies" (Bool "not" (Bool P4[(Set (Var "c"))])) ")" & "(" (Bool (Bool P2[(Set (Var "c"))])) "implies" (Bool "not" (Bool P3[(Set (Var "c"))])) ")" & "(" (Bool (Bool P2[(Set (Var "c"))])) "implies" (Bool "not" (Bool P4[(Set (Var "c"))])) ")" & "(" (Bool (Bool P3[(Set (Var "c"))])) "implies" (Bool "not" (Bool P4[(Set (Var "c"))])) ")" ")" )) and (Bool "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) "holds" (Bool "(" (Bool P1[(Set (Var "c"))]) "or" (Bool P2[(Set (Var "c"))]) "or" (Bool P3[(Set (Var "c"))]) "or" (Bool P4[(Set (Var "c"))]) ")" )) proof end; scheme :: SCHEME1:sch 21 FuncExCD2{ F1() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , F2() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , F3() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , P1[ ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ], F4( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F3 "(" ")" ), F5( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F3 "(" ")" ) } : (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set F1 "(" ")" ) "," (Set F2 "(" ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set F3 "(" ")" ) "st" (Bool "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "c")) "," (Set (Var "d")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool "(" "(" (Bool (Bool P1[(Set (Var "c")) "," (Set (Var "d"))])) "implies" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "c")) "," (Set (Var "d")) ($#k4_tarski :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Set F4 "(" (Set (Var "c")) "," (Set (Var "d")) ")" )) ")" & "(" (Bool (Bool P1[(Set (Var "c")) "," (Set (Var "d"))])) "implies" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "c")) "," (Set (Var "d")) ($#k4_tarski :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Set F5 "(" (Set (Var "c")) "," (Set (Var "d")) ")" )) ")" ")" )))) proof end; scheme :: SCHEME1:sch 22 FuncExCD3{ F1() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , F2() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , F3() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , P1[ ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ], P2[ ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ], P3[ ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ], F4( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F3 "(" ")" ), F5( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F3 "(" ")" ), F6( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F3 "(" ")" ) } : (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set F1 "(" ")" ) "," (Set F2 "(" ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set F3 "(" ")" ) "st" (Bool "(" (Bool "(" "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ) "holds" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "c")) "," (Set (Var "d")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) "iff" (Bool "(" (Bool P1[(Set (Var "c")) "," (Set (Var "d"))]) "or" (Bool P2[(Set (Var "c")) "," (Set (Var "d"))]) "or" (Bool P3[(Set (Var "c")) "," (Set (Var "d"))]) ")" ) ")" )) ")" ) & (Bool "(" "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "c")) "," (Set (Var "d")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool "(" "(" (Bool (Bool P1[(Set (Var "c")) "," (Set (Var "d"))])) "implies" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "c")) "," (Set (Var "d")) ($#k4_tarski :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Set F4 "(" (Set (Var "c")) "," (Set (Var "d")) ")" )) ")" & "(" (Bool (Bool P2[(Set (Var "c")) "," (Set (Var "d"))])) "implies" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "c")) "," (Set (Var "d")) ($#k4_tarski :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Set F5 "(" (Set (Var "c")) "," (Set (Var "d")) ")" )) ")" & "(" (Bool (Bool P3[(Set (Var "c")) "," (Set (Var "d"))])) "implies" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "c")) "," (Set (Var "d")) ($#k4_tarski :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Set F6 "(" (Set (Var "c")) "," (Set (Var "d")) ")" )) ")" ")" )) ")" ) ")" )) provided (Bool "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ) "holds" (Bool "(" "(" (Bool (Bool P1[(Set (Var "c")) "," (Set (Var "d"))])) "implies" (Bool "not" (Bool P2[(Set (Var "c")) "," (Set (Var "d"))])) ")" & "(" (Bool (Bool P1[(Set (Var "c")) "," (Set (Var "d"))])) "implies" (Bool "not" (Bool P3[(Set (Var "c")) "," (Set (Var "d"))])) ")" & "(" (Bool (Bool P2[(Set (Var "c")) "," (Set (Var "d"))])) "implies" (Bool "not" (Bool P3[(Set (Var "c")) "," (Set (Var "d"))])) ")" ")" ))) and (Bool "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ) "holds" (Bool "(" (Bool P1[(Set (Var "c")) "," (Set (Var "d"))]) "or" (Bool P2[(Set (Var "c")) "," (Set (Var "d"))]) "or" (Bool P3[(Set (Var "c")) "," (Set (Var "d"))]) ")" ))) proof end;