:: SCMRING4 semantic presentation begin theorem :: SCMRING4:1 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "R")) "being" ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#l6_algstr_0 :::"Ring":::) "holds" (Bool (Set ($#k2_scmring3 :::"dl."::: ) "(" (Set (Var "R")) "," (Set (Var "n")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Num 1) "," (Set (Var "n")) ($#k1_domain_1 :::"]"::: ) )))) ; theorem :: SCMRING4:2 (Bool "for" (Set (Var "R")) "being" ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "dl")) "being" ($#m1_subset_1 :::"Data-Location":::) "of" (Set (Var "R")) (Bool "ex" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Set (Var "dl")) ($#r1_hidden :::"="::: ) (Set ($#k2_scmring3 :::"dl."::: ) "(" (Set (Var "R")) "," (Set (Var "i")) ")" ))))) ; theorem :: SCMRING4:3 (Bool "for" (Set (Var "R")) "being" ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r1_hidden :::"<>"::: ) (Set (Var "j")))) "holds" (Bool (Set ($#k2_scmring3 :::"dl."::: ) "(" (Set (Var "R")) "," (Set (Var "i")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k2_scmring3 :::"dl."::: ) "(" (Set (Var "R")) "," (Set (Var "j")) ")" )))) ; theorem :: SCMRING4:4 (Bool "for" (Set (Var "R")) "being" ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set "(" ($#k1_scmring2 :::"SCM"::: ) (Set (Var "R")) ")" ) "holds" (Bool (Set ($#k8_struct_0 :::"Data-Locations"::: ) ) ($#r1_tarski :::"c="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "s")))))) ; theorem :: SCMRING4:5 (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 "loc")) "being" ($#m2_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 (Set (Set (Var "s")) ($#k2_scmring2 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "s")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k7_memstr_0 :::"Start-At"::: ) "(" (Set (Var "loc")) "," (Set "(" ($#k1_scmring2 :::"SCM"::: ) (Set (Var "R")) ")" ) ")" ")" ) ")" ) ($#k2_scmring2 :::"."::: ) (Set (Var "a")))))))) ; theorem :: SCMRING4:6 (Bool "for" (Set (Var "R")) "being" ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "s1")) "," (Set (Var "s2")) "being" ($#m1_hidden :::"State":::) "of" (Set "(" ($#k1_scmring2 :::"SCM"::: ) (Set (Var "R")) ")" ) "st" (Bool (Bool (Set ($#k5_memstr_0 :::"IC"::: ) (Set (Var "s1"))) ($#r1_hidden :::"="::: ) (Set ($#k5_memstr_0 :::"IC"::: ) (Set (Var "s2")))) & (Bool "(" "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Data-Location":::) "of" (Set (Var "R")) "holds" (Bool (Set (Set (Var "s1")) ($#k2_scmring2 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s2")) ($#k2_scmring2 :::"."::: ) (Set (Var "a")))) ")" )) "holds" (Bool (Set (Var "s1")) ($#r8_pboole :::"="::: ) (Set (Var "s2"))))) ; registrationlet "R" be ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#l6_algstr_0 :::"Ring":::); cluster (Set ($#k1_scmring2 :::"SCM"::: ) "R") -> ($#v2_amistd_5 :::"relocable"::: ) ; end; definitionlet "R" be ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#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")); :: original: :::".-->"::: redefine func "a" :::".-->"::: "r" -> ($#m1_hidden :::"FinPartState":::) "of" (Set "(" ($#k1_scmring2 :::"SCM"::: ) "R" ")" ); end; registrationlet "R" be ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#l6_algstr_0 :::"Ring":::); cluster (Set ($#k1_scmring2 :::"SCM"::: ) "R") -> ($#v3_amistd_5 :::"IC-recognized"::: ) ; end; registrationlet "R" be ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#l6_algstr_0 :::"Ring":::); cluster (Set ($#k1_scmring2 :::"SCM"::: ) "R") -> ($#v4_amistd_5 :::"CurIns-recognized"::: ) ; end; theorem :: SCMRING4:7 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "R")) "being" ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#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 "s1")) "," (Set (Var "s2")) "being" ($#m1_hidden :::"State":::) "of" (Set "(" ($#k1_scmring2 :::"SCM"::: ) (Set (Var "R")) ")" ) (Bool "for" (Set (Var "P1")) "," (Set (Var "P2")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set "(" ($#k1_scmring2 :::"SCM"::: ) (Set (Var "R")) ")" ) (Bool "for" (Set (Var "q")) "being" (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" (Set "(" ($#k1_scmring2 :::"SCM"::: ) (Set (Var "b2")) ")" )) ($#v5_relat_1 :::"-valued"::: ) ($#v1_finset_1 :::"finite"::: ) ($#~v2_compos_1 "non" ($#v2_compos_1 :::"halt-free"::: ) ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "p")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) (Set (Var "b9")) ($#v4_extpro_1 :::"-autonomic"::: ) ($#m1_hidden :::"FinPartState":::) "of" (Set "(" ($#k1_scmring2 :::"SCM"::: ) (Set (Var "R")) ")" ) "st" (Bool (Bool (Set (Var "p")) ($#r1_tarski :::"c="::: ) (Set (Var "s1"))) & (Bool (Set (Var "p")) ($#r1_tarski :::"c="::: ) (Set (Var "s2"))) & (Bool (Set (Var "q")) ($#r1_tarski :::"c="::: ) (Set (Var "P1"))) & (Bool (Set (Var "q")) ($#r1_tarski :::"c="::: ) (Set (Var "P2"))) & (Bool (Set ($#k3_extpro_1 :::"CurInstr"::: ) "(" (Set (Var "P1")) "," (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P1")) "," (Set (Var "s1")) "," (Set (Var "n")) ")" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k3_scmring2 :::":="::: ) (Set (Var "b")))) & (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "p"))))) "holds" (Bool (Set (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P1")) "," (Set (Var "s1")) "," (Set (Var "n")) ")" ")" ) ($#k2_scmring2 :::"."::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P2")) "," (Set (Var "s2")) "," (Set (Var "n")) ")" ")" ) ($#k2_scmring2 :::"."::: ) (Set (Var "b"))))))))))) ; theorem :: SCMRING4:8 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "R")) "being" ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#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 "s1")) "," (Set (Var "s2")) "being" ($#m1_hidden :::"State":::) "of" (Set "(" ($#k1_scmring2 :::"SCM"::: ) (Set (Var "R")) ")" ) (Bool "for" (Set (Var "P1")) "," (Set (Var "P2")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set "(" ($#k1_scmring2 :::"SCM"::: ) (Set (Var "R")) ")" ) (Bool "for" (Set (Var "q")) "being" (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" (Set "(" ($#k1_scmring2 :::"SCM"::: ) (Set (Var "b2")) ")" )) ($#v5_relat_1 :::"-valued"::: ) ($#v1_finset_1 :::"finite"::: ) ($#~v2_compos_1 "non" ($#v2_compos_1 :::"halt-free"::: ) ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "p")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) (Set (Var "b9")) ($#v4_extpro_1 :::"-autonomic"::: ) ($#m1_hidden :::"FinPartState":::) "of" (Set "(" ($#k1_scmring2 :::"SCM"::: ) (Set (Var "R")) ")" ) "st" (Bool (Bool (Set (Var "p")) ($#r1_tarski :::"c="::: ) (Set (Var "s1"))) & (Bool (Set (Var "p")) ($#r1_tarski :::"c="::: ) (Set (Var "s2"))) & (Bool (Set (Var "q")) ($#r1_tarski :::"c="::: ) (Set (Var "P1"))) & (Bool (Set (Var "q")) ($#r1_tarski :::"c="::: ) (Set (Var "P2"))) & (Bool (Set ($#k3_extpro_1 :::"CurInstr"::: ) "(" (Set (Var "P1")) "," (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P1")) "," (Set (Var "s1")) "," (Set (Var "n")) ")" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_scmring2 :::"AddTo"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" )) & (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "p"))))) "holds" (Bool (Set (Set "(" (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P1")) "," (Set (Var "s1")) "," (Set (Var "n")) ")" ")" ) ($#k2_scmring2 :::"."::: ) (Set (Var "a")) ")" ) ($#k1_algstr_0 :::"+"::: ) (Set "(" (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P1")) "," (Set (Var "s1")) "," (Set (Var "n")) ")" ")" ) ($#k2_scmring2 :::"."::: ) (Set (Var "b")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P2")) "," (Set (Var "s2")) "," (Set (Var "n")) ")" ")" ) ($#k2_scmring2 :::"."::: ) (Set (Var "a")) ")" ) ($#k1_algstr_0 :::"+"::: ) (Set "(" (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P2")) "," (Set (Var "s2")) "," (Set (Var "n")) ")" ")" ) ($#k2_scmring2 :::"."::: ) (Set (Var "b")) ")" )))))))))) ; theorem :: SCMRING4:9 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "R")) "being" ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#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 "s1")) "," (Set (Var "s2")) "being" ($#m1_hidden :::"State":::) "of" (Set "(" ($#k1_scmring2 :::"SCM"::: ) (Set (Var "R")) ")" ) (Bool "for" (Set (Var "P1")) "," (Set (Var "P2")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set "(" ($#k1_scmring2 :::"SCM"::: ) (Set (Var "R")) ")" ) (Bool "for" (Set (Var "q")) "being" (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" (Set "(" ($#k1_scmring2 :::"SCM"::: ) (Set (Var "b2")) ")" )) ($#v5_relat_1 :::"-valued"::: ) ($#v1_finset_1 :::"finite"::: ) ($#~v2_compos_1 "non" ($#v2_compos_1 :::"halt-free"::: ) ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "p")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) (Set (Var "b9")) ($#v4_extpro_1 :::"-autonomic"::: ) ($#m1_hidden :::"FinPartState":::) "of" (Set "(" ($#k1_scmring2 :::"SCM"::: ) (Set (Var "R")) ")" ) "st" (Bool (Bool (Set (Var "p")) ($#r1_tarski :::"c="::: ) (Set (Var "s1"))) & (Bool (Set (Var "p")) ($#r1_tarski :::"c="::: ) (Set (Var "s2"))) & (Bool (Set (Var "q")) ($#r1_tarski :::"c="::: ) (Set (Var "P1"))) & (Bool (Set (Var "q")) ($#r1_tarski :::"c="::: ) (Set (Var "P2"))) & (Bool (Set ($#k3_extpro_1 :::"CurInstr"::: ) "(" (Set (Var "P1")) "," (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P1")) "," (Set (Var "s1")) "," (Set (Var "n")) ")" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k5_scmring2 :::"SubFrom"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" )) & (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "p"))))) "holds" (Bool (Set (Set "(" (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P1")) "," (Set (Var "s1")) "," (Set (Var "n")) ")" ")" ) ($#k2_scmring2 :::"."::: ) (Set (Var "a")) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P1")) "," (Set (Var "s1")) "," (Set (Var "n")) ")" ")" ) ($#k2_scmring2 :::"."::: ) (Set (Var "b")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P2")) "," (Set (Var "s2")) "," (Set (Var "n")) ")" ")" ) ($#k2_scmring2 :::"."::: ) (Set (Var "a")) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P2")) "," (Set (Var "s2")) "," (Set (Var "n")) ")" ")" ) ($#k2_scmring2 :::"."::: ) (Set (Var "b")) ")" )))))))))) ; theorem :: SCMRING4:10 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "R")) "being" ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#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 "s1")) "," (Set (Var "s2")) "being" ($#m1_hidden :::"State":::) "of" (Set "(" ($#k1_scmring2 :::"SCM"::: ) (Set (Var "R")) ")" ) (Bool "for" (Set (Var "P1")) "," (Set (Var "P2")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set "(" ($#k1_scmring2 :::"SCM"::: ) (Set (Var "R")) ")" ) (Bool "for" (Set (Var "q")) "being" (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" (Set "(" ($#k1_scmring2 :::"SCM"::: ) (Set (Var "b2")) ")" )) ($#v5_relat_1 :::"-valued"::: ) ($#v1_finset_1 :::"finite"::: ) ($#~v2_compos_1 "non" ($#v2_compos_1 :::"halt-free"::: ) ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "p")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) (Set (Var "b9")) ($#v4_extpro_1 :::"-autonomic"::: ) ($#m1_hidden :::"FinPartState":::) "of" (Set "(" ($#k1_scmring2 :::"SCM"::: ) (Set (Var "R")) ")" ) "st" (Bool (Bool (Set (Var "p")) ($#r1_tarski :::"c="::: ) (Set (Var "s1"))) & (Bool (Set (Var "p")) ($#r1_tarski :::"c="::: ) (Set (Var "s2"))) & (Bool (Set (Var "q")) ($#r1_tarski :::"c="::: ) (Set (Var "P1"))) & (Bool (Set (Var "q")) ($#r1_tarski :::"c="::: ) (Set (Var "P2"))) & (Bool (Set ($#k3_extpro_1 :::"CurInstr"::: ) "(" (Set (Var "P1")) "," (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P1")) "," (Set (Var "s1")) "," (Set (Var "n")) ")" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_scmring2 :::"MultBy"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" )) & (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "p"))))) "holds" (Bool (Set (Set "(" (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P1")) "," (Set (Var "s1")) "," (Set (Var "n")) ")" ")" ) ($#k2_scmring2 :::"."::: ) (Set (Var "a")) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set "(" (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P1")) "," (Set (Var "s1")) "," (Set (Var "n")) ")" ")" ) ($#k2_scmring2 :::"."::: ) (Set (Var "b")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P2")) "," (Set (Var "s2")) "," (Set (Var "n")) ")" ")" ) ($#k2_scmring2 :::"."::: ) (Set (Var "a")) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set "(" (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P2")) "," (Set (Var "s2")) "," (Set (Var "n")) ")" ")" ) ($#k2_scmring2 :::"."::: ) (Set (Var "b")) ")" )))))))))) ; theorem :: SCMRING4:11 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (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 "loc")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "s1")) "," (Set (Var "s2")) "being" ($#m1_hidden :::"State":::) "of" (Set "(" ($#k1_scmring2 :::"SCM"::: ) (Set (Var "R")) ")" ) (Bool "for" (Set (Var "P1")) "," (Set (Var "P2")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set "(" ($#k1_scmring2 :::"SCM"::: ) (Set (Var "R")) ")" ) (Bool "for" (Set (Var "q")) "being" (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" (Set "(" ($#k1_scmring2 :::"SCM"::: ) (Set (Var "b2")) ")" )) ($#v5_relat_1 :::"-valued"::: ) ($#v1_finset_1 :::"finite"::: ) ($#~v2_compos_1 "non" ($#v2_compos_1 :::"halt-free"::: ) ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "p")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) (Set (Var "b9")) ($#v4_extpro_1 :::"-autonomic"::: ) ($#m1_hidden :::"FinPartState":::) "of" (Set "(" ($#k1_scmring2 :::"SCM"::: ) (Set (Var "R")) ")" ) "st" (Bool (Bool (Set (Var "p")) ($#r1_tarski :::"c="::: ) (Set (Var "s1"))) & (Bool (Set (Var "p")) ($#r1_tarski :::"c="::: ) (Set (Var "s2"))) & (Bool (Set (Var "q")) ($#r1_tarski :::"c="::: ) (Set (Var "P1"))) & (Bool (Set (Var "q")) ($#r1_tarski :::"c="::: ) (Set (Var "P2"))) & (Bool (Set ($#k3_extpro_1 :::"CurInstr"::: ) "(" (Set (Var "P1")) "," (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P1")) "," (Set (Var "s1")) "," (Set (Var "n")) ")" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k9_scmring2 :::"=0_goto"::: ) (Set (Var "loc")))) & (Bool (Set (Var "loc")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_ordinal1 :::"succ"::: ) (Set "(" ($#k5_memstr_0 :::"IC"::: ) (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P1")) "," (Set (Var "s1")) "," (Set (Var "n")) ")" ")" ) ")" )))) "holds" (Bool "(" (Bool (Set (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P1")) "," (Set (Var "s1")) "," (Set (Var "n")) ")" ")" ) ($#k2_scmring2 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "R")))) "iff" (Bool (Set (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P2")) "," (Set (Var "s2")) "," (Set (Var "n")) ")" ")" ) ($#k2_scmring2 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "R")))) ")" ))))))))) ; begin theorem :: SCMRING4:12 (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "R")) "being" ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "s1")) "," (Set (Var "s2")) "being" ($#m1_hidden :::"State":::) "of" (Set "(" ($#k1_scmring2 :::"SCM"::: ) (Set (Var "R")) ")" ) (Bool "for" (Set (Var "q")) "being" (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" (Set "(" ($#k1_scmring2 :::"SCM"::: ) (Set (Var "b2")) ")" )) ($#v5_relat_1 :::"-valued"::: ) ($#v1_finset_1 :::"finite"::: ) ($#~v2_compos_1 "non" ($#v2_compos_1 :::"halt-free"::: ) ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "p")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) (Set (Var "b5")) ($#v4_extpro_1 :::"-autonomic"::: ) ($#m1_hidden :::"FinPartState":::) "of" (Set "(" ($#k1_scmring2 :::"SCM"::: ) (Set (Var "R")) ")" ) "st" (Bool (Bool (Set (Var "p")) ($#r1_tarski :::"c="::: ) (Set (Var "s1"))) & (Bool (Set ($#k9_memstr_0 :::"IncIC"::: ) "(" (Set (Var "p")) "," (Set (Var "k")) ")" ) ($#r1_tarski :::"c="::: ) (Set (Var "s2")))) "holds" (Bool "for" (Set (Var "P1")) "," (Set (Var "P2")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set "(" ($#k1_scmring2 :::"SCM"::: ) (Set (Var "R")) ")" ) "st" (Bool (Bool (Set (Var "q")) ($#r1_tarski :::"c="::: ) (Set (Var "P1"))) & (Bool (Set ($#k6_compos_1 :::"Reloc"::: ) "(" (Set (Var "q")) "," (Set (Var "k")) ")" ) ($#r1_tarski :::"c="::: ) (Set (Var "P2")))) "holds" (Bool "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set (Set "(" ($#k5_memstr_0 :::"IC"::: ) (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P1")) "," (Set (Var "s1")) "," (Set (Var "i")) ")" ")" ) ")" ) ($#k2_nat_1 :::"+"::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set ($#k5_memstr_0 :::"IC"::: ) (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P2")) "," (Set (Var "s2")) "," (Set (Var "i")) ")" ")" ))) & (Bool (Set ($#k5_compos_0 :::"IncAddr"::: ) "(" (Set "(" ($#k3_extpro_1 :::"CurInstr"::: ) "(" (Set (Var "P1")) "," (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P1")) "," (Set (Var "s1")) "," (Set (Var "i")) ")" ")" ) ")" ")" ) "," (Set (Var "k")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k3_extpro_1 :::"CurInstr"::: ) "(" (Set (Var "P2")) "," (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P2")) "," (Set (Var "s2")) "," (Set (Var "i")) ")" ")" ) ")" )) & (Bool (Set (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P1")) "," (Set (Var "s1")) "," (Set (Var "i")) ")" ")" ) ($#k5_relat_1 :::"|"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k6_memstr_0 :::"DataPart"::: ) (Set (Var "p")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P2")) "," (Set (Var "s2")) "," (Set (Var "i")) ")" ")" ) ($#k5_relat_1 :::"|"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k6_memstr_0 :::"DataPart"::: ) (Set (Var "p")) ")" ) ")" ))) & (Bool (Set ($#k6_memstr_0 :::"DataPart"::: ) (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P1")) "," (Set "(" (Set (Var "s1")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k6_memstr_0 :::"DataPart"::: ) (Set (Var "s2")) ")" ) ")" ) "," (Set (Var "i")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_memstr_0 :::"DataPart"::: ) (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P2")) "," (Set (Var "s2")) "," (Set (Var "i")) ")" ")" ))) ")" )))))))) ; registrationlet "R" be ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#l6_algstr_0 :::"Ring":::); cluster (Set ($#k1_scmring2 :::"SCM"::: ) "R") -> ($#v5_amistd_5 :::"relocable1"::: ) ($#v6_amistd_5 :::"relocable2"::: ) ; end;