:: SCMRING1 semantic presentation begin definitioncanceled; canceled; let "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_struct_0 :::"1-sorted"::: ) ; func :::"SCM-VAL"::: "S" -> ($#m1_hidden :::"ManySortedSet":::) "of" (Num 2) equals :: SCMRING1:def 3 (Set ($#k6_afinsq_1 :::"<%"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "S") ($#k6_afinsq_1 :::"%>"::: ) ); end; :: deftheorem SCMRING1:def 1 : canceled; :: deftheorem SCMRING1:def 2 : canceled; :: deftheorem defines :::"SCM-VAL"::: SCMRING1:def 3 : (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_struct_0 :::"1-sorted"::: ) "holds" (Bool (Set ($#k1_scmring1 :::"SCM-VAL"::: ) (Set (Var "S"))) ($#r1_hidden :::"="::: ) (Set ($#k6_afinsq_1 :::"<%"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) ($#k6_afinsq_1 :::"%>"::: ) ))); theorem :: SCMRING1:1 canceled; theorem :: SCMRING1:2 (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_struct_0 :::"1-sorted"::: ) "holds" (Bool (Set (Set "(" (Set "(" ($#k1_scmring1 :::"SCM-VAL"::: ) (Set (Var "G")) ")" ) ($#k3_relat_1 :::"*"::: ) (Set ($#k3_ami_2 :::"SCM-OK"::: ) ) ")" ) ($#k1_funct_1 :::"."::: ) (Set ($#k5_numbers :::"NAT"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k5_numbers :::"NAT"::: ) ))) ; theorem :: SCMRING1:3 (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_struct_0 :::"1-sorted"::: ) (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 "(" ($#k1_scmring1 :::"SCM-VAL"::: ) (Set (Var "G")) ")" ) ($#k3_relat_1 :::"*"::: ) (Set ($#k3_ami_2 :::"SCM-OK"::: ) ) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G")))))) ; registrationlet "G" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_struct_0 :::"1-sorted"::: ) ; cluster (Set (Set ($#k3_ami_2 :::"SCM-OK"::: ) ) ($#k3_relat_1 :::"*"::: ) (Set "(" ($#k1_scmring1 :::"SCM-VAL"::: ) "G" ")" )) -> ($#v2_relat_1 :::"non-empty"::: ) ; end; definitionlet "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_struct_0 :::"1-sorted"::: ) ; mode SCM-State of "S" is ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_card_3 :::"product"::: ) (Set "(" (Set "(" ($#k1_scmring1 :::"SCM-VAL"::: ) "S" ")" ) ($#k3_relat_1 :::"*"::: ) (Set ($#k3_ami_2 :::"SCM-OK"::: ) ) ")" )); end; theorem :: SCMRING1:4 (Bool "for" (Set (Var "d1")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k2_ami_2 :::"SCM-Data-Loc"::: ) ) (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_struct_0 :::"1-sorted"::: ) "holds" (Bool (Set (Set "(" (Set "(" ($#k1_scmring1 :::"SCM-VAL"::: ) (Set (Var "G")) ")" ) ($#k3_relat_1 :::"*"::: ) (Set ($#k3_ami_2 :::"SCM-OK"::: ) ) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "d1"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G")))))) ; theorem :: SCMRING1:5 (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_struct_0 :::"1-sorted"::: ) "holds" (Bool (Set ($#k5_card_3 :::"pi"::: ) "(" (Set "(" ($#k4_card_3 :::"product"::: ) (Set "(" (Set "(" ($#k1_scmring1 :::"SCM-VAL"::: ) (Set (Var "G")) ")" ) ($#k3_relat_1 :::"*"::: ) (Set ($#k3_ami_2 :::"SCM-OK"::: ) ) ")" ) ")" ) "," (Set ($#k5_numbers :::"NAT"::: ) ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k5_numbers :::"NAT"::: ) ))) ; theorem :: SCMRING1:6 (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_struct_0 :::"1-sorted"::: ) (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 "(" ($#k1_scmring1 :::"SCM-VAL"::: ) (Set (Var "G")) ")" ) ($#k3_relat_1 :::"*"::: ) (Set ($#k3_ami_2 :::"SCM-OK"::: ) ) ")" ) ")" ) "," (Set (Var "a")) ")" ) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G")))))) ; definitionlet "G" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_struct_0 :::"1-sorted"::: ) ; let "s" be ($#m1_subset_1 :::"SCM-State":::) "of" (Set (Const "G")); func :::"IC"::: "s" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) equals :: SCMRING1:def 4 (Set "s" ($#k1_funct_1 :::"."::: ) (Set ($#k5_numbers :::"NAT"::: ) )); end; :: deftheorem defines :::"IC"::: SCMRING1:def 4 : (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_struct_0 :::"1-sorted"::: ) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"SCM-State":::) "of" (Set (Var "G")) "holds" (Bool (Set ($#k2_scmring1 :::"IC"::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set ($#k5_numbers :::"NAT"::: ) ))))); definitionlet "R" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_struct_0 :::"1-sorted"::: ) ; let "s" be ($#m1_subset_1 :::"SCM-State":::) "of" (Set (Const "R")); let "u" be ($#m1_hidden :::"Nat":::); func :::"SCM-Chg"::: "(" "s" "," "u" ")" -> ($#m1_subset_1 :::"SCM-State":::) "of" "R" equals :: SCMRING1:def 5 (Set "s" ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set ($#k5_numbers :::"NAT"::: ) ) ($#k16_funcop_1 :::".-->"::: ) "u" ")" )); end; :: deftheorem defines :::"SCM-Chg"::: SCMRING1:def 5 : (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_struct_0 :::"1-sorted"::: ) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"SCM-State":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "u")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k3_scmring1 :::"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 :: SCMRING1:7 (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_struct_0 :::"1-sorted"::: ) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"SCM-State":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "u")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set "(" ($#k3_scmring1 :::"SCM-Chg"::: ) "(" (Set (Var "s")) "," (Set (Var "u")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set ($#k5_numbers :::"NAT"::: ) )) ($#r1_hidden :::"="::: ) (Set (Var "u")))))) ; theorem :: SCMRING1:8 (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_struct_0 :::"1-sorted"::: ) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"SCM-State":::) "of" (Set (Var "G")) (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 "(" ($#k3_scmring1 :::"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 :: SCMRING1:9 (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_struct_0 :::"1-sorted"::: ) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"SCM-State":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "u")) "," (Set (Var "v")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set "(" ($#k3_scmring1 :::"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 "R" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_struct_0 :::"1-sorted"::: ) ; let "s" be ($#m1_subset_1 :::"SCM-State":::) "of" (Set (Const "R")); let "t" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k2_ami_2 :::"SCM-Data-Loc"::: ) ); let "u" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "R")); func :::"SCM-Chg"::: "(" "s" "," "t" "," "u" ")" -> ($#m1_subset_1 :::"SCM-State":::) "of" "R" equals :: SCMRING1:def 6 (Set "s" ($#k1_funct_4 :::"+*"::: ) (Set "(" "t" ($#k16_funcop_1 :::".-->"::: ) "u" ")" )); end; :: deftheorem defines :::"SCM-Chg"::: SCMRING1:def 6 : (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_struct_0 :::"1-sorted"::: ) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"SCM-State":::) "of" (Set (Var "R")) (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_subset_1 :::"Element":::) "of" (Set (Var "R")) "holds" (Bool (Set ($#k4_scmring1 :::"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 :: SCMRING1:10 (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_struct_0 :::"1-sorted"::: ) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"SCM-State":::) "of" (Set (Var "G")) (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_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool (Set (Set "(" ($#k4_scmring1 :::"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 :: SCMRING1:11 (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_struct_0 :::"1-sorted"::: ) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"SCM-State":::) "of" (Set (Var "G")) (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_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool (Set (Set "(" ($#k4_scmring1 :::"SCM-Chg"::: ) "(" (Set (Var "s")) "," (Set (Var "t")) "," (Set (Var "u")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "t"))) ($#r1_hidden :::"="::: ) (Set (Var "u"))))))) ; theorem :: SCMRING1:12 (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_struct_0 :::"1-sorted"::: ) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"SCM-State":::) "of" (Set (Var "G")) (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_subset_1 :::"Element":::) "of" (Set (Var "G")) (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 "(" ($#k4_scmring1 :::"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"))))))))) ; definitionlet "R" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_struct_0 :::"1-sorted"::: ) ; let "s" be ($#m1_subset_1 :::"SCM-State":::) "of" (Set (Const "R")); let "a" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k2_ami_2 :::"SCM-Data-Loc"::: ) ); :: original: :::"."::: redefine func "s" :::"."::: "a" -> ($#m1_subset_1 :::"Element":::) "of" "R"; end; definitionlet "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_struct_0 :::"1-sorted"::: ) ; let "d" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k2_ami_2 :::"SCM-Data-Loc"::: ) ); let "s" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "S")); :: original: :::"<*"::: redefine func :::"<*":::"d" "," "s":::"*>"::: -> ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Set ($#k2_ami_2 :::"SCM-Data-Loc"::: ) ) ($#k2_xboole_0 :::"\/"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "S")); end; definitioncanceled; canceled; canceled; canceled; canceled; canceled; canceled; let "R" be ($#l6_algstr_0 :::"Ring":::); let "x" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_scmringi :::"SCM-Instr"::: ) (Set (Const "R"))); let "s" be ($#m1_subset_1 :::"SCM-State":::) "of" (Set (Const "R")); func :::"SCM-Exec-Res"::: "(" "x" "," "s" ")" -> ($#m1_subset_1 :::"SCM-State":::) "of" "R" equals :: SCMRING1:def 14 (Set ($#k3_scmring1 :::"SCM-Chg"::: ) "(" (Set "(" ($#k4_scmring1 :::"SCM-Chg"::: ) "(" "s" "," (Set "(" "x" ($#k2_scmringi :::"address_1"::: ) ")" ) "," (Set "(" "s" ($#k5_scmring1 :::"."::: ) (Set "(" "x" ($#k3_scmringi :::"address_2"::: ) ")" ) ")" ) ")" ")" ) "," (Set "(" ($#k1_ordinal1 :::"succ"::: ) (Set "(" ($#k2_scmring1 :::"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 ($#k3_scmring1 :::"SCM-Chg"::: ) "(" (Set "(" ($#k4_scmring1 :::"SCM-Chg"::: ) "(" "s" "," (Set "(" "x" ($#k2_scmringi :::"address_1"::: ) ")" ) "," (Set "(" (Set "(" "s" ($#k5_scmring1 :::"."::: ) (Set "(" "x" ($#k2_scmringi :::"address_1"::: ) ")" ) ")" ) ($#k1_algstr_0 :::"+"::: ) (Set "(" "s" ($#k5_scmring1 :::"."::: ) (Set "(" "x" ($#k3_scmringi :::"address_2"::: ) ")" ) ")" ) ")" ) ")" ")" ) "," (Set "(" ($#k1_ordinal1 :::"succ"::: ) (Set "(" ($#k2_scmring1 :::"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 ($#k3_scmring1 :::"SCM-Chg"::: ) "(" (Set "(" ($#k4_scmring1 :::"SCM-Chg"::: ) "(" "s" "," (Set "(" "x" ($#k2_scmringi :::"address_1"::: ) ")" ) "," (Set "(" (Set "(" "s" ($#k5_scmring1 :::"."::: ) (Set "(" "x" ($#k2_scmringi :::"address_1"::: ) ")" ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" "s" ($#k5_scmring1 :::"."::: ) (Set "(" "x" ($#k3_scmringi :::"address_2"::: ) ")" ) ")" ) ")" ) ")" ")" ) "," (Set "(" ($#k1_ordinal1 :::"succ"::: ) (Set "(" ($#k2_scmring1 :::"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 ($#k3_scmring1 :::"SCM-Chg"::: ) "(" (Set "(" ($#k4_scmring1 :::"SCM-Chg"::: ) "(" "s" "," (Set "(" "x" ($#k2_scmringi :::"address_1"::: ) ")" ) "," (Set "(" (Set "(" "s" ($#k5_scmring1 :::"."::: ) (Set "(" "x" ($#k2_scmringi :::"address_1"::: ) ")" ) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set "(" "s" ($#k5_scmring1 :::"."::: ) (Set "(" "x" ($#k3_scmringi :::"address_2"::: ) ")" ) ")" ) ")" ) ")" ")" ) "," (Set "(" ($#k1_ordinal1 :::"succ"::: ) (Set "(" ($#k2_scmring1 :::"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 ($#k3_scmring1 :::"SCM-Chg"::: ) "(" "s" "," (Set "(" "x" ($#k4_scmringi :::"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 ($#k12_finseq_1 :::"<*"::: ) (Set (Var "mk")) ($#k12_finseq_1 :::"*>"::: ) ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k3_xtuple_0 :::"]"::: ) ))) (Set ($#k3_scmring1 :::"SCM-Chg"::: ) "(" "s" "," (Set "(" ($#k14_funcop_1 :::"IFEQ"::: ) "(" (Set "(" "s" ($#k5_scmring1 :::"."::: ) (Set "(" "x" ($#k6_scmringi :::"cond_address"::: ) ")" ) ")" ) "," (Set "(" ($#k4_struct_0 :::"0."::: ) "R" ")" ) "," (Set "(" "x" ($#k5_scmringi :::"cjump_address"::: ) ")" ) "," (Set "(" ($#k1_ordinal1 :::"succ"::: ) (Set "(" ($#k2_scmring1 :::"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 ($#k12_finseq_1 :::"<*"::: ) (Set (Var "mk")) ($#k12_finseq_1 :::"*>"::: ) ) "," (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "ml")) ($#k12_finseq_1 :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) )))) (Set ($#k3_scmring1 :::"SCM-Chg"::: ) "(" (Set "(" ($#k4_scmring1 :::"SCM-Chg"::: ) "(" "s" "," (Set "(" "x" ($#k8_scmringi :::"const_address"::: ) ")" ) "," (Set "(" "x" ($#k9_scmringi :::"const_value"::: ) ")" ) ")" ")" ) "," (Set "(" ($#k1_ordinal1 :::"succ"::: ) (Set "(" ($#k2_scmring1 :::"IC"::: ) "s" ")" ) ")" ) ")" ) if (Bool "ex" (Set (Var "mk")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k2_ami_2 :::"SCM-Data-Loc"::: ) )(Bool "ex" (Set (Var "r")) "being" ($#m1_subset_1 :::"Element":::) "of" "R" "st" (Bool "x" ($#r1_hidden :::"="::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Num 5) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k6_scmring1 :::"<*"::: ) (Set (Var "mk")) "," (Set (Var "r")) ($#k6_scmring1 :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) )))) otherwise "s"; end; :: deftheorem SCMRING1:def 7 : canceled; :: deftheorem SCMRING1:def 8 : canceled; :: deftheorem SCMRING1:def 9 : canceled; :: deftheorem SCMRING1:def 10 : canceled; :: deftheorem SCMRING1:def 11 : canceled; :: deftheorem SCMRING1:def 12 : canceled; :: deftheorem SCMRING1:def 13 : canceled; :: deftheorem defines :::"SCM-Exec-Res"::: SCMRING1:def 14 : (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_scmringi :::"SCM-Instr"::: ) (Set (Var "R"))) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"SCM-State":::) "of" (Set (Var "R")) "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 ($#k7_scmring1 :::"SCM-Exec-Res"::: ) "(" (Set (Var "x")) "," (Set (Var "s")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k3_scmring1 :::"SCM-Chg"::: ) "(" (Set "(" ($#k4_scmring1 :::"SCM-Chg"::: ) "(" (Set (Var "s")) "," (Set "(" (Set (Var "x")) ($#k2_scmringi :::"address_1"::: ) ")" ) "," (Set "(" (Set (Var "s")) ($#k5_scmring1 :::"."::: ) (Set "(" (Set (Var "x")) ($#k3_scmringi :::"address_2"::: ) ")" ) ")" ) ")" ")" ) "," (Set "(" ($#k1_ordinal1 :::"succ"::: ) (Set "(" ($#k2_scmring1 :::"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 ($#k7_scmring1 :::"SCM-Exec-Res"::: ) "(" (Set (Var "x")) "," (Set (Var "s")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k3_scmring1 :::"SCM-Chg"::: ) "(" (Set "(" ($#k4_scmring1 :::"SCM-Chg"::: ) "(" (Set (Var "s")) "," (Set "(" (Set (Var "x")) ($#k2_scmringi :::"address_1"::: ) ")" ) "," (Set "(" (Set "(" (Set (Var "s")) ($#k5_scmring1 :::"."::: ) (Set "(" (Set (Var "x")) ($#k2_scmringi :::"address_1"::: ) ")" ) ")" ) ($#k1_algstr_0 :::"+"::: ) (Set "(" (Set (Var "s")) ($#k5_scmring1 :::"."::: ) (Set "(" (Set (Var "x")) ($#k3_scmringi :::"address_2"::: ) ")" ) ")" ) ")" ) ")" ")" ) "," (Set "(" ($#k1_ordinal1 :::"succ"::: ) (Set "(" ($#k2_scmring1 :::"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 ($#k7_scmring1 :::"SCM-Exec-Res"::: ) "(" (Set (Var "x")) "," (Set (Var "s")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k3_scmring1 :::"SCM-Chg"::: ) "(" (Set "(" ($#k4_scmring1 :::"SCM-Chg"::: ) "(" (Set (Var "s")) "," (Set "(" (Set (Var "x")) ($#k2_scmringi :::"address_1"::: ) ")" ) "," (Set "(" (Set "(" (Set (Var "s")) ($#k5_scmring1 :::"."::: ) (Set "(" (Set (Var "x")) ($#k2_scmringi :::"address_1"::: ) ")" ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set (Var "s")) ($#k5_scmring1 :::"."::: ) (Set "(" (Set (Var "x")) ($#k3_scmringi :::"address_2"::: ) ")" ) ")" ) ")" ) ")" ")" ) "," (Set "(" ($#k1_ordinal1 :::"succ"::: ) (Set "(" ($#k2_scmring1 :::"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 ($#k7_scmring1 :::"SCM-Exec-Res"::: ) "(" (Set (Var "x")) "," (Set (Var "s")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k3_scmring1 :::"SCM-Chg"::: ) "(" (Set "(" ($#k4_scmring1 :::"SCM-Chg"::: ) "(" (Set (Var "s")) "," (Set "(" (Set (Var "x")) ($#k2_scmringi :::"address_1"::: ) ")" ) "," (Set "(" (Set "(" (Set (Var "s")) ($#k5_scmring1 :::"."::: ) (Set "(" (Set (Var "x")) ($#k2_scmringi :::"address_1"::: ) ")" ) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set "(" (Set (Var "s")) ($#k5_scmring1 :::"."::: ) (Set "(" (Set (Var "x")) ($#k3_scmringi :::"address_2"::: ) ")" ) ")" ) ")" ) ")" ")" ) "," (Set "(" ($#k1_ordinal1 :::"succ"::: ) (Set "(" ($#k2_scmring1 :::"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 ($#k12_finseq_1 :::"<*"::: ) (Set (Var "mk")) ($#k12_finseq_1 :::"*>"::: ) ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k3_xtuple_0 :::"]"::: ) )))) "implies" (Bool (Set ($#k7_scmring1 :::"SCM-Exec-Res"::: ) "(" (Set (Var "x")) "," (Set (Var "s")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k3_scmring1 :::"SCM-Chg"::: ) "(" (Set (Var "s")) "," (Set "(" (Set (Var "x")) ($#k4_scmringi :::"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 ($#k12_finseq_1 :::"<*"::: ) (Set (Var "mk")) ($#k12_finseq_1 :::"*>"::: ) ) "," (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "ml")) ($#k12_finseq_1 :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) ))))) "implies" (Bool (Set ($#k7_scmring1 :::"SCM-Exec-Res"::: ) "(" (Set (Var "x")) "," (Set (Var "s")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k3_scmring1 :::"SCM-Chg"::: ) "(" (Set (Var "s")) "," (Set "(" ($#k14_funcop_1 :::"IFEQ"::: ) "(" (Set "(" (Set (Var "s")) ($#k5_scmring1 :::"."::: ) (Set "(" (Set (Var "x")) ($#k6_scmringi :::"cond_address"::: ) ")" ) ")" ) "," (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "R")) ")" ) "," (Set "(" (Set (Var "x")) ($#k5_scmringi :::"cjump_address"::: ) ")" ) "," (Set "(" ($#k1_ordinal1 :::"succ"::: ) (Set "(" ($#k2_scmring1 :::"IC"::: ) (Set (Var "s")) ")" ) ")" ) ")" ")" ) ")" )) ")" & "(" (Bool (Bool "ex" (Set (Var "mk")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k2_ami_2 :::"SCM-Data-Loc"::: ) )(Bool "ex" (Set (Var "r")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) "st" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Num 5) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k6_scmring1 :::"<*"::: ) (Set (Var "mk")) "," (Set (Var "r")) ($#k6_scmring1 :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) ))))) "implies" (Bool (Set ($#k7_scmring1 :::"SCM-Exec-Res"::: ) "(" (Set (Var "x")) "," (Set (Var "s")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k3_scmring1 :::"SCM-Chg"::: ) "(" (Set "(" ($#k4_scmring1 :::"SCM-Chg"::: ) "(" (Set (Var "s")) "," (Set "(" (Set (Var "x")) ($#k8_scmringi :::"const_address"::: ) ")" ) "," (Set "(" (Set (Var "x")) ($#k9_scmringi :::"const_value"::: ) ")" ) ")" ")" ) "," (Set "(" ($#k1_ordinal1 :::"succ"::: ) (Set "(" ($#k2_scmring1 :::"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")) "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 ($#k12_finseq_1 :::"<*"::: ) (Set (Var "mk")) ($#k12_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 ($#k12_finseq_1 :::"<*"::: ) (Set (Var "mk")) ($#k12_finseq_1 :::"*>"::: ) ) "," (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "ml")) ($#k12_finseq_1 :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) )))) ")" ) & (Bool "(" "for" (Set (Var "mk")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k2_ami_2 :::"SCM-Data-Loc"::: ) ) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) "holds" (Bool (Bool "not" (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Num 5) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k6_scmring1 :::"<*"::: ) (Set (Var "mk")) "," (Set (Var "r")) ($#k6_scmring1 :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) )))) ")" )) "implies" (Bool (Set ($#k7_scmring1 :::"SCM-Exec-Res"::: ) "(" (Set (Var "x")) "," (Set (Var "s")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "s"))) ")" ")" )))); definitionlet "R" be ($#l6_algstr_0 :::"Ring":::); func :::"SCM-Exec"::: "R" -> ($#m1_subset_1 :::"Action":::) "of" (Set "(" ($#k1_scmringi :::"SCM-Instr"::: ) "R" ")" ) "," (Set "(" ($#k4_card_3 :::"product"::: ) (Set "(" (Set "(" ($#k1_scmring1 :::"SCM-VAL"::: ) "R" ")" ) ($#k3_relat_1 :::"*"::: ) (Set ($#k3_ami_2 :::"SCM-OK"::: ) ) ")" ) ")" ) means :: SCMRING1:def 15 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_scmringi :::"SCM-Instr"::: ) "R") (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"SCM-State":::) "of" "R" "holds" (Bool (Set (Set "(" it ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set ($#k7_scmring1 :::"SCM-Exec-Res"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" )))); end; :: deftheorem defines :::"SCM-Exec"::: SCMRING1:def 15 : (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"Action":::) "of" (Set "(" ($#k1_scmringi :::"SCM-Instr"::: ) (Set (Var "R")) ")" ) "," (Set "(" ($#k4_card_3 :::"product"::: ) (Set "(" (Set "(" ($#k1_scmring1 :::"SCM-VAL"::: ) (Set (Var "R")) ")" ) ($#k3_relat_1 :::"*"::: ) (Set ($#k3_ami_2 :::"SCM-OK"::: ) ) ")" ) ")" ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k8_scmring1 :::"SCM-Exec"::: ) (Set (Var "R")))) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_scmringi :::"SCM-Instr"::: ) (Set (Var "R"))) (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"SCM-State":::) "of" (Set (Var "R")) "holds" (Bool (Set (Set "(" (Set (Var "b2")) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set ($#k7_scmring1 :::"SCM-Exec-Res"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" )))) ")" ))); theorem :: SCMRING1:13 canceled; theorem :: SCMRING1:14 canceled; theorem :: SCMRING1:15 canceled; theorem :: SCMRING1:16 canceled; theorem :: SCMRING1:17 canceled; theorem :: SCMRING1:18 canceled; theorem :: SCMRING1:19 (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_struct_0 :::"1-sorted"::: ) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"SCM-State":::) "of" (Set (Var "S")) "holds" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set ($#k1_ami_2 :::"SCM-Memory"::: ) )))) ;