:: AMI_2 semantic presentation begin definitionfunc :::"SCM-Memory"::: -> ($#m1_hidden :::"set"::: ) equals :: AMI_2:def 1 (Set (Set ($#k1_tarski :::"{"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#k1_tarski :::"}"::: ) ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k2_scm_inst :::"SCM-Data-Loc"::: ) )); end; :: deftheorem defines :::"SCM-Memory"::: AMI_2:def 1 : (Bool (Set ($#k1_ami_2 :::"SCM-Memory"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set ($#k1_tarski :::"{"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#k1_tarski :::"}"::: ) ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k2_scm_inst :::"SCM-Data-Loc"::: ) ))); registration cluster (Set ($#k1_ami_2 :::"SCM-Memory"::: ) ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; definition:: original: :::"SCM-Data-Loc"::: redefine func :::"SCM-Data-Loc"::: -> ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_ami_2 :::"SCM-Memory"::: ) ); end; definitioncanceled; canceled; func :::"SCM-OK"::: -> ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_ami_2 :::"SCM-Memory"::: ) ) "," (Num 2) means :: AMI_2:def 4 (Bool "for" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_ami_2 :::"SCM-Memory"::: ) ) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "k")) ($#r1_hidden :::"="::: ) (Set ($#k5_numbers :::"NAT"::: ) ))) "implies" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" & "(" (Bool (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k2_ami_2 :::"SCM-Data-Loc"::: ) ))) "implies" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Num 1)) ")" ")" )); end; :: deftheorem AMI_2:def 2 : canceled; :: deftheorem AMI_2:def 3 : canceled; :: deftheorem defines :::"SCM-OK"::: AMI_2:def 4 : (Bool "for" (Set (Var "b1")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_ami_2 :::"SCM-Memory"::: ) ) "," (Num 2) "holds" (Bool "(" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k3_ami_2 :::"SCM-OK"::: ) )) "iff" (Bool "for" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_ami_2 :::"SCM-Memory"::: ) ) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "k")) ($#r1_hidden :::"="::: ) (Set ($#k5_numbers :::"NAT"::: ) ))) "implies" (Bool (Set (Set (Var "b1")) ($#k3_funct_2 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" & "(" (Bool (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k2_ami_2 :::"SCM-Data-Loc"::: ) ))) "implies" (Bool (Set (Set (Var "b1")) ($#k3_funct_2 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Num 1)) ")" ")" )) ")" )); theorem :: AMI_2:1 canceled; definitionfunc :::"SCM-VAL"::: -> ($#m1_hidden :::"ManySortedSet":::) "of" (Num 2) equals :: AMI_2:def 5 (Set ($#k6_afinsq_1 :::"<%"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set ($#k4_numbers :::"INT"::: ) ) ($#k6_afinsq_1 :::"%>"::: ) ); end; :: deftheorem defines :::"SCM-VAL"::: AMI_2:def 5 : (Bool (Set ($#k4_ami_2 :::"SCM-VAL"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k6_afinsq_1 :::"<%"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set ($#k4_numbers :::"INT"::: ) ) ($#k6_afinsq_1 :::"%>"::: ) )); theorem :: AMI_2:2 canceled; theorem :: AMI_2:3 canceled; theorem :: AMI_2:4 canceled; theorem :: AMI_2:5 canceled; theorem :: AMI_2:6 (Bool (Set (Set "(" (Set ($#k4_ami_2 :::"SCM-VAL"::: ) ) ($#k3_relat_1 :::"*"::: ) (Set ($#k3_ami_2 :::"SCM-OK"::: ) ) ")" ) ($#k1_funct_1 :::"."::: ) (Set ($#k5_numbers :::"NAT"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k5_numbers :::"NAT"::: ) )) ; theorem :: AMI_2:7 (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_ami_2 :::"SCM-Memory"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k2_ami_2 :::"SCM-Data-Loc"::: ) ))) "holds" (Bool (Set (Set "(" (Set ($#k4_ami_2 :::"SCM-VAL"::: ) ) ($#k3_relat_1 :::"*"::: ) (Set ($#k3_ami_2 :::"SCM-OK"::: ) ) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k4_numbers :::"INT"::: ) ))) ; registration cluster (Set (Set ($#k3_ami_2 :::"SCM-OK"::: ) ) ($#k3_relat_1 :::"*"::: ) (Set ($#k4_ami_2 :::"SCM-VAL"::: ) )) -> ($#v2_relat_1 :::"non-empty"::: ) ; end; definitionmode SCM-State is ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_card_3 :::"product"::: ) (Set "(" (Set ($#k4_ami_2 :::"SCM-VAL"::: ) ) ($#k3_relat_1 :::"*"::: ) (Set ($#k3_ami_2 :::"SCM-OK"::: ) ) ")" )); end; theorem :: AMI_2:8 (Bool "for" (Set (Var "a")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k2_ami_2 :::"SCM-Data-Loc"::: ) ) "holds" (Bool (Set (Set "(" (Set ($#k4_ami_2 :::"SCM-VAL"::: ) ) ($#k3_relat_1 :::"*"::: ) (Set ($#k3_ami_2 :::"SCM-OK"::: ) ) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k4_numbers :::"INT"::: ) ))) ; theorem :: AMI_2:9 (Bool (Set ($#k5_card_3 :::"pi"::: ) "(" (Set "(" ($#k4_card_3 :::"product"::: ) (Set "(" (Set ($#k4_ami_2 :::"SCM-VAL"::: ) ) ($#k3_relat_1 :::"*"::: ) (Set ($#k3_ami_2 :::"SCM-OK"::: ) ) ")" ) ")" ) "," (Set ($#k5_numbers :::"NAT"::: ) ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k5_numbers :::"NAT"::: ) )) ; theorem :: AMI_2:10 (Bool "for" (Set (Var "a")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k2_ami_2 :::"SCM-Data-Loc"::: ) ) "holds" (Bool (Set ($#k5_card_3 :::"pi"::: ) "(" (Set "(" ($#k4_card_3 :::"product"::: ) (Set "(" (Set ($#k4_ami_2 :::"SCM-VAL"::: ) ) ($#k3_relat_1 :::"*"::: ) (Set ($#k3_ami_2 :::"SCM-OK"::: ) ) ")" ) ")" ) "," (Set (Var "a")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_numbers :::"INT"::: ) ))) ; definitionlet "s" be ($#m1_subset_1 :::"SCM-State":::); func :::"IC"::: "s" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) equals :: AMI_2:def 6 (Set "s" ($#k1_funct_1 :::"."::: ) (Set ($#k5_numbers :::"NAT"::: ) )); end; :: deftheorem defines :::"IC"::: AMI_2:def 6 : (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"SCM-State":::) "holds" (Bool (Set ($#k5_ami_2 :::"IC"::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set ($#k5_numbers :::"NAT"::: ) )))); definitionlet "s" be ($#m1_subset_1 :::"SCM-State":::); let "u" be ($#m1_hidden :::"Nat":::); func :::"SCM-Chg"::: "(" "s" "," "u" ")" -> ($#m1_subset_1 :::"SCM-State":::) equals :: AMI_2:def 7 (Set "s" ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set ($#k5_numbers :::"NAT"::: ) ) ($#k16_funcop_1 :::".-->"::: ) "u" ")" )); end; :: deftheorem defines :::"SCM-Chg"::: AMI_2:def 7 : (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"SCM-State":::) (Bool "for" (Set (Var "u")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k6_ami_2 :::"SCM-Chg"::: ) "(" (Set (Var "s")) "," (Set (Var "u")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set ($#k5_numbers :::"NAT"::: ) ) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "u")) ")" ))))); theorem :: AMI_2:11 (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"SCM-State":::) (Bool "for" (Set (Var "u")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set "(" ($#k6_ami_2 :::"SCM-Chg"::: ) "(" (Set (Var "s")) "," (Set (Var "u")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set ($#k5_numbers :::"NAT"::: ) )) ($#r1_hidden :::"="::: ) (Set (Var "u"))))) ; theorem :: AMI_2:12 (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"SCM-State":::) (Bool "for" (Set (Var "u")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "mk")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k2_ami_2 :::"SCM-Data-Loc"::: ) ) "holds" (Bool (Set (Set "(" ($#k6_ami_2 :::"SCM-Chg"::: ) "(" (Set (Var "s")) "," (Set (Var "u")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "mk"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "mk"))))))) ; theorem :: AMI_2:13 (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"SCM-State":::) (Bool "for" (Set (Var "u")) "," (Set (Var "v")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set "(" ($#k6_ami_2 :::"SCM-Chg"::: ) "(" (Set (Var "s")) "," (Set (Var "u")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "v")))))) ; definitionlet "s" be ($#m1_subset_1 :::"SCM-State":::); let "t" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k2_ami_2 :::"SCM-Data-Loc"::: ) ); let "u" be ($#m1_hidden :::"Integer":::); func :::"SCM-Chg"::: "(" "s" "," "t" "," "u" ")" -> ($#m1_subset_1 :::"SCM-State":::) equals :: AMI_2:def 8 (Set "s" ($#k1_funct_4 :::"+*"::: ) (Set "(" "t" ($#k16_funcop_1 :::".-->"::: ) "u" ")" )); end; :: deftheorem defines :::"SCM-Chg"::: AMI_2:def 8 : (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"SCM-State":::) (Bool "for" (Set (Var "t")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k2_ami_2 :::"SCM-Data-Loc"::: ) ) (Bool "for" (Set (Var "u")) "being" ($#m1_hidden :::"Integer":::) "holds" (Bool (Set ($#k7_ami_2 :::"SCM-Chg"::: ) "(" (Set (Var "s")) "," (Set (Var "t")) "," (Set (Var "u")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "t")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "u")) ")" )))))); theorem :: AMI_2:14 (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"SCM-State":::) (Bool "for" (Set (Var "t")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k2_ami_2 :::"SCM-Data-Loc"::: ) ) (Bool "for" (Set (Var "u")) "being" ($#m1_hidden :::"Integer":::) "holds" (Bool (Set (Set "(" ($#k7_ami_2 :::"SCM-Chg"::: ) "(" (Set (Var "s")) "," (Set (Var "t")) "," (Set (Var "u")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set ($#k5_numbers :::"NAT"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set ($#k5_numbers :::"NAT"::: ) )))))) ; theorem :: AMI_2:15 (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"SCM-State":::) (Bool "for" (Set (Var "t")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k2_ami_2 :::"SCM-Data-Loc"::: ) ) (Bool "for" (Set (Var "u")) "being" ($#m1_hidden :::"Integer":::) "holds" (Bool (Set (Set "(" ($#k7_ami_2 :::"SCM-Chg"::: ) "(" (Set (Var "s")) "," (Set (Var "t")) "," (Set (Var "u")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "t"))) ($#r1_hidden :::"="::: ) (Set (Var "u")))))) ; theorem :: AMI_2:16 (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"SCM-State":::) (Bool "for" (Set (Var "t")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k2_ami_2 :::"SCM-Data-Loc"::: ) ) (Bool "for" (Set (Var "u")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "mk")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k2_ami_2 :::"SCM-Data-Loc"::: ) ) "st" (Bool (Bool (Set (Var "mk")) ($#r1_hidden :::"<>"::: ) (Set (Var "t")))) "holds" (Bool (Set (Set "(" ($#k7_ami_2 :::"SCM-Chg"::: ) "(" (Set (Var "s")) "," (Set (Var "t")) "," (Set (Var "u")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "mk"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "mk")))))))) ; registrationlet "s" be ($#m1_subset_1 :::"SCM-State":::); let "a" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k2_ami_2 :::"SCM-Data-Loc"::: ) ); cluster (Set "s" ($#k1_funct_1 :::"."::: ) "a") -> ($#v1_int_1 :::"integer"::: ) ; end; definitioncanceled; canceled; canceled; canceled; canceled; let "x" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_scm_inst :::"SCM-Instr"::: ) ); let "s" be ($#m1_subset_1 :::"SCM-State":::); func :::"SCM-Exec-Res"::: "(" "x" "," "s" ")" -> ($#m1_subset_1 :::"SCM-State":::) equals :: AMI_2:def 14 (Set ($#k6_ami_2 :::"SCM-Chg"::: ) "(" (Set "(" ($#k7_ami_2 :::"SCM-Chg"::: ) "(" "s" "," (Set "(" "x" ($#k4_scm_inst :::"address_1"::: ) ")" ) "," (Set "(" "s" ($#k1_funct_1 :::"."::: ) (Set "(" "x" ($#k5_scm_inst :::"address_2"::: ) ")" ) ")" ) ")" ")" ) "," (Set "(" ($#k4_card_1 :::"succ"::: ) (Set "(" ($#k5_ami_2 :::"IC"::: ) "s" ")" ) ")" ) ")" ) if (Bool "ex" (Set (Var "mk")) "," (Set (Var "ml")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k2_ami_2 :::"SCM-Data-Loc"::: ) ) "st" (Bool "x" ($#r1_hidden :::"="::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Num 1) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "mk")) "," (Set (Var "ml")) ($#k10_finseq_1 :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) ))) (Set ($#k6_ami_2 :::"SCM-Chg"::: ) "(" (Set "(" ($#k7_ami_2 :::"SCM-Chg"::: ) "(" "s" "," (Set "(" "x" ($#k4_scm_inst :::"address_1"::: ) ")" ) "," (Set "(" (Set "(" "s" ($#k1_funct_1 :::"."::: ) (Set "(" "x" ($#k4_scm_inst :::"address_1"::: ) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" "s" ($#k1_funct_1 :::"."::: ) (Set "(" "x" ($#k5_scm_inst :::"address_2"::: ) ")" ) ")" ) ")" ) ")" ")" ) "," (Set "(" ($#k4_card_1 :::"succ"::: ) (Set "(" ($#k5_ami_2 :::"IC"::: ) "s" ")" ) ")" ) ")" ) if (Bool "ex" (Set (Var "mk")) "," (Set (Var "ml")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k2_ami_2 :::"SCM-Data-Loc"::: ) ) "st" (Bool "x" ($#r1_hidden :::"="::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Num 2) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "mk")) "," (Set (Var "ml")) ($#k10_finseq_1 :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) ))) (Set ($#k6_ami_2 :::"SCM-Chg"::: ) "(" (Set "(" ($#k7_ami_2 :::"SCM-Chg"::: ) "(" "s" "," (Set "(" "x" ($#k4_scm_inst :::"address_1"::: ) ")" ) "," (Set "(" (Set "(" "s" ($#k1_funct_1 :::"."::: ) (Set "(" "x" ($#k4_scm_inst :::"address_1"::: ) ")" ) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" "s" ($#k1_funct_1 :::"."::: ) (Set "(" "x" ($#k5_scm_inst :::"address_2"::: ) ")" ) ")" ) ")" ) ")" ")" ) "," (Set "(" ($#k4_card_1 :::"succ"::: ) (Set "(" ($#k5_ami_2 :::"IC"::: ) "s" ")" ) ")" ) ")" ) if (Bool "ex" (Set (Var "mk")) "," (Set (Var "ml")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k2_ami_2 :::"SCM-Data-Loc"::: ) ) "st" (Bool "x" ($#r1_hidden :::"="::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Num 3) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "mk")) "," (Set (Var "ml")) ($#k10_finseq_1 :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) ))) (Set ($#k6_ami_2 :::"SCM-Chg"::: ) "(" (Set "(" ($#k7_ami_2 :::"SCM-Chg"::: ) "(" "s" "," (Set "(" "x" ($#k4_scm_inst :::"address_1"::: ) ")" ) "," (Set "(" (Set "(" "s" ($#k1_funct_1 :::"."::: ) (Set "(" "x" ($#k4_scm_inst :::"address_1"::: ) ")" ) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" "s" ($#k1_funct_1 :::"."::: ) (Set "(" "x" ($#k5_scm_inst :::"address_2"::: ) ")" ) ")" ) ")" ) ")" ")" ) "," (Set "(" ($#k4_card_1 :::"succ"::: ) (Set "(" ($#k5_ami_2 :::"IC"::: ) "s" ")" ) ")" ) ")" ) if (Bool "ex" (Set (Var "mk")) "," (Set (Var "ml")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k2_ami_2 :::"SCM-Data-Loc"::: ) ) "st" (Bool "x" ($#r1_hidden :::"="::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Num 4) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "mk")) "," (Set (Var "ml")) ($#k10_finseq_1 :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) ))) (Set ($#k6_ami_2 :::"SCM-Chg"::: ) "(" (Set "(" ($#k7_ami_2 :::"SCM-Chg"::: ) "(" (Set "(" ($#k7_ami_2 :::"SCM-Chg"::: ) "(" "s" "," (Set "(" "x" ($#k4_scm_inst :::"address_1"::: ) ")" ) "," (Set "(" (Set "(" "s" ($#k1_funct_1 :::"."::: ) (Set "(" "x" ($#k4_scm_inst :::"address_1"::: ) ")" ) ")" ) ($#k5_int_1 :::"div"::: ) (Set "(" "s" ($#k1_funct_1 :::"."::: ) (Set "(" "x" ($#k5_scm_inst :::"address_2"::: ) ")" ) ")" ) ")" ) ")" ")" ) "," (Set "(" "x" ($#k5_scm_inst :::"address_2"::: ) ")" ) "," (Set "(" (Set "(" "s" ($#k1_funct_1 :::"."::: ) (Set "(" "x" ($#k4_scm_inst :::"address_1"::: ) ")" ) ")" ) ($#k6_int_1 :::"mod"::: ) (Set "(" "s" ($#k1_funct_1 :::"."::: ) (Set "(" "x" ($#k5_scm_inst :::"address_2"::: ) ")" ) ")" ) ")" ) ")" ")" ) "," (Set "(" ($#k4_card_1 :::"succ"::: ) (Set "(" ($#k5_ami_2 :::"IC"::: ) "s" ")" ) ")" ) ")" ) if (Bool "ex" (Set (Var "mk")) "," (Set (Var "ml")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k2_ami_2 :::"SCM-Data-Loc"::: ) ) "st" (Bool "x" ($#r1_hidden :::"="::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Num 5) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "mk")) "," (Set (Var "ml")) ($#k10_finseq_1 :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) ))) (Set ($#k6_ami_2 :::"SCM-Chg"::: ) "(" "s" "," (Set "(" "x" ($#k6_scm_inst :::"jump_address"::: ) ")" ) ")" ) if (Bool "ex" (Set (Var "mk")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "x" ($#r1_hidden :::"="::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Num 6) "," (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "mk")) ($#k9_finseq_1 :::"*>"::: ) ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k3_xtuple_0 :::"]"::: ) ))) (Set ($#k6_ami_2 :::"SCM-Chg"::: ) "(" "s" "," (Set "(" ($#k15_funcop_1 :::"IFEQ"::: ) "(" (Set "(" "s" ($#k1_funct_1 :::"."::: ) (Set "(" "x" ($#k8_scm_inst :::"cond_address"::: ) ")" ) ")" ) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set "(" "x" ($#k7_scm_inst :::"cjump_address"::: ) ")" ) "," (Set "(" ($#k4_card_1 :::"succ"::: ) (Set "(" ($#k5_ami_2 :::"IC"::: ) "s" ")" ) ")" ) ")" ")" ) ")" ) if (Bool "ex" (Set (Var "mk")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) )(Bool "ex" (Set (Var "ml")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k2_ami_2 :::"SCM-Data-Loc"::: ) ) "st" (Bool "x" ($#r1_hidden :::"="::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Num 7) "," (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "mk")) ($#k9_finseq_1 :::"*>"::: ) ) "," (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "ml")) ($#k12_finseq_1 :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) )))) (Set ($#k6_ami_2 :::"SCM-Chg"::: ) "(" "s" "," (Set "(" ($#k5_xxreal_0 :::"IFGT"::: ) "(" (Set "(" "s" ($#k1_funct_1 :::"."::: ) (Set "(" "x" ($#k8_scm_inst :::"cond_address"::: ) ")" ) ")" ) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set "(" "x" ($#k7_scm_inst :::"cjump_address"::: ) ")" ) "," (Set "(" ($#k4_card_1 :::"succ"::: ) (Set "(" ($#k5_ami_2 :::"IC"::: ) "s" ")" ) ")" ) ")" ")" ) ")" ) if (Bool "ex" (Set (Var "mk")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) )(Bool "ex" (Set (Var "ml")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k2_ami_2 :::"SCM-Data-Loc"::: ) ) "st" (Bool "x" ($#r1_hidden :::"="::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Num 8) "," (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "mk")) ($#k9_finseq_1 :::"*>"::: ) ) "," (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "ml")) ($#k12_finseq_1 :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) )))) otherwise "s"; end; :: deftheorem AMI_2:def 9 : canceled; :: deftheorem AMI_2:def 10 : canceled; :: deftheorem AMI_2:def 11 : canceled; :: deftheorem AMI_2:def 12 : canceled; :: deftheorem AMI_2:def 13 : canceled; :: deftheorem defines :::"SCM-Exec-Res"::: AMI_2:def 14 : (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_scm_inst :::"SCM-Instr"::: ) ) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"SCM-State":::) "holds" (Bool "(" "(" (Bool (Bool "ex" (Set (Var "mk")) "," (Set (Var "ml")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k2_ami_2 :::"SCM-Data-Loc"::: ) ) "st" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Num 1) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "mk")) "," (Set (Var "ml")) ($#k10_finseq_1 :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) )))) "implies" (Bool (Set ($#k8_ami_2 :::"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")) ($#k4_scm_inst :::"address_1"::: ) ")" ) "," (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "x")) ($#k5_scm_inst :::"address_2"::: ) ")" ) ")" ) ")" ")" ) "," (Set "(" ($#k4_card_1 :::"succ"::: ) (Set "(" ($#k5_ami_2 :::"IC"::: ) (Set (Var "s")) ")" ) ")" ) ")" )) ")" & "(" (Bool (Bool "ex" (Set (Var "mk")) "," (Set (Var "ml")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k2_ami_2 :::"SCM-Data-Loc"::: ) ) "st" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Num 2) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "mk")) "," (Set (Var "ml")) ($#k10_finseq_1 :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) )))) "implies" (Bool (Set ($#k8_ami_2 :::"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")) ($#k4_scm_inst :::"address_1"::: ) ")" ) "," (Set "(" (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "x")) ($#k4_scm_inst :::"address_1"::: ) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "x")) ($#k5_scm_inst :::"address_2"::: ) ")" ) ")" ) ")" ) ")" ")" ) "," (Set "(" ($#k4_card_1 :::"succ"::: ) (Set "(" ($#k5_ami_2 :::"IC"::: ) (Set (Var "s")) ")" ) ")" ) ")" )) ")" & "(" (Bool (Bool "ex" (Set (Var "mk")) "," (Set (Var "ml")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k2_ami_2 :::"SCM-Data-Loc"::: ) ) "st" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Num 3) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "mk")) "," (Set (Var "ml")) ($#k10_finseq_1 :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) )))) "implies" (Bool (Set ($#k8_ami_2 :::"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")) ($#k4_scm_inst :::"address_1"::: ) ")" ) "," (Set "(" (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "x")) ($#k4_scm_inst :::"address_1"::: ) ")" ) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "x")) ($#k5_scm_inst :::"address_2"::: ) ")" ) ")" ) ")" ) ")" ")" ) "," (Set "(" ($#k4_card_1 :::"succ"::: ) (Set "(" ($#k5_ami_2 :::"IC"::: ) (Set (Var "s")) ")" ) ")" ) ")" )) ")" & "(" (Bool (Bool "ex" (Set (Var "mk")) "," (Set (Var "ml")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k2_ami_2 :::"SCM-Data-Loc"::: ) ) "st" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Num 4) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "mk")) "," (Set (Var "ml")) ($#k10_finseq_1 :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) )))) "implies" (Bool (Set ($#k8_ami_2 :::"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")) ($#k4_scm_inst :::"address_1"::: ) ")" ) "," (Set "(" (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "x")) ($#k4_scm_inst :::"address_1"::: ) ")" ) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "x")) ($#k5_scm_inst :::"address_2"::: ) ")" ) ")" ) ")" ) ")" ")" ) "," (Set "(" ($#k4_card_1 :::"succ"::: ) (Set "(" ($#k5_ami_2 :::"IC"::: ) (Set (Var "s")) ")" ) ")" ) ")" )) ")" & "(" (Bool (Bool "ex" (Set (Var "mk")) "," (Set (Var "ml")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k2_ami_2 :::"SCM-Data-Loc"::: ) ) "st" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Num 5) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "mk")) "," (Set (Var "ml")) ($#k10_finseq_1 :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) )))) "implies" (Bool (Set ($#k8_ami_2 :::"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 "(" (Set (Var "x")) ($#k4_scm_inst :::"address_1"::: ) ")" ) "," (Set "(" (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "x")) ($#k4_scm_inst :::"address_1"::: ) ")" ) ")" ) ($#k5_int_1 :::"div"::: ) (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "x")) ($#k5_scm_inst :::"address_2"::: ) ")" ) ")" ) ")" ) ")" ")" ) "," (Set "(" (Set (Var "x")) ($#k5_scm_inst :::"address_2"::: ) ")" ) "," (Set "(" (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "x")) ($#k4_scm_inst :::"address_1"::: ) ")" ) ")" ) ($#k6_int_1 :::"mod"::: ) (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "x")) ($#k5_scm_inst :::"address_2"::: ) ")" ) ")" ) ")" ) ")" ")" ) "," (Set "(" ($#k4_card_1 :::"succ"::: ) (Set "(" ($#k5_ami_2 :::"IC"::: ) (Set (Var "s")) ")" ) ")" ) ")" )) ")" & "(" (Bool (Bool "ex" (Set (Var "mk")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Num 6) "," (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "mk")) ($#k9_finseq_1 :::"*>"::: ) ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k3_xtuple_0 :::"]"::: ) )))) "implies" (Bool (Set ($#k8_ami_2 :::"SCM-Exec-Res"::: ) "(" (Set (Var "x")) "," (Set (Var "s")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_ami_2 :::"SCM-Chg"::: ) "(" (Set (Var "s")) "," (Set "(" (Set (Var "x")) ($#k6_scm_inst :::"jump_address"::: ) ")" ) ")" )) ")" & "(" (Bool (Bool "ex" (Set (Var "mk")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) )(Bool "ex" (Set (Var "ml")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k2_ami_2 :::"SCM-Data-Loc"::: ) ) "st" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Num 7) "," (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "mk")) ($#k9_finseq_1 :::"*>"::: ) ) "," (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "ml")) ($#k12_finseq_1 :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) ))))) "implies" (Bool (Set ($#k8_ami_2 :::"SCM-Exec-Res"::: ) "(" (Set (Var "x")) "," (Set (Var "s")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_ami_2 :::"SCM-Chg"::: ) "(" (Set (Var "s")) "," (Set "(" ($#k15_funcop_1 :::"IFEQ"::: ) "(" (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "x")) ($#k8_scm_inst :::"cond_address"::: ) ")" ) ")" ) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set "(" (Set (Var "x")) ($#k7_scm_inst :::"cjump_address"::: ) ")" ) "," (Set "(" ($#k4_card_1 :::"succ"::: ) (Set "(" ($#k5_ami_2 :::"IC"::: ) (Set (Var "s")) ")" ) ")" ) ")" ")" ) ")" )) ")" & "(" (Bool (Bool "ex" (Set (Var "mk")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) )(Bool "ex" (Set (Var "ml")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k2_ami_2 :::"SCM-Data-Loc"::: ) ) "st" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Num 8) "," (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "mk")) ($#k9_finseq_1 :::"*>"::: ) ) "," (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "ml")) ($#k12_finseq_1 :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) ))))) "implies" (Bool (Set ($#k8_ami_2 :::"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 "(" (Set (Var "x")) ($#k8_scm_inst :::"cond_address"::: ) ")" ) ")" ) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set "(" (Set (Var "x")) ($#k7_scm_inst :::"cjump_address"::: ) ")" ) "," (Set "(" ($#k4_card_1 :::"succ"::: ) (Set "(" ($#k5_ami_2 :::"IC"::: ) (Set (Var "s")) ")" ) ")" ) ")" ")" ) ")" )) ")" & "(" (Bool (Bool "(" "for" (Set (Var "mk")) "," (Set (Var "ml")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k2_ami_2 :::"SCM-Data-Loc"::: ) ) "holds" (Bool (Bool "not" (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Num 1) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "mk")) "," (Set (Var "ml")) ($#k10_finseq_1 :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) ))) ")" ) & (Bool "(" "for" (Set (Var "mk")) "," (Set (Var "ml")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k2_ami_2 :::"SCM-Data-Loc"::: ) ) "holds" (Bool (Bool "not" (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Num 2) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "mk")) "," (Set (Var "ml")) ($#k10_finseq_1 :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) ))) ")" ) & (Bool "(" "for" (Set (Var "mk")) "," (Set (Var "ml")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k2_ami_2 :::"SCM-Data-Loc"::: ) ) "holds" (Bool (Bool "not" (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Num 3) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "mk")) "," (Set (Var "ml")) ($#k10_finseq_1 :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) ))) ")" ) & (Bool "(" "for" (Set (Var "mk")) "," (Set (Var "ml")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k2_ami_2 :::"SCM-Data-Loc"::: ) ) "holds" (Bool (Bool "not" (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Num 4) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "mk")) "," (Set (Var "ml")) ($#k10_finseq_1 :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) ))) ")" ) & (Bool "(" "for" (Set (Var "mk")) "," (Set (Var "ml")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k2_ami_2 :::"SCM-Data-Loc"::: ) ) "holds" (Bool (Bool "not" (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Num 5) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "mk")) "," (Set (Var "ml")) ($#k10_finseq_1 :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) ))) ")" ) & (Bool "(" "for" (Set (Var "mk")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Bool "not" (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Num 6) "," (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "mk")) ($#k9_finseq_1 :::"*>"::: ) ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k3_xtuple_0 :::"]"::: ) ))) ")" ) & (Bool "(" "for" (Set (Var "mk")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "ml")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k2_ami_2 :::"SCM-Data-Loc"::: ) ) "holds" (Bool (Bool "not" (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Num 7) "," (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "mk")) ($#k9_finseq_1 :::"*>"::: ) ) "," (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "ml")) ($#k12_finseq_1 :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) )))) ")" ) & (Bool "(" "for" (Set (Var "mk")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "ml")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k2_ami_2 :::"SCM-Data-Loc"::: ) ) "holds" (Bool (Bool "not" (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Num 8) "," (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "mk")) ($#k9_finseq_1 :::"*>"::: ) ) "," (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "ml")) ($#k12_finseq_1 :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) )))) ")" )) "implies" (Bool (Set ($#k8_ami_2 :::"SCM-Exec-Res"::: ) "(" (Set (Var "x")) "," (Set (Var "s")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "s"))) ")" ")" ))); definitionfunc :::"SCM-Exec"::: -> ($#m1_subset_1 :::"Action":::) "of" (Set ($#k3_scm_inst :::"SCM-Instr"::: ) ) "," (Set "(" ($#k4_card_3 :::"product"::: ) (Set "(" (Set ($#k4_ami_2 :::"SCM-VAL"::: ) ) ($#k3_relat_1 :::"*"::: ) (Set ($#k3_ami_2 :::"SCM-OK"::: ) ) ")" ) ")" ) means :: AMI_2:def 15 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_scm_inst :::"SCM-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 ($#k8_ami_2 :::"SCM-Exec-Res"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" )))); end; :: deftheorem defines :::"SCM-Exec"::: AMI_2:def 15 : (Bool "for" (Set (Var "b1")) "being" ($#m1_subset_1 :::"Action":::) "of" (Set ($#k3_scm_inst :::"SCM-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 ($#k9_ami_2 :::"SCM-Exec"::: ) )) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_scm_inst :::"SCM-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 ($#k8_ami_2 :::"SCM-Exec-Res"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" )))) ")" )); begin theorem :: AMI_2:17 canceled; theorem :: AMI_2:18 canceled; theorem :: AMI_2:19 canceled; theorem :: AMI_2:20 (Bool (Bool "not" (Set ($#k5_numbers :::"NAT"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_ami_2 :::"SCM-Data-Loc"::: ) ))) ; theorem :: AMI_2:21 canceled; theorem :: AMI_2:22 (Bool (Set ($#k5_numbers :::"NAT"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k1_ami_2 :::"SCM-Memory"::: ) )) ; theorem :: AMI_2:23 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_ami_2 :::"SCM-Data-Loc"::: ) ))) "holds" (Bool "ex" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Num 1) "," (Set (Var "k")) ($#k4_tarski :::"]"::: ) )))) ; theorem :: AMI_2:24 (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k4_tarski :::"["::: ) (Num 1) "," (Set (Var "k")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_ami_2 :::"SCM-Data-Loc"::: ) ))) ; theorem :: AMI_2:25 canceled; theorem :: AMI_2:26 (Bool "for" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_ami_2 :::"SCM-Memory"::: ) ) "holds" (Bool "(" (Bool (Set (Var "k")) ($#r1_hidden :::"="::: ) (Set ($#k5_numbers :::"NAT"::: ) )) "or" (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k2_ami_2 :::"SCM-Data-Loc"::: ) )) ")" )) ; theorem :: AMI_2:27 (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" (Set ($#k4_ami_2 :::"SCM-VAL"::: ) ) ($#k3_relat_1 :::"*"::: ) (Set ($#k3_ami_2 :::"SCM-OK"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_ami_2 :::"SCM-Memory"::: ) )) ; theorem :: AMI_2:28 (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"SCM-State":::) "holds" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set ($#k1_ami_2 :::"SCM-Memory"::: ) ))) ; definitionlet "x" be ($#m1_hidden :::"set"::: ) ; attr "x" is :::"Int-like"::: means :: AMI_2:def 16 (Bool "x" ($#r2_hidden :::"in"::: ) (Set ($#k2_ami_2 :::"SCM-Data-Loc"::: ) )); end; :: deftheorem defines :::"Int-like"::: AMI_2:def 16 : (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) "is" ($#v1_ami_2 :::"Int-like"::: ) ) "iff" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_ami_2 :::"SCM-Data-Loc"::: ) )) ")" ));