:: COMPOS_1 semantic presentation begin definitionattr "c1" is :::"strict"::: ; struct :::"COM-Struct"::: -> ; aggr :::"COM-Struct":::(# :::"InstructionsF"::: #) -> ($#l1_compos_1 :::"COM-Struct"::: ) ; sel :::"InstructionsF"::: "c1" -> ($#m1_hidden :::"Instructions":::); end; definitioncanceled; canceled; canceled; canceled; canceled; canceled; canceled; func :::"Trivial-COM"::: -> ($#v1_compos_1 :::"strict"::: ) ($#l1_compos_1 :::"COM-Struct"::: ) means :: COMPOS_1:def 8 (Bool (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k3_xtuple_0 :::"]"::: ) ) ($#k1_tarski :::"}"::: ) )); end; :: deftheorem COMPOS_1:def 1 : canceled; :: deftheorem COMPOS_1:def 2 : canceled; :: deftheorem COMPOS_1:def 3 : canceled; :: deftheorem COMPOS_1:def 4 : canceled; :: deftheorem COMPOS_1:def 5 : canceled; :: deftheorem COMPOS_1:def 6 : canceled; :: deftheorem COMPOS_1:def 7 : canceled; :: deftheorem defines :::"Trivial-COM"::: COMPOS_1:def 8 : (Bool "for" (Set (Var "b1")) "being" ($#v1_compos_1 :::"strict"::: ) ($#l1_compos_1 :::"COM-Struct"::: ) "holds" (Bool "(" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k1_compos_1 :::"Trivial-COM"::: ) )) "iff" (Bool (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" (Set (Var "b1"))) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k3_xtuple_0 :::"]"::: ) ) ($#k1_tarski :::"}"::: ) )) ")" )); definitionlet "S" be ($#l1_compos_1 :::"COM-Struct"::: ) ; mode Instruction of "S" is ($#m1_subset_1 :::"Element"::: ) "of" (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" "S"); end; definitioncanceled; let "S" be ($#l1_compos_1 :::"COM-Struct"::: ) ; func :::"halt"::: "S" -> ($#m1_subset_1 :::"Instruction":::) "of" "S" equals :: COMPOS_1:def 10 (Set ($#k6_compos_0 :::"halt"::: ) (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" "S")); end; :: deftheorem COMPOS_1:def 9 : canceled; :: deftheorem defines :::"halt"::: COMPOS_1:def 10 : (Bool "for" (Set (Var "S")) "being" ($#l1_compos_1 :::"COM-Struct"::: ) "holds" (Bool (Set ($#k2_compos_1 :::"halt"::: ) (Set (Var "S"))) ($#r1_hidden :::"="::: ) (Set ($#k6_compos_0 :::"halt"::: ) (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" (Set (Var "S")))))); definitionlet "S" be ($#l1_compos_1 :::"COM-Struct"::: ) ; let "I" be (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" (Set (Const "S"))) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"Function":::); attr "I" is :::"halt-free"::: means :: COMPOS_1:def 11 (Bool (Bool "not" (Set ($#k2_compos_1 :::"halt"::: ) "S") ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) "I"))); end; :: deftheorem defines :::"halt-free"::: COMPOS_1:def 11 : (Bool "for" (Set (Var "S")) "being" ($#l1_compos_1 :::"COM-Struct"::: ) (Bool "for" (Set (Var "I")) "being" (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" (Set (Var "b1"))) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Var "I")) "is" ($#v2_compos_1 :::"halt-free"::: ) ) "iff" (Bool (Bool "not" (Set ($#k2_compos_1 :::"halt"::: ) (Set (Var "S"))) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "I"))))) ")" ))); begin definitionlet "S" be ($#l1_compos_1 :::"COM-Struct"::: ) ; mode Instruction-Sequence of "S" is (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" "S") ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"ManySortedSet":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ); end; definitionlet "S" be ($#l1_compos_1 :::"COM-Struct"::: ) ; let "P" be ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set (Const "S")); let "k" be ($#m1_hidden :::"Nat":::); :: original: :::"."::: redefine func "P" :::"."::: "k" -> ($#m1_subset_1 :::"Instruction":::) "of" "S"; end; begin definitionlet "S" be ($#l1_compos_1 :::"COM-Struct"::: ) ; let "p" be (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" (Set (Const "S"))) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"Function":::); let "l" be ($#m1_hidden :::"set"::: ) ; pred "p" :::"halts_at"::: "l" means :: COMPOS_1:def 12 (Bool "(" (Bool "l" ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) "p")) & (Bool (Set "p" ($#k1_funct_1 :::"."::: ) "l") ($#r1_hidden :::"="::: ) (Set ($#k2_compos_1 :::"halt"::: ) "S")) ")" ); end; :: deftheorem defines :::"halts_at"::: COMPOS_1:def 12 : (Bool "for" (Set (Var "S")) "being" ($#l1_compos_1 :::"COM-Struct"::: ) (Bool "for" (Set (Var "p")) "being" (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" (Set (Var "b1"))) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "l")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "p")) ($#r1_compos_1 :::"halts_at"::: ) (Set (Var "l"))) "iff" (Bool "(" (Bool (Set (Var "l")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "p")))) & (Bool (Set (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set (Var "l"))) ($#r1_hidden :::"="::: ) (Set ($#k2_compos_1 :::"halt"::: ) (Set (Var "S")))) ")" ) ")" )))); definitionlet "S" be ($#l1_compos_1 :::"COM-Struct"::: ) ; let "s" be ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set (Const "S")); let "l" be ($#m1_hidden :::"Nat":::); redefine pred "s" :::"halts_at"::: "l" means :: COMPOS_1:def 13 (Bool (Set "s" ($#k3_compos_1 :::"."::: ) "l") ($#r1_hidden :::"="::: ) (Set ($#k2_compos_1 :::"halt"::: ) "S")); end; :: deftheorem defines :::"halts_at"::: COMPOS_1:def 13 : (Bool "for" (Set (Var "S")) "being" ($#l1_compos_1 :::"COM-Struct"::: ) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "l")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool "(" (Bool (Set (Var "s")) ($#r1_compos_1 :::"halts_at"::: ) (Set (Var "l"))) "iff" (Bool (Set (Set (Var "s")) ($#k3_compos_1 :::"."::: ) (Set (Var "l"))) ($#r1_hidden :::"="::: ) (Set ($#k2_compos_1 :::"halt"::: ) (Set (Var "S")))) ")" )))); begin notationlet "S" be ($#l1_compos_1 :::"COM-Struct"::: ) ; let "i" be ($#m1_subset_1 :::"Instruction":::) "of" (Set (Const "S")); synonym :::"Load"::: "i" for :::"<%":::"S":::"%>":::; end; registrationlet "S" be ($#l1_compos_1 :::"COM-Struct"::: ) ; cluster ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" "S") ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) (Num 1) ($#v3_card_1 :::"-element"::: ) ($#v1_afinsq_1 :::"initial"::: ) for ($#m1_hidden :::"set"::: ) ; end; definitionlet "S" be ($#l1_compos_1 :::"COM-Struct"::: ) ; mode preProgram of "S" is (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" "S") ($#v5_relat_1 :::"-valued"::: ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"Function":::); end; definitionlet "S" be ($#l1_compos_1 :::"COM-Struct"::: ) ; let "F" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"preProgram":::) "of" (Set (Const "S")); attr "F" is :::"halt-ending"::: means :: COMPOS_1:def 14 (Bool (Set "F" ($#k1_funct_1 :::"."::: ) (Set "(" ($#k62_valued_1 :::"LastLoc"::: ) "F" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_compos_1 :::"halt"::: ) "S")); attr "F" is :::"unique-halt"::: means :: COMPOS_1:def 15 (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set "F" ($#k1_funct_1 :::"."::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k2_compos_1 :::"halt"::: ) "S")) & (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) "F"))) "holds" (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set ($#k62_valued_1 :::"LastLoc"::: ) "F"))); end; :: deftheorem defines :::"halt-ending"::: COMPOS_1:def 14 : (Bool "for" (Set (Var "S")) "being" ($#l1_compos_1 :::"COM-Struct"::: ) (Bool "for" (Set (Var "F")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"preProgram":::) "of" (Set (Var "S")) "holds" (Bool "(" (Bool (Set (Var "F")) "is" ($#v3_compos_1 :::"halt-ending"::: ) ) "iff" (Bool (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k62_valued_1 :::"LastLoc"::: ) (Set (Var "F")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_compos_1 :::"halt"::: ) (Set (Var "S")))) ")" ))); :: deftheorem defines :::"unique-halt"::: COMPOS_1:def 15 : (Bool "for" (Set (Var "S")) "being" ($#l1_compos_1 :::"COM-Struct"::: ) (Bool "for" (Set (Var "F")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"preProgram":::) "of" (Set (Var "S")) "holds" (Bool "(" (Bool (Set (Var "F")) "is" ($#v4_compos_1 :::"unique-halt"::: ) ) "iff" (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k2_compos_1 :::"halt"::: ) (Set (Var "S")))) & (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "F"))))) "holds" (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set ($#k62_valued_1 :::"LastLoc"::: ) (Set (Var "F"))))) ")" ))); registrationlet "S" be ($#l1_compos_1 :::"COM-Struct"::: ) ; cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_zfmisc_1 :::"trivial"::: ) ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" "S") ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_finset_1 :::"finite"::: ) ($#v4_card_3 :::"countable"::: ) bbbadV2_PRE_POLY() ($#v1_afinsq_1 :::"initial"::: ) for ($#m1_hidden :::"set"::: ) ; end; definitionlet "S" be ($#l1_compos_1 :::"COM-Struct"::: ) ; mode Program of "S" is ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_afinsq_1 :::"initial"::: ) ($#m1_hidden :::"preProgram":::) "of" "S"; end; theorem :: COMPOS_1:1 canceled; theorem :: COMPOS_1:2 (Bool "for" (Set (Var "ins")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" (Set ($#k1_compos_1 :::"Trivial-COM"::: ) )) "holds" (Bool (Set ($#k2_compos_0 :::"InsCode"::: ) (Set (Var "ins"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) ; begin definitionlet "S" be ($#l1_compos_1 :::"COM-Struct"::: ) ; func :::"Stop"::: "S" -> ($#m1_hidden :::"preProgram":::) "of" "S" equals :: COMPOS_1:def 16 (Set ($#k3_afinsq_1 :::"Load"::: ) ); end; :: deftheorem defines :::"Stop"::: COMPOS_1:def 16 : (Bool "for" (Set (Var "S")) "being" ($#l1_compos_1 :::"COM-Struct"::: ) "holds" (Bool (Set ($#k4_compos_1 :::"Stop"::: ) (Set (Var "S"))) ($#r1_hidden :::"="::: ) (Set ($#k3_afinsq_1 :::"Load"::: ) ))); registrationlet "S" be ($#l1_compos_1 :::"COM-Struct"::: ) ; cluster (Set ($#k4_compos_1 :::"Stop"::: ) "S") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_afinsq_1 :::"initial"::: ) ; end; registrationlet "S" be ($#l1_compos_1 :::"COM-Struct"::: ) ; cluster (Set ($#k4_compos_1 :::"Stop"::: ) "S") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_zfmisc_1 :::"trivial"::: ) ($#v1_afinsq_1 :::"initial"::: ) ; end; registrationlet "S" be ($#l1_compos_1 :::"COM-Struct"::: ) ; cluster (Set ($#k4_compos_1 :::"Stop"::: ) "S") -> ($#v3_compos_1 :::"halt-ending"::: ) ($#v4_compos_1 :::"unique-halt"::: ) ; end; registrationlet "S" be ($#l1_compos_1 :::"COM-Struct"::: ) ; cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_zfmisc_1 :::"trivial"::: ) ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" "S") ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v5_ordinal1 :::"T-Sequence-like"::: ) ($#v1_finset_1 :::"finite"::: ) ($#v4_card_3 :::"countable"::: ) bbbadV2_PRE_POLY() ($#v1_afinsq_1 :::"initial"::: ) ($#v3_compos_1 :::"halt-ending"::: ) ($#v4_compos_1 :::"unique-halt"::: ) for ($#m1_hidden :::"set"::: ) ; end; definitionlet "S" be ($#l1_compos_1 :::"COM-Struct"::: ) ; mode MacroInstruction of "S" is ($#v3_compos_1 :::"halt-ending"::: ) ($#v4_compos_1 :::"unique-halt"::: ) ($#m1_hidden :::"Program":::) "of" "S"; end; registrationlet "S" be ($#l1_compos_1 :::"COM-Struct"::: ) ; cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" "S") ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_finset_1 :::"finite"::: ) ($#v4_card_3 :::"countable"::: ) bbbadV2_PRE_POLY() ($#v1_afinsq_1 :::"initial"::: ) for ($#m1_hidden :::"set"::: ) ; end; theorem :: COMPOS_1:3 (Bool "for" (Set (Var "S")) "being" ($#l1_compos_1 :::"COM-Struct"::: ) "holds" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_afinsq_1 :::"dom"::: ) (Set "(" ($#k4_compos_1 :::"Stop"::: ) (Set (Var "S")) ")" )))) ; theorem :: COMPOS_1:4 (Bool "for" (Set (Var "S")) "being" ($#l1_compos_1 :::"COM-Struct"::: ) "holds" (Bool (Set ($#k5_card_1 :::"card"::: ) (Set "(" ($#k4_compos_1 :::"Stop"::: ) (Set (Var "S")) ")" )) ($#r1_hidden :::"="::: ) (Num 1))) ; begin theorem :: COMPOS_1:5 (Bool "for" (Set (Var "I")) "being" ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_compos_1 :::"Trivial-COM"::: ) ) "holds" (Bool (Set ($#k5_xtuple_0 :::"JumpPart"::: ) (Set (Var "I"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) ; theorem :: COMPOS_1:6 (Bool "for" (Set (Var "T")) "being" ($#m1_subset_1 :::"InsType":::) "of" (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" (Set ($#k1_compos_1 :::"Trivial-COM"::: ) )) "holds" (Bool (Set ($#k3_compos_0 :::"JumpParts"::: ) (Set (Var "T"))) ($#r1_hidden :::"="::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k6_domain_1 :::"}"::: ) ))) ; registrationlet "S" be ($#l1_compos_1 :::"COM-Struct"::: ) ; cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_zfmisc_1 :::"trivial"::: ) ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" "S") ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_finset_1 :::"finite"::: ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v4_compos_1 :::"unique-halt"::: ) for ($#m1_hidden :::"set"::: ) ; end; theorem :: COMPOS_1:7 canceled; theorem :: COMPOS_1:8 (Bool "for" (Set (Var "S")) "being" ($#l1_compos_1 :::"COM-Struct"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_hidden :::"MacroInstruction":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set ($#k5_card_1 :::"card"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Num 1))) "holds" (Bool (Set (Var "F")) ($#r1_hidden :::"="::: ) (Set ($#k4_compos_1 :::"Stop"::: ) (Set (Var "S")))))) ; theorem :: COMPOS_1:9 (Bool "for" (Set (Var "S")) "being" ($#l1_compos_1 :::"COM-Struct"::: ) "holds" (Bool (Set ($#k62_valued_1 :::"LastLoc"::: ) (Set "(" ($#k4_compos_1 :::"Stop"::: ) (Set (Var "S")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) ; begin definitioncanceled; canceled; canceled; canceled; let "S" be ($#l1_compos_1 :::"COM-Struct"::: ) ; let "p" be (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" (Set (Const "S"))) ($#v5_relat_1 :::"-valued"::: ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"Function":::); let "k" be ($#m1_hidden :::"Nat":::); func :::"IncAddr"::: "(" "p" "," "k" ")" -> (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" "S") ($#v5_relat_1 :::"-valued"::: ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"Function":::) means :: COMPOS_1:def 21 (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) "p")) & (Bool "(" "for" (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "m")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) "p"))) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "m"))) ($#r1_hidden :::"="::: ) (Set ($#k5_compos_0 :::"IncAddr"::: ) "(" (Set "(" "p" ($#k7_partfun1 :::"/."::: ) (Set (Var "m")) ")" ) "," "k" ")" )) ")" ) ")" ); end; :: deftheorem COMPOS_1:def 17 : canceled; :: deftheorem COMPOS_1:def 18 : canceled; :: deftheorem COMPOS_1:def 19 : canceled; :: deftheorem COMPOS_1:def 20 : canceled; :: deftheorem defines :::"IncAddr"::: COMPOS_1:def 21 : (Bool "for" (Set (Var "S")) "being" ($#l1_compos_1 :::"COM-Struct"::: ) (Bool "for" (Set (Var "p")) "being" (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" (Set (Var "b1"))) ($#v5_relat_1 :::"-valued"::: ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "b4")) "being" (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" (Set (Var "b1"))) ($#v5_relat_1 :::"-valued"::: ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k5_compos_1 :::"IncAddr"::: ) "(" (Set (Var "p")) "," (Set (Var "k")) ")" )) "iff" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "b4"))) ($#r1_hidden :::"="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "p")))) & (Bool "(" "for" (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "m")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "p"))))) "holds" (Bool (Set (Set (Var "b4")) ($#k1_funct_1 :::"."::: ) (Set (Var "m"))) ($#r1_hidden :::"="::: ) (Set ($#k5_compos_0 :::"IncAddr"::: ) "(" (Set "(" (Set (Var "p")) ($#k7_partfun1 :::"/."::: ) (Set (Var "m")) ")" ) "," (Set (Var "k")) ")" )) ")" ) ")" ) ")" ))))); registrationlet "S" be ($#l1_compos_1 :::"COM-Struct"::: ) ; let "F" be (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" (Set (Const "S"))) ($#v5_relat_1 :::"-valued"::: ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"Function":::); let "k" be ($#m1_hidden :::"Nat":::); cluster (Set ($#k5_compos_1 :::"IncAddr"::: ) "(" "F" "," "k" ")" ) -> (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" "S") ($#v5_relat_1 :::"-valued"::: ) ($#v1_finset_1 :::"finite"::: ) ; end; registrationlet "S" be ($#l1_compos_1 :::"COM-Struct"::: ) ; let "F" be ($#v1_xboole_0 :::"empty"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" (Set (Const "S"))) ($#v5_relat_1 :::"-valued"::: ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"Function":::); let "k" be ($#m1_hidden :::"Nat":::); cluster (Set ($#k5_compos_1 :::"IncAddr"::: ) "(" "F" "," "k" ")" ) -> ($#v1_xboole_0 :::"empty"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" "S") ($#v5_relat_1 :::"-valued"::: ) ($#v1_finset_1 :::"finite"::: ) ; end; registrationlet "S" be ($#l1_compos_1 :::"COM-Struct"::: ) ; let "F" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" (Set (Const "S"))) ($#v5_relat_1 :::"-valued"::: ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"Function":::); let "k" be ($#m1_hidden :::"Nat":::); cluster (Set ($#k5_compos_1 :::"IncAddr"::: ) "(" "F" "," "k" ")" ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" "S") ($#v5_relat_1 :::"-valued"::: ) ($#v1_finset_1 :::"finite"::: ) ; end; registrationlet "S" be ($#l1_compos_1 :::"COM-Struct"::: ) ; let "F" be (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" (Set (Const "S"))) ($#v5_relat_1 :::"-valued"::: ) ($#v1_finset_1 :::"finite"::: ) ($#v1_afinsq_1 :::"initial"::: ) ($#m1_hidden :::"Function":::); let "k" be ($#m1_hidden :::"Nat":::); cluster (Set ($#k5_compos_1 :::"IncAddr"::: ) "(" "F" "," "k" ")" ) -> (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" "S") ($#v5_relat_1 :::"-valued"::: ) ($#v1_finset_1 :::"finite"::: ) ($#v1_afinsq_1 :::"initial"::: ) ; end; theorem :: COMPOS_1:10 canceled; theorem :: COMPOS_1:11 canceled; theorem :: COMPOS_1:12 canceled; theorem :: COMPOS_1:13 canceled; theorem :: COMPOS_1:14 canceled; theorem :: COMPOS_1:15 canceled; registrationlet "S" be ($#l1_compos_1 :::"COM-Struct"::: ) ; let "F" be (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" (Set (Const "S"))) ($#v5_relat_1 :::"-valued"::: ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"Function":::); reduce ; end; theorem :: COMPOS_1:16 (Bool "for" (Set (Var "S")) "being" ($#l1_compos_1 :::"COM-Struct"::: ) (Bool "for" (Set (Var "F")) "being" (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" (Set (Var "b1"))) ($#v5_relat_1 :::"-valued"::: ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"Function":::) "holds" (Bool (Set ($#k5_compos_1 :::"IncAddr"::: ) "(" (Set (Var "F")) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "F"))))) ; theorem :: COMPOS_1:17 (Bool "for" (Set (Var "k")) "," (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "S")) "being" ($#l1_compos_1 :::"COM-Struct"::: ) (Bool "for" (Set (Var "F")) "being" (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" (Set (Var "b3"))) ($#v5_relat_1 :::"-valued"::: ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"Function":::) "holds" (Bool (Set ($#k5_compos_1 :::"IncAddr"::: ) "(" (Set "(" ($#k5_compos_1 :::"IncAddr"::: ) "(" (Set (Var "F")) "," (Set (Var "k")) ")" ")" ) "," (Set (Var "m")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k5_compos_1 :::"IncAddr"::: ) "(" (Set (Var "F")) "," (Set "(" (Set (Var "k")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "m")) ")" ) ")" ))))) ; definitionlet "S" be ($#l1_compos_1 :::"COM-Struct"::: ) ; let "p" be (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" (Set (Const "S"))) ($#v5_relat_1 :::"-valued"::: ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"Function":::); let "k" be ($#m1_hidden :::"Nat":::); func :::"Reloc"::: "(" "p" "," "k" ")" -> (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" "S") ($#v5_relat_1 :::"-valued"::: ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"Function":::) equals :: COMPOS_1:def 22 (Set ($#k61_valued_1 :::"Shift"::: ) "(" (Set "(" ($#k5_compos_1 :::"IncAddr"::: ) "(" "p" "," "k" ")" ")" ) "," "k" ")" ); end; :: deftheorem defines :::"Reloc"::: COMPOS_1:def 22 : (Bool "for" (Set (Var "S")) "being" ($#l1_compos_1 :::"COM-Struct"::: ) (Bool "for" (Set (Var "p")) "being" (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" (Set (Var "b1"))) ($#v5_relat_1 :::"-valued"::: ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k6_compos_1 :::"Reloc"::: ) "(" (Set (Var "p")) "," (Set (Var "k")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k61_valued_1 :::"Shift"::: ) "(" (Set "(" ($#k5_compos_1 :::"IncAddr"::: ) "(" (Set (Var "p")) "," (Set (Var "k")) ")" ")" ) "," (Set (Var "k")) ")" ))))); theorem :: COMPOS_1:18 (Bool "for" (Set (Var "S")) "being" ($#l1_compos_1 :::"COM-Struct"::: ) (Bool "for" (Set (Var "F")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_afinsq_1 :::"initial"::: ) ($#m1_hidden :::"preProgram":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "G")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" (Set (Var "b1"))) ($#v5_relat_1 :::"-valued"::: ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"Function":::) "holds" (Bool (Set ($#k2_afinsq_1 :::"dom"::: ) (Set "(" ($#k63_valued_1 :::"CutLastLoc"::: ) (Set (Var "F")) ")" )) ($#r1_xboole_0 :::"misses"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k6_compos_1 :::"Reloc"::: ) "(" (Set (Var "G")) "," (Set "(" (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "F")) ")" ) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ")" ")" )))))) ; theorem :: COMPOS_1:19 (Bool "for" (Set (Var "S")) "being" ($#l1_compos_1 :::"COM-Struct"::: ) (Bool "for" (Set (Var "F")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_afinsq_1 :::"initial"::: ) ($#v4_compos_1 :::"unique-halt"::: ) ($#m1_hidden :::"preProgram":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "I")) ($#r2_hidden :::"in"::: ) (Set ($#k2_afinsq_1 :::"dom"::: ) (Set "(" ($#k63_valued_1 :::"CutLastLoc"::: ) (Set (Var "F")) ")" )))) "holds" (Bool (Set (Set "(" ($#k63_valued_1 :::"CutLastLoc"::: ) (Set (Var "F")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "I"))) ($#r1_hidden :::"<>"::: ) (Set ($#k2_compos_1 :::"halt"::: ) (Set (Var "S"))))))) ; definitionlet "S" be ($#l1_compos_1 :::"COM-Struct"::: ) ; let "F", "G" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"preProgram":::) "of" (Set (Const "S")); func "F" :::"';'"::: "G" -> ($#m1_hidden :::"preProgram":::) "of" "S" equals :: COMPOS_1:def 23 (Set (Set "(" ($#k63_valued_1 :::"CutLastLoc"::: ) "F" ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k6_compos_1 :::"Reloc"::: ) "(" "G" "," (Set "(" (Set "(" ($#k5_card_1 :::"card"::: ) "F" ")" ) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ")" ")" )); end; :: deftheorem defines :::"';'"::: COMPOS_1:def 23 : (Bool "for" (Set (Var "S")) "being" ($#l1_compos_1 :::"COM-Struct"::: ) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"preProgram":::) "of" (Set (Var "S")) "holds" (Bool (Set (Set (Var "F")) ($#k7_compos_1 :::"';'"::: ) (Set (Var "G"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k63_valued_1 :::"CutLastLoc"::: ) (Set (Var "F")) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k6_compos_1 :::"Reloc"::: ) "(" (Set (Var "G")) "," (Set "(" (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "F")) ")" ) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ")" ")" ))))); registrationlet "S" be ($#l1_compos_1 :::"COM-Struct"::: ) ; let "F", "G" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" (Set (Const "S"))) ($#v5_relat_1 :::"-valued"::: ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"Function":::); cluster (Set "F" ($#k7_compos_1 :::"';'"::: ) "G") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; theorem :: COMPOS_1:20 (Bool "for" (Set (Var "S")) "being" ($#l1_compos_1 :::"COM-Struct"::: ) (Bool "for" (Set (Var "F")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_afinsq_1 :::"initial"::: ) ($#m1_hidden :::"preProgram":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "G")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" (Set (Var "b1"))) ($#v5_relat_1 :::"-valued"::: ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set ($#k5_card_1 :::"card"::: ) (Set "(" (Set (Var "F")) ($#k7_compos_1 :::"';'"::: ) (Set (Var "G")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "F")) ")" ) ($#k2_nat_1 :::"+"::: ) (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "G")) ")" ) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Num 1))) & (Bool (Set ($#k5_card_1 :::"card"::: ) (Set "(" (Set (Var "F")) ($#k7_compos_1 :::"';'"::: ) (Set (Var "G")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "F")) ")" ) ($#k2_nat_1 :::"+"::: ) (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "G")) ")" ) ")" ) ($#k7_nat_d :::"-'"::: ) (Num 1))) ")" )))) ; registrationlet "S" be ($#l1_compos_1 :::"COM-Struct"::: ) ; let "F", "G" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_afinsq_1 :::"initial"::: ) ($#m1_hidden :::"preProgram":::) "of" (Set (Const "S")); cluster (Set "F" ($#k7_compos_1 :::"';'"::: ) "G") -> ($#v1_afinsq_1 :::"initial"::: ) ; end; theorem :: COMPOS_1:21 (Bool "for" (Set (Var "S")) "being" ($#l1_compos_1 :::"COM-Struct"::: ) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_afinsq_1 :::"initial"::: ) ($#m1_hidden :::"preProgram":::) "of" (Set (Var "S")) "holds" (Bool (Set ($#k2_afinsq_1 :::"dom"::: ) (Set (Var "F"))) ($#r1_ordinal1 :::"c="::: ) (Set ($#k2_afinsq_1 :::"dom"::: ) (Set "(" (Set (Var "F")) ($#k7_compos_1 :::"';'"::: ) (Set (Var "G")) ")" ))))) ; registrationlet "S" be ($#l1_compos_1 :::"COM-Struct"::: ) ; let "F", "G" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_afinsq_1 :::"initial"::: ) ($#m1_hidden :::"preProgram":::) "of" (Set (Const "S")); cluster (Set "F" ($#k7_compos_1 :::"';'"::: ) "G") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_afinsq_1 :::"initial"::: ) ; end; theorem :: COMPOS_1:22 (Bool "for" (Set (Var "S")) "being" ($#l1_compos_1 :::"COM-Struct"::: ) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_afinsq_1 :::"initial"::: ) ($#m1_hidden :::"preProgram":::) "of" (Set (Var "S")) "holds" (Bool (Set ($#k63_valued_1 :::"CutLastLoc"::: ) (Set (Var "F"))) ($#r1_tarski :::"c="::: ) (Set ($#k63_valued_1 :::"CutLastLoc"::: ) (Set "(" (Set (Var "F")) ($#k7_compos_1 :::"';'"::: ) (Set (Var "G")) ")" ))))) ; theorem :: COMPOS_1:23 (Bool "for" (Set (Var "S")) "being" ($#l1_compos_1 :::"COM-Struct"::: ) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_afinsq_1 :::"initial"::: ) ($#m1_hidden :::"preProgram":::) "of" (Set (Var "S")) "holds" (Bool (Set (Set "(" (Set (Var "F")) ($#k7_compos_1 :::"';'"::: ) (Set (Var "G")) ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k62_valued_1 :::"LastLoc"::: ) (Set (Var "F")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_compos_1 :::"IncAddr"::: ) "(" (Set (Var "G")) "," (Set "(" (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "F")) ")" ) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ))))) ; theorem :: COMPOS_1:24 (Bool "for" (Set (Var "S")) "being" ($#l1_compos_1 :::"COM-Struct"::: ) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_afinsq_1 :::"initial"::: ) ($#m1_hidden :::"preProgram":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "f")) ($#r1_xxreal_0 :::"<"::: ) (Set (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "F")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Num 1)))) "holds" (Bool (Set (Set "(" ($#k5_compos_1 :::"IncAddr"::: ) "(" (Set (Var "F")) "," (Set "(" (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "F")) ")" ) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_compos_1 :::"IncAddr"::: ) "(" (Set "(" (Set (Var "F")) ($#k7_compos_1 :::"';'"::: ) (Set (Var "G")) ")" ) "," (Set "(" (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "F")) ")" ) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "f"))))))) ; registrationlet "S" be ($#l1_compos_1 :::"COM-Struct"::: ) ; let "F" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" (Set (Const "S"))) ($#v5_relat_1 :::"-valued"::: ) ($#v1_finset_1 :::"finite"::: ) ($#v1_afinsq_1 :::"initial"::: ) ($#m1_hidden :::"Function":::); let "G" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" (Set (Const "S"))) ($#v5_relat_1 :::"-valued"::: ) ($#v1_finset_1 :::"finite"::: ) ($#v1_afinsq_1 :::"initial"::: ) ($#v3_compos_1 :::"halt-ending"::: ) ($#m1_hidden :::"Function":::); cluster (Set "F" ($#k7_compos_1 :::"';'"::: ) "G") -> ($#v3_compos_1 :::"halt-ending"::: ) ; end; registrationlet "S" be ($#l1_compos_1 :::"COM-Struct"::: ) ; let "F", "G" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" (Set (Const "S"))) ($#v5_relat_1 :::"-valued"::: ) ($#v1_finset_1 :::"finite"::: ) ($#v1_afinsq_1 :::"initial"::: ) ($#v3_compos_1 :::"halt-ending"::: ) ($#v4_compos_1 :::"unique-halt"::: ) ($#m1_hidden :::"Function":::); cluster (Set "F" ($#k7_compos_1 :::"';'"::: ) "G") -> ($#v4_compos_1 :::"unique-halt"::: ) ; end; definitionlet "S" be ($#l1_compos_1 :::"COM-Struct"::: ) ; let "F", "G" be ($#m1_hidden :::"MacroInstruction":::) "of" (Set (Const "S")); :: original: :::"';'"::: redefine func "F" :::"';'"::: "G" -> ($#m1_hidden :::"MacroInstruction":::) "of" "S"; end; registrationlet "S" be ($#l1_compos_1 :::"COM-Struct"::: ) ; let "k" be ($#m1_hidden :::"Nat":::); reduce ; end; theorem :: COMPOS_1:25 (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "S")) "being" ($#l1_compos_1 :::"COM-Struct"::: ) "holds" (Bool (Set ($#k5_compos_1 :::"IncAddr"::: ) "(" (Set "(" ($#k4_compos_1 :::"Stop"::: ) (Set (Var "S")) ")" ) "," (Set (Var "k")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_compos_1 :::"Stop"::: ) (Set (Var "S")))))) ; theorem :: COMPOS_1:26 (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "S")) "being" ($#l1_compos_1 :::"COM-Struct"::: ) "holds" (Bool (Set ($#k61_valued_1 :::"Shift"::: ) "(" (Set "(" ($#k4_compos_1 :::"Stop"::: ) (Set (Var "S")) ")" ) "," (Set (Var "k")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "k")) ($#k16_funcop_1 :::".-->"::: ) (Set "(" ($#k2_compos_1 :::"halt"::: ) (Set (Var "S")) ")" ))))) ; registrationlet "S" be ($#l1_compos_1 :::"COM-Struct"::: ) ; let "F" be ($#m1_hidden :::"MacroInstruction":::) "of" (Set (Const "S")); reduce ; end; theorem :: COMPOS_1:27 (Bool "for" (Set (Var "S")) "being" ($#l1_compos_1 :::"COM-Struct"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_hidden :::"MacroInstruction":::) "of" (Set (Var "S")) "holds" (Bool (Set (Set (Var "F")) ($#k8_compos_1 :::"';'"::: ) (Set "(" ($#k4_compos_1 :::"Stop"::: ) (Set (Var "S")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "F"))))) ; registrationlet "S" be ($#l1_compos_1 :::"COM-Struct"::: ) ; let "F" be ($#m1_hidden :::"MacroInstruction":::) "of" (Set (Const "S")); reduce ; end; theorem :: COMPOS_1:28 (Bool "for" (Set (Var "S")) "being" ($#l1_compos_1 :::"COM-Struct"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_hidden :::"MacroInstruction":::) "of" (Set (Var "S")) "holds" (Bool (Set (Set "(" ($#k4_compos_1 :::"Stop"::: ) (Set (Var "S")) ")" ) ($#k8_compos_1 :::"';'"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set (Var "F"))))) ; theorem :: COMPOS_1:29 (Bool "for" (Set (Var "S")) "being" ($#l1_compos_1 :::"COM-Struct"::: ) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "," (Set (Var "H")) "being" ($#m1_hidden :::"MacroInstruction":::) "of" (Set (Var "S")) "holds" (Bool (Set (Set "(" (Set (Var "F")) ($#k8_compos_1 :::"';'"::: ) (Set (Var "G")) ")" ) ($#k8_compos_1 :::"';'"::: ) (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k8_compos_1 :::"';'"::: ) (Set "(" (Set (Var "G")) ($#k8_compos_1 :::"';'"::: ) (Set (Var "H")) ")" ))))) ; theorem :: COMPOS_1:30 canceled; theorem :: COMPOS_1:31 (Bool "for" (Set (Var "I")) "being" ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_compos_1 :::"Trivial-COM"::: ) ) "holds" (Bool (Set ($#k5_xtuple_0 :::"JumpPart"::: ) (Set (Var "I"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) ; begin theorem :: COMPOS_1:32 (Bool "for" (Set (Var "S")) "being" ($#l1_compos_1 :::"COM-Struct"::: ) (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "p")) "being" (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" (Set (Var "b1"))) ($#v5_relat_1 :::"-valued"::: ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"Function":::) "holds" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k6_compos_1 :::"Reloc"::: ) "(" (Set (Var "p")) "," (Set (Var "k")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k61_valued_1 :::"Shift"::: ) "(" (Set (Var "p")) "," (Set (Var "k")) ")" ")" )))))) ; theorem :: COMPOS_1:33 (Bool "for" (Set (Var "S")) "being" ($#l1_compos_1 :::"COM-Struct"::: ) (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "p")) "being" (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" (Set (Var "b1"))) ($#v5_relat_1 :::"-valued"::: ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"Function":::) "holds" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k6_compos_1 :::"Reloc"::: ) "(" (Set (Var "p")) "," (Set (Var "k")) ")" ")" )) ($#r1_hidden :::"="::: ) "{" (Set "(" (Set (Var "j")) ($#k2_nat_1 :::"+"::: ) (Set (Var "k")) ")" ) where j "is" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) : (Bool (Set (Var "j")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "p")))) "}" )))) ; theorem :: COMPOS_1:34 (Bool "for" (Set (Var "S")) "being" ($#l1_compos_1 :::"COM-Struct"::: ) (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "p")) "being" (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" (Set (Var "b1"))) ($#v5_relat_1 :::"-valued"::: ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"Function":::) "holds" (Bool (Set ($#k61_valued_1 :::"Shift"::: ) "(" (Set "(" ($#k5_compos_1 :::"IncAddr"::: ) "(" (Set (Var "p")) "," (Set (Var "i")) ")" ")" ) "," (Set (Var "j")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k5_compos_1 :::"IncAddr"::: ) "(" (Set "(" ($#k61_valued_1 :::"Shift"::: ) "(" (Set (Var "p")) "," (Set (Var "j")) ")" ")" ) "," (Set (Var "i")) ")" ))))) ; theorem :: COMPOS_1:35 (Bool "for" (Set (Var "il")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "S")) "being" ($#l1_compos_1 :::"COM-Struct"::: ) (Bool "for" (Set (Var "g")) "being" (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" (Set (Var "b2"))) ($#v5_relat_1 :::"-valued"::: ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "I")) "being" ($#m1_subset_1 :::"Instruction":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "il")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "g")))) & (Bool (Set (Var "I")) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set (Var "il"))))) "holds" (Bool (Set ($#k5_compos_0 :::"IncAddr"::: ) "(" (Set (Var "I")) "," (Set (Var "k")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k6_compos_1 :::"Reloc"::: ) "(" (Set (Var "g")) "," (Set (Var "k")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "il")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "k")) ")" )))))))) ; definitionlet "S" be ($#l1_compos_1 :::"COM-Struct"::: ) ; let "i" be ($#m1_subset_1 :::"Instruction":::) "of" (Set (Const "S")); :: original: :::"Load"::: redefine func :::"Load"::: "i" -> ($#m1_hidden :::"preProgram":::) "of" "S"; end; definitionlet "S" be ($#l1_compos_1 :::"COM-Struct"::: ) ; let "I" be ($#v1_afinsq_1 :::"initial"::: ) ($#m1_hidden :::"preProgram":::) "of" (Set (Const "S")); func :::"stop"::: "I" -> ($#m1_hidden :::"preProgram":::) "of" "S" equals :: COMPOS_1:def 24 (Set "I" ($#k1_ordinal4 :::"^"::: ) (Set "(" ($#k4_compos_1 :::"Stop"::: ) "S" ")" )); end; :: deftheorem defines :::"stop"::: COMPOS_1:def 24 : (Bool "for" (Set (Var "S")) "being" ($#l1_compos_1 :::"COM-Struct"::: ) (Bool "for" (Set (Var "I")) "being" ($#v1_afinsq_1 :::"initial"::: ) ($#m1_hidden :::"preProgram":::) "of" (Set (Var "S")) "holds" (Bool (Set ($#k10_compos_1 :::"stop"::: ) (Set (Var "I"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "I")) ($#k1_ordinal4 :::"^"::: ) (Set "(" ($#k4_compos_1 :::"Stop"::: ) (Set (Var "S")) ")" ))))); registrationlet "S" be ($#l1_compos_1 :::"COM-Struct"::: ) ; let "I" be ($#v1_afinsq_1 :::"initial"::: ) ($#m1_hidden :::"preProgram":::) "of" (Set (Const "S")); cluster (Set ($#k10_compos_1 :::"stop"::: ) "I") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_afinsq_1 :::"initial"::: ) ; end; theorem :: COMPOS_1:36 (Bool "for" (Set (Var "S")) "being" ($#l1_compos_1 :::"COM-Struct"::: ) (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" (Set (Var "S")) "holds" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_afinsq_1 :::"dom"::: ) (Set "(" ($#k10_compos_1 :::"stop"::: ) (Set (Var "I")) ")" ))))) ; begin definitionlet "S" be ($#l1_compos_1 :::"COM-Struct"::: ) ; let "i" be ($#m1_subset_1 :::"Instruction":::) "of" (Set (Const "S")); func :::"Macro"::: "i" -> ($#m1_hidden :::"preProgram":::) "of" "S" equals :: COMPOS_1:def 25 (Set ($#k10_compos_1 :::"stop"::: ) (Set "(" ($#k9_compos_1 :::"Load"::: ) "i" ")" )); end; :: deftheorem defines :::"Macro"::: COMPOS_1:def 25 : (Bool "for" (Set (Var "S")) "being" ($#l1_compos_1 :::"COM-Struct"::: ) (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Instruction":::) "of" (Set (Var "S")) "holds" (Bool (Set ($#k11_compos_1 :::"Macro"::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k10_compos_1 :::"stop"::: ) (Set "(" ($#k9_compos_1 :::"Load"::: ) (Set (Var "i")) ")" ))))); registrationlet "S" be ($#l1_compos_1 :::"COM-Struct"::: ) ; let "i" be ($#m1_subset_1 :::"Instruction":::) "of" (Set (Const "S")); cluster (Set ($#k11_compos_1 :::"Macro"::: ) "i") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_afinsq_1 :::"initial"::: ) ; end; begin registrationlet "S" be ($#l1_compos_1 :::"COM-Struct"::: ) ; cluster (Set ($#k4_compos_1 :::"Stop"::: ) "S") -> ($#~v2_compos_1 "non" ($#v2_compos_1 :::"halt-free"::: ) ) ; end; registrationlet "S" be ($#l1_compos_1 :::"COM-Struct"::: ) ; cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" "S") ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v5_ordinal1 :::"T-Sequence-like"::: ) ($#v1_finset_1 :::"finite"::: ) ($#v4_card_3 :::"countable"::: ) bbbadV2_PRE_POLY() ($#v1_afinsq_1 :::"initial"::: ) ($#~v2_compos_1 "non" ($#v2_compos_1 :::"halt-free"::: ) ) for ($#m1_hidden :::"set"::: ) ; end; registrationlet "S" be ($#l1_compos_1 :::"COM-Struct"::: ) ; let "p" be (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" (Set (Const "S"))) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"Function":::); let "q" be (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" (Set (Const "S"))) ($#v5_relat_1 :::"-valued"::: ) ($#~v2_compos_1 "non" ($#v2_compos_1 :::"halt-free"::: ) ) ($#m1_hidden :::"Function":::); cluster (Set "p" ($#k1_funct_4 :::"+*"::: ) "q") -> ($#~v2_compos_1 "non" ($#v2_compos_1 :::"halt-free"::: ) ) ; end; registrationlet "S" be ($#l1_compos_1 :::"COM-Struct"::: ) ; let "p" be (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" (Set (Const "S"))) ($#v5_relat_1 :::"-valued"::: ) ($#v1_finset_1 :::"finite"::: ) ($#~v2_compos_1 "non" ($#v2_compos_1 :::"halt-free"::: ) ) ($#m1_hidden :::"Function":::); let "k" be ($#m1_hidden :::"Nat":::); cluster (Set ($#k6_compos_1 :::"Reloc"::: ) "(" "p" "," "k" ")" ) -> (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" "S") ($#v5_relat_1 :::"-valued"::: ) ($#v1_finset_1 :::"finite"::: ) ($#~v2_compos_1 "non" ($#v2_compos_1 :::"halt-free"::: ) ) ; end; registrationlet "S" be ($#l1_compos_1 :::"COM-Struct"::: ) ; cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" "S") ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v5_ordinal1 :::"T-Sequence-like"::: ) ($#v1_finset_1 :::"finite"::: ) ($#v4_card_3 :::"countable"::: ) bbbadV2_PRE_POLY() ($#v1_afinsq_1 :::"initial"::: ) ($#~v2_compos_1 "non" ($#v2_compos_1 :::"halt-free"::: ) ) for ($#m1_hidden :::"set"::: ) ; end; theorem :: COMPOS_1:37 canceled; theorem :: COMPOS_1:38 canceled; theorem :: COMPOS_1:39 canceled; theorem :: COMPOS_1:40 canceled; theorem :: COMPOS_1:41 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "S")) "being" ($#l1_compos_1 :::"COM-Struct"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" (Set (Var "b2"))) ($#v5_relat_1 :::"-valued"::: ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"Function":::) "holds" (Bool (Set ($#k5_compos_1 :::"IncAddr"::: ) "(" (Set "(" (Set (Var "p")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "q")) ")" ) "," (Set (Var "n")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_compos_1 :::"IncAddr"::: ) "(" (Set (Var "p")) "," (Set (Var "n")) ")" ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k5_compos_1 :::"IncAddr"::: ) "(" (Set (Var "q")) "," (Set (Var "n")) ")" ")" )))))) ; theorem :: COMPOS_1:42 (Bool "for" (Set (Var "S")) "being" ($#l1_compos_1 :::"COM-Struct"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" (Set (Var "b1"))) ($#v5_relat_1 :::"-valued"::: ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k6_compos_1 :::"Reloc"::: ) "(" (Set "(" (Set (Var "p")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "q")) ")" ) "," (Set (Var "k")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k6_compos_1 :::"Reloc"::: ) "(" (Set (Var "p")) "," (Set (Var "k")) ")" ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k6_compos_1 :::"Reloc"::: ) "(" (Set (Var "q")) "," (Set (Var "k")) ")" ")" )))))) ; theorem :: COMPOS_1:43 (Bool "for" (Set (Var "S")) "being" ($#l1_compos_1 :::"COM-Struct"::: ) (Bool "for" (Set (Var "p")) "being" (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" (Set (Var "b1"))) ($#v5_relat_1 :::"-valued"::: ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k6_compos_1 :::"Reloc"::: ) "(" (Set "(" ($#k6_compos_1 :::"Reloc"::: ) "(" (Set (Var "p")) "," (Set (Var "m")) ")" ")" ) "," (Set (Var "n")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_compos_1 :::"Reloc"::: ) "(" (Set (Var "p")) "," (Set "(" (Set (Var "m")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "n")) ")" ) ")" ))))) ; theorem :: COMPOS_1:44 (Bool "for" (Set (Var "S")) "being" ($#l1_compos_1 :::"COM-Struct"::: ) (Bool "for" (Set (Var "P")) "," (Set (Var "Q")) "being" (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" (Set (Var "b1"))) ($#v5_relat_1 :::"-valued"::: ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "P")) ($#r1_tarski :::"c="::: ) (Set (Var "Q")))) "holds" (Bool (Set ($#k6_compos_1 :::"Reloc"::: ) "(" (Set (Var "P")) "," (Set (Var "k")) ")" ) ($#r1_tarski :::"c="::: ) (Set ($#k6_compos_1 :::"Reloc"::: ) "(" (Set (Var "Q")) "," (Set (Var "k")) ")" ))))) ; registrationlet "S" be ($#l1_compos_1 :::"COM-Struct"::: ) ; let "P" be ($#m1_hidden :::"preProgram":::) "of" (Set (Const "S")); reduce ; end; theorem :: COMPOS_1:45 (Bool "for" (Set (Var "S")) "being" ($#l1_compos_1 :::"COM-Struct"::: ) (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"preProgram":::) "of" (Set (Var "S")) "holds" (Bool (Set ($#k6_compos_1 :::"Reloc"::: ) "(" (Set (Var "P")) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "P"))))) ; theorem :: COMPOS_1:46 (Bool "for" (Set (Var "il")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "S")) "being" ($#l1_compos_1 :::"COM-Struct"::: ) (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"preProgram":::) "of" (Set (Var "S")) "holds" (Bool "(" (Bool (Set (Var "il")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "P")))) "iff" (Bool (Set (Set (Var "il")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "k"))) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k6_compos_1 :::"Reloc"::: ) "(" (Set (Var "P")) "," (Set (Var "k")) ")" ")" ))) ")" ))))) ; theorem :: COMPOS_1:47 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "S")) "being" ($#l1_compos_1 :::"COM-Struct"::: ) (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Instruction":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" (Set (Var "S"))) "," (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" (Set (Var "S"))) "st" (Bool (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k6_partfun1 :::"id"::: ) (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" (Set (Var "S"))) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set "(" ($#k2_compos_1 :::"halt"::: ) (Set (Var "S")) ")" ) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "i")) ")" )))) "holds" (Bool "for" (Set (Var "s")) "being" (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" (Set (Var "b2"))) ($#v5_relat_1 :::"-valued"::: ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"Function":::) "holds" (Bool (Set ($#k5_compos_1 :::"IncAddr"::: ) "(" (Set "(" (Set (Var "f")) ($#k3_relat_1 :::"*"::: ) (Set (Var "s")) ")" ) "," (Set (Var "n")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k6_partfun1 :::"id"::: ) (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" (Set (Var "S"))) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set "(" ($#k2_compos_1 :::"halt"::: ) (Set (Var "S")) ")" ) ($#k16_funcop_1 :::".-->"::: ) (Set "(" ($#k5_compos_0 :::"IncAddr"::: ) "(" (Set (Var "i")) "," (Set (Var "n")) ")" ")" ) ")" ) ")" ) ($#k3_relat_1 :::"*"::: ) (Set "(" ($#k5_compos_1 :::"IncAddr"::: ) "(" (Set (Var "s")) "," (Set (Var "n")) ")" ")" )))))))) ; theorem :: COMPOS_1:48 (Bool "for" (Set (Var "S")) "being" ($#l1_compos_1 :::"COM-Struct"::: ) (Bool "for" (Set (Var "I")) "," (Set (Var "J")) "being" ($#m1_hidden :::"Program":::) "of" (Set (Var "S")) "holds" (Bool (Set ($#k2_afinsq_1 :::"dom"::: ) (Set (Var "I"))) ($#r1_xboole_0 :::"misses"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k6_compos_1 :::"Reloc"::: ) "(" (Set (Var "J")) "," (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "I")) ")" ) ")" ")" ))))) ; theorem :: COMPOS_1:49 (Bool "for" (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "S")) "being" ($#l1_compos_1 :::"COM-Struct"::: ) (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"preProgram":::) "of" (Set (Var "S")) "holds" (Bool (Set ($#k5_card_1 :::"card"::: ) (Set "(" ($#k6_compos_1 :::"Reloc"::: ) "(" (Set (Var "I")) "," (Set (Var "m")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set (Var "I"))))))) ; theorem :: COMPOS_1:50 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#l1_compos_1 :::"COM-Struct"::: ) (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Instruction":::) "of" (Set (Var "S")) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_afinsq_1 :::"dom"::: ) (Set "(" ($#k9_compos_1 :::"Load"::: ) (Set (Var "i")) ")" ))) "iff" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" )))) ; theorem :: COMPOS_1:51 (Bool "for" (Set (Var "S")) "being" ($#l1_compos_1 :::"COM-Struct"::: ) (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "loc")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "loc")) ($#r2_hidden :::"in"::: ) (Set ($#k2_afinsq_1 :::"dom"::: ) (Set "(" ($#k10_compos_1 :::"stop"::: ) (Set (Var "I")) ")" ))) & (Bool (Set (Set "(" ($#k10_compos_1 :::"stop"::: ) (Set (Var "I")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "loc"))) ($#r1_hidden :::"<>"::: ) (Set ($#k2_compos_1 :::"halt"::: ) (Set (Var "S"))))) "holds" (Bool (Set (Var "loc")) ($#r2_hidden :::"in"::: ) (Set ($#k2_afinsq_1 :::"dom"::: ) (Set (Var "I"))))))) ; theorem :: COMPOS_1:52 (Bool "for" (Set (Var "S")) "being" ($#l1_compos_1 :::"COM-Struct"::: ) (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Instruction":::) "of" (Set (Var "S")) "holds" (Bool "(" (Bool (Set ($#k2_afinsq_1 :::"dom"::: ) (Set "(" ($#k9_compos_1 :::"Load"::: ) (Set (Var "i")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k6_domain_1 :::"}"::: ) )) & (Bool (Set (Set "(" ($#k9_compos_1 :::"Load"::: ) (Set (Var "i")) ")" ) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set (Var "i"))) ")" ))) ; theorem :: COMPOS_1:53 (Bool "for" (Set (Var "S")) "being" ($#l1_compos_1 :::"COM-Struct"::: ) (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Instruction":::) "of" (Set (Var "S")) "holds" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_afinsq_1 :::"dom"::: ) (Set "(" ($#k9_compos_1 :::"Load"::: ) (Set (Var "i")) ")" ))))) ; theorem :: COMPOS_1:54 (Bool "for" (Set (Var "S")) "being" ($#l1_compos_1 :::"COM-Struct"::: ) (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Instruction":::) "of" (Set (Var "S")) "holds" (Bool (Set ($#k5_card_1 :::"card"::: ) (Set "(" ($#k9_compos_1 :::"Load"::: ) (Set (Var "i")) ")" )) ($#r1_hidden :::"="::: ) (Num 1)))) ; theorem :: COMPOS_1:55 (Bool "for" (Set (Var "S")) "being" ($#l1_compos_1 :::"COM-Struct"::: ) (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" (Set (Var "S")) "holds" (Bool (Set ($#k5_card_1 :::"card"::: ) (Set "(" ($#k10_compos_1 :::"stop"::: ) (Set (Var "I")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "I")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1))))) ; theorem :: COMPOS_1:56 (Bool "for" (Set (Var "S")) "being" ($#l1_compos_1 :::"COM-Struct"::: ) (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Instruction":::) "of" (Set (Var "S")) "holds" (Bool (Set ($#k5_card_1 :::"card"::: ) (Set "(" ($#k11_compos_1 :::"Macro"::: ) (Set (Var "i")) ")" )) ($#r1_hidden :::"="::: ) (Num 2)))) ; theorem :: COMPOS_1:57 (Bool "for" (Set (Var "S")) "being" ($#l1_compos_1 :::"COM-Struct"::: ) (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Instruction":::) "of" (Set (Var "S")) "holds" (Bool "(" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_afinsq_1 :::"dom"::: ) (Set "(" ($#k11_compos_1 :::"Macro"::: ) (Set (Var "i")) ")" ))) & (Bool (Num 1) ($#r2_hidden :::"in"::: ) (Set ($#k2_afinsq_1 :::"dom"::: ) (Set "(" ($#k11_compos_1 :::"Macro"::: ) (Set (Var "i")) ")" ))) ")" ))) ; theorem :: COMPOS_1:58 (Bool "for" (Set (Var "S")) "being" ($#l1_compos_1 :::"COM-Struct"::: ) (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Instruction":::) "of" (Set (Var "S")) "holds" (Bool (Set (Set "(" ($#k11_compos_1 :::"Macro"::: ) (Set (Var "i")) ")" ) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set (Var "i"))))) ; theorem :: COMPOS_1:59 (Bool "for" (Set (Var "S")) "being" ($#l1_compos_1 :::"COM-Struct"::: ) (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Instruction":::) "of" (Set (Var "S")) "holds" (Bool (Set (Set "(" ($#k11_compos_1 :::"Macro"::: ) (Set (Var "i")) ")" ) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set ($#k2_compos_1 :::"halt"::: ) (Set (Var "S")))))) ; theorem :: COMPOS_1:60 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#l1_compos_1 :::"COM-Struct"::: ) (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Instruction":::) "of" (Set (Var "S")) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_afinsq_1 :::"dom"::: ) (Set "(" ($#k11_compos_1 :::"Macro"::: ) (Set (Var "i")) ")" ))) "iff" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) "or" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Num 1)) ")" ) ")" )))) ; theorem :: COMPOS_1:61 (Bool "for" (Set (Var "S")) "being" ($#l1_compos_1 :::"COM-Struct"::: ) (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Instruction":::) "of" (Set (Var "S")) "holds" (Bool (Set ($#k2_afinsq_1 :::"dom"::: ) (Set "(" ($#k11_compos_1 :::"Macro"::: ) (Set (Var "i")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k7_domain_1 :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k7_domain_1 :::"}"::: ) )))) ; theorem :: COMPOS_1:62 (Bool "for" (Set (Var "S")) "being" ($#l1_compos_1 :::"COM-Struct"::: ) (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "loc")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "loc")) ($#r2_hidden :::"in"::: ) (Set ($#k2_afinsq_1 :::"dom"::: ) (Set (Var "I"))))) "holds" (Bool (Set (Var "loc")) ($#r2_hidden :::"in"::: ) (Set ($#k2_afinsq_1 :::"dom"::: ) (Set "(" ($#k10_compos_1 :::"stop"::: ) (Set (Var "I")) ")" )))))) ; theorem :: COMPOS_1:63 (Bool "for" (Set (Var "S")) "being" ($#l1_compos_1 :::"COM-Struct"::: ) (Bool "for" (Set (Var "loc")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "I")) "being" ($#v1_afinsq_1 :::"initial"::: ) ($#m1_hidden :::"preProgram":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "loc")) ($#r2_hidden :::"in"::: ) (Set ($#k2_afinsq_1 :::"dom"::: ) (Set (Var "I"))))) "holds" (Bool (Set (Set "(" ($#k10_compos_1 :::"stop"::: ) (Set (Var "I")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "loc"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "I")) ($#k1_funct_1 :::"."::: ) (Set (Var "loc"))))))) ; theorem :: COMPOS_1:64 (Bool "for" (Set (Var "S")) "being" ($#l1_compos_1 :::"COM-Struct"::: ) (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" (Set (Var "S")) "holds" (Bool "(" (Bool (Set ($#k5_card_1 :::"card"::: ) (Set (Var "I"))) ($#r2_hidden :::"in"::: ) (Set ($#k2_afinsq_1 :::"dom"::: ) (Set "(" ($#k10_compos_1 :::"stop"::: ) (Set (Var "I")) ")" ))) & (Bool (Set (Set "(" ($#k10_compos_1 :::"stop"::: ) (Set (Var "I")) ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "I")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_compos_1 :::"halt"::: ) (Set (Var "S")))) ")" ))) ; theorem :: COMPOS_1:65 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "S")) "being" ($#l1_compos_1 :::"COM-Struct"::: ) (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "loc")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "loc")) ($#r2_hidden :::"in"::: ) (Set ($#k2_afinsq_1 :::"dom"::: ) (Set (Var "I"))))) "holds" (Bool (Set (Set "(" ($#k61_valued_1 :::"Shift"::: ) "(" (Set "(" ($#k10_compos_1 :::"stop"::: ) (Set (Var "I")) ")" ) "," (Set (Var "n")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "loc")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "n")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k61_valued_1 :::"Shift"::: ) "(" (Set (Var "I")) "," (Set (Var "n")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "loc")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "n")) ")" ))))))) ; theorem :: COMPOS_1:66 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "S")) "being" ($#l1_compos_1 :::"COM-Struct"::: ) (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" (Set (Var "S")) "holds" (Bool (Set (Set "(" ($#k61_valued_1 :::"Shift"::: ) "(" (Set "(" ($#k10_compos_1 :::"stop"::: ) (Set (Var "I")) ")" ) "," (Set (Var "n")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k61_valued_1 :::"Shift"::: ) "(" (Set (Var "I")) "," (Set (Var "n")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))))))) ; registrationlet "S" be ($#l1_compos_1 :::"COM-Struct"::: ) ; cluster ($#v1_xboole_0 :::"empty"::: ) ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" "S") ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_finset_1 :::"finite"::: ) ($#v4_card_3 :::"countable"::: ) bbbadV2_PRE_POLY() for ($#m1_hidden :::"set"::: ) ; end; registrationlet "S" be ($#l1_compos_1 :::"COM-Struct"::: ) ; cluster ($#v1_xboole_0 :::"empty"::: ) ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" "S") ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_finset_1 :::"finite"::: ) -> ($#v2_compos_1 :::"halt-free"::: ) for ($#m1_hidden :::"set"::: ) ; end; definitioncanceled; let "S" be ($#l1_compos_1 :::"COM-Struct"::: ) ; let "IT" be (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" (Set (Const "S"))) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"Function":::); redefine attr "IT" is :::"halt-free"::: means :: COMPOS_1:def 27 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) "IT"))) "holds" (Bool (Set "IT" ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"<>"::: ) (Set ($#k2_compos_1 :::"halt"::: ) "S"))); end; :: deftheorem COMPOS_1:def 26 : canceled; :: deftheorem defines :::"halt-free"::: COMPOS_1:def 27 : (Bool "for" (Set (Var "S")) "being" ($#l1_compos_1 :::"COM-Struct"::: ) (Bool "for" (Set (Var "IT")) "being" (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" (Set (Var "b1"))) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v2_compos_1 :::"halt-free"::: ) ) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "IT"))))) "holds" (Bool (Set (Set (Var "IT")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"<>"::: ) (Set ($#k2_compos_1 :::"halt"::: ) (Set (Var "S"))))) ")" ))); registrationlet "S" be ($#l1_compos_1 :::"COM-Struct"::: ) ; cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" "S") ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_finset_1 :::"finite"::: ) ($#v2_compos_1 :::"halt-free"::: ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v4_compos_1 :::"unique-halt"::: ) for ($#m1_hidden :::"set"::: ) ; end; theorem :: COMPOS_1:67 (Bool "for" (Set (Var "S")) "being" ($#l1_compos_1 :::"COM-Struct"::: ) (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Instruction":::) "of" (Set (Var "S")) "holds" (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" ($#k11_compos_1 :::"Macro"::: ) (Set (Var "i")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k7_domain_1 :::"{"::: ) (Set (Var "i")) "," (Set "(" ($#k2_compos_1 :::"halt"::: ) (Set (Var "S")) ")" ) ($#k7_domain_1 :::"}"::: ) )))) ; registrationlet "S" be ($#l1_compos_1 :::"COM-Struct"::: ) ; let "p" be ($#v1_afinsq_1 :::"initial"::: ) ($#m1_hidden :::"preProgram":::) "of" (Set (Const "S")); reduce ; end; theorem :: COMPOS_1:68 (Bool "for" (Set (Var "S")) "being" ($#l1_compos_1 :::"COM-Struct"::: ) (Bool "for" (Set (Var "p")) "being" ($#v1_afinsq_1 :::"initial"::: ) ($#m1_hidden :::"preProgram":::) "of" (Set (Var "S")) "holds" (Bool (Set ($#k63_valued_1 :::"CutLastLoc"::: ) (Set "(" ($#k10_compos_1 :::"stop"::: ) (Set (Var "p")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "p"))))) ; registrationlet "S" be ($#l1_compos_1 :::"COM-Struct"::: ) ; let "p" be ($#v1_afinsq_1 :::"initial"::: ) ($#v2_compos_1 :::"halt-free"::: ) ($#m1_hidden :::"preProgram":::) "of" (Set (Const "S")); cluster (Set ($#k10_compos_1 :::"stop"::: ) "p") -> ($#v4_compos_1 :::"unique-halt"::: ) ; end; registrationlet "S" be ($#l1_compos_1 :::"COM-Struct"::: ) ; let "I" be ($#m1_hidden :::"Program":::) "of" (Set (Const "S")); let "J" be ($#~v2_compos_1 "non" ($#v2_compos_1 :::"halt-free"::: ) ) ($#m1_hidden :::"Program":::) "of" (Set (Const "S")); cluster (Set "I" ($#k7_compos_1 :::"';'"::: ) "J") -> ($#~v2_compos_1 "non" ($#v2_compos_1 :::"halt-free"::: ) ) ; end; theorem :: COMPOS_1:69 (Bool "for" (Set (Var "S")) "being" ($#l1_compos_1 :::"COM-Struct"::: ) (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" (Set (Var "S")) "holds" (Bool (Set ($#k63_valued_1 :::"CutLastLoc"::: ) (Set "(" ($#k10_compos_1 :::"stop"::: ) (Set (Var "I")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "I"))))) ; theorem :: COMPOS_1:70 (Bool "for" (Set (Var "S")) "being" ($#l1_compos_1 :::"COM-Struct"::: ) "holds" (Bool (Set ($#k2_compos_0 :::"InsCode"::: ) (Set "(" ($#k2_compos_1 :::"halt"::: ) (Set (Var "S")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) ;