:: COMPUT_1 semantic presentation begin theorem :: COMPUT_1:1 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k10_finseq_1 :::"*>"::: ) ) ($#k2_funct_7 :::"+*"::: ) "(" (Num 1) "," (Set (Var "z")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "z")) "," (Set (Var "y")) ($#k10_finseq_1 :::"*>"::: ) )) & (Bool (Set (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k10_finseq_1 :::"*>"::: ) ) ($#k2_funct_7 :::"+*"::: ) "(" (Num 2) "," (Set (Var "z")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "z")) ($#k10_finseq_1 :::"*>"::: ) )) ")" )) ; theorem :: COMPUT_1:2 (Bool "for" (Set (Var "a")) "," (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Set (Var "f")) ($#k2_funct_7 :::"+*"::: ) "(" (Set (Var "a")) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k2_funct_7 :::"+*"::: ) "(" (Set (Var "a")) "," (Set (Var "y")) ")" ))) "holds" (Bool (Set (Set (Var "f")) ($#k2_funct_7 :::"+*"::: ) "(" (Set (Var "a")) "," (Set (Var "z")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k2_funct_7 :::"+*"::: ) "(" (Set (Var "a")) "," (Set (Var "z")) ")" )))) ; theorem :: COMPUT_1:3 (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"FinSequence":::) "holds" (Bool (Set ($#k2_finseq_3 :::"Del"::: ) "(" (Set "(" (Set (Var "p")) ($#k2_funct_7 :::"+*"::: ) "(" (Set (Var "i")) "," (Set (Var "x")) ")" ")" ) "," (Set (Var "i")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k2_finseq_3 :::"Del"::: ) "(" (Set (Var "p")) "," (Set (Var "i")) ")" ))))) ; theorem :: COMPUT_1:4 (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set (Set (Var "p")) ($#k2_funct_7 :::"+*"::: ) "(" (Set (Var "i")) "," (Set (Var "a")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "q")) ($#k2_funct_7 :::"+*"::: ) "(" (Set (Var "i")) "," (Set (Var "a")) ")" ))) "holds" (Bool (Set ($#k2_finseq_3 :::"Del"::: ) "(" (Set (Var "p")) "," (Set (Var "i")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k2_finseq_3 :::"Del"::: ) "(" (Set (Var "q")) "," (Set (Var "i")) ")" ))))) ; theorem :: COMPUT_1:5 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set ($#k6_numbers :::"0"::: ) ) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) ))) ; theorem :: COMPUT_1:6 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "n")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set (Var "n")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) ; theorem :: COMPUT_1:7 (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "f"))))) "holds" (Bool (Set ($#k6_funct_6 :::"<:"::: ) (Set (Var "f")) ($#k6_funct_6 :::":>"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) ; theorem :: COMPUT_1:8 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Var "D")))) "holds" (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set ($#k6_funct_6 :::"<:"::: ) (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "f")) ($#k9_finseq_1 :::"*>"::: ) ) ($#k6_funct_6 :::":>"::: ) )) ($#r1_hidden :::"="::: ) (Set (Num 1) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set (Var "D")))))) ; theorem :: COMPUT_1:9 (Bool "for" (Set (Var "i")) "," (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1)))) "holds" (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set (Var "D"))) "holds" (Bool (Set ($#k2_finseq_3 :::"Del"::: ) "(" (Set (Var "p")) "," (Set (Var "i")) ")" ) ($#r2_hidden :::"in"::: ) (Set (Set (Var "n")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set (Var "D"))))))) ; theorem :: COMPUT_1:10 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Y")) "being" ($#m1_finseq_2 :::"FinSequenceSet"::: ) "of" (Set (Var "X")) "holds" (Bool (Set (Var "Y")) ($#r1_tarski :::"c="::: ) (Set (Set (Var "X")) ($#k3_finseq_2 :::"*"::: ) )))) ; begin definitionlet "X" be ($#m1_hidden :::"set"::: ) ; attr "X" is :::"compatible"::: means :: COMPUT_1:def 1 (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) "X") & (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) "X")) "holds" (Bool (Set (Var "f")) ($#r1_partfun1 :::"tolerates"::: ) (Set (Var "g")))); end; :: deftheorem defines :::"compatible"::: COMPUT_1:def 1 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "X")) "is" ($#v1_comput_1 :::"compatible"::: ) ) "iff" (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set (Var "f")) ($#r1_partfun1 :::"tolerates"::: ) (Set (Var "g")))) ")" )); registration cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v4_funct_1 :::"functional"::: ) ($#v1_comput_1 :::"compatible"::: ) for ($#m1_hidden :::"set"::: ) ; end; registrationlet "X" be ($#v4_funct_1 :::"functional"::: ) ($#v1_comput_1 :::"compatible"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k3_tarski :::"union"::: ) "X") -> ($#v1_relat_1 :::"Relation-like"::: ) ($#v1_funct_1 :::"Function-like"::: ) ; end; theorem :: COMPUT_1:11 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool "(" (Bool (Set (Var "X")) "is" ($#v4_funct_1 :::"functional"::: ) ) & (Bool (Set (Var "X")) "is" ($#v1_comput_1 :::"compatible"::: ) ) ")" ) "iff" (Bool (Set ($#k3_tarski :::"union"::: ) (Set (Var "X"))) "is" ($#m1_hidden :::"Function":::)) ")" )) ; registrationlet "X", "Y" be ($#m1_hidden :::"set"::: ) ; cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_comput_1 :::"compatible"::: ) for ($#m1_rfunct_3 :::"PartFunc-set"::: ) "of" "X" "," "Y"; end; theorem :: COMPUT_1:12 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v4_funct_1 :::"functional"::: ) ($#v1_comput_1 :::"compatible"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k3_tarski :::"union"::: ) (Set (Var "X")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_tarski :::"union"::: ) "{" (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")) ")" ) where f "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) : (Bool verum) "}" ))) ; theorem :: COMPUT_1:13 (Bool "for" (Set (Var "X")) "being" ($#v4_funct_1 :::"functional"::: ) ($#v1_comput_1 :::"compatible"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))) ($#r1_tarski :::"c="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k3_tarski :::"union"::: ) (Set (Var "X")) ")" ))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set "(" ($#k3_tarski :::"union"::: ) (Set (Var "X")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")))) ")" ) ")" ))) ; theorem :: COMPUT_1:14 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v4_funct_1 :::"functional"::: ) ($#v1_comput_1 :::"compatible"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" ($#k3_tarski :::"union"::: ) (Set (Var "X")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_tarski :::"union"::: ) "{" (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "f")) ")" ) where f "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) : (Bool verum) "}" ))) ; registrationlet "X", "Y" be ($#m1_hidden :::"set"::: ) ; cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) -> ($#v4_funct_1 :::"functional"::: ) for ($#m1_rfunct_3 :::"PartFunc-set"::: ) "of" "X" "," "Y"; end; theorem :: COMPUT_1:15 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "P")) "being" ($#v1_comput_1 :::"compatible"::: ) ($#m1_rfunct_3 :::"PFUNC_DOMAIN":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "holds" (Bool (Set ($#k3_tarski :::"union"::: ) (Set (Var "P"))) "is" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set (Var "Y"))))) ; begin notationlet "f" be ($#m1_hidden :::"Relation":::); synonym :::"to-naturals"::: "f" for :::"natural-valued"::: ; end; registration cluster ($#v1_relat_1 :::"Relation-like"::: ) (Set (Set ($#k5_numbers :::"NAT"::: ) ) ($#k3_finseq_2 :::"*"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v4_valued_0 :::"to-naturals"::: ) for ($#m1_hidden :::"set"::: ) ; end; definitionlet "f" be (Set (Set ($#k5_numbers :::"NAT"::: ) ) ($#k3_finseq_2 :::"*"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ($#m1_hidden :::"Relation":::); attr "f" is :::"len-total"::: means :: COMPUT_1:def 2 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "y")))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) "f"))) "holds" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) "f"))); end; :: deftheorem defines :::"len-total"::: COMPUT_1:def 2 : (Bool "for" (Set (Var "f")) "being" (Set (Set ($#k5_numbers :::"NAT"::: ) ) ($#k3_finseq_2 :::"*"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ($#m1_hidden :::"Relation":::) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v2_comput_1 :::"len-total"::: ) ) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "y")))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f"))))) ")" )); theorem :: COMPUT_1:16 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "st" (Bool (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "R"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "n")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set (Var "D"))))) "holds" (Bool (Set (Var "R")) "is" ($#v2_margrel1 :::"homogeneous"::: ) )))) ; registration cluster ($#v1_xboole_0 :::"empty"::: ) ($#v1_relat_1 :::"Relation-like"::: ) -> ($#v2_margrel1 :::"homogeneous"::: ) for ($#m1_hidden :::"set"::: ) ; end; registrationlet "p" be ($#m1_hidden :::"FinSequence":::); let "x" be ($#m1_hidden :::"set"::: ) ; cluster (Set "p" ($#k16_funcop_1 :::".-->"::: ) "x") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_margrel1 :::"homogeneous"::: ) ; end; registration cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_relat_1 :::"Relation-like"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v2_margrel1 :::"homogeneous"::: ) for ($#m1_hidden :::"set"::: ) ; end; registrationlet "f" be ($#v2_margrel1 :::"homogeneous"::: ) ($#m1_hidden :::"Function":::); let "g" be ($#m1_hidden :::"Function":::); cluster (Set "f" ($#k3_relat_1 :::"*"::: ) "g") -> ($#v2_margrel1 :::"homogeneous"::: ) ; end; registrationlet "X", "Y" be ($#m1_hidden :::"set"::: ) ; cluster ($#v1_relat_1 :::"Relation-like"::: ) (Set "X" ($#k3_finseq_2 :::"*"::: ) ) ($#v4_relat_1 :::"-defined"::: ) "Y" ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v2_margrel1 :::"homogeneous"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set bbbadK1_ZFMISC_1((Set bbbadK2_ZFMISC_1((Set "(" "X" ($#k3_finseq_2 :::"*"::: ) ")" ) "," "Y")))); end; registrationlet "X", "Y" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_relat_1 :::"Relation-like"::: ) (Set "X" ($#k3_finseq_2 :::"*"::: ) ) ($#v4_relat_1 :::"-defined"::: ) "Y" ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v2_margrel1 :::"homogeneous"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set bbbadK1_ZFMISC_1((Set bbbadK2_ZFMISC_1((Set "(" "X" ($#k3_finseq_2 :::"*"::: ) ")" ) "," "Y")))); end; registrationlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_relat_1 :::"Relation-like"::: ) (Set "X" ($#k3_finseq_2 :::"*"::: ) ) ($#v4_relat_1 :::"-defined"::: ) "X" ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v2_margrel1 :::"homogeneous"::: ) ($#v3_margrel1 :::"quasi_total"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set bbbadK1_ZFMISC_1((Set bbbadK2_ZFMISC_1((Set "(" "X" ($#k3_finseq_2 :::"*"::: ) ")" ) "," "X")))); end; registration cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_relat_1 :::"Relation-like"::: ) (Set (Set ($#k5_numbers :::"NAT"::: ) ) ($#k3_finseq_2 :::"*"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v4_valued_0 :::"to-naturals"::: ) ($#v2_margrel1 :::"homogeneous"::: ) ($#v2_comput_1 :::"len-total"::: ) for ($#m1_hidden :::"set"::: ) ; end; registration cluster ($#v1_funct_1 :::"Function-like"::: ) -> (Set (Set ($#k5_numbers :::"NAT"::: ) ) ($#k3_finseq_2 :::"*"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ($#v4_valued_0 :::"to-naturals"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set bbbadK1_ZFMISC_1((Set bbbadK2_ZFMISC_1((Set "(" (Set ($#k5_numbers :::"NAT"::: ) ) ($#k3_finseq_2 :::"*"::: ) ")" ) "," (Set ($#k5_numbers :::"NAT"::: ) ))))); end; registration cluster ($#v1_funct_1 :::"Function-like"::: ) ($#v3_margrel1 :::"quasi_total"::: ) -> ($#v2_comput_1 :::"len-total"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set bbbadK1_ZFMISC_1((Set bbbadK2_ZFMISC_1((Set "(" (Set ($#k5_numbers :::"NAT"::: ) ) ($#k3_finseq_2 :::"*"::: ) ")" ) "," (Set ($#k5_numbers :::"NAT"::: ) ))))); end; theorem :: COMPUT_1:17 (Bool "for" (Set (Var "g")) "being" (Set (Set ($#k5_numbers :::"NAT"::: ) ) ($#k3_finseq_2 :::"*"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ($#v4_valued_0 :::"to-naturals"::: ) ($#v2_comput_1 :::"len-total"::: ) ($#m1_hidden :::"Function":::) "holds" (Bool (Set (Var "g")) "is" ($#v3_margrel1 :::"quasi_total"::: ) ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" (Set ($#k5_numbers :::"NAT"::: ) ) ($#k3_finseq_2 :::"*"::: ) ")" ) "," (Set ($#k5_numbers :::"NAT"::: ) ))) ; theorem :: COMPUT_1:18 (Bool (Set ($#k19_margrel1 :::"arity"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ; theorem :: COMPUT_1:19 (Bool "for" (Set (Var "f")) "being" ($#v2_margrel1 :::"homogeneous"::: ) ($#m1_hidden :::"Relation":::) "st" (Bool (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) ))) "holds" (Bool (Set ($#k18_margrel1 :::"arity"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) ; theorem :: COMPUT_1:20 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#v2_margrel1 :::"homogeneous"::: ) ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" (Set (Var "X")) ($#k3_finseq_2 :::"*"::: ) ")" ) "," (Set (Var "Y")) "holds" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f"))) ($#r1_tarski :::"c="::: ) (Set (Set "(" ($#k19_margrel1 :::"arity"::: ) (Set (Var "f")) ")" ) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set (Var "X")))))) ; theorem :: COMPUT_1:21 (Bool "for" (Set (Var "f")) "being" (Set (Set ($#k5_numbers :::"NAT"::: ) ) ($#k3_finseq_2 :::"*"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ($#v2_margrel1 :::"homogeneous"::: ) ($#m1_hidden :::"Function":::) "holds" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f"))) ($#r1_tarski :::"c="::: ) (Set (Set "(" ($#k19_margrel1 :::"arity"::: ) (Set (Var "f")) ")" ) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k5_numbers :::"NAT"::: ) )))) ; theorem :: COMPUT_1:22 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#v2_margrel1 :::"homogeneous"::: ) ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" (Set (Var "X")) ($#k3_finseq_2 :::"*"::: ) ")" ) "," (Set (Var "X")) "holds" (Bool "(" (Bool "(" (Bool (Set (Var "f")) "is" ($#v3_margrel1 :::"quasi_total"::: ) ) & (Bool (Bool "not" (Set (Var "f")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" ) "iff" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k19_margrel1 :::"arity"::: ) (Set (Var "f")) ")" ) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set (Var "X")))) ")" ))) ; theorem :: COMPUT_1:23 (Bool "for" (Set (Var "f")) "being" (Set (Set ($#k5_numbers :::"NAT"::: ) ) ($#k3_finseq_2 :::"*"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ($#v4_valued_0 :::"to-naturals"::: ) ($#v2_margrel1 :::"homogeneous"::: ) ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool "(" (Bool (Set (Var "f")) "is" ($#v2_comput_1 :::"len-total"::: ) ) & (Bool (Bool "not" (Set (Var "f")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" ) "iff" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k19_margrel1 :::"arity"::: ) (Set (Var "f")) ")" ) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k5_numbers :::"NAT"::: ) ))) ")" )) ; theorem :: COMPUT_1:24 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_margrel1 :::"homogeneous"::: ) ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" (Set (Var "D")) ($#k3_finseq_2 :::"*"::: ) ")" ) "," (Set (Var "D")) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "n")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set (Var "D"))))) "holds" (Bool (Set ($#k19_margrel1 :::"arity"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Var "n")))))) ; theorem :: COMPUT_1:25 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#v2_margrel1 :::"homogeneous"::: ) ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" (Set (Var "D")) ($#k3_finseq_2 :::"*"::: ) ")" ) "," (Set (Var "D")) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "n")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set (Var "D"))))) "holds" (Bool (Set ($#k19_margrel1 :::"arity"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Var "n")))))) ; definitionlet "R" be ($#m1_hidden :::"Relation":::); attr "R" is :::"with_the_same_arity"::: means :: COMPUT_1:def 3 (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) "R")) & (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) "R"))) "holds" (Bool "(" (Bool "(" "not" (Bool (Set (Var "f")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" (Bool (Set (Var "g")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) )) ")" ) & "(" (Bool (Bool (Bool "not" (Set (Var "f")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Bool "not" (Set (Var "g")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "ex" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) )(Bool "ex" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "n")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set (Var "X")))) & (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "g"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "n")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set (Var "X")))) ")" ))) ")" ")" )); end; :: deftheorem defines :::"with_the_same_arity"::: COMPUT_1:def 3 : (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool "(" (Bool (Set (Var "R")) "is" ($#v3_comput_1 :::"with_the_same_arity"::: ) ) "iff" (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "R")))) & (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "R"))))) "holds" (Bool "(" (Bool "(" "not" (Bool (Set (Var "f")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" (Bool (Set (Var "g")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) )) ")" ) & "(" (Bool (Bool (Bool "not" (Set (Var "f")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Bool "not" (Set (Var "g")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "ex" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) )(Bool "ex" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "n")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set (Var "X")))) & (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "g"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "n")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set (Var "X")))) ")" ))) ")" ")" )) ")" )); registration cluster ($#v1_xboole_0 :::"empty"::: ) ($#v1_relat_1 :::"Relation-like"::: ) -> ($#v3_comput_1 :::"with_the_same_arity"::: ) for ($#m1_hidden :::"set"::: ) ; end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; cluster ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) "X" ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_finset_1 :::"finite"::: ) ($#v4_card_3 :::"countable"::: ) ($#v1_finseq_1 :::"FinSequence-like"::: ) ($#v2_finseq_1 :::"FinSubsequence-like"::: ) ($#v3_comput_1 :::"with_the_same_arity"::: ) for ($#m1_finseq_1 :::"FinSequence"::: ) "of" "X"; cluster ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) "X" ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_finset_1 :::"finite"::: ) ($#v4_card_3 :::"countable"::: ) ($#v1_finseq_1 :::"FinSequence-like"::: ) ($#v2_finseq_1 :::"FinSubsequence-like"::: ) ($#v3_comput_1 :::"with_the_same_arity"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set "X" ($#k3_finseq_2 :::"*"::: ) ); end; definitionlet "F" be ($#v3_comput_1 :::"with_the_same_arity"::: ) ($#m1_hidden :::"Relation":::); func :::"arity"::: "F" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) means :: COMPUT_1:def 4 (Bool "for" (Set (Var "f")) "being" ($#v2_margrel1 :::"homogeneous"::: ) ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) "F"))) "holds" (Bool it ($#r1_hidden :::"="::: ) (Set ($#k19_margrel1 :::"arity"::: ) (Set (Var "f"))))) if (Bool "ex" (Set (Var "f")) "being" ($#v2_margrel1 :::"homogeneous"::: ) ($#m1_hidden :::"Function":::) "st" (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) "F"))) otherwise (Bool it ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )); end; :: deftheorem defines :::"arity"::: COMPUT_1:def 4 : (Bool "for" (Set (Var "F")) "being" ($#v3_comput_1 :::"with_the_same_arity"::: ) ($#m1_hidden :::"Relation":::) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" "(" (Bool (Bool "ex" (Set (Var "f")) "being" ($#v2_margrel1 :::"homogeneous"::: ) ($#m1_hidden :::"Function":::) "st" (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "F")))))) "implies" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k1_comput_1 :::"arity"::: ) (Set (Var "F")))) "iff" (Bool "for" (Set (Var "f")) "being" ($#v2_margrel1 :::"homogeneous"::: ) ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "F"))))) "holds" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k19_margrel1 :::"arity"::: ) (Set (Var "f"))))) ")" ) ")" & "(" (Bool (Bool "(" "for" (Set (Var "f")) "being" ($#v2_margrel1 :::"homogeneous"::: ) ($#m1_hidden :::"Function":::) "holds" (Bool (Bool "not" (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "F"))))) ")" )) "implies" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k1_comput_1 :::"arity"::: ) (Set (Var "F")))) "iff" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ) ")" ")" ))); theorem :: COMPUT_1:26 (Bool "for" (Set (Var "F")) "being" ($#v3_comput_1 :::"with_the_same_arity"::: ) ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set ($#k1_comput_1 :::"arity"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) ; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; func :::"HFuncs"::: "X" -> ($#m1_rfunct_3 :::"PFUNC_DOMAIN":::) "of" (Set "X" ($#k3_finseq_2 :::"*"::: ) ) "," "X" equals :: COMPUT_1:def 5 "{" (Set (Var "f")) where f "is" ($#m2_rfunct_3 :::"Element"::: ) "of" (Set ($#k3_rfunct_3 :::"PFuncs"::: ) "(" (Set "(" "X" ($#k3_finseq_2 :::"*"::: ) ")" ) "," "X" ")" ) : (Bool (Set (Var "f")) "is" ($#v2_margrel1 :::"homogeneous"::: ) ) "}" ; end; :: deftheorem defines :::"HFuncs"::: COMPUT_1:def 5 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k2_comput_1 :::"HFuncs"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) "{" (Set (Var "f")) where f "is" ($#m2_rfunct_3 :::"Element"::: ) "of" (Set ($#k3_rfunct_3 :::"PFuncs"::: ) "(" (Set "(" (Set (Var "X")) ($#k3_finseq_2 :::"*"::: ) ")" ) "," (Set (Var "X")) ")" ) : (Bool (Set (Var "f")) "is" ($#v2_margrel1 :::"homogeneous"::: ) ) "}" )); theorem :: COMPUT_1:27 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_comput_1 :::"HFuncs"::: ) (Set (Var "X"))))) ; registrationlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_relat_1 :::"Relation-like"::: ) (Set "X" ($#k3_finseq_2 :::"*"::: ) ) ($#v4_relat_1 :::"-defined"::: ) "X" ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v2_margrel1 :::"homogeneous"::: ) ($#v3_margrel1 :::"quasi_total"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_comput_1 :::"HFuncs"::: ) "X"); end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; cluster -> ($#v2_margrel1 :::"homogeneous"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_comput_1 :::"HFuncs"::: ) "X"); end; registrationlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "S" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k2_comput_1 :::"HFuncs"::: ) (Set (Const "X")) ")" ); cluster -> ($#v2_margrel1 :::"homogeneous"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" "S"; end; theorem :: COMPUT_1:28 (Bool "for" (Set (Var "f")) "being" (Set (Set ($#k5_numbers :::"NAT"::: ) ) ($#k3_finseq_2 :::"*"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ($#v4_valued_0 :::"to-naturals"::: ) ($#v2_margrel1 :::"homogeneous"::: ) ($#m1_hidden :::"Function":::) "holds" (Bool (Set (Var "f")) "is" ($#m2_rfunct_3 :::"Element"::: ) "of" (Set ($#k2_comput_1 :::"HFuncs"::: ) (Set ($#k5_numbers :::"NAT"::: ) )))) ; theorem :: COMPUT_1:29 (Bool "for" (Set (Var "f")) "being" (Set (Set ($#k5_numbers :::"NAT"::: ) ) ($#k3_finseq_2 :::"*"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ($#v4_valued_0 :::"to-naturals"::: ) ($#v2_margrel1 :::"homogeneous"::: ) ($#v2_comput_1 :::"len-total"::: ) ($#m1_hidden :::"Function":::) "holds" (Bool (Set (Var "f")) "is" ($#v3_margrel1 :::"quasi_total"::: ) ($#m2_rfunct_3 :::"Element"::: ) "of" (Set ($#k2_comput_1 :::"HFuncs"::: ) (Set ($#k5_numbers :::"NAT"::: ) )))) ; theorem :: COMPUT_1:30 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_hidden :::"Relation":::) "st" (Bool (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "F"))) ($#r1_tarski :::"c="::: ) (Set ($#k2_comput_1 :::"HFuncs"::: ) (Set (Var "X")))) & (Bool "(" "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#v2_margrel1 :::"homogeneous"::: ) ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "F")))) & (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "F"))))) "holds" (Bool (Set ($#k19_margrel1 :::"arity"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k19_margrel1 :::"arity"::: ) (Set (Var "g")))) ")" )) "holds" (Bool (Set (Var "F")) "is" ($#v3_comput_1 :::"with_the_same_arity"::: ) ))) ; definitionlet "n", "m" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); func "n" :::"const"::: "m" -> (Set (Set ($#k5_numbers :::"NAT"::: ) ) ($#k3_finseq_2 :::"*"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ($#v4_valued_0 :::"to-naturals"::: ) ($#v2_margrel1 :::"homogeneous"::: ) ($#m1_hidden :::"Function":::) equals :: COMPUT_1:def 6 (Set (Set "(" "n" ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ")" ) ($#k8_funcop_1 :::"-->"::: ) "m"); end; :: deftheorem defines :::"const"::: COMPUT_1:def 6 : (Bool "for" (Set (Var "n")) "," (Set (Var "m")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "n")) ($#k3_comput_1 :::"const"::: ) (Set (Var "m"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "n")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ")" ) ($#k8_funcop_1 :::"-->"::: ) (Set (Var "m"))))); theorem :: COMPUT_1:31 (Bool "for" (Set (Var "n")) "," (Set (Var "m")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "n")) ($#k3_comput_1 :::"const"::: ) (Set (Var "m"))) ($#r2_hidden :::"in"::: ) (Set ($#k2_comput_1 :::"HFuncs"::: ) (Set ($#k5_numbers :::"NAT"::: ) )))) ; registrationlet "n", "m" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); cluster (Set "n" ($#k3_comput_1 :::"const"::: ) "m") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) (Set (Set ($#k5_numbers :::"NAT"::: ) ) ($#k3_finseq_2 :::"*"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ($#v4_valued_0 :::"to-naturals"::: ) ($#v2_margrel1 :::"homogeneous"::: ) ($#v2_comput_1 :::"len-total"::: ) ; end; theorem :: COMPUT_1:32 (Bool "for" (Set (Var "n")) "," (Set (Var "m")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k19_margrel1 :::"arity"::: ) (Set "(" (Set (Var "n")) ($#k3_comput_1 :::"const"::: ) (Set (Var "m")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "n")))) ; registration cluster -> (Set (Set ($#k5_numbers :::"NAT"::: ) ) ($#k3_finseq_2 :::"*"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ($#v4_valued_0 :::"to-naturals"::: ) ($#v2_margrel1 :::"homogeneous"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_comput_1 :::"HFuncs"::: ) (Set ($#k5_numbers :::"NAT"::: ) )); end; definitionlet "n", "i" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); func "n" :::"succ"::: "i" -> (Set (Set ($#k5_numbers :::"NAT"::: ) ) ($#k3_finseq_2 :::"*"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ($#v4_valued_0 :::"to-naturals"::: ) ($#v2_margrel1 :::"homogeneous"::: ) ($#m1_hidden :::"Function":::) means :: COMPUT_1:def 7 (Bool "(" (Bool (Set ($#k1_relset_1 :::"dom"::: ) it) ($#r1_hidden :::"="::: ) (Set "n" ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k5_numbers :::"NAT"::: ) ))) & (Bool "(" "for" (Set (Var "p")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set "n" ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k5_numbers :::"NAT"::: ) )) "holds" (Bool (Set it ($#k1_recdef_1 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "p")) ($#k7_partfun1 :::"/."::: ) "i" ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1))) ")" ) ")" ); end; :: deftheorem defines :::"succ"::: COMPUT_1:def 7 : (Bool "for" (Set (Var "n")) "," (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "b3")) "being" (Set (Set ($#k5_numbers :::"NAT"::: ) ) ($#k3_finseq_2 :::"*"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ($#v4_valued_0 :::"to-naturals"::: ) ($#v2_margrel1 :::"homogeneous"::: ) ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "n")) ($#k4_comput_1 :::"succ"::: ) (Set (Var "i")))) "iff" (Bool "(" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "b3"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "n")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k5_numbers :::"NAT"::: ) ))) & (Bool "(" "for" (Set (Var "p")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set (Var "n")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k5_numbers :::"NAT"::: ) )) "holds" (Bool (Set (Set (Var "b3")) ($#k1_recdef_1 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "p")) ($#k7_partfun1 :::"/."::: ) (Set (Var "i")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1))) ")" ) ")" ) ")" ))); theorem :: COMPUT_1:33 (Bool "for" (Set (Var "n")) "," (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "n")) ($#k4_comput_1 :::"succ"::: ) (Set (Var "i"))) ($#r2_hidden :::"in"::: ) (Set ($#k2_comput_1 :::"HFuncs"::: ) (Set ($#k5_numbers :::"NAT"::: ) )))) ; registrationlet "n", "i" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); cluster (Set "n" ($#k4_comput_1 :::"succ"::: ) "i") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) (Set (Set ($#k5_numbers :::"NAT"::: ) ) ($#k3_finseq_2 :::"*"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ($#v4_valued_0 :::"to-naturals"::: ) ($#v2_margrel1 :::"homogeneous"::: ) ($#v2_comput_1 :::"len-total"::: ) ; end; theorem :: COMPUT_1:34 (Bool "for" (Set (Var "n")) "," (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k19_margrel1 :::"arity"::: ) (Set "(" (Set (Var "n")) ($#k4_comput_1 :::"succ"::: ) (Set (Var "i")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "n")))) ; definitionlet "n", "i" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); func "n" :::"proj"::: "i" -> (Set (Set ($#k5_numbers :::"NAT"::: ) ) ($#k3_finseq_2 :::"*"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ($#v4_valued_0 :::"to-naturals"::: ) ($#v2_margrel1 :::"homogeneous"::: ) ($#m1_hidden :::"Function":::) equals :: COMPUT_1:def 8 (Set ($#k12_card_3 :::"proj"::: ) "(" (Set "(" "n" ($#k5_finseq_2 :::"|->"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ")" ) "," "i" ")" ); end; :: deftheorem defines :::"proj"::: COMPUT_1:def 8 : (Bool "for" (Set (Var "n")) "," (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "n")) ($#k5_comput_1 :::"proj"::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k12_card_3 :::"proj"::: ) "(" (Set "(" (Set (Var "n")) ($#k5_finseq_2 :::"|->"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ")" ) "," (Set (Var "i")) ")" ))); theorem :: COMPUT_1:35 (Bool "for" (Set (Var "n")) "," (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "n")) ($#k5_comput_1 :::"proj"::: ) (Set (Var "i"))) ($#r2_hidden :::"in"::: ) (Set ($#k2_comput_1 :::"HFuncs"::: ) (Set ($#k5_numbers :::"NAT"::: ) )))) ; theorem :: COMPUT_1:36 (Bool "for" (Set (Var "n")) "," (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "n")) ($#k5_comput_1 :::"proj"::: ) (Set (Var "i")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "n")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k5_numbers :::"NAT"::: ) ))) & "(" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n")))) "implies" (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" (Set (Var "n")) ($#k5_comput_1 :::"proj"::: ) (Set (Var "i")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k5_numbers :::"NAT"::: ) )) ")" ")" )) ; registrationlet "n", "i" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); cluster (Set "n" ($#k5_comput_1 :::"proj"::: ) "i") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) (Set (Set ($#k5_numbers :::"NAT"::: ) ) ($#k3_finseq_2 :::"*"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ($#v4_valued_0 :::"to-naturals"::: ) ($#v2_margrel1 :::"homogeneous"::: ) ($#v2_comput_1 :::"len-total"::: ) ; end; theorem :: COMPUT_1:37 (Bool "for" (Set (Var "n")) "," (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k19_margrel1 :::"arity"::: ) (Set "(" (Set (Var "n")) ($#k5_comput_1 :::"proj"::: ) (Set (Var "i")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "n")))) ; theorem :: COMPUT_1:38 (Bool "for" (Set (Var "n")) "," (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "t")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set (Var "n")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k5_numbers :::"NAT"::: ) )) "holds" (Bool (Set (Set "(" (Set (Var "n")) ($#k5_comput_1 :::"proj"::: ) (Set (Var "i")) ")" ) ($#k1_recdef_1 :::"."::: ) (Set (Var "t"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "t")) ($#k1_recdef_1 :::"."::: ) (Set (Var "i")))))) ; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k2_comput_1 :::"HFuncs"::: ) "X") -> ($#v4_funct_1 :::"functional"::: ) ; end; theorem :: COMPUT_1:39 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "D")) "," (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "D")) "," (Set "(" ($#k2_comput_1 :::"HFuncs"::: ) (Set (Var "E")) ")" ) "st" (Bool (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "F"))) "is" ($#v1_comput_1 :::"compatible"::: ) ) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) "holds" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Set (Var "n")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set (Var "E")))) ")" )) "holds" (Bool "ex" (Set (Var "f")) "being" ($#m2_rfunct_3 :::"Element"::: ) "of" (Set ($#k2_comput_1 :::"HFuncs"::: ) (Set (Var "E"))) "st" (Bool "(" (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set ($#k3_card_3 :::"Union"::: ) (Set (Var "F")))) & (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "n")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set (Var "E")))) ")" ))))) ; theorem :: COMPUT_1:40 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "(" ($#k2_comput_1 :::"HFuncs"::: ) (Set (Var "D")) ")" ) "st" (Bool (Bool "(" "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "F")) ($#k8_nat_1 :::"."::: ) (Set (Var "i"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "F")) ($#k8_nat_1 :::"."::: ) (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ))) ")" )) "holds" (Bool (Set ($#k3_card_3 :::"Union"::: ) (Set (Var "F"))) ($#r2_hidden :::"in"::: ) (Set ($#k2_comput_1 :::"HFuncs"::: ) (Set (Var "D")))))) ; theorem :: COMPUT_1:41 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#v3_comput_1 :::"with_the_same_arity"::: ) ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_comput_1 :::"HFuncs"::: ) (Set (Var "D"))) "holds" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set ($#k6_funct_6 :::"<:"::: ) (Set (Var "F")) ($#k6_funct_6 :::":>"::: ) )) ($#r1_tarski :::"c="::: ) (Set (Set "(" ($#k1_comput_1 :::"arity"::: ) (Set (Var "F")) ")" ) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set (Var "D")))))) ; registrationlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "F" be ($#v3_comput_1 :::"with_the_same_arity"::: ) ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_comput_1 :::"HFuncs"::: ) (Set (Const "X"))); cluster (Set ($#k6_funct_6 :::"<:"::: ) "F" ($#k6_funct_6 :::":>"::: ) ) -> ($#v2_margrel1 :::"homogeneous"::: ) ; end; theorem :: COMPUT_1:42 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m2_rfunct_3 :::"Element"::: ) "of" (Set ($#k2_comput_1 :::"HFuncs"::: ) (Set (Var "D"))) (Bool "for" (Set (Var "F")) "being" ($#v3_comput_1 :::"with_the_same_arity"::: ) ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_comput_1 :::"HFuncs"::: ) (Set (Var "D"))) "holds" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" (Set (Var "f")) ($#k3_relat_1 :::"*"::: ) (Set ($#k6_funct_6 :::"<:"::: ) (Set (Var "F")) ($#k6_funct_6 :::":>"::: ) ) ")" )) ($#r1_tarski :::"c="::: ) (Set (Set "(" ($#k1_comput_1 :::"arity"::: ) (Set (Var "F")) ")" ) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set (Var "D")))) & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" (Set (Var "f")) ($#k3_relat_1 :::"*"::: ) (Set ($#k6_funct_6 :::"<:"::: ) (Set (Var "F")) ($#k6_funct_6 :::":>"::: ) ) ")" )) ($#r1_tarski :::"c="::: ) (Set (Var "D"))) & (Bool (Set (Set (Var "f")) ($#k3_relat_1 :::"*"::: ) (Set ($#k6_funct_6 :::"<:"::: ) (Set (Var "F")) ($#k6_funct_6 :::":>"::: ) )) ($#r2_hidden :::"in"::: ) (Set ($#k2_comput_1 :::"HFuncs"::: ) (Set (Var "D")))) ")" )))) ; definitionlet "X", "Y" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "P" be ($#m1_rfunct_3 :::"PFUNC_DOMAIN":::) "of" (Set (Const "X")) "," (Set (Const "Y")); let "S" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "P")); :: original: :::"Element"::: redefine mode :::"Element"::: "of" "S" -> ($#m2_rfunct_3 :::"Element"::: ) "of" "P"; end; registrationlet "f" be (Set (Set ($#k5_numbers :::"NAT"::: ) ) ($#k3_finseq_2 :::"*"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ($#v2_margrel1 :::"homogeneous"::: ) ($#m1_hidden :::"Function":::); cluster (Set ($#k5_finseq_1 :::"<*"::: ) "f" ($#k5_finseq_1 :::"*>"::: ) ) -> ($#v3_comput_1 :::"with_the_same_arity"::: ) ; end; theorem :: COMPUT_1:43 (Bool "for" (Set (Var "f")) "being" (Set (Set ($#k5_numbers :::"NAT"::: ) ) ($#k3_finseq_2 :::"*"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ($#v4_valued_0 :::"to-naturals"::: ) ($#v2_margrel1 :::"homogeneous"::: ) ($#m1_hidden :::"Function":::) "holds" (Bool (Set ($#k1_comput_1 :::"arity"::: ) (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "f")) ($#k9_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k19_margrel1 :::"arity"::: ) (Set (Var "f"))))) ; theorem :: COMPUT_1:44 (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m2_rfunct_3 :::"Element"::: ) "of" (Set ($#k2_comput_1 :::"HFuncs"::: ) (Set ($#k5_numbers :::"NAT"::: ) )) (Bool "for" (Set (Var "F")) "being" ($#v3_comput_1 :::"with_the_same_arity"::: ) ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_comput_1 :::"HFuncs"::: ) (Set ($#k5_numbers :::"NAT"::: ) )) "st" (Bool (Bool (Set (Var "g")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k3_relat_1 :::"*"::: ) (Set ($#k6_funct_6 :::"<:"::: ) (Set (Var "F")) ($#k6_funct_6 :::":>"::: ) )))) "holds" (Bool (Set ($#k19_margrel1 :::"arity"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set ($#k1_comput_1 :::"arity"::: ) (Set (Var "F")))))) ; theorem :: COMPUT_1:45 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v3_margrel1 :::"quasi_total"::: ) ($#m2_rfunct_3 :::"Element"::: ) "of" (Set ($#k2_comput_1 :::"HFuncs"::: ) (Set (Var "D"))) (Bool "for" (Set (Var "F")) "being" ($#v3_comput_1 :::"with_the_same_arity"::: ) ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_comput_1 :::"HFuncs"::: ) (Set (Var "D"))) "st" (Bool (Bool (Set ($#k19_margrel1 :::"arity"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "F")))) & (Bool (Bool "not" (Set (Var "F")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool "(" "for" (Set (Var "h")) "being" ($#m2_rfunct_3 :::"Element"::: ) "of" (Set ($#k2_comput_1 :::"HFuncs"::: ) (Set (Var "D"))) "st" (Bool (Bool (Set (Var "h")) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "F"))))) "holds" (Bool "(" (Bool (Set (Var "h")) "is" ($#v3_margrel1 :::"quasi_total"::: ) ) & (Bool (Bool "not" (Set (Var "h")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" ) ")" )) "holds" (Bool "(" (Bool (Set (Set (Var "f")) ($#k3_relat_1 :::"*"::: ) (Set ($#k6_funct_6 :::"<:"::: ) (Set (Var "F")) ($#k6_funct_6 :::":>"::: ) )) "is" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v3_margrel1 :::"quasi_total"::: ) ($#m2_rfunct_3 :::"Element"::: ) "of" (Set ($#k2_comput_1 :::"HFuncs"::: ) (Set (Var "D")))) & (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" (Set (Var "f")) ($#k3_relat_1 :::"*"::: ) (Set ($#k6_funct_6 :::"<:"::: ) (Set (Var "F")) ($#k6_funct_6 :::":>"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_comput_1 :::"arity"::: ) (Set (Var "F")) ")" ) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set (Var "D")))) ")" )))) ; theorem :: COMPUT_1:46 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#v3_margrel1 :::"quasi_total"::: ) ($#m2_rfunct_3 :::"Element"::: ) "of" (Set ($#k2_comput_1 :::"HFuncs"::: ) (Set (Var "D"))) (Bool "for" (Set (Var "F")) "being" ($#v3_comput_1 :::"with_the_same_arity"::: ) ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_comput_1 :::"HFuncs"::: ) (Set (Var "D"))) "st" (Bool (Bool (Set ($#k19_margrel1 :::"arity"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "F")))) & (Bool "(" "for" (Set (Var "h")) "being" ($#m2_rfunct_3 :::"Element"::: ) "of" (Set ($#k2_comput_1 :::"HFuncs"::: ) (Set (Var "D"))) "st" (Bool (Bool (Set (Var "h")) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "F"))))) "holds" (Bool (Set (Var "h")) "is" ($#v3_margrel1 :::"quasi_total"::: ) ) ")" )) "holds" (Bool (Set (Set (Var "f")) ($#k3_relat_1 :::"*"::: ) (Set ($#k6_funct_6 :::"<:"::: ) (Set (Var "F")) ($#k6_funct_6 :::":>"::: ) )) "is" ($#v3_margrel1 :::"quasi_total"::: ) ($#m2_rfunct_3 :::"Element"::: ) "of" (Set ($#k2_comput_1 :::"HFuncs"::: ) (Set (Var "D"))))))) ; theorem :: COMPUT_1:47 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v3_margrel1 :::"quasi_total"::: ) ($#m2_rfunct_3 :::"Element"::: ) "of" (Set ($#k2_comput_1 :::"HFuncs"::: ) (Set (Var "D"))) "st" (Bool (Bool (Set ($#k19_margrel1 :::"arity"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k19_margrel1 :::"arity"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )))) "holds" (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set (Var "g"))))) ; theorem :: COMPUT_1:48 (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) (Set (Set ($#k5_numbers :::"NAT"::: ) ) ($#k3_finseq_2 :::"*"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ($#v4_valued_0 :::"to-naturals"::: ) ($#v2_margrel1 :::"homogeneous"::: ) ($#v2_comput_1 :::"len-total"::: ) ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set ($#k19_margrel1 :::"arity"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k19_margrel1 :::"arity"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set (Var "f")) ($#k1_recdef_1 :::"."::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k1_recdef_1 :::"."::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )))) "holds" (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set (Var "g")))) ; begin definitionlet "g", "f1", "f2" be (Set (Set ($#k5_numbers :::"NAT"::: ) ) ($#k3_finseq_2 :::"*"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ($#v4_valued_0 :::"to-naturals"::: ) ($#v2_margrel1 :::"homogeneous"::: ) ($#m1_hidden :::"Function":::); let "i" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); pred "g" :::"is_primitive-recursively_expressed_by"::: "f1" "," "f2" "," "i" means :: COMPUT_1:def 9 (Bool "ex" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set ($#k1_relset_1 :::"dom"::: ) "g") ($#r1_tarski :::"c="::: ) (Set (Set (Var "n")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k5_numbers :::"NAT"::: ) ))) & (Bool "i" ($#r1_xxreal_0 :::">="::: ) (Num 1)) & (Bool "i" ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) & (Bool (Set (Set "(" ($#k19_margrel1 :::"arity"::: ) "f1" ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Var "n"))) & (Bool (Set (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set ($#k19_margrel1 :::"arity"::: ) "f2")) & (Bool "(" "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Var "n")))) "holds" (Bool "(" "(" (Bool (Bool (Set (Set (Var "p")) ($#k3_funct_7 :::"+*"::: ) "(" "i" "," (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) "g"))) "implies" (Bool (Set ($#k2_finseq_3 :::"Del"::: ) "(" (Set (Var "p")) "," "i" ")" ) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) "f1")) ")" & "(" (Bool (Bool (Set ($#k2_finseq_3 :::"Del"::: ) "(" (Set (Var "p")) "," "i" ")" ) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) "f1"))) "implies" (Bool (Set (Set (Var "p")) ($#k3_funct_7 :::"+*"::: ) "(" "i" "," (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) "g")) ")" & "(" (Bool (Bool (Set (Set (Var "p")) ($#k3_funct_7 :::"+*"::: ) "(" "i" "," (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) "g"))) "implies" (Bool (Set "g" ($#k1_recdef_1 :::"."::: ) (Set "(" (Set (Var "p")) ($#k3_funct_7 :::"+*"::: ) "(" "i" "," (Set ($#k6_numbers :::"0"::: ) ) ")" ")" )) ($#r1_hidden :::"="::: ) (Set "f1" ($#k1_recdef_1 :::"."::: ) (Set "(" ($#k2_finseq_3 :::"Del"::: ) "(" (Set (Var "p")) "," "i" ")" ")" ))) ")" & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" "(" (Bool (Bool (Set (Set (Var "p")) ($#k3_funct_7 :::"+*"::: ) "(" "i" "," (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) "g"))) "implies" (Bool "(" (Bool (Set (Set (Var "p")) ($#k3_funct_7 :::"+*"::: ) "(" "i" "," (Set (Var "n")) ")" ) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) "g")) & (Bool (Set (Set "(" (Set (Var "p")) ($#k3_funct_7 :::"+*"::: ) "(" "i" "," (Set (Var "n")) ")" ")" ) ($#k8_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set "(" "g" ($#k1_recdef_1 :::"."::: ) (Set "(" (Set (Var "p")) ($#k3_funct_7 :::"+*"::: ) "(" "i" "," (Set (Var "n")) ")" ")" ) ")" ) ($#k12_finseq_1 :::"*>"::: ) )) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) "f2")) ")" ) ")" & "(" (Bool (Bool (Set (Set (Var "p")) ($#k3_funct_7 :::"+*"::: ) "(" "i" "," (Set (Var "n")) ")" ) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) "g")) & (Bool (Set (Set "(" (Set (Var "p")) ($#k3_funct_7 :::"+*"::: ) "(" "i" "," (Set (Var "n")) ")" ")" ) ($#k8_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set "(" "g" ($#k1_recdef_1 :::"."::: ) (Set "(" (Set (Var "p")) ($#k3_funct_7 :::"+*"::: ) "(" "i" "," (Set (Var "n")) ")" ")" ) ")" ) ($#k12_finseq_1 :::"*>"::: ) )) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) "f2"))) "implies" (Bool (Set (Set (Var "p")) ($#k3_funct_7 :::"+*"::: ) "(" "i" "," (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) "g")) ")" & "(" (Bool (Bool (Set (Set (Var "p")) ($#k3_funct_7 :::"+*"::: ) "(" "i" "," (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) "g"))) "implies" (Bool (Set "g" ($#k1_recdef_1 :::"."::: ) (Set "(" (Set (Var "p")) ($#k3_funct_7 :::"+*"::: ) "(" "i" "," (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ")" )) ($#r1_hidden :::"="::: ) (Set "f2" ($#k1_recdef_1 :::"."::: ) (Set "(" (Set "(" (Set (Var "p")) ($#k3_funct_7 :::"+*"::: ) "(" "i" "," (Set (Var "n")) ")" ")" ) ($#k8_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set "(" "g" ($#k1_recdef_1 :::"."::: ) (Set "(" (Set (Var "p")) ($#k3_funct_7 :::"+*"::: ) "(" "i" "," (Set (Var "n")) ")" ")" ) ")" ) ($#k12_finseq_1 :::"*>"::: ) ) ")" ))) ")" ")" ) ")" ) ")" ) ")" ) ")" )); end; :: deftheorem defines :::"is_primitive-recursively_expressed_by"::: COMPUT_1:def 9 : (Bool "for" (Set (Var "g")) "," (Set (Var "f1")) "," (Set (Var "f2")) "being" (Set (Set ($#k5_numbers :::"NAT"::: ) ) ($#k3_finseq_2 :::"*"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ($#v4_valued_0 :::"to-naturals"::: ) ($#v2_margrel1 :::"homogeneous"::: ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set (Var "g")) ($#r1_comput_1 :::"is_primitive-recursively_expressed_by"::: ) (Set (Var "f1")) "," (Set (Var "f2")) "," (Set (Var "i"))) "iff" (Bool "ex" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "g"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "n")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k5_numbers :::"NAT"::: ) ))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::">="::: ) (Num 1)) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) & (Bool (Set (Set "(" ($#k19_margrel1 :::"arity"::: ) (Set (Var "f1")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Var "n"))) & (Bool (Set (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set ($#k19_margrel1 :::"arity"::: ) (Set (Var "f2")))) & (Bool "(" "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Var "n")))) "holds" (Bool "(" "(" (Bool (Bool (Set (Set (Var "p")) ($#k3_funct_7 :::"+*"::: ) "(" (Set (Var "i")) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "g"))))) "implies" (Bool (Set ($#k2_finseq_3 :::"Del"::: ) "(" (Set (Var "p")) "," (Set (Var "i")) ")" ) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f1")))) ")" & "(" (Bool (Bool (Set ($#k2_finseq_3 :::"Del"::: ) "(" (Set (Var "p")) "," (Set (Var "i")) ")" ) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f1"))))) "implies" (Bool (Set (Set (Var "p")) ($#k3_funct_7 :::"+*"::: ) "(" (Set (Var "i")) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "g")))) ")" & "(" (Bool (Bool (Set (Set (Var "p")) ($#k3_funct_7 :::"+*"::: ) "(" (Set (Var "i")) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "g"))))) "implies" (Bool (Set (Set (Var "g")) ($#k1_recdef_1 :::"."::: ) (Set "(" (Set (Var "p")) ($#k3_funct_7 :::"+*"::: ) "(" (Set (Var "i")) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "f1")) ($#k1_recdef_1 :::"."::: ) (Set "(" ($#k2_finseq_3 :::"Del"::: ) "(" (Set (Var "p")) "," (Set (Var "i")) ")" ")" ))) ")" & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" "(" (Bool (Bool (Set (Set (Var "p")) ($#k3_funct_7 :::"+*"::: ) "(" (Set (Var "i")) "," (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "g"))))) "implies" (Bool "(" (Bool (Set (Set (Var "p")) ($#k3_funct_7 :::"+*"::: ) "(" (Set (Var "i")) "," (Set (Var "n")) ")" ) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "g")))) & (Bool (Set (Set "(" (Set (Var "p")) ($#k3_funct_7 :::"+*"::: ) "(" (Set (Var "i")) "," (Set (Var "n")) ")" ")" ) ($#k8_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set "(" (Set (Var "g")) ($#k1_recdef_1 :::"."::: ) (Set "(" (Set (Var "p")) ($#k3_funct_7 :::"+*"::: ) "(" (Set (Var "i")) "," (Set (Var "n")) ")" ")" ) ")" ) ($#k12_finseq_1 :::"*>"::: ) )) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f2")))) ")" ) ")" & "(" (Bool (Bool (Set (Set (Var "p")) ($#k3_funct_7 :::"+*"::: ) "(" (Set (Var "i")) "," (Set (Var "n")) ")" ) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "g")))) & (Bool (Set (Set "(" (Set (Var "p")) ($#k3_funct_7 :::"+*"::: ) "(" (Set (Var "i")) "," (Set (Var "n")) ")" ")" ) ($#k8_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set "(" (Set (Var "g")) ($#k1_recdef_1 :::"."::: ) (Set "(" (Set (Var "p")) ($#k3_funct_7 :::"+*"::: ) "(" (Set (Var "i")) "," (Set (Var "n")) ")" ")" ) ")" ) ($#k12_finseq_1 :::"*>"::: ) )) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f2"))))) "implies" (Bool (Set (Set (Var "p")) ($#k3_funct_7 :::"+*"::: ) "(" (Set (Var "i")) "," (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "g")))) ")" & "(" (Bool (Bool (Set (Set (Var "p")) ($#k3_funct_7 :::"+*"::: ) "(" (Set (Var "i")) "," (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "g"))))) "implies" (Bool (Set (Set (Var "g")) ($#k1_recdef_1 :::"."::: ) (Set "(" (Set (Var "p")) ($#k3_funct_7 :::"+*"::: ) "(" (Set (Var "i")) "," (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "f2")) ($#k1_recdef_1 :::"."::: ) (Set "(" (Set "(" (Set (Var "p")) ($#k3_funct_7 :::"+*"::: ) "(" (Set (Var "i")) "," (Set (Var "n")) ")" ")" ) ($#k8_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set "(" (Set (Var "g")) ($#k1_recdef_1 :::"."::: ) (Set "(" (Set (Var "p")) ($#k3_funct_7 :::"+*"::: ) "(" (Set (Var "i")) "," (Set (Var "n")) ")" ")" ) ")" ) ($#k12_finseq_1 :::"*>"::: ) ) ")" ))) ")" ")" ) ")" ) ")" ) ")" ) ")" )) ")" ))); definitionlet "f1", "f2" be (Set (Set ($#k5_numbers :::"NAT"::: ) ) ($#k3_finseq_2 :::"*"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ($#v4_valued_0 :::"to-naturals"::: ) ($#v2_margrel1 :::"homogeneous"::: ) ($#m1_hidden :::"Function":::); let "i" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "p" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); func :::"primrec"::: "(" "f1" "," "f2" "," "i" "," "p" ")" -> ($#m2_rfunct_3 :::"Element"::: ) "of" (Set ($#k2_comput_1 :::"HFuncs"::: ) (Set ($#k5_numbers :::"NAT"::: ) )) means :: COMPUT_1:def 10 (Bool "ex" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "(" ($#k2_comput_1 :::"HFuncs"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ")" ) "st" (Bool "(" (Bool it ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k8_nat_1 :::"."::: ) (Set "(" "p" ($#k7_partfun1 :::"/."::: ) "i" ")" ))) & "(" (Bool (Bool "i" ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) "p")) & (Bool (Set ($#k2_finseq_3 :::"Del"::: ) "(" "p" "," "i" ")" ) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) "f1"))) "implies" (Bool (Set (Set (Var "F")) ($#k8_nat_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set "(" "p" ($#k3_funct_7 :::"+*"::: ) "(" "i" "," (Set ($#k6_numbers :::"0"::: ) ) ")" ")" ) ($#k16_funcop_1 :::".-->"::: ) (Set "(" "f1" ($#k1_recdef_1 :::"."::: ) (Set "(" ($#k2_finseq_3 :::"Del"::: ) "(" "p" "," "i" ")" ")" ) ")" ))) ")" & "(" (Bool (Bool "(" "not" (Bool "i" ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) "p")) "or" "not" (Bool (Set ($#k2_finseq_3 :::"Del"::: ) "(" "p" "," "i" ")" ) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) "f1")) ")" )) "implies" (Bool (Set (Set (Var "F")) ($#k8_nat_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" & (Bool "(" "for" (Set (Var "m")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" "(" (Bool (Bool "i" ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) "p")) & (Bool (Set "p" ($#k3_funct_7 :::"+*"::: ) "(" "i" "," (Set (Var "m")) ")" ) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "F")) ($#k8_nat_1 :::"."::: ) (Set (Var "m")) ")" ))) & (Bool (Set (Set "(" "p" ($#k3_funct_7 :::"+*"::: ) "(" "i" "," (Set (Var "m")) ")" ")" ) ($#k8_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set "(" (Set "(" (Set (Var "F")) ($#k8_nat_1 :::"."::: ) (Set (Var "m")) ")" ) ($#k1_recdef_1 :::"."::: ) (Set "(" "p" ($#k3_funct_7 :::"+*"::: ) "(" "i" "," (Set (Var "m")) ")" ")" ) ")" ) ($#k12_finseq_1 :::"*>"::: ) )) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) "f2"))) "implies" (Bool (Set (Set (Var "F")) ($#k8_nat_1 :::"."::: ) (Set "(" (Set (Var "m")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "F")) ($#k8_nat_1 :::"."::: ) (Set (Var "m")) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set "(" "p" ($#k3_funct_7 :::"+*"::: ) "(" "i" "," (Set "(" (Set (Var "m")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ")" ) ($#k16_funcop_1 :::".-->"::: ) (Set "(" "f2" ($#k1_recdef_1 :::"."::: ) (Set "(" (Set "(" "p" ($#k3_funct_7 :::"+*"::: ) "(" "i" "," (Set (Var "m")) ")" ")" ) ($#k8_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set "(" (Set "(" (Set (Var "F")) ($#k8_nat_1 :::"."::: ) (Set (Var "m")) ")" ) ($#k1_recdef_1 :::"."::: ) (Set "(" "p" ($#k3_funct_7 :::"+*"::: ) "(" "i" "," (Set (Var "m")) ")" ")" ) ")" ) ($#k12_finseq_1 :::"*>"::: ) ) ")" ) ")" ) ")" ))) ")" & "(" (Bool (Bool "(" "not" (Bool "i" ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) "p")) "or" "not" (Bool (Set "p" ($#k3_funct_7 :::"+*"::: ) "(" "i" "," (Set (Var "m")) ")" ) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "F")) ($#k8_nat_1 :::"."::: ) (Set (Var "m")) ")" ))) "or" "not" (Bool (Set (Set "(" "p" ($#k3_funct_7 :::"+*"::: ) "(" "i" "," (Set (Var "m")) ")" ")" ) ($#k8_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set "(" (Set "(" (Set (Var "F")) ($#k8_nat_1 :::"."::: ) (Set (Var "m")) ")" ) ($#k1_recdef_1 :::"."::: ) (Set "(" "p" ($#k3_funct_7 :::"+*"::: ) "(" "i" "," (Set (Var "m")) ")" ")" ) ")" ) ($#k12_finseq_1 :::"*>"::: ) )) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) "f2")) ")" )) "implies" (Bool (Set (Set (Var "F")) ($#k8_nat_1 :::"."::: ) (Set "(" (Set (Var "m")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k8_nat_1 :::"."::: ) (Set (Var "m")))) ")" ")" ) ")" ) ")" )); end; :: deftheorem defines :::"primrec"::: COMPUT_1:def 10 : (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" (Set (Set ($#k5_numbers :::"NAT"::: ) ) ($#k3_finseq_2 :::"*"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ($#v4_valued_0 :::"to-naturals"::: ) ($#v2_margrel1 :::"homogeneous"::: ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "b5")) "being" ($#m2_rfunct_3 :::"Element"::: ) "of" (Set ($#k2_comput_1 :::"HFuncs"::: ) (Set ($#k5_numbers :::"NAT"::: ) )) "holds" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set ($#k6_comput_1 :::"primrec"::: ) "(" (Set (Var "f1")) "," (Set (Var "f2")) "," (Set (Var "i")) "," (Set (Var "p")) ")" )) "iff" (Bool "ex" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "(" ($#k2_comput_1 :::"HFuncs"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ")" ) "st" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k8_nat_1 :::"."::: ) (Set "(" (Set (Var "p")) ($#k7_partfun1 :::"/."::: ) (Set (Var "i")) ")" ))) & "(" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "p")))) & (Bool (Set ($#k2_finseq_3 :::"Del"::: ) "(" (Set (Var "p")) "," (Set (Var "i")) ")" ) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f1"))))) "implies" (Bool (Set (Set (Var "F")) ($#k8_nat_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "p")) ($#k3_funct_7 :::"+*"::: ) "(" (Set (Var "i")) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ")" ) ($#k16_funcop_1 :::".-->"::: ) (Set "(" (Set (Var "f1")) ($#k1_recdef_1 :::"."::: ) (Set "(" ($#k2_finseq_3 :::"Del"::: ) "(" (Set (Var "p")) "," (Set (Var "i")) ")" ")" ) ")" ))) ")" & "(" (Bool (Bool "(" "not" (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "p")))) "or" "not" (Bool (Set ($#k2_finseq_3 :::"Del"::: ) "(" (Set (Var "p")) "," (Set (Var "i")) ")" ) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f1")))) ")" )) "implies" (Bool (Set (Set (Var "F")) ($#k8_nat_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" & (Bool "(" "for" (Set (Var "m")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "p")))) & (Bool (Set (Set (Var "p")) ($#k3_funct_7 :::"+*"::: ) "(" (Set (Var "i")) "," (Set (Var "m")) ")" ) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "F")) ($#k8_nat_1 :::"."::: ) (Set (Var "m")) ")" ))) & (Bool (Set (Set "(" (Set (Var "p")) ($#k3_funct_7 :::"+*"::: ) "(" (Set (Var "i")) "," (Set (Var "m")) ")" ")" ) ($#k8_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set "(" (Set "(" (Set (Var "F")) ($#k8_nat_1 :::"."::: ) (Set (Var "m")) ")" ) ($#k1_recdef_1 :::"."::: ) (Set "(" (Set (Var "p")) ($#k3_funct_7 :::"+*"::: ) "(" (Set (Var "i")) "," (Set (Var "m")) ")" ")" ) ")" ) ($#k12_finseq_1 :::"*>"::: ) )) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f2"))))) "implies" (Bool (Set (Set (Var "F")) ($#k8_nat_1 :::"."::: ) (Set "(" (Set (Var "m")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "F")) ($#k8_nat_1 :::"."::: ) (Set (Var "m")) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set "(" (Set (Var "p")) ($#k3_funct_7 :::"+*"::: ) "(" (Set (Var "i")) "," (Set "(" (Set (Var "m")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ")" ) ($#k16_funcop_1 :::".-->"::: ) (Set "(" (Set (Var "f2")) ($#k1_recdef_1 :::"."::: ) (Set "(" (Set "(" (Set (Var "p")) ($#k3_funct_7 :::"+*"::: ) "(" (Set (Var "i")) "," (Set (Var "m")) ")" ")" ) ($#k8_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set "(" (Set "(" (Set (Var "F")) ($#k8_nat_1 :::"."::: ) (Set (Var "m")) ")" ) ($#k1_recdef_1 :::"."::: ) (Set "(" (Set (Var "p")) ($#k3_funct_7 :::"+*"::: ) "(" (Set (Var "i")) "," (Set (Var "m")) ")" ")" ) ")" ) ($#k12_finseq_1 :::"*>"::: ) ) ")" ) ")" ) ")" ))) ")" & "(" (Bool (Bool "(" "not" (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "p")))) "or" "not" (Bool (Set (Set (Var "p")) ($#k3_funct_7 :::"+*"::: ) "(" (Set (Var "i")) "," (Set (Var "m")) ")" ) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "F")) ($#k8_nat_1 :::"."::: ) (Set (Var "m")) ")" ))) "or" "not" (Bool (Set (Set "(" (Set (Var "p")) ($#k3_funct_7 :::"+*"::: ) "(" (Set (Var "i")) "," (Set (Var "m")) ")" ")" ) ($#k8_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set "(" (Set "(" (Set (Var "F")) ($#k8_nat_1 :::"."::: ) (Set (Var "m")) ")" ) ($#k1_recdef_1 :::"."::: ) (Set "(" (Set (Var "p")) ($#k3_funct_7 :::"+*"::: ) "(" (Set (Var "i")) "," (Set (Var "m")) ")" ")" ) ")" ) ($#k12_finseq_1 :::"*>"::: ) )) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f2")))) ")" )) "implies" (Bool (Set (Set (Var "F")) ($#k8_nat_1 :::"."::: ) (Set "(" (Set (Var "m")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k8_nat_1 :::"."::: ) (Set (Var "m")))) ")" ")" ) ")" ) ")" )) ")" ))))); theorem :: COMPUT_1:49 (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "e1")) "," (Set (Var "e2")) "being" (Set (Set ($#k5_numbers :::"NAT"::: ) ) ($#k3_finseq_2 :::"*"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ($#v4_valued_0 :::"to-naturals"::: ) ($#v2_margrel1 :::"homogeneous"::: ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" ($#k6_comput_1 :::"primrec"::: ) "(" (Set (Var "e1")) "," (Set (Var "e2")) "," (Set (Var "i")) "," (Set (Var "p")) ")" ")" )))) "holds" (Bool "ex" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Set (Var "q")) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k3_funct_7 :::"+*"::: ) "(" (Set (Var "i")) "," (Set (Var "k")) ")" )))))) ; theorem :: COMPUT_1:50 (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "e1")) "," (Set (Var "e2")) "being" (Set (Set ($#k5_numbers :::"NAT"::: ) ) ($#k3_finseq_2 :::"*"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ($#v4_valued_0 :::"to-naturals"::: ) ($#v2_margrel1 :::"homogeneous"::: ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Bool "not" (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "p")))))) "holds" (Bool (Set ($#k6_comput_1 :::"primrec"::: ) "(" (Set (Var "e1")) "," (Set (Var "e2")) "," (Set (Var "i")) "," (Set (Var "p")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))))) ; theorem :: COMPUT_1:51 (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "e1")) "," (Set (Var "e2")) "being" (Set (Set ($#k5_numbers :::"NAT"::: ) ) ($#k3_finseq_2 :::"*"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ($#v4_valued_0 :::"to-naturals"::: ) ($#v2_margrel1 :::"homogeneous"::: ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k6_comput_1 :::"primrec"::: ) "(" (Set (Var "e1")) "," (Set (Var "e2")) "," (Set (Var "i")) "," (Set (Var "p")) ")" ) ($#r1_partfun1 :::"tolerates"::: ) (Set ($#k6_comput_1 :::"primrec"::: ) "(" (Set (Var "e1")) "," (Set (Var "e2")) "," (Set (Var "i")) "," (Set (Var "q")) ")" ))))) ; theorem :: COMPUT_1:52 (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "e1")) "," (Set (Var "e2")) "being" (Set (Set ($#k5_numbers :::"NAT"::: ) ) ($#k3_finseq_2 :::"*"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ($#v4_valued_0 :::"to-naturals"::: ) ($#v2_margrel1 :::"homogeneous"::: ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" ($#k6_comput_1 :::"primrec"::: ) "(" (Set (Var "e1")) "," (Set (Var "e2")) "," (Set (Var "i")) "," (Set (Var "p")) ")" ")" )) ($#r1_tarski :::"c="::: ) (Set (Set "(" (Num 1) ($#k2_nat_1 :::"+"::: ) (Set "(" ($#k19_margrel1 :::"arity"::: ) (Set (Var "e1")) ")" ) ")" ) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k5_numbers :::"NAT"::: ) )))))) ; theorem :: COMPUT_1:53 (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "e1")) "," (Set (Var "e2")) "being" (Set (Set ($#k5_numbers :::"NAT"::: ) ) ($#k3_finseq_2 :::"*"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ($#v4_valued_0 :::"to-naturals"::: ) ($#v2_margrel1 :::"homogeneous"::: ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "e1")) "is" ($#v1_xboole_0 :::"empty"::: ) )) "holds" (Bool (Set ($#k6_comput_1 :::"primrec"::: ) "(" (Set (Var "e1")) "," (Set (Var "e2")) "," (Set (Var "i")) "," (Set (Var "p")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )))) ; theorem :: COMPUT_1:54 (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) (Set (Set ($#k5_numbers :::"NAT"::: ) ) ($#k3_finseq_2 :::"*"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ($#v4_valued_0 :::"to-naturals"::: ) ($#v2_margrel1 :::"homogeneous"::: ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set "(" (Set "(" ($#k19_margrel1 :::"arity"::: ) (Set (Var "f1")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k5_numbers :::"NAT"::: ) )) "st" (Bool (Bool (Set (Var "f1")) "is" ($#v2_comput_1 :::"len-total"::: ) ) & (Bool (Set (Var "f2")) "is" ($#v2_comput_1 :::"len-total"::: ) ) & (Bool (Set (Set "(" ($#k19_margrel1 :::"arity"::: ) (Set (Var "f1")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 2)) ($#r1_hidden :::"="::: ) (Set ($#k19_margrel1 :::"arity"::: ) (Set (Var "f2")))) & (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set (Num 1) ($#k2_nat_1 :::"+"::: ) (Set "(" ($#k19_margrel1 :::"arity"::: ) (Set (Var "f1")) ")" )))) "holds" (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" ($#k6_comput_1 :::"primrec"::: ) "(" (Set (Var "f1")) "," (Set (Var "f2")) "," (Set (Var "i")) "," (Set (Var "p")) ")" ")" )))))) ; definitionlet "f1", "f2" be (Set (Set ($#k5_numbers :::"NAT"::: ) ) ($#k3_finseq_2 :::"*"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ($#v4_valued_0 :::"to-naturals"::: ) ($#v2_margrel1 :::"homogeneous"::: ) ($#m1_hidden :::"Function":::); let "i" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); func :::"primrec"::: "(" "f1" "," "f2" "," "i" ")" -> ($#m2_rfunct_3 :::"Element"::: ) "of" (Set ($#k2_comput_1 :::"HFuncs"::: ) (Set ($#k5_numbers :::"NAT"::: ) )) means :: COMPUT_1:def 11 (Bool "ex" (Set (Var "G")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Set "(" (Set "(" ($#k19_margrel1 :::"arity"::: ) "f1" ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ")" ) "," (Set "(" ($#k2_comput_1 :::"HFuncs"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ")" ) "st" (Bool "(" (Bool it ($#r1_hidden :::"="::: ) (Set ($#k3_card_3 :::"Union"::: ) (Set (Var "G")))) & (Bool "(" "for" (Set (Var "p")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set "(" (Set "(" ($#k19_margrel1 :::"arity"::: ) "f1" ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k5_numbers :::"NAT"::: ) )) "holds" (Bool (Set (Set (Var "G")) ($#k3_funct_2 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k6_comput_1 :::"primrec"::: ) "(" "f1" "," "f2" "," "i" "," (Set (Var "p")) ")" )) ")" ) ")" )); end; :: deftheorem defines :::"primrec"::: COMPUT_1:def 11 : (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" (Set (Set ($#k5_numbers :::"NAT"::: ) ) ($#k3_finseq_2 :::"*"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ($#v4_valued_0 :::"to-naturals"::: ) ($#v2_margrel1 :::"homogeneous"::: ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "b4")) "being" ($#m2_rfunct_3 :::"Element"::: ) "of" (Set ($#k2_comput_1 :::"HFuncs"::: ) (Set ($#k5_numbers :::"NAT"::: ) )) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k7_comput_1 :::"primrec"::: ) "(" (Set (Var "f1")) "," (Set (Var "f2")) "," (Set (Var "i")) ")" )) "iff" (Bool "ex" (Set (Var "G")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Set "(" (Set "(" ($#k19_margrel1 :::"arity"::: ) (Set (Var "f1")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ")" ) "," (Set "(" ($#k2_comput_1 :::"HFuncs"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ")" ) "st" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k3_card_3 :::"Union"::: ) (Set (Var "G")))) & (Bool "(" "for" (Set (Var "p")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set "(" (Set "(" ($#k19_margrel1 :::"arity"::: ) (Set (Var "f1")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k5_numbers :::"NAT"::: ) )) "holds" (Bool (Set (Set (Var "G")) ($#k3_funct_2 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k6_comput_1 :::"primrec"::: ) "(" (Set (Var "f1")) "," (Set (Var "f2")) "," (Set (Var "i")) "," (Set (Var "p")) ")" )) ")" ) ")" )) ")" )))); theorem :: COMPUT_1:55 (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "e1")) "," (Set (Var "e2")) "being" (Set (Set ($#k5_numbers :::"NAT"::: ) ) ($#k3_finseq_2 :::"*"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ($#v4_valued_0 :::"to-naturals"::: ) ($#v2_margrel1 :::"homogeneous"::: ) ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "e1")) "is" ($#v1_xboole_0 :::"empty"::: ) )) "holds" (Bool (Set ($#k7_comput_1 :::"primrec"::: ) "(" (Set (Var "e1")) "," (Set (Var "e2")) "," (Set (Var "i")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) ; theorem :: COMPUT_1:56 (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) (Set (Set ($#k5_numbers :::"NAT"::: ) ) ($#k3_finseq_2 :::"*"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ($#v4_valued_0 :::"to-naturals"::: ) ($#v2_margrel1 :::"homogeneous"::: ) ($#m1_hidden :::"Function":::) "holds" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" ($#k7_comput_1 :::"primrec"::: ) "(" (Set (Var "f1")) "," (Set (Var "f2")) "," (Set (Var "i")) ")" ")" )) ($#r1_tarski :::"c="::: ) (Set (Set "(" (Set "(" ($#k19_margrel1 :::"arity"::: ) (Set (Var "f1")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k5_numbers :::"NAT"::: ) ))))) ; theorem :: COMPUT_1:57 (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) (Set (Set ($#k5_numbers :::"NAT"::: ) ) ($#k3_finseq_2 :::"*"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ($#v4_valued_0 :::"to-naturals"::: ) ($#v2_margrel1 :::"homogeneous"::: ) ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "f1")) "is" ($#v2_comput_1 :::"len-total"::: ) ) & (Bool (Set (Var "f2")) "is" ($#v2_comput_1 :::"len-total"::: ) ) & (Bool (Set (Set "(" ($#k19_margrel1 :::"arity"::: ) (Set (Var "f1")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 2)) ($#r1_hidden :::"="::: ) (Set ($#k19_margrel1 :::"arity"::: ) (Set (Var "f2")))) & (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set (Num 1) ($#k2_nat_1 :::"+"::: ) (Set "(" ($#k19_margrel1 :::"arity"::: ) (Set (Var "f1")) ")" )))) "holds" (Bool "(" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" ($#k7_comput_1 :::"primrec"::: ) "(" (Set (Var "f1")) "," (Set (Var "f2")) "," (Set (Var "i")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k19_margrel1 :::"arity"::: ) (Set (Var "f1")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k5_numbers :::"NAT"::: ) ))) & (Bool (Set ($#k19_margrel1 :::"arity"::: ) (Set "(" ($#k7_comput_1 :::"primrec"::: ) "(" (Set (Var "f1")) "," (Set (Var "f2")) "," (Set (Var "i")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k19_margrel1 :::"arity"::: ) (Set (Var "f1")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1))) ")" ))) ; definitionlet "n" be ($#m1_hidden :::"Nat":::); let "p" be ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set (Const "n")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k5_numbers :::"NAT"::: ) )); let "i", "k" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); :: original: :::"+*"::: redefine func "p" :::"+*"::: "(" "i" "," "k" ")" -> ($#m2_finseq_2 :::"Element"::: ) "of" (Set "n" ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k5_numbers :::"NAT"::: ) )); end; theorem :: COMPUT_1:58 (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) (Set (Set ($#k5_numbers :::"NAT"::: ) ) ($#k3_finseq_2 :::"*"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ($#v4_valued_0 :::"to-naturals"::: ) ($#v2_margrel1 :::"homogeneous"::: ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set "(" (Set "(" ($#k19_margrel1 :::"arity"::: ) (Set (Var "f1")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k5_numbers :::"NAT"::: ) )) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "p"))))) "holds" (Bool "(" (Bool (Set (Set (Var "p")) ($#k8_comput_1 :::"+*"::: ) "(" (Set (Var "i")) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" ($#k7_comput_1 :::"primrec"::: ) "(" (Set (Var "f1")) "," (Set (Var "f2")) "," (Set (Var "i")) ")" ")" ))) "iff" (Bool (Set ($#k2_finseq_3 :::"Del"::: ) "(" (Set (Var "p")) "," (Set (Var "i")) ")" ) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f1")))) ")" )))) ; theorem :: COMPUT_1:59 (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) (Set (Set ($#k5_numbers :::"NAT"::: ) ) ($#k3_finseq_2 :::"*"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ($#v4_valued_0 :::"to-naturals"::: ) ($#v2_margrel1 :::"homogeneous"::: ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set "(" (Set "(" ($#k19_margrel1 :::"arity"::: ) (Set (Var "f1")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k5_numbers :::"NAT"::: ) )) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "p")))) & (Bool (Set (Set (Var "p")) ($#k8_comput_1 :::"+*"::: ) "(" (Set (Var "i")) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" ($#k7_comput_1 :::"primrec"::: ) "(" (Set (Var "f1")) "," (Set (Var "f2")) "," (Set (Var "i")) ")" ")" )))) "holds" (Bool (Set (Set "(" ($#k7_comput_1 :::"primrec"::: ) "(" (Set (Var "f1")) "," (Set (Var "f2")) "," (Set (Var "i")) ")" ")" ) ($#k1_recdef_1 :::"."::: ) (Set "(" (Set (Var "p")) ($#k8_comput_1 :::"+*"::: ) "(" (Set (Var "i")) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "f1")) ($#k1_recdef_1 :::"."::: ) (Set "(" ($#k2_finseq_3 :::"Del"::: ) "(" (Set (Var "p")) "," (Set (Var "i")) ")" ")" )))))) ; theorem :: COMPUT_1:60 (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) (Set (Set ($#k5_numbers :::"NAT"::: ) ) ($#k3_finseq_2 :::"*"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ($#v4_valued_0 :::"to-naturals"::: ) ($#v2_margrel1 :::"homogeneous"::: ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set "(" (Set "(" ($#k19_margrel1 :::"arity"::: ) (Set (Var "f1")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k5_numbers :::"NAT"::: ) )) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "p")))) & (Bool (Set (Var "f1")) "is" ($#v2_comput_1 :::"len-total"::: ) )) "holds" (Bool (Set (Set "(" ($#k7_comput_1 :::"primrec"::: ) "(" (Set (Var "f1")) "," (Set (Var "f2")) "," (Set (Var "i")) ")" ")" ) ($#k1_recdef_1 :::"."::: ) (Set "(" (Set (Var "p")) ($#k8_comput_1 :::"+*"::: ) "(" (Set (Var "i")) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "f1")) ($#k1_recdef_1 :::"."::: ) (Set "(" ($#k2_finseq_3 :::"Del"::: ) "(" (Set (Var "p")) "," (Set (Var "i")) ")" ")" )))))) ; theorem :: COMPUT_1:61 (Bool "for" (Set (Var "i")) "," (Set (Var "m")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) (Set (Set ($#k5_numbers :::"NAT"::: ) ) ($#k3_finseq_2 :::"*"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ($#v4_valued_0 :::"to-naturals"::: ) ($#v2_margrel1 :::"homogeneous"::: ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set "(" (Set "(" ($#k19_margrel1 :::"arity"::: ) (Set (Var "f1")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k5_numbers :::"NAT"::: ) )) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "p"))))) "holds" (Bool "(" (Bool (Set (Set (Var "p")) ($#k8_comput_1 :::"+*"::: ) "(" (Set (Var "i")) "," (Set "(" (Set (Var "m")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" ($#k7_comput_1 :::"primrec"::: ) "(" (Set (Var "f1")) "," (Set (Var "f2")) "," (Set (Var "i")) ")" ")" ))) "iff" (Bool "(" (Bool (Set (Set (Var "p")) ($#k8_comput_1 :::"+*"::: ) "(" (Set (Var "i")) "," (Set (Var "m")) ")" ) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" ($#k7_comput_1 :::"primrec"::: ) "(" (Set (Var "f1")) "," (Set (Var "f2")) "," (Set (Var "i")) ")" ")" ))) & (Bool (Set (Set "(" (Set (Var "p")) ($#k8_comput_1 :::"+*"::: ) "(" (Set (Var "i")) "," (Set (Var "m")) ")" ")" ) ($#k8_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set "(" (Set "(" ($#k7_comput_1 :::"primrec"::: ) "(" (Set (Var "f1")) "," (Set (Var "f2")) "," (Set (Var "i")) ")" ")" ) ($#k1_recdef_1 :::"."::: ) (Set "(" (Set (Var "p")) ($#k8_comput_1 :::"+*"::: ) "(" (Set (Var "i")) "," (Set (Var "m")) ")" ")" ) ")" ) ($#k12_finseq_1 :::"*>"::: ) )) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f2")))) ")" ) ")" )))) ; theorem :: COMPUT_1:62 (Bool "for" (Set (Var "i")) "," (Set (Var "m")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) (Set (Set ($#k5_numbers :::"NAT"::: ) ) ($#k3_finseq_2 :::"*"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ($#v4_valued_0 :::"to-naturals"::: ) ($#v2_margrel1 :::"homogeneous"::: ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set "(" (Set "(" ($#k19_margrel1 :::"arity"::: ) (Set (Var "f1")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k5_numbers :::"NAT"::: ) )) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "p")))) & (Bool (Set (Set (Var "p")) ($#k8_comput_1 :::"+*"::: ) "(" (Set (Var "i")) "," (Set "(" (Set (Var "m")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" ($#k7_comput_1 :::"primrec"::: ) "(" (Set (Var "f1")) "," (Set (Var "f2")) "," (Set (Var "i")) ")" ")" )))) "holds" (Bool (Set (Set "(" ($#k7_comput_1 :::"primrec"::: ) "(" (Set (Var "f1")) "," (Set (Var "f2")) "," (Set (Var "i")) ")" ")" ) ($#k1_recdef_1 :::"."::: ) (Set "(" (Set (Var "p")) ($#k8_comput_1 :::"+*"::: ) "(" (Set (Var "i")) "," (Set "(" (Set (Var "m")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "f2")) ($#k1_recdef_1 :::"."::: ) (Set "(" (Set "(" (Set (Var "p")) ($#k8_comput_1 :::"+*"::: ) "(" (Set (Var "i")) "," (Set (Var "m")) ")" ")" ) ($#k8_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set "(" (Set "(" ($#k7_comput_1 :::"primrec"::: ) "(" (Set (Var "f1")) "," (Set (Var "f2")) "," (Set (Var "i")) ")" ")" ) ($#k1_recdef_1 :::"."::: ) (Set "(" (Set (Var "p")) ($#k8_comput_1 :::"+*"::: ) "(" (Set (Var "i")) "," (Set (Var "m")) ")" ")" ) ")" ) ($#k12_finseq_1 :::"*>"::: ) ) ")" )))))) ; theorem :: COMPUT_1:63 (Bool "for" (Set (Var "i")) "," (Set (Var "m")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) (Set (Set ($#k5_numbers :::"NAT"::: ) ) ($#k3_finseq_2 :::"*"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ($#v4_valued_0 :::"to-naturals"::: ) ($#v2_margrel1 :::"homogeneous"::: ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set "(" (Set "(" ($#k19_margrel1 :::"arity"::: ) (Set (Var "f1")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k5_numbers :::"NAT"::: ) )) "st" (Bool (Bool (Set (Var "f1")) "is" ($#v2_comput_1 :::"len-total"::: ) ) & (Bool (Set (Var "f2")) "is" ($#v2_comput_1 :::"len-total"::: ) ) & (Bool (Set (Set "(" ($#k19_margrel1 :::"arity"::: ) (Set (Var "f1")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 2)) ($#r1_hidden :::"="::: ) (Set ($#k19_margrel1 :::"arity"::: ) (Set (Var "f2")))) & (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set (Num 1) ($#k2_nat_1 :::"+"::: ) (Set "(" ($#k19_margrel1 :::"arity"::: ) (Set (Var "f1")) ")" )))) "holds" (Bool (Set (Set "(" ($#k7_comput_1 :::"primrec"::: ) "(" (Set (Var "f1")) "," (Set (Var "f2")) "," (Set (Var "i")) ")" ")" ) ($#k1_recdef_1 :::"."::: ) (Set "(" (Set (Var "p")) ($#k8_comput_1 :::"+*"::: ) "(" (Set (Var "i")) "," (Set "(" (Set (Var "m")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "f2")) ($#k1_recdef_1 :::"."::: ) (Set "(" (Set "(" (Set (Var "p")) ($#k8_comput_1 :::"+*"::: ) "(" (Set (Var "i")) "," (Set (Var "m")) ")" ")" ) ($#k8_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set "(" (Set "(" ($#k7_comput_1 :::"primrec"::: ) "(" (Set (Var "f1")) "," (Set (Var "f2")) "," (Set (Var "i")) ")" ")" ) ($#k1_recdef_1 :::"."::: ) (Set "(" (Set (Var "p")) ($#k8_comput_1 :::"+*"::: ) "(" (Set (Var "i")) "," (Set (Var "m")) ")" ")" ) ")" ) ($#k12_finseq_1 :::"*>"::: ) ) ")" )))))) ; theorem :: COMPUT_1:64 (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) (Set (Set ($#k5_numbers :::"NAT"::: ) ) ($#k3_finseq_2 :::"*"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ($#v4_valued_0 :::"to-naturals"::: ) ($#v2_margrel1 :::"homogeneous"::: ) ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Set "(" ($#k19_margrel1 :::"arity"::: ) (Set (Var "f1")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 2)) ($#r1_hidden :::"="::: ) (Set ($#k19_margrel1 :::"arity"::: ) (Set (Var "f2")))) & (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" ($#k19_margrel1 :::"arity"::: ) (Set (Var "f1")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1)))) "holds" (Bool (Set ($#k7_comput_1 :::"primrec"::: ) "(" (Set (Var "f1")) "," (Set (Var "f2")) "," (Set (Var "i")) ")" ) ($#r1_comput_1 :::"is_primitive-recursively_expressed_by"::: ) (Set (Var "f1")) "," (Set (Var "f2")) "," (Set (Var "i"))))) ; theorem :: COMPUT_1:65 (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) (Set (Set ($#k5_numbers :::"NAT"::: ) ) ($#k3_finseq_2 :::"*"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ($#v4_valued_0 :::"to-naturals"::: ) ($#v2_margrel1 :::"homogeneous"::: ) ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" ($#k19_margrel1 :::"arity"::: ) (Set (Var "f1")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1)))) "holds" (Bool "for" (Set (Var "g")) "being" ($#m2_rfunct_3 :::"Element"::: ) "of" (Set ($#k2_comput_1 :::"HFuncs"::: ) (Set ($#k5_numbers :::"NAT"::: ) )) "st" (Bool (Bool (Set (Var "g")) ($#r1_comput_1 :::"is_primitive-recursively_expressed_by"::: ) (Set (Var "f1")) "," (Set (Var "f2")) "," (Set (Var "i")))) "holds" (Bool (Set (Var "g")) ($#r1_hidden :::"="::: ) (Set ($#k7_comput_1 :::"primrec"::: ) "(" (Set (Var "f1")) "," (Set (Var "f2")) "," (Set (Var "i")) ")" ))))) ; begin definitionlet "X" be ($#m1_hidden :::"set"::: ) ; attr "X" is :::"composition_closed"::: means :: COMPUT_1:def 12 (Bool "for" (Set (Var "f")) "being" ($#m2_rfunct_3 :::"Element"::: ) "of" (Set ($#k2_comput_1 :::"HFuncs"::: ) (Set ($#k5_numbers :::"NAT"::: ) )) (Bool "for" (Set (Var "F")) "being" ($#v3_comput_1 :::"with_the_same_arity"::: ) ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_comput_1 :::"HFuncs"::: ) (Set ($#k5_numbers :::"NAT"::: ) )) "st" (Bool (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) "X") & (Bool (Set ($#k19_margrel1 :::"arity"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "F")))) & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "F"))) ($#r1_tarski :::"c="::: ) "X")) "holds" (Bool (Set (Set (Var "f")) ($#k3_relat_1 :::"*"::: ) (Set ($#k6_funct_6 :::"<:"::: ) (Set (Var "F")) ($#k6_funct_6 :::":>"::: ) )) ($#r2_hidden :::"in"::: ) "X"))); attr "X" is :::"primitive-recursion_closed"::: means :: COMPUT_1:def 13 (Bool "for" (Set (Var "g")) "," (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m2_rfunct_3 :::"Element"::: ) "of" (Set ($#k2_comput_1 :::"HFuncs"::: ) (Set ($#k5_numbers :::"NAT"::: ) )) (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "g")) ($#r1_comput_1 :::"is_primitive-recursively_expressed_by"::: ) (Set (Var "f1")) "," (Set (Var "f2")) "," (Set (Var "i"))) & (Bool (Set (Var "f1")) ($#r2_hidden :::"in"::: ) "X") & (Bool (Set (Var "f2")) ($#r2_hidden :::"in"::: ) "X")) "holds" (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) "X"))); end; :: deftheorem defines :::"composition_closed"::: COMPUT_1:def 12 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "X")) "is" ($#v4_comput_1 :::"composition_closed"::: ) ) "iff" (Bool "for" (Set (Var "f")) "being" ($#m2_rfunct_3 :::"Element"::: ) "of" (Set ($#k2_comput_1 :::"HFuncs"::: ) (Set ($#k5_numbers :::"NAT"::: ) )) (Bool "for" (Set (Var "F")) "being" ($#v3_comput_1 :::"with_the_same_arity"::: ) ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_comput_1 :::"HFuncs"::: ) (Set ($#k5_numbers :::"NAT"::: ) )) "st" (Bool (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set ($#k19_margrel1 :::"arity"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "F")))) & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "F"))) ($#r1_tarski :::"c="::: ) (Set (Var "X")))) "holds" (Bool (Set (Set (Var "f")) ($#k3_relat_1 :::"*"::: ) (Set ($#k6_funct_6 :::"<:"::: ) (Set (Var "F")) ($#k6_funct_6 :::":>"::: ) )) ($#r2_hidden :::"in"::: ) (Set (Var "X"))))) ")" )); :: deftheorem defines :::"primitive-recursion_closed"::: COMPUT_1:def 13 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "X")) "is" ($#v5_comput_1 :::"primitive-recursion_closed"::: ) ) "iff" (Bool "for" (Set (Var "g")) "," (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m2_rfunct_3 :::"Element"::: ) "of" (Set ($#k2_comput_1 :::"HFuncs"::: ) (Set ($#k5_numbers :::"NAT"::: ) )) (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "g")) ($#r1_comput_1 :::"is_primitive-recursively_expressed_by"::: ) (Set (Var "f1")) "," (Set (Var "f2")) "," (Set (Var "i"))) & (Bool (Set (Var "f1")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Var "f2")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))))) ")" )); definitionlet "X" be ($#m1_hidden :::"set"::: ) ; attr "X" is :::"primitive-recursively_closed"::: means :: COMPUT_1:def 14 (Bool "(" (Bool (Set (Set ($#k6_numbers :::"0"::: ) ) ($#k3_comput_1 :::"const"::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r2_hidden :::"in"::: ) "X") & (Bool (Set (Num 1) ($#k4_comput_1 :::"succ"::: ) (Num 1)) ($#r2_hidden :::"in"::: ) "X") & (Bool "(" "for" (Set (Var "n")) "," (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n")))) "holds" (Bool (Set (Set (Var "n")) ($#k5_comput_1 :::"proj"::: ) (Set (Var "i"))) ($#r2_hidden :::"in"::: ) "X") ")" ) & (Bool "X" "is" ($#v4_comput_1 :::"composition_closed"::: ) ) & (Bool "X" "is" ($#v5_comput_1 :::"primitive-recursion_closed"::: ) ) ")" ); end; :: deftheorem defines :::"primitive-recursively_closed"::: COMPUT_1:def 14 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "X")) "is" ($#v6_comput_1 :::"primitive-recursively_closed"::: ) ) "iff" (Bool "(" (Bool (Set (Set ($#k6_numbers :::"0"::: ) ) ($#k3_comput_1 :::"const"::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Num 1) ($#k4_comput_1 :::"succ"::: ) (Num 1)) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool "(" "for" (Set (Var "n")) "," (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n")))) "holds" (Bool (Set (Set (Var "n")) ($#k5_comput_1 :::"proj"::: ) (Set (Var "i"))) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) ")" ) & (Bool (Set (Var "X")) "is" ($#v4_comput_1 :::"composition_closed"::: ) ) & (Bool (Set (Var "X")) "is" ($#v5_comput_1 :::"primitive-recursion_closed"::: ) ) ")" ) ")" )); theorem :: COMPUT_1:66 (Bool (Set ($#k2_comput_1 :::"HFuncs"::: ) (Set ($#k5_numbers :::"NAT"::: ) )) "is" ($#v6_comput_1 :::"primitive-recursively_closed"::: ) ) ; registration cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v4_funct_1 :::"functional"::: ) ($#v6_comput_1 :::"primitive-recursively_closed"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set bbbadK1_ZFMISC_1((Set "(" ($#k2_comput_1 :::"HFuncs"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ")" ))); end; theorem :: COMPUT_1:67 (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "e1")) "," (Set (Var "e2")) "being" (Set (Set ($#k5_numbers :::"NAT"::: ) ) ($#k3_finseq_2 :::"*"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ($#v4_valued_0 :::"to-naturals"::: ) ($#v2_margrel1 :::"homogeneous"::: ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "g")) "being" ($#m2_rfunct_3 :::"Element"::: ) "of" (Set ($#k2_comput_1 :::"HFuncs"::: ) (Set ($#k5_numbers :::"NAT"::: ) )) "st" (Bool (Bool (Set (Var "e1")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "g")) ($#r1_comput_1 :::"is_primitive-recursively_expressed_by"::: ) (Set (Var "e1")) "," (Set (Var "e2")) "," (Set (Var "i")))) "holds" (Bool (Set (Var "g")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))))) ; theorem :: COMPUT_1:68 (Bool "for" (Set (Var "g")) "being" ($#m2_rfunct_3 :::"Element"::: ) "of" (Set ($#k2_comput_1 :::"HFuncs"::: ) (Set ($#k5_numbers :::"NAT"::: ) )) (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#v3_margrel1 :::"quasi_total"::: ) ($#m2_rfunct_3 :::"Element"::: ) "of" (Set ($#k2_comput_1 :::"HFuncs"::: ) (Set ($#k5_numbers :::"NAT"::: ) )) (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "g")) ($#r1_comput_1 :::"is_primitive-recursively_expressed_by"::: ) (Set (Var "f1")) "," (Set (Var "f2")) "," (Set (Var "i")))) "holds" (Bool "(" (Bool (Set (Var "g")) "is" ($#v3_margrel1 :::"quasi_total"::: ) ) & "(" (Bool (Bool (Bool "not" (Set (Var "f1")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool "not" (Bool (Set (Var "g")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" ")" )))) ; theorem :: COMPUT_1:69 (Bool "for" (Set (Var "n")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "P")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v6_comput_1 :::"primitive-recursively_closed"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k2_comput_1 :::"HFuncs"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ")" ) "holds" (Bool (Set (Set (Var "n")) ($#k3_comput_1 :::"const"::: ) (Set (Var "c"))) ($#r2_hidden :::"in"::: ) (Set (Var "P"))))) ; theorem :: COMPUT_1:70 (Bool "for" (Set (Var "i")) "," (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "P")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v6_comput_1 :::"primitive-recursively_closed"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k2_comput_1 :::"HFuncs"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ")" ) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n")))) "holds" (Bool (Set (Set (Var "n")) ($#k4_comput_1 :::"succ"::: ) (Set (Var "i"))) ($#r2_hidden :::"in"::: ) (Set (Var "P"))))) ; theorem :: COMPUT_1:71 (Bool "for" (Set (Var "P")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v6_comput_1 :::"primitive-recursively_closed"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k2_comput_1 :::"HFuncs"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ")" ) "holds" (Bool (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "P")))) ; theorem :: COMPUT_1:72 (Bool "for" (Set (Var "P")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v6_comput_1 :::"primitive-recursively_closed"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k2_comput_1 :::"HFuncs"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ")" ) (Bool "for" (Set (Var "f")) "being" ($#m1_comput_1 :::"Element"::: ) "of" (Set (Var "P")) (Bool "for" (Set (Var "F")) "being" ($#v3_comput_1 :::"with_the_same_arity"::: ) ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "P")) "st" (Bool (Bool (Set ($#k19_margrel1 :::"arity"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "F"))))) "holds" (Bool (Set (Set (Var "f")) ($#k3_relat_1 :::"*"::: ) (Set ($#k6_funct_6 :::"<:"::: ) (Set (Var "F")) ($#k6_funct_6 :::":>"::: ) )) ($#r2_hidden :::"in"::: ) (Set (Var "P")))))) ; theorem :: COMPUT_1:73 (Bool "for" (Set (Var "P")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v6_comput_1 :::"primitive-recursively_closed"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k2_comput_1 :::"HFuncs"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ")" ) (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m1_comput_1 :::"Element"::: ) "of" (Set (Var "P")) "st" (Bool (Bool (Set (Set "(" ($#k19_margrel1 :::"arity"::: ) (Set (Var "f1")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 2)) ($#r1_hidden :::"="::: ) (Set ($#k19_margrel1 :::"arity"::: ) (Set (Var "f2"))))) "holds" (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" ($#k19_margrel1 :::"arity"::: ) (Set (Var "f1")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1)))) "holds" (Bool (Set ($#k7_comput_1 :::"primrec"::: ) "(" (Set (Var "f1")) "," (Set (Var "f2")) "," (Set (Var "i")) ")" ) ($#r2_hidden :::"in"::: ) (Set (Var "P")))))) ; definitionfunc :::"PrimRec"::: -> ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k2_comput_1 :::"HFuncs"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ")" ) equals :: COMPUT_1:def 15 (Set ($#k1_setfam_1 :::"meet"::: ) "{" (Set (Var "R")) where R "is" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k2_comput_1 :::"HFuncs"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ")" ) : (Bool (Set (Var "R")) "is" ($#v6_comput_1 :::"primitive-recursively_closed"::: ) ) "}" ); end; :: deftheorem defines :::"PrimRec"::: COMPUT_1:def 15 : (Bool (Set ($#k9_comput_1 :::"PrimRec"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k1_setfam_1 :::"meet"::: ) "{" (Set (Var "R")) where R "is" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k2_comput_1 :::"HFuncs"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ")" ) : (Bool (Set (Var "R")) "is" ($#v6_comput_1 :::"primitive-recursively_closed"::: ) ) "}" )); theorem :: COMPUT_1:74 (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k2_comput_1 :::"HFuncs"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ")" ) "st" (Bool (Bool (Set (Var "X")) "is" ($#v6_comput_1 :::"primitive-recursively_closed"::: ) )) "holds" (Bool (Set ($#k9_comput_1 :::"PrimRec"::: ) ) ($#r1_tarski :::"c="::: ) (Set (Var "X")))) ; registration cluster (Set ($#k9_comput_1 :::"PrimRec"::: ) ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v6_comput_1 :::"primitive-recursively_closed"::: ) ; end; registration cluster -> ($#v2_margrel1 :::"homogeneous"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_comput_1 :::"PrimRec"::: ) ); end; definitionlet "x" be ($#m1_hidden :::"set"::: ) ; attr "x" is :::"primitive-recursive"::: means :: COMPUT_1:def 16 (Bool "x" ($#r2_hidden :::"in"::: ) (Set ($#k9_comput_1 :::"PrimRec"::: ) )); end; :: deftheorem defines :::"primitive-recursive"::: COMPUT_1:def 16 : (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) "is" ($#v7_comput_1 :::"primitive-recursive"::: ) ) "iff" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_comput_1 :::"PrimRec"::: ) )) ")" )); registration cluster ($#v7_comput_1 :::"primitive-recursive"::: ) -> ($#v1_relat_1 :::"Relation-like"::: ) ($#v1_funct_1 :::"Function-like"::: ) for ($#m1_hidden :::"set"::: ) ; end; registration cluster ($#v1_relat_1 :::"Relation-like"::: ) ($#v7_comput_1 :::"primitive-recursive"::: ) -> (Set (Set ($#k5_numbers :::"NAT"::: ) ) ($#k3_finseq_2 :::"*"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ($#v4_valued_0 :::"to-naturals"::: ) ($#v2_margrel1 :::"homogeneous"::: ) for ($#m1_hidden :::"set"::: ) ; end; registration cluster -> ($#v7_comput_1 :::"primitive-recursive"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_comput_1 :::"PrimRec"::: ) ); end; registration cluster ($#v1_relat_1 :::"Relation-like"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v7_comput_1 :::"primitive-recursive"::: ) for ($#m1_hidden :::"set"::: ) ; cluster ($#v1_relat_1 :::"Relation-like"::: ) (Set (Set ($#k5_numbers :::"NAT"::: ) ) ($#k3_finseq_2 :::"*"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_valued_0 :::"complex-valued"::: ) ($#v2_valued_0 :::"ext-real-valued"::: ) ($#v3_valued_0 :::"real-valued"::: ) ($#v4_valued_0 :::"to-naturals"::: ) ($#v2_margrel1 :::"homogeneous"::: ) ($#v7_comput_1 :::"primitive-recursive"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_comput_1 :::"HFuncs"::: ) (Set ($#k5_numbers :::"NAT"::: ) )); end; definitionfunc :::"initial-funcs"::: -> ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k2_comput_1 :::"HFuncs"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ")" ) equals :: COMPUT_1:def 17 (Set (Set ($#k2_tarski :::"{"::: ) (Set "(" (Set ($#k6_numbers :::"0"::: ) ) ($#k3_comput_1 :::"const"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) "," (Set "(" (Num 1) ($#k4_comput_1 :::"succ"::: ) (Num 1) ")" ) ($#k2_tarski :::"}"::: ) ) ($#k2_xboole_0 :::"\/"::: ) "{" (Set "(" (Set (Var "n")) ($#k5_comput_1 :::"proj"::: ) (Set (Var "i")) ")" ) where n, i "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) : (Bool "(" (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) ")" ) "}" ); let "Q" be ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k2_comput_1 :::"HFuncs"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ")" ); func :::"PR-closure"::: "Q" -> ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k2_comput_1 :::"HFuncs"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ")" ) equals :: COMPUT_1:def 18 (Set "Q" ($#k2_xboole_0 :::"\/"::: ) "{" (Set (Var "g")) where g "is" ($#m2_rfunct_3 :::"Element"::: ) "of" (Set ($#k2_comput_1 :::"HFuncs"::: ) (Set ($#k5_numbers :::"NAT"::: ) )) : (Bool "ex" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m2_rfunct_3 :::"Element"::: ) "of" (Set ($#k2_comput_1 :::"HFuncs"::: ) (Set ($#k5_numbers :::"NAT"::: ) ))(Bool "ex" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set (Var "f1")) ($#r2_hidden :::"in"::: ) "Q") & (Bool (Set (Var "f2")) ($#r2_hidden :::"in"::: ) "Q") & (Bool (Set (Var "g")) ($#r1_comput_1 :::"is_primitive-recursively_expressed_by"::: ) (Set (Var "f1")) "," (Set (Var "f2")) "," (Set (Var "i"))) ")" ))) "}" ); func :::"composition-closure"::: "Q" -> ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k2_comput_1 :::"HFuncs"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ")" ) equals :: COMPUT_1:def 19 (Set "Q" ($#k2_xboole_0 :::"\/"::: ) "{" (Set "(" (Set (Var "f")) ($#k3_relat_1 :::"*"::: ) (Set ($#k6_funct_6 :::"<:"::: ) (Set (Var "F")) ($#k6_funct_6 :::":>"::: ) ) ")" ) where f "is" ($#m2_rfunct_3 :::"Element"::: ) "of" (Set ($#k2_comput_1 :::"HFuncs"::: ) (Set ($#k5_numbers :::"NAT"::: ) )), F "is" ($#v3_comput_1 :::"with_the_same_arity"::: ) ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set "(" ($#k2_comput_1 :::"HFuncs"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ")" ) ($#k3_finseq_2 :::"*"::: ) ) : (Bool "(" (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) "Q") & (Bool (Set ($#k19_margrel1 :::"arity"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "F")))) & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "F"))) ($#r1_tarski :::"c="::: ) "Q") ")" ) "}" ); end; :: deftheorem defines :::"initial-funcs"::: COMPUT_1:def 17 : (Bool (Set ($#k10_comput_1 :::"initial-funcs"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set ($#k2_tarski :::"{"::: ) (Set "(" (Set ($#k6_numbers :::"0"::: ) ) ($#k3_comput_1 :::"const"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) "," (Set "(" (Num 1) ($#k4_comput_1 :::"succ"::: ) (Num 1) ")" ) ($#k2_tarski :::"}"::: ) ) ($#k2_xboole_0 :::"\/"::: ) "{" (Set "(" (Set (Var "n")) ($#k5_comput_1 :::"proj"::: ) (Set (Var "i")) ")" ) where n, i "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) : (Bool "(" (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) ")" ) "}" )); :: deftheorem defines :::"PR-closure"::: COMPUT_1:def 18 : (Bool "for" (Set (Var "Q")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k2_comput_1 :::"HFuncs"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ")" ) "holds" (Bool (Set ($#k11_comput_1 :::"PR-closure"::: ) (Set (Var "Q"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "Q")) ($#k2_xboole_0 :::"\/"::: ) "{" (Set (Var "g")) where g "is" ($#m2_rfunct_3 :::"Element"::: ) "of" (Set ($#k2_comput_1 :::"HFuncs"::: ) (Set ($#k5_numbers :::"NAT"::: ) )) : (Bool "ex" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m2_rfunct_3 :::"Element"::: ) "of" (Set ($#k2_comput_1 :::"HFuncs"::: ) (Set ($#k5_numbers :::"NAT"::: ) ))(Bool "ex" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set (Var "f1")) ($#r2_hidden :::"in"::: ) (Set (Var "Q"))) & (Bool (Set (Var "f2")) ($#r2_hidden :::"in"::: ) (Set (Var "Q"))) & (Bool (Set (Var "g")) ($#r1_comput_1 :::"is_primitive-recursively_expressed_by"::: ) (Set (Var "f1")) "," (Set (Var "f2")) "," (Set (Var "i"))) ")" ))) "}" ))); :: deftheorem defines :::"composition-closure"::: COMPUT_1:def 19 : (Bool "for" (Set (Var "Q")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k2_comput_1 :::"HFuncs"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ")" ) "holds" (Bool (Set ($#k12_comput_1 :::"composition-closure"::: ) (Set (Var "Q"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "Q")) ($#k2_xboole_0 :::"\/"::: ) "{" (Set "(" (Set (Var "f")) ($#k3_relat_1 :::"*"::: ) (Set ($#k6_funct_6 :::"<:"::: ) (Set (Var "F")) ($#k6_funct_6 :::":>"::: ) ) ")" ) where f "is" ($#m2_rfunct_3 :::"Element"::: ) "of" (Set ($#k2_comput_1 :::"HFuncs"::: ) (Set ($#k5_numbers :::"NAT"::: ) )), F "is" ($#v3_comput_1 :::"with_the_same_arity"::: ) ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set "(" ($#k2_comput_1 :::"HFuncs"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ")" ) ($#k3_finseq_2 :::"*"::: ) ) : (Bool "(" (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set (Var "Q"))) & (Bool (Set ($#k19_margrel1 :::"arity"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "F")))) & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "F"))) ($#r1_tarski :::"c="::: ) (Set (Var "Q"))) ")" ) "}" ))); definitionfunc :::"PrimRec-Approximation"::: -> ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "(" ($#k9_setfam_1 :::"bool"::: ) (Set "(" ($#k2_comput_1 :::"HFuncs"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ")" ) ")" ) means :: COMPUT_1:def 20 (Bool "(" (Bool (Set it ($#k8_nat_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k10_comput_1 :::"initial-funcs"::: ) )) & (Bool "(" "for" (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set it ($#k8_nat_1 :::"."::: ) (Set "(" (Set (Var "m")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k11_comput_1 :::"PR-closure"::: ) (Set "(" it ($#k8_nat_1 :::"."::: ) (Set (Var "m")) ")" ) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k12_comput_1 :::"composition-closure"::: ) (Set "(" it ($#k8_nat_1 :::"."::: ) (Set (Var "m")) ")" ) ")" ))) ")" ) ")" ); end; :: deftheorem defines :::"PrimRec-Approximation"::: COMPUT_1:def 20 : (Bool "for" (Set (Var "b1")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "(" ($#k9_setfam_1 :::"bool"::: ) (Set "(" ($#k2_comput_1 :::"HFuncs"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ")" ) ")" ) "holds" (Bool "(" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k13_comput_1 :::"PrimRec-Approximation"::: ) )) "iff" (Bool "(" (Bool (Set (Set (Var "b1")) ($#k8_nat_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k10_comput_1 :::"initial-funcs"::: ) )) & (Bool "(" "for" (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "b1")) ($#k8_nat_1 :::"."::: ) (Set "(" (Set (Var "m")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k11_comput_1 :::"PR-closure"::: ) (Set "(" (Set (Var "b1")) ($#k8_nat_1 :::"."::: ) (Set (Var "m")) ")" ) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k12_comput_1 :::"composition-closure"::: ) (Set "(" (Set (Var "b1")) ($#k8_nat_1 :::"."::: ) (Set (Var "m")) ")" ) ")" ))) ")" ) ")" ) ")" )); theorem :: COMPUT_1:75 (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "m")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n")))) "holds" (Bool (Set (Set ($#k13_comput_1 :::"PrimRec-Approximation"::: ) ) ($#k8_nat_1 :::"."::: ) (Set (Var "m"))) ($#r1_tarski :::"c="::: ) (Set (Set ($#k13_comput_1 :::"PrimRec-Approximation"::: ) ) ($#k8_nat_1 :::"."::: ) (Set (Var "n"))))) ; theorem :: COMPUT_1:76 (Bool (Set ($#k1_prob_1 :::"Union"::: ) (Set ($#k13_comput_1 :::"PrimRec-Approximation"::: ) )) "is" ($#v6_comput_1 :::"primitive-recursively_closed"::: ) ) ; theorem :: COMPUT_1:77 (Bool (Set ($#k9_comput_1 :::"PrimRec"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k1_prob_1 :::"Union"::: ) (Set ($#k13_comput_1 :::"PrimRec-Approximation"::: ) ))) ; theorem :: COMPUT_1:78 (Bool "for" (Set (Var "m")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m2_rfunct_3 :::"Element"::: ) "of" (Set ($#k2_comput_1 :::"HFuncs"::: ) (Set ($#k5_numbers :::"NAT"::: ) )) "st" (Bool (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set (Set ($#k13_comput_1 :::"PrimRec-Approximation"::: ) ) ($#k8_nat_1 :::"."::: ) (Set (Var "m"))))) "holds" (Bool (Set (Var "f")) "is" ($#v3_margrel1 :::"quasi_total"::: ) ))) ; registration cluster -> ($#v2_margrel1 :::"homogeneous"::: ) ($#v3_margrel1 :::"quasi_total"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_comput_1 :::"PrimRec"::: ) ); end; registration cluster ($#v7_comput_1 :::"primitive-recursive"::: ) -> ($#v3_margrel1 :::"quasi_total"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_comput_1 :::"HFuncs"::: ) (Set ($#k5_numbers :::"NAT"::: ) )); end; registration cluster ($#v1_relat_1 :::"Relation-like"::: ) (Set (Set ($#k5_numbers :::"NAT"::: ) ) ($#k3_finseq_2 :::"*"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v7_comput_1 :::"primitive-recursive"::: ) -> (Set (Set ($#k5_numbers :::"NAT"::: ) ) ($#k3_finseq_2 :::"*"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ($#v2_comput_1 :::"len-total"::: ) for ($#m1_hidden :::"set"::: ) ; cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_relat_1 :::"Relation-like"::: ) (Set (Set ($#k5_numbers :::"NAT"::: ) ) ($#k3_finseq_2 :::"*"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_valued_0 :::"complex-valued"::: ) ($#v2_valued_0 :::"ext-real-valued"::: ) ($#v3_valued_0 :::"real-valued"::: ) ($#v4_valued_0 :::"to-naturals"::: ) ($#v2_margrel1 :::"homogeneous"::: ) ($#v3_margrel1 :::"quasi_total"::: ) ($#v7_comput_1 :::"primitive-recursive"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_comput_1 :::"PrimRec"::: ) ); end; begin definitionlet "n" be ($#m1_hidden :::"set"::: ) ; let "f" be ($#v2_margrel1 :::"homogeneous"::: ) ($#m1_hidden :::"Relation":::); attr "f" is "n" :::"-ary"::: means :: COMPUT_1:def 21 (Bool (Set ($#k18_margrel1 :::"arity"::: ) "f") ($#r1_hidden :::"="::: ) "n"); end; :: deftheorem defines :::"-ary"::: COMPUT_1:def 21 : (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#v2_margrel1 :::"homogeneous"::: ) ($#m1_hidden :::"Relation":::) "holds" (Bool "(" (Bool (Set (Var "f")) "is" (Set (Var "n")) ($#v8_comput_1 :::"-ary"::: ) ) "iff" (Bool (Set ($#k18_margrel1 :::"arity"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Var "n"))) ")" ))); registration cluster ($#v1_relat_1 :::"Relation-like"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v2_margrel1 :::"homogeneous"::: ) (Num 1) ($#v8_comput_1 :::"-ary"::: ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_margrel1 :::"homogeneous"::: ) for ($#m1_hidden :::"set"::: ) ; cluster ($#v1_relat_1 :::"Relation-like"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v2_margrel1 :::"homogeneous"::: ) (Num 2) ($#v8_comput_1 :::"-ary"::: ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_margrel1 :::"homogeneous"::: ) for ($#m1_hidden :::"set"::: ) ; cluster ($#v1_relat_1 :::"Relation-like"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v2_margrel1 :::"homogeneous"::: ) (Num 3) ($#v8_comput_1 :::"-ary"::: ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_margrel1 :::"homogeneous"::: ) for ($#m1_hidden :::"set"::: ) ; end; registrationlet "n" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); cluster (Set "n" ($#k5_comput_1 :::"proj"::: ) (Num 1)) -> (Set (Set ($#k5_numbers :::"NAT"::: ) ) ($#k3_finseq_2 :::"*"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ($#v4_valued_0 :::"to-naturals"::: ) ($#v2_margrel1 :::"homogeneous"::: ) ($#v7_comput_1 :::"primitive-recursive"::: ) ; end; registration cluster (Set (Num 2) ($#k5_comput_1 :::"proj"::: ) (Num 2)) -> (Set (Set ($#k5_numbers :::"NAT"::: ) ) ($#k3_finseq_2 :::"*"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ($#v4_valued_0 :::"to-naturals"::: ) ($#v2_margrel1 :::"homogeneous"::: ) ($#v7_comput_1 :::"primitive-recursive"::: ) ; cluster (Set (Num 1) ($#k4_comput_1 :::"succ"::: ) (Num 1)) -> (Set (Set ($#k5_numbers :::"NAT"::: ) ) ($#k3_finseq_2 :::"*"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ($#v4_valued_0 :::"to-naturals"::: ) ($#v2_margrel1 :::"homogeneous"::: ) ($#v7_comput_1 :::"primitive-recursive"::: ) ; cluster (Set (Num 3) ($#k4_comput_1 :::"succ"::: ) (Num 3)) -> (Set (Set ($#k5_numbers :::"NAT"::: ) ) ($#k3_finseq_2 :::"*"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ($#v4_valued_0 :::"to-naturals"::: ) ($#v2_margrel1 :::"homogeneous"::: ) ($#v7_comput_1 :::"primitive-recursive"::: ) ; let "i" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); cluster (Set (Set ($#k6_numbers :::"0"::: ) ) ($#k3_comput_1 :::"const"::: ) "i") -> (Set (Set ($#k5_numbers :::"NAT"::: ) ) ($#k3_finseq_2 :::"*"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ($#v4_valued_0 :::"to-naturals"::: ) ($#v2_margrel1 :::"homogeneous"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#v8_comput_1 :::"-ary"::: ) ; cluster (Set (Num 1) ($#k3_comput_1 :::"const"::: ) "i") -> (Set (Set ($#k5_numbers :::"NAT"::: ) ) ($#k3_finseq_2 :::"*"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ($#v4_valued_0 :::"to-naturals"::: ) ($#v2_margrel1 :::"homogeneous"::: ) (Num 1) ($#v8_comput_1 :::"-ary"::: ) ; cluster (Set (Num 2) ($#k3_comput_1 :::"const"::: ) "i") -> (Set (Set ($#k5_numbers :::"NAT"::: ) ) ($#k3_finseq_2 :::"*"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ($#v4_valued_0 :::"to-naturals"::: ) ($#v2_margrel1 :::"homogeneous"::: ) (Num 2) ($#v8_comput_1 :::"-ary"::: ) ; cluster (Set (Num 3) ($#k3_comput_1 :::"const"::: ) "i") -> (Set (Set ($#k5_numbers :::"NAT"::: ) ) ($#k3_finseq_2 :::"*"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ($#v4_valued_0 :::"to-naturals"::: ) ($#v2_margrel1 :::"homogeneous"::: ) (Num 3) ($#v8_comput_1 :::"-ary"::: ) ; cluster (Set (Num 1) ($#k5_comput_1 :::"proj"::: ) "i") -> (Set (Set ($#k5_numbers :::"NAT"::: ) ) ($#k3_finseq_2 :::"*"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ($#v4_valued_0 :::"to-naturals"::: ) ($#v2_margrel1 :::"homogeneous"::: ) (Num 1) ($#v8_comput_1 :::"-ary"::: ) ; cluster (Set (Num 2) ($#k5_comput_1 :::"proj"::: ) "i") -> (Set (Set ($#k5_numbers :::"NAT"::: ) ) ($#k3_finseq_2 :::"*"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ($#v4_valued_0 :::"to-naturals"::: ) ($#v2_margrel1 :::"homogeneous"::: ) (Num 2) ($#v8_comput_1 :::"-ary"::: ) ; cluster (Set (Num 3) ($#k5_comput_1 :::"proj"::: ) "i") -> (Set (Set ($#k5_numbers :::"NAT"::: ) ) ($#k3_finseq_2 :::"*"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ($#v4_valued_0 :::"to-naturals"::: ) ($#v2_margrel1 :::"homogeneous"::: ) (Num 3) ($#v8_comput_1 :::"-ary"::: ) ; cluster (Set (Num 1) ($#k4_comput_1 :::"succ"::: ) "i") -> (Set (Set ($#k5_numbers :::"NAT"::: ) ) ($#k3_finseq_2 :::"*"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ($#v4_valued_0 :::"to-naturals"::: ) ($#v2_margrel1 :::"homogeneous"::: ) (Num 1) ($#v8_comput_1 :::"-ary"::: ) ; cluster (Set (Num 2) ($#k4_comput_1 :::"succ"::: ) "i") -> (Set (Set ($#k5_numbers :::"NAT"::: ) ) ($#k3_finseq_2 :::"*"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ($#v4_valued_0 :::"to-naturals"::: ) ($#v2_margrel1 :::"homogeneous"::: ) (Num 2) ($#v8_comput_1 :::"-ary"::: ) ; cluster (Set (Num 3) ($#k4_comput_1 :::"succ"::: ) "i") -> (Set (Set ($#k5_numbers :::"NAT"::: ) ) ($#k3_finseq_2 :::"*"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ($#v4_valued_0 :::"to-naturals"::: ) ($#v2_margrel1 :::"homogeneous"::: ) (Num 3) ($#v8_comput_1 :::"-ary"::: ) ; let "j" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); cluster (Set "i" ($#k3_comput_1 :::"const"::: ) "j") -> (Set (Set ($#k5_numbers :::"NAT"::: ) ) ($#k3_finseq_2 :::"*"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ($#v4_valued_0 :::"to-naturals"::: ) ($#v2_margrel1 :::"homogeneous"::: ) ($#v7_comput_1 :::"primitive-recursive"::: ) ; end; registration cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_relat_1 :::"Relation-like"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v2_margrel1 :::"homogeneous"::: ) ($#v7_comput_1 :::"primitive-recursive"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#v8_comput_1 :::"-ary"::: ) for ($#m1_hidden :::"set"::: ) ; cluster ($#v1_relat_1 :::"Relation-like"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v2_margrel1 :::"homogeneous"::: ) ($#v7_comput_1 :::"primitive-recursive"::: ) (Num 1) ($#v8_comput_1 :::"-ary"::: ) for ($#m1_hidden :::"set"::: ) ; cluster ($#v1_relat_1 :::"Relation-like"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v2_margrel1 :::"homogeneous"::: ) ($#v7_comput_1 :::"primitive-recursive"::: ) (Num 2) ($#v8_comput_1 :::"-ary"::: ) for ($#m1_hidden :::"set"::: ) ; cluster ($#v1_relat_1 :::"Relation-like"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v2_margrel1 :::"homogeneous"::: ) ($#v7_comput_1 :::"primitive-recursive"::: ) (Num 3) ($#v8_comput_1 :::"-ary"::: ) for ($#m1_hidden :::"set"::: ) ; end; registration cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_relat_1 :::"Relation-like"::: ) (Set (Set ($#k5_numbers :::"NAT"::: ) ) ($#k3_finseq_2 :::"*"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v4_valued_0 :::"to-naturals"::: ) ($#v2_margrel1 :::"homogeneous"::: ) ($#v2_comput_1 :::"len-total"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#v8_comput_1 :::"-ary"::: ) for ($#m1_hidden :::"set"::: ) ; cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_relat_1 :::"Relation-like"::: ) (Set (Set ($#k5_numbers :::"NAT"::: ) ) ($#k3_finseq_2 :::"*"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v4_valued_0 :::"to-naturals"::: ) ($#v2_margrel1 :::"homogeneous"::: ) ($#v2_comput_1 :::"len-total"::: ) (Num 1) ($#v8_comput_1 :::"-ary"::: ) for ($#m1_hidden :::"set"::: ) ; cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_relat_1 :::"Relation-like"::: ) (Set (Set ($#k5_numbers :::"NAT"::: ) ) ($#k3_finseq_2 :::"*"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v4_valued_0 :::"to-naturals"::: ) ($#v2_margrel1 :::"homogeneous"::: ) ($#v2_comput_1 :::"len-total"::: ) (Num 2) ($#v8_comput_1 :::"-ary"::: ) for ($#m1_hidden :::"set"::: ) ; cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_relat_1 :::"Relation-like"::: ) (Set (Set ($#k5_numbers :::"NAT"::: ) ) ($#k3_finseq_2 :::"*"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v4_valued_0 :::"to-naturals"::: ) ($#v2_margrel1 :::"homogeneous"::: ) ($#v2_comput_1 :::"len-total"::: ) (Num 3) ($#v8_comput_1 :::"-ary"::: ) for ($#m1_hidden :::"set"::: ) ; end; registrationlet "f" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v7_comput_1 :::"primitive-recursive"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#v8_comput_1 :::"-ary"::: ) ($#m1_hidden :::"Function":::); let "g" be ($#v7_comput_1 :::"primitive-recursive"::: ) (Num 2) ($#v8_comput_1 :::"-ary"::: ) ($#m1_hidden :::"Function":::); cluster (Set ($#k7_comput_1 :::"primrec"::: ) "(" "f" "," "g" "," (Num 1) ")" ) -> ($#v7_comput_1 :::"primitive-recursive"::: ) (Num 1) ($#v8_comput_1 :::"-ary"::: ) ; end; registrationlet "f" be ($#v7_comput_1 :::"primitive-recursive"::: ) (Num 1) ($#v8_comput_1 :::"-ary"::: ) ($#m1_hidden :::"Function":::); let "g" be ($#v7_comput_1 :::"primitive-recursive"::: ) (Num 3) ($#v8_comput_1 :::"-ary"::: ) ($#m1_hidden :::"Function":::); cluster (Set ($#k7_comput_1 :::"primrec"::: ) "(" "f" "," "g" "," (Num 1) ")" ) -> ($#v7_comput_1 :::"primitive-recursive"::: ) (Num 2) ($#v8_comput_1 :::"-ary"::: ) ; cluster (Set ($#k7_comput_1 :::"primrec"::: ) "(" "f" "," "g" "," (Num 2) ")" ) -> ($#v7_comput_1 :::"primitive-recursive"::: ) (Num 2) ($#v8_comput_1 :::"-ary"::: ) ; end; theorem :: COMPUT_1:79 (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "f1")) "being" (Set (Set ($#k5_numbers :::"NAT"::: ) ) ($#k3_finseq_2 :::"*"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ($#v4_valued_0 :::"to-naturals"::: ) ($#v2_margrel1 :::"homogeneous"::: ) ($#v2_comput_1 :::"len-total"::: ) (Num 1) ($#v8_comput_1 :::"-ary"::: ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "f2")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) (Set (Set ($#k5_numbers :::"NAT"::: ) ) ($#k3_finseq_2 :::"*"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ($#v4_valued_0 :::"to-naturals"::: ) ($#v2_margrel1 :::"homogeneous"::: ) ($#m1_hidden :::"Function":::) "holds" (Bool (Set (Set "(" ($#k7_comput_1 :::"primrec"::: ) "(" (Set (Var "f1")) "," (Set (Var "f2")) "," (Num 2) ")" ")" ) ($#k1_recdef_1 :::"."::: ) (Set ($#k2_finseq_4 :::"<*"::: ) (Set (Var "i")) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k2_finseq_4 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set (Var "f1")) ($#k1_recdef_1 :::"."::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "i")) ($#k12_finseq_1 :::"*>"::: ) )))))) ; theorem :: COMPUT_1:80 (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) (Set (Set ($#k5_numbers :::"NAT"::: ) ) ($#k3_finseq_2 :::"*"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ($#v4_valued_0 :::"to-naturals"::: ) ($#v2_margrel1 :::"homogeneous"::: ) ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "f1")) "is" ($#v2_comput_1 :::"len-total"::: ) ) & (Bool (Set ($#k19_margrel1 :::"arity"::: ) (Set (Var "f1"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set "(" ($#k7_comput_1 :::"primrec"::: ) "(" (Set (Var "f1")) "," (Set (Var "f2")) "," (Num 1) ")" ")" ) ($#k1_recdef_1 :::"."::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k12_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set (Var "f1")) ($#k1_recdef_1 :::"."::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )))) ; theorem :: COMPUT_1:81 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "f1")) "being" (Set (Set ($#k5_numbers :::"NAT"::: ) ) ($#k3_finseq_2 :::"*"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ($#v4_valued_0 :::"to-naturals"::: ) ($#v2_margrel1 :::"homogeneous"::: ) ($#v2_comput_1 :::"len-total"::: ) (Num 1) ($#v8_comput_1 :::"-ary"::: ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "f2")) "being" (Set (Set ($#k5_numbers :::"NAT"::: ) ) ($#k3_finseq_2 :::"*"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ($#v4_valued_0 :::"to-naturals"::: ) ($#v2_margrel1 :::"homogeneous"::: ) ($#v2_comput_1 :::"len-total"::: ) (Num 3) ($#v8_comput_1 :::"-ary"::: ) ($#m1_hidden :::"Function":::) "holds" (Bool (Set (Set "(" ($#k7_comput_1 :::"primrec"::: ) "(" (Set (Var "f1")) "," (Set (Var "f2")) "," (Num 2) ")" ")" ) ($#k1_recdef_1 :::"."::: ) (Set ($#k2_finseq_4 :::"<*"::: ) (Set (Var "i")) "," (Set "(" (Set (Var "j")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ($#k2_finseq_4 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set (Var "f2")) ($#k1_recdef_1 :::"."::: ) (Set ($#k3_finseq_4 :::"<*"::: ) (Set (Var "i")) "," (Set (Var "j")) "," (Set "(" (Set "(" ($#k7_comput_1 :::"primrec"::: ) "(" (Set (Var "f1")) "," (Set (Var "f2")) "," (Num 2) ")" ")" ) ($#k1_recdef_1 :::"."::: ) (Set ($#k2_finseq_4 :::"<*"::: ) (Set (Var "i")) "," (Set (Var "j")) ($#k2_finseq_4 :::"*>"::: ) ) ")" ) ($#k3_finseq_4 :::"*>"::: ) )))))) ; theorem :: COMPUT_1:82 (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) (Set (Set ($#k5_numbers :::"NAT"::: ) ) ($#k3_finseq_2 :::"*"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ($#v4_valued_0 :::"to-naturals"::: ) ($#v2_margrel1 :::"homogeneous"::: ) ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "f1")) "is" ($#v2_comput_1 :::"len-total"::: ) ) & (Bool (Set (Var "f2")) "is" ($#v2_comput_1 :::"len-total"::: ) ) & (Bool (Set ($#k19_margrel1 :::"arity"::: ) (Set (Var "f1"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k19_margrel1 :::"arity"::: ) (Set (Var "f2"))) ($#r1_hidden :::"="::: ) (Num 2))) "holds" (Bool (Set (Set "(" ($#k7_comput_1 :::"primrec"::: ) "(" (Set (Var "f1")) "," (Set (Var "f2")) "," (Num 1) ")" ")" ) ($#k1_recdef_1 :::"."::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ($#k12_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set (Var "f2")) ($#k1_recdef_1 :::"."::: ) (Set ($#k2_finseq_4 :::"<*"::: ) (Set (Var "i")) "," (Set "(" (Set "(" ($#k7_comput_1 :::"primrec"::: ) "(" (Set (Var "f1")) "," (Set (Var "f2")) "," (Num 1) ")" ")" ) ($#k1_recdef_1 :::"."::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "i")) ($#k12_finseq_1 :::"*>"::: ) ) ")" ) ($#k2_finseq_4 :::"*>"::: ) ))))) ; definitionlet "g" be ($#m1_hidden :::"Function":::); func :::"(1,2)->(1,?,2)"::: "g" -> ($#m1_hidden :::"Function":::) equals :: COMPUT_1:def 22 (Set "g" ($#k3_relat_1 :::"*"::: ) (Set ($#k6_funct_6 :::"<:"::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set "(" (Num 3) ($#k5_comput_1 :::"proj"::: ) (Num 1) ")" ) "," (Set "(" (Num 3) ($#k5_comput_1 :::"proj"::: ) (Num 3) ")" ) ($#k10_finseq_1 :::"*>"::: ) ) ($#k6_funct_6 :::":>"::: ) )); end; :: deftheorem defines :::"(1,2)->(1,?,2)"::: COMPUT_1:def 22 : (Bool "for" (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool (Set ($#k14_comput_1 :::"(1,2)->(1,?,2)"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k3_relat_1 :::"*"::: ) (Set ($#k6_funct_6 :::"<:"::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set "(" (Num 3) ($#k5_comput_1 :::"proj"::: ) (Num 1) ")" ) "," (Set "(" (Num 3) ($#k5_comput_1 :::"proj"::: ) (Num 3) ")" ) ($#k10_finseq_1 :::"*>"::: ) ) ($#k6_funct_6 :::":>"::: ) )))); registrationlet "g" be (Set (Set ($#k5_numbers :::"NAT"::: ) ) ($#k3_finseq_2 :::"*"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ($#v4_valued_0 :::"to-naturals"::: ) ($#m1_hidden :::"Function":::); cluster (Set ($#k14_comput_1 :::"(1,2)->(1,?,2)"::: ) "g") -> (Set (Set ($#k5_numbers :::"NAT"::: ) ) ($#k3_finseq_2 :::"*"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ($#v4_valued_0 :::"to-naturals"::: ) ; end; registrationlet "g" be ($#v2_margrel1 :::"homogeneous"::: ) ($#m1_hidden :::"Function":::); cluster (Set ($#k14_comput_1 :::"(1,2)->(1,?,2)"::: ) "g") -> ($#v2_margrel1 :::"homogeneous"::: ) ; end; registrationlet "g" be (Set (Set ($#k5_numbers :::"NAT"::: ) ) ($#k3_finseq_2 :::"*"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ($#v4_valued_0 :::"to-naturals"::: ) ($#v2_margrel1 :::"homogeneous"::: ) ($#v2_comput_1 :::"len-total"::: ) (Num 2) ($#v8_comput_1 :::"-ary"::: ) ($#m1_hidden :::"Function":::); cluster (Set ($#k14_comput_1 :::"(1,2)->(1,?,2)"::: ) "g") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_comput_1 :::"len-total"::: ) (Num 3) ($#v8_comput_1 :::"-ary"::: ) ; end; theorem :: COMPUT_1:83 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "f")) "being" (Set (Set ($#k5_numbers :::"NAT"::: ) ) ($#k3_finseq_2 :::"*"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ($#v4_valued_0 :::"to-naturals"::: ) ($#v2_margrel1 :::"homogeneous"::: ) ($#v2_comput_1 :::"len-total"::: ) (Num 2) ($#v8_comput_1 :::"-ary"::: ) ($#m1_hidden :::"Function":::) "holds" (Bool (Set (Set "(" ($#k14_comput_1 :::"(1,2)->(1,?,2)"::: ) (Set (Var "f")) ")" ) ($#k1_recdef_1 :::"."::: ) (Set ($#k3_finseq_4 :::"<*"::: ) (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "k")) ($#k3_finseq_4 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_recdef_1 :::"."::: ) (Set ($#k2_finseq_4 :::"<*"::: ) (Set (Var "i")) "," (Set (Var "k")) ($#k2_finseq_4 :::"*>"::: ) ))))) ; theorem :: COMPUT_1:84 (Bool "for" (Set (Var "g")) "being" ($#v7_comput_1 :::"primitive-recursive"::: ) (Num 2) ($#v8_comput_1 :::"-ary"::: ) ($#m1_hidden :::"Function":::) "holds" (Bool (Set ($#k14_comput_1 :::"(1,2)->(1,?,2)"::: ) (Set (Var "g"))) ($#r2_hidden :::"in"::: ) (Set ($#k9_comput_1 :::"PrimRec"::: ) ))) ; registrationlet "f" be ($#v2_margrel1 :::"homogeneous"::: ) ($#v7_comput_1 :::"primitive-recursive"::: ) (Num 2) ($#v8_comput_1 :::"-ary"::: ) ($#m1_hidden :::"Function":::); cluster (Set ($#k14_comput_1 :::"(1,2)->(1,?,2)"::: ) "f") -> ($#v7_comput_1 :::"primitive-recursive"::: ) (Num 3) ($#v8_comput_1 :::"-ary"::: ) ; end; definitionfunc :::"[+]"::: -> ($#v7_comput_1 :::"primitive-recursive"::: ) (Num 2) ($#v8_comput_1 :::"-ary"::: ) ($#m1_hidden :::"Function":::) equals :: COMPUT_1:def 23 (Set ($#k7_comput_1 :::"primrec"::: ) "(" (Set "(" (Num 1) ($#k5_comput_1 :::"proj"::: ) (Num 1) ")" ) "," (Set "(" (Num 3) ($#k4_comput_1 :::"succ"::: ) (Num 3) ")" ) "," (Num 2) ")" ); end; :: deftheorem defines :::"[+]"::: COMPUT_1:def 23 : (Bool (Set ($#k15_comput_1 :::"[+]"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k7_comput_1 :::"primrec"::: ) "(" (Set "(" (Num 1) ($#k5_comput_1 :::"proj"::: ) (Num 1) ")" ) "," (Set "(" (Num 3) ($#k4_comput_1 :::"succ"::: ) (Num 3) ")" ) "," (Num 2) ")" )); theorem :: COMPUT_1:85 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set ($#k15_comput_1 :::"[+]"::: ) ) ($#k1_recdef_1 :::"."::: ) (Set ($#k2_finseq_4 :::"<*"::: ) (Set (Var "i")) "," (Set (Var "j")) ($#k2_finseq_4 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Set (Var "j"))))) ; definitionfunc :::"[*]"::: -> ($#v7_comput_1 :::"primitive-recursive"::: ) (Num 2) ($#v8_comput_1 :::"-ary"::: ) ($#m1_hidden :::"Function":::) equals :: COMPUT_1:def 24 (Set ($#k7_comput_1 :::"primrec"::: ) "(" (Set "(" (Num 1) ($#k3_comput_1 :::"const"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) "," (Set "(" ($#k14_comput_1 :::"(1,2)->(1,?,2)"::: ) (Set ($#k15_comput_1 :::"[+]"::: ) ) ")" ) "," (Num 2) ")" ); end; :: deftheorem defines :::"[*]"::: COMPUT_1:def 24 : (Bool (Set ($#k16_comput_1 :::"[*]"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k7_comput_1 :::"primrec"::: ) "(" (Set "(" (Num 1) ($#k3_comput_1 :::"const"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) "," (Set "(" ($#k14_comput_1 :::"(1,2)->(1,?,2)"::: ) (Set ($#k15_comput_1 :::"[+]"::: ) ) ")" ) "," (Num 2) ")" )); theorem :: COMPUT_1:86 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set ($#k16_comput_1 :::"[*]"::: ) ) ($#k1_recdef_1 :::"."::: ) (Set ($#k2_finseq_4 :::"<*"::: ) (Set (Var "i")) "," (Set (Var "j")) ($#k2_finseq_4 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set (Var "i")) ($#k4_nat_1 :::"*"::: ) (Set (Var "j"))))) ; registrationlet "g", "h" be ($#v2_margrel1 :::"homogeneous"::: ) ($#v7_comput_1 :::"primitive-recursive"::: ) (Num 2) ($#v8_comput_1 :::"-ary"::: ) ($#m1_hidden :::"Function":::); cluster (Set ($#k10_finseq_1 :::"<*"::: ) "g" "," "h" ($#k10_finseq_1 :::"*>"::: ) ) -> ($#v3_comput_1 :::"with_the_same_arity"::: ) ; end; registrationlet "f", "g", "h" be ($#v7_comput_1 :::"primitive-recursive"::: ) (Num 2) ($#v8_comput_1 :::"-ary"::: ) ($#m1_hidden :::"Function":::); cluster (Set (Set ($#k6_funct_6 :::"<:"::: ) (Set ($#k10_finseq_1 :::"<*"::: ) "g" "," "h" ($#k10_finseq_1 :::"*>"::: ) ) ($#k6_funct_6 :::":>"::: ) ) ($#k3_relat_1 :::"*"::: ) "f") -> ($#v7_comput_1 :::"primitive-recursive"::: ) ; end; registrationlet "f", "g", "h" be ($#v7_comput_1 :::"primitive-recursive"::: ) (Num 2) ($#v8_comput_1 :::"-ary"::: ) ($#m1_hidden :::"Function":::); cluster (Set (Set ($#k6_funct_6 :::"<:"::: ) (Set ($#k10_finseq_1 :::"<*"::: ) "g" "," "h" ($#k10_finseq_1 :::"*>"::: ) ) ($#k6_funct_6 :::":>"::: ) ) ($#k3_relat_1 :::"*"::: ) "f") -> (Num 2) ($#v8_comput_1 :::"-ary"::: ) ; end; registrationlet "f" be ($#v7_comput_1 :::"primitive-recursive"::: ) (Num 1) ($#v8_comput_1 :::"-ary"::: ) ($#m1_hidden :::"Function":::); let "g" be ($#v7_comput_1 :::"primitive-recursive"::: ) ($#m1_hidden :::"Function":::); cluster (Set (Set ($#k6_funct_6 :::"<:"::: ) (Set ($#k9_finseq_1 :::"<*"::: ) "g" ($#k9_finseq_1 :::"*>"::: ) ) ($#k6_funct_6 :::":>"::: ) ) ($#k3_relat_1 :::"*"::: ) "f") -> ($#v7_comput_1 :::"primitive-recursive"::: ) ; end; registrationlet "f" be ($#v7_comput_1 :::"primitive-recursive"::: ) (Num 1) ($#v8_comput_1 :::"-ary"::: ) ($#m1_hidden :::"Function":::); let "g" be ($#v7_comput_1 :::"primitive-recursive"::: ) (Num 2) ($#v8_comput_1 :::"-ary"::: ) ($#m1_hidden :::"Function":::); cluster (Set (Set ($#k6_funct_6 :::"<:"::: ) (Set ($#k9_finseq_1 :::"<*"::: ) "g" ($#k9_finseq_1 :::"*>"::: ) ) ($#k6_funct_6 :::":>"::: ) ) ($#k3_relat_1 :::"*"::: ) "f") -> (Num 2) ($#v8_comput_1 :::"-ary"::: ) ; end; definitionfunc :::"[!]"::: -> ($#v7_comput_1 :::"primitive-recursive"::: ) (Num 1) ($#v8_comput_1 :::"-ary"::: ) ($#m1_hidden :::"Function":::) equals :: COMPUT_1:def 25 (Set ($#k7_comput_1 :::"primrec"::: ) "(" (Set "(" (Set ($#k6_numbers :::"0"::: ) ) ($#k3_comput_1 :::"const"::: ) (Num 1) ")" ) "," (Set "(" (Set ($#k16_comput_1 :::"[*]"::: ) ) ($#k3_relat_1 :::"*"::: ) (Set ($#k6_funct_6 :::"<:"::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set "(" (Set "(" (Num 1) ($#k4_comput_1 :::"succ"::: ) (Num 1) ")" ) ($#k3_relat_1 :::"*"::: ) (Set ($#k6_funct_6 :::"<:"::: ) (Set ($#k9_finseq_1 :::"<*"::: ) (Set "(" (Num 2) ($#k5_comput_1 :::"proj"::: ) (Num 1) ")" ) ($#k9_finseq_1 :::"*>"::: ) ) ($#k6_funct_6 :::":>"::: ) ) ")" ) "," (Set "(" (Num 2) ($#k5_comput_1 :::"proj"::: ) (Num 2) ")" ) ($#k10_finseq_1 :::"*>"::: ) ) ($#k6_funct_6 :::":>"::: ) ) ")" ) "," (Num 1) ")" ); end; :: deftheorem defines :::"[!]"::: COMPUT_1:def 25 : (Bool (Set ($#k17_comput_1 :::"[!]"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k7_comput_1 :::"primrec"::: ) "(" (Set "(" (Set ($#k6_numbers :::"0"::: ) ) ($#k3_comput_1 :::"const"::: ) (Num 1) ")" ) "," (Set "(" (Set ($#k16_comput_1 :::"[*]"::: ) ) ($#k3_relat_1 :::"*"::: ) (Set ($#k6_funct_6 :::"<:"::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set "(" (Set "(" (Num 1) ($#k4_comput_1 :::"succ"::: ) (Num 1) ")" ) ($#k3_relat_1 :::"*"::: ) (Set ($#k6_funct_6 :::"<:"::: ) (Set ($#k9_finseq_1 :::"<*"::: ) (Set "(" (Num 2) ($#k5_comput_1 :::"proj"::: ) (Num 1) ")" ) ($#k9_finseq_1 :::"*>"::: ) ) ($#k6_funct_6 :::":>"::: ) ) ")" ) "," (Set "(" (Num 2) ($#k5_comput_1 :::"proj"::: ) (Num 2) ")" ) ($#k10_finseq_1 :::"*>"::: ) ) ($#k6_funct_6 :::":>"::: ) ) ")" ) "," (Num 1) ")" )); scheme :: COMPUT_1:sch 1 Primrec1{ F1() -> (Set (Set ($#k5_numbers :::"NAT"::: ) ) ($#k3_finseq_2 :::"*"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ($#v4_valued_0 :::"to-naturals"::: ) ($#v2_margrel1 :::"homogeneous"::: ) ($#v2_comput_1 :::"len-total"::: ) (Num 1) ($#v8_comput_1 :::"-ary"::: ) ($#m1_hidden :::"Function":::), F2() -> (Set (Set ($#k5_numbers :::"NAT"::: ) ) ($#k3_finseq_2 :::"*"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ($#v4_valued_0 :::"to-naturals"::: ) ($#v2_margrel1 :::"homogeneous"::: ) ($#v2_comput_1 :::"len-total"::: ) (Num 2) ($#v8_comput_1 :::"-ary"::: ) ($#m1_hidden :::"Function":::), F3( ($#m1_hidden :::"set"::: ) ) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ), F4( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) } : (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set "(" (Set F1 "(" ")" ) ($#k3_relat_1 :::"*"::: ) (Set ($#k6_funct_6 :::"<:"::: ) (Set ($#k9_finseq_1 :::"<*"::: ) (Set F2 "(" ")" ) ($#k9_finseq_1 :::"*>"::: ) ) ($#k6_funct_6 :::":>"::: ) ) ")" ) ($#k1_recdef_1 :::"."::: ) (Set ($#k2_finseq_4 :::"<*"::: ) (Set (Var "i")) "," (Set (Var "j")) ($#k2_finseq_4 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set F3 "(" (Set F4 "(" (Set (Var "i")) "," (Set (Var "j")) ")" ) ")" ))) provided (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set F1 "(" ")" ) ($#k1_recdef_1 :::"."::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "i")) ($#k12_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set F3 "(" (Set (Var "i")) ")" ))) and (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set F2 "(" ")" ) ($#k1_recdef_1 :::"."::: ) (Set ($#k2_finseq_4 :::"<*"::: ) (Set (Var "i")) "," (Set (Var "j")) ($#k2_finseq_4 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set F4 "(" (Set (Var "i")) "," (Set (Var "j")) ")" ))) proof end; scheme :: COMPUT_1:sch 2 Primrec2{ F1() -> (Set (Set ($#k5_numbers :::"NAT"::: ) ) ($#k3_finseq_2 :::"*"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ($#v4_valued_0 :::"to-naturals"::: ) ($#v2_margrel1 :::"homogeneous"::: ) ($#v2_comput_1 :::"len-total"::: ) (Num 2) ($#v8_comput_1 :::"-ary"::: ) ($#m1_hidden :::"Function":::), F2() -> (Set (Set ($#k5_numbers :::"NAT"::: ) ) ($#k3_finseq_2 :::"*"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ($#v4_valued_0 :::"to-naturals"::: ) ($#v2_margrel1 :::"homogeneous"::: ) ($#v2_comput_1 :::"len-total"::: ) (Num 2) ($#v8_comput_1 :::"-ary"::: ) ($#m1_hidden :::"Function":::), F3() -> (Set (Set ($#k5_numbers :::"NAT"::: ) ) ($#k3_finseq_2 :::"*"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ($#v4_valued_0 :::"to-naturals"::: ) ($#v2_margrel1 :::"homogeneous"::: ) ($#v2_comput_1 :::"len-total"::: ) (Num 2) ($#v8_comput_1 :::"-ary"::: ) ($#m1_hidden :::"Function":::), F4( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ), F5( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ), F6( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) } : (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set "(" (Set F1 "(" ")" ) ($#k3_relat_1 :::"*"::: ) (Set ($#k6_funct_6 :::"<:"::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set F2 "(" ")" ) "," (Set F3 "(" ")" ) ($#k10_finseq_1 :::"*>"::: ) ) ($#k6_funct_6 :::":>"::: ) ) ")" ) ($#k1_recdef_1 :::"."::: ) (Set ($#k2_finseq_4 :::"<*"::: ) (Set (Var "i")) "," (Set (Var "j")) ($#k2_finseq_4 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set F4 "(" (Set F5 "(" (Set (Var "i")) "," (Set (Var "j")) ")" ) "," (Set F6 "(" (Set (Var "i")) "," (Set (Var "j")) ")" ) ")" ))) provided (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set F1 "(" ")" ) ($#k1_recdef_1 :::"."::: ) (Set ($#k2_finseq_4 :::"<*"::: ) (Set (Var "i")) "," (Set (Var "j")) ($#k2_finseq_4 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set F4 "(" (Set (Var "i")) "," (Set (Var "j")) ")" ))) and (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set F2 "(" ")" ) ($#k1_recdef_1 :::"."::: ) (Set ($#k2_finseq_4 :::"<*"::: ) (Set (Var "i")) "," (Set (Var "j")) ($#k2_finseq_4 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set F5 "(" (Set (Var "i")) "," (Set (Var "j")) ")" ))) and (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set F3 "(" ")" ) ($#k1_recdef_1 :::"."::: ) (Set ($#k2_finseq_4 :::"<*"::: ) (Set (Var "i")) "," (Set (Var "j")) ($#k2_finseq_4 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set F6 "(" (Set (Var "i")) "," (Set (Var "j")) ")" ))) proof end; theorem :: COMPUT_1:87 (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set ($#k17_comput_1 :::"[!]"::: ) ) ($#k1_recdef_1 :::"."::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "i")) ($#k12_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set (Var "i")) ($#k9_newton :::"!"::: ) ))) ; definitionfunc :::"[^]"::: -> ($#v7_comput_1 :::"primitive-recursive"::: ) (Num 2) ($#v8_comput_1 :::"-ary"::: ) ($#m1_hidden :::"Function":::) equals :: COMPUT_1:def 26 (Set ($#k7_comput_1 :::"primrec"::: ) "(" (Set "(" (Num 1) ($#k3_comput_1 :::"const"::: ) (Num 1) ")" ) "," (Set "(" ($#k14_comput_1 :::"(1,2)->(1,?,2)"::: ) (Set ($#k16_comput_1 :::"[*]"::: ) ) ")" ) "," (Num 2) ")" ); end; :: deftheorem defines :::"[^]"::: COMPUT_1:def 26 : (Bool (Set ($#k18_comput_1 :::"[^]"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k7_comput_1 :::"primrec"::: ) "(" (Set "(" (Num 1) ($#k3_comput_1 :::"const"::: ) (Num 1) ")" ) "," (Set "(" ($#k14_comput_1 :::"(1,2)->(1,?,2)"::: ) (Set ($#k16_comput_1 :::"[*]"::: ) ) ")" ) "," (Num 2) ")" )); theorem :: COMPUT_1:88 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set ($#k18_comput_1 :::"[^]"::: ) ) ($#k1_recdef_1 :::"."::: ) (Set ($#k2_finseq_4 :::"<*"::: ) (Set (Var "i")) "," (Set (Var "j")) ($#k2_finseq_4 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set (Var "i")) ($#k13_newton :::"|^"::: ) (Set (Var "j"))))) ; definitionfunc :::"[pred]"::: -> ($#v7_comput_1 :::"primitive-recursive"::: ) (Num 1) ($#v8_comput_1 :::"-ary"::: ) ($#m1_hidden :::"Function":::) equals :: COMPUT_1:def 27 (Set ($#k7_comput_1 :::"primrec"::: ) "(" (Set "(" (Set ($#k6_numbers :::"0"::: ) ) ($#k3_comput_1 :::"const"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) "," (Set "(" (Num 2) ($#k5_comput_1 :::"proj"::: ) (Num 1) ")" ) "," (Num 1) ")" ); end; :: deftheorem defines :::"[pred]"::: COMPUT_1:def 27 : (Bool (Set ($#k19_comput_1 :::"[pred]"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k7_comput_1 :::"primrec"::: ) "(" (Set "(" (Set ($#k6_numbers :::"0"::: ) ) ($#k3_comput_1 :::"const"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) "," (Set "(" (Num 2) ($#k5_comput_1 :::"proj"::: ) (Num 1) ")" ) "," (Num 1) ")" )); theorem :: COMPUT_1:89 (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set (Set ($#k19_comput_1 :::"[pred]"::: ) ) ($#k1_recdef_1 :::"."::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k12_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set ($#k19_comput_1 :::"[pred]"::: ) ) ($#k1_recdef_1 :::"."::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ($#k12_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set (Var "i"))) ")" )) ; definitionfunc :::"[-]"::: -> ($#v7_comput_1 :::"primitive-recursive"::: ) (Num 2) ($#v8_comput_1 :::"-ary"::: ) ($#m1_hidden :::"Function":::) equals :: COMPUT_1:def 28 (Set ($#k7_comput_1 :::"primrec"::: ) "(" (Set "(" (Num 1) ($#k5_comput_1 :::"proj"::: ) (Num 1) ")" ) "," (Set "(" ($#k14_comput_1 :::"(1,2)->(1,?,2)"::: ) (Set "(" (Set ($#k19_comput_1 :::"[pred]"::: ) ) ($#k3_relat_1 :::"*"::: ) (Set ($#k6_funct_6 :::"<:"::: ) (Set ($#k9_finseq_1 :::"<*"::: ) (Set "(" (Num 2) ($#k5_comput_1 :::"proj"::: ) (Num 2) ")" ) ($#k9_finseq_1 :::"*>"::: ) ) ($#k6_funct_6 :::":>"::: ) ) ")" ) ")" ) "," (Num 2) ")" ); end; :: deftheorem defines :::"[-]"::: COMPUT_1:def 28 : (Bool (Set ($#k20_comput_1 :::"[-]"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k7_comput_1 :::"primrec"::: ) "(" (Set "(" (Num 1) ($#k5_comput_1 :::"proj"::: ) (Num 1) ")" ) "," (Set "(" ($#k14_comput_1 :::"(1,2)->(1,?,2)"::: ) (Set "(" (Set ($#k19_comput_1 :::"[pred]"::: ) ) ($#k3_relat_1 :::"*"::: ) (Set ($#k6_funct_6 :::"<:"::: ) (Set ($#k9_finseq_1 :::"<*"::: ) (Set "(" (Num 2) ($#k5_comput_1 :::"proj"::: ) (Num 2) ")" ) ($#k9_finseq_1 :::"*>"::: ) ) ($#k6_funct_6 :::":>"::: ) ) ")" ) ")" ) "," (Num 2) ")" )); theorem :: COMPUT_1:90 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set ($#k20_comput_1 :::"[-]"::: ) ) ($#k1_recdef_1 :::"."::: ) (Set ($#k2_finseq_4 :::"<*"::: ) (Set (Var "i")) "," (Set (Var "j")) ($#k2_finseq_4 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set (Var "i")) ($#k7_nat_d :::"-'"::: ) (Set (Var "j"))))) ;