:: RECDEF_2 semantic presentation begin definitionlet "x" be ($#v2_xtuple_0 :::"triple"::: ) ($#m1_hidden :::"set"::: ) ; redefine func "x" :::"`1_3"::: means :: RECDEF_2:def 1 (Bool "for" (Set (Var "y1")) "," (Set (Var "y2")) "," (Set (Var "y3")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool "x" ($#r1_hidden :::"="::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Set (Var "y1")) "," (Set (Var "y2")) "," (Set (Var "y3")) ($#k3_xtuple_0 :::"]"::: ) ))) "holds" (Bool it ($#r1_hidden :::"="::: ) (Set (Var "y1")))); redefine func "x" :::"`2_3"::: means :: RECDEF_2:def 2 (Bool "for" (Set (Var "y1")) "," (Set (Var "y2")) "," (Set (Var "y3")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool "x" ($#r1_hidden :::"="::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Set (Var "y1")) "," (Set (Var "y2")) "," (Set (Var "y3")) ($#k3_xtuple_0 :::"]"::: ) ))) "holds" (Bool it ($#r1_hidden :::"="::: ) (Set (Var "y2")))); redefine func "x" :::"`2"::: means :: RECDEF_2:def 3 (Bool "for" (Set (Var "y1")) "," (Set (Var "y2")) "," (Set (Var "y3")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool "x" ($#r1_hidden :::"="::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Set (Var "y1")) "," (Set (Var "y2")) "," (Set (Var "y3")) ($#k3_xtuple_0 :::"]"::: ) ))) "holds" (Bool it ($#r1_hidden :::"="::: ) (Set (Var "y3")))); end; :: deftheorem defines :::"`1_3"::: RECDEF_2:def 1 : (Bool "for" (Set (Var "x")) "being" ($#v2_xtuple_0 :::"triple"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b2")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k4_xtuple_0 :::"`1_3"::: ) )) "iff" (Bool "for" (Set (Var "y1")) "," (Set (Var "y2")) "," (Set (Var "y3")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Set (Var "y1")) "," (Set (Var "y2")) "," (Set (Var "y3")) ($#k3_xtuple_0 :::"]"::: ) ))) "holds" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set (Var "y1")))) ")" ))); :: deftheorem defines :::"`2_3"::: RECDEF_2:def 2 : (Bool "for" (Set (Var "x")) "being" ($#v2_xtuple_0 :::"triple"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b2")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k5_xtuple_0 :::"`2_3"::: ) )) "iff" (Bool "for" (Set (Var "y1")) "," (Set (Var "y2")) "," (Set (Var "y3")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Set (Var "y1")) "," (Set (Var "y2")) "," (Set (Var "y3")) ($#k3_xtuple_0 :::"]"::: ) ))) "holds" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set (Var "y2")))) ")" ))); :: deftheorem defines :::"`3_3"::: RECDEF_2:def 3 : (Bool "for" (Set (Var "x")) "being" ($#v2_xtuple_0 :::"triple"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b2")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k2_xtuple_0 :::"`3_3"::: ) )) "iff" (Bool "for" (Set (Var "y1")) "," (Set (Var "y2")) "," (Set (Var "y3")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Set (Var "y1")) "," (Set (Var "y2")) "," (Set (Var "y3")) ($#k3_xtuple_0 :::"]"::: ) ))) "holds" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set (Var "y3")))) ")" ))); theorem :: RECDEF_2:1 (Bool "for" (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool "ex" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ($#k3_xtuple_0 :::"]"::: ) )))) "holds" (Bool (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Set "(" (Set (Var "z")) ($#k4_xtuple_0 :::"`1_3"::: ) ")" ) "," (Set "(" (Set (Var "z")) ($#k5_xtuple_0 :::"`2_3"::: ) ")" ) "," (Set "(" (Set (Var "z")) ($#k2_xtuple_0 :::"`3_3"::: ) ")" ) ($#k3_xtuple_0 :::"]"::: ) ))) ; theorem :: RECDEF_2:2 (Bool "for" (Set (Var "z")) "," (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set ($#k3_zfmisc_1 :::"[:"::: ) (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) ($#k3_zfmisc_1 :::":]"::: ) ))) "holds" (Bool "(" (Bool (Set (Set (Var "z")) ($#k4_xtuple_0 :::"`1_3"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Set (Var "z")) ($#k5_xtuple_0 :::"`2_3"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "B"))) & (Bool (Set (Set (Var "z")) ($#k2_xtuple_0 :::"`3_3"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "C"))) ")" )) ; theorem :: RECDEF_2:3 (Bool "for" (Set (Var "z")) "," (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set ($#k3_zfmisc_1 :::"[:"::: ) (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) ($#k3_zfmisc_1 :::":]"::: ) ))) "holds" (Bool (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Set "(" (Set (Var "z")) ($#k4_xtuple_0 :::"`1_3"::: ) ")" ) "," (Set "(" (Set (Var "z")) ($#k5_xtuple_0 :::"`2_3"::: ) ")" ) "," (Set "(" (Set (Var "z")) ($#k2_xtuple_0 :::"`3_3"::: ) ")" ) ($#k3_xtuple_0 :::"]"::: ) ))) ; definitionlet "x" be ($#v3_xtuple_0 :::"quadruple"::: ) ($#m1_hidden :::"set"::: ) ; redefine func "x" :::"`1_4"::: means :: RECDEF_2:def 4 (Bool "for" (Set (Var "y1")) "," (Set (Var "y2")) "," (Set (Var "y3")) "," (Set (Var "y4")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool "x" ($#r1_hidden :::"="::: ) (Set ($#k6_xtuple_0 :::"["::: ) (Set (Var "y1")) "," (Set (Var "y2")) "," (Set (Var "y3")) "," (Set (Var "y4")) ($#k6_xtuple_0 :::"]"::: ) ))) "holds" (Bool it ($#r1_hidden :::"="::: ) (Set (Var "y1")))); redefine func "x" :::"`2_4"::: means :: RECDEF_2:def 5 (Bool "for" (Set (Var "y1")) "," (Set (Var "y2")) "," (Set (Var "y3")) "," (Set (Var "y4")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool "x" ($#r1_hidden :::"="::: ) (Set ($#k6_xtuple_0 :::"["::: ) (Set (Var "y1")) "," (Set (Var "y2")) "," (Set (Var "y3")) "," (Set (Var "y4")) ($#k6_xtuple_0 :::"]"::: ) ))) "holds" (Bool it ($#r1_hidden :::"="::: ) (Set (Var "y2")))); redefine func "x" :::"`2_3"::: means :: RECDEF_2:def 6 (Bool "for" (Set (Var "y1")) "," (Set (Var "y2")) "," (Set (Var "y3")) "," (Set (Var "y4")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool "x" ($#r1_hidden :::"="::: ) (Set ($#k6_xtuple_0 :::"["::: ) (Set (Var "y1")) "," (Set (Var "y2")) "," (Set (Var "y3")) "," (Set (Var "y4")) ($#k6_xtuple_0 :::"]"::: ) ))) "holds" (Bool it ($#r1_hidden :::"="::: ) (Set (Var "y3")))); redefine func "x" :::"`2"::: means :: RECDEF_2:def 7 (Bool "for" (Set (Var "y1")) "," (Set (Var "y2")) "," (Set (Var "y3")) "," (Set (Var "y4")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool "x" ($#r1_hidden :::"="::: ) (Set ($#k6_xtuple_0 :::"["::: ) (Set (Var "y1")) "," (Set (Var "y2")) "," (Set (Var "y3")) "," (Set (Var "y4")) ($#k6_xtuple_0 :::"]"::: ) ))) "holds" (Bool it ($#r1_hidden :::"="::: ) (Set (Var "y4")))); end; :: deftheorem defines :::"`1_4"::: RECDEF_2:def 4 : (Bool "for" (Set (Var "x")) "being" ($#v3_xtuple_0 :::"quadruple"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b2")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k7_xtuple_0 :::"`1_4"::: ) )) "iff" (Bool "for" (Set (Var "y1")) "," (Set (Var "y2")) "," (Set (Var "y3")) "," (Set (Var "y4")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k6_xtuple_0 :::"["::: ) (Set (Var "y1")) "," (Set (Var "y2")) "," (Set (Var "y3")) "," (Set (Var "y4")) ($#k6_xtuple_0 :::"]"::: ) ))) "holds" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set (Var "y1")))) ")" ))); :: deftheorem defines :::"`2_4"::: RECDEF_2:def 5 : (Bool "for" (Set (Var "x")) "being" ($#v3_xtuple_0 :::"quadruple"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b2")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k8_xtuple_0 :::"`2_4"::: ) )) "iff" (Bool "for" (Set (Var "y1")) "," (Set (Var "y2")) "," (Set (Var "y3")) "," (Set (Var "y4")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k6_xtuple_0 :::"["::: ) (Set (Var "y1")) "," (Set (Var "y2")) "," (Set (Var "y3")) "," (Set (Var "y4")) ($#k6_xtuple_0 :::"]"::: ) ))) "holds" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set (Var "y2")))) ")" ))); :: deftheorem defines :::"`2_3"::: RECDEF_2:def 6 : (Bool "for" (Set (Var "x")) "being" ($#v3_xtuple_0 :::"quadruple"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b2")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k5_xtuple_0 :::"`2_3"::: ) )) "iff" (Bool "for" (Set (Var "y1")) "," (Set (Var "y2")) "," (Set (Var "y3")) "," (Set (Var "y4")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k6_xtuple_0 :::"["::: ) (Set (Var "y1")) "," (Set (Var "y2")) "," (Set (Var "y3")) "," (Set (Var "y4")) ($#k6_xtuple_0 :::"]"::: ) ))) "holds" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set (Var "y3")))) ")" ))); :: deftheorem defines :::"`3_3"::: RECDEF_2:def 7 : (Bool "for" (Set (Var "x")) "being" ($#v3_xtuple_0 :::"quadruple"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b2")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k2_xtuple_0 :::"`3_3"::: ) )) "iff" (Bool "for" (Set (Var "y1")) "," (Set (Var "y2")) "," (Set (Var "y3")) "," (Set (Var "y4")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k6_xtuple_0 :::"["::: ) (Set (Var "y1")) "," (Set (Var "y2")) "," (Set (Var "y3")) "," (Set (Var "y4")) ($#k6_xtuple_0 :::"]"::: ) ))) "holds" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set (Var "y4")))) ")" ))); theorem :: RECDEF_2:4 (Bool "for" (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool "ex" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set ($#k6_xtuple_0 :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) ($#k6_xtuple_0 :::"]"::: ) )))) "holds" (Bool (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set ($#k6_xtuple_0 :::"["::: ) (Set "(" (Set (Var "z")) ($#k7_xtuple_0 :::"`1_4"::: ) ")" ) "," (Set "(" (Set (Var "z")) ($#k8_xtuple_0 :::"`2_4"::: ) ")" ) "," (Set "(" (Set (Var "z")) ($#k5_xtuple_0 :::"`3_4"::: ) ")" ) "," (Set "(" (Set (Var "z")) ($#k2_xtuple_0 :::"`4_4"::: ) ")" ) ($#k6_xtuple_0 :::"]"::: ) ))) ; theorem :: RECDEF_2:5 (Bool "for" (Set (Var "z")) "," (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "D")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set ($#k4_zfmisc_1 :::"[:"::: ) (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "D")) ($#k4_zfmisc_1 :::":]"::: ) ))) "holds" (Bool "(" (Bool (Set (Set (Var "z")) ($#k7_xtuple_0 :::"`1_4"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Set (Var "z")) ($#k8_xtuple_0 :::"`2_4"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "B"))) & (Bool (Set (Set (Var "z")) ($#k5_xtuple_0 :::"`3_4"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "C"))) & (Bool (Set (Set (Var "z")) ($#k2_xtuple_0 :::"`4_4"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "D"))) ")" )) ; theorem :: RECDEF_2:6 (Bool "for" (Set (Var "z")) "," (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "D")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set ($#k4_zfmisc_1 :::"[:"::: ) (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "D")) ($#k4_zfmisc_1 :::":]"::: ) ))) "holds" (Bool (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set ($#k6_xtuple_0 :::"["::: ) (Set "(" (Set (Var "z")) ($#k7_xtuple_0 :::"`1_4"::: ) ")" ) "," (Set "(" (Set (Var "z")) ($#k8_xtuple_0 :::"`2_4"::: ) ")" ) "," (Set "(" (Set (Var "z")) ($#k5_xtuple_0 :::"`3_4"::: ) ")" ) "," (Set "(" (Set (Var "z")) ($#k2_xtuple_0 :::"`4_4"::: ) ")" ) ($#k6_xtuple_0 :::"]"::: ) ))) ; definitioncanceled; canceled; canceled; canceled; canceled; end; :: deftheorem RECDEF_2:def 8 : canceled; :: deftheorem RECDEF_2:def 9 : canceled; :: deftheorem RECDEF_2:def 10 : canceled; :: deftheorem RECDEF_2:def 11 : canceled; :: deftheorem RECDEF_2:def 12 : canceled; theorem :: RECDEF_2:7 canceled; theorem :: RECDEF_2:8 canceled; theorem :: RECDEF_2:9 canceled; scheme :: RECDEF_2:sch 1 ExFunc3Cond{ F1() -> ($#m1_hidden :::"set"::: ) , P1[ ($#m1_hidden :::"set"::: ) ], P2[ ($#m1_hidden :::"set"::: ) ], P3[ ($#m1_hidden :::"set"::: ) ], F2( ($#m1_hidden :::"set"::: ) ) -> ($#m1_hidden :::"set"::: ) , F3( ($#m1_hidden :::"set"::: ) ) -> ($#m1_hidden :::"set"::: ) , F4( ($#m1_hidden :::"set"::: ) ) -> ($#m1_hidden :::"set"::: ) } : (Bool "ex" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "st" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set F1 "(" ")" )) & (Bool "(" "for" (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set F1 "(" ")" ))) "holds" (Bool "(" "(" (Bool (Bool P1[(Set (Var "c"))])) "implies" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set F2 "(" (Set (Var "c")) ")" )) ")" & "(" (Bool (Bool P2[(Set (Var "c"))])) "implies" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set F3 "(" (Set (Var "c")) ")" )) ")" & "(" (Bool (Bool P3[(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_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (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_hidden :::"set"::: ) "holds" (Bool "(" "not" (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set F1 "(" ")" )) "or" (Bool P1[(Set (Var "c"))]) "or" (Bool P2[(Set (Var "c"))]) "or" (Bool P3[(Set (Var "c"))]) ")" )) proof end; scheme :: RECDEF_2:sch 2 ExFunc4Cond{ F1() -> ($#m1_hidden :::"set"::: ) , P1[ ($#m1_hidden :::"set"::: ) ], P2[ ($#m1_hidden :::"set"::: ) ], P3[ ($#m1_hidden :::"set"::: ) ], P4[ ($#m1_hidden :::"set"::: ) ], F2( ($#m1_hidden :::"set"::: ) ) -> ($#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_hidden :::"Function":::) "st" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set F1 "(" ")" )) & (Bool "(" "for" (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set F1 "(" ")" ))) "holds" (Bool "(" "(" (Bool (Bool P1[(Set (Var "c"))])) "implies" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set F2 "(" (Set (Var "c")) ")" )) ")" & "(" (Bool (Bool P2[(Set (Var "c"))])) "implies" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set F3 "(" (Set (Var "c")) ")" )) ")" & "(" (Bool (Bool P3[(Set (Var "c"))])) "implies" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set F4 "(" (Set (Var "c")) ")" )) ")" & "(" (Bool (Bool P4[(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_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (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_hidden :::"set"::: ) "holds" (Bool "(" "not" (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set F1 "(" ")" )) "or" (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 :: RECDEF_2:sch 3 DoubleChoiceRec{ 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() -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ), F4() -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ), P1[ ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ] } : (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set F1 "(" ")" )(Bool "ex" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set F2 "(" ")" ) "st" (Bool "(" (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set F3 "(" ")" )) & (Bool (Set (Set (Var "g")) ($#k3_funct_2 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set F4 "(" ")" )) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool P1[(Set (Var "n")) "," (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "n"))) "," (Set (Set (Var "g")) ($#k3_funct_2 :::"."::: ) (Set (Var "n"))) "," (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) "," (Set (Set (Var "g")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ))]) ")" ) ")" ))) provided (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ) (Bool "ex" (Set (Var "x1")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" )(Bool "ex" (Set (Var "y1")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ) "st" (Bool P1[(Set (Var "n")) "," (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "x1")) "," (Set (Var "y1"))])))))) proof end; scheme :: RECDEF_2:sch 4 LambdaRec2Ex{ F1() -> ($#m1_hidden :::"set"::: ) , F2() -> ($#m1_hidden :::"set"::: ) , F3( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#m1_hidden :::"set"::: ) } : (Bool "ex" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "st" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k5_numbers :::"NAT"::: ) )) & (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set F1 "(" ")" )) & (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set F2 "(" ")" )) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 2) ")" )) ($#r1_hidden :::"="::: ) (Set F3 "(" (Set (Var "n")) "," (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")) ")" ) "," (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ")" )) ")" ) ")" )) proof end; scheme :: RECDEF_2:sch 5 LambdaRec2ExD{ F1() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , F2() -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ), F3() -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ), F4( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) } : (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set F1 "(" ")" ) "st" (Bool "(" (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set F2 "(" ")" )) & (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set F3 "(" ")" )) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 2) ")" )) ($#r1_hidden :::"="::: ) (Set F4 "(" (Set (Var "n")) "," (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "n")) ")" ) "," (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ")" )) ")" ) ")" )) proof end; scheme :: RECDEF_2:sch 6 LambdaRec2Un{ F1() -> ($#m1_hidden :::"set"::: ) , F2() -> ($#m1_hidden :::"set"::: ) , F3() -> ($#m1_hidden :::"Function":::), F4() -> ($#m1_hidden :::"Function":::), F5( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#m1_hidden :::"set"::: ) } : (Bool (Set F3 "(" ")" ) ($#r1_hidden :::"="::: ) (Set F4 "(" ")" )) provided (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set F3 "(" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k5_numbers :::"NAT"::: ) )) and (Bool "(" (Bool (Set (Set F3 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set F1 "(" ")" )) & (Bool (Set (Set F3 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set F2 "(" ")" )) ")" ) and (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set F3 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 2) ")" )) ($#r1_hidden :::"="::: ) (Set F5 "(" (Set (Var "n")) "," (Set "(" (Set F3 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "n")) ")" ) "," (Set "(" (Set F3 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ")" ))) and (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set F4 "(" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k5_numbers :::"NAT"::: ) )) and (Bool "(" (Bool (Set (Set F4 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set F1 "(" ")" )) & (Bool (Set (Set F4 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set F2 "(" ")" )) ")" ) and (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set F4 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 2) ")" )) ($#r1_hidden :::"="::: ) (Set F5 "(" (Set (Var "n")) "," (Set "(" (Set F4 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "n")) ")" ) "," (Set "(" (Set F4 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ")" ))) proof end; scheme :: RECDEF_2:sch 7 LambdaRec2UnD{ F1() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , F2() -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ), F3() -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ), F4() -> ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set F1 "(" ")" ), F5() -> ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set F1 "(" ")" ), F6( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) } : (Bool (Set F4 "(" ")" ) ($#r2_funct_2 :::"="::: ) (Set F5 "(" ")" )) provided (Bool "(" (Bool (Set (Set F4 "(" ")" ) ($#k3_funct_2 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set F2 "(" ")" )) & (Bool (Set (Set F4 "(" ")" ) ($#k3_funct_2 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set F3 "(" ")" )) ")" ) and (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set F4 "(" ")" ) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 2) ")" )) ($#r1_hidden :::"="::: ) (Set F6 "(" (Set (Var "n")) "," (Set "(" (Set F4 "(" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "n")) ")" ) "," (Set "(" (Set F4 "(" ")" ) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ")" ))) and (Bool "(" (Bool (Set (Set F5 "(" ")" ) ($#k3_funct_2 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set F2 "(" ")" )) & (Bool (Set (Set F5 "(" ")" ) ($#k3_funct_2 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set F3 "(" ")" )) ")" ) and (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set F5 "(" ")" ) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 2) ")" )) ($#r1_hidden :::"="::: ) (Set F6 "(" (Set (Var "n")) "," (Set "(" (Set F5 "(" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "n")) ")" ) "," (Set "(" (Set F5 "(" ")" ) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ")" ))) proof end; scheme :: RECDEF_2:sch 8 LambdaRec3Ex{ F1() -> ($#m1_hidden :::"set"::: ) , F2() -> ($#m1_hidden :::"set"::: ) , F3() -> ($#m1_hidden :::"set"::: ) , F4( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#m1_hidden :::"set"::: ) } : (Bool "ex" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "st" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k5_numbers :::"NAT"::: ) )) & (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set F1 "(" ")" )) & (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set F2 "(" ")" )) & (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Num 2)) ($#r1_hidden :::"="::: ) (Set F3 "(" ")" )) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 3) ")" )) ($#r1_hidden :::"="::: ) (Set F4 "(" (Set (Var "n")) "," (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")) ")" ) "," (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) "," (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 2) ")" ) ")" ) ")" )) ")" ) ")" )) proof end; scheme :: RECDEF_2:sch 9 LambdaRec3ExD{ F1() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , F2() -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ), F3() -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ), F4() -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ), F5( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) } : (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set F1 "(" ")" ) "st" (Bool "(" (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set F2 "(" ")" )) & (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set F3 "(" ")" )) & (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Num 2)) ($#r1_hidden :::"="::: ) (Set F4 "(" ")" )) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 3) ")" )) ($#r1_hidden :::"="::: ) (Set F5 "(" (Set (Var "n")) "," (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "n")) ")" ) "," (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) "," (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 2) ")" ) ")" ) ")" )) ")" ) ")" )) proof end; scheme :: RECDEF_2:sch 10 LambdaRec3Un{ F1() -> ($#m1_hidden :::"set"::: ) , F2() -> ($#m1_hidden :::"set"::: ) , F3() -> ($#m1_hidden :::"set"::: ) , F4() -> ($#m1_hidden :::"Function":::), F5() -> ($#m1_hidden :::"Function":::), F6( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#m1_hidden :::"set"::: ) } : (Bool (Set F4 "(" ")" ) ($#r1_hidden :::"="::: ) (Set F5 "(" ")" )) provided (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set F4 "(" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k5_numbers :::"NAT"::: ) )) and (Bool "(" (Bool (Set (Set F4 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set F1 "(" ")" )) & (Bool (Set (Set F4 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set F2 "(" ")" )) & (Bool (Set (Set F4 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Num 2)) ($#r1_hidden :::"="::: ) (Set F3 "(" ")" )) ")" ) and (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set F4 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 3) ")" )) ($#r1_hidden :::"="::: ) (Set F6 "(" (Set (Var "n")) "," (Set "(" (Set F4 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "n")) ")" ) "," (Set "(" (Set F4 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) "," (Set "(" (Set F4 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 2) ")" ) ")" ) ")" ))) and (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set F5 "(" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k5_numbers :::"NAT"::: ) )) and (Bool "(" (Bool (Set (Set F5 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set F1 "(" ")" )) & (Bool (Set (Set F5 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set F2 "(" ")" )) & (Bool (Set (Set F5 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Num 2)) ($#r1_hidden :::"="::: ) (Set F3 "(" ")" )) ")" ) and (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set F5 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 3) ")" )) ($#r1_hidden :::"="::: ) (Set F6 "(" (Set (Var "n")) "," (Set "(" (Set F5 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "n")) ")" ) "," (Set "(" (Set F5 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) "," (Set "(" (Set F5 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 2) ")" ) ")" ) ")" ))) proof end; scheme :: RECDEF_2:sch 11 LambdaRec3UnD{ F1() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , F2() -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ), F3() -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ), F4() -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ), F5() -> ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set F1 "(" ")" ), F6() -> ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set F1 "(" ")" ), F7( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) } : (Bool (Set F5 "(" ")" ) ($#r2_funct_2 :::"="::: ) (Set F6 "(" ")" )) provided (Bool "(" (Bool (Set (Set F5 "(" ")" ) ($#k3_funct_2 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set F2 "(" ")" )) & (Bool (Set (Set F5 "(" ")" ) ($#k3_funct_2 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set F3 "(" ")" )) & (Bool (Set (Set F5 "(" ")" ) ($#k3_funct_2 :::"."::: ) (Num 2)) ($#r1_hidden :::"="::: ) (Set F4 "(" ")" )) ")" ) and (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set F5 "(" ")" ) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 3) ")" )) ($#r1_hidden :::"="::: ) (Set F7 "(" (Set (Var "n")) "," (Set "(" (Set F5 "(" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "n")) ")" ) "," (Set "(" (Set F5 "(" ")" ) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) "," (Set "(" (Set F5 "(" ")" ) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 2) ")" ) ")" ) ")" ))) and (Bool "(" (Bool (Set (Set F6 "(" ")" ) ($#k3_funct_2 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set F2 "(" ")" )) & (Bool (Set (Set F6 "(" ")" ) ($#k3_funct_2 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set F3 "(" ")" )) & (Bool (Set (Set F6 "(" ")" ) ($#k3_funct_2 :::"."::: ) (Num 2)) ($#r1_hidden :::"="::: ) (Set F4 "(" ")" )) ")" ) and (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set F6 "(" ")" ) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 3) ")" )) ($#r1_hidden :::"="::: ) (Set F7 "(" (Set (Var "n")) "," (Set "(" (Set F6 "(" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "n")) ")" ) "," (Set "(" (Set F6 "(" ")" ) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) "," (Set "(" (Set F6 "(" ")" ) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 2) ")" ) ")" ) ")" ))) proof end; scheme :: RECDEF_2:sch 12 LambdaRec4Un{ F1() -> ($#m1_hidden :::"set"::: ) , F2() -> ($#m1_hidden :::"set"::: ) , F3() -> ($#m1_hidden :::"set"::: ) , F4() -> ($#m1_hidden :::"set"::: ) , F5() -> ($#m1_hidden :::"Function":::), F6() -> ($#m1_hidden :::"Function":::), F7( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#m1_hidden :::"set"::: ) } : (Bool (Set F5 "(" ")" ) ($#r1_hidden :::"="::: ) (Set F6 "(" ")" )) provided (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set F5 "(" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k5_numbers :::"NAT"::: ) )) and (Bool "(" (Bool (Set (Set F5 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set F1 "(" ")" )) & (Bool (Set (Set F5 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set F2 "(" ")" )) & (Bool (Set (Set F5 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Num 2)) ($#r1_hidden :::"="::: ) (Set F3 "(" ")" )) & (Bool (Set (Set F5 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Num 3)) ($#r1_hidden :::"="::: ) (Set F4 "(" ")" )) ")" ) and (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set F5 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 4) ")" )) ($#r1_hidden :::"="::: ) (Set F7 "(" (Set (Var "n")) "," (Set "(" (Set F5 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "n")) ")" ) "," (Set "(" (Set F5 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) "," (Set "(" (Set F5 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 2) ")" ) ")" ) "," (Set "(" (Set F5 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 3) ")" ) ")" ) ")" ))) and (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set F6 "(" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k5_numbers :::"NAT"::: ) )) and (Bool "(" (Bool (Set (Set F6 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set F1 "(" ")" )) & (Bool (Set (Set F6 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set F2 "(" ")" )) & (Bool (Set (Set F6 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Num 2)) ($#r1_hidden :::"="::: ) (Set F3 "(" ")" )) & (Bool (Set (Set F6 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Num 3)) ($#r1_hidden :::"="::: ) (Set F4 "(" ")" )) ")" ) and (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set F6 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 4) ")" )) ($#r1_hidden :::"="::: ) (Set F7 "(" (Set (Var "n")) "," (Set "(" (Set F6 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "n")) ")" ) "," (Set "(" (Set F6 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) "," (Set "(" (Set F6 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 2) ")" ) ")" ) "," (Set "(" (Set F6 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 3) ")" ) ")" ) ")" ))) proof end; scheme :: RECDEF_2:sch 13 LambdaRec4UnD{ F1() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , F2() -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ), F3() -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ), F4() -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ), F5() -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ), F6() -> ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set F1 "(" ")" ), F7() -> ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set F1 "(" ")" ), F8( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) } : (Bool (Set F6 "(" ")" ) ($#r2_funct_2 :::"="::: ) (Set F7 "(" ")" )) provided (Bool "(" (Bool (Set (Set F6 "(" ")" ) ($#k3_funct_2 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set F2 "(" ")" )) & (Bool (Set (Set F6 "(" ")" ) ($#k3_funct_2 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set F3 "(" ")" )) & (Bool (Set (Set F6 "(" ")" ) ($#k3_funct_2 :::"."::: ) (Num 2)) ($#r1_hidden :::"="::: ) (Set F4 "(" ")" )) & (Bool (Set (Set F6 "(" ")" ) ($#k3_funct_2 :::"."::: ) (Num 3)) ($#r1_hidden :::"="::: ) (Set F5 "(" ")" )) ")" ) and (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set F6 "(" ")" ) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 4) ")" )) ($#r1_hidden :::"="::: ) (Set F8 "(" (Set (Var "n")) "," (Set "(" (Set F6 "(" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "n")) ")" ) "," (Set "(" (Set F6 "(" ")" ) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) "," (Set "(" (Set F6 "(" ")" ) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 2) ")" ) ")" ) "," (Set "(" (Set F6 "(" ")" ) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 3) ")" ) ")" ) ")" ))) and (Bool "(" (Bool (Set (Set F7 "(" ")" ) ($#k3_funct_2 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set F2 "(" ")" )) & (Bool (Set (Set F7 "(" ")" ) ($#k3_funct_2 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set F3 "(" ")" )) & (Bool (Set (Set F7 "(" ")" ) ($#k3_funct_2 :::"."::: ) (Num 2)) ($#r1_hidden :::"="::: ) (Set F4 "(" ")" )) & (Bool (Set (Set F7 "(" ")" ) ($#k3_funct_2 :::"."::: ) (Num 3)) ($#r1_hidden :::"="::: ) (Set F5 "(" ")" )) ")" ) and (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set F7 "(" ")" ) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 4) ")" )) ($#r1_hidden :::"="::: ) (Set F8 "(" (Set (Var "n")) "," (Set "(" (Set F7 "(" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "n")) ")" ) "," (Set "(" (Set F7 "(" ")" ) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) "," (Set "(" (Set F7 "(" ")" ) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 2) ")" ) ")" ) "," (Set "(" (Set F7 "(" ")" ) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 3) ")" ) ")" ) ")" ))) proof end; begin theorem :: RECDEF_2:10 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Set (Var "x")) ($#k4_xtuple_0 :::"`1_3"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "y")) ($#k4_xtuple_0 :::"`1_3"::: ) )) & (Bool (Set (Set (Var "x")) ($#k5_xtuple_0 :::"`2_3"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "y")) ($#k5_xtuple_0 :::"`2_3"::: ) )) & (Bool (Set (Set (Var "x")) ($#k2_xtuple_0 :::"`3_3"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "y")) ($#k2_xtuple_0 :::"`3_3"::: ) )) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k3_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) ($#k3_zfmisc_1 :::":]"::: ) )) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k3_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) ($#k3_zfmisc_1 :::":]"::: ) ))) "holds" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "y")))) ;