:: SCMPDS_2 semantic presentation begin definitionfunc :::"SCMPDS"::: -> ($#v1_extpro_1 :::"strict"::: ) ($#l1_extpro_1 :::"AMI-Struct"::: ) "over" (Num 2) equals :: SCMPDS_2:def 1 (Set ($#g1_extpro_1 :::"AMI-Struct"::: ) "(#" (Set ($#k1_ami_2 :::"SCM-Memory"::: ) ) "," (Set "(" ($#k1_funct_7 :::"In"::: ) "(" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set ($#k1_ami_2 :::"SCM-Memory"::: ) ) ")" ")" ) "," (Set ($#k1_scmpds_i :::"SCMPDS-Instr"::: ) ) "," (Set ($#k3_ami_2 :::"SCM-OK"::: ) ) "," (Set ($#k4_ami_2 :::"SCM-VAL"::: ) ) "," (Set ($#k6_scmpds_1 :::"SCMPDS-Exec"::: ) ) "#)" ); end; :: deftheorem defines :::"SCMPDS"::: SCMPDS_2:def 1 : (Bool (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#g1_extpro_1 :::"AMI-Struct"::: ) "(#" (Set ($#k1_ami_2 :::"SCM-Memory"::: ) ) "," (Set "(" ($#k1_funct_7 :::"In"::: ) "(" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set ($#k1_ami_2 :::"SCM-Memory"::: ) ) ")" ")" ) "," (Set ($#k1_scmpds_i :::"SCMPDS-Instr"::: ) ) "," (Set ($#k3_ami_2 :::"SCM-OK"::: ) ) "," (Set ($#k4_ami_2 :::"SCM-VAL"::: ) ) "," (Set ($#k6_scmpds_1 :::"SCMPDS-Exec"::: ) ) "#)" )); registration cluster (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_extpro_1 :::"strict"::: ) ; end; registration cluster (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) -> ($#v2_memstr_0 :::"with_non-empty_values"::: ) ($#v3_memstr_0 :::"IC-Ins-separated"::: ) ($#v1_extpro_1 :::"strict"::: ) ; end; theorem :: SCMPDS_2:1 canceled; theorem :: SCMPDS_2:2 (Bool (Set ($#k4_struct_0 :::"IC"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k5_numbers :::"NAT"::: ) )) ; begin registration cluster ($#v1_ami_2 :::"Int-like"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) )); end; definitionmode Int_position is ($#v1_ami_2 :::"Int-like"::: ) ($#m1_subset_1 :::"Object":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ); canceled; end; :: deftheorem SCMPDS_2:def 2 : canceled; theorem :: SCMPDS_2:3 canceled; theorem :: SCMPDS_2:4 canceled; theorem :: SCMPDS_2:5 (Bool "for" (Set (Var "l")) "being" ($#m1_subset_1 :::"Int_position":::) "holds" (Bool (Set ($#k4_memstr_0 :::"Values"::: ) (Set (Var "l"))) ($#r1_hidden :::"="::: ) (Set ($#k4_numbers :::"INT"::: ) ))) ; begin theorem :: SCMPDS_2:6 (Bool "for" (Set (Var "I")) "being" ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "holds" (Bool (Set ($#k2_compos_0 :::"InsCode"::: ) (Set (Var "I"))) ($#r1_xxreal_0 :::"<="::: ) (Num 14))) ; registrationlet "s" be ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ); let "d" be ($#m1_subset_1 :::"Int_position":::); cluster (Set "s" ($#k1_funct_1 :::"."::: ) "d") -> ($#v1_int_1 :::"integer"::: ) ; end; definitionlet "m", "n" be ($#m1_hidden :::"Integer":::); func :::"DataLoc"::: "(" "m" "," "n" ")" -> ($#m1_subset_1 :::"Int_position":::) equals :: SCMPDS_2:def 3 (Set ($#k4_tarski :::"["::: ) (Num 1) "," (Set "(" ($#k1_int_2 :::"abs"::: ) (Set "(" "m" ($#k2_xcmplx_0 :::"+"::: ) "n" ")" ) ")" ) ($#k4_tarski :::"]"::: ) ); end; :: deftheorem defines :::"DataLoc"::: SCMPDS_2:def 3 : (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#m1_hidden :::"Integer":::) "holds" (Bool (Set ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set (Var "m")) "," (Set (Var "n")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Num 1) "," (Set "(" ($#k1_int_2 :::"abs"::: ) (Set "(" (Set (Var "m")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "n")) ")" ) ")" ) ($#k4_tarski :::"]"::: ) ))); theorem :: SCMPDS_2:7 (Bool "for" (Set (Var "k1")) "being" ($#m1_hidden :::"Integer":::) "holds" (Bool (Set ($#k3_xtuple_0 :::"["::: ) (Num 14) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "k1")) ($#k9_finseq_1 :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k1_scmpds_i :::"SCMPDS-Instr"::: ) ))) ; theorem :: SCMPDS_2:8 (Bool "for" (Set (Var "d1")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k2_ami_2 :::"SCM-Data-Loc"::: ) ) "holds" (Bool (Set ($#k3_xtuple_0 :::"["::: ) (Num 1) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "d1")) ($#k12_finseq_1 :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k1_scmpds_i :::"SCMPDS-Instr"::: ) ))) ; theorem :: SCMPDS_2:9 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "d2")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k2_ami_2 :::"SCM-Data-Loc"::: ) ) (Bool "for" (Set (Var "k2")) "being" ($#m1_hidden :::"Integer":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_tarski :::"{"::: ) (Num 2) "," (Num 3) ($#k2_tarski :::"}"::: ) ))) "holds" (Bool (Set ($#k3_xtuple_0 :::"["::: ) (Set (Var "x")) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k3_scmpds_1 :::"<*"::: ) (Set (Var "d2")) "," (Set (Var "k2")) ($#k3_scmpds_1 :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k1_scmpds_i :::"SCMPDS-Instr"::: ) ))))) ; theorem :: SCMPDS_2:10 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "d2")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k2_ami_2 :::"SCM-Data-Loc"::: ) ) (Bool "for" (Set (Var "k3")) "," (Set (Var "k4")) "being" ($#m1_hidden :::"Integer":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k3_enumset1 :::"{"::: ) (Num 4) "," (Num 5) "," (Num 6) "," (Num 7) "," (Num 8) ($#k3_enumset1 :::"}"::: ) ))) "holds" (Bool (Set ($#k3_xtuple_0 :::"["::: ) (Set (Var "x")) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "d2")) "," (Set (Var "k3")) "," (Set (Var "k4")) ($#k11_finseq_1 :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k1_scmpds_i :::"SCMPDS-Instr"::: ) ))))) ; theorem :: SCMPDS_2:11 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "d4")) "," (Set (Var "d5")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k2_ami_2 :::"SCM-Data-Loc"::: ) ) (Bool "for" (Set (Var "k5")) "," (Set (Var "k6")) "being" ($#m1_hidden :::"Integer":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k3_enumset1 :::"{"::: ) (Num 9) "," (Num 10) "," (Num 11) "," (Num 12) "," (Num 13) ($#k3_enumset1 :::"}"::: ) ))) "holds" (Bool (Set ($#k3_xtuple_0 :::"["::: ) (Set (Var "x")) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k7_finseq_4 :::"<*"::: ) (Set (Var "d4")) "," (Set (Var "d5")) "," (Set (Var "k5")) "," (Set (Var "k6")) ($#k7_finseq_4 :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k1_scmpds_i :::"SCMPDS-Instr"::: ) ))))) ; definitionlet "k1" be ($#m1_hidden :::"Integer":::); func :::"goto"::: "k1" -> ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) equals :: SCMPDS_2:def 4 (Set ($#k3_xtuple_0 :::"["::: ) (Num 14) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k9_finseq_1 :::"<*"::: ) "k1" ($#k9_finseq_1 :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) ); end; :: deftheorem defines :::"goto"::: SCMPDS_2:def 4 : (Bool "for" (Set (Var "k1")) "being" ($#m1_hidden :::"Integer":::) "holds" (Bool (Set ($#k3_scmpds_2 :::"goto"::: ) (Set (Var "k1"))) ($#r1_hidden :::"="::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Num 14) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "k1")) ($#k9_finseq_1 :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) ))); definitionlet "a" be ($#m1_subset_1 :::"Int_position":::); func :::"return"::: "a" -> ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) equals :: SCMPDS_2:def 5 (Set ($#k3_xtuple_0 :::"["::: ) (Num 1) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k9_finseq_1 :::"<*"::: ) "a" ($#k9_finseq_1 :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) ); end; :: deftheorem defines :::"return"::: SCMPDS_2:def 5 : (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int_position":::) "holds" (Bool (Set ($#k4_scmpds_2 :::"return"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Num 1) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "a")) ($#k9_finseq_1 :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) ))); definitionlet "a" be ($#m1_subset_1 :::"Int_position":::); let "k1" be ($#m1_hidden :::"Integer":::); func "a" :::":="::: "k1" -> ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) equals :: SCMPDS_2:def 6 (Set ($#k3_xtuple_0 :::"["::: ) (Num 2) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k10_finseq_1 :::"<*"::: ) "a" "," "k1" ($#k10_finseq_1 :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) ); func :::"saveIC"::: "(" "a" "," "k1" ")" -> ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) equals :: SCMPDS_2:def 7 (Set ($#k3_xtuple_0 :::"["::: ) (Num 3) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k10_finseq_1 :::"<*"::: ) "a" "," "k1" ($#k10_finseq_1 :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) ); end; :: deftheorem defines :::":="::: SCMPDS_2:def 6 : (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int_position":::) (Bool "for" (Set (Var "k1")) "being" ($#m1_hidden :::"Integer":::) "holds" (Bool (Set (Set (Var "a")) ($#k5_scmpds_2 :::":="::: ) (Set (Var "k1"))) ($#r1_hidden :::"="::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Num 2) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "a")) "," (Set (Var "k1")) ($#k10_finseq_1 :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) )))); :: deftheorem defines :::"saveIC"::: SCMPDS_2:def 7 : (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int_position":::) (Bool "for" (Set (Var "k1")) "being" ($#m1_hidden :::"Integer":::) "holds" (Bool (Set ($#k6_scmpds_2 :::"saveIC"::: ) "(" (Set (Var "a")) "," (Set (Var "k1")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Num 3) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "a")) "," (Set (Var "k1")) ($#k10_finseq_1 :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) )))); definitionlet "a" be ($#m1_subset_1 :::"Int_position":::); let "k1", "k2" be ($#m1_hidden :::"Integer":::); func "(" "a" "," "k1" ")" :::"<>0_goto"::: "k2" -> ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) equals :: SCMPDS_2:def 8 (Set ($#k3_xtuple_0 :::"["::: ) (Num 4) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k11_finseq_1 :::"<*"::: ) "a" "," "k1" "," "k2" ($#k11_finseq_1 :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) ); func "(" "a" "," "k1" ")" :::"<=0_goto"::: "k2" -> ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) equals :: SCMPDS_2:def 9 (Set ($#k3_xtuple_0 :::"["::: ) (Num 5) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k11_finseq_1 :::"<*"::: ) "a" "," "k1" "," "k2" ($#k11_finseq_1 :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) ); func "(" "a" "," "k1" ")" :::">=0_goto"::: "k2" -> ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) equals :: SCMPDS_2:def 10 (Set ($#k3_xtuple_0 :::"["::: ) (Num 6) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k11_finseq_1 :::"<*"::: ) "a" "," "k1" "," "k2" ($#k11_finseq_1 :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) ); func "(" "a" "," "k1" ")" :::":="::: "k2" -> ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) equals :: SCMPDS_2:def 11 (Set ($#k3_xtuple_0 :::"["::: ) (Num 7) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k11_finseq_1 :::"<*"::: ) "a" "," "k1" "," "k2" ($#k11_finseq_1 :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) ); func :::"AddTo"::: "(" "a" "," "k1" "," "k2" ")" -> ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) equals :: SCMPDS_2:def 12 (Set ($#k3_xtuple_0 :::"["::: ) (Num 8) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k11_finseq_1 :::"<*"::: ) "a" "," "k1" "," "k2" ($#k11_finseq_1 :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) ); end; :: deftheorem defines :::"<>0_goto"::: SCMPDS_2:def 8 : (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int_position":::) (Bool "for" (Set (Var "k1")) "," (Set (Var "k2")) "being" ($#m1_hidden :::"Integer":::) "holds" (Bool (Set "(" (Set (Var "a")) "," (Set (Var "k1")) ")" ($#k7_scmpds_2 :::"<>0_goto"::: ) (Set (Var "k2"))) ($#r1_hidden :::"="::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Num 4) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "a")) "," (Set (Var "k1")) "," (Set (Var "k2")) ($#k11_finseq_1 :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) )))); :: deftheorem defines :::"<=0_goto"::: SCMPDS_2:def 9 : (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int_position":::) (Bool "for" (Set (Var "k1")) "," (Set (Var "k2")) "being" ($#m1_hidden :::"Integer":::) "holds" (Bool (Set "(" (Set (Var "a")) "," (Set (Var "k1")) ")" ($#k8_scmpds_2 :::"<=0_goto"::: ) (Set (Var "k2"))) ($#r1_hidden :::"="::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Num 5) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "a")) "," (Set (Var "k1")) "," (Set (Var "k2")) ($#k11_finseq_1 :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) )))); :: deftheorem defines :::">=0_goto"::: SCMPDS_2:def 10 : (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int_position":::) (Bool "for" (Set (Var "k1")) "," (Set (Var "k2")) "being" ($#m1_hidden :::"Integer":::) "holds" (Bool (Set "(" (Set (Var "a")) "," (Set (Var "k1")) ")" ($#k9_scmpds_2 :::">=0_goto"::: ) (Set (Var "k2"))) ($#r1_hidden :::"="::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Num 6) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "a")) "," (Set (Var "k1")) "," (Set (Var "k2")) ($#k11_finseq_1 :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) )))); :: deftheorem defines :::":="::: SCMPDS_2:def 11 : (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int_position":::) (Bool "for" (Set (Var "k1")) "," (Set (Var "k2")) "being" ($#m1_hidden :::"Integer":::) "holds" (Bool (Set "(" (Set (Var "a")) "," (Set (Var "k1")) ")" ($#k10_scmpds_2 :::":="::: ) (Set (Var "k2"))) ($#r1_hidden :::"="::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Num 7) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "a")) "," (Set (Var "k1")) "," (Set (Var "k2")) ($#k11_finseq_1 :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) )))); :: deftheorem defines :::"AddTo"::: SCMPDS_2:def 12 : (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int_position":::) (Bool "for" (Set (Var "k1")) "," (Set (Var "k2")) "being" ($#m1_hidden :::"Integer":::) "holds" (Bool (Set ($#k11_scmpds_2 :::"AddTo"::: ) "(" (Set (Var "a")) "," (Set (Var "k1")) "," (Set (Var "k2")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Num 8) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "a")) "," (Set (Var "k1")) "," (Set (Var "k2")) ($#k11_finseq_1 :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) )))); definitionlet "a", "b" be ($#m1_subset_1 :::"Int_position":::); let "k1", "k2" be ($#m1_hidden :::"Integer":::); func :::"AddTo"::: "(" "a" "," "k1" "," "b" "," "k2" ")" -> ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) equals :: SCMPDS_2:def 13 (Set ($#k3_xtuple_0 :::"["::: ) (Num 9) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k7_finseq_4 :::"<*"::: ) "a" "," "b" "," "k1" "," "k2" ($#k7_finseq_4 :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) ); func :::"SubFrom"::: "(" "a" "," "k1" "," "b" "," "k2" ")" -> ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) equals :: SCMPDS_2:def 14 (Set ($#k3_xtuple_0 :::"["::: ) (Num 10) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k7_finseq_4 :::"<*"::: ) "a" "," "b" "," "k1" "," "k2" ($#k7_finseq_4 :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) ); func :::"MultBy"::: "(" "a" "," "k1" "," "b" "," "k2" ")" -> ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) equals :: SCMPDS_2:def 15 (Set ($#k3_xtuple_0 :::"["::: ) (Num 11) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k7_finseq_4 :::"<*"::: ) "a" "," "b" "," "k1" "," "k2" ($#k7_finseq_4 :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) ); func :::"Divide"::: "(" "a" "," "k1" "," "b" "," "k2" ")" -> ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) equals :: SCMPDS_2:def 16 (Set ($#k3_xtuple_0 :::"["::: ) (Num 12) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k7_finseq_4 :::"<*"::: ) "a" "," "b" "," "k1" "," "k2" ($#k7_finseq_4 :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) ); func "(" "a" "," "k1" ")" :::":="::: "(" "b" "," "k2" ")" -> ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) equals :: SCMPDS_2:def 17 (Set ($#k3_xtuple_0 :::"["::: ) (Num 13) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k7_finseq_4 :::"<*"::: ) "a" "," "b" "," "k1" "," "k2" ($#k7_finseq_4 :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) ); end; :: deftheorem defines :::"AddTo"::: SCMPDS_2:def 13 : (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Int_position":::) (Bool "for" (Set (Var "k1")) "," (Set (Var "k2")) "being" ($#m1_hidden :::"Integer":::) "holds" (Bool (Set ($#k12_scmpds_2 :::"AddTo"::: ) "(" (Set (Var "a")) "," (Set (Var "k1")) "," (Set (Var "b")) "," (Set (Var "k2")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Num 9) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k7_finseq_4 :::"<*"::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "k1")) "," (Set (Var "k2")) ($#k7_finseq_4 :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) )))); :: deftheorem defines :::"SubFrom"::: SCMPDS_2:def 14 : (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Int_position":::) (Bool "for" (Set (Var "k1")) "," (Set (Var "k2")) "being" ($#m1_hidden :::"Integer":::) "holds" (Bool (Set ($#k13_scmpds_2 :::"SubFrom"::: ) "(" (Set (Var "a")) "," (Set (Var "k1")) "," (Set (Var "b")) "," (Set (Var "k2")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Num 10) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k7_finseq_4 :::"<*"::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "k1")) "," (Set (Var "k2")) ($#k7_finseq_4 :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) )))); :: deftheorem defines :::"MultBy"::: SCMPDS_2:def 15 : (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Int_position":::) (Bool "for" (Set (Var "k1")) "," (Set (Var "k2")) "being" ($#m1_hidden :::"Integer":::) "holds" (Bool (Set ($#k14_scmpds_2 :::"MultBy"::: ) "(" (Set (Var "a")) "," (Set (Var "k1")) "," (Set (Var "b")) "," (Set (Var "k2")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Num 11) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k7_finseq_4 :::"<*"::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "k1")) "," (Set (Var "k2")) ($#k7_finseq_4 :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) )))); :: deftheorem defines :::"Divide"::: SCMPDS_2:def 16 : (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Int_position":::) (Bool "for" (Set (Var "k1")) "," (Set (Var "k2")) "being" ($#m1_hidden :::"Integer":::) "holds" (Bool (Set ($#k15_scmpds_2 :::"Divide"::: ) "(" (Set (Var "a")) "," (Set (Var "k1")) "," (Set (Var "b")) "," (Set (Var "k2")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Num 12) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k7_finseq_4 :::"<*"::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "k1")) "," (Set (Var "k2")) ($#k7_finseq_4 :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) )))); :: deftheorem defines :::":="::: SCMPDS_2:def 17 : (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Int_position":::) (Bool "for" (Set (Var "k1")) "," (Set (Var "k2")) "being" ($#m1_hidden :::"Integer":::) "holds" (Bool (Set "(" (Set (Var "a")) "," (Set (Var "k1")) ")" ($#k16_scmpds_2 :::":="::: ) "(" (Set (Var "b")) "," (Set (Var "k2")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Num 13) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k7_finseq_4 :::"<*"::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "k1")) "," (Set (Var "k2")) ($#k7_finseq_4 :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) )))); theorem :: SCMPDS_2:12 (Bool "for" (Set (Var "k1")) "being" ($#m1_hidden :::"Integer":::) "holds" (Bool (Set ($#k2_compos_0 :::"InsCode"::: ) (Set "(" ($#k3_scmpds_2 :::"goto"::: ) (Set (Var "k1")) ")" )) ($#r1_hidden :::"="::: ) (Num 14))) ; theorem :: SCMPDS_2:13 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int_position":::) "holds" (Bool (Set ($#k2_compos_0 :::"InsCode"::: ) (Set "(" ($#k4_scmpds_2 :::"return"::: ) (Set (Var "a")) ")" )) ($#r1_hidden :::"="::: ) (Num 1))) ; theorem :: SCMPDS_2:14 (Bool "for" (Set (Var "k1")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int_position":::) "holds" (Bool (Set ($#k2_compos_0 :::"InsCode"::: ) (Set "(" (Set (Var "a")) ($#k5_scmpds_2 :::":="::: ) (Set (Var "k1")) ")" )) ($#r1_hidden :::"="::: ) (Num 2)))) ; theorem :: SCMPDS_2:15 (Bool "for" (Set (Var "k1")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int_position":::) "holds" (Bool (Set ($#k2_compos_0 :::"InsCode"::: ) (Set "(" ($#k6_scmpds_2 :::"saveIC"::: ) "(" (Set (Var "a")) "," (Set (Var "k1")) ")" ")" )) ($#r1_hidden :::"="::: ) (Num 3)))) ; theorem :: SCMPDS_2:16 (Bool "for" (Set (Var "k1")) "," (Set (Var "k2")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int_position":::) "holds" (Bool (Set ($#k2_compos_0 :::"InsCode"::: ) (Set "(" "(" (Set (Var "a")) "," (Set (Var "k1")) ")" ($#k7_scmpds_2 :::"<>0_goto"::: ) (Set (Var "k2")) ")" )) ($#r1_hidden :::"="::: ) (Num 4)))) ; theorem :: SCMPDS_2:17 (Bool "for" (Set (Var "k1")) "," (Set (Var "k2")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int_position":::) "holds" (Bool (Set ($#k2_compos_0 :::"InsCode"::: ) (Set "(" "(" (Set (Var "a")) "," (Set (Var "k1")) ")" ($#k8_scmpds_2 :::"<=0_goto"::: ) (Set (Var "k2")) ")" )) ($#r1_hidden :::"="::: ) (Num 5)))) ; theorem :: SCMPDS_2:18 (Bool "for" (Set (Var "k1")) "," (Set (Var "k2")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int_position":::) "holds" (Bool (Set ($#k2_compos_0 :::"InsCode"::: ) (Set "(" "(" (Set (Var "a")) "," (Set (Var "k1")) ")" ($#k9_scmpds_2 :::">=0_goto"::: ) (Set (Var "k2")) ")" )) ($#r1_hidden :::"="::: ) (Num 6)))) ; theorem :: SCMPDS_2:19 (Bool "for" (Set (Var "k1")) "," (Set (Var "k2")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int_position":::) "holds" (Bool (Set ($#k2_compos_0 :::"InsCode"::: ) (Set "(" "(" (Set (Var "a")) "," (Set (Var "k1")) ")" ($#k10_scmpds_2 :::":="::: ) (Set (Var "k2")) ")" )) ($#r1_hidden :::"="::: ) (Num 7)))) ; theorem :: SCMPDS_2:20 (Bool "for" (Set (Var "k1")) "," (Set (Var "k2")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int_position":::) "holds" (Bool (Set ($#k2_compos_0 :::"InsCode"::: ) (Set "(" ($#k11_scmpds_2 :::"AddTo"::: ) "(" (Set (Var "a")) "," (Set (Var "k1")) "," (Set (Var "k2")) ")" ")" )) ($#r1_hidden :::"="::: ) (Num 8)))) ; theorem :: SCMPDS_2:21 (Bool "for" (Set (Var "k1")) "," (Set (Var "k2")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Int_position":::) "holds" (Bool (Set ($#k2_compos_0 :::"InsCode"::: ) (Set "(" ($#k12_scmpds_2 :::"AddTo"::: ) "(" (Set (Var "a")) "," (Set (Var "k1")) "," (Set (Var "b")) "," (Set (Var "k2")) ")" ")" )) ($#r1_hidden :::"="::: ) (Num 9)))) ; theorem :: SCMPDS_2:22 (Bool "for" (Set (Var "k1")) "," (Set (Var "k2")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Int_position":::) "holds" (Bool (Set ($#k2_compos_0 :::"InsCode"::: ) (Set "(" ($#k13_scmpds_2 :::"SubFrom"::: ) "(" (Set (Var "a")) "," (Set (Var "k1")) "," (Set (Var "b")) "," (Set (Var "k2")) ")" ")" )) ($#r1_hidden :::"="::: ) (Num 10)))) ; theorem :: SCMPDS_2:23 (Bool "for" (Set (Var "k1")) "," (Set (Var "k2")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Int_position":::) "holds" (Bool (Set ($#k2_compos_0 :::"InsCode"::: ) (Set "(" ($#k14_scmpds_2 :::"MultBy"::: ) "(" (Set (Var "a")) "," (Set (Var "k1")) "," (Set (Var "b")) "," (Set (Var "k2")) ")" ")" )) ($#r1_hidden :::"="::: ) (Num 11)))) ; theorem :: SCMPDS_2:24 (Bool "for" (Set (Var "k1")) "," (Set (Var "k2")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Int_position":::) "holds" (Bool (Set ($#k2_compos_0 :::"InsCode"::: ) (Set "(" ($#k15_scmpds_2 :::"Divide"::: ) "(" (Set (Var "a")) "," (Set (Var "k1")) "," (Set (Var "b")) "," (Set (Var "k2")) ")" ")" )) ($#r1_hidden :::"="::: ) (Num 12)))) ; theorem :: SCMPDS_2:25 (Bool "for" (Set (Var "k1")) "," (Set (Var "k2")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Int_position":::) "holds" (Bool (Set ($#k2_compos_0 :::"InsCode"::: ) (Set "(" "(" (Set (Var "a")) "," (Set (Var "k1")) ")" ($#k16_scmpds_2 :::":="::: ) "(" (Set (Var "b")) "," (Set (Var "k2")) ")" ")" )) ($#r1_hidden :::"="::: ) (Num 13)))) ; theorem :: SCMPDS_2:26 (Bool "for" (Set (Var "ins")) "being" ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "st" (Bool (Bool (Set ($#k2_compos_0 :::"InsCode"::: ) (Set (Var "ins"))) ($#r1_hidden :::"="::: ) (Num 14))) "holds" (Bool "ex" (Set (Var "k1")) "being" ($#m1_hidden :::"Integer":::) "st" (Bool (Set (Var "ins")) ($#r1_hidden :::"="::: ) (Set ($#k3_scmpds_2 :::"goto"::: ) (Set (Var "k1")))))) ; theorem :: SCMPDS_2:27 (Bool "for" (Set (Var "ins")) "being" ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "st" (Bool (Bool (Set ($#k2_compos_0 :::"InsCode"::: ) (Set (Var "ins"))) ($#r1_hidden :::"="::: ) (Num 1))) "holds" (Bool "ex" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int_position":::) "st" (Bool (Set (Var "ins")) ($#r1_hidden :::"="::: ) (Set ($#k4_scmpds_2 :::"return"::: ) (Set (Var "a")))))) ; theorem :: SCMPDS_2:28 (Bool "for" (Set (Var "ins")) "being" ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "st" (Bool (Bool (Set ($#k2_compos_0 :::"InsCode"::: ) (Set (Var "ins"))) ($#r1_hidden :::"="::: ) (Num 2))) "holds" (Bool "ex" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int_position":::)(Bool "ex" (Set (Var "k1")) "being" ($#m1_hidden :::"Integer":::) "st" (Bool (Set (Var "ins")) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k5_scmpds_2 :::":="::: ) (Set (Var "k1"))))))) ; theorem :: SCMPDS_2:29 (Bool "for" (Set (Var "ins")) "being" ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "st" (Bool (Bool (Set ($#k2_compos_0 :::"InsCode"::: ) (Set (Var "ins"))) ($#r1_hidden :::"="::: ) (Num 3))) "holds" (Bool "ex" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int_position":::)(Bool "ex" (Set (Var "k1")) "being" ($#m1_hidden :::"Integer":::) "st" (Bool (Set (Var "ins")) ($#r1_hidden :::"="::: ) (Set ($#k6_scmpds_2 :::"saveIC"::: ) "(" (Set (Var "a")) "," (Set (Var "k1")) ")" ))))) ; theorem :: SCMPDS_2:30 (Bool "for" (Set (Var "ins")) "being" ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "st" (Bool (Bool (Set ($#k2_compos_0 :::"InsCode"::: ) (Set (Var "ins"))) ($#r1_hidden :::"="::: ) (Num 4))) "holds" (Bool "ex" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int_position":::)(Bool "ex" (Set (Var "k1")) "," (Set (Var "k2")) "being" ($#m1_hidden :::"Integer":::) "st" (Bool (Set (Var "ins")) ($#r1_hidden :::"="::: ) (Set "(" (Set (Var "a")) "," (Set (Var "k1")) ")" ($#k7_scmpds_2 :::"<>0_goto"::: ) (Set (Var "k2"))))))) ; theorem :: SCMPDS_2:31 (Bool "for" (Set (Var "ins")) "being" ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "st" (Bool (Bool (Set ($#k2_compos_0 :::"InsCode"::: ) (Set (Var "ins"))) ($#r1_hidden :::"="::: ) (Num 5))) "holds" (Bool "ex" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int_position":::)(Bool "ex" (Set (Var "k1")) "," (Set (Var "k2")) "being" ($#m1_hidden :::"Integer":::) "st" (Bool (Set (Var "ins")) ($#r1_hidden :::"="::: ) (Set "(" (Set (Var "a")) "," (Set (Var "k1")) ")" ($#k8_scmpds_2 :::"<=0_goto"::: ) (Set (Var "k2"))))))) ; theorem :: SCMPDS_2:32 (Bool "for" (Set (Var "ins")) "being" ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "st" (Bool (Bool (Set ($#k2_compos_0 :::"InsCode"::: ) (Set (Var "ins"))) ($#r1_hidden :::"="::: ) (Num 6))) "holds" (Bool "ex" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int_position":::)(Bool "ex" (Set (Var "k1")) "," (Set (Var "k2")) "being" ($#m1_hidden :::"Integer":::) "st" (Bool (Set (Var "ins")) ($#r1_hidden :::"="::: ) (Set "(" (Set (Var "a")) "," (Set (Var "k1")) ")" ($#k9_scmpds_2 :::">=0_goto"::: ) (Set (Var "k2"))))))) ; theorem :: SCMPDS_2:33 (Bool "for" (Set (Var "ins")) "being" ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "st" (Bool (Bool (Set ($#k2_compos_0 :::"InsCode"::: ) (Set (Var "ins"))) ($#r1_hidden :::"="::: ) (Num 7))) "holds" (Bool "ex" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int_position":::)(Bool "ex" (Set (Var "k1")) "," (Set (Var "k2")) "being" ($#m1_hidden :::"Integer":::) "st" (Bool (Set (Var "ins")) ($#r1_hidden :::"="::: ) (Set "(" (Set (Var "a")) "," (Set (Var "k1")) ")" ($#k10_scmpds_2 :::":="::: ) (Set (Var "k2"))))))) ; theorem :: SCMPDS_2:34 (Bool "for" (Set (Var "ins")) "being" ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "st" (Bool (Bool (Set ($#k2_compos_0 :::"InsCode"::: ) (Set (Var "ins"))) ($#r1_hidden :::"="::: ) (Num 8))) "holds" (Bool "ex" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int_position":::)(Bool "ex" (Set (Var "k1")) "," (Set (Var "k2")) "being" ($#m1_hidden :::"Integer":::) "st" (Bool (Set (Var "ins")) ($#r1_hidden :::"="::: ) (Set ($#k11_scmpds_2 :::"AddTo"::: ) "(" (Set (Var "a")) "," (Set (Var "k1")) "," (Set (Var "k2")) ")" ))))) ; theorem :: SCMPDS_2:35 (Bool "for" (Set (Var "ins")) "being" ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "st" (Bool (Bool (Set ($#k2_compos_0 :::"InsCode"::: ) (Set (Var "ins"))) ($#r1_hidden :::"="::: ) (Num 9))) "holds" (Bool "ex" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Int_position":::)(Bool "ex" (Set (Var "k1")) "," (Set (Var "k2")) "being" ($#m1_hidden :::"Integer":::) "st" (Bool (Set (Var "ins")) ($#r1_hidden :::"="::: ) (Set ($#k12_scmpds_2 :::"AddTo"::: ) "(" (Set (Var "a")) "," (Set (Var "k1")) "," (Set (Var "b")) "," (Set (Var "k2")) ")" ))))) ; theorem :: SCMPDS_2:36 (Bool "for" (Set (Var "ins")) "being" ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "st" (Bool (Bool (Set ($#k2_compos_0 :::"InsCode"::: ) (Set (Var "ins"))) ($#r1_hidden :::"="::: ) (Num 10))) "holds" (Bool "ex" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Int_position":::)(Bool "ex" (Set (Var "k1")) "," (Set (Var "k2")) "being" ($#m1_hidden :::"Integer":::) "st" (Bool (Set (Var "ins")) ($#r1_hidden :::"="::: ) (Set ($#k13_scmpds_2 :::"SubFrom"::: ) "(" (Set (Var "a")) "," (Set (Var "k1")) "," (Set (Var "b")) "," (Set (Var "k2")) ")" ))))) ; theorem :: SCMPDS_2:37 (Bool "for" (Set (Var "ins")) "being" ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "st" (Bool (Bool (Set ($#k2_compos_0 :::"InsCode"::: ) (Set (Var "ins"))) ($#r1_hidden :::"="::: ) (Num 11))) "holds" (Bool "ex" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Int_position":::)(Bool "ex" (Set (Var "k1")) "," (Set (Var "k2")) "being" ($#m1_hidden :::"Integer":::) "st" (Bool (Set (Var "ins")) ($#r1_hidden :::"="::: ) (Set ($#k14_scmpds_2 :::"MultBy"::: ) "(" (Set (Var "a")) "," (Set (Var "k1")) "," (Set (Var "b")) "," (Set (Var "k2")) ")" ))))) ; theorem :: SCMPDS_2:38 (Bool "for" (Set (Var "ins")) "being" ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "st" (Bool (Bool (Set ($#k2_compos_0 :::"InsCode"::: ) (Set (Var "ins"))) ($#r1_hidden :::"="::: ) (Num 12))) "holds" (Bool "ex" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Int_position":::)(Bool "ex" (Set (Var "k1")) "," (Set (Var "k2")) "being" ($#m1_hidden :::"Integer":::) "st" (Bool (Set (Var "ins")) ($#r1_hidden :::"="::: ) (Set ($#k15_scmpds_2 :::"Divide"::: ) "(" (Set (Var "a")) "," (Set (Var "k1")) "," (Set (Var "b")) "," (Set (Var "k2")) ")" ))))) ; theorem :: SCMPDS_2:39 (Bool "for" (Set (Var "ins")) "being" ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "st" (Bool (Bool (Set ($#k2_compos_0 :::"InsCode"::: ) (Set (Var "ins"))) ($#r1_hidden :::"="::: ) (Num 13))) "holds" (Bool "ex" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Int_position":::)(Bool "ex" (Set (Var "k1")) "," (Set (Var "k2")) "being" ($#m1_hidden :::"Integer":::) "st" (Bool (Set (Var "ins")) ($#r1_hidden :::"="::: ) (Set "(" (Set (Var "a")) "," (Set (Var "k1")) ")" ($#k16_scmpds_2 :::":="::: ) "(" (Set (Var "b")) "," (Set (Var "k2")) ")" ))))) ; theorem :: SCMPDS_2:40 (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Int_position":::) "holds" (Bool (Set (Var "d")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "s")))))) ; theorem :: SCMPDS_2:41 (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "holds" (Bool (Set ($#k2_ami_2 :::"SCM-Data-Loc"::: ) ) ($#r1_tarski :::"c="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "s"))))) ; theorem :: SCMPDS_2:42 (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "holds" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k6_memstr_0 :::"DataPart"::: ) (Set (Var "s")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_ami_2 :::"SCM-Data-Loc"::: ) ))) ; theorem :: SCMPDS_2:43 (Bool "for" (Set (Var "dl")) "being" ($#m1_subset_1 :::"Int_position":::) "holds" (Bool (Set (Var "dl")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"IC"::: ) ))) ; theorem :: SCMPDS_2:44 (Bool "for" (Set (Var "s1")) "," (Set (Var "s2")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "st" (Bool (Bool (Set ($#k5_memstr_0 :::"IC"::: ) (Set (Var "s1"))) ($#r1_hidden :::"="::: ) (Set ($#k5_memstr_0 :::"IC"::: ) (Set (Var "s2")))) & (Bool "(" "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int_position":::) "holds" (Bool (Set (Set (Var "s1")) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s2")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")))) ")" )) "holds" (Bool (Set (Var "s1")) ($#r1_hidden :::"="::: ) (Set (Var "s2")))) ; begin theorem :: SCMPDS_2:45 (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "k1")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int_position":::) "holds" (Bool "(" (Bool (Set (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set "(" (Set (Var "a")) ($#k5_scmpds_2 :::":="::: ) (Set (Var "k1")) ")" ) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k4_struct_0 :::"IC"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_card_1 :::"succ"::: ) (Set "(" ($#k5_memstr_0 :::"IC"::: ) (Set (Var "s")) ")" ))) & (Bool (Set (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set "(" (Set (Var "a")) ($#k5_scmpds_2 :::":="::: ) (Set (Var "k1")) ")" ) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Var "k1"))) & (Bool "(" "for" (Set (Var "b")) "being" ($#m1_subset_1 :::"Int_position":::) "st" (Bool (Bool (Set (Var "b")) ($#r1_hidden :::"<>"::: ) (Set (Var "a")))) "holds" (Bool (Set (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set "(" (Set (Var "a")) ($#k5_scmpds_2 :::":="::: ) (Set (Var "k1")) ")" ) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "b")))) ")" ) ")" )))) ; theorem :: SCMPDS_2:46 (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "k1")) "," (Set (Var "k2")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int_position":::) "holds" (Bool "(" (Bool (Set (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set "(" "(" (Set (Var "a")) "," (Set (Var "k1")) ")" ($#k10_scmpds_2 :::":="::: ) (Set (Var "k2")) ")" ) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k4_struct_0 :::"IC"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_card_1 :::"succ"::: ) (Set "(" ($#k5_memstr_0 :::"IC"::: ) (Set (Var "s")) ")" ))) & (Bool (Set (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set "(" "(" (Set (Var "a")) "," (Set (Var "k1")) ")" ($#k10_scmpds_2 :::":="::: ) (Set (Var "k2")) ")" ) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ) "," (Set (Var "k1")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Var "k2"))) & (Bool "(" "for" (Set (Var "b")) "being" ($#m1_subset_1 :::"Int_position":::) "st" (Bool (Bool (Set (Var "b")) ($#r1_hidden :::"<>"::: ) (Set ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ) "," (Set (Var "k1")) ")" ))) "holds" (Bool (Set (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set "(" "(" (Set (Var "a")) "," (Set (Var "k1")) ")" ($#k10_scmpds_2 :::":="::: ) (Set (Var "k2")) ")" ) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "b")))) ")" ) ")" )))) ; theorem :: SCMPDS_2:47 (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "k1")) "," (Set (Var "k2")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Int_position":::) "holds" (Bool "(" (Bool (Set (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set "(" "(" (Set (Var "a")) "," (Set (Var "k1")) ")" ($#k16_scmpds_2 :::":="::: ) "(" (Set (Var "b")) "," (Set (Var "k2")) ")" ")" ) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k4_struct_0 :::"IC"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_card_1 :::"succ"::: ) (Set "(" ($#k5_memstr_0 :::"IC"::: ) (Set (Var "s")) ")" ))) & (Bool (Set (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set "(" "(" (Set (Var "a")) "," (Set (Var "k1")) ")" ($#k16_scmpds_2 :::":="::: ) "(" (Set (Var "b")) "," (Set (Var "k2")) ")" ")" ) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ) "," (Set (Var "k1")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "b")) ")" ) "," (Set (Var "k2")) ")" ")" ))) & (Bool "(" "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Int_position":::) "st" (Bool (Bool (Set (Var "c")) ($#r1_hidden :::"<>"::: ) (Set ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ) "," (Set (Var "k1")) ")" ))) "holds" (Bool (Set (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set "(" "(" (Set (Var "a")) "," (Set (Var "k1")) ")" ($#k16_scmpds_2 :::":="::: ) "(" (Set (Var "b")) "," (Set (Var "k2")) ")" ")" ) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "c")))) ")" ) ")" )))) ; theorem :: SCMPDS_2:48 (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "k1")) "," (Set (Var "k2")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int_position":::) "holds" (Bool "(" (Bool (Set (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set "(" ($#k11_scmpds_2 :::"AddTo"::: ) "(" (Set (Var "a")) "," (Set (Var "k1")) "," (Set (Var "k2")) ")" ")" ) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k4_struct_0 :::"IC"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_card_1 :::"succ"::: ) (Set "(" ($#k5_memstr_0 :::"IC"::: ) (Set (Var "s")) ")" ))) & (Bool (Set (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set "(" ($#k11_scmpds_2 :::"AddTo"::: ) "(" (Set (Var "a")) "," (Set (Var "k1")) "," (Set (Var "k2")) ")" ")" ) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ) "," (Set (Var "k1")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ) "," (Set (Var "k1")) ")" ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "k2")))) & (Bool "(" "for" (Set (Var "b")) "being" ($#m1_subset_1 :::"Int_position":::) "st" (Bool (Bool (Set (Var "b")) ($#r1_hidden :::"<>"::: ) (Set ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ) "," (Set (Var "k1")) ")" ))) "holds" (Bool (Set (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set "(" ($#k11_scmpds_2 :::"AddTo"::: ) "(" (Set (Var "a")) "," (Set (Var "k1")) "," (Set (Var "k2")) ")" ")" ) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "b")))) ")" ) ")" )))) ; theorem :: SCMPDS_2:49 (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "k1")) "," (Set (Var "k2")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Int_position":::) "holds" (Bool "(" (Bool (Set (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set "(" ($#k12_scmpds_2 :::"AddTo"::: ) "(" (Set (Var "a")) "," (Set (Var "k1")) "," (Set (Var "b")) "," (Set (Var "k2")) ")" ")" ) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k4_struct_0 :::"IC"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_card_1 :::"succ"::: ) (Set "(" ($#k5_memstr_0 :::"IC"::: ) (Set (Var "s")) ")" ))) & (Bool (Set (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set "(" ($#k12_scmpds_2 :::"AddTo"::: ) "(" (Set (Var "a")) "," (Set (Var "k1")) "," (Set (Var "b")) "," (Set (Var "k2")) ")" ")" ) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ) "," (Set (Var "k1")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ) "," (Set (Var "k1")) ")" ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "b")) ")" ) "," (Set (Var "k2")) ")" ")" ) ")" ))) & (Bool "(" "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Int_position":::) "st" (Bool (Bool (Set (Var "c")) ($#r1_hidden :::"<>"::: ) (Set ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ) "," (Set (Var "k1")) ")" ))) "holds" (Bool (Set (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set "(" ($#k12_scmpds_2 :::"AddTo"::: ) "(" (Set (Var "a")) "," (Set (Var "k1")) "," (Set (Var "b")) "," (Set (Var "k2")) ")" ")" ) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "c")))) ")" ) ")" )))) ; theorem :: SCMPDS_2:50 (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "k1")) "," (Set (Var "k2")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Int_position":::) "holds" (Bool "(" (Bool (Set (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set "(" ($#k13_scmpds_2 :::"SubFrom"::: ) "(" (Set (Var "a")) "," (Set (Var "k1")) "," (Set (Var "b")) "," (Set (Var "k2")) ")" ")" ) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k4_struct_0 :::"IC"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_card_1 :::"succ"::: ) (Set "(" ($#k5_memstr_0 :::"IC"::: ) (Set (Var "s")) ")" ))) & (Bool (Set (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set "(" ($#k13_scmpds_2 :::"SubFrom"::: ) "(" (Set (Var "a")) "," (Set (Var "k1")) "," (Set (Var "b")) "," (Set (Var "k2")) ")" ")" ) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ) "," (Set (Var "k1")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ) "," (Set (Var "k1")) ")" ")" ) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "b")) ")" ) "," (Set (Var "k2")) ")" ")" ) ")" ))) & (Bool "(" "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Int_position":::) "st" (Bool (Bool (Set (Var "c")) ($#r1_hidden :::"<>"::: ) (Set ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ) "," (Set (Var "k1")) ")" ))) "holds" (Bool (Set (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set "(" ($#k13_scmpds_2 :::"SubFrom"::: ) "(" (Set (Var "a")) "," (Set (Var "k1")) "," (Set (Var "b")) "," (Set (Var "k2")) ")" ")" ) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "c")))) ")" ) ")" )))) ; theorem :: SCMPDS_2:51 (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "k1")) "," (Set (Var "k2")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Int_position":::) "holds" (Bool "(" (Bool (Set (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set "(" ($#k14_scmpds_2 :::"MultBy"::: ) "(" (Set (Var "a")) "," (Set (Var "k1")) "," (Set (Var "b")) "," (Set (Var "k2")) ")" ")" ) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k4_struct_0 :::"IC"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_card_1 :::"succ"::: ) (Set "(" ($#k5_memstr_0 :::"IC"::: ) (Set (Var "s")) ")" ))) & (Bool (Set (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set "(" ($#k14_scmpds_2 :::"MultBy"::: ) "(" (Set (Var "a")) "," (Set (Var "k1")) "," (Set (Var "b")) "," (Set (Var "k2")) ")" ")" ) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ) "," (Set (Var "k1")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ) "," (Set (Var "k1")) ")" ")" ) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "b")) ")" ) "," (Set (Var "k2")) ")" ")" ) ")" ))) & (Bool "(" "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Int_position":::) "st" (Bool (Bool (Set (Var "c")) ($#r1_hidden :::"<>"::: ) (Set ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ) "," (Set (Var "k1")) ")" ))) "holds" (Bool (Set (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set "(" ($#k14_scmpds_2 :::"MultBy"::: ) "(" (Set (Var "a")) "," (Set (Var "k1")) "," (Set (Var "b")) "," (Set (Var "k2")) ")" ")" ) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "c")))) ")" ) ")" )))) ; theorem :: SCMPDS_2:52 (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "k1")) "," (Set (Var "k2")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Int_position":::) "holds" (Bool "(" (Bool (Set (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set "(" ($#k15_scmpds_2 :::"Divide"::: ) "(" (Set (Var "a")) "," (Set (Var "k1")) "," (Set (Var "b")) "," (Set (Var "k2")) ")" ")" ) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k4_struct_0 :::"IC"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_card_1 :::"succ"::: ) (Set "(" ($#k5_memstr_0 :::"IC"::: ) (Set (Var "s")) ")" ))) & "(" (Bool (Bool (Set ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ) "," (Set (Var "k1")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "b")) ")" ) "," (Set (Var "k2")) ")" ))) "implies" (Bool (Set (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set "(" ($#k15_scmpds_2 :::"Divide"::: ) "(" (Set (Var "a")) "," (Set (Var "k1")) "," (Set (Var "b")) "," (Set (Var "k2")) ")" ")" ) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ) "," (Set (Var "k1")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ) "," (Set (Var "k1")) ")" ")" ) ")" ) ($#k5_int_1 :::"div"::: ) (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "b")) ")" ) "," (Set (Var "k2")) ")" ")" ) ")" ))) ")" & (Bool (Set (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set "(" ($#k15_scmpds_2 :::"Divide"::: ) "(" (Set (Var "a")) "," (Set (Var "k1")) "," (Set (Var "b")) "," (Set (Var "k2")) ")" ")" ) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "b")) ")" ) "," (Set (Var "k2")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ) "," (Set (Var "k1")) ")" ")" ) ")" ) ($#k6_int_1 :::"mod"::: ) (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "b")) ")" ) "," (Set (Var "k2")) ")" ")" ) ")" ))) & (Bool "(" "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Int_position":::) "st" (Bool (Bool (Set (Var "c")) ($#r1_hidden :::"<>"::: ) (Set ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ) "," (Set (Var "k1")) ")" )) & (Bool (Set (Var "c")) ($#r1_hidden :::"<>"::: ) (Set ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "b")) ")" ) "," (Set (Var "k2")) ")" ))) "holds" (Bool (Set (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set "(" ($#k15_scmpds_2 :::"Divide"::: ) "(" (Set (Var "a")) "," (Set (Var "k1")) "," (Set (Var "b")) "," (Set (Var "k2")) ")" ")" ) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "c")))) ")" ) ")" )))) ; theorem :: SCMPDS_2:53 (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "k1")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int_position":::) "holds" (Bool "(" (Bool (Set (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set "(" ($#k15_scmpds_2 :::"Divide"::: ) "(" (Set (Var "a")) "," (Set (Var "k1")) "," (Set (Var "a")) "," (Set (Var "k1")) ")" ")" ) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k4_struct_0 :::"IC"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_card_1 :::"succ"::: ) (Set "(" ($#k5_memstr_0 :::"IC"::: ) (Set (Var "s")) ")" ))) & (Bool (Set (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set "(" ($#k15_scmpds_2 :::"Divide"::: ) "(" (Set (Var "a")) "," (Set (Var "k1")) "," (Set (Var "a")) "," (Set (Var "k1")) ")" ")" ) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ) "," (Set (Var "k1")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ) "," (Set (Var "k1")) ")" ")" ) ")" ) ($#k6_int_1 :::"mod"::: ) (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ) "," (Set (Var "k1")) ")" ")" ) ")" ))) & (Bool "(" "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Int_position":::) "st" (Bool (Bool (Set (Var "c")) ($#r1_hidden :::"<>"::: ) (Set ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ) "," (Set (Var "k1")) ")" ))) "holds" (Bool (Set (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set "(" ($#k15_scmpds_2 :::"Divide"::: ) "(" (Set (Var "a")) "," (Set (Var "k1")) "," (Set (Var "a")) "," (Set (Var "k1")) ")" ")" ) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "c")))) ")" ) ")" )))) ; definitionlet "s" be ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ); let "c" be ($#m1_hidden :::"Integer":::); func :::"ICplusConst"::: "(" "s" "," "c" ")" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) means :: SCMPDS_2:def 18 (Bool "ex" (Set (Var "m")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set (Var "m")) ($#r1_hidden :::"="::: ) (Set ($#k5_memstr_0 :::"IC"::: ) "s")) & (Bool it ($#r1_hidden :::"="::: ) (Set ($#k1_int_2 :::"abs"::: ) (Set "(" (Set (Var "m")) ($#k2_xcmplx_0 :::"+"::: ) "c" ")" ))) ")" )); end; :: deftheorem defines :::"ICplusConst"::: SCMPDS_2:def 18 : (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "c")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k17_scmpds_2 :::"ICplusConst"::: ) "(" (Set (Var "s")) "," (Set (Var "c")) ")" )) "iff" (Bool "ex" (Set (Var "m")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set (Var "m")) ($#r1_hidden :::"="::: ) (Set ($#k5_memstr_0 :::"IC"::: ) (Set (Var "s")))) & (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k1_int_2 :::"abs"::: ) (Set "(" (Set (Var "m")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "c")) ")" ))) ")" )) ")" )))); theorem :: SCMPDS_2:54 (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "k1")) "being" ($#m1_hidden :::"Integer":::) "holds" (Bool "(" (Bool (Set (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set "(" ($#k3_scmpds_2 :::"goto"::: ) (Set (Var "k1")) ")" ) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k4_struct_0 :::"IC"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k17_scmpds_2 :::"ICplusConst"::: ) "(" (Set (Var "s")) "," (Set (Var "k1")) ")" )) & (Bool "(" "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int_position":::) "holds" (Bool (Set (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set "(" ($#k3_scmpds_2 :::"goto"::: ) (Set (Var "k1")) ")" ) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")))) ")" ) ")" ))) ; theorem :: SCMPDS_2:55 (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "k1")) "," (Set (Var "k2")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Int_position":::) "holds" (Bool "(" "(" (Bool (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ) "," (Set (Var "k1")) ")" ")" )) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "implies" (Bool (Set (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set "(" "(" (Set (Var "a")) "," (Set (Var "k1")) ")" ($#k7_scmpds_2 :::"<>0_goto"::: ) (Set (Var "k2")) ")" ) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k4_struct_0 :::"IC"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k17_scmpds_2 :::"ICplusConst"::: ) "(" (Set (Var "s")) "," (Set (Var "k2")) ")" )) ")" & "(" (Bool (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ) "," (Set (Var "k1")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "implies" (Bool (Set (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set "(" "(" (Set (Var "a")) "," (Set (Var "k1")) ")" ($#k7_scmpds_2 :::"<>0_goto"::: ) (Set (Var "k2")) ")" ) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k4_struct_0 :::"IC"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_card_1 :::"succ"::: ) (Set "(" ($#k5_memstr_0 :::"IC"::: ) (Set (Var "s")) ")" ))) ")" & (Bool (Set (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set "(" "(" (Set (Var "a")) "," (Set (Var "k1")) ")" ($#k7_scmpds_2 :::"<>0_goto"::: ) (Set (Var "k2")) ")" ) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "b")))) ")" )))) ; theorem :: SCMPDS_2:56 (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "k1")) "," (Set (Var "k2")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Int_position":::) "holds" (Bool "(" "(" (Bool (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ) "," (Set (Var "k1")) ")" ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "implies" (Bool (Set (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set "(" "(" (Set (Var "a")) "," (Set (Var "k1")) ")" ($#k8_scmpds_2 :::"<=0_goto"::: ) (Set (Var "k2")) ")" ) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k4_struct_0 :::"IC"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k17_scmpds_2 :::"ICplusConst"::: ) "(" (Set (Var "s")) "," (Set (Var "k2")) ")" )) ")" & "(" (Bool (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ) "," (Set (Var "k1")) ")" ")" )) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "implies" (Bool (Set (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set "(" "(" (Set (Var "a")) "," (Set (Var "k1")) ")" ($#k8_scmpds_2 :::"<=0_goto"::: ) (Set (Var "k2")) ")" ) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k4_struct_0 :::"IC"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_card_1 :::"succ"::: ) (Set "(" ($#k5_memstr_0 :::"IC"::: ) (Set (Var "s")) ")" ))) ")" & (Bool (Set (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set "(" "(" (Set (Var "a")) "," (Set (Var "k1")) ")" ($#k8_scmpds_2 :::"<=0_goto"::: ) (Set (Var "k2")) ")" ) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "b")))) ")" )))) ; theorem :: SCMPDS_2:57 (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "k1")) "," (Set (Var "k2")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Int_position":::) "holds" (Bool "(" "(" (Bool (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ) "," (Set (Var "k1")) ")" ")" )) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "implies" (Bool (Set (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set "(" "(" (Set (Var "a")) "," (Set (Var "k1")) ")" ($#k9_scmpds_2 :::">=0_goto"::: ) (Set (Var "k2")) ")" ) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k4_struct_0 :::"IC"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k17_scmpds_2 :::"ICplusConst"::: ) "(" (Set (Var "s")) "," (Set (Var "k2")) ")" )) ")" & "(" (Bool (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ) "," (Set (Var "k1")) ")" ")" )) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "implies" (Bool (Set (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set "(" "(" (Set (Var "a")) "," (Set (Var "k1")) ")" ($#k9_scmpds_2 :::">=0_goto"::: ) (Set (Var "k2")) ")" ) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k4_struct_0 :::"IC"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_card_1 :::"succ"::: ) (Set "(" ($#k5_memstr_0 :::"IC"::: ) (Set (Var "s")) ")" ))) ")" & (Bool (Set (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set "(" "(" (Set (Var "a")) "," (Set (Var "k1")) ")" ($#k9_scmpds_2 :::">=0_goto"::: ) (Set (Var "k2")) ")" ) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "b")))) ")" )))) ; theorem :: SCMPDS_2:58 (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int_position":::) "holds" (Bool "(" (Bool (Set (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set "(" ($#k4_scmpds_2 :::"return"::: ) (Set (Var "a")) ")" ) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k4_struct_0 :::"IC"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_int_2 :::"abs"::: ) (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ) "," (Set ($#k15_scmpds_i :::"RetIC"::: ) ) ")" ")" ) ")" ) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 2))) & (Bool (Set (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set "(" ($#k4_scmpds_2 :::"return"::: ) (Set (Var "a")) ")" ) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ) "," (Set ($#k14_scmpds_i :::"RetSP"::: ) ) ")" ")" ))) & (Bool "(" "for" (Set (Var "b")) "being" ($#m1_subset_1 :::"Int_position":::) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Var "b")))) "holds" (Bool (Set (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set "(" ($#k4_scmpds_2 :::"return"::: ) (Set (Var "a")) ")" ) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "b")))) ")" ) ")" ))) ; theorem :: SCMPDS_2:59 (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "k1")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int_position":::) "holds" (Bool "(" (Bool (Set (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set "(" ($#k6_scmpds_2 :::"saveIC"::: ) "(" (Set (Var "a")) "," (Set (Var "k1")) ")" ")" ) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k4_struct_0 :::"IC"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_card_1 :::"succ"::: ) (Set "(" ($#k5_memstr_0 :::"IC"::: ) (Set (Var "s")) ")" ))) & (Bool (Set (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set "(" ($#k6_scmpds_2 :::"saveIC"::: ) "(" (Set (Var "a")) "," (Set (Var "k1")) ")" ")" ) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ) "," (Set (Var "k1")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k5_memstr_0 :::"IC"::: ) (Set (Var "s")))) & (Bool "(" "for" (Set (Var "b")) "being" ($#m1_subset_1 :::"Int_position":::) "st" (Bool (Bool (Set ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ) "," (Set (Var "k1")) ")" ) ($#r1_hidden :::"<>"::: ) (Set (Var "b")))) "holds" (Bool (Set (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set "(" ($#k6_scmpds_2 :::"saveIC"::: ) "(" (Set (Var "a")) "," (Set (Var "k1")) ")" ")" ) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "b")))) ")" ) ")" )))) ; theorem :: SCMPDS_2:60 canceled; theorem :: SCMPDS_2:61 (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Integer":::) (Bool "ex" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "st" (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Int_position":::) "holds" (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "d"))) ($#r1_hidden :::"="::: ) (Set (Var "k")))))) ; theorem :: SCMPDS_2:62 (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "loc")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "ex" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "st" (Bool "(" (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set ($#k5_numbers :::"NAT"::: ) )) ($#r1_hidden :::"="::: ) (Set (Var "loc"))) & (Bool "(" "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Int_position":::) "holds" (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "d"))) ($#r1_hidden :::"="::: ) (Set (Var "k"))) ")" ) ")" )))) ; theorem :: SCMPDS_2:63 (Bool "for" (Set (Var "I")) "being" ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "st" (Bool (Bool (Set (Var "I")) ($#r1_hidden :::"="::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k3_xtuple_0 :::"]"::: ) ))) "holds" (Bool (Set (Var "I")) "is" ($#v2_extpro_1 :::"halting"::: ) )) ; theorem :: SCMPDS_2:64 (Bool "for" (Set (Var "I")) "being" ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "st" (Bool (Bool "ex" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "st" (Bool (Set (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set (Var "I")) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k4_struct_0 :::"IC"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_card_1 :::"succ"::: ) (Set "(" ($#k5_memstr_0 :::"IC"::: ) (Set (Var "s")) ")" ))))) "holds" (Bool "not" (Bool (Set (Var "I")) "is" ($#v2_extpro_1 :::"halting"::: ) ))) ; theorem :: SCMPDS_2:65 (Bool "for" (Set (Var "k1")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int_position":::) "holds" (Bool (Bool "not" (Set (Set (Var "a")) ($#k5_scmpds_2 :::":="::: ) (Set (Var "k1"))) "is" ($#v2_extpro_1 :::"halting"::: ) )))) ; theorem :: SCMPDS_2:66 (Bool "for" (Set (Var "k1")) "," (Set (Var "k2")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int_position":::) "holds" (Bool (Bool "not" (Set "(" (Set (Var "a")) "," (Set (Var "k1")) ")" ($#k10_scmpds_2 :::":="::: ) (Set (Var "k2"))) "is" ($#v2_extpro_1 :::"halting"::: ) )))) ; theorem :: SCMPDS_2:67 (Bool "for" (Set (Var "k1")) "," (Set (Var "k2")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Int_position":::) "holds" (Bool (Bool "not" (Set "(" (Set (Var "a")) "," (Set (Var "k1")) ")" ($#k16_scmpds_2 :::":="::: ) "(" (Set (Var "b")) "," (Set (Var "k2")) ")" ) "is" ($#v2_extpro_1 :::"halting"::: ) )))) ; theorem :: SCMPDS_2:68 (Bool "for" (Set (Var "k1")) "," (Set (Var "k2")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int_position":::) "holds" (Bool (Bool "not" (Set ($#k11_scmpds_2 :::"AddTo"::: ) "(" (Set (Var "a")) "," (Set (Var "k1")) "," (Set (Var "k2")) ")" ) "is" ($#v2_extpro_1 :::"halting"::: ) )))) ; theorem :: SCMPDS_2:69 (Bool "for" (Set (Var "k1")) "," (Set (Var "k2")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Int_position":::) "holds" (Bool (Bool "not" (Set ($#k12_scmpds_2 :::"AddTo"::: ) "(" (Set (Var "a")) "," (Set (Var "k1")) "," (Set (Var "b")) "," (Set (Var "k2")) ")" ) "is" ($#v2_extpro_1 :::"halting"::: ) )))) ; theorem :: SCMPDS_2:70 (Bool "for" (Set (Var "k1")) "," (Set (Var "k2")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Int_position":::) "holds" (Bool (Bool "not" (Set ($#k13_scmpds_2 :::"SubFrom"::: ) "(" (Set (Var "a")) "," (Set (Var "k1")) "," (Set (Var "b")) "," (Set (Var "k2")) ")" ) "is" ($#v2_extpro_1 :::"halting"::: ) )))) ; theorem :: SCMPDS_2:71 (Bool "for" (Set (Var "k1")) "," (Set (Var "k2")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Int_position":::) "holds" (Bool (Bool "not" (Set ($#k14_scmpds_2 :::"MultBy"::: ) "(" (Set (Var "a")) "," (Set (Var "k1")) "," (Set (Var "b")) "," (Set (Var "k2")) ")" ) "is" ($#v2_extpro_1 :::"halting"::: ) )))) ; theorem :: SCMPDS_2:72 (Bool "for" (Set (Var "k1")) "," (Set (Var "k2")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Int_position":::) "holds" (Bool (Bool "not" (Set ($#k15_scmpds_2 :::"Divide"::: ) "(" (Set (Var "a")) "," (Set (Var "k1")) "," (Set (Var "b")) "," (Set (Var "k2")) ")" ) "is" ($#v2_extpro_1 :::"halting"::: ) )))) ; theorem :: SCMPDS_2:73 (Bool "for" (Set (Var "k1")) "being" ($#m1_hidden :::"Integer":::) "st" (Bool (Bool (Set (Var "k1")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "not" (Bool (Set ($#k3_scmpds_2 :::"goto"::: ) (Set (Var "k1"))) "is" ($#v2_extpro_1 :::"halting"::: ) ))) ; theorem :: SCMPDS_2:74 (Bool "for" (Set (Var "k1")) "," (Set (Var "k2")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int_position":::) "holds" (Bool (Bool "not" (Set "(" (Set (Var "a")) "," (Set (Var "k1")) ")" ($#k7_scmpds_2 :::"<>0_goto"::: ) (Set (Var "k2"))) "is" ($#v2_extpro_1 :::"halting"::: ) )))) ; theorem :: SCMPDS_2:75 (Bool "for" (Set (Var "k1")) "," (Set (Var "k2")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int_position":::) "holds" (Bool (Bool "not" (Set "(" (Set (Var "a")) "," (Set (Var "k1")) ")" ($#k8_scmpds_2 :::"<=0_goto"::: ) (Set (Var "k2"))) "is" ($#v2_extpro_1 :::"halting"::: ) )))) ; theorem :: SCMPDS_2:76 (Bool "for" (Set (Var "k1")) "," (Set (Var "k2")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int_position":::) "holds" (Bool (Bool "not" (Set "(" (Set (Var "a")) "," (Set (Var "k1")) ")" ($#k9_scmpds_2 :::">=0_goto"::: ) (Set (Var "k2"))) "is" ($#v2_extpro_1 :::"halting"::: ) )))) ; theorem :: SCMPDS_2:77 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int_position":::) "holds" (Bool (Bool "not" (Set ($#k4_scmpds_2 :::"return"::: ) (Set (Var "a"))) "is" ($#v2_extpro_1 :::"halting"::: ) ))) ; theorem :: SCMPDS_2:78 (Bool "for" (Set (Var "k1")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int_position":::) "holds" (Bool (Bool "not" (Set ($#k6_scmpds_2 :::"saveIC"::: ) "(" (Set (Var "a")) "," (Set (Var "k1")) ")" ) "is" ($#v2_extpro_1 :::"halting"::: ) )))) ; theorem :: SCMPDS_2:79 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" "not" (Bool (Set (Var "I")) "is" ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) )) "or" (Bool (Set (Var "I")) ($#r1_hidden :::"="::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k3_xtuple_0 :::"]"::: ) )) "or" (Bool "ex" (Set (Var "k1")) "being" ($#m1_hidden :::"Integer":::) "st" (Bool (Set (Var "I")) ($#r1_hidden :::"="::: ) (Set ($#k3_scmpds_2 :::"goto"::: ) (Set (Var "k1"))))) "or" (Bool "ex" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int_position":::) "st" (Bool (Set (Var "I")) ($#r1_hidden :::"="::: ) (Set ($#k4_scmpds_2 :::"return"::: ) (Set (Var "a"))))) "or" (Bool "ex" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int_position":::)(Bool "ex" (Set (Var "k1")) "being" ($#m1_hidden :::"Integer":::) "st" (Bool (Set (Var "I")) ($#r1_hidden :::"="::: ) (Set ($#k6_scmpds_2 :::"saveIC"::: ) "(" (Set (Var "a")) "," (Set (Var "k1")) ")" )))) "or" (Bool "ex" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int_position":::)(Bool "ex" (Set (Var "k1")) "being" ($#m1_hidden :::"Integer":::) "st" (Bool (Set (Var "I")) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k5_scmpds_2 :::":="::: ) (Set (Var "k1")))))) "or" (Bool "ex" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int_position":::)(Bool "ex" (Set (Var "k1")) "," (Set (Var "k2")) "being" ($#m1_hidden :::"Integer":::) "st" (Bool (Set (Var "I")) ($#r1_hidden :::"="::: ) (Set "(" (Set (Var "a")) "," (Set (Var "k1")) ")" ($#k10_scmpds_2 :::":="::: ) (Set (Var "k2")))))) "or" (Bool "ex" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int_position":::)(Bool "ex" (Set (Var "k1")) "," (Set (Var "k2")) "being" ($#m1_hidden :::"Integer":::) "st" (Bool (Set (Var "I")) ($#r1_hidden :::"="::: ) (Set "(" (Set (Var "a")) "," (Set (Var "k1")) ")" ($#k7_scmpds_2 :::"<>0_goto"::: ) (Set (Var "k2")))))) "or" (Bool "ex" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int_position":::)(Bool "ex" (Set (Var "k1")) "," (Set (Var "k2")) "being" ($#m1_hidden :::"Integer":::) "st" (Bool (Set (Var "I")) ($#r1_hidden :::"="::: ) (Set "(" (Set (Var "a")) "," (Set (Var "k1")) ")" ($#k8_scmpds_2 :::"<=0_goto"::: ) (Set (Var "k2")))))) "or" (Bool "ex" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int_position":::)(Bool "ex" (Set (Var "k1")) "," (Set (Var "k2")) "being" ($#m1_hidden :::"Integer":::) "st" (Bool (Set (Var "I")) ($#r1_hidden :::"="::: ) (Set "(" (Set (Var "a")) "," (Set (Var "k1")) ")" ($#k9_scmpds_2 :::">=0_goto"::: ) (Set (Var "k2")))))) "or" (Bool "ex" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Int_position":::)(Bool "ex" (Set (Var "k1")) "," (Set (Var "k2")) "being" ($#m1_hidden :::"Integer":::) "st" (Bool (Set (Var "I")) ($#r1_hidden :::"="::: ) (Set ($#k11_scmpds_2 :::"AddTo"::: ) "(" (Set (Var "a")) "," (Set (Var "k1")) "," (Set (Var "k2")) ")" )))) "or" (Bool "ex" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Int_position":::)(Bool "ex" (Set (Var "k1")) "," (Set (Var "k2")) "being" ($#m1_hidden :::"Integer":::) "st" (Bool (Set (Var "I")) ($#r1_hidden :::"="::: ) (Set ($#k12_scmpds_2 :::"AddTo"::: ) "(" (Set (Var "a")) "," (Set (Var "k1")) "," (Set (Var "b")) "," (Set (Var "k2")) ")" )))) "or" (Bool "ex" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Int_position":::)(Bool "ex" (Set (Var "k1")) "," (Set (Var "k2")) "being" ($#m1_hidden :::"Integer":::) "st" (Bool (Set (Var "I")) ($#r1_hidden :::"="::: ) (Set ($#k13_scmpds_2 :::"SubFrom"::: ) "(" (Set (Var "a")) "," (Set (Var "k1")) "," (Set (Var "b")) "," (Set (Var "k2")) ")" )))) "or" (Bool "ex" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Int_position":::)(Bool "ex" (Set (Var "k1")) "," (Set (Var "k2")) "being" ($#m1_hidden :::"Integer":::) "st" (Bool (Set (Var "I")) ($#r1_hidden :::"="::: ) (Set ($#k14_scmpds_2 :::"MultBy"::: ) "(" (Set (Var "a")) "," (Set (Var "k1")) "," (Set (Var "b")) "," (Set (Var "k2")) ")" )))) "or" (Bool "ex" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Int_position":::)(Bool "ex" (Set (Var "k1")) "," (Set (Var "k2")) "being" ($#m1_hidden :::"Integer":::) "st" (Bool (Set (Var "I")) ($#r1_hidden :::"="::: ) (Set ($#k15_scmpds_2 :::"Divide"::: ) "(" (Set (Var "a")) "," (Set (Var "k1")) "," (Set (Var "b")) "," (Set (Var "k2")) ")" )))) "or" (Bool "ex" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Int_position":::)(Bool "ex" (Set (Var "k1")) "," (Set (Var "k2")) "being" ($#m1_hidden :::"Integer":::) "st" (Bool (Set (Var "I")) ($#r1_hidden :::"="::: ) (Set "(" (Set (Var "a")) "," (Set (Var "k1")) ")" ($#k16_scmpds_2 :::":="::: ) "(" (Set (Var "b")) "," (Set (Var "k2")) ")" )))) ")" )) ; registration cluster (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) -> ($#v1_extpro_1 :::"strict"::: ) ($#v3_extpro_1 :::"halting"::: ) ; end; theorem :: SCMPDS_2:80 (Bool (Set ($#k2_compos_1 :::"halt"::: ) (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k3_xtuple_0 :::"]"::: ) )) ; theorem :: SCMPDS_2:81 canceled; theorem :: SCMPDS_2:82 (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k4_struct_0 :::"IC"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k10_ami_3 :::"dl."::: ) (Set (Var "i"))))) ; theorem :: SCMPDS_2:83 canceled; theorem :: SCMPDS_2:84 (Bool (Set ($#k8_struct_0 :::"Data-Locations"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k2_ami_2 :::"SCM-Data-Loc"::: ) )) ; theorem :: SCMPDS_2:85 canceled; theorem :: SCMPDS_2:86 (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "st" (Bool (Bool (Set ($#k2_compos_0 :::"InsCode"::: ) (Set (Var "I"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set ($#k2_extpro_1 :::"Exec"::: ) "(" (Set (Var "I")) "," (Set (Var "s")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "s"))))) ;