:: SCMRING3  semantic presentation begin  































theorem :: SCMRING3:1 (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")) "holds"  (Bool (Set   ($#k4_memstr_0 :::"Values"::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "R")))))) ; 
 definitionlet "R" be   ($#l6_algstr_0 :::"Ring":::); let "la", "lb" be   ($#m1_subset_1 :::"Data-Location":::) "of" (Set (Const "R")); let "a", "b" be   ($#m1_subset_1 :::"Element":::) "of" (Set (Const "R")); :: original: :::"-->"::: redefine func  "(" "la" "," "lb" ")"  :::"-->":::  "(" "a" "," "b" ")"  ->   ($#m1_hidden :::"FinPartState":::) "of" (Set  "("  ($#k1_scmring2 :::"SCM"::: )  "R" ")" ); end; 
theorem :: SCMRING3:2 (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"))  "holds" (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k4_struct_0 :::"IC"::: )  )))) ; 
 
theorem :: SCMRING3:3 (Bool  "for" (Set (Var "R")) "being"   ($#l6_algstr_0 :::"Ring":::)  (Bool  "for" (Set (Var "o")) "being"   ($#m1_subset_1 :::"Object":::) "of" (Set  "("  ($#k1_scmring2 :::"SCM"::: )  (Set (Var "R")) ")" )  "holds"  (Bool  "("  (Bool (Set (Var "o"))  ($#r1_hidden :::"="::: )  (Set   ($#k4_struct_0 :::"IC"::: )  )) "or" (Bool (Set (Var "o")) "is"   ($#m1_subset_1 :::"Data-Location":::) "of" (Set (Var "R")))  ")" ))) ; 
 
theorem :: SCMRING3:4 canceled; 
 
theorem :: SCMRING3: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   ($#k2_compos_0 :::"InsCode"::: )  (Set  "(" (Set (Var "a"))  ($#k3_scmring2 :::":="::: )  (Set (Var "b")) ")" ))  ($#r1_hidden :::"="::: )  (Num 1)))) ; 
 
theorem :: SCMRING3: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   ($#k2_compos_0 :::"InsCode"::: )  (Set  "("  ($#k4_scmring2 :::"AddTo"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Num 2)))) ; 
 
theorem :: SCMRING3:7 (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   ($#k2_compos_0 :::"InsCode"::: )  (Set  "("  ($#k5_scmring2 :::"SubFrom"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Num 3)))) ; 
 
theorem :: SCMRING3:8 (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   ($#k2_compos_0 :::"InsCode"::: )  (Set  "("  ($#k6_scmring2 :::"MultBy"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Num 4)))) ; 
 
theorem :: SCMRING3:9 (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")) "holds"  (Bool (Set   ($#k2_compos_0 :::"InsCode"::: )  (Set  "(" (Set (Var "a"))  ($#k7_scmring2 :::":="::: )  (Set (Var "r")) ")" ))  ($#r1_hidden :::"="::: )  (Num 5))))) ; 
 
theorem :: SCMRING3:10 (Bool  "for" (Set (Var "R")) "being"   ($#l6_algstr_0 :::"Ring":::)  (Bool  "for" (Set (Var "i1")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set   ($#k2_compos_0 :::"InsCode"::: )  (Set  "("  ($#k8_scmring2 :::"goto"::: )   "(" (Set (Var "i1")) "," (Set (Var "R")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Num 6)))) ; 
 
theorem :: SCMRING3:11 (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 "i1")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set   ($#k2_compos_0 :::"InsCode"::: )  (Set  "(" (Set (Var "a"))  ($#k9_scmring2 :::"=0_goto"::: )  (Set (Var "i1")) ")" ))  ($#r1_hidden :::"="::: )  (Num 7))))) ; 
 
theorem :: SCMRING3:12 (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   ($#k2_compos_0 :::"InsCode"::: )  (Set (Var "I")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Var "I"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_compos_1 :::"halt"::: )  (Set  "("  ($#k1_scmring2 :::"SCM"::: )  (Set (Var "R")) ")" ))))) ; 
 
theorem :: SCMRING3:13 (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   ($#k2_compos_0 :::"InsCode"::: )  (Set (Var "I")))  ($#r1_hidden :::"="::: )  (Num 1))) "holds"  (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"))))))) ; 
 
theorem :: SCMRING3:14 (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   ($#k2_compos_0 :::"InsCode"::: )  (Set (Var "I")))  ($#r1_hidden :::"="::: )  (Num 2))) "holds"  (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")) ")" ))))) ; 
 
theorem :: SCMRING3:15 (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   ($#k2_compos_0 :::"InsCode"::: )  (Set (Var "I")))  ($#r1_hidden :::"="::: )  (Num 3))) "holds"  (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")) ")" ))))) ; 
 
theorem :: SCMRING3:16 (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   ($#k2_compos_0 :::"InsCode"::: )  (Set (Var "I")))  ($#r1_hidden :::"="::: )  (Num 4))) "holds"  (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")) ")" ))))) ; 
 
theorem :: SCMRING3:17 (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   ($#k2_compos_0 :::"InsCode"::: )  (Set (Var "I")))  ($#r1_hidden :::"="::: )  (Num 5))) "holds"  (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")))))))) ; 
 
theorem :: SCMRING3: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 (Set   ($#k2_compos_0 :::"InsCode"::: )  (Set (Var "I")))  ($#r1_hidden :::"="::: )  (Num 6))) "holds"  (Bool  "ex" (Set (Var "i2")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "st" (Bool (Set (Var "I"))  ($#r1_hidden :::"="::: )  (Set   ($#k8_scmring2 :::"goto"::: )   "(" (Set (Var "i2")) "," (Set (Var "R")) ")" ))))) ; 
 
theorem :: SCMRING3: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   ($#k2_compos_0 :::"InsCode"::: )  (Set (Var "I")))  ($#r1_hidden :::"="::: )  (Num 7))) "holds"  (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")))))))) ; 
 
theorem :: SCMRING3:20 (Bool  "for" (Set (Var "R")) "being"   ($#l6_algstr_0 :::"Ring":::)  (Bool  "for" (Set (Var "T")) "being"   ($#m1_subset_1 :::"InsType":::) "of" (Set  "the"  ($#u1_compos_1 :::"InstructionsF"::: )  "of" (Set  "("  ($#k1_scmring2 :::"SCM"::: )  (Set (Var "R")) ")" ))  "st" (Bool (Bool (Set (Var "T"))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set   ($#k3_compos_0 :::"JumpParts"::: )  (Set (Var "T")))  ($#r1_hidden :::"="::: )  (Set  ($#k1_tarski :::"{"::: ) (Set  ($#k6_numbers :::"0"::: ) ) ($#k1_tarski :::"}"::: ) )))) ; 
 
theorem :: SCMRING3:21 (Bool  "for" (Set (Var "R")) "being"   ($#l6_algstr_0 :::"Ring":::)  (Bool  "for" (Set (Var "T")) "being"   ($#m1_subset_1 :::"InsType":::) "of" (Set  "the"  ($#u1_compos_1 :::"InstructionsF"::: )  "of" (Set  "("  ($#k1_scmring2 :::"SCM"::: )  (Set (Var "R")) ")" ))  "st" (Bool (Bool (Set (Var "T"))  ($#r1_hidden :::"="::: )  (Num 1))) "holds"  (Bool (Set   ($#k3_compos_0 :::"JumpParts"::: )  (Set (Var "T")))  ($#r1_hidden :::"="::: )  (Set  ($#k1_tarski :::"{"::: ) (Set  ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) )))) ; 
 
theorem :: SCMRING3:22 (Bool  "for" (Set (Var "R")) "being"   ($#l6_algstr_0 :::"Ring":::)  (Bool  "for" (Set (Var "T")) "being"   ($#m1_subset_1 :::"InsType":::) "of" (Set  "the"  ($#u1_compos_1 :::"InstructionsF"::: )  "of" (Set  "("  ($#k1_scmring2 :::"SCM"::: )  (Set (Var "R")) ")" ))  "st" (Bool (Bool (Set (Var "T"))  ($#r1_hidden :::"="::: )  (Num 2))) "holds"  (Bool (Set   ($#k3_compos_0 :::"JumpParts"::: )  (Set (Var "T")))  ($#r1_hidden :::"="::: )  (Set  ($#k1_tarski :::"{"::: ) (Set  ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) )))) ; 
 
theorem :: SCMRING3:23 (Bool  "for" (Set (Var "R")) "being"   ($#l6_algstr_0 :::"Ring":::)  (Bool  "for" (Set (Var "T")) "being"   ($#m1_subset_1 :::"InsType":::) "of" (Set  "the"  ($#u1_compos_1 :::"InstructionsF"::: )  "of" (Set  "("  ($#k1_scmring2 :::"SCM"::: )  (Set (Var "R")) ")" ))  "st" (Bool (Bool (Set (Var "T"))  ($#r1_hidden :::"="::: )  (Num 3))) "holds"  (Bool (Set   ($#k3_compos_0 :::"JumpParts"::: )  (Set (Var "T")))  ($#r1_hidden :::"="::: )  (Set  ($#k1_tarski :::"{"::: ) (Set  ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) )))) ; 
 
theorem :: SCMRING3:24 (Bool  "for" (Set (Var "R")) "being"   ($#l6_algstr_0 :::"Ring":::)  (Bool  "for" (Set (Var "T")) "being"   ($#m1_subset_1 :::"InsType":::) "of" (Set  "the"  ($#u1_compos_1 :::"InstructionsF"::: )  "of" (Set  "("  ($#k1_scmring2 :::"SCM"::: )  (Set (Var "R")) ")" ))  "st" (Bool (Bool (Set (Var "T"))  ($#r1_hidden :::"="::: )  (Num 4))) "holds"  (Bool (Set   ($#k3_compos_0 :::"JumpParts"::: )  (Set (Var "T")))  ($#r1_hidden :::"="::: )  (Set  ($#k1_tarski :::"{"::: ) (Set  ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) )))) ; 
 
theorem :: SCMRING3:25 (Bool  "for" (Set (Var "R")) "being"   ($#l6_algstr_0 :::"Ring":::)  (Bool  "for" (Set (Var "T")) "being"   ($#m1_subset_1 :::"InsType":::) "of" (Set  "the"  ($#u1_compos_1 :::"InstructionsF"::: )  "of" (Set  "("  ($#k1_scmring2 :::"SCM"::: )  (Set (Var "R")) ")" ))  "st" (Bool (Bool (Set (Var "T"))  ($#r1_hidden :::"="::: )  (Num 5))) "holds"  (Bool (Set   ($#k3_compos_0 :::"JumpParts"::: )  (Set (Var "T")))  ($#r1_hidden :::"="::: )  (Set  ($#k1_tarski :::"{"::: ) (Set  ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) )))) ; 
 
theorem :: SCMRING3:26 (Bool  "for" (Set (Var "R")) "being"   ($#l6_algstr_0 :::"Ring":::)  (Bool  "for" (Set (Var "T")) "being"   ($#m1_subset_1 :::"InsType":::) "of" (Set  "the"  ($#u1_compos_1 :::"InstructionsF"::: )  "of" (Set  "("  ($#k1_scmring2 :::"SCM"::: )  (Set (Var "R")) ")" ))  "st" (Bool (Bool (Set (Var "T"))  ($#r1_hidden :::"="::: )  (Num 6))) "holds"  (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set  "("  ($#k10_card_3 :::"product""::: )  (Set  "("  ($#k3_compos_0 :::"JumpParts"::: )  (Set (Var "T")) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set  ($#k1_tarski :::"{"::: ) (Num 1) ($#k1_tarski :::"}"::: ) )))) ; 
 
theorem :: SCMRING3:27 (Bool  "for" (Set (Var "R")) "being"   ($#l6_algstr_0 :::"Ring":::)  (Bool  "for" (Set (Var "T")) "being"   ($#m1_subset_1 :::"InsType":::) "of" (Set  "the"  ($#u1_compos_1 :::"InstructionsF"::: )  "of" (Set  "("  ($#k1_scmring2 :::"SCM"::: )  (Set (Var "R")) ")" ))  "st" (Bool (Bool (Set (Var "T"))  ($#r1_hidden :::"="::: )  (Num 7))) "holds"  (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set  "("  ($#k10_card_3 :::"product""::: )  (Set  "("  ($#k3_compos_0 :::"JumpParts"::: )  (Set (Var "T")) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set  ($#k1_tarski :::"{"::: ) (Num 1) ($#k1_tarski :::"}"::: ) )))) ; 
 
theorem :: SCMRING3:28 (Bool  "for" (Set (Var "R")) "being"   ($#l6_algstr_0 :::"Ring":::)  (Bool  "for" (Set (Var "i1")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set (Set  "("  ($#k10_card_3 :::"product""::: )  (Set  "("  ($#k3_compos_0 :::"JumpParts"::: )  (Set  "("  ($#k2_compos_0 :::"InsCode"::: )  (Set  "("  ($#k8_scmring2 :::"goto"::: )   "(" (Set (Var "i1")) "," (Set (Var "R")) ")"  ")" ) ")" ) ")" ) ")" )  ($#k1_funct_1 :::"."::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Set   ($#k5_numbers :::"NAT"::: )  )))) ; 
 
theorem :: SCMRING3:29 (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 "i1")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set (Set  "("  ($#k10_card_3 :::"product""::: )  (Set  "("  ($#k3_compos_0 :::"JumpParts"::: )  (Set  "("  ($#k2_compos_0 :::"InsCode"::: )  (Set  "(" (Set (Var "a"))  ($#k9_scmring2 :::"=0_goto"::: )  (Set (Var "i1")) ")" ) ")" ) ")" ) ")" )  ($#k1_funct_1 :::"."::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Set   ($#k5_numbers :::"NAT"::: )  ))))) ; 
 registrationlet "R" be   ($#l6_algstr_0 :::"Ring":::); 
cluster (Set   ($#k2_amistd_1 :::"JUMP"::: )  (Set  "("  ($#k2_compos_1 :::"halt"::: )  (Set  "("  ($#k1_scmring2 :::"SCM"::: )  "R" ")" ) ")" )) ->   ($#v1_xboole_0 :::"empty"::: )   ; 
end; 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") ->   ($#v4_amistd_1 :::"sequential"::: )   ; 

cluster (Set   ($#k4_scmring2 :::"AddTo"::: )   "(" "a" "," "b" ")" ) ->   ($#v4_amistd_1 :::"sequential"::: )   ; 

cluster (Set   ($#k5_scmring2 :::"SubFrom"::: )   "(" "a" "," "b" ")" ) ->   ($#v4_amistd_1 :::"sequential"::: )   ; 

cluster (Set   ($#k6_scmring2 :::"MultBy"::: )   "(" "a" "," "b" ")" ) ->   ($#v4_amistd_1 :::"sequential"::: )   ; 
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") ->   ($#v4_amistd_1 :::"sequential"::: )   ; 
end; registrationlet "R" be   ($#l6_algstr_0 :::"Ring":::); let "a", "b" be   ($#m1_subset_1 :::"Data-Location":::) "of" (Set (Const "R")); 
cluster (Set   ($#k2_amistd_1 :::"JUMP"::: )  (Set  "(" "a"  ($#k3_scmring2 :::":="::: )  "b" ")" )) ->   ($#v1_xboole_0 :::"empty"::: )   ; 
end; registrationlet "R" be   ($#l6_algstr_0 :::"Ring":::); let "a", "b" be   ($#m1_subset_1 :::"Data-Location":::) "of" (Set (Const "R")); 
cluster (Set   ($#k2_amistd_1 :::"JUMP"::: )  (Set  "("  ($#k4_scmring2 :::"AddTo"::: )   "(" "a" "," "b" ")"  ")" )) ->   ($#v1_xboole_0 :::"empty"::: )   ; 
end; registrationlet "R" be   ($#l6_algstr_0 :::"Ring":::); let "a", "b" be   ($#m1_subset_1 :::"Data-Location":::) "of" (Set (Const "R")); 
cluster (Set   ($#k2_amistd_1 :::"JUMP"::: )  (Set  "("  ($#k5_scmring2 :::"SubFrom"::: )   "(" "a" "," "b" ")"  ")" )) ->   ($#v1_xboole_0 :::"empty"::: )   ; 
end; registrationlet "R" be   ($#l6_algstr_0 :::"Ring":::); let "a", "b" be   ($#m1_subset_1 :::"Data-Location":::) "of" (Set (Const "R")); 
cluster (Set   ($#k2_amistd_1 :::"JUMP"::: )  (Set  "("  ($#k6_scmring2 :::"MultBy"::: )   "(" "a" "," "b" ")"  ")" )) ->   ($#v1_xboole_0 :::"empty"::: )   ; 
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   ($#k2_amistd_1 :::"JUMP"::: )  (Set  "(" "a"  ($#k7_scmring2 :::":="::: )  "r" ")" )) ->   ($#v1_xboole_0 :::"empty"::: )   ; 
end; 
theorem :: SCMRING3:30 (Bool  "for" (Set (Var "R")) "being"   ($#l6_algstr_0 :::"Ring":::)  (Bool  "for" (Set (Var "i1")) "," (Set (Var "il")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set   ($#k1_amistd_1 :::"NIC"::: )   "(" (Set  "("  ($#k8_scmring2 :::"goto"::: )   "(" (Set (Var "i1")) "," (Set (Var "R")) ")"  ")" ) "," (Set (Var "il")) ")" )  ($#r1_hidden :::"="::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "i1")) ($#k1_tarski :::"}"::: ) )))) ; 
 
theorem :: SCMRING3:31 (Bool  "for" (Set (Var "R")) "being"   ($#l6_algstr_0 :::"Ring":::)  (Bool  "for" (Set (Var "i1")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set   ($#k2_amistd_1 :::"JUMP"::: )  (Set  "("  ($#k8_scmring2 :::"goto"::: )   "(" (Set (Var "i1")) "," (Set (Var "R")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "i1")) ($#k1_tarski :::"}"::: ) )))) ; 
 registrationlet "R" be   ($#l6_algstr_0 :::"Ring":::); let "i1" be    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); 
cluster (Set   ($#k2_amistd_1 :::"JUMP"::: )  (Set  "("  ($#k8_scmring2 :::"goto"::: )   "(" "i1" "," "R" ")"  ")" )) -> (Num 1)  ($#v3_card_1 :::"-element"::: )   ; 
end; 
theorem :: SCMRING3:32 (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 "i1")) "," (Set (Var "il")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"   (Bool  "("  (Bool (Set (Var "i1"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_amistd_1 :::"NIC"::: )   "(" (Set  "(" (Set (Var "a"))  ($#k9_scmring2 :::"=0_goto"::: )  (Set (Var "i1")) ")" ) "," (Set (Var "il")) ")" )) & (Bool (Set   ($#k1_amistd_1 :::"NIC"::: )   "(" (Set  "(" (Set (Var "a"))  ($#k9_scmring2 :::"=0_goto"::: )  (Set (Var "i1")) ")" ) "," (Set (Var "il")) ")" )  ($#r1_tarski :::"c="::: )  (Set  ($#k2_tarski :::"{"::: ) (Set (Var "i1")) "," (Set  "("  ($#k1_ordinal1 :::"succ"::: )  (Set (Var "il")) ")" ) ($#k2_tarski :::"}"::: ) ))  ")" )))) ; 
 
theorem :: SCMRING3:33 (Bool  "for" (Set (Var "R")) "being"  ($#~v7_struct_0  "non"   ($#v7_struct_0 :::"trivial"::: )   )   ($#l6_algstr_0 :::"Ring":::)  (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Data-Location":::) "of" (Set (Var "R"))  (Bool  "for" (Set (Var "il")) "," (Set (Var "i1")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set   ($#k1_amistd_1 :::"NIC"::: )   "(" (Set  "(" (Set (Var "a"))  ($#k9_scmring2 :::"=0_goto"::: )  (Set (Var "i1")) ")" ) "," (Set (Var "il")) ")" )  ($#r1_hidden :::"="::: )  (Set  ($#k2_tarski :::"{"::: ) (Set (Var "i1")) "," (Set  "("  ($#k1_ordinal1 :::"succ"::: )  (Set (Var "il")) ")" ) ($#k2_tarski :::"}"::: ) ))))) ; 
 
theorem :: SCMRING3:34 (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 "i1")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set   ($#k2_amistd_1 :::"JUMP"::: )  (Set  "(" (Set (Var "a"))  ($#k9_scmring2 :::"=0_goto"::: )  (Set (Var "i1")) ")" ))  ($#r1_hidden :::"="::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "i1")) ($#k1_tarski :::"}"::: ) ))))) ; 
 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   ($#k2_amistd_1 :::"JUMP"::: )  (Set  "(" "a"  ($#k9_scmring2 :::"=0_goto"::: )  "i1" ")" )) -> (Num 1)  ($#v3_card_1 :::"-element"::: )   ; 
end; 
theorem :: SCMRING3:35 (Bool  "for" (Set (Var "R")) "being"   ($#l6_algstr_0 :::"Ring":::)  (Bool  "for" (Set (Var "il")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set   ($#k3_amistd_1 :::"SUCC"::: )   "(" (Set (Var "il")) "," (Set  "("  ($#k1_scmring2 :::"SCM"::: )  (Set (Var "R")) ")" ) ")" )  ($#r1_hidden :::"="::: )  (Set  ($#k2_tarski :::"{"::: ) (Set (Var "il")) "," (Set  "("  ($#k1_ordinal1 :::"succ"::: )  (Set (Var "il")) ")" ) ($#k2_tarski :::"}"::: ) )))) ; 
 
theorem :: SCMRING3:36 (Bool  "for" (Set (Var "R")) "being"   ($#l6_algstr_0 :::"Ring":::)  (Bool  "for" (Set (Var "k")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"   (Bool  "("  (Bool (Set (Set (Var "k"))  ($#k2_nat_1 :::"+"::: )  (Num 1))  ($#r2_hidden :::"in"::: )  (Set   ($#k3_amistd_1 :::"SUCC"::: )   "(" (Set (Var "k")) "," (Set  "("  ($#k1_scmring2 :::"SCM"::: )  (Set (Var "R")) ")" ) ")" )) & (Bool  "("   "for" (Set (Var "j")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "j"))  ($#r2_hidden :::"in"::: )  (Set   ($#k3_amistd_1 :::"SUCC"::: )   "(" (Set (Var "k")) "," (Set  "("  ($#k1_scmring2 :::"SCM"::: )  (Set (Var "R")) ")" ) ")" ))) "holds"  (Bool (Set (Var "k"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "j")))  ")" )  ")" ))) ; 
 registrationlet "R" be   ($#l6_algstr_0 :::"Ring":::); 
cluster (Set   ($#k1_scmring2 :::"SCM"::: )  "R") ->   ($#v3_amistd_1 :::"standard"::: )   ; 
end; definitionlet "R" be   ($#l6_algstr_0 :::"Ring":::); let "k" be    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); func  :::"dl.":::  "(" "R" "," "k" ")"  ->   ($#m1_subset_1 :::"Data-Location":::) "of" "R" equals :: SCMRING3:def 1 (Set   ($#k10_ami_3 :::"dl."::: )  "k"); end; 






:: deftheorem    defines :::"dl."::: SCMRING3:def 1 :  (Bool  "for" (Set (Var "R")) "being"   ($#l6_algstr_0 :::"Ring":::)  (Bool  "for" (Set (Var "k")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set   ($#k2_scmring3 :::"dl."::: )   "(" (Set (Var "R")) "," (Set (Var "k")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k10_ami_3 :::"dl."::: )  (Set (Var "k")))))); 
 registrationlet "R" be   ($#l6_algstr_0 :::"Ring":::); 
cluster (Set   ($#k4_xtuple_0 :::"InsCode"::: )  (Set  "("  ($#k2_compos_1 :::"halt"::: )  (Set  "("  ($#k1_scmring2 :::"SCM"::: )  "R" ")" ) ")" )) ->   ($#v1_amistd_1 :::"jump-only"::: )    for  ($#m1_subset_1 :::"InsType":::) "of" (Set  "the"  ($#u1_compos_1 :::"InstructionsF"::: )  "of" (Set  "("  ($#k1_scmring2 :::"SCM"::: )  "R" ")" )); 
end; registrationlet "R" be   ($#l6_algstr_0 :::"Ring":::); 
cluster (Set   ($#k2_compos_1 :::"halt"::: )  (Set  "("  ($#k1_scmring2 :::"SCM"::: )  "R" ")" )) ->   ($#v2_amistd_1 :::"jump-only"::: )   ; 
end; registrationlet "R" be   ($#l6_algstr_0 :::"Ring":::); let "i1" be    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); 
cluster (Set   ($#k4_xtuple_0 :::"InsCode"::: )  (Set  "("  ($#k8_scmring2 :::"goto"::: )   "(" "i1" "," "R" ")"  ")" )) ->   ($#v1_amistd_1 :::"jump-only"::: )    for  ($#m1_subset_1 :::"InsType":::) "of" (Set  "the"  ($#u1_compos_1 :::"InstructionsF"::: )  "of" (Set  "("  ($#k1_scmring2 :::"SCM"::: )  "R" ")" )); 
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_amistd_1 :::"jump-only"::: )   ; 
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   ($#k4_xtuple_0 :::"InsCode"::: )  (Set  "(" "a"  ($#k9_scmring2 :::"=0_goto"::: )  "i1" ")" )) ->   ($#v1_amistd_1 :::"jump-only"::: )    for  ($#m1_subset_1 :::"InsType":::) "of" (Set  "the"  ($#u1_compos_1 :::"InstructionsF"::: )  "of" (Set  "("  ($#k1_scmring2 :::"SCM"::: )  "R" ")" )); 
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_amistd_1 :::"jump-only"::: )   ; 
end; 









registrationlet "S" be  ($#~v7_struct_0  "non"   ($#v7_struct_0 :::"trivial"::: )   )   ($#l6_algstr_0 :::"Ring":::); let "p", "q" be   ($#m1_subset_1 :::"Data-Location":::) "of" (Set (Const "S")); 
cluster (Set   ($#k4_xtuple_0 :::"InsCode"::: )  (Set  "(" "p"  ($#k3_scmring2 :::":="::: )  "q" ")" )) ->  ($#~v1_amistd_1  "non"   ($#v1_amistd_1 :::"jump-only"::: )   )   for  ($#m1_subset_1 :::"InsType":::) "of" (Set  "the"  ($#u1_compos_1 :::"InstructionsF"::: )  "of" (Set  "("  ($#k1_scmring2 :::"SCM"::: )  "S" ")" )); 
end; registrationlet "S" be  ($#~v7_struct_0  "non"   ($#v7_struct_0 :::"trivial"::: )   )   ($#l6_algstr_0 :::"Ring":::); let "p", "q" be   ($#m1_subset_1 :::"Data-Location":::) "of" (Set (Const "S")); 
cluster (Set "p"  ($#k3_scmring2 :::":="::: )  "q") ->  ($#~v2_amistd_1  "non"   ($#v2_amistd_1 :::"jump-only"::: )   )  ; 
end; registrationlet "S" be  ($#~v7_struct_0  "non"   ($#v7_struct_0 :::"trivial"::: )   )   ($#l6_algstr_0 :::"Ring":::); let "p", "q" be   ($#m1_subset_1 :::"Data-Location":::) "of" (Set (Const "S")); 
cluster (Set   ($#k4_xtuple_0 :::"InsCode"::: )  (Set  "("  ($#k4_scmring2 :::"AddTo"::: )   "(" "p" "," "q" ")"  ")" )) ->  ($#~v1_amistd_1  "non"   ($#v1_amistd_1 :::"jump-only"::: )   )   for  ($#m1_subset_1 :::"InsType":::) "of" (Set  "the"  ($#u1_compos_1 :::"InstructionsF"::: )  "of" (Set  "("  ($#k1_scmring2 :::"SCM"::: )  "S" ")" )); 
end; registrationlet "S" be  ($#~v7_struct_0  "non"   ($#v7_struct_0 :::"trivial"::: )   )   ($#l6_algstr_0 :::"Ring":::); let "p", "q" be   ($#m1_subset_1 :::"Data-Location":::) "of" (Set (Const "S")); 
cluster (Set   ($#k4_scmring2 :::"AddTo"::: )   "(" "p" "," "q" ")" ) ->  ($#~v2_amistd_1  "non"   ($#v2_amistd_1 :::"jump-only"::: )   )  ; 
end; registrationlet "S" be  ($#~v7_struct_0  "non"   ($#v7_struct_0 :::"trivial"::: )   )   ($#l6_algstr_0 :::"Ring":::); let "p", "q" be   ($#m1_subset_1 :::"Data-Location":::) "of" (Set (Const "S")); 
cluster (Set   ($#k4_xtuple_0 :::"InsCode"::: )  (Set  "("  ($#k5_scmring2 :::"SubFrom"::: )   "(" "p" "," "q" ")"  ")" )) ->  ($#~v1_amistd_1  "non"   ($#v1_amistd_1 :::"jump-only"::: )   )   for  ($#m1_subset_1 :::"InsType":::) "of" (Set  "the"  ($#u1_compos_1 :::"InstructionsF"::: )  "of" (Set  "("  ($#k1_scmring2 :::"SCM"::: )  "S" ")" )); 
end; registrationlet "S" be  ($#~v7_struct_0  "non"   ($#v7_struct_0 :::"trivial"::: )   )   ($#l6_algstr_0 :::"Ring":::); let "p", "q" be   ($#m1_subset_1 :::"Data-Location":::) "of" (Set (Const "S")); 
cluster (Set   ($#k5_scmring2 :::"SubFrom"::: )   "(" "p" "," "q" ")" ) ->  ($#~v2_amistd_1  "non"   ($#v2_amistd_1 :::"jump-only"::: )   )  ; 
end; registrationlet "S" be  ($#~v7_struct_0  "non"   ($#v7_struct_0 :::"trivial"::: )   )   ($#l6_algstr_0 :::"Ring":::); let "p", "q" be   ($#m1_subset_1 :::"Data-Location":::) "of" (Set (Const "S")); 
cluster (Set   ($#k4_xtuple_0 :::"InsCode"::: )  (Set  "("  ($#k6_scmring2 :::"MultBy"::: )   "(" "p" "," "q" ")"  ")" )) ->  ($#~v1_amistd_1  "non"   ($#v1_amistd_1 :::"jump-only"::: )   )   for  ($#m1_subset_1 :::"InsType":::) "of" (Set  "the"  ($#u1_compos_1 :::"InstructionsF"::: )  "of" (Set  "("  ($#k1_scmring2 :::"SCM"::: )  "S" ")" )); 
end; registrationlet "S" be  ($#~v7_struct_0  "non"   ($#v7_struct_0 :::"trivial"::: )   )   ($#l6_algstr_0 :::"Ring":::); let "p", "q" be   ($#m1_subset_1 :::"Data-Location":::) "of" (Set (Const "S")); 
cluster (Set   ($#k6_scmring2 :::"MultBy"::: )   "(" "p" "," "q" ")" ) ->  ($#~v2_amistd_1  "non"   ($#v2_amistd_1 :::"jump-only"::: )   )  ; 
end; registrationlet "S" be  ($#~v7_struct_0  "non"   ($#v7_struct_0 :::"trivial"::: )   )   ($#l6_algstr_0 :::"Ring":::); let "p" be   ($#m1_subset_1 :::"Data-Location":::) "of" (Set (Const "S")); let "w" be   ($#m1_subset_1 :::"Element":::) "of" (Set (Const "S")); 
cluster (Set   ($#k4_xtuple_0 :::"InsCode"::: )  (Set  "(" "p"  ($#k7_scmring2 :::":="::: )  "w" ")" )) ->  ($#~v1_amistd_1  "non"   ($#v1_amistd_1 :::"jump-only"::: )   )   for  ($#m1_subset_1 :::"InsType":::) "of" (Set  "the"  ($#u1_compos_1 :::"InstructionsF"::: )  "of" (Set  "("  ($#k1_scmring2 :::"SCM"::: )  "S" ")" )); 
end; registrationlet "S" be  ($#~v7_struct_0  "non"   ($#v7_struct_0 :::"trivial"::: )   )   ($#l6_algstr_0 :::"Ring":::); let "p" be   ($#m1_subset_1 :::"Data-Location":::) "of" (Set (Const "S")); let "w" be   ($#m1_subset_1 :::"Element":::) "of" (Set (Const "S")); 
cluster (Set "p"  ($#k7_scmring2 :::":="::: )  "w") ->  ($#~v2_amistd_1  "non"   ($#v2_amistd_1 :::"jump-only"::: )   )  ; 
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" ")" ) ->  ($#~v4_amistd_1  "non"   ($#v4_amistd_1 :::"sequential"::: )   )  ; 
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") ->  ($#~v4_amistd_1  "non"   ($#v4_amistd_1 :::"sequential"::: )   )  ; 
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" ")" ) ->  ($#~v4_compos_0  "non"   ($#v4_compos_0 :::"ins-loc-free"::: )   )  ; 
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") ->  ($#~v4_compos_0  "non"   ($#v4_compos_0 :::"ins-loc-free"::: )   )  ; 
end; registrationlet "R" be   ($#l6_algstr_0 :::"Ring":::); 
cluster (Set   ($#k1_scmring2 :::"SCM"::: )  "R") ->   ($#v2_amistd_2 :::"with_explicit_jumps"::: )   ; 
end; 
theorem :: SCMRING3:37 (Bool  "for" (Set (Var "R")) "being"   ($#l6_algstr_0 :::"Ring":::)  (Bool  "for" (Set (Var "i1")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set   ($#k5_compos_0 :::"IncAddr"::: )   "(" (Set  "("  ($#k8_scmring2 :::"goto"::: )   "(" (Set (Var "i1")) "," (Set (Var "R")) ")"  ")" ) "," (Set (Var "k")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k8_scmring2 :::"goto"::: )   "(" (Set  "(" (Set (Var "i1"))  ($#k2_nat_1 :::"+"::: )  (Set (Var "k")) ")" ) "," (Set (Var "R")) ")" ))))) ; 
 
theorem :: SCMRING3:38 (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 "i1")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set   ($#k5_compos_0 :::"IncAddr"::: )   "(" (Set  "(" (Set (Var "a"))  ($#k9_scmring2 :::"=0_goto"::: )  (Set (Var "i1")) ")" ) "," (Set (Var "k")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k9_scmring2 :::"=0_goto"::: )  (Set  "(" (Set (Var "i1"))  ($#k2_nat_1 :::"+"::: )  (Set (Var "k")) ")" ))))))) ; 
 registrationlet "R" be   ($#l6_algstr_0 :::"Ring":::); 
cluster (Set   ($#k1_scmring2 :::"SCM"::: )  "R") ->   ($#v4_amistd_2 :::"IC-relocable"::: )   ; 
end; 
theorem :: SCMRING3:39 (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")) ")" ) "holds"  (Bool (Set   ($#k2_compos_0 :::"InsCode"::: )  (Set (Var "I")))  ($#r1_xxreal_0 :::"<="::: )  (Num 7)))) ;