:: COMPOS_0 semantic presentation begin definitionlet "S" be ($#m1_hidden :::"set"::: ) ; attr "S" is :::"standard-ins"::: means :: COMPOS_0:def 1 (Bool "ex" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "st" (Bool "S" ($#r1_tarski :::"c="::: ) (Set ($#k3_zfmisc_1 :::"[:"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "(" (Set ($#k5_numbers :::"NAT"::: ) ) ($#k13_finseq_1 :::"*"::: ) ")" ) "," (Set "(" (Set (Var "X")) ($#k13_finseq_1 :::"*"::: ) ")" ) ($#k3_zfmisc_1 :::":]"::: ) ))); end; :: deftheorem defines :::"standard-ins"::: COMPOS_0:def 1 : (Bool "for" (Set (Var "S")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "S")) "is" ($#v1_compos_0 :::"standard-ins"::: ) ) "iff" (Bool "ex" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "st" (Bool (Set (Var "S")) ($#r1_tarski :::"c="::: ) (Set ($#k3_zfmisc_1 :::"[:"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "(" (Set ($#k5_numbers :::"NAT"::: ) ) ($#k13_finseq_1 :::"*"::: ) ")" ) "," (Set "(" (Set (Var "X")) ($#k13_finseq_1 :::"*"::: ) ")" ) ($#k3_zfmisc_1 :::":]"::: ) ))) ")" )); registration cluster (Set ($#k1_tarski :::"{"::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k3_xtuple_0 :::"]"::: ) ) ($#k1_tarski :::"}"::: ) ) -> ($#v1_compos_0 :::"standard-ins"::: ) ; cluster (Set ($#k1_tarski :::"{"::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Num 1) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k3_xtuple_0 :::"]"::: ) ) ($#k1_tarski :::"}"::: ) ) -> ($#v1_compos_0 :::"standard-ins"::: ) ; end; notationlet "x" be ($#m1_hidden :::"set"::: ) ; synonym :::"InsCode"::: "x" for "x" :::"`1_3"::: ; synonym :::"JumpPart"::: "x" for "x" :::"`2_3"::: ; synonym :::"AddressPart"::: "x" for "x" :::"`3_3"::: ; end; registration cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_compos_0 :::"standard-ins"::: ) for ($#m1_hidden :::"set"::: ) ; end; registrationlet "S" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_compos_0 :::"standard-ins"::: ) ($#m1_hidden :::"set"::: ) ; let "I" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "S")); cluster (Set ($#k2_xtuple_0 :::"AddressPart"::: ) "I") -> ($#v1_relat_1 :::"Relation-like"::: ) ($#v1_funct_1 :::"Function-like"::: ) ; cluster (Set ($#k5_xtuple_0 :::"JumpPart"::: ) "I") -> ($#v1_relat_1 :::"Relation-like"::: ) ($#v1_funct_1 :::"Function-like"::: ) ; end; registrationlet "S" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_compos_0 :::"standard-ins"::: ) ($#m1_hidden :::"set"::: ) ; let "I" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "S")); cluster (Set ($#k2_xtuple_0 :::"AddressPart"::: ) "I") -> ($#v1_finseq_1 :::"FinSequence-like"::: ) ; cluster (Set ($#k5_xtuple_0 :::"JumpPart"::: ) "I") -> ($#v1_finseq_1 :::"FinSequence-like"::: ) ; end; registrationlet "S" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_compos_0 :::"standard-ins"::: ) ($#m1_hidden :::"set"::: ) ; let "x" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "S")); cluster (Set ($#k4_xtuple_0 :::"InsCode"::: ) "x") -> ($#v7_ordinal1 :::"natural"::: ) ; end; registration cluster ($#v1_compos_0 :::"standard-ins"::: ) -> ($#v1_relat_1 :::"Relation-like"::: ) for ($#m1_hidden :::"set"::: ) ; end; definitionlet "S" be ($#v1_compos_0 :::"standard-ins"::: ) ($#m1_hidden :::"set"::: ) ; func :::"InsCodes"::: "S" -> ($#m1_hidden :::"set"::: ) equals :: COMPOS_0:def 2 (Set ($#k11_xtuple_0 :::"proj1_3"::: ) "S"); end; :: deftheorem defines :::"InsCodes"::: COMPOS_0:def 2 : (Bool "for" (Set (Var "S")) "being" ($#v1_compos_0 :::"standard-ins"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k1_compos_0 :::"InsCodes"::: ) (Set (Var "S"))) ($#r1_hidden :::"="::: ) (Set ($#k11_xtuple_0 :::"proj1_3"::: ) (Set (Var "S"))))); registrationlet "S" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_compos_0 :::"standard-ins"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k1_compos_0 :::"InsCodes"::: ) "S") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; definitionlet "S" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_compos_0 :::"standard-ins"::: ) ($#m1_hidden :::"set"::: ) ; mode InsType of "S" is ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_compos_0 :::"InsCodes"::: ) "S"); end; definitionlet "S" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_compos_0 :::"standard-ins"::: ) ($#m1_hidden :::"set"::: ) ; let "I" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "S")); :: original: :::"InsCode"::: redefine func :::"InsCode"::: "I" -> ($#m1_subset_1 :::"InsType":::) "of" "S"; end; definitionlet "S" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_compos_0 :::"standard-ins"::: ) ($#m1_hidden :::"set"::: ) ; let "T" be ($#m1_subset_1 :::"InsType":::) "of" (Set (Const "S")); func :::"JumpParts"::: "T" -> ($#m1_hidden :::"set"::: ) equals :: COMPOS_0:def 3 "{" (Set "(" ($#k5_xtuple_0 :::"JumpPart"::: ) (Set (Var "I")) ")" ) where I "is" ($#m1_subset_1 :::"Element"::: ) "of" "S" : (Bool (Set ($#k2_compos_0 :::"InsCode"::: ) (Set (Var "I"))) ($#r1_hidden :::"="::: ) "T") "}" ; func :::"AddressParts"::: "T" -> ($#m1_hidden :::"set"::: ) equals :: COMPOS_0:def 4 "{" (Set "(" ($#k2_xtuple_0 :::"AddressPart"::: ) (Set (Var "I")) ")" ) where I "is" ($#m1_subset_1 :::"Element"::: ) "of" "S" : (Bool (Set ($#k2_compos_0 :::"InsCode"::: ) (Set (Var "I"))) ($#r1_hidden :::"="::: ) "T") "}" ; end; :: deftheorem defines :::"JumpParts"::: COMPOS_0:def 3 : (Bool "for" (Set (Var "S")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_compos_0 :::"standard-ins"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "T")) "being" ($#m1_subset_1 :::"InsType":::) "of" (Set (Var "S")) "holds" (Bool (Set ($#k3_compos_0 :::"JumpParts"::: ) (Set (Var "T"))) ($#r1_hidden :::"="::: ) "{" (Set "(" ($#k5_xtuple_0 :::"JumpPart"::: ) (Set (Var "I")) ")" ) where I "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "S")) : (Bool (Set ($#k2_compos_0 :::"InsCode"::: ) (Set (Var "I"))) ($#r1_hidden :::"="::: ) (Set (Var "T"))) "}" ))); :: deftheorem defines :::"AddressParts"::: COMPOS_0:def 4 : (Bool "for" (Set (Var "S")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_compos_0 :::"standard-ins"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "T")) "being" ($#m1_subset_1 :::"InsType":::) "of" (Set (Var "S")) "holds" (Bool (Set ($#k4_compos_0 :::"AddressParts"::: ) (Set (Var "T"))) ($#r1_hidden :::"="::: ) "{" (Set "(" ($#k2_xtuple_0 :::"AddressPart"::: ) (Set (Var "I")) ")" ) where I "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "S")) : (Bool (Set ($#k2_compos_0 :::"InsCode"::: ) (Set (Var "I"))) ($#r1_hidden :::"="::: ) (Set (Var "T"))) "}" ))); registrationlet "S" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_compos_0 :::"standard-ins"::: ) ($#m1_hidden :::"set"::: ) ; let "T" be ($#m1_subset_1 :::"InsType":::) "of" (Set (Const "S")); cluster (Set ($#k4_compos_0 :::"AddressParts"::: ) "T") -> ($#v4_funct_1 :::"functional"::: ) ; cluster (Set ($#k3_compos_0 :::"JumpParts"::: ) "T") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v4_funct_1 :::"functional"::: ) ; end; definitionlet "S" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_compos_0 :::"standard-ins"::: ) ($#m1_hidden :::"set"::: ) ; attr "S" is :::"homogeneous"::: means :: COMPOS_0:def 5 (Bool "for" (Set (Var "I")) "," (Set (Var "J")) "being" ($#m1_subset_1 :::"Element"::: ) "of" "S" "st" (Bool (Bool (Set ($#k2_compos_0 :::"InsCode"::: ) (Set (Var "I"))) ($#r1_hidden :::"="::: ) (Set ($#k2_compos_0 :::"InsCode"::: ) (Set (Var "J"))))) "holds" (Bool (Set ($#k4_finseq_1 :::"dom"::: ) (Set "(" ($#k5_xtuple_0 :::"JumpPart"::: ) (Set (Var "I")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set "(" ($#k5_xtuple_0 :::"JumpPart"::: ) (Set (Var "J")) ")" )))); canceled; attr "S" is :::"J/A-independent"::: means :: COMPOS_0:def 7 (Bool "for" (Set (Var "T")) "being" ($#m1_subset_1 :::"InsType":::) "of" "S" (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#v4_valued_0 :::"natural-valued"::: ) ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "f1")) ($#r2_hidden :::"in"::: ) (Set ($#k3_compos_0 :::"JumpParts"::: ) (Set (Var "T")))) & (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f1"))) ($#r1_hidden :::"="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f2"))))) "holds" (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set ($#k3_xtuple_0 :::"["::: ) (Set (Var "T")) "," (Set (Var "f1")) "," (Set (Var "p")) ($#k3_xtuple_0 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) "S")) "holds" (Bool (Set ($#k3_xtuple_0 :::"["::: ) (Set (Var "T")) "," (Set (Var "f2")) "," (Set (Var "p")) ($#k3_xtuple_0 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) "S")))); end; :: deftheorem defines :::"homogeneous"::: COMPOS_0:def 5 : (Bool "for" (Set (Var "S")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_compos_0 :::"standard-ins"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "S")) "is" ($#v2_compos_0 :::"homogeneous"::: ) ) "iff" (Bool "for" (Set (Var "I")) "," (Set (Var "J")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "S")) "st" (Bool (Bool (Set ($#k2_compos_0 :::"InsCode"::: ) (Set (Var "I"))) ($#r1_hidden :::"="::: ) (Set ($#k2_compos_0 :::"InsCode"::: ) (Set (Var "J"))))) "holds" (Bool (Set ($#k4_finseq_1 :::"dom"::: ) (Set "(" ($#k5_xtuple_0 :::"JumpPart"::: ) (Set (Var "I")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set "(" ($#k5_xtuple_0 :::"JumpPart"::: ) (Set (Var "J")) ")" )))) ")" )); :: deftheorem COMPOS_0:def 6 : canceled; :: deftheorem defines :::"J/A-independent"::: COMPOS_0:def 7 : (Bool "for" (Set (Var "S")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_compos_0 :::"standard-ins"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "S")) "is" ($#v3_compos_0 :::"J/A-independent"::: ) ) "iff" (Bool "for" (Set (Var "T")) "being" ($#m1_subset_1 :::"InsType":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#v4_valued_0 :::"natural-valued"::: ) ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "f1")) ($#r2_hidden :::"in"::: ) (Set ($#k3_compos_0 :::"JumpParts"::: ) (Set (Var "T")))) & (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f1"))) ($#r1_hidden :::"="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f2"))))) "holds" (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set ($#k3_xtuple_0 :::"["::: ) (Set (Var "T")) "," (Set (Var "f1")) "," (Set (Var "p")) ($#k3_xtuple_0 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "S")))) "holds" (Bool (Set ($#k3_xtuple_0 :::"["::: ) (Set (Var "T")) "," (Set (Var "f2")) "," (Set (Var "p")) ($#k3_xtuple_0 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "S")))))) ")" )); registration cluster (Set ($#k1_tarski :::"{"::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k3_xtuple_0 :::"]"::: ) ) ($#k1_tarski :::"}"::: ) ) -> ($#v2_compos_0 :::"homogeneous"::: ) ($#v3_compos_0 :::"J/A-independent"::: ) ; end; registration cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_relat_1 :::"Relation-like"::: ) ($#v1_compos_0 :::"standard-ins"::: ) ($#v2_compos_0 :::"homogeneous"::: ) ($#v3_compos_0 :::"J/A-independent"::: ) for ($#m1_hidden :::"set"::: ) ; end; registrationlet "S" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_compos_0 :::"standard-ins"::: ) ($#v2_compos_0 :::"homogeneous"::: ) ($#m1_hidden :::"set"::: ) ; let "T" be ($#m1_subset_1 :::"InsType":::) "of" (Set (Const "S")); cluster (Set ($#k3_compos_0 :::"JumpParts"::: ) "T") -> ($#v2_card_3 :::"with_common_domain"::: ) ; end; registrationlet "S" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_compos_0 :::"standard-ins"::: ) ($#m1_hidden :::"set"::: ) ; let "I" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "S")); cluster (Set ($#k5_xtuple_0 :::"JumpPart"::: ) "I") -> (Set ($#k5_numbers :::"NAT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) for ($#m1_hidden :::"Function":::); end; theorem :: COMPOS_0:1 (Bool "for" (Set (Var "S")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_compos_0 :::"standard-ins"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "I")) "," (Set (Var "J")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "S")) "st" (Bool (Bool (Set ($#k2_compos_0 :::"InsCode"::: ) (Set (Var "I"))) ($#r1_hidden :::"="::: ) (Set ($#k2_compos_0 :::"InsCode"::: ) (Set (Var "J")))) & (Bool (Set ($#k5_xtuple_0 :::"JumpPart"::: ) (Set (Var "I"))) ($#r1_hidden :::"="::: ) (Set ($#k5_xtuple_0 :::"JumpPart"::: ) (Set (Var "J")))) & (Bool (Set ($#k2_xtuple_0 :::"AddressPart"::: ) (Set (Var "I"))) ($#r1_hidden :::"="::: ) (Set ($#k2_xtuple_0 :::"AddressPart"::: ) (Set (Var "J"))))) "holds" (Bool (Set (Var "I")) ($#r1_hidden :::"="::: ) (Set (Var "J"))))) ; registrationlet "S" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_compos_0 :::"standard-ins"::: ) ($#v2_compos_0 :::"homogeneous"::: ) ($#v3_compos_0 :::"J/A-independent"::: ) ($#m1_hidden :::"set"::: ) ; let "T" be ($#m1_subset_1 :::"InsType":::) "of" (Set (Const "S")); cluster (Set ($#k3_compos_0 :::"JumpParts"::: ) "T") -> ($#v3_card_3 :::"product-like"::: ) ; end; definitionlet "S" be ($#v1_compos_0 :::"standard-ins"::: ) ($#m1_hidden :::"set"::: ) ; let "I" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "S")); attr "I" is :::"ins-loc-free"::: means :: COMPOS_0:def 8 (Bool (Set ($#k5_xtuple_0 :::"JumpPart"::: ) "I") "is" ($#v1_xboole_0 :::"empty"::: ) ); end; :: deftheorem defines :::"ins-loc-free"::: COMPOS_0:def 8 : (Bool "for" (Set (Var "S")) "being" ($#v1_compos_0 :::"standard-ins"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "I")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "S")) "holds" (Bool "(" (Bool (Set (Var "I")) "is" ($#v4_compos_0 :::"ins-loc-free"::: ) ) "iff" (Bool (Set ($#k5_xtuple_0 :::"JumpPart"::: ) (Set (Var "I"))) "is" ($#v1_xboole_0 :::"empty"::: ) ) ")" ))); registrationlet "S" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_compos_0 :::"standard-ins"::: ) ($#m1_hidden :::"set"::: ) ; let "I" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "S")); cluster (Set ($#k5_xtuple_0 :::"JumpPart"::: ) "I") -> ($#v4_valued_0 :::"natural-valued"::: ) for ($#m1_hidden :::"Function":::); end; definitionlet "S" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_compos_0 :::"standard-ins"::: ) ($#v2_compos_0 :::"homogeneous"::: ) ($#v3_compos_0 :::"J/A-independent"::: ) ($#m1_hidden :::"set"::: ) ; let "I" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "S")); let "k" be ($#m1_hidden :::"Nat":::); func :::"IncAddr"::: "(" "I" "," "k" ")" -> ($#m1_subset_1 :::"Element"::: ) "of" "S" means :: COMPOS_0:def 9 (Bool "(" (Bool (Set ($#k2_compos_0 :::"InsCode"::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k2_compos_0 :::"InsCode"::: ) "I")) & (Bool (Set ($#k2_xtuple_0 :::"AddressPart"::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k2_xtuple_0 :::"AddressPart"::: ) "I")) & (Bool (Set ($#k5_xtuple_0 :::"JumpPart"::: ) it) ($#r1_hidden :::"="::: ) (Set "k" ($#k7_valued_1 :::"+"::: ) (Set "(" ($#k5_xtuple_0 :::"JumpPart"::: ) "I" ")" ))) ")" ); end; :: deftheorem defines :::"IncAddr"::: COMPOS_0:def 9 : (Bool "for" (Set (Var "S")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_compos_0 :::"standard-ins"::: ) ($#v2_compos_0 :::"homogeneous"::: ) ($#v3_compos_0 :::"J/A-independent"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "I")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "S")) (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "b4")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "S")) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k5_compos_0 :::"IncAddr"::: ) "(" (Set (Var "I")) "," (Set (Var "k")) ")" )) "iff" (Bool "(" (Bool (Set ($#k2_compos_0 :::"InsCode"::: ) (Set (Var "b4"))) ($#r1_hidden :::"="::: ) (Set ($#k2_compos_0 :::"InsCode"::: ) (Set (Var "I")))) & (Bool (Set ($#k2_xtuple_0 :::"AddressPart"::: ) (Set (Var "b4"))) ($#r1_hidden :::"="::: ) (Set ($#k2_xtuple_0 :::"AddressPart"::: ) (Set (Var "I")))) & (Bool (Set ($#k5_xtuple_0 :::"JumpPart"::: ) (Set (Var "b4"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "k")) ($#k7_valued_1 :::"+"::: ) (Set "(" ($#k5_xtuple_0 :::"JumpPart"::: ) (Set (Var "I")) ")" ))) ")" ) ")" ))))); theorem :: COMPOS_0:2 canceled; theorem :: COMPOS_0:3 (Bool "for" (Set (Var "S")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_compos_0 :::"standard-ins"::: ) ($#v2_compos_0 :::"homogeneous"::: ) ($#v3_compos_0 :::"J/A-independent"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "I")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "S")) "holds" (Bool (Set ($#k5_compos_0 :::"IncAddr"::: ) "(" (Set (Var "I")) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "I"))))) ; theorem :: COMPOS_0:4 (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "S")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_compos_0 :::"standard-ins"::: ) ($#v2_compos_0 :::"homogeneous"::: ) ($#v3_compos_0 :::"J/A-independent"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "I")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "I")) "is" ($#v4_compos_0 :::"ins-loc-free"::: ) )) "holds" (Bool (Set ($#k5_compos_0 :::"IncAddr"::: ) "(" (Set (Var "I")) "," (Set (Var "k")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "I")))))) ; theorem :: COMPOS_0:5 (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "S")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_compos_0 :::"standard-ins"::: ) ($#v2_compos_0 :::"homogeneous"::: ) ($#v3_compos_0 :::"J/A-independent"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "I")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "S")) "holds" (Bool (Set ($#k3_compos_0 :::"JumpParts"::: ) (Set "(" ($#k2_compos_0 :::"InsCode"::: ) (Set (Var "I")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_compos_0 :::"JumpParts"::: ) (Set "(" ($#k2_compos_0 :::"InsCode"::: ) (Set "(" ($#k5_compos_0 :::"IncAddr"::: ) "(" (Set (Var "I")) "," (Set (Var "k")) ")" ")" ) ")" )))))) ; theorem :: COMPOS_0:6 (Bool "for" (Set (Var "S")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_compos_0 :::"standard-ins"::: ) ($#v2_compos_0 :::"homogeneous"::: ) ($#v3_compos_0 :::"J/A-independent"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "I")) "," (Set (Var "J")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "S")) "st" (Bool (Bool "ex" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Set ($#k5_compos_0 :::"IncAddr"::: ) "(" (Set (Var "I")) "," (Set (Var "k")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k5_compos_0 :::"IncAddr"::: ) "(" (Set (Var "J")) "," (Set (Var "k")) ")" )))) "holds" (Bool (Set (Var "I")) ($#r1_hidden :::"="::: ) (Set (Var "J"))))) ; theorem :: COMPOS_0:7 (Bool "for" (Set (Var "k")) "," (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "S")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_compos_0 :::"standard-ins"::: ) ($#v2_compos_0 :::"homogeneous"::: ) ($#v3_compos_0 :::"J/A-independent"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "I")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "S")) "holds" (Bool (Set ($#k5_compos_0 :::"IncAddr"::: ) "(" (Set "(" ($#k5_compos_0 :::"IncAddr"::: ) "(" (Set (Var "I")) "," (Set (Var "k")) ")" ")" ) "," (Set (Var "m")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k5_compos_0 :::"IncAddr"::: ) "(" (Set (Var "I")) "," (Set "(" (Set (Var "k")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "m")) ")" ) ")" ))))) ; theorem :: COMPOS_0:8 (Bool "for" (Set (Var "S")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_compos_0 :::"standard-ins"::: ) ($#v2_compos_0 :::"homogeneous"::: ) ($#v3_compos_0 :::"J/A-independent"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "I")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "S")) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set "(" ($#k5_xtuple_0 :::"JumpPart"::: ) (Set (Var "I")) ")" )))) "holds" (Bool (Set (Set "(" ($#k5_xtuple_0 :::"JumpPart"::: ) (Set (Var "I")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r2_hidden :::"in"::: ) (Set (Set "(" ($#k10_card_3 :::"product""::: ) (Set "(" ($#k3_compos_0 :::"JumpParts"::: ) (Set "(" ($#k2_compos_0 :::"InsCode"::: ) (Set (Var "I")) ")" ) ")" ) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))))))) ; registration cluster (Set ($#k2_tarski :::"{"::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k3_xtuple_0 :::"]"::: ) ) "," (Set ($#k3_xtuple_0 :::"["::: ) (Num 1) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k3_xtuple_0 :::"]"::: ) ) ($#k2_tarski :::"}"::: ) ) -> ($#v1_compos_0 :::"standard-ins"::: ) ; end; theorem :: COMPOS_0:9 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_tarski :::"{"::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k3_xtuple_0 :::"]"::: ) ) "," (Set ($#k3_xtuple_0 :::"["::: ) (Num 1) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k3_xtuple_0 :::"]"::: ) ) ($#k2_tarski :::"}"::: ) ) "holds" (Bool (Set ($#k5_xtuple_0 :::"JumpPart"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) ; registration cluster (Set ($#k2_tarski :::"{"::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k3_xtuple_0 :::"]"::: ) ) "," (Set ($#k3_xtuple_0 :::"["::: ) (Num 1) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k3_xtuple_0 :::"]"::: ) ) ($#k2_tarski :::"}"::: ) ) -> ($#v2_compos_0 :::"homogeneous"::: ) ($#v3_compos_0 :::"J/A-independent"::: ) ; end; theorem :: COMPOS_0:10 (Bool "for" (Set (Var "S")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_compos_0 :::"standard-ins"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "T")) "being" ($#m1_subset_1 :::"InsType":::) "of" (Set (Var "S")) (Bool "ex" (Set (Var "I")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "S")) "st" (Bool (Set ($#k2_compos_0 :::"InsCode"::: ) (Set (Var "I"))) ($#r1_hidden :::"="::: ) (Set (Var "T")))))) ; theorem :: COMPOS_0:11 (Bool "for" (Set (Var "S")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_compos_0 :::"standard-ins"::: ) ($#v2_compos_0 :::"homogeneous"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "I")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "S")) "st" (Bool (Bool (Set ($#k5_xtuple_0 :::"JumpPart"::: ) (Set (Var "I"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set ($#k3_compos_0 :::"JumpParts"::: ) (Set "(" ($#k2_compos_0 :::"InsCode"::: ) (Set (Var "I")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k6_domain_1 :::"}"::: ) )))) ; begin definitionlet "X" be ($#m1_hidden :::"set"::: ) ; attr "X" is :::"with_halt"::: means :: COMPOS_0:def 10 (Bool (Set ($#k3_xtuple_0 :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k3_xtuple_0 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) "X"); end; :: deftheorem defines :::"with_halt"::: COMPOS_0:def 10 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "X")) "is" ($#v5_compos_0 :::"with_halt"::: ) ) "iff" (Bool (Set ($#k3_xtuple_0 :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k3_xtuple_0 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) ")" )); registration cluster ($#v5_compos_0 :::"with_halt"::: ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) for ($#m1_hidden :::"set"::: ) ; end; registration cluster (Set ($#k1_tarski :::"{"::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k3_xtuple_0 :::"]"::: ) ) ($#k1_tarski :::"}"::: ) ) -> ($#v5_compos_0 :::"with_halt"::: ) ; cluster (Set ($#k2_tarski :::"{"::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k3_xtuple_0 :::"]"::: ) ) "," (Set ($#k3_xtuple_0 :::"["::: ) (Num 1) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k3_xtuple_0 :::"]"::: ) ) ($#k2_tarski :::"}"::: ) ) -> ($#v5_compos_0 :::"with_halt"::: ) ; end; registration cluster ($#v1_compos_0 :::"standard-ins"::: ) ($#v5_compos_0 :::"with_halt"::: ) for ($#m1_hidden :::"set"::: ) ; end; registration cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_relat_1 :::"Relation-like"::: ) ($#v1_compos_0 :::"standard-ins"::: ) ($#v2_compos_0 :::"homogeneous"::: ) ($#v3_compos_0 :::"J/A-independent"::: ) ($#v5_compos_0 :::"with_halt"::: ) for ($#m1_hidden :::"set"::: ) ; end; definitionlet "S" be ($#v5_compos_0 :::"with_halt"::: ) ($#m1_hidden :::"set"::: ) ; func :::"halt"::: "S" -> ($#m1_subset_1 :::"Element"::: ) "of" "S" equals :: COMPOS_0:def 11 (Set ($#k3_xtuple_0 :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k3_xtuple_0 :::"]"::: ) ); end; :: deftheorem defines :::"halt"::: COMPOS_0:def 11 : (Bool "for" (Set (Var "S")) "being" ($#v5_compos_0 :::"with_halt"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k6_compos_0 :::"halt"::: ) (Set (Var "S"))) ($#r1_hidden :::"="::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k3_xtuple_0 :::"]"::: ) ))); registrationlet "S" be ($#v1_compos_0 :::"standard-ins"::: ) ($#v5_compos_0 :::"with_halt"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k6_compos_0 :::"halt"::: ) "S") -> ($#v4_compos_0 :::"ins-loc-free"::: ) ; end; registrationlet "S" be ($#v1_compos_0 :::"standard-ins"::: ) ($#v5_compos_0 :::"with_halt"::: ) ($#m1_hidden :::"set"::: ) ; cluster ($#v4_compos_0 :::"ins-loc-free"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" "S"; end; registrationlet "S" be ($#v1_compos_0 :::"standard-ins"::: ) ($#v5_compos_0 :::"with_halt"::: ) ($#m1_hidden :::"set"::: ) ; let "I" be ($#v4_compos_0 :::"ins-loc-free"::: ) ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "S")); cluster (Set ($#k5_xtuple_0 :::"JumpPart"::: ) "I") -> ($#v1_xboole_0 :::"empty"::: ) ; end; theorem :: COMPOS_0:12 (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "S")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_compos_0 :::"standard-ins"::: ) ($#v2_compos_0 :::"homogeneous"::: ) ($#v3_compos_0 :::"J/A-independent"::: ) ($#v5_compos_0 :::"with_halt"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "I")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "S")) "st" (Bool (Bool (Set ($#k5_compos_0 :::"IncAddr"::: ) "(" (Set (Var "I")) "," (Set (Var "k")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_compos_0 :::"halt"::: ) (Set (Var "S"))))) "holds" (Bool (Set (Var "I")) ($#r1_hidden :::"="::: ) (Set ($#k6_compos_0 :::"halt"::: ) (Set (Var "S"))))))) ; definitionlet "S" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_compos_0 :::"standard-ins"::: ) ($#v2_compos_0 :::"homogeneous"::: ) ($#v3_compos_0 :::"J/A-independent"::: ) ($#v5_compos_0 :::"with_halt"::: ) ($#m1_hidden :::"set"::: ) ; let "i" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "S")); attr "i" is :::"No-StopCode"::: means :: COMPOS_0:def 12 (Bool "i" ($#r1_hidden :::"<>"::: ) (Set ($#k6_compos_0 :::"halt"::: ) "S")); end; :: deftheorem defines :::"No-StopCode"::: COMPOS_0:def 12 : (Bool "for" (Set (Var "S")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_compos_0 :::"standard-ins"::: ) ($#v2_compos_0 :::"homogeneous"::: ) ($#v3_compos_0 :::"J/A-independent"::: ) ($#v5_compos_0 :::"with_halt"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "S")) "holds" (Bool "(" (Bool (Set (Var "i")) "is" ($#v6_compos_0 :::"No-StopCode"::: ) ) "iff" (Bool (Set (Var "i")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_compos_0 :::"halt"::: ) (Set (Var "S")))) ")" ))); begin definitionmode Instructions is ($#v1_compos_0 :::"standard-ins"::: ) ($#v2_compos_0 :::"homogeneous"::: ) ($#v3_compos_0 :::"J/A-independent"::: ) ($#v5_compos_0 :::"with_halt"::: ) ($#m1_hidden :::"set"::: ) ; end; registration cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#~v1_zfmisc_1 "non" ($#v1_zfmisc_1 :::"trivial"::: ) ) ($#v1_relat_1 :::"Relation-like"::: ) ($#v1_compos_0 :::"standard-ins"::: ) ($#v2_compos_0 :::"homogeneous"::: ) ($#v3_compos_0 :::"J/A-independent"::: ) ($#v5_compos_0 :::"with_halt"::: ) for ($#m1_hidden :::"set"::: ) ; end;