:: SCMPDS_1 semantic presentation begin theorem :: SCMPDS_1:1 canceled; theorem :: SCMPDS_1:2 canceled; theorem :: SCMPDS_1:3 (Bool "for" (Set (Var "d")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k2_ami_2 :::"SCM-Data-Loc"::: ) ) "holds" (Bool (Set (Var "d")) ($#r2_hidden :::"in"::: ) (Set (Set ($#k2_ami_2 :::"SCM-Data-Loc"::: ) ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k4_numbers :::"INT"::: ) )))) ; begin definitioncanceled; canceled; canceled; canceled; canceled; let "s" be ($#m1_subset_1 :::"SCM-State":::); let "a" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k2_ami_2 :::"SCM-Data-Loc"::: ) ); let "n" be ($#m1_hidden :::"Integer":::); func :::"Address_Add"::: "(" "s" "," "a" "," "n" ")" -> ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k2_ami_2 :::"SCM-Data-Loc"::: ) ) equals :: SCMPDS_1:def 6 (Set ($#k4_tarski :::"["::: ) (Num 1) "," (Set "(" ($#k1_int_2 :::"abs"::: ) (Set "(" (Set "(" "s" ($#k1_funct_1 :::"."::: ) "a" ")" ) ($#k2_xcmplx_0 :::"+"::: ) "n" ")" ) ")" ) ($#k4_tarski :::"]"::: ) ); end; :: deftheorem SCMPDS_1:def 1 : canceled; :: deftheorem SCMPDS_1:def 2 : canceled; :: deftheorem SCMPDS_1:def 3 : canceled; :: deftheorem SCMPDS_1:def 4 : canceled; :: deftheorem SCMPDS_1:def 5 : canceled; :: deftheorem defines :::"Address_Add"::: SCMPDS_1:def 6 : (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"SCM-State":::) (Bool "for" (Set (Var "a")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k2_ami_2 :::"SCM-Data-Loc"::: ) ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Integer":::) "holds" (Bool (Set ($#k1_scmpds_1 :::"Address_Add"::: ) "(" (Set (Var "s")) "," (Set (Var "a")) "," (Set (Var "n")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Num 1) "," (Set "(" ($#k1_int_2 :::"abs"::: ) (Set "(" (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "n")) ")" ) ")" ) ($#k4_tarski :::"]"::: ) ))))); definitionlet "s" be ($#m1_subset_1 :::"SCM-State":::); let "n" be ($#m1_hidden :::"Integer":::); func :::"jump_address"::: "(" "s" "," "n" ")" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) equals :: SCMPDS_1:def 7 (Set ($#k1_int_2 :::"abs"::: ) (Set "(" (Set "(" ($#k5_ami_2 :::"IC"::: ) "s" ")" ) ($#k2_xcmplx_0 :::"+"::: ) "n" ")" )); end; :: deftheorem defines :::"jump_address"::: SCMPDS_1:def 7 : (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"SCM-State":::) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Integer":::) "holds" (Bool (Set ($#k2_scmpds_1 :::"jump_address"::: ) "(" (Set (Var "s")) "," (Set (Var "n")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_int_2 :::"abs"::: ) (Set "(" (Set "(" ($#k5_ami_2 :::"IC"::: ) (Set (Var "s")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "n")) ")" ))))); definitionlet "d" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k2_ami_2 :::"SCM-Data-Loc"::: ) ); let "s" be ($#m1_hidden :::"Integer":::); :: original: :::"<*"::: redefine func :::"<*":::"d" "," "s":::"*>"::: -> ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Set ($#k2_ami_2 :::"SCM-Data-Loc"::: ) ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k4_numbers :::"INT"::: ) )); end; definitioncanceled; canceled; canceled; canceled; canceled; canceled; canceled; canceled; canceled; canceled; canceled; let "s" be ($#m1_subset_1 :::"SCM-State":::); let "a" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k2_ami_2 :::"SCM-Data-Loc"::: ) ); func :::"PopInstrLoc"::: "(" "s" "," "a" ")" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) equals :: SCMPDS_1:def 19 (Set (Set "(" ($#k1_int_2 :::"abs"::: ) (Set "(" "s" ($#k1_funct_1 :::"."::: ) "a" ")" ) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 2)); end; :: deftheorem SCMPDS_1:def 8 : canceled; :: deftheorem SCMPDS_1:def 9 : canceled; :: deftheorem SCMPDS_1:def 10 : canceled; :: deftheorem SCMPDS_1:def 11 : canceled; :: deftheorem SCMPDS_1:def 12 : canceled; :: deftheorem SCMPDS_1:def 13 : canceled; :: deftheorem SCMPDS_1:def 14 : canceled; :: deftheorem SCMPDS_1:def 15 : canceled; :: deftheorem SCMPDS_1:def 16 : canceled; :: deftheorem SCMPDS_1:def 17 : canceled; :: deftheorem SCMPDS_1:def 18 : canceled; :: deftheorem defines :::"PopInstrLoc"::: SCMPDS_1:def 19 : (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"SCM-State":::) (Bool "for" (Set (Var "a")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k2_ami_2 :::"SCM-Data-Loc"::: ) ) "holds" (Bool (Set ($#k4_scmpds_1 :::"PopInstrLoc"::: ) "(" (Set (Var "s")) "," (Set (Var "a")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_int_2 :::"abs"::: ) (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 2))))); definitioncanceled; canceled; end; :: deftheorem SCMPDS_1:def 20 : canceled; :: deftheorem SCMPDS_1:def 21 : canceled; definitionlet "x" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_scmpds_i :::"SCMPDS-Instr"::: ) ); let "s" be ($#m1_subset_1 :::"SCM-State":::); func :::"SCM-Exec-Res"::: "(" "x" "," "s" ")" -> ($#m1_subset_1 :::"SCM-State":::) equals :: SCMPDS_1:def 22 (Set ($#k6_ami_2 :::"SCM-Chg"::: ) "(" "s" "," (Set "(" ($#k2_scmpds_1 :::"jump_address"::: ) "(" "s" "," (Set "(" "x" ($#k4_scmpds_i :::"const_INT"::: ) ")" ) ")" ")" ) ")" ) if (Bool (Set ($#k2_compos_0 :::"InsCode"::: ) "x") ($#r1_hidden :::"="::: ) (Num 14)) (Set ($#k6_ami_2 :::"SCM-Chg"::: ) "(" (Set "(" ($#k7_ami_2 :::"SCM-Chg"::: ) "(" "s" "," (Set "(" "x" ($#k5_scmpds_i :::"P21address"::: ) ")" ) "," (Set "(" "x" ($#k6_scmpds_i :::"P22const"::: ) ")" ) ")" ")" ) "," (Set "(" ($#k1_ordinal1 :::"succ"::: ) (Set "(" ($#k5_ami_2 :::"IC"::: ) "s" ")" ) ")" ) ")" ) if (Bool (Set ($#k2_compos_0 :::"InsCode"::: ) "x") ($#r1_hidden :::"="::: ) (Num 2)) (Set ($#k6_ami_2 :::"SCM-Chg"::: ) "(" (Set "(" ($#k7_ami_2 :::"SCM-Chg"::: ) "(" "s" "," (Set "(" ($#k1_scmpds_1 :::"Address_Add"::: ) "(" "s" "," (Set "(" "x" ($#k5_scmpds_i :::"P21address"::: ) ")" ) "," (Set "(" "x" ($#k6_scmpds_i :::"P22const"::: ) ")" ) ")" ")" ) "," (Set "(" ($#k5_ami_2 :::"IC"::: ) "s" ")" ) ")" ")" ) "," (Set "(" ($#k1_ordinal1 :::"succ"::: ) (Set "(" ($#k5_ami_2 :::"IC"::: ) "s" ")" ) ")" ) ")" ) if (Bool (Set ($#k2_compos_0 :::"InsCode"::: ) "x") ($#r1_hidden :::"="::: ) (Num 3)) (Set ($#k6_ami_2 :::"SCM-Chg"::: ) "(" (Set "(" ($#k7_ami_2 :::"SCM-Chg"::: ) "(" "s" "," (Set "(" "x" ($#k3_scmpds_i :::"address_1"::: ) ")" ) "," (Set "(" "s" ($#k1_funct_1 :::"."::: ) (Set "(" ($#k1_scmpds_1 :::"Address_Add"::: ) "(" "s" "," (Set "(" "x" ($#k3_scmpds_i :::"address_1"::: ) ")" ) "," (Set ($#k14_scmpds_i :::"RetSP"::: ) ) ")" ")" ) ")" ) ")" ")" ) "," (Set "(" ($#k4_scmpds_1 :::"PopInstrLoc"::: ) "(" "s" "," (Set "(" ($#k1_scmpds_1 :::"Address_Add"::: ) "(" "s" "," (Set "(" "x" ($#k3_scmpds_i :::"address_1"::: ) ")" ) "," (Set ($#k15_scmpds_i :::"RetIC"::: ) ) ")" ")" ) ")" ")" ) ")" ) if (Bool (Set ($#k2_compos_0 :::"InsCode"::: ) "x") ($#r1_hidden :::"="::: ) (Num 1)) (Set ($#k6_ami_2 :::"SCM-Chg"::: ) "(" "s" "," (Set "(" ($#k14_funcop_1 :::"IFEQ"::: ) "(" (Set "(" "s" ($#k1_funct_1 :::"."::: ) (Set "(" ($#k1_scmpds_1 :::"Address_Add"::: ) "(" "s" "," (Set "(" "x" ($#k7_scmpds_i :::"P31address"::: ) ")" ) "," (Set "(" "x" ($#k8_scmpds_i :::"P32const"::: ) ")" ) ")" ")" ) ")" ) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set "(" ($#k1_ordinal1 :::"succ"::: ) (Set "(" ($#k5_ami_2 :::"IC"::: ) "s" ")" ) ")" ) "," (Set "(" ($#k2_scmpds_1 :::"jump_address"::: ) "(" "s" "," (Set "(" "x" ($#k9_scmpds_i :::"P33const"::: ) ")" ) ")" ")" ) ")" ")" ) ")" ) if (Bool (Set ($#k2_compos_0 :::"InsCode"::: ) "x") ($#r1_hidden :::"="::: ) (Num 4)) (Set ($#k6_ami_2 :::"SCM-Chg"::: ) "(" "s" "," (Set "(" ($#k5_xxreal_0 :::"IFGT"::: ) "(" (Set "(" "s" ($#k1_funct_1 :::"."::: ) (Set "(" ($#k1_scmpds_1 :::"Address_Add"::: ) "(" "s" "," (Set "(" "x" ($#k7_scmpds_i :::"P31address"::: ) ")" ) "," (Set "(" "x" ($#k8_scmpds_i :::"P32const"::: ) ")" ) ")" ")" ) ")" ) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set "(" ($#k1_ordinal1 :::"succ"::: ) (Set "(" ($#k5_ami_2 :::"IC"::: ) "s" ")" ) ")" ) "," (Set "(" ($#k2_scmpds_1 :::"jump_address"::: ) "(" "s" "," (Set "(" "x" ($#k9_scmpds_i :::"P33const"::: ) ")" ) ")" ")" ) ")" ")" ) ")" ) if (Bool (Set ($#k2_compos_0 :::"InsCode"::: ) "x") ($#r1_hidden :::"="::: ) (Num 5)) (Set ($#k6_ami_2 :::"SCM-Chg"::: ) "(" "s" "," (Set "(" ($#k5_xxreal_0 :::"IFGT"::: ) "(" (Set ($#k6_numbers :::"0"::: ) ) "," (Set "(" "s" ($#k1_funct_1 :::"."::: ) (Set "(" ($#k1_scmpds_1 :::"Address_Add"::: ) "(" "s" "," (Set "(" "x" ($#k7_scmpds_i :::"P31address"::: ) ")" ) "," (Set "(" "x" ($#k8_scmpds_i :::"P32const"::: ) ")" ) ")" ")" ) ")" ) "," (Set "(" ($#k1_ordinal1 :::"succ"::: ) (Set "(" ($#k5_ami_2 :::"IC"::: ) "s" ")" ) ")" ) "," (Set "(" ($#k2_scmpds_1 :::"jump_address"::: ) "(" "s" "," (Set "(" "x" ($#k9_scmpds_i :::"P33const"::: ) ")" ) ")" ")" ) ")" ")" ) ")" ) if (Bool (Set ($#k2_compos_0 :::"InsCode"::: ) "x") ($#r1_hidden :::"="::: ) (Num 6)) (Set ($#k6_ami_2 :::"SCM-Chg"::: ) "(" (Set "(" ($#k7_ami_2 :::"SCM-Chg"::: ) "(" "s" "," (Set "(" ($#k1_scmpds_1 :::"Address_Add"::: ) "(" "s" "," (Set "(" "x" ($#k7_scmpds_i :::"P31address"::: ) ")" ) "," (Set "(" "x" ($#k8_scmpds_i :::"P32const"::: ) ")" ) ")" ")" ) "," (Set "(" "x" ($#k9_scmpds_i :::"P33const"::: ) ")" ) ")" ")" ) "," (Set "(" ($#k1_ordinal1 :::"succ"::: ) (Set "(" ($#k5_ami_2 :::"IC"::: ) "s" ")" ) ")" ) ")" ) if (Bool (Set ($#k2_compos_0 :::"InsCode"::: ) "x") ($#r1_hidden :::"="::: ) (Num 7)) (Set ($#k6_ami_2 :::"SCM-Chg"::: ) "(" (Set "(" ($#k7_ami_2 :::"SCM-Chg"::: ) "(" "s" "," (Set "(" ($#k1_scmpds_1 :::"Address_Add"::: ) "(" "s" "," (Set "(" "x" ($#k7_scmpds_i :::"P31address"::: ) ")" ) "," (Set "(" "x" ($#k8_scmpds_i :::"P32const"::: ) ")" ) ")" ")" ) "," (Set "(" (Set "(" "s" ($#k1_funct_1 :::"."::: ) (Set "(" ($#k1_scmpds_1 :::"Address_Add"::: ) "(" "s" "," (Set "(" "x" ($#k7_scmpds_i :::"P31address"::: ) ")" ) "," (Set "(" "x" ($#k8_scmpds_i :::"P32const"::: ) ")" ) ")" ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" "x" ($#k9_scmpds_i :::"P33const"::: ) ")" ) ")" ) ")" ")" ) "," (Set "(" ($#k1_ordinal1 :::"succ"::: ) (Set "(" ($#k5_ami_2 :::"IC"::: ) "s" ")" ) ")" ) ")" ) if (Bool (Set ($#k2_compos_0 :::"InsCode"::: ) "x") ($#r1_hidden :::"="::: ) (Num 8)) (Set ($#k6_ami_2 :::"SCM-Chg"::: ) "(" (Set "(" ($#k7_ami_2 :::"SCM-Chg"::: ) "(" "s" "," (Set "(" ($#k1_scmpds_1 :::"Address_Add"::: ) "(" "s" "," (Set "(" "x" ($#k10_scmpds_i :::"P41address"::: ) ")" ) "," (Set "(" "x" ($#k12_scmpds_i :::"P43const"::: ) ")" ) ")" ")" ) "," (Set "(" (Set "(" "s" ($#k1_funct_1 :::"."::: ) (Set "(" ($#k1_scmpds_1 :::"Address_Add"::: ) "(" "s" "," (Set "(" "x" ($#k10_scmpds_i :::"P41address"::: ) ")" ) "," (Set "(" "x" ($#k12_scmpds_i :::"P43const"::: ) ")" ) ")" ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" "s" ($#k1_funct_1 :::"."::: ) (Set "(" ($#k1_scmpds_1 :::"Address_Add"::: ) "(" "s" "," (Set "(" "x" ($#k11_scmpds_i :::"P42address"::: ) ")" ) "," (Set "(" "x" ($#k13_scmpds_i :::"P44const"::: ) ")" ) ")" ")" ) ")" ) ")" ) ")" ")" ) "," (Set "(" ($#k1_ordinal1 :::"succ"::: ) (Set "(" ($#k5_ami_2 :::"IC"::: ) "s" ")" ) ")" ) ")" ) if (Bool (Set ($#k2_compos_0 :::"InsCode"::: ) "x") ($#r1_hidden :::"="::: ) (Num 9)) (Set ($#k6_ami_2 :::"SCM-Chg"::: ) "(" (Set "(" ($#k7_ami_2 :::"SCM-Chg"::: ) "(" "s" "," (Set "(" ($#k1_scmpds_1 :::"Address_Add"::: ) "(" "s" "," (Set "(" "x" ($#k10_scmpds_i :::"P41address"::: ) ")" ) "," (Set "(" "x" ($#k12_scmpds_i :::"P43const"::: ) ")" ) ")" ")" ) "," (Set "(" (Set "(" "s" ($#k1_funct_1 :::"."::: ) (Set "(" ($#k1_scmpds_1 :::"Address_Add"::: ) "(" "s" "," (Set "(" "x" ($#k10_scmpds_i :::"P41address"::: ) ")" ) "," (Set "(" "x" ($#k12_scmpds_i :::"P43const"::: ) ")" ) ")" ")" ) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" "s" ($#k1_funct_1 :::"."::: ) (Set "(" ($#k1_scmpds_1 :::"Address_Add"::: ) "(" "s" "," (Set "(" "x" ($#k11_scmpds_i :::"P42address"::: ) ")" ) "," (Set "(" "x" ($#k13_scmpds_i :::"P44const"::: ) ")" ) ")" ")" ) ")" ) ")" ) ")" ")" ) "," (Set "(" ($#k1_ordinal1 :::"succ"::: ) (Set "(" ($#k5_ami_2 :::"IC"::: ) "s" ")" ) ")" ) ")" ) if (Bool (Set ($#k2_compos_0 :::"InsCode"::: ) "x") ($#r1_hidden :::"="::: ) (Num 10)) (Set ($#k6_ami_2 :::"SCM-Chg"::: ) "(" (Set "(" ($#k7_ami_2 :::"SCM-Chg"::: ) "(" "s" "," (Set "(" ($#k1_scmpds_1 :::"Address_Add"::: ) "(" "s" "," (Set "(" "x" ($#k10_scmpds_i :::"P41address"::: ) ")" ) "," (Set "(" "x" ($#k12_scmpds_i :::"P43const"::: ) ")" ) ")" ")" ) "," (Set "(" (Set "(" "s" ($#k1_funct_1 :::"."::: ) (Set "(" ($#k1_scmpds_1 :::"Address_Add"::: ) "(" "s" "," (Set "(" "x" ($#k10_scmpds_i :::"P41address"::: ) ")" ) "," (Set "(" "x" ($#k12_scmpds_i :::"P43const"::: ) ")" ) ")" ")" ) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" "s" ($#k1_funct_1 :::"."::: ) (Set "(" ($#k1_scmpds_1 :::"Address_Add"::: ) "(" "s" "," (Set "(" "x" ($#k11_scmpds_i :::"P42address"::: ) ")" ) "," (Set "(" "x" ($#k13_scmpds_i :::"P44const"::: ) ")" ) ")" ")" ) ")" ) ")" ) ")" ")" ) "," (Set "(" ($#k1_ordinal1 :::"succ"::: ) (Set "(" ($#k5_ami_2 :::"IC"::: ) "s" ")" ) ")" ) ")" ) if (Bool (Set ($#k2_compos_0 :::"InsCode"::: ) "x") ($#r1_hidden :::"="::: ) (Num 11)) (Set ($#k6_ami_2 :::"SCM-Chg"::: ) "(" (Set "(" ($#k7_ami_2 :::"SCM-Chg"::: ) "(" "s" "," (Set "(" ($#k1_scmpds_1 :::"Address_Add"::: ) "(" "s" "," (Set "(" "x" ($#k10_scmpds_i :::"P41address"::: ) ")" ) "," (Set "(" "x" ($#k12_scmpds_i :::"P43const"::: ) ")" ) ")" ")" ) "," (Set "(" "s" ($#k1_funct_1 :::"."::: ) (Set "(" ($#k1_scmpds_1 :::"Address_Add"::: ) "(" "s" "," (Set "(" "x" ($#k11_scmpds_i :::"P42address"::: ) ")" ) "," (Set "(" "x" ($#k13_scmpds_i :::"P44const"::: ) ")" ) ")" ")" ) ")" ) ")" ")" ) "," (Set "(" ($#k1_ordinal1 :::"succ"::: ) (Set "(" ($#k5_ami_2 :::"IC"::: ) "s" ")" ) ")" ) ")" ) if (Bool (Set ($#k2_compos_0 :::"InsCode"::: ) "x") ($#r1_hidden :::"="::: ) (Num 13)) (Set ($#k6_ami_2 :::"SCM-Chg"::: ) "(" (Set "(" ($#k7_ami_2 :::"SCM-Chg"::: ) "(" (Set "(" ($#k7_ami_2 :::"SCM-Chg"::: ) "(" "s" "," (Set "(" ($#k1_scmpds_1 :::"Address_Add"::: ) "(" "s" "," (Set "(" "x" ($#k10_scmpds_i :::"P41address"::: ) ")" ) "," (Set "(" "x" ($#k12_scmpds_i :::"P43const"::: ) ")" ) ")" ")" ) "," (Set "(" (Set "(" "s" ($#k1_funct_1 :::"."::: ) (Set "(" ($#k1_scmpds_1 :::"Address_Add"::: ) "(" "s" "," (Set "(" "x" ($#k10_scmpds_i :::"P41address"::: ) ")" ) "," (Set "(" "x" ($#k12_scmpds_i :::"P43const"::: ) ")" ) ")" ")" ) ")" ) ($#k5_int_1 :::"div"::: ) (Set "(" "s" ($#k1_funct_1 :::"."::: ) (Set "(" ($#k1_scmpds_1 :::"Address_Add"::: ) "(" "s" "," (Set "(" "x" ($#k11_scmpds_i :::"P42address"::: ) ")" ) "," (Set "(" "x" ($#k13_scmpds_i :::"P44const"::: ) ")" ) ")" ")" ) ")" ) ")" ) ")" ")" ) "," (Set "(" ($#k1_scmpds_1 :::"Address_Add"::: ) "(" "s" "," (Set "(" "x" ($#k11_scmpds_i :::"P42address"::: ) ")" ) "," (Set "(" "x" ($#k13_scmpds_i :::"P44const"::: ) ")" ) ")" ")" ) "," (Set "(" (Set "(" "s" ($#k1_funct_1 :::"."::: ) (Set "(" ($#k1_scmpds_1 :::"Address_Add"::: ) "(" "s" "," (Set "(" "x" ($#k10_scmpds_i :::"P41address"::: ) ")" ) "," (Set "(" "x" ($#k12_scmpds_i :::"P43const"::: ) ")" ) ")" ")" ) ")" ) ($#k6_int_1 :::"mod"::: ) (Set "(" "s" ($#k1_funct_1 :::"."::: ) (Set "(" ($#k1_scmpds_1 :::"Address_Add"::: ) "(" "s" "," (Set "(" "x" ($#k11_scmpds_i :::"P42address"::: ) ")" ) "," (Set "(" "x" ($#k13_scmpds_i :::"P44const"::: ) ")" ) ")" ")" ) ")" ) ")" ) ")" ")" ) "," (Set "(" ($#k1_ordinal1 :::"succ"::: ) (Set "(" ($#k5_ami_2 :::"IC"::: ) "s" ")" ) ")" ) ")" ) if (Bool (Set ($#k2_compos_0 :::"InsCode"::: ) "x") ($#r1_hidden :::"="::: ) (Num 12)) otherwise "s"; end; :: deftheorem defines :::"SCM-Exec-Res"::: SCMPDS_1:def 22 : (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_scmpds_i :::"SCMPDS-Instr"::: ) ) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"SCM-State":::) "holds" (Bool "(" "(" (Bool (Bool (Set ($#k2_compos_0 :::"InsCode"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Num 14))) "implies" (Bool (Set ($#k5_scmpds_1 :::"SCM-Exec-Res"::: ) "(" (Set (Var "x")) "," (Set (Var "s")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_ami_2 :::"SCM-Chg"::: ) "(" (Set (Var "s")) "," (Set "(" ($#k2_scmpds_1 :::"jump_address"::: ) "(" (Set (Var "s")) "," (Set "(" (Set (Var "x")) ($#k4_scmpds_i :::"const_INT"::: ) ")" ) ")" ")" ) ")" )) ")" & "(" (Bool (Bool (Set ($#k2_compos_0 :::"InsCode"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Num 2))) "implies" (Bool (Set ($#k5_scmpds_1 :::"SCM-Exec-Res"::: ) "(" (Set (Var "x")) "," (Set (Var "s")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_ami_2 :::"SCM-Chg"::: ) "(" (Set "(" ($#k7_ami_2 :::"SCM-Chg"::: ) "(" (Set (Var "s")) "," (Set "(" (Set (Var "x")) ($#k5_scmpds_i :::"P21address"::: ) ")" ) "," (Set "(" (Set (Var "x")) ($#k6_scmpds_i :::"P22const"::: ) ")" ) ")" ")" ) "," (Set "(" ($#k1_ordinal1 :::"succ"::: ) (Set "(" ($#k5_ami_2 :::"IC"::: ) (Set (Var "s")) ")" ) ")" ) ")" )) ")" & "(" (Bool (Bool (Set ($#k2_compos_0 :::"InsCode"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Num 3))) "implies" (Bool (Set ($#k5_scmpds_1 :::"SCM-Exec-Res"::: ) "(" (Set (Var "x")) "," (Set (Var "s")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_ami_2 :::"SCM-Chg"::: ) "(" (Set "(" ($#k7_ami_2 :::"SCM-Chg"::: ) "(" (Set (Var "s")) "," (Set "(" ($#k1_scmpds_1 :::"Address_Add"::: ) "(" (Set (Var "s")) "," (Set "(" (Set (Var "x")) ($#k5_scmpds_i :::"P21address"::: ) ")" ) "," (Set "(" (Set (Var "x")) ($#k6_scmpds_i :::"P22const"::: ) ")" ) ")" ")" ) "," (Set "(" ($#k5_ami_2 :::"IC"::: ) (Set (Var "s")) ")" ) ")" ")" ) "," (Set "(" ($#k1_ordinal1 :::"succ"::: ) (Set "(" ($#k5_ami_2 :::"IC"::: ) (Set (Var "s")) ")" ) ")" ) ")" )) ")" & "(" (Bool (Bool (Set ($#k2_compos_0 :::"InsCode"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Num 1))) "implies" (Bool (Set ($#k5_scmpds_1 :::"SCM-Exec-Res"::: ) "(" (Set (Var "x")) "," (Set (Var "s")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_ami_2 :::"SCM-Chg"::: ) "(" (Set "(" ($#k7_ami_2 :::"SCM-Chg"::: ) "(" (Set (Var "s")) "," (Set "(" (Set (Var "x")) ($#k3_scmpds_i :::"address_1"::: ) ")" ) "," (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k1_scmpds_1 :::"Address_Add"::: ) "(" (Set (Var "s")) "," (Set "(" (Set (Var "x")) ($#k3_scmpds_i :::"address_1"::: ) ")" ) "," (Set ($#k14_scmpds_i :::"RetSP"::: ) ) ")" ")" ) ")" ) ")" ")" ) "," (Set "(" ($#k4_scmpds_1 :::"PopInstrLoc"::: ) "(" (Set (Var "s")) "," (Set "(" ($#k1_scmpds_1 :::"Address_Add"::: ) "(" (Set (Var "s")) "," (Set "(" (Set (Var "x")) ($#k3_scmpds_i :::"address_1"::: ) ")" ) "," (Set ($#k15_scmpds_i :::"RetIC"::: ) ) ")" ")" ) ")" ")" ) ")" )) ")" & "(" (Bool (Bool (Set ($#k2_compos_0 :::"InsCode"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Num 4))) "implies" (Bool (Set ($#k5_scmpds_1 :::"SCM-Exec-Res"::: ) "(" (Set (Var "x")) "," (Set (Var "s")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_ami_2 :::"SCM-Chg"::: ) "(" (Set (Var "s")) "," (Set "(" ($#k14_funcop_1 :::"IFEQ"::: ) "(" (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k1_scmpds_1 :::"Address_Add"::: ) "(" (Set (Var "s")) "," (Set "(" (Set (Var "x")) ($#k7_scmpds_i :::"P31address"::: ) ")" ) "," (Set "(" (Set (Var "x")) ($#k8_scmpds_i :::"P32const"::: ) ")" ) ")" ")" ) ")" ) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set "(" ($#k1_ordinal1 :::"succ"::: ) (Set "(" ($#k5_ami_2 :::"IC"::: ) (Set (Var "s")) ")" ) ")" ) "," (Set "(" ($#k2_scmpds_1 :::"jump_address"::: ) "(" (Set (Var "s")) "," (Set "(" (Set (Var "x")) ($#k9_scmpds_i :::"P33const"::: ) ")" ) ")" ")" ) ")" ")" ) ")" )) ")" & "(" (Bool (Bool (Set ($#k2_compos_0 :::"InsCode"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Num 5))) "implies" (Bool (Set ($#k5_scmpds_1 :::"SCM-Exec-Res"::: ) "(" (Set (Var "x")) "," (Set (Var "s")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_ami_2 :::"SCM-Chg"::: ) "(" (Set (Var "s")) "," (Set "(" ($#k5_xxreal_0 :::"IFGT"::: ) "(" (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k1_scmpds_1 :::"Address_Add"::: ) "(" (Set (Var "s")) "," (Set "(" (Set (Var "x")) ($#k7_scmpds_i :::"P31address"::: ) ")" ) "," (Set "(" (Set (Var "x")) ($#k8_scmpds_i :::"P32const"::: ) ")" ) ")" ")" ) ")" ) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set "(" ($#k1_ordinal1 :::"succ"::: ) (Set "(" ($#k5_ami_2 :::"IC"::: ) (Set (Var "s")) ")" ) ")" ) "," (Set "(" ($#k2_scmpds_1 :::"jump_address"::: ) "(" (Set (Var "s")) "," (Set "(" (Set (Var "x")) ($#k9_scmpds_i :::"P33const"::: ) ")" ) ")" ")" ) ")" ")" ) ")" )) ")" & "(" (Bool (Bool (Set ($#k2_compos_0 :::"InsCode"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Num 6))) "implies" (Bool (Set ($#k5_scmpds_1 :::"SCM-Exec-Res"::: ) "(" (Set (Var "x")) "," (Set (Var "s")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_ami_2 :::"SCM-Chg"::: ) "(" (Set (Var "s")) "," (Set "(" ($#k5_xxreal_0 :::"IFGT"::: ) "(" (Set ($#k6_numbers :::"0"::: ) ) "," (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k1_scmpds_1 :::"Address_Add"::: ) "(" (Set (Var "s")) "," (Set "(" (Set (Var "x")) ($#k7_scmpds_i :::"P31address"::: ) ")" ) "," (Set "(" (Set (Var "x")) ($#k8_scmpds_i :::"P32const"::: ) ")" ) ")" ")" ) ")" ) "," (Set "(" ($#k1_ordinal1 :::"succ"::: ) (Set "(" ($#k5_ami_2 :::"IC"::: ) (Set (Var "s")) ")" ) ")" ) "," (Set "(" ($#k2_scmpds_1 :::"jump_address"::: ) "(" (Set (Var "s")) "," (Set "(" (Set (Var "x")) ($#k9_scmpds_i :::"P33const"::: ) ")" ) ")" ")" ) ")" ")" ) ")" )) ")" & "(" (Bool (Bool (Set ($#k2_compos_0 :::"InsCode"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Num 7))) "implies" (Bool (Set ($#k5_scmpds_1 :::"SCM-Exec-Res"::: ) "(" (Set (Var "x")) "," (Set (Var "s")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_ami_2 :::"SCM-Chg"::: ) "(" (Set "(" ($#k7_ami_2 :::"SCM-Chg"::: ) "(" (Set (Var "s")) "," (Set "(" ($#k1_scmpds_1 :::"Address_Add"::: ) "(" (Set (Var "s")) "," (Set "(" (Set (Var "x")) ($#k7_scmpds_i :::"P31address"::: ) ")" ) "," (Set "(" (Set (Var "x")) ($#k8_scmpds_i :::"P32const"::: ) ")" ) ")" ")" ) "," (Set "(" (Set (Var "x")) ($#k9_scmpds_i :::"P33const"::: ) ")" ) ")" ")" ) "," (Set "(" ($#k1_ordinal1 :::"succ"::: ) (Set "(" ($#k5_ami_2 :::"IC"::: ) (Set (Var "s")) ")" ) ")" ) ")" )) ")" & "(" (Bool (Bool (Set ($#k2_compos_0 :::"InsCode"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Num 8))) "implies" (Bool (Set ($#k5_scmpds_1 :::"SCM-Exec-Res"::: ) "(" (Set (Var "x")) "," (Set (Var "s")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_ami_2 :::"SCM-Chg"::: ) "(" (Set "(" ($#k7_ami_2 :::"SCM-Chg"::: ) "(" (Set (Var "s")) "," (Set "(" ($#k1_scmpds_1 :::"Address_Add"::: ) "(" (Set (Var "s")) "," (Set "(" (Set (Var "x")) ($#k7_scmpds_i :::"P31address"::: ) ")" ) "," (Set "(" (Set (Var "x")) ($#k8_scmpds_i :::"P32const"::: ) ")" ) ")" ")" ) "," (Set "(" (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k1_scmpds_1 :::"Address_Add"::: ) "(" (Set (Var "s")) "," (Set "(" (Set (Var "x")) ($#k7_scmpds_i :::"P31address"::: ) ")" ) "," (Set "(" (Set (Var "x")) ($#k8_scmpds_i :::"P32const"::: ) ")" ) ")" ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set (Var "x")) ($#k9_scmpds_i :::"P33const"::: ) ")" ) ")" ) ")" ")" ) "," (Set "(" ($#k1_ordinal1 :::"succ"::: ) (Set "(" ($#k5_ami_2 :::"IC"::: ) (Set (Var "s")) ")" ) ")" ) ")" )) ")" & "(" (Bool (Bool (Set ($#k2_compos_0 :::"InsCode"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Num 9))) "implies" (Bool (Set ($#k5_scmpds_1 :::"SCM-Exec-Res"::: ) "(" (Set (Var "x")) "," (Set (Var "s")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_ami_2 :::"SCM-Chg"::: ) "(" (Set "(" ($#k7_ami_2 :::"SCM-Chg"::: ) "(" (Set (Var "s")) "," (Set "(" ($#k1_scmpds_1 :::"Address_Add"::: ) "(" (Set (Var "s")) "," (Set "(" (Set (Var "x")) ($#k10_scmpds_i :::"P41address"::: ) ")" ) "," (Set "(" (Set (Var "x")) ($#k12_scmpds_i :::"P43const"::: ) ")" ) ")" ")" ) "," (Set "(" (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k1_scmpds_1 :::"Address_Add"::: ) "(" (Set (Var "s")) "," (Set "(" (Set (Var "x")) ($#k10_scmpds_i :::"P41address"::: ) ")" ) "," (Set "(" (Set (Var "x")) ($#k12_scmpds_i :::"P43const"::: ) ")" ) ")" ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k1_scmpds_1 :::"Address_Add"::: ) "(" (Set (Var "s")) "," (Set "(" (Set (Var "x")) ($#k11_scmpds_i :::"P42address"::: ) ")" ) "," (Set "(" (Set (Var "x")) ($#k13_scmpds_i :::"P44const"::: ) ")" ) ")" ")" ) ")" ) ")" ) ")" ")" ) "," (Set "(" ($#k1_ordinal1 :::"succ"::: ) (Set "(" ($#k5_ami_2 :::"IC"::: ) (Set (Var "s")) ")" ) ")" ) ")" )) ")" & "(" (Bool (Bool (Set ($#k2_compos_0 :::"InsCode"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Num 10))) "implies" (Bool (Set ($#k5_scmpds_1 :::"SCM-Exec-Res"::: ) "(" (Set (Var "x")) "," (Set (Var "s")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_ami_2 :::"SCM-Chg"::: ) "(" (Set "(" ($#k7_ami_2 :::"SCM-Chg"::: ) "(" (Set (Var "s")) "," (Set "(" ($#k1_scmpds_1 :::"Address_Add"::: ) "(" (Set (Var "s")) "," (Set "(" (Set (Var "x")) ($#k10_scmpds_i :::"P41address"::: ) ")" ) "," (Set "(" (Set (Var "x")) ($#k12_scmpds_i :::"P43const"::: ) ")" ) ")" ")" ) "," (Set "(" (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k1_scmpds_1 :::"Address_Add"::: ) "(" (Set (Var "s")) "," (Set "(" (Set (Var "x")) ($#k10_scmpds_i :::"P41address"::: ) ")" ) "," (Set "(" (Set (Var "x")) ($#k12_scmpds_i :::"P43const"::: ) ")" ) ")" ")" ) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k1_scmpds_1 :::"Address_Add"::: ) "(" (Set (Var "s")) "," (Set "(" (Set (Var "x")) ($#k11_scmpds_i :::"P42address"::: ) ")" ) "," (Set "(" (Set (Var "x")) ($#k13_scmpds_i :::"P44const"::: ) ")" ) ")" ")" ) ")" ) ")" ) ")" ")" ) "," (Set "(" ($#k1_ordinal1 :::"succ"::: ) (Set "(" ($#k5_ami_2 :::"IC"::: ) (Set (Var "s")) ")" ) ")" ) ")" )) ")" & "(" (Bool (Bool (Set ($#k2_compos_0 :::"InsCode"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Num 11))) "implies" (Bool (Set ($#k5_scmpds_1 :::"SCM-Exec-Res"::: ) "(" (Set (Var "x")) "," (Set (Var "s")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_ami_2 :::"SCM-Chg"::: ) "(" (Set "(" ($#k7_ami_2 :::"SCM-Chg"::: ) "(" (Set (Var "s")) "," (Set "(" ($#k1_scmpds_1 :::"Address_Add"::: ) "(" (Set (Var "s")) "," (Set "(" (Set (Var "x")) ($#k10_scmpds_i :::"P41address"::: ) ")" ) "," (Set "(" (Set (Var "x")) ($#k12_scmpds_i :::"P43const"::: ) ")" ) ")" ")" ) "," (Set "(" (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k1_scmpds_1 :::"Address_Add"::: ) "(" (Set (Var "s")) "," (Set "(" (Set (Var "x")) ($#k10_scmpds_i :::"P41address"::: ) ")" ) "," (Set "(" (Set (Var "x")) ($#k12_scmpds_i :::"P43const"::: ) ")" ) ")" ")" ) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k1_scmpds_1 :::"Address_Add"::: ) "(" (Set (Var "s")) "," (Set "(" (Set (Var "x")) ($#k11_scmpds_i :::"P42address"::: ) ")" ) "," (Set "(" (Set (Var "x")) ($#k13_scmpds_i :::"P44const"::: ) ")" ) ")" ")" ) ")" ) ")" ) ")" ")" ) "," (Set "(" ($#k1_ordinal1 :::"succ"::: ) (Set "(" ($#k5_ami_2 :::"IC"::: ) (Set (Var "s")) ")" ) ")" ) ")" )) ")" & "(" (Bool (Bool (Set ($#k2_compos_0 :::"InsCode"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Num 13))) "implies" (Bool (Set ($#k5_scmpds_1 :::"SCM-Exec-Res"::: ) "(" (Set (Var "x")) "," (Set (Var "s")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_ami_2 :::"SCM-Chg"::: ) "(" (Set "(" ($#k7_ami_2 :::"SCM-Chg"::: ) "(" (Set (Var "s")) "," (Set "(" ($#k1_scmpds_1 :::"Address_Add"::: ) "(" (Set (Var "s")) "," (Set "(" (Set (Var "x")) ($#k10_scmpds_i :::"P41address"::: ) ")" ) "," (Set "(" (Set (Var "x")) ($#k12_scmpds_i :::"P43const"::: ) ")" ) ")" ")" ) "," (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k1_scmpds_1 :::"Address_Add"::: ) "(" (Set (Var "s")) "," (Set "(" (Set (Var "x")) ($#k11_scmpds_i :::"P42address"::: ) ")" ) "," (Set "(" (Set (Var "x")) ($#k13_scmpds_i :::"P44const"::: ) ")" ) ")" ")" ) ")" ) ")" ")" ) "," (Set "(" ($#k1_ordinal1 :::"succ"::: ) (Set "(" ($#k5_ami_2 :::"IC"::: ) (Set (Var "s")) ")" ) ")" ) ")" )) ")" & "(" (Bool (Bool (Set ($#k2_compos_0 :::"InsCode"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Num 12))) "implies" (Bool (Set ($#k5_scmpds_1 :::"SCM-Exec-Res"::: ) "(" (Set (Var "x")) "," (Set (Var "s")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_ami_2 :::"SCM-Chg"::: ) "(" (Set "(" ($#k7_ami_2 :::"SCM-Chg"::: ) "(" (Set "(" ($#k7_ami_2 :::"SCM-Chg"::: ) "(" (Set (Var "s")) "," (Set "(" ($#k1_scmpds_1 :::"Address_Add"::: ) "(" (Set (Var "s")) "," (Set "(" (Set (Var "x")) ($#k10_scmpds_i :::"P41address"::: ) ")" ) "," (Set "(" (Set (Var "x")) ($#k12_scmpds_i :::"P43const"::: ) ")" ) ")" ")" ) "," (Set "(" (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k1_scmpds_1 :::"Address_Add"::: ) "(" (Set (Var "s")) "," (Set "(" (Set (Var "x")) ($#k10_scmpds_i :::"P41address"::: ) ")" ) "," (Set "(" (Set (Var "x")) ($#k12_scmpds_i :::"P43const"::: ) ")" ) ")" ")" ) ")" ) ($#k5_int_1 :::"div"::: ) (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k1_scmpds_1 :::"Address_Add"::: ) "(" (Set (Var "s")) "," (Set "(" (Set (Var "x")) ($#k11_scmpds_i :::"P42address"::: ) ")" ) "," (Set "(" (Set (Var "x")) ($#k13_scmpds_i :::"P44const"::: ) ")" ) ")" ")" ) ")" ) ")" ) ")" ")" ) "," (Set "(" ($#k1_scmpds_1 :::"Address_Add"::: ) "(" (Set (Var "s")) "," (Set "(" (Set (Var "x")) ($#k11_scmpds_i :::"P42address"::: ) ")" ) "," (Set "(" (Set (Var "x")) ($#k13_scmpds_i :::"P44const"::: ) ")" ) ")" ")" ) "," (Set "(" (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k1_scmpds_1 :::"Address_Add"::: ) "(" (Set (Var "s")) "," (Set "(" (Set (Var "x")) ($#k10_scmpds_i :::"P41address"::: ) ")" ) "," (Set "(" (Set (Var "x")) ($#k12_scmpds_i :::"P43const"::: ) ")" ) ")" ")" ) ")" ) ($#k6_int_1 :::"mod"::: ) (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k1_scmpds_1 :::"Address_Add"::: ) "(" (Set (Var "s")) "," (Set "(" (Set (Var "x")) ($#k11_scmpds_i :::"P42address"::: ) ")" ) "," (Set "(" (Set (Var "x")) ($#k13_scmpds_i :::"P44const"::: ) ")" ) ")" ")" ) ")" ) ")" ) ")" ")" ) "," (Set "(" ($#k1_ordinal1 :::"succ"::: ) (Set "(" ($#k5_ami_2 :::"IC"::: ) (Set (Var "s")) ")" ) ")" ) ")" )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k2_compos_0 :::"InsCode"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Num 14))) & (Bool (Bool "not" (Set ($#k2_compos_0 :::"InsCode"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Num 2))) & (Bool (Bool "not" (Set ($#k2_compos_0 :::"InsCode"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Num 3))) & (Bool (Bool "not" (Set ($#k2_compos_0 :::"InsCode"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Num 1))) & (Bool (Bool "not" (Set ($#k2_compos_0 :::"InsCode"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Num 4))) & (Bool (Bool "not" (Set ($#k2_compos_0 :::"InsCode"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Num 5))) & (Bool (Bool "not" (Set ($#k2_compos_0 :::"InsCode"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Num 6))) & (Bool (Bool "not" (Set ($#k2_compos_0 :::"InsCode"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Num 7))) & (Bool (Bool "not" (Set ($#k2_compos_0 :::"InsCode"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Num 8))) & (Bool (Bool "not" (Set ($#k2_compos_0 :::"InsCode"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Num 9))) & (Bool (Bool "not" (Set ($#k2_compos_0 :::"InsCode"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Num 10))) & (Bool (Bool "not" (Set ($#k2_compos_0 :::"InsCode"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Num 11))) & (Bool (Bool "not" (Set ($#k2_compos_0 :::"InsCode"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Num 13))) & (Bool (Bool "not" (Set ($#k2_compos_0 :::"InsCode"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Num 12)))) "implies" (Bool (Set ($#k5_scmpds_1 :::"SCM-Exec-Res"::: ) "(" (Set (Var "x")) "," (Set (Var "s")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "s"))) ")" ")" ))); definitionfunc :::"SCMPDS-Exec"::: -> ($#m1_subset_1 :::"Action":::) "of" (Set ($#k1_scmpds_i :::"SCMPDS-Instr"::: ) ) "," (Set "(" ($#k4_card_3 :::"product"::: ) (Set "(" (Set ($#k4_ami_2 :::"SCM-VAL"::: ) ) ($#k3_relat_1 :::"*"::: ) (Set ($#k3_ami_2 :::"SCM-OK"::: ) ) ")" ) ")" ) means :: SCMPDS_1:def 23 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_scmpds_i :::"SCMPDS-Instr"::: ) ) (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"SCM-State":::) "holds" (Bool (Set (Set "(" it ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set ($#k5_scmpds_1 :::"SCM-Exec-Res"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" )))); end; :: deftheorem defines :::"SCMPDS-Exec"::: SCMPDS_1:def 23 : (Bool "for" (Set (Var "b1")) "being" ($#m1_subset_1 :::"Action":::) "of" (Set ($#k1_scmpds_i :::"SCMPDS-Instr"::: ) ) "," (Set "(" ($#k4_card_3 :::"product"::: ) (Set "(" (Set ($#k4_ami_2 :::"SCM-VAL"::: ) ) ($#k3_relat_1 :::"*"::: ) (Set ($#k3_ami_2 :::"SCM-OK"::: ) ) ")" ) ")" ) "holds" (Bool "(" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k6_scmpds_1 :::"SCMPDS-Exec"::: ) )) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_scmpds_i :::"SCMPDS-Instr"::: ) ) (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"SCM-State":::) "holds" (Bool (Set (Set "(" (Set (Var "b1")) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set ($#k5_scmpds_1 :::"SCM-Exec-Res"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" )))) ")" ));