:: SCMRING2 semantic presentation begin definitionlet "R" be ($#l6_algstr_0 :::"Ring":::); func :::"SCM"::: "R" -> ($#v1_extpro_1 :::"strict"::: ) ($#l1_extpro_1 :::"AMI-Struct"::: ) "over" (Num 2) means :: SCMRING2:def 1 (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set ($#k1_ami_2 :::"SCM-Memory"::: ) )) & (Bool (Set "the" ($#u2_struct_0 :::"ZeroF"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set ($#k5_numbers :::"NAT"::: ) )) & (Bool (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set ($#k1_scmringi :::"SCM-Instr"::: ) "R")) & (Bool (Set "the" ($#u1_memstr_0 :::"Object-Kind"::: ) "of" it) ($#r1_funct_2 :::"="::: ) (Set ($#k3_ami_2 :::"SCM-OK"::: ) )) & (Bool (Set "the" ($#u2_memstr_0 :::"ValuesF"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set ($#k1_scmring1 :::"SCM-VAL"::: ) "R")) & (Bool (Set "the" ($#u1_extpro_1 :::"Execution"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set ($#k8_scmring1 :::"SCM-Exec"::: ) "R")) ")" ); end; :: deftheorem defines :::"SCM"::: SCMRING2:def 1 : (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "b2")) "being" ($#v1_extpro_1 :::"strict"::: ) ($#l1_extpro_1 :::"AMI-Struct"::: ) "over" (Num 2) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k1_scmring2 :::"SCM"::: ) (Set (Var "R")))) "iff" (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set ($#k1_ami_2 :::"SCM-Memory"::: ) )) & (Bool (Set "the" ($#u2_struct_0 :::"ZeroF"::: ) "of" (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set ($#k5_numbers :::"NAT"::: ) )) & (Bool (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set ($#k1_scmringi :::"SCM-Instr"::: ) (Set (Var "R")))) & (Bool (Set "the" ($#u1_memstr_0 :::"Object-Kind"::: ) "of" (Set (Var "b2"))) ($#r1_funct_2 :::"="::: ) (Set ($#k3_ami_2 :::"SCM-OK"::: ) )) & (Bool (Set "the" ($#u2_memstr_0 :::"ValuesF"::: ) "of" (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set ($#k1_scmring1 :::"SCM-VAL"::: ) (Set (Var "R")))) & (Bool (Set "the" ($#u1_extpro_1 :::"Execution"::: ) "of" (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set ($#k8_scmring1 :::"SCM-Exec"::: ) (Set (Var "R")))) ")" ) ")" ))); registrationlet "R" be ($#l6_algstr_0 :::"Ring":::); cluster (Set ($#k1_scmring2 :::"SCM"::: ) "R") -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_extpro_1 :::"strict"::: ) ; end; registrationlet "R" be ($#l6_algstr_0 :::"Ring":::); cluster (Set ($#k1_scmring2 :::"SCM"::: ) "R") -> ($#v2_memstr_0 :::"with_non-empty_values"::: ) ($#v1_extpro_1 :::"strict"::: ) ; end; registrationlet "R" be ($#l6_algstr_0 :::"Ring":::); cluster ($#v1_ami_2 :::"Int-like"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k1_scmring2 :::"SCM"::: ) "R" ")" )); end; definitionlet "R" be ($#l6_algstr_0 :::"Ring":::); mode Data-Location of "R" is ($#v1_ami_2 :::"Int-like"::: ) ($#m1_subset_1 :::"Object":::) "of" (Set "(" ($#k1_scmring2 :::"SCM"::: ) "R" ")" ); canceled; end; :: deftheorem SCMRING2:def 2 : canceled; theorem :: SCMRING2:1 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"Ring":::) "holds" (Bool "(" (Bool (Set (Var "x")) "is" ($#m1_subset_1 :::"Data-Location":::) "of" (Set (Var "R"))) "iff" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k8_struct_0 :::"Data-Locations"::: ) )) ")" ))) ; definitionlet "R" be ($#l6_algstr_0 :::"Ring":::); let "s" be ($#m1_hidden :::"State":::) "of" (Set "(" ($#k1_scmring2 :::"SCM"::: ) (Set (Const "R")) ")" ); let "a" be ($#m1_subset_1 :::"Data-Location":::) "of" (Set (Const "R")); :: original: :::"."::: redefine func "s" :::"."::: "a" -> ($#m1_subset_1 :::"Element":::) "of" "R"; end; theorem :: SCMRING2:2 (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"Ring":::) "holds" (Bool (Set ($#k3_xtuple_0 :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k3_xtuple_0 :::"]"::: ) ) "is" ($#m1_subset_1 :::"Instruction":::) "of" (Set "(" ($#k1_scmring2 :::"SCM"::: ) (Set (Var "R")) ")" ))) ; theorem :: SCMRING2:3 (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_struct_0 :::"1-sorted"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "d1")) "," (Set (Var "d2")) "being" ($#m1_subset_1 :::"Data-Location":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_domain_1 :::"{"::: ) (Num 1) "," (Num 2) "," (Num 3) "," (Num 4) ($#k9_domain_1 :::"}"::: ) ))) "holds" (Bool (Set ($#k3_xtuple_0 :::"["::: ) (Set (Var "x")) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "d1")) "," (Set (Var "d2")) ($#k10_finseq_1 :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k1_scmringi :::"SCM-Instr"::: ) (Set (Var "S")))))))) ; theorem :: SCMRING2:4 (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_struct_0 :::"1-sorted"::: ) (Bool "for" (Set (Var "t")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "d1")) "being" ($#m1_subset_1 :::"Data-Location":::) "of" (Set (Var "R")) "holds" (Bool (Set ($#k3_xtuple_0 :::"["::: ) (Num 5) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "d1")) "," (Set (Var "t")) ($#k10_finseq_1 :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k1_scmringi :::"SCM-Instr"::: ) (Set (Var "S")))))))) ; theorem :: SCMRING2:5 (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_struct_0 :::"1-sorted"::: ) (Bool "for" (Set (Var "i1")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k3_xtuple_0 :::"["::: ) (Num 6) "," (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "i1")) ($#k12_finseq_1 :::"*>"::: ) ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k3_xtuple_0 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k1_scmringi :::"SCM-Instr"::: ) (Set (Var "S")))))) ; theorem :: SCMRING2:6 (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_struct_0 :::"1-sorted"::: ) (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "d1")) "being" ($#m1_subset_1 :::"Data-Location":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "i1")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k3_xtuple_0 :::"["::: ) (Num 7) "," (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "i1")) ($#k12_finseq_1 :::"*>"::: ) ) "," (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "d1")) ($#k12_finseq_1 :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k1_scmringi :::"SCM-Instr"::: ) (Set (Var "S")))))))) ; definitionlet "R" be ($#l6_algstr_0 :::"Ring":::); let "a", "b" be ($#m1_subset_1 :::"Data-Location":::) "of" (Set (Const "R")); func "a" :::":="::: "b" -> ($#m1_subset_1 :::"Instruction":::) "of" (Set "(" ($#k1_scmring2 :::"SCM"::: ) "R" ")" ) equals :: SCMRING2:def 3 (Set ($#k3_xtuple_0 :::"["::: ) (Num 1) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k10_finseq_1 :::"<*"::: ) "a" "," "b" ($#k10_finseq_1 :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) ); func :::"AddTo"::: "(" "a" "," "b" ")" -> ($#m1_subset_1 :::"Instruction":::) "of" (Set "(" ($#k1_scmring2 :::"SCM"::: ) "R" ")" ) equals :: SCMRING2:def 4 (Set ($#k3_xtuple_0 :::"["::: ) (Num 2) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k10_finseq_1 :::"<*"::: ) "a" "," "b" ($#k10_finseq_1 :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) ); func :::"SubFrom"::: "(" "a" "," "b" ")" -> ($#m1_subset_1 :::"Instruction":::) "of" (Set "(" ($#k1_scmring2 :::"SCM"::: ) "R" ")" ) equals :: SCMRING2:def 5 (Set ($#k3_xtuple_0 :::"["::: ) (Num 3) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k10_finseq_1 :::"<*"::: ) "a" "," "b" ($#k10_finseq_1 :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) ); func :::"MultBy"::: "(" "a" "," "b" ")" -> ($#m1_subset_1 :::"Instruction":::) "of" (Set "(" ($#k1_scmring2 :::"SCM"::: ) "R" ")" ) equals :: SCMRING2:def 6 (Set ($#k3_xtuple_0 :::"["::: ) (Num 4) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k10_finseq_1 :::"<*"::: ) "a" "," "b" ($#k10_finseq_1 :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) ); end; :: deftheorem defines :::":="::: SCMRING2:def 3 : (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Data-Location":::) "of" (Set (Var "R")) "holds" (Bool (Set (Set (Var "a")) ($#k3_scmring2 :::":="::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Num 1) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k10_finseq_1 :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) )))); :: deftheorem defines :::"AddTo"::: SCMRING2:def 4 : (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Data-Location":::) "of" (Set (Var "R")) "holds" (Bool (Set ($#k4_scmring2 :::"AddTo"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Num 2) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k10_finseq_1 :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) )))); :: deftheorem defines :::"SubFrom"::: SCMRING2:def 5 : (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Data-Location":::) "of" (Set (Var "R")) "holds" (Bool (Set ($#k5_scmring2 :::"SubFrom"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Num 3) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k10_finseq_1 :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) )))); :: deftheorem defines :::"MultBy"::: SCMRING2:def 6 : (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Data-Location":::) "of" (Set (Var "R")) "holds" (Bool (Set ($#k6_scmring2 :::"MultBy"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Num 4) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k10_finseq_1 :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) )))); definitionlet "R" be ($#l6_algstr_0 :::"Ring":::); let "a" be ($#m1_subset_1 :::"Data-Location":::) "of" (Set (Const "R")); let "r" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "R")); func "a" :::":="::: "r" -> ($#m1_subset_1 :::"Instruction":::) "of" (Set "(" ($#k1_scmring2 :::"SCM"::: ) "R" ")" ) equals :: SCMRING2:def 7 (Set ($#k3_xtuple_0 :::"["::: ) (Num 5) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k10_finseq_1 :::"<*"::: ) "a" "," "r" ($#k10_finseq_1 :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) ); end; :: deftheorem defines :::":="::: SCMRING2:def 7 : (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Data-Location":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) "holds" (Bool (Set (Set (Var "a")) ($#k7_scmring2 :::":="::: ) (Set (Var "r"))) ($#r1_hidden :::"="::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Num 5) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "a")) "," (Set (Var "r")) ($#k10_finseq_1 :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) ))))); definitionlet "R" be ($#l6_algstr_0 :::"Ring":::); let "l" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); func :::"goto"::: "(" "l" "," "R" ")" -> ($#m1_subset_1 :::"Instruction":::) "of" (Set "(" ($#k1_scmring2 :::"SCM"::: ) "R" ")" ) equals :: SCMRING2:def 8 (Set ($#k3_xtuple_0 :::"["::: ) (Num 6) "," (Set ($#k12_finseq_1 :::"<*"::: ) "l" ($#k12_finseq_1 :::"*>"::: ) ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k3_xtuple_0 :::"]"::: ) ); end; :: deftheorem defines :::"goto"::: SCMRING2:def 8 : (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "l")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k8_scmring2 :::"goto"::: ) "(" (Set (Var "l")) "," (Set (Var "R")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Num 6) "," (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "l")) ($#k12_finseq_1 :::"*>"::: ) ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k3_xtuple_0 :::"]"::: ) )))); definitionlet "R" be ($#l6_algstr_0 :::"Ring":::); let "l" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "a" be ($#m1_subset_1 :::"Data-Location":::) "of" (Set (Const "R")); func "a" :::"=0_goto"::: "l" -> ($#m1_subset_1 :::"Instruction":::) "of" (Set "(" ($#k1_scmring2 :::"SCM"::: ) "R" ")" ) equals :: SCMRING2:def 9 (Set ($#k3_xtuple_0 :::"["::: ) (Num 7) "," (Set ($#k12_finseq_1 :::"<*"::: ) "l" ($#k12_finseq_1 :::"*>"::: ) ) "," (Set ($#k12_finseq_1 :::"<*"::: ) "a" ($#k12_finseq_1 :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) ); end; :: deftheorem defines :::"=0_goto"::: SCMRING2:def 9 : (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "l")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Data-Location":::) "of" (Set (Var "R")) "holds" (Bool (Set (Set (Var "a")) ($#k9_scmring2 :::"=0_goto"::: ) (Set (Var "l"))) ($#r1_hidden :::"="::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Num 7) "," (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "l")) ($#k12_finseq_1 :::"*>"::: ) ) "," (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "a")) ($#k12_finseq_1 :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) ))))); theorem :: SCMRING2:7 (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "I")) "is" ($#m1_subset_1 :::"Instruction":::) "of" (Set "(" ($#k1_scmring2 :::"SCM"::: ) (Set (Var "R")) ")" )) "iff" (Bool "(" (Bool (Set (Var "I")) ($#r1_hidden :::"="::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k3_xtuple_0 :::"]"::: ) )) "or" (Bool "ex" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Data-Location":::) "of" (Set (Var "R")) "st" (Bool (Set (Var "I")) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k3_scmring2 :::":="::: ) (Set (Var "b"))))) "or" (Bool "ex" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Data-Location":::) "of" (Set (Var "R")) "st" (Bool (Set (Var "I")) ($#r1_hidden :::"="::: ) (Set ($#k4_scmring2 :::"AddTo"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ))) "or" (Bool "ex" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Data-Location":::) "of" (Set (Var "R")) "st" (Bool (Set (Var "I")) ($#r1_hidden :::"="::: ) (Set ($#k5_scmring2 :::"SubFrom"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ))) "or" (Bool "ex" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Data-Location":::) "of" (Set (Var "R")) "st" (Bool (Set (Var "I")) ($#r1_hidden :::"="::: ) (Set ($#k6_scmring2 :::"MultBy"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ))) "or" (Bool "ex" (Set (Var "i1")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Set (Var "I")) ($#r1_hidden :::"="::: ) (Set ($#k8_scmring2 :::"goto"::: ) "(" (Set (Var "i1")) "," (Set (Var "R")) ")" ))) "or" (Bool "ex" (Set (Var "a")) "being" ($#m1_subset_1 :::"Data-Location":::) "of" (Set (Var "R"))(Bool "ex" (Set (Var "i1")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Set (Var "I")) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k9_scmring2 :::"=0_goto"::: ) (Set (Var "i1")))))) "or" (Bool "ex" (Set (Var "a")) "being" ($#m1_subset_1 :::"Data-Location":::) "of" (Set (Var "R"))(Bool "ex" (Set (Var "r")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) "st" (Bool (Set (Var "I")) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k7_scmring2 :::":="::: ) (Set (Var "r")))))) ")" ) ")" ))) ; registrationlet "R" be ($#l6_algstr_0 :::"Ring":::); cluster (Set ($#k1_scmring2 :::"SCM"::: ) "R") -> ($#v3_memstr_0 :::"IC-Ins-separated"::: ) ($#v1_extpro_1 :::"strict"::: ) ; end; theorem :: SCMRING2:8 (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"Ring":::) "holds" (Bool (Set ($#k4_struct_0 :::"IC"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k5_numbers :::"NAT"::: ) ))) ; theorem :: SCMRING2:9 (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set "(" ($#k1_scmring2 :::"SCM"::: ) (Set (Var "R")) ")" ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"SCM-State":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set (Var "S")) ($#r1_hidden :::"="::: ) (Set (Var "s")))) "holds" (Bool (Set ($#k5_memstr_0 :::"IC"::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set ($#k2_scmring1 :::"IC"::: ) (Set (Var "S"))))))) ; theorem :: SCMRING2:10 (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set "(" ($#k1_scmring2 :::"SCM"::: ) (Set (Var "R")) ")" ) (Bool "for" (Set (Var "I")) "being" ($#m1_subset_1 :::"Instruction":::) "of" (Set "(" ($#k1_scmring2 :::"SCM"::: ) (Set (Var "R")) ")" ) (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_scmringi :::"SCM-Instr"::: ) (Set (Var "R"))) "st" (Bool (Bool (Set (Var "i")) ($#r1_hidden :::"="::: ) (Set (Var "I")))) "holds" (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"SCM-State":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set (Var "S")) ($#r1_hidden :::"="::: ) (Set (Var "s")))) "holds" (Bool (Set ($#k2_extpro_1 :::"Exec"::: ) "(" (Set (Var "I")) "," (Set (Var "s")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k7_scmring1 :::"SCM-Exec-Res"::: ) "(" (Set (Var "i")) "," (Set (Var "S")) ")" ))))))) ; begin theorem :: SCMRING2:11 (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Data-Location":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set "(" ($#k1_scmring2 :::"SCM"::: ) (Set (Var "R")) ")" ) "holds" (Bool "(" (Bool (Set (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set "(" (Set (Var "a")) ($#k3_scmring2 :::":="::: ) (Set (Var "b")) ")" ) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k4_struct_0 :::"IC"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_card_1 :::"succ"::: ) (Set "(" ($#k5_memstr_0 :::"IC"::: ) (Set (Var "s")) ")" ))) & (Bool (Set (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set "(" (Set (Var "a")) ($#k3_scmring2 :::":="::: ) (Set (Var "b")) ")" ) "," (Set (Var "s")) ")" ")" ) ($#k2_scmring2 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k2_scmring2 :::"."::: ) (Set (Var "b")))) & (Bool "(" "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Data-Location":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set (Var "c")) ($#r1_hidden :::"<>"::: ) (Set (Var "a")))) "holds" (Bool (Set (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set "(" (Set (Var "a")) ($#k3_scmring2 :::":="::: ) (Set (Var "b")) ")" ) "," (Set (Var "s")) ")" ")" ) ($#k2_scmring2 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k2_scmring2 :::"."::: ) (Set (Var "c")))) ")" ) ")" )))) ; theorem :: SCMRING2:12 (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Data-Location":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set "(" ($#k1_scmring2 :::"SCM"::: ) (Set (Var "R")) ")" ) "holds" (Bool "(" (Bool (Set (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set "(" ($#k4_scmring2 :::"AddTo"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" ) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k4_struct_0 :::"IC"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_card_1 :::"succ"::: ) (Set "(" ($#k5_memstr_0 :::"IC"::: ) (Set (Var "s")) ")" ))) & (Bool (Set (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set "(" ($#k4_scmring2 :::"AddTo"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" ) "," (Set (Var "s")) ")" ")" ) ($#k2_scmring2 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "s")) ($#k2_scmring2 :::"."::: ) (Set (Var "a")) ")" ) ($#k1_algstr_0 :::"+"::: ) (Set "(" (Set (Var "s")) ($#k2_scmring2 :::"."::: ) (Set (Var "b")) ")" ))) & (Bool "(" "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Data-Location":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set (Var "c")) ($#r1_hidden :::"<>"::: ) (Set (Var "a")))) "holds" (Bool (Set (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set "(" ($#k4_scmring2 :::"AddTo"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" ) "," (Set (Var "s")) ")" ")" ) ($#k2_scmring2 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k2_scmring2 :::"."::: ) (Set (Var "c")))) ")" ) ")" )))) ; theorem :: SCMRING2:13 (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Data-Location":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set "(" ($#k1_scmring2 :::"SCM"::: ) (Set (Var "R")) ")" ) "holds" (Bool "(" (Bool (Set (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set "(" ($#k5_scmring2 :::"SubFrom"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" ) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k4_struct_0 :::"IC"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_card_1 :::"succ"::: ) (Set "(" ($#k5_memstr_0 :::"IC"::: ) (Set (Var "s")) ")" ))) & (Bool (Set (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set "(" ($#k5_scmring2 :::"SubFrom"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" ) "," (Set (Var "s")) ")" ")" ) ($#k2_scmring2 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "s")) ($#k2_scmring2 :::"."::: ) (Set (Var "a")) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set (Var "s")) ($#k2_scmring2 :::"."::: ) (Set (Var "b")) ")" ))) & (Bool "(" "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Data-Location":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set (Var "c")) ($#r1_hidden :::"<>"::: ) (Set (Var "a")))) "holds" (Bool (Set (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set "(" ($#k5_scmring2 :::"SubFrom"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" ) "," (Set (Var "s")) ")" ")" ) ($#k2_scmring2 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k2_scmring2 :::"."::: ) (Set (Var "c")))) ")" ) ")" )))) ; theorem :: SCMRING2:14 (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Data-Location":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set "(" ($#k1_scmring2 :::"SCM"::: ) (Set (Var "R")) ")" ) "holds" (Bool "(" (Bool (Set (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set "(" ($#k6_scmring2 :::"MultBy"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" ) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k4_struct_0 :::"IC"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_card_1 :::"succ"::: ) (Set "(" ($#k5_memstr_0 :::"IC"::: ) (Set (Var "s")) ")" ))) & (Bool (Set (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set "(" ($#k6_scmring2 :::"MultBy"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" ) "," (Set (Var "s")) ")" ")" ) ($#k2_scmring2 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "s")) ($#k2_scmring2 :::"."::: ) (Set (Var "a")) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set "(" (Set (Var "s")) ($#k2_scmring2 :::"."::: ) (Set (Var "b")) ")" ))) & (Bool "(" "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Data-Location":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set (Var "c")) ($#r1_hidden :::"<>"::: ) (Set (Var "a")))) "holds" (Bool (Set (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set "(" ($#k6_scmring2 :::"MultBy"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" ) "," (Set (Var "s")) ")" ")" ) ($#k2_scmring2 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k2_scmring2 :::"."::: ) (Set (Var "c")))) ")" ) ")" )))) ; theorem :: SCMRING2:15 (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Data-Location":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "i1")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set "(" ($#k1_scmring2 :::"SCM"::: ) (Set (Var "R")) ")" ) "holds" (Bool "(" (Bool (Set (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set "(" ($#k8_scmring2 :::"goto"::: ) "(" (Set (Var "i1")) "," (Set (Var "R")) ")" ")" ) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k4_struct_0 :::"IC"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "i1"))) & (Bool (Set (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set "(" ($#k8_scmring2 :::"goto"::: ) "(" (Set (Var "i1")) "," (Set (Var "R")) ")" ")" ) "," (Set (Var "s")) ")" ")" ) ($#k2_scmring2 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k2_scmring2 :::"."::: ) (Set (Var "c")))) ")" ))))) ; theorem :: SCMRING2:16 (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "a")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Data-Location":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "i1")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set "(" ($#k1_scmring2 :::"SCM"::: ) (Set (Var "R")) ")" ) "holds" (Bool "(" "(" (Bool (Bool (Set (Set (Var "s")) ($#k2_scmring2 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "R"))))) "implies" (Bool (Set (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set "(" (Set (Var "a")) ($#k9_scmring2 :::"=0_goto"::: ) (Set (Var "i1")) ")" ) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k4_struct_0 :::"IC"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "i1"))) ")" & "(" (Bool (Bool (Set (Set (Var "s")) ($#k2_scmring2 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "R"))))) "implies" (Bool (Set (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set "(" (Set (Var "a")) ($#k9_scmring2 :::"=0_goto"::: ) (Set (Var "i1")) ")" ) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k4_struct_0 :::"IC"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_card_1 :::"succ"::: ) (Set "(" ($#k5_memstr_0 :::"IC"::: ) (Set (Var "s")) ")" ))) ")" & (Bool (Set (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set "(" (Set (Var "a")) ($#k9_scmring2 :::"=0_goto"::: ) (Set (Var "i1")) ")" ) "," (Set (Var "s")) ")" ")" ) ($#k2_scmring2 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k2_scmring2 :::"."::: ) (Set (Var "c")))) ")" ))))) ; theorem :: SCMRING2:17 (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Data-Location":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set "(" ($#k1_scmring2 :::"SCM"::: ) (Set (Var "R")) ")" ) "holds" (Bool "(" (Bool (Set (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set "(" (Set (Var "a")) ($#k7_scmring2 :::":="::: ) (Set (Var "r")) ")" ) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k4_struct_0 :::"IC"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_card_1 :::"succ"::: ) (Set "(" ($#k5_memstr_0 :::"IC"::: ) (Set (Var "s")) ")" ))) & (Bool (Set (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set "(" (Set (Var "a")) ($#k7_scmring2 :::":="::: ) (Set (Var "r")) ")" ) "," (Set (Var "s")) ")" ")" ) ($#k2_scmring2 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Var "r"))) & (Bool "(" "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Data-Location":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set (Var "c")) ($#r1_hidden :::"<>"::: ) (Set (Var "a")))) "holds" (Bool (Set (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set "(" (Set (Var "a")) ($#k7_scmring2 :::":="::: ) (Set (Var "r")) ")" ) "," (Set (Var "s")) ")" ")" ) ($#k2_scmring2 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k2_scmring2 :::"."::: ) (Set (Var "c")))) ")" ) ")" ))))) ; begin theorem :: SCMRING2:18 (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "I")) "being" ($#m1_subset_1 :::"Instruction":::) "of" (Set "(" ($#k1_scmring2 :::"SCM"::: ) (Set (Var "R")) ")" ) "st" (Bool (Bool "ex" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set "(" ($#k1_scmring2 :::"SCM"::: ) (Set (Var "R")) ")" ) "st" (Bool (Set (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set (Var "I")) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k4_struct_0 :::"IC"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_card_1 :::"succ"::: ) (Set "(" ($#k5_memstr_0 :::"IC"::: ) (Set (Var "s")) ")" ))))) "holds" (Bool "not" (Bool (Set (Var "I")) "is" ($#v2_extpro_1 :::"halting"::: ) )))) ; theorem :: SCMRING2:19 (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "I")) "being" ($#m1_subset_1 :::"Instruction":::) "of" (Set "(" ($#k1_scmring2 :::"SCM"::: ) (Set (Var "R")) ")" ) "st" (Bool (Bool (Set (Var "I")) ($#r1_hidden :::"="::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k3_xtuple_0 :::"]"::: ) ))) "holds" (Bool (Set (Var "I")) "is" ($#v2_extpro_1 :::"halting"::: ) ))) ; registrationlet "R" be ($#l6_algstr_0 :::"Ring":::); let "a", "b" be ($#m1_subset_1 :::"Data-Location":::) "of" (Set (Const "R")); cluster (Set "a" ($#k3_scmring2 :::":="::: ) "b") -> ($#~v2_extpro_1 "non" ($#v2_extpro_1 :::"halting"::: ) ) ; cluster (Set ($#k4_scmring2 :::"AddTo"::: ) "(" "a" "," "b" ")" ) -> ($#~v2_extpro_1 "non" ($#v2_extpro_1 :::"halting"::: ) ) ; cluster (Set ($#k5_scmring2 :::"SubFrom"::: ) "(" "a" "," "b" ")" ) -> ($#~v2_extpro_1 "non" ($#v2_extpro_1 :::"halting"::: ) ) ; cluster (Set ($#k6_scmring2 :::"MultBy"::: ) "(" "a" "," "b" ")" ) -> ($#~v2_extpro_1 "non" ($#v2_extpro_1 :::"halting"::: ) ) ; end; registrationlet "R" be ($#l6_algstr_0 :::"Ring":::); let "i1" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); cluster (Set ($#k8_scmring2 :::"goto"::: ) "(" "i1" "," "R" ")" ) -> ($#~v2_extpro_1 "non" ($#v2_extpro_1 :::"halting"::: ) ) ; end; registrationlet "R" be ($#l6_algstr_0 :::"Ring":::); let "a" be ($#m1_subset_1 :::"Data-Location":::) "of" (Set (Const "R")); let "i1" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); cluster (Set "a" ($#k9_scmring2 :::"=0_goto"::: ) "i1") -> ($#~v2_extpro_1 "non" ($#v2_extpro_1 :::"halting"::: ) ) ; end; registrationlet "R" be ($#l6_algstr_0 :::"Ring":::); let "a" be ($#m1_subset_1 :::"Data-Location":::) "of" (Set (Const "R")); let "r" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "R")); cluster (Set "a" ($#k7_scmring2 :::":="::: ) "r") -> ($#~v2_extpro_1 "non" ($#v2_extpro_1 :::"halting"::: ) ) ; end; registrationlet "R" be ($#l6_algstr_0 :::"Ring":::); cluster (Set ($#k1_scmring2 :::"SCM"::: ) "R") -> ($#v1_extpro_1 :::"strict"::: ) ($#v3_extpro_1 :::"halting"::: ) ; end; theorem :: SCMRING2:20 (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "I")) "being" ($#m1_subset_1 :::"Instruction":::) "of" (Set "(" ($#k1_scmring2 :::"SCM"::: ) (Set (Var "R")) ")" ) "st" (Bool (Bool (Set (Var "I")) "is" ($#v2_extpro_1 :::"halting"::: ) )) "holds" (Bool (Set (Var "I")) ($#r1_hidden :::"="::: ) (Set ($#k2_compos_1 :::"halt"::: ) (Set "(" ($#k1_scmring2 :::"SCM"::: ) (Set (Var "R")) ")" ))))) ; theorem :: SCMRING2:21 (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"Ring":::) "holds" (Bool (Set ($#k2_compos_1 :::"halt"::: ) (Set "(" ($#k1_scmring2 :::"SCM"::: ) (Set (Var "R")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k3_xtuple_0 :::"]"::: ) ))) ; theorem :: SCMRING2:22 (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"Ring":::) "holds" (Bool (Set ($#k8_struct_0 :::"Data-Locations"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k8_struct_0 :::"Data-Locations"::: ) ))) ; theorem :: SCMRING2:23 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"Ring":::) "holds" (Bool "(" (Bool (Set (Var "x")) "is" ($#m1_subset_1 :::"Data-Location":::) "of" (Set (Var "R"))) "iff" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k8_struct_0 :::"Data-Locations"::: ) )) ")" ))) ; theorem :: SCMRING2:24 (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"Ring":::) "holds" (Bool (Set ($#k2_memstr_0 :::"the_Values_of"::: ) (Set "(" ($#k1_scmring2 :::"SCM"::: ) (Set (Var "R")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_scmring1 :::"SCM-VAL"::: ) (Set (Var "R")) ")" ) ($#k3_relat_1 :::"*"::: ) (Set ($#k3_ami_2 :::"SCM-OK"::: ) )))) ; theorem :: SCMRING2:25 (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"Ring":::) "holds" (Bool (Set (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k1_scmring2 :::"SCM"::: ) (Set (Var "R")) ")" )) ($#k6_subset_1 :::"\"::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#k1_tarski :::"}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k2_ami_2 :::"SCM-Data-Loc"::: ) ))) ;