:: COMPOS_2 semantic presentation begin registration cluster ($#v1_amistd_4 :::"with_non_trivial_Instructions"::: ) for ($#l1_compos_1 :::"COM-Struct"::: ) ; end; registrationlet "S" be ($#v1_amistd_4 :::"with_non_trivial_Instructions"::: ) ($#l1_compos_1 :::"COM-Struct"::: ) ; cluster ($#v6_compos_0 :::"No-StopCode"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" "S"); end; registrationlet "S" be ($#v1_amistd_4 :::"with_non_trivial_Instructions"::: ) ($#l1_compos_1 :::"COM-Struct"::: ) ; let "i" be ($#v6_compos_0 :::"No-StopCode"::: ) ($#m1_subset_1 :::"Instruction":::) "of" (Set (Const "S")); cluster (Set ($#k11_compos_1 :::"Macro"::: ) "i") -> ($#v3_compos_1 :::"halt-ending"::: ) ($#v4_compos_1 :::"unique-halt"::: ) ; end; definitionlet "S" be ($#v1_amistd_4 :::"with_non_trivial_Instructions"::: ) ($#l1_compos_1 :::"COM-Struct"::: ) ; let "i" be ($#v6_compos_0 :::"No-StopCode"::: ) ($#m1_subset_1 :::"Instruction":::) "of" (Set (Const "S")); let "J" be ($#m1_hidden :::"MacroInstruction":::) "of" (Set (Const "S")); func "i" :::"';'"::: "J" -> ($#m1_hidden :::"MacroInstruction":::) "of" "S" equals :: COMPOS_2:def 1 (Set (Set "(" ($#k11_compos_1 :::"Macro"::: ) "i" ")" ) ($#k8_compos_1 :::"';'"::: ) "J"); end; :: deftheorem defines :::"';'"::: COMPOS_2:def 1 : (Bool "for" (Set (Var "S")) "being" ($#v1_amistd_4 :::"with_non_trivial_Instructions"::: ) ($#l1_compos_1 :::"COM-Struct"::: ) (Bool "for" (Set (Var "i")) "being" ($#v6_compos_0 :::"No-StopCode"::: ) ($#m1_subset_1 :::"Instruction":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "J")) "being" ($#m1_hidden :::"MacroInstruction":::) "of" (Set (Var "S")) "holds" (Bool (Set (Set (Var "i")) ($#k1_compos_2 :::"';'"::: ) (Set (Var "J"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k11_compos_1 :::"Macro"::: ) (Set (Var "i")) ")" ) ($#k8_compos_1 :::"';'"::: ) (Set (Var "J"))))))); definitionlet "S" be ($#v1_amistd_4 :::"with_non_trivial_Instructions"::: ) ($#l1_compos_1 :::"COM-Struct"::: ) ; let "I" be ($#m1_hidden :::"MacroInstruction":::) "of" (Set (Const "S")); let "j" be ($#v6_compos_0 :::"No-StopCode"::: ) ($#m1_subset_1 :::"Instruction":::) "of" (Set (Const "S")); func "I" :::"';'"::: "j" -> ($#m1_hidden :::"MacroInstruction":::) "of" "S" equals :: COMPOS_2:def 2 (Set "I" ($#k8_compos_1 :::"';'"::: ) (Set "(" ($#k11_compos_1 :::"Macro"::: ) "j" ")" )); end; :: deftheorem defines :::"';'"::: COMPOS_2:def 2 : (Bool "for" (Set (Var "S")) "being" ($#v1_amistd_4 :::"with_non_trivial_Instructions"::: ) ($#l1_compos_1 :::"COM-Struct"::: ) (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"MacroInstruction":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "j")) "being" ($#v6_compos_0 :::"No-StopCode"::: ) ($#m1_subset_1 :::"Instruction":::) "of" (Set (Var "S")) "holds" (Bool (Set (Set (Var "I")) ($#k2_compos_2 :::"';'"::: ) (Set (Var "j"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "I")) ($#k8_compos_1 :::"';'"::: ) (Set "(" ($#k11_compos_1 :::"Macro"::: ) (Set (Var "j")) ")" )))))); definitionlet "S" be ($#v1_amistd_4 :::"with_non_trivial_Instructions"::: ) ($#l1_compos_1 :::"COM-Struct"::: ) ; let "i", "j" be ($#v6_compos_0 :::"No-StopCode"::: ) ($#m1_subset_1 :::"Instruction":::) "of" (Set (Const "S")); func "i" :::"';'"::: "j" -> ($#m1_hidden :::"MacroInstruction":::) "of" "S" equals :: COMPOS_2:def 3 (Set (Set "(" ($#k11_compos_1 :::"Macro"::: ) "i" ")" ) ($#k8_compos_1 :::"';'"::: ) (Set "(" ($#k11_compos_1 :::"Macro"::: ) "j" ")" )); end; :: deftheorem defines :::"';'"::: COMPOS_2:def 3 : (Bool "for" (Set (Var "S")) "being" ($#v1_amistd_4 :::"with_non_trivial_Instructions"::: ) ($#l1_compos_1 :::"COM-Struct"::: ) (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#v6_compos_0 :::"No-StopCode"::: ) ($#m1_subset_1 :::"Instruction":::) "of" (Set (Var "S")) "holds" (Bool (Set (Set (Var "i")) ($#k3_compos_2 :::"';'"::: ) (Set (Var "j"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k11_compos_1 :::"Macro"::: ) (Set (Var "i")) ")" ) ($#k8_compos_1 :::"';'"::: ) (Set "(" ($#k11_compos_1 :::"Macro"::: ) (Set (Var "j")) ")" ))))); theorem :: COMPOS_2:1 (Bool "for" (Set (Var "S")) "being" ($#v1_amistd_4 :::"with_non_trivial_Instructions"::: ) ($#l1_compos_1 :::"COM-Struct"::: ) (Bool "for" (Set (Var "k")) "being" ($#v6_compos_0 :::"No-StopCode"::: ) ($#m1_subset_1 :::"Instruction":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "I")) "," (Set (Var "J")) "being" ($#m1_hidden :::"MacroInstruction":::) "of" (Set (Var "S")) "holds" (Bool (Set (Set "(" (Set (Var "I")) ($#k8_compos_1 :::"';'"::: ) (Set (Var "J")) ")" ) ($#k2_compos_2 :::"';'"::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "I")) ($#k8_compos_1 :::"';'"::: ) (Set "(" (Set (Var "J")) ($#k2_compos_2 :::"';'"::: ) (Set (Var "k")) ")" )))))) ; theorem :: COMPOS_2:2 (Bool "for" (Set (Var "S")) "being" ($#v1_amistd_4 :::"with_non_trivial_Instructions"::: ) ($#l1_compos_1 :::"COM-Struct"::: ) (Bool "for" (Set (Var "j")) "being" ($#v6_compos_0 :::"No-StopCode"::: ) ($#m1_subset_1 :::"Instruction":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "I")) "," (Set (Var "K")) "being" ($#m1_hidden :::"MacroInstruction":::) "of" (Set (Var "S")) "holds" (Bool (Set (Set "(" (Set (Var "I")) ($#k2_compos_2 :::"';'"::: ) (Set (Var "j")) ")" ) ($#k8_compos_1 :::"';'"::: ) (Set (Var "K"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "I")) ($#k8_compos_1 :::"';'"::: ) (Set "(" (Set (Var "j")) ($#k1_compos_2 :::"';'"::: ) (Set (Var "K")) ")" )))))) ; theorem :: COMPOS_2:3 (Bool "for" (Set (Var "S")) "being" ($#v1_amistd_4 :::"with_non_trivial_Instructions"::: ) ($#l1_compos_1 :::"COM-Struct"::: ) (Bool "for" (Set (Var "j")) "," (Set (Var "k")) "being" ($#v6_compos_0 :::"No-StopCode"::: ) ($#m1_subset_1 :::"Instruction":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"MacroInstruction":::) "of" (Set (Var "S")) "holds" (Bool (Set (Set "(" (Set (Var "I")) ($#k2_compos_2 :::"';'"::: ) (Set (Var "j")) ")" ) ($#k2_compos_2 :::"';'"::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "I")) ($#k8_compos_1 :::"';'"::: ) (Set "(" (Set (Var "j")) ($#k3_compos_2 :::"';'"::: ) (Set (Var "k")) ")" )))))) ; theorem :: COMPOS_2:4 (Bool "for" (Set (Var "S")) "being" ($#v1_amistd_4 :::"with_non_trivial_Instructions"::: ) ($#l1_compos_1 :::"COM-Struct"::: ) (Bool "for" (Set (Var "i")) "being" ($#v6_compos_0 :::"No-StopCode"::: ) ($#m1_subset_1 :::"Instruction":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "J")) "," (Set (Var "K")) "being" ($#m1_hidden :::"MacroInstruction":::) "of" (Set (Var "S")) "holds" (Bool (Set (Set "(" (Set (Var "i")) ($#k1_compos_2 :::"';'"::: ) (Set (Var "J")) ")" ) ($#k8_compos_1 :::"';'"::: ) (Set (Var "K"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "i")) ($#k1_compos_2 :::"';'"::: ) (Set "(" (Set (Var "J")) ($#k8_compos_1 :::"';'"::: ) (Set (Var "K")) ")" )))))) ; theorem :: COMPOS_2:5 (Bool "for" (Set (Var "S")) "being" ($#v1_amistd_4 :::"with_non_trivial_Instructions"::: ) ($#l1_compos_1 :::"COM-Struct"::: ) (Bool "for" (Set (Var "i")) "," (Set (Var "k")) "being" ($#v6_compos_0 :::"No-StopCode"::: ) ($#m1_subset_1 :::"Instruction":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "J")) "being" ($#m1_hidden :::"MacroInstruction":::) "of" (Set (Var "S")) "holds" (Bool (Set (Set "(" (Set (Var "i")) ($#k1_compos_2 :::"';'"::: ) (Set (Var "J")) ")" ) ($#k2_compos_2 :::"';'"::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "i")) ($#k1_compos_2 :::"';'"::: ) (Set "(" (Set (Var "J")) ($#k2_compos_2 :::"';'"::: ) (Set (Var "k")) ")" )))))) ; theorem :: COMPOS_2:6 (Bool "for" (Set (Var "S")) "being" ($#v1_amistd_4 :::"with_non_trivial_Instructions"::: ) ($#l1_compos_1 :::"COM-Struct"::: ) (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#v6_compos_0 :::"No-StopCode"::: ) ($#m1_subset_1 :::"Instruction":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "K")) "being" ($#m1_hidden :::"MacroInstruction":::) "of" (Set (Var "S")) "holds" (Bool (Set (Set "(" (Set (Var "i")) ($#k3_compos_2 :::"';'"::: ) (Set (Var "j")) ")" ) ($#k8_compos_1 :::"';'"::: ) (Set (Var "K"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "i")) ($#k1_compos_2 :::"';'"::: ) (Set "(" (Set (Var "j")) ($#k1_compos_2 :::"';'"::: ) (Set (Var "K")) ")" )))))) ; theorem :: COMPOS_2:7 (Bool "for" (Set (Var "S")) "being" ($#v1_amistd_4 :::"with_non_trivial_Instructions"::: ) ($#l1_compos_1 :::"COM-Struct"::: ) (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "k")) "being" ($#v6_compos_0 :::"No-StopCode"::: ) ($#m1_subset_1 :::"Instruction":::) "of" (Set (Var "S")) "holds" (Bool (Set (Set "(" (Set (Var "i")) ($#k3_compos_2 :::"';'"::: ) (Set (Var "j")) ")" ) ($#k2_compos_2 :::"';'"::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "i")) ($#k1_compos_2 :::"';'"::: ) (Set "(" (Set (Var "j")) ($#k3_compos_2 :::"';'"::: ) (Set (Var "k")) ")" ))))) ; theorem :: COMPOS_2:8 (Bool "for" (Set (Var "S")) "being" ($#v1_amistd_4 :::"with_non_trivial_Instructions"::: ) ($#l1_compos_1 :::"COM-Struct"::: ) (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#v6_compos_0 :::"No-StopCode"::: ) ($#m1_subset_1 :::"Instruction":::) "of" (Set (Var "S")) "holds" (Bool (Set (Set (Var "i")) ($#k3_compos_2 :::"';'"::: ) (Set (Var "j"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k11_compos_1 :::"Macro"::: ) (Set (Var "i")) ")" ) ($#k2_compos_2 :::"';'"::: ) (Set (Var "j")))))) ; theorem :: COMPOS_2:9 (Bool "for" (Set (Var "S")) "being" ($#v1_amistd_4 :::"with_non_trivial_Instructions"::: ) ($#l1_compos_1 :::"COM-Struct"::: ) (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#v6_compos_0 :::"No-StopCode"::: ) ($#m1_subset_1 :::"Instruction":::) "of" (Set (Var "S")) "holds" (Bool (Set (Set (Var "i")) ($#k3_compos_2 :::"';'"::: ) (Set (Var "j"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "i")) ($#k1_compos_2 :::"';'"::: ) (Set "(" ($#k11_compos_1 :::"Macro"::: ) (Set (Var "j")) ")" ))))) ; theorem :: COMPOS_2:10 (Bool "for" (Set (Var "S")) "being" ($#v1_amistd_4 :::"with_non_trivial_Instructions"::: ) ($#l1_compos_1 :::"COM-Struct"::: ) (Bool "for" (Set (Var "i")) "being" ($#v6_compos_0 :::"No-StopCode"::: ) ($#m1_subset_1 :::"Instruction":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "J")) "being" ($#m1_hidden :::"MacroInstruction":::) "of" (Set (Var "S")) "holds" (Bool (Set ($#k5_card_1 :::"card"::: ) (Set "(" (Set (Var "i")) ($#k1_compos_2 :::"';'"::: ) (Set (Var "J")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "J")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Num 1)))))) ; theorem :: COMPOS_2:11 (Bool "for" (Set (Var "S")) "being" ($#v1_amistd_4 :::"with_non_trivial_Instructions"::: ) ($#l1_compos_1 :::"COM-Struct"::: ) (Bool "for" (Set (Var "j")) "being" ($#v6_compos_0 :::"No-StopCode"::: ) ($#m1_subset_1 :::"Instruction":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"MacroInstruction":::) "of" (Set (Var "S")) "holds" (Bool (Set ($#k5_card_1 :::"card"::: ) (Set "(" (Set (Var "I")) ($#k2_compos_2 :::"';'"::: ) (Set (Var "j")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "I")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Num 1)))))) ; theorem :: COMPOS_2:12 (Bool "for" (Set (Var "S")) "being" ($#v1_amistd_4 :::"with_non_trivial_Instructions"::: ) ($#l1_compos_1 :::"COM-Struct"::: ) (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#v6_compos_0 :::"No-StopCode"::: ) ($#m1_subset_1 :::"Instruction":::) "of" (Set (Var "S")) "holds" (Bool (Set ($#k5_card_1 :::"card"::: ) (Set "(" (Set (Var "i")) ($#k3_compos_2 :::"';'"::: ) (Set (Var "j")) ")" )) ($#r1_hidden :::"="::: ) (Num 3)))) ; theorem :: COMPOS_2:13 (Bool "for" (Set (Var "S")) "being" ($#v1_amistd_4 :::"with_non_trivial_Instructions"::: ) ($#l1_compos_1 :::"COM-Struct"::: ) (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "k")) "being" ($#v6_compos_0 :::"No-StopCode"::: ) ($#m1_subset_1 :::"Instruction":::) "of" (Set (Var "S")) "holds" (Bool (Set ($#k5_card_1 :::"card"::: ) (Set "(" (Set "(" (Set (Var "i")) ($#k3_compos_2 :::"';'"::: ) (Set (Var "j")) ")" ) ($#k2_compos_2 :::"';'"::: ) (Set (Var "k")) ")" )) ($#r1_hidden :::"="::: ) (Num 4)))) ; theorem :: COMPOS_2:14 (Bool "for" (Set (Var "S")) "being" ($#v1_amistd_4 :::"with_non_trivial_Instructions"::: ) ($#l1_compos_1 :::"COM-Struct"::: ) (Bool "for" (Set (Var "i1")) "," (Set (Var "i2")) "," (Set (Var "i3")) "," (Set (Var "i4")) "being" ($#v6_compos_0 :::"No-StopCode"::: ) ($#m1_subset_1 :::"Instruction":::) "of" (Set (Var "S")) "holds" (Bool (Set ($#k5_card_1 :::"card"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "i1")) ($#k3_compos_2 :::"';'"::: ) (Set (Var "i2")) ")" ) ($#k2_compos_2 :::"';'"::: ) (Set (Var "i3")) ")" ) ($#k2_compos_2 :::"';'"::: ) (Set (Var "i4")) ")" )) ($#r1_hidden :::"="::: ) (Num 5)))) ; theorem :: COMPOS_2:15 (Bool "for" (Set (Var "S")) "being" ($#v1_amistd_4 :::"with_non_trivial_Instructions"::: ) ($#l1_compos_1 :::"COM-Struct"::: ) (Bool "for" (Set (Var "i1")) "," (Set (Var "i2")) "," (Set (Var "i3")) "," (Set (Var "i4")) "," (Set (Var "i5")) "being" ($#v6_compos_0 :::"No-StopCode"::: ) ($#m1_subset_1 :::"Instruction":::) "of" (Set (Var "S")) "holds" (Bool (Set ($#k5_card_1 :::"card"::: ) (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "i1")) ($#k3_compos_2 :::"';'"::: ) (Set (Var "i2")) ")" ) ($#k2_compos_2 :::"';'"::: ) (Set (Var "i3")) ")" ) ($#k2_compos_2 :::"';'"::: ) (Set (Var "i4")) ")" ) ($#k2_compos_2 :::"';'"::: ) (Set (Var "i5")) ")" )) ($#r1_hidden :::"="::: ) (Num 6)))) ; theorem :: COMPOS_2:16 (Bool "for" (Set (Var "S")) "being" ($#v1_amistd_4 :::"with_non_trivial_Instructions"::: ) ($#l1_compos_1 :::"COM-Struct"::: ) (Bool "for" (Set (Var "i1")) "," (Set (Var "i2")) "," (Set (Var "i3")) "," (Set (Var "i4")) "," (Set (Var "i5")) "," (Set (Var "i6")) "being" ($#v6_compos_0 :::"No-StopCode"::: ) ($#m1_subset_1 :::"Instruction":::) "of" (Set (Var "S")) "holds" (Bool (Set ($#k5_card_1 :::"card"::: ) (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "i1")) ($#k3_compos_2 :::"';'"::: ) (Set (Var "i2")) ")" ) ($#k2_compos_2 :::"';'"::: ) (Set (Var "i3")) ")" ) ($#k2_compos_2 :::"';'"::: ) (Set (Var "i4")) ")" ) ($#k2_compos_2 :::"';'"::: ) (Set (Var "i5")) ")" ) ($#k2_compos_2 :::"';'"::: ) (Set (Var "i6")) ")" )) ($#r1_hidden :::"="::: ) (Num 7)))) ; definitionlet "I" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"Function":::); let "J" be ($#m1_hidden :::"set"::: ) ; pred "I" :::"<="::: "J" means :: COMPOS_2:def 4 (Bool (Set ($#k63_valued_1 :::"CutLastLoc"::: ) "I") ($#r1_tarski :::"c="::: ) "J"); end; :: deftheorem defines :::"<="::: COMPOS_2:def 4 : (Bool "for" (Set (Var "I")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "J")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "I")) ($#r1_compos_2 :::"<="::: ) (Set (Var "J"))) "iff" (Bool (Set ($#k63_valued_1 :::"CutLastLoc"::: ) (Set (Var "I"))) ($#r1_tarski :::"c="::: ) (Set (Var "J"))) ")" ))); definitionlet "I", "J" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"Function":::); :: original: :::"<="::: redefine pred "I" :::"<="::: "J"; reflexivity (Bool "for" (Set (Var "I")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"Function":::) "holds" (Bool ((Set (Var "b1")) "," (Set (Var "b1"))))) ; end; theorem :: COMPOS_2:17 (Bool "for" (Set (Var "F")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"Function":::) "holds" (Bool (Bool "not" (Set ($#k62_valued_1 :::"LastLoc"::: ) (Set (Var "F"))) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k63_valued_1 :::"CutLastLoc"::: ) (Set (Var "F")) ")" ))))) ; registrationlet "S" be ($#v1_amistd_4 :::"with_non_trivial_Instructions"::: ) ($#l1_compos_1 :::"COM-Struct"::: ) ; let "I" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v4_compos_1 :::"unique-halt"::: ) ($#m1_hidden :::"preProgram":::) "of" (Set (Const "S")); cluster (Set ($#k63_valued_1 :::"CutLastLoc"::: ) "I") -> ($#v2_compos_1 :::"halt-free"::: ) ; end; theorem :: COMPOS_2:18 (Bool "for" (Set (Var "S")) "being" ($#v1_amistd_4 :::"with_non_trivial_Instructions"::: ) ($#l1_compos_1 :::"COM-Struct"::: ) (Bool "for" (Set (Var "I")) "being" ($#v4_compos_1 :::"unique-halt"::: ) ($#m1_hidden :::"Program":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "J")) "being" ($#v3_compos_1 :::"halt-ending"::: ) ($#m1_hidden :::"Program":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set ($#k63_valued_1 :::"CutLastLoc"::: ) (Set (Var "I"))) ($#r1_tarski :::"c="::: ) (Set (Var "J")))) "holds" (Bool (Set ($#k63_valued_1 :::"CutLastLoc"::: ) (Set (Var "I"))) ($#r1_tarski :::"c="::: ) (Set ($#k63_valued_1 :::"CutLastLoc"::: ) (Set (Var "J"))))))) ; theorem :: COMPOS_2:19 (Bool "for" (Set (Var "S")) "being" ($#v1_amistd_4 :::"with_non_trivial_Instructions"::: ) ($#l1_compos_1 :::"COM-Struct"::: ) (Bool "for" (Set (Var "I")) "," (Set (Var "J")) "being" ($#m1_hidden :::"MacroInstruction":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "K")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "I")) ($#r2_compos_2 :::"<="::: ) (Set (Var "J"))) & (Bool (Set (Var "J")) ($#r1_compos_2 :::"<="::: ) (Set (Var "K")))) "holds" (Bool (Set (Var "I")) ($#r1_compos_2 :::"<="::: ) (Set (Var "K")))))) ; theorem :: COMPOS_2:20 (Bool "for" (Set (Var "S")) "being" ($#v1_amistd_4 :::"with_non_trivial_Instructions"::: ) ($#l1_compos_1 :::"COM-Struct"::: ) (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"MacroInstruction":::) "of" (Set (Var "S")) "holds" (Bool (Set (Var "I")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k63_valued_1 :::"CutLastLoc"::: ) (Set (Var "I")) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set "(" ($#k62_valued_1 :::"LastLoc"::: ) (Set (Var "I")) ")" ) ($#k16_funcop_1 :::".-->"::: ) (Set "(" ($#k2_compos_1 :::"halt"::: ) (Set (Var "S")) ")" ) ")" ))))) ; theorem :: COMPOS_2:21 (Bool "for" (Set (Var "S")) "being" ($#v1_amistd_4 :::"with_non_trivial_Instructions"::: ) ($#l1_compos_1 :::"COM-Struct"::: ) (Bool "for" (Set (Var "I")) "," (Set (Var "J")) "being" ($#m1_hidden :::"MacroInstruction":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set ($#k63_valued_1 :::"CutLastLoc"::: ) (Set (Var "I"))) ($#r1_hidden :::"="::: ) (Set ($#k63_valued_1 :::"CutLastLoc"::: ) (Set (Var "J"))))) "holds" (Bool (Set (Var "I")) ($#r1_hidden :::"="::: ) (Set (Var "J"))))) ; theorem :: COMPOS_2:22 (Bool "for" (Set (Var "S")) "being" ($#v1_amistd_4 :::"with_non_trivial_Instructions"::: ) ($#l1_compos_1 :::"COM-Struct"::: ) (Bool "for" (Set (Var "I")) "," (Set (Var "J")) "being" ($#m1_hidden :::"MacroInstruction":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "I")) ($#r2_compos_2 :::"<="::: ) (Set (Var "J"))) & (Bool (Set (Var "J")) ($#r2_compos_2 :::"<="::: ) (Set (Var "I")))) "holds" (Bool (Set (Var "I")) ($#r1_hidden :::"="::: ) (Set (Var "J"))))) ; theorem :: COMPOS_2:23 (Bool "for" (Set (Var "S")) "being" ($#v1_amistd_4 :::"with_non_trivial_Instructions"::: ) ($#l1_compos_1 :::"COM-Struct"::: ) (Bool "for" (Set (Var "I")) "," (Set (Var "J")) "being" ($#m1_hidden :::"MacroInstruction":::) "of" (Set (Var "S")) "holds" (Bool (Set (Var "I")) ($#r2_compos_2 :::"<="::: ) (Set (Set (Var "I")) ($#k8_compos_1 :::"';'"::: ) (Set (Var "J")))))) ; theorem :: COMPOS_2:24 (Bool "for" (Set (Var "S")) "being" ($#v1_amistd_4 :::"with_non_trivial_Instructions"::: ) ($#l1_compos_1 :::"COM-Struct"::: ) (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"MacroInstruction":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "I")) ($#r1_tarski :::"c="::: ) (Set (Var "X")))) "holds" (Bool (Set (Var "I")) ($#r1_compos_2 :::"<="::: ) (Set (Var "X")))))) ; theorem :: COMPOS_2:25 (Bool "for" (Set (Var "S")) "being" ($#v1_amistd_4 :::"with_non_trivial_Instructions"::: ) ($#l1_compos_1 :::"COM-Struct"::: ) (Bool "for" (Set (Var "I")) "," (Set (Var "J")) "being" ($#m1_hidden :::"MacroInstruction":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "I")) ($#r2_compos_2 :::"<="::: ) (Set (Var "J")))) "holds" (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "J")) ($#r1_tarski :::"c="::: ) (Set (Var "X")))) "holds" (Bool (Set (Var "I")) ($#r1_compos_2 :::"<="::: ) (Set (Var "X")))))) ; theorem :: COMPOS_2:26 (Bool "for" (Set (Var "S")) "being" ($#v1_amistd_4 :::"with_non_trivial_Instructions"::: ) ($#l1_compos_1 :::"COM-Struct"::: ) (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"MacroInstruction":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool "(" (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k62_valued_1 :::"LastLoc"::: ) (Set (Var "I")))) "iff" (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k63_valued_1 :::"CutLastLoc"::: ) (Set (Var "I")) ")" ))) ")" )))) ; theorem :: COMPOS_2:27 (Bool "for" (Set (Var "S")) "being" ($#v1_amistd_4 :::"with_non_trivial_Instructions"::: ) ($#l1_compos_1 :::"COM-Struct"::: ) (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"MacroInstruction":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k62_valued_1 :::"LastLoc"::: ) (Set (Var "I"))))) "holds" (Bool (Set (Set "(" ($#k63_valued_1 :::"CutLastLoc"::: ) (Set (Var "I")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "I")) ($#k1_funct_1 :::"."::: ) (Set (Var "k"))))))) ; theorem :: COMPOS_2:28 (Bool "for" (Set (Var "S")) "being" ($#v1_amistd_4 :::"with_non_trivial_Instructions"::: ) ($#l1_compos_1 :::"COM-Struct"::: ) (Bool "for" (Set (Var "I")) "," (Set (Var "J")) "being" ($#m1_hidden :::"MacroInstruction":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k62_valued_1 :::"LastLoc"::: ) (Set (Var "I")))) & (Bool (Set (Var "I")) ($#r2_compos_2 :::"<="::: ) (Set (Var "J")))) "holds" (Bool (Set (Set (Var "I")) ($#k1_funct_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "J")) ($#k1_funct_1 :::"."::: ) (Set (Var "k"))))))) ; theorem :: COMPOS_2:29 (Bool "for" (Set (Var "S")) "being" ($#v1_amistd_4 :::"with_non_trivial_Instructions"::: ) ($#l1_compos_1 :::"COM-Struct"::: ) (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"MacroInstruction":::) "of" (Set (Var "S")) "holds" (Bool (Set ($#k62_valued_1 :::"LastLoc"::: ) (Set (Var "I"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "I")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Num 1))))) ; theorem :: COMPOS_2:30 (Bool "for" (Set (Var "S")) "being" ($#v1_amistd_4 :::"with_non_trivial_Instructions"::: ) ($#l1_compos_1 :::"COM-Struct"::: ) (Bool "for" (Set (Var "i")) "being" ($#v6_compos_0 :::"No-StopCode"::: ) ($#m1_subset_1 :::"Instruction":::) "of" (Set (Var "S")) "holds" (Bool (Set ($#k62_valued_1 :::"LastLoc"::: ) (Set "(" ($#k11_compos_1 :::"Macro"::: ) (Set (Var "i")) ")" )) ($#r1_hidden :::"="::: ) (Num 1)))) ; theorem :: COMPOS_2:31 (Bool "for" (Set (Var "S")) "being" ($#v1_amistd_4 :::"with_non_trivial_Instructions"::: ) ($#l1_compos_1 :::"COM-Struct"::: ) (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#v6_compos_0 :::"No-StopCode"::: ) ($#m1_subset_1 :::"Instruction":::) "of" (Set (Var "S")) "holds" (Bool (Set ($#k62_valued_1 :::"LastLoc"::: ) (Set "(" (Set (Var "i")) ($#k3_compos_2 :::"';'"::: ) (Set (Var "j")) ")" )) ($#r1_hidden :::"="::: ) (Num 2)))) ; theorem :: COMPOS_2:32 (Bool "for" (Set (Var "S")) "being" ($#v1_amistd_4 :::"with_non_trivial_Instructions"::: ) ($#l1_compos_1 :::"COM-Struct"::: ) (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "k")) "being" ($#v6_compos_0 :::"No-StopCode"::: ) ($#m1_subset_1 :::"Instruction":::) "of" (Set (Var "S")) "holds" (Bool (Set ($#k62_valued_1 :::"LastLoc"::: ) (Set "(" (Set "(" (Set (Var "i")) ($#k3_compos_2 :::"';'"::: ) (Set (Var "j")) ")" ) ($#k2_compos_2 :::"';'"::: ) (Set (Var "k")) ")" )) ($#r1_hidden :::"="::: ) (Num 3)))) ; theorem :: COMPOS_2:33 (Bool "for" (Set (Var "S")) "being" ($#v1_amistd_4 :::"with_non_trivial_Instructions"::: ) ($#l1_compos_1 :::"COM-Struct"::: ) (Bool "for" (Set (Var "i1")) "," (Set (Var "i2")) "," (Set (Var "i3")) "," (Set (Var "i4")) "being" ($#v6_compos_0 :::"No-StopCode"::: ) ($#m1_subset_1 :::"Instruction":::) "of" (Set (Var "S")) "holds" (Bool (Set ($#k62_valued_1 :::"LastLoc"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "i1")) ($#k3_compos_2 :::"';'"::: ) (Set (Var "i2")) ")" ) ($#k2_compos_2 :::"';'"::: ) (Set (Var "i3")) ")" ) ($#k2_compos_2 :::"';'"::: ) (Set (Var "i4")) ")" )) ($#r1_hidden :::"="::: ) (Num 4)))) ; theorem :: COMPOS_2:34 (Bool "for" (Set (Var "S")) "being" ($#v1_amistd_4 :::"with_non_trivial_Instructions"::: ) ($#l1_compos_1 :::"COM-Struct"::: ) (Bool "for" (Set (Var "i1")) "," (Set (Var "i2")) "," (Set (Var "i3")) "," (Set (Var "i4")) "," (Set (Var "i5")) "being" ($#v6_compos_0 :::"No-StopCode"::: ) ($#m1_subset_1 :::"Instruction":::) "of" (Set (Var "S")) "holds" (Bool (Set ($#k62_valued_1 :::"LastLoc"::: ) (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "i1")) ($#k3_compos_2 :::"';'"::: ) (Set (Var "i2")) ")" ) ($#k2_compos_2 :::"';'"::: ) (Set (Var "i3")) ")" ) ($#k2_compos_2 :::"';'"::: ) (Set (Var "i4")) ")" ) ($#k2_compos_2 :::"';'"::: ) (Set (Var "i5")) ")" )) ($#r1_hidden :::"="::: ) (Num 5)))) ; theorem :: COMPOS_2:35 (Bool "for" (Set (Var "S")) "being" ($#v1_amistd_4 :::"with_non_trivial_Instructions"::: ) ($#l1_compos_1 :::"COM-Struct"::: ) (Bool "for" (Set (Var "i1")) "," (Set (Var "i2")) "," (Set (Var "i3")) "," (Set (Var "i4")) "," (Set (Var "i5")) "," (Set (Var "i6")) "being" ($#v6_compos_0 :::"No-StopCode"::: ) ($#m1_subset_1 :::"Instruction":::) "of" (Set (Var "S")) "holds" (Bool (Set ($#k62_valued_1 :::"LastLoc"::: ) (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "i1")) ($#k3_compos_2 :::"';'"::: ) (Set (Var "i2")) ")" ) ($#k2_compos_2 :::"';'"::: ) (Set (Var "i3")) ")" ) ($#k2_compos_2 :::"';'"::: ) (Set (Var "i4")) ")" ) ($#k2_compos_2 :::"';'"::: ) (Set (Var "i5")) ")" ) ($#k2_compos_2 :::"';'"::: ) (Set (Var "i6")) ")" )) ($#r1_hidden :::"="::: ) (Num 6)))) ; theorem :: COMPOS_2:36 (Bool "for" (Set (Var "S")) "being" ($#v1_amistd_4 :::"with_non_trivial_Instructions"::: ) ($#l1_compos_1 :::"COM-Struct"::: ) (Bool "for" (Set (Var "i")) "being" ($#v6_compos_0 :::"No-StopCode"::: ) ($#m1_subset_1 :::"Instruction":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "J")) "being" ($#m1_hidden :::"MacroInstruction":::) "of" (Set (Var "S")) "holds" (Bool (Set (Set "(" (Set (Var "i")) ($#k1_compos_2 :::"';'"::: ) (Set (Var "J")) ")" ) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set (Var "i")))))) ; theorem :: COMPOS_2:37 (Bool "for" (Set (Var "S")) "being" ($#v1_amistd_4 :::"with_non_trivial_Instructions"::: ) ($#l1_compos_1 :::"COM-Struct"::: ) (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#v6_compos_0 :::"No-StopCode"::: ) ($#m1_subset_1 :::"Instruction":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "K")) "being" ($#m1_hidden :::"MacroInstruction":::) "of" (Set (Var "S")) "holds" (Bool (Set (Set "(" (Set "(" (Set (Var "i")) ($#k3_compos_2 :::"';'"::: ) (Set (Var "j")) ")" ) ($#k8_compos_1 :::"';'"::: ) (Set (Var "K")) ")" ) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set (Var "i")))))) ; theorem :: COMPOS_2:38 (Bool "for" (Set (Var "S")) "being" ($#v1_amistd_4 :::"with_non_trivial_Instructions"::: ) ($#l1_compos_1 :::"COM-Struct"::: ) (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "k")) "being" ($#v6_compos_0 :::"No-StopCode"::: ) ($#m1_subset_1 :::"Instruction":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "K")) "being" ($#m1_hidden :::"MacroInstruction":::) "of" (Set (Var "S")) "holds" (Bool (Set (Set "(" (Set "(" (Set "(" (Set (Var "i")) ($#k3_compos_2 :::"';'"::: ) (Set (Var "j")) ")" ) ($#k2_compos_2 :::"';'"::: ) (Set (Var "k")) ")" ) ($#k8_compos_1 :::"';'"::: ) (Set (Var "K")) ")" ) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set (Var "i")))))) ; theorem :: COMPOS_2:39 (Bool "for" (Set (Var "S")) "being" ($#v1_amistd_4 :::"with_non_trivial_Instructions"::: ) ($#l1_compos_1 :::"COM-Struct"::: ) (Bool "for" (Set (Var "K")) "being" ($#m1_hidden :::"MacroInstruction":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "i1")) "," (Set (Var "i2")) "," (Set (Var "i3")) "," (Set (Var "i4")) "being" ($#v6_compos_0 :::"No-StopCode"::: ) ($#m1_subset_1 :::"Instruction":::) "of" (Set (Var "S")) "holds" (Bool (Set (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "i1")) ($#k3_compos_2 :::"';'"::: ) (Set (Var "i2")) ")" ) ($#k2_compos_2 :::"';'"::: ) (Set (Var "i3")) ")" ) ($#k2_compos_2 :::"';'"::: ) (Set (Var "i4")) ")" ) ($#k8_compos_1 :::"';'"::: ) (Set (Var "K")) ")" ) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set (Var "i1")))))) ; theorem :: COMPOS_2:40 (Bool "for" (Set (Var "S")) "being" ($#v1_amistd_4 :::"with_non_trivial_Instructions"::: ) ($#l1_compos_1 :::"COM-Struct"::: ) (Bool "for" (Set (Var "K")) "being" ($#m1_hidden :::"MacroInstruction":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "i1")) "," (Set (Var "i2")) "," (Set (Var "i3")) "," (Set (Var "i4")) "," (Set (Var "i5")) "being" ($#v6_compos_0 :::"No-StopCode"::: ) ($#m1_subset_1 :::"Instruction":::) "of" (Set (Var "S")) "holds" (Bool (Set (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "i1")) ($#k3_compos_2 :::"';'"::: ) (Set (Var "i2")) ")" ) ($#k2_compos_2 :::"';'"::: ) (Set (Var "i3")) ")" ) ($#k2_compos_2 :::"';'"::: ) (Set (Var "i4")) ")" ) ($#k2_compos_2 :::"';'"::: ) (Set (Var "i5")) ")" ) ($#k8_compos_1 :::"';'"::: ) (Set (Var "K")) ")" ) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set (Var "i1")))))) ; theorem :: COMPOS_2:41 (Bool "for" (Set (Var "S")) "being" ($#v1_amistd_4 :::"with_non_trivial_Instructions"::: ) ($#l1_compos_1 :::"COM-Struct"::: ) (Bool "for" (Set (Var "K")) "being" ($#m1_hidden :::"MacroInstruction":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "i1")) "," (Set (Var "i2")) "," (Set (Var "i3")) "," (Set (Var "i4")) "," (Set (Var "i5")) "," (Set (Var "i6")) "being" ($#v6_compos_0 :::"No-StopCode"::: ) ($#m1_subset_1 :::"Instruction":::) "of" (Set (Var "S")) "holds" (Bool (Set (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "i1")) ($#k3_compos_2 :::"';'"::: ) (Set (Var "i2")) ")" ) ($#k2_compos_2 :::"';'"::: ) (Set (Var "i3")) ")" ) ($#k2_compos_2 :::"';'"::: ) (Set (Var "i4")) ")" ) ($#k2_compos_2 :::"';'"::: ) (Set (Var "i5")) ")" ) ($#k2_compos_2 :::"';'"::: ) (Set (Var "i6")) ")" ) ($#k8_compos_1 :::"';'"::: ) (Set (Var "K")) ")" ) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set (Var "i1")))))) ; theorem :: COMPOS_2:42 (Bool "for" (Set (Var "S")) "being" ($#v1_amistd_4 :::"with_non_trivial_Instructions"::: ) ($#l1_compos_1 :::"COM-Struct"::: ) (Bool "for" (Set (Var "I")) "," (Set (Var "J")) "being" ($#m1_hidden :::"MacroInstruction":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k62_valued_1 :::"LastLoc"::: ) (Set (Var "I"))))) "holds" (Bool (Set (Set "(" (Set (Var "I")) ($#k8_compos_1 :::"';'"::: ) (Set (Var "J")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "I")) ($#k1_funct_1 :::"."::: ) (Set (Var "k"))))))) ; theorem :: COMPOS_2:43 (Bool "for" (Set (Var "S")) "being" ($#v1_amistd_4 :::"with_non_trivial_Instructions"::: ) ($#l1_compos_1 :::"COM-Struct"::: ) (Bool "for" (Set (Var "I")) "," (Set (Var "J")) "being" ($#m1_hidden :::"MacroInstruction":::) "of" (Set (Var "S")) "holds" (Bool (Set ($#k62_valued_1 :::"LastLoc"::: ) (Set "(" (Set (Var "I")) ($#k8_compos_1 :::"';'"::: ) (Set (Var "J")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k62_valued_1 :::"LastLoc"::: ) (Set (Var "I")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" ($#k62_valued_1 :::"LastLoc"::: ) (Set (Var "J")) ")" ))))) ; theorem :: COMPOS_2:44 (Bool "for" (Set (Var "S")) "being" ($#v1_amistd_4 :::"with_non_trivial_Instructions"::: ) ($#l1_compos_1 :::"COM-Struct"::: ) (Bool "for" (Set (Var "J")) "," (Set (Var "I")) "being" ($#m1_hidden :::"MacroInstruction":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "j")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k62_valued_1 :::"LastLoc"::: ) (Set (Var "J"))))) "holds" (Bool (Set (Set "(" (Set (Var "I")) ($#k8_compos_1 :::"';'"::: ) (Set (Var "J")) ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set "(" ($#k62_valued_1 :::"LastLoc"::: ) (Set (Var "I")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "j")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k5_compos_0 :::"IncAddr"::: ) "(" (Set "(" (Set (Var "J")) ($#k7_partfun1 :::"/."::: ) (Set (Var "j")) ")" ) "," (Set "(" ($#k62_valued_1 :::"LastLoc"::: ) (Set (Var "I")) ")" ) ")" ))))) ; theorem :: COMPOS_2:45 (Bool "for" (Set (Var "S")) "being" ($#v1_amistd_4 :::"with_non_trivial_Instructions"::: ) ($#l1_compos_1 :::"COM-Struct"::: ) (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#v6_compos_0 :::"No-StopCode"::: ) ($#m1_subset_1 :::"Instruction":::) "of" (Set (Var "S")) "holds" (Bool (Set (Set "(" (Set (Var "i")) ($#k3_compos_2 :::"';'"::: ) (Set (Var "j")) ")" ) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set ($#k5_compos_0 :::"IncAddr"::: ) "(" (Set (Var "j")) "," (Num 1) ")" )))) ; theorem :: COMPOS_2:46 (Bool "for" (Set (Var "S")) "being" ($#v1_amistd_4 :::"with_non_trivial_Instructions"::: ) ($#l1_compos_1 :::"COM-Struct"::: ) (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "k")) "being" ($#v6_compos_0 :::"No-StopCode"::: ) ($#m1_subset_1 :::"Instruction":::) "of" (Set (Var "S")) "holds" (Bool (Set (Set "(" (Set "(" (Set (Var "i")) ($#k3_compos_2 :::"';'"::: ) (Set (Var "j")) ")" ) ($#k2_compos_2 :::"';'"::: ) (Set (Var "k")) ")" ) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set ($#k5_compos_0 :::"IncAddr"::: ) "(" (Set (Var "j")) "," (Num 1) ")" )))) ; theorem :: COMPOS_2:47 (Bool "for" (Set (Var "S")) "being" ($#v1_amistd_4 :::"with_non_trivial_Instructions"::: ) ($#l1_compos_1 :::"COM-Struct"::: ) (Bool "for" (Set (Var "i1")) "," (Set (Var "i2")) "," (Set (Var "i3")) "," (Set (Var "i4")) "being" ($#v6_compos_0 :::"No-StopCode"::: ) ($#m1_subset_1 :::"Instruction":::) "of" (Set (Var "S")) "holds" (Bool (Set (Set "(" (Set "(" (Set "(" (Set (Var "i1")) ($#k3_compos_2 :::"';'"::: ) (Set (Var "i2")) ")" ) ($#k2_compos_2 :::"';'"::: ) (Set (Var "i3")) ")" ) ($#k2_compos_2 :::"';'"::: ) (Set (Var "i4")) ")" ) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set ($#k5_compos_0 :::"IncAddr"::: ) "(" (Set (Var "i2")) "," (Num 1) ")" )))) ; theorem :: COMPOS_2:48 (Bool "for" (Set (Var "S")) "being" ($#v1_amistd_4 :::"with_non_trivial_Instructions"::: ) ($#l1_compos_1 :::"COM-Struct"::: ) (Bool "for" (Set (Var "i1")) "," (Set (Var "i2")) "," (Set (Var "i3")) "," (Set (Var "i4")) "," (Set (Var "i5")) "being" ($#v6_compos_0 :::"No-StopCode"::: ) ($#m1_subset_1 :::"Instruction":::) "of" (Set (Var "S")) "holds" (Bool (Set (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "i1")) ($#k3_compos_2 :::"';'"::: ) (Set (Var "i2")) ")" ) ($#k2_compos_2 :::"';'"::: ) (Set (Var "i3")) ")" ) ($#k2_compos_2 :::"';'"::: ) (Set (Var "i4")) ")" ) ($#k2_compos_2 :::"';'"::: ) (Set (Var "i5")) ")" ) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set ($#k5_compos_0 :::"IncAddr"::: ) "(" (Set (Var "i2")) "," (Num 1) ")" )))) ; theorem :: COMPOS_2:49 (Bool "for" (Set (Var "S")) "being" ($#v1_amistd_4 :::"with_non_trivial_Instructions"::: ) ($#l1_compos_1 :::"COM-Struct"::: ) (Bool "for" (Set (Var "i1")) "," (Set (Var "i2")) "," (Set (Var "i3")) "," (Set (Var "i4")) "," (Set (Var "i5")) "," (Set (Var "i6")) "being" ($#v6_compos_0 :::"No-StopCode"::: ) ($#m1_subset_1 :::"Instruction":::) "of" (Set (Var "S")) "holds" (Bool (Set (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "i1")) ($#k3_compos_2 :::"';'"::: ) (Set (Var "i2")) ")" ) ($#k2_compos_2 :::"';'"::: ) (Set (Var "i3")) ")" ) ($#k2_compos_2 :::"';'"::: ) (Set (Var "i4")) ")" ) ($#k2_compos_2 :::"';'"::: ) (Set (Var "i5")) ")" ) ($#k2_compos_2 :::"';'"::: ) (Set (Var "i6")) ")" ) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set ($#k5_compos_0 :::"IncAddr"::: ) "(" (Set (Var "i2")) "," (Num 1) ")" )))) ; theorem :: COMPOS_2:50 (Bool "for" (Set (Var "S")) "being" ($#v1_amistd_4 :::"with_non_trivial_Instructions"::: ) ($#l1_compos_1 :::"COM-Struct"::: ) (Bool "for" (Set (Var "j")) "being" ($#v6_compos_0 :::"No-StopCode"::: ) ($#m1_subset_1 :::"Instruction":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"MacroInstruction":::) "of" (Set (Var "S")) "holds" (Bool (Set (Set "(" (Set (Var "I")) ($#k2_compos_2 :::"';'"::: ) (Set (Var "j")) ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k62_valued_1 :::"LastLoc"::: ) (Set (Var "I")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k5_compos_0 :::"IncAddr"::: ) "(" (Set (Var "j")) "," (Set "(" ($#k62_valued_1 :::"LastLoc"::: ) (Set (Var "I")) ")" ) ")" ))))) ; theorem :: COMPOS_2:51 (Bool "for" (Set (Var "S")) "being" ($#v1_amistd_4 :::"with_non_trivial_Instructions"::: ) ($#l1_compos_1 :::"COM-Struct"::: ) (Bool "for" (Set (Var "i1")) "," (Set (Var "i2")) "," (Set (Var "i3")) "being" ($#v6_compos_0 :::"No-StopCode"::: ) ($#m1_subset_1 :::"Instruction":::) "of" (Set (Var "S")) "holds" (Bool (Set (Set "(" (Set "(" (Set (Var "i1")) ($#k3_compos_2 :::"';'"::: ) (Set (Var "i2")) ")" ) ($#k2_compos_2 :::"';'"::: ) (Set (Var "i3")) ")" ) ($#k1_funct_1 :::"."::: ) (Num 2)) ($#r1_hidden :::"="::: ) (Set ($#k5_compos_0 :::"IncAddr"::: ) "(" (Set (Var "i3")) "," (Num 2) ")" )))) ; theorem :: COMPOS_2:52 (Bool "for" (Set (Var "S")) "being" ($#v1_amistd_4 :::"with_non_trivial_Instructions"::: ) ($#l1_compos_1 :::"COM-Struct"::: ) (Bool "for" (Set (Var "i1")) "," (Set (Var "i2")) "," (Set (Var "i3")) "," (Set (Var "i4")) "being" ($#v6_compos_0 :::"No-StopCode"::: ) ($#m1_subset_1 :::"Instruction":::) "of" (Set (Var "S")) "holds" (Bool (Set (Set "(" (Set "(" (Set "(" (Set (Var "i1")) ($#k3_compos_2 :::"';'"::: ) (Set (Var "i2")) ")" ) ($#k2_compos_2 :::"';'"::: ) (Set (Var "i3")) ")" ) ($#k2_compos_2 :::"';'"::: ) (Set (Var "i4")) ")" ) ($#k1_funct_1 :::"."::: ) (Num 2)) ($#r1_hidden :::"="::: ) (Set ($#k5_compos_0 :::"IncAddr"::: ) "(" (Set (Var "i3")) "," (Num 2) ")" )))) ; theorem :: COMPOS_2:53 (Bool "for" (Set (Var "S")) "being" ($#v1_amistd_4 :::"with_non_trivial_Instructions"::: ) ($#l1_compos_1 :::"COM-Struct"::: ) (Bool "for" (Set (Var "i1")) "," (Set (Var "i2")) "," (Set (Var "i3")) "," (Set (Var "i4")) "," (Set (Var "i5")) "being" ($#v6_compos_0 :::"No-StopCode"::: ) ($#m1_subset_1 :::"Instruction":::) "of" (Set (Var "S")) "holds" (Bool (Set (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "i1")) ($#k3_compos_2 :::"';'"::: ) (Set (Var "i2")) ")" ) ($#k2_compos_2 :::"';'"::: ) (Set (Var "i3")) ")" ) ($#k2_compos_2 :::"';'"::: ) (Set (Var "i4")) ")" ) ($#k2_compos_2 :::"';'"::: ) (Set (Var "i5")) ")" ) ($#k1_funct_1 :::"."::: ) (Num 2)) ($#r1_hidden :::"="::: ) (Set ($#k5_compos_0 :::"IncAddr"::: ) "(" (Set (Var "i3")) "," (Num 2) ")" )))) ; theorem :: COMPOS_2:54 (Bool "for" (Set (Var "S")) "being" ($#v1_amistd_4 :::"with_non_trivial_Instructions"::: ) ($#l1_compos_1 :::"COM-Struct"::: ) (Bool "for" (Set (Var "i1")) "," (Set (Var "i2")) "," (Set (Var "i3")) "," (Set (Var "i4")) "," (Set (Var "i5")) "," (Set (Var "i6")) "being" ($#v6_compos_0 :::"No-StopCode"::: ) ($#m1_subset_1 :::"Instruction":::) "of" (Set (Var "S")) "holds" (Bool (Set (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "i1")) ($#k3_compos_2 :::"';'"::: ) (Set (Var "i2")) ")" ) ($#k2_compos_2 :::"';'"::: ) (Set (Var "i3")) ")" ) ($#k2_compos_2 :::"';'"::: ) (Set (Var "i4")) ")" ) ($#k2_compos_2 :::"';'"::: ) (Set (Var "i5")) ")" ) ($#k2_compos_2 :::"';'"::: ) (Set (Var "i6")) ")" ) ($#k1_funct_1 :::"."::: ) (Num 2)) ($#r1_hidden :::"="::: ) (Set ($#k5_compos_0 :::"IncAddr"::: ) "(" (Set (Var "i3")) "," (Num 2) ")" )))) ; theorem :: COMPOS_2:55 (Bool "for" (Set (Var "S")) "being" ($#v1_amistd_4 :::"with_non_trivial_Instructions"::: ) ($#l1_compos_1 :::"COM-Struct"::: ) (Bool "for" (Set (Var "i1")) "," (Set (Var "i2")) "," (Set (Var "i3")) "," (Set (Var "i4")) "being" ($#v6_compos_0 :::"No-StopCode"::: ) ($#m1_subset_1 :::"Instruction":::) "of" (Set (Var "S")) "holds" (Bool (Set (Set "(" (Set "(" (Set "(" (Set (Var "i1")) ($#k3_compos_2 :::"';'"::: ) (Set (Var "i2")) ")" ) ($#k2_compos_2 :::"';'"::: ) (Set (Var "i3")) ")" ) ($#k2_compos_2 :::"';'"::: ) (Set (Var "i4")) ")" ) ($#k1_funct_1 :::"."::: ) (Num 3)) ($#r1_hidden :::"="::: ) (Set ($#k5_compos_0 :::"IncAddr"::: ) "(" (Set (Var "i4")) "," (Num 3) ")" )))) ; theorem :: COMPOS_2:56 (Bool "for" (Set (Var "S")) "being" ($#v1_amistd_4 :::"with_non_trivial_Instructions"::: ) ($#l1_compos_1 :::"COM-Struct"::: ) (Bool "for" (Set (Var "i1")) "," (Set (Var "i2")) "," (Set (Var "i3")) "," (Set (Var "i4")) "," (Set (Var "i5")) "being" ($#v6_compos_0 :::"No-StopCode"::: ) ($#m1_subset_1 :::"Instruction":::) "of" (Set (Var "S")) "holds" (Bool (Set (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "i1")) ($#k3_compos_2 :::"';'"::: ) (Set (Var "i2")) ")" ) ($#k2_compos_2 :::"';'"::: ) (Set (Var "i3")) ")" ) ($#k2_compos_2 :::"';'"::: ) (Set (Var "i4")) ")" ) ($#k2_compos_2 :::"';'"::: ) (Set (Var "i5")) ")" ) ($#k1_funct_1 :::"."::: ) (Num 3)) ($#r1_hidden :::"="::: ) (Set ($#k5_compos_0 :::"IncAddr"::: ) "(" (Set (Var "i4")) "," (Num 3) ")" )))) ; theorem :: COMPOS_2:57 (Bool "for" (Set (Var "S")) "being" ($#v1_amistd_4 :::"with_non_trivial_Instructions"::: ) ($#l1_compos_1 :::"COM-Struct"::: ) (Bool "for" (Set (Var "i1")) "," (Set (Var "i2")) "," (Set (Var "i3")) "," (Set (Var "i4")) "," (Set (Var "i5")) "," (Set (Var "i6")) "being" ($#v6_compos_0 :::"No-StopCode"::: ) ($#m1_subset_1 :::"Instruction":::) "of" (Set (Var "S")) "holds" (Bool (Set (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "i1")) ($#k3_compos_2 :::"';'"::: ) (Set (Var "i2")) ")" ) ($#k2_compos_2 :::"';'"::: ) (Set (Var "i3")) ")" ) ($#k2_compos_2 :::"';'"::: ) (Set (Var "i4")) ")" ) ($#k2_compos_2 :::"';'"::: ) (Set (Var "i5")) ")" ) ($#k2_compos_2 :::"';'"::: ) (Set (Var "i6")) ")" ) ($#k1_funct_1 :::"."::: ) (Num 3)) ($#r1_hidden :::"="::: ) (Set ($#k5_compos_0 :::"IncAddr"::: ) "(" (Set (Var "i4")) "," (Num 3) ")" )))) ; theorem :: COMPOS_2:58 (Bool "for" (Set (Var "S")) "being" ($#v1_amistd_4 :::"with_non_trivial_Instructions"::: ) ($#l1_compos_1 :::"COM-Struct"::: ) (Bool "for" (Set (Var "i1")) "," (Set (Var "i2")) "," (Set (Var "i3")) "," (Set (Var "i4")) "," (Set (Var "i5")) "being" ($#v6_compos_0 :::"No-StopCode"::: ) ($#m1_subset_1 :::"Instruction":::) "of" (Set (Var "S")) "holds" (Bool (Set (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "i1")) ($#k3_compos_2 :::"';'"::: ) (Set (Var "i2")) ")" ) ($#k2_compos_2 :::"';'"::: ) (Set (Var "i3")) ")" ) ($#k2_compos_2 :::"';'"::: ) (Set (Var "i4")) ")" ) ($#k2_compos_2 :::"';'"::: ) (Set (Var "i5")) ")" ) ($#k1_funct_1 :::"."::: ) (Num 4)) ($#r1_hidden :::"="::: ) (Set ($#k5_compos_0 :::"IncAddr"::: ) "(" (Set (Var "i5")) "," (Num 4) ")" )))) ; theorem :: COMPOS_2:59 (Bool "for" (Set (Var "S")) "being" ($#v1_amistd_4 :::"with_non_trivial_Instructions"::: ) ($#l1_compos_1 :::"COM-Struct"::: ) (Bool "for" (Set (Var "i1")) "," (Set (Var "i2")) "," (Set (Var "i3")) "," (Set (Var "i4")) "," (Set (Var "i5")) "," (Set (Var "i6")) "being" ($#v6_compos_0 :::"No-StopCode"::: ) ($#m1_subset_1 :::"Instruction":::) "of" (Set (Var "S")) "holds" (Bool (Set (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "i1")) ($#k3_compos_2 :::"';'"::: ) (Set (Var "i2")) ")" ) ($#k2_compos_2 :::"';'"::: ) (Set (Var "i3")) ")" ) ($#k2_compos_2 :::"';'"::: ) (Set (Var "i4")) ")" ) ($#k2_compos_2 :::"';'"::: ) (Set (Var "i5")) ")" ) ($#k2_compos_2 :::"';'"::: ) (Set (Var "i6")) ")" ) ($#k1_funct_1 :::"."::: ) (Num 4)) ($#r1_hidden :::"="::: ) (Set ($#k5_compos_0 :::"IncAddr"::: ) "(" (Set (Var "i5")) "," (Num 4) ")" )))) ; theorem :: COMPOS_2:60 (Bool "for" (Set (Var "S")) "being" ($#v1_amistd_4 :::"with_non_trivial_Instructions"::: ) ($#l1_compos_1 :::"COM-Struct"::: ) (Bool "for" (Set (Var "i1")) "," (Set (Var "i2")) "," (Set (Var "i3")) "," (Set (Var "i4")) "," (Set (Var "i5")) "," (Set (Var "i6")) "being" ($#v6_compos_0 :::"No-StopCode"::: ) ($#m1_subset_1 :::"Instruction":::) "of" (Set (Var "S")) "holds" (Bool (Set (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "i1")) ($#k3_compos_2 :::"';'"::: ) (Set (Var "i2")) ")" ) ($#k2_compos_2 :::"';'"::: ) (Set (Var "i3")) ")" ) ($#k2_compos_2 :::"';'"::: ) (Set (Var "i4")) ")" ) ($#k2_compos_2 :::"';'"::: ) (Set (Var "i5")) ")" ) ($#k2_compos_2 :::"';'"::: ) (Set (Var "i6")) ")" ) ($#k1_funct_1 :::"."::: ) (Num 5)) ($#r1_hidden :::"="::: ) (Set ($#k5_compos_0 :::"IncAddr"::: ) "(" (Set (Var "i6")) "," (Num 5) ")" )))) ; definitionlet "S" be ($#v1_amistd_4 :::"with_non_trivial_Instructions"::: ) ($#l1_compos_1 :::"COM-Struct"::: ) ; let "I" be ($#m1_hidden :::"preProgram":::) "of" (Set (Const "S")); attr "I" is :::"closed"::: means :: COMPOS_2:def 5 (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Instruction":::) "of" "S" "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) "I"))) "holds" (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" ($#k5_xtuple_0 :::"JumpPart"::: ) (Set (Var "i")) ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) "I"))); end; :: deftheorem defines :::"closed"::: COMPOS_2:def 5 : (Bool "for" (Set (Var "S")) "being" ($#v1_amistd_4 :::"with_non_trivial_Instructions"::: ) ($#l1_compos_1 :::"COM-Struct"::: ) (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"preProgram":::) "of" (Set (Var "S")) "holds" (Bool "(" (Bool (Set (Var "I")) "is" ($#v1_compos_2 :::"closed"::: ) ) "iff" (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Instruction":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "I"))))) "holds" (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" ($#k5_xtuple_0 :::"JumpPart"::: ) (Set (Var "i")) ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "I"))))) ")" ))); registrationlet "S" be ($#v1_amistd_4 :::"with_non_trivial_Instructions"::: ) ($#l1_compos_1 :::"COM-Struct"::: ) ; cluster (Set ($#k4_compos_1 :::"Stop"::: ) "S") -> ($#v1_compos_2 :::"closed"::: ) ; end; registrationlet "S" be ($#v1_amistd_4 :::"with_non_trivial_Instructions"::: ) ($#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"::: ) bbbadV1_AFINSQ_1() ($#v3_compos_1 :::"halt-ending"::: ) ($#v4_compos_1 :::"unique-halt"::: ) ($#v1_compos_2 :::"closed"::: ) for ($#m1_hidden :::"set"::: ) ; end; theorem :: COMPOS_2:61 (Bool "for" (Set (Var "S")) "being" ($#v1_amistd_4 :::"with_non_trivial_Instructions"::: ) ($#l1_compos_1 :::"COM-Struct"::: ) (Bool "for" (Set (Var "i")) "being" ($#v6_compos_0 :::"No-StopCode"::: ) ($#m1_subset_1 :::"Instruction":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "i")) "is" ($#v4_compos_0 :::"ins-loc-free"::: ) )) "holds" (Bool (Set ($#k11_compos_1 :::"Macro"::: ) (Set (Var "i"))) "is" ($#v1_compos_2 :::"closed"::: ) ))) ; registrationlet "S" be ($#v1_amistd_4 :::"with_non_trivial_Instructions"::: ) ($#l1_compos_1 :::"COM-Struct"::: ) ; let "I" be ($#v1_compos_2 :::"closed"::: ) ($#m1_hidden :::"MacroInstruction":::) "of" (Set (Const "S")); let "k" be ($#m1_hidden :::"Nat":::); cluster (Set ($#k6_compos_1 :::"Reloc"::: ) "(" "I" "," "k" ")" ) -> ($#v1_compos_2 :::"closed"::: ) ; end; registrationlet "S" be ($#v1_amistd_4 :::"with_non_trivial_Instructions"::: ) ($#l1_compos_1 :::"COM-Struct"::: ) ; let "I", "J" be ($#v1_compos_2 :::"closed"::: ) ($#m1_hidden :::"MacroInstruction":::) "of" (Set (Const "S")); cluster (Set "I" ($#k7_compos_1 :::"';'"::: ) "J") -> ($#v1_compos_2 :::"closed"::: ) ; end;