:: SCMRING2 semantic presentation begin definition let R be Ring; func SCM R -> strict AMI-Struct over 2 means :Def1: :: SCMRING2:def 1 ( the carrier of it = SCM-Memory & the ZeroF of it = NAT & the InstructionsF of it = SCM-Instr R & the Object-Kind of it = SCM-OK & the ValuesF of it = SCM-VAL R & the Execution of it = SCM-Exec R ); existence ex b1 being strict AMI-Struct over 2 st ( the carrier of b1 = SCM-Memory & the ZeroF of b1 = NAT & the InstructionsF of b1 = SCM-Instr R & the Object-Kind of b1 = SCM-OK & the ValuesF of b1 = SCM-VAL R & the Execution of b1 = SCM-Exec R ) proof take AMI-Struct(# SCM-Memory,(In (NAT,SCM-Memory)),(SCM-Instr R),SCM-OK,(SCM-VAL R),(SCM-Exec R) #) ; ::_thesis: ( the carrier of AMI-Struct(# SCM-Memory,(In (NAT,SCM-Memory)),(SCM-Instr R),SCM-OK,(SCM-VAL R),(SCM-Exec R) #) = SCM-Memory & the ZeroF of AMI-Struct(# SCM-Memory,(In (NAT,SCM-Memory)),(SCM-Instr R),SCM-OK,(SCM-VAL R),(SCM-Exec R) #) = NAT & the InstructionsF of AMI-Struct(# SCM-Memory,(In (NAT,SCM-Memory)),(SCM-Instr R),SCM-OK,(SCM-VAL R),(SCM-Exec R) #) = SCM-Instr R & the Object-Kind of AMI-Struct(# SCM-Memory,(In (NAT,SCM-Memory)),(SCM-Instr R),SCM-OK,(SCM-VAL R),(SCM-Exec R) #) = SCM-OK & the ValuesF of AMI-Struct(# SCM-Memory,(In (NAT,SCM-Memory)),(SCM-Instr R),SCM-OK,(SCM-VAL R),(SCM-Exec R) #) = SCM-VAL R & the Execution of AMI-Struct(# SCM-Memory,(In (NAT,SCM-Memory)),(SCM-Instr R),SCM-OK,(SCM-VAL R),(SCM-Exec R) #) = SCM-Exec R ) thus ( the carrier of AMI-Struct(# SCM-Memory,(In (NAT,SCM-Memory)),(SCM-Instr R),SCM-OK,(SCM-VAL R),(SCM-Exec R) #) = SCM-Memory & the ZeroF of AMI-Struct(# SCM-Memory,(In (NAT,SCM-Memory)),(SCM-Instr R),SCM-OK,(SCM-VAL R),(SCM-Exec R) #) = NAT & the InstructionsF of AMI-Struct(# SCM-Memory,(In (NAT,SCM-Memory)),(SCM-Instr R),SCM-OK,(SCM-VAL R),(SCM-Exec R) #) = SCM-Instr R & the Object-Kind of AMI-Struct(# SCM-Memory,(In (NAT,SCM-Memory)),(SCM-Instr R),SCM-OK,(SCM-VAL R),(SCM-Exec R) #) = SCM-OK & the ValuesF of AMI-Struct(# SCM-Memory,(In (NAT,SCM-Memory)),(SCM-Instr R),SCM-OK,(SCM-VAL R),(SCM-Exec R) #) = SCM-VAL R & the Execution of AMI-Struct(# SCM-Memory,(In (NAT,SCM-Memory)),(SCM-Instr R),SCM-OK,(SCM-VAL R),(SCM-Exec R) #) = SCM-Exec R ) by AMI_2:22, FUNCT_7:def_1; ::_thesis: verum end; uniqueness for b1, b2 being strict AMI-Struct over 2 st the carrier of b1 = SCM-Memory & the ZeroF of b1 = NAT & the InstructionsF of b1 = SCM-Instr R & the Object-Kind of b1 = SCM-OK & the ValuesF of b1 = SCM-VAL R & the Execution of b1 = SCM-Exec R & the carrier of b2 = SCM-Memory & the ZeroF of b2 = NAT & the InstructionsF of b2 = SCM-Instr R & the Object-Kind of b2 = SCM-OK & the ValuesF of b2 = SCM-VAL R & the Execution of b2 = SCM-Exec R holds b1 = b2 ; end; :: deftheorem Def1 defines SCM SCMRING2:def_1_:_ for R being Ring for b2 being strict AMI-Struct over 2 holds ( b2 = SCM R iff ( the carrier of b2 = SCM-Memory & the ZeroF of b2 = NAT & the InstructionsF of b2 = SCM-Instr R & the Object-Kind of b2 = SCM-OK & the ValuesF of b2 = SCM-VAL R & the Execution of b2 = SCM-Exec R ) ); registration let R be Ring; cluster SCM R -> non empty strict ; coherence not SCM R is empty by Def1; end; Lm1: now__::_thesis:_for_R_being_Ring_holds_the_Values_of_(SCM_R)_=_(SCM-VAL_R)_*_SCM-OK let R be Ring; ::_thesis: the_Values_of (SCM R) = (SCM-VAL R) * SCM-OK thus the_Values_of (SCM R) = the ValuesF of (SCM R) * the Object-Kind of (SCM R) .= the ValuesF of (SCM R) * SCM-OK by Def1 .= (SCM-VAL R) * SCM-OK by Def1 ; ::_thesis: verum end; registration let R be Ring; cluster SCM R -> with_non-empty_values strict ; coherence SCM R is with_non-empty_values proof the_Values_of (SCM R) = (SCM-VAL R) * SCM-OK by Lm1; hence the_Values_of (SCM R) is non-empty ; :: according to MEMSTR_0:def_3 ::_thesis: verum end; end; Lm2: for R being Ring holds the carrier of (SCM R) \ {NAT} = SCM-Data-Loc proof let R be Ring; ::_thesis: the carrier of (SCM R) \ {NAT} = SCM-Data-Loc A1: not NAT in SCM-Data-Loc by AMI_2:20; thus the carrier of (SCM R) \ {NAT} = SCM-Memory \ {NAT} by Def1 .= ({NAT} \/ SCM-Data-Loc) \ {NAT} .= SCM-Data-Loc by A1, ZFMISC_1:117 ; ::_thesis: verum end; registration let R be Ring; cluster Int-like for Element of the carrier of (SCM R); existence ex b1 being Object of (SCM R) st b1 is Int-like proof the carrier of (SCM R) = SCM-Memory by Def1; then reconsider x = the Element of SCM-Data-Loc as Object of (SCM R) ; take x ; ::_thesis: x is Int-like thus x is Int-like by AMI_2:def_16; ::_thesis: verum end; end; definition let R be Ring; mode Data-Location of R is Int-like Object of (SCM R); canceled; end; :: deftheorem SCMRING2:def_2_:_ canceled; theorem Th1: :: SCMRING2:1 for x being set for R being Ring holds ( x is Data-Location of R iff x in Data-Locations ) by Def1, AMI_2:def_16, AMI_3:27; definition let R be Ring; let s be State of (SCM R); let a be Data-Location of R; :: original: . redefine funcs . a -> Element of R; coherence s . a is Element of R proof the_Values_of (SCM R) = (SCM-VAL R) * SCM-OK by Lm1; then reconsider S = s as SCM-State of R by CARD_3:107; a is Element of Data-Locations by Th1; then reconsider a = a as Element of SCM-Data-Loc by AMI_3:27; S . a in the carrier of R ; hence s . a is Element of R ; ::_thesis: verum end; end; theorem :: SCMRING2:2 for R being Ring holds [0,{},{}] is Instruction of (SCM R) proof let R be Ring; ::_thesis: [0,{},{}] is Instruction of (SCM R) halt (SCM R) = [0,{},{}] ; hence [0,{},{}] is Instruction of (SCM R) ; ::_thesis: verum end; theorem Th3: :: SCMRING2:3 for S being non empty 1-sorted for x being set for R being Ring for d1, d2 being Data-Location of R st x in {1,2,3,4} holds [x,{},<*d1,d2*>] in SCM-Instr S proof let S be non empty 1-sorted ; ::_thesis: for x being set for R being Ring for d1, d2 being Data-Location of R st x in {1,2,3,4} holds [x,{},<*d1,d2*>] in SCM-Instr S let x be set ; ::_thesis: for R being Ring for d1, d2 being Data-Location of R st x in {1,2,3,4} holds [x,{},<*d1,d2*>] in SCM-Instr S let R be Ring; ::_thesis: for d1, d2 being Data-Location of R st x in {1,2,3,4} holds [x,{},<*d1,d2*>] in SCM-Instr S let d1, d2 be Data-Location of R; ::_thesis: ( x in {1,2,3,4} implies [x,{},<*d1,d2*>] in SCM-Instr S ) reconsider d1 = d1, d2 = d2 as Element of SCM-Data-Loc by Th1, AMI_3:27; ( x in {1,2,3,4} implies [x,{},<*d1,d2*>] in SCM-Instr S ) by SCMRINGI:8; hence ( x in {1,2,3,4} implies [x,{},<*d1,d2*>] in SCM-Instr S ) ; ::_thesis: verum end; theorem Th4: :: SCMRING2:4 for S being non empty 1-sorted for t being Element of S for R being Ring for d1 being Data-Location of R holds [5,{},<*d1,t*>] in SCM-Instr S proof let S be non empty 1-sorted ; ::_thesis: for t being Element of S for R being Ring for d1 being Data-Location of R holds [5,{},<*d1,t*>] in SCM-Instr S let t be Element of S; ::_thesis: for R being Ring for d1 being Data-Location of R holds [5,{},<*d1,t*>] in SCM-Instr S let R be Ring; ::_thesis: for d1 being Data-Location of R holds [5,{},<*d1,t*>] in SCM-Instr S let d1 be Data-Location of R; ::_thesis: [5,{},<*d1,t*>] in SCM-Instr S reconsider d1 = d1 as Element of SCM-Data-Loc by Th1, AMI_3:27; [5,{},<*d1,t*>] in SCM-Instr S by SCMRINGI:9; hence [5,{},<*d1,t*>] in SCM-Instr S ; ::_thesis: verum end; theorem Th5: :: SCMRING2:5 for S being non empty 1-sorted for i1 being Element of NAT holds [6,<*i1*>,{}] in SCM-Instr S by SCMRINGI:10; theorem Th6: :: SCMRING2:6 for S being non empty 1-sorted for R being Ring for d1 being Data-Location of R for i1 being Element of NAT holds [7,<*i1*>,<*d1*>] in SCM-Instr S proof let S be non empty 1-sorted ; ::_thesis: for R being Ring for d1 being Data-Location of R for i1 being Element of NAT holds [7,<*i1*>,<*d1*>] in SCM-Instr S let R be Ring; ::_thesis: for d1 being Data-Location of R for i1 being Element of NAT holds [7,<*i1*>,<*d1*>] in SCM-Instr S let d1 be Data-Location of R; ::_thesis: for i1 being Element of NAT holds [7,<*i1*>,<*d1*>] in SCM-Instr S let i1 be Element of NAT ; ::_thesis: [7,<*i1*>,<*d1*>] in SCM-Instr S reconsider d1 = d1 as Element of SCM-Data-Loc by Th1, AMI_3:27; [7,<*i1*>,<*d1*>] in SCM-Instr S by SCMRINGI:11; hence [7,<*i1*>,<*d1*>] in SCM-Instr S ; ::_thesis: verum end; definition let R be Ring; let a, b be Data-Location of R; funca := b -> Instruction of (SCM R) equals :: SCMRING2:def 3 [1,{},<*a,b*>]; coherence [1,{},<*a,b*>] is Instruction of (SCM R) proof 1 in {1,2,3,4} by ENUMSET1:def_2; then [1,{},<*a,b*>] in SCM-Instr R by Th3; hence [1,{},<*a,b*>] is Instruction of (SCM R) by Def1; ::_thesis: verum end; func AddTo (a,b) -> Instruction of (SCM R) equals :: SCMRING2:def 4 [2,{},<*a,b*>]; coherence [2,{},<*a,b*>] is Instruction of (SCM R) proof 2 in {1,2,3,4} by ENUMSET1:def_2; then [2,{},<*a,b*>] in SCM-Instr R by Th3; hence [2,{},<*a,b*>] is Instruction of (SCM R) by Def1; ::_thesis: verum end; func SubFrom (a,b) -> Instruction of (SCM R) equals :: SCMRING2:def 5 [3,{},<*a,b*>]; coherence [3,{},<*a,b*>] is Instruction of (SCM R) proof 3 in {1,2,3,4} by ENUMSET1:def_2; then [3,{},<*a,b*>] in SCM-Instr R by Th3; hence [3,{},<*a,b*>] is Instruction of (SCM R) by Def1; ::_thesis: verum end; func MultBy (a,b) -> Instruction of (SCM R) equals :: SCMRING2:def 6 [4,{},<*a,b*>]; coherence [4,{},<*a,b*>] is Instruction of (SCM R) proof 4 in {1,2,3,4} by ENUMSET1:def_2; then [4,{},<*a,b*>] in SCM-Instr R by Th3; hence [4,{},<*a,b*>] is Instruction of (SCM R) by Def1; ::_thesis: verum end; end; :: deftheorem defines := SCMRING2:def_3_:_ for R being Ring for a, b being Data-Location of R holds a := b = [1,{},<*a,b*>]; :: deftheorem defines AddTo SCMRING2:def_4_:_ for R being Ring for a, b being Data-Location of R holds AddTo (a,b) = [2,{},<*a,b*>]; :: deftheorem defines SubFrom SCMRING2:def_5_:_ for R being Ring for a, b being Data-Location of R holds SubFrom (a,b) = [3,{},<*a,b*>]; :: deftheorem defines MultBy SCMRING2:def_6_:_ for R being Ring for a, b being Data-Location of R holds MultBy (a,b) = [4,{},<*a,b*>]; definition let R be Ring; let a be Data-Location of R; let r be Element of R; funca := r -> Instruction of (SCM R) equals :: SCMRING2:def 7 [5,{},<*a,r*>]; coherence [5,{},<*a,r*>] is Instruction of (SCM R) proof [5,{},<*a,r*>] in SCM-Instr R by Th4; hence [5,{},<*a,r*>] is Instruction of (SCM R) by Def1; ::_thesis: verum end; end; :: deftheorem defines := SCMRING2:def_7_:_ for R being Ring for a being Data-Location of R for r being Element of R holds a := r = [5,{},<*a,r*>]; definition let R be Ring; let l be Element of NAT ; func goto (l,R) -> Instruction of (SCM R) equals :: SCMRING2:def 8 [6,<*l*>,{}]; coherence [6,<*l*>,{}] is Instruction of (SCM R) proof [6,<*l*>,{}] in SCM-Instr R by Th5; hence [6,<*l*>,{}] is Instruction of (SCM R) by Def1; ::_thesis: verum end; end; :: deftheorem defines goto SCMRING2:def_8_:_ for R being Ring for l being Element of NAT holds goto (l,R) = [6,<*l*>,{}]; definition let R be Ring; let l be Element of NAT ; let a be Data-Location of R; funca =0_goto l -> Instruction of (SCM R) equals :: SCMRING2:def 9 [7,<*l*>,<*a*>]; coherence [7,<*l*>,<*a*>] is Instruction of (SCM R) proof [7,<*l*>,<*a*>] in SCM-Instr R by Th6; hence [7,<*l*>,<*a*>] is Instruction of (SCM R) by Def1; ::_thesis: verum end; end; :: deftheorem defines =0_goto SCMRING2:def_9_:_ for R being Ring for l being Element of NAT for a being Data-Location of R holds a =0_goto l = [7,<*l*>,<*a*>]; theorem Th7: :: SCMRING2:7 for R being Ring for I being set holds ( I is Instruction of (SCM R) iff ( I = [0,{},{}] or ex a, b being Data-Location of R st I = a := b or ex a, b being Data-Location of R st I = AddTo (a,b) or ex a, b being Data-Location of R st I = SubFrom (a,b) or ex a, b being Data-Location of R st I = MultBy (a,b) or ex i1 being Element of NAT st I = goto (i1,R) or ex a being Data-Location of R ex i1 being Element of NAT st I = a =0_goto i1 or ex a being Data-Location of R ex r being Element of R st I = a := r ) ) proof let R be Ring; ::_thesis: for I being set holds ( I is Instruction of (SCM R) iff ( I = [0,{},{}] or ex a, b being Data-Location of R st I = a := b or ex a, b being Data-Location of R st I = AddTo (a,b) or ex a, b being Data-Location of R st I = SubFrom (a,b) or ex a, b being Data-Location of R st I = MultBy (a,b) or ex i1 being Element of NAT st I = goto (i1,R) or ex a being Data-Location of R ex i1 being Element of NAT st I = a =0_goto i1 or ex a being Data-Location of R ex r being Element of R st I = a := r ) ) let J be set ; ::_thesis: ( J is Instruction of (SCM R) iff ( J = [0,{},{}] or ex a, b being Data-Location of R st J = a := b or ex a, b being Data-Location of R st J = AddTo (a,b) or ex a, b being Data-Location of R st J = SubFrom (a,b) or ex a, b being Data-Location of R st J = MultBy (a,b) or ex i1 being Element of NAT st J = goto (i1,R) or ex a being Data-Location of R ex i1 being Element of NAT st J = a =0_goto i1 or ex a being Data-Location of R ex r being Element of R st J = a := r ) ) A1: the InstructionsF of (SCM R) = SCM-Instr R by Def1; thus ( not J is Instruction of (SCM R) or J = [0,{},{}] or ex a, b being Data-Location of R st J = a := b or ex a, b being Data-Location of R st J = AddTo (a,b) or ex a, b being Data-Location of R st J = SubFrom (a,b) or ex a, b being Data-Location of R st J = MultBy (a,b) or ex i1 being Element of NAT st J = goto (i1,R) or ex a being Data-Location of R ex i1 being Element of NAT st J = a =0_goto i1 or ex a being Data-Location of R ex r being Element of R st J = a := r ) ::_thesis: ( ( J = [0,{},{}] or ex a, b being Data-Location of R st J = a := b or ex a, b being Data-Location of R st J = AddTo (a,b) or ex a, b being Data-Location of R st J = SubFrom (a,b) or ex a, b being Data-Location of R st J = MultBy (a,b) or ex i1 being Element of NAT st J = goto (i1,R) or ex a being Data-Location of R ex i1 being Element of NAT st J = a =0_goto i1 or ex a being Data-Location of R ex r being Element of R st J = a := r ) implies J is Instruction of (SCM R) ) proof assume J is Instruction of (SCM R) ; ::_thesis: ( J = [0,{},{}] or ex a, b being Data-Location of R st J = a := b or ex a, b being Data-Location of R st J = AddTo (a,b) or ex a, b being Data-Location of R st J = SubFrom (a,b) or ex a, b being Data-Location of R st J = MultBy (a,b) or ex i1 being Element of NAT st J = goto (i1,R) or ex a being Data-Location of R ex i1 being Element of NAT st J = a =0_goto i1 or ex a being Data-Location of R ex r being Element of R st J = a := r ) then ( J in (({[0,{},{}]} \/ { [I,{},<*a,b*>] where I is Element of Segm 8, a, b is Element of Data-Locations : I in {1,2,3,4} } ) \/ { [6,<*i*>,{}] where i is Element of NAT : verum } ) \/ { [7,<*i*>,<*a*>] where i is Element of NAT , a is Element of Data-Locations : verum } or J in { [5,{},<*a,r*>] where a is Element of Data-Locations , r is Element of R : verum } ) by A1, AMI_3:27, XBOOLE_0:def_3; then ( J in ({[0,{},{}]} \/ { [I,{},<*a,b*>] where I is Element of Segm 8, a, b is Element of Data-Locations : I in {1,2,3,4} } ) \/ { [6,<*i*>,{}] where i is Element of NAT : verum } or J in { [7,<*i*>,<*a*>] where i is Element of NAT , a is Element of Data-Locations : verum } or J in { [5,{},<*a,r*>] where a is Element of Data-Locations , r is Element of R : verum } ) by XBOOLE_0:def_3; then A2: ( J in {[0,{},{}]} \/ { [I,{},<*a,b*>] where I is Element of Segm 8, a, b is Element of Data-Locations : I in {1,2,3,4} } or J in { [6,<*i*>,{}] where i is Element of NAT : verum } or J in { [7,<*i*>,<*a*>] where i is Element of NAT , a is Element of Data-Locations : verum } or J in { [5,{},<*a,r*>] where a is Element of Data-Locations , r is Element of R : verum } ) by XBOOLE_0:def_3; percases ( J in {[0,{},{}]} or J in { [6,<*i*>,{}] where i is Element of NAT : verum } or J in { [7,<*i*>,<*a*>] where i is Element of NAT , a is Element of Data-Locations : verum } or J in { [5,{},<*a,r*>] where a is Element of Data-Locations , r is Element of R : verum } or J in { [I,{},<*a,b*>] where I is Element of Segm 8, a, b is Element of Data-Locations : I in {1,2,3,4} } ) by A2, XBOOLE_0:def_3; suppose J in {[0,{},{}]} ; ::_thesis: ( J = [0,{},{}] or ex a, b being Data-Location of R st J = a := b or ex a, b being Data-Location of R st J = AddTo (a,b) or ex a, b being Data-Location of R st J = SubFrom (a,b) or ex a, b being Data-Location of R st J = MultBy (a,b) or ex i1 being Element of NAT st J = goto (i1,R) or ex a being Data-Location of R ex i1 being Element of NAT st J = a =0_goto i1 or ex a being Data-Location of R ex r being Element of R st J = a := r ) hence ( J = [0,{},{}] or ex a, b being Data-Location of R st J = a := b or ex a, b being Data-Location of R st J = AddTo (a,b) or ex a, b being Data-Location of R st J = SubFrom (a,b) or ex a, b being Data-Location of R st J = MultBy (a,b) or ex i1 being Element of NAT st J = goto (i1,R) or ex a being Data-Location of R ex i1 being Element of NAT st J = a =0_goto i1 or ex a being Data-Location of R ex r being Element of R st J = a := r ) by TARSKI:def_1; ::_thesis: verum end; suppose J in { [6,<*i*>,{}] where i is Element of NAT : verum } ; ::_thesis: ( J = [0,{},{}] or ex a, b being Data-Location of R st J = a := b or ex a, b being Data-Location of R st J = AddTo (a,b) or ex a, b being Data-Location of R st J = SubFrom (a,b) or ex a, b being Data-Location of R st J = MultBy (a,b) or ex i1 being Element of NAT st J = goto (i1,R) or ex a being Data-Location of R ex i1 being Element of NAT st J = a =0_goto i1 or ex a being Data-Location of R ex r being Element of R st J = a := r ) then consider i being Element of NAT such that A3: J = [6,<*i*>,{}] and verum ; reconsider i = i as Element of NAT ; J = goto (i,R) by A3; hence ( J = [0,{},{}] or ex a, b being Data-Location of R st J = a := b or ex a, b being Data-Location of R st J = AddTo (a,b) or ex a, b being Data-Location of R st J = SubFrom (a,b) or ex a, b being Data-Location of R st J = MultBy (a,b) or ex i1 being Element of NAT st J = goto (i1,R) or ex a being Data-Location of R ex i1 being Element of NAT st J = a =0_goto i1 or ex a being Data-Location of R ex r being Element of R st J = a := r ) ; ::_thesis: verum end; suppose J in { [7,<*i*>,<*a*>] where i is Element of NAT , a is Element of Data-Locations : verum } ; ::_thesis: ( J = [0,{},{}] or ex a, b being Data-Location of R st J = a := b or ex a, b being Data-Location of R st J = AddTo (a,b) or ex a, b being Data-Location of R st J = SubFrom (a,b) or ex a, b being Data-Location of R st J = MultBy (a,b) or ex i1 being Element of NAT st J = goto (i1,R) or ex a being Data-Location of R ex i1 being Element of NAT st J = a =0_goto i1 or ex a being Data-Location of R ex r being Element of R st J = a := r ) then consider i being Element of NAT , a being Element of Data-Locations such that A4: J = [7,<*i*>,<*a*>] and verum ; reconsider A = a as Data-Location of R by Th1, AMI_3:27; reconsider I = i as Element of NAT ; J = A =0_goto I by A4; hence ( J = [0,{},{}] or ex a, b being Data-Location of R st J = a := b or ex a, b being Data-Location of R st J = AddTo (a,b) or ex a, b being Data-Location of R st J = SubFrom (a,b) or ex a, b being Data-Location of R st J = MultBy (a,b) or ex i1 being Element of NAT st J = goto (i1,R) or ex a being Data-Location of R ex i1 being Element of NAT st J = a =0_goto i1 or ex a being Data-Location of R ex r being Element of R st J = a := r ) ; ::_thesis: verum end; suppose J in { [5,{},<*a,r*>] where a is Element of Data-Locations , r is Element of R : verum } ; ::_thesis: ( J = [0,{},{}] or ex a, b being Data-Location of R st J = a := b or ex a, b being Data-Location of R st J = AddTo (a,b) or ex a, b being Data-Location of R st J = SubFrom (a,b) or ex a, b being Data-Location of R st J = MultBy (a,b) or ex i1 being Element of NAT st J = goto (i1,R) or ex a being Data-Location of R ex i1 being Element of NAT st J = a =0_goto i1 or ex a being Data-Location of R ex r being Element of R st J = a := r ) then consider a being Element of Data-Locations , r being Element of R such that A5: J = [5,{},<*a,r*>] and verum ; reconsider A = a as Data-Location of R by Th1, AMI_3:27; J = A := r by A5; hence ( J = [0,{},{}] or ex a, b being Data-Location of R st J = a := b or ex a, b being Data-Location of R st J = AddTo (a,b) or ex a, b being Data-Location of R st J = SubFrom (a,b) or ex a, b being Data-Location of R st J = MultBy (a,b) or ex i1 being Element of NAT st J = goto (i1,R) or ex a being Data-Location of R ex i1 being Element of NAT st J = a =0_goto i1 or ex a being Data-Location of R ex r being Element of R st J = a := r ) ; ::_thesis: verum end; suppose J in { [I,{},<*a,b*>] where I is Element of Segm 8, a, b is Element of Data-Locations : I in {1,2,3,4} } ; ::_thesis: ( J = [0,{},{}] or ex a, b being Data-Location of R st J = a := b or ex a, b being Data-Location of R st J = AddTo (a,b) or ex a, b being Data-Location of R st J = SubFrom (a,b) or ex a, b being Data-Location of R st J = MultBy (a,b) or ex i1 being Element of NAT st J = goto (i1,R) or ex a being Data-Location of R ex i1 being Element of NAT st J = a =0_goto i1 or ex a being Data-Location of R ex r being Element of R st J = a := r ) then consider I being Element of Segm 8, a, b being Element of Data-Locations such that A6: ( J = [I,{},<*a,b*>] & I in {1,2,3,4} ) ; reconsider A = a, B = b as Data-Location of R by Th1, AMI_3:27; ( J = A := B or J = AddTo (A,B) or J = SubFrom (A,B) or J = MultBy (A,B) ) by A6, ENUMSET1:def_2; hence ( J = [0,{},{}] or ex a, b being Data-Location of R st J = a := b or ex a, b being Data-Location of R st J = AddTo (a,b) or ex a, b being Data-Location of R st J = SubFrom (a,b) or ex a, b being Data-Location of R st J = MultBy (a,b) or ex i1 being Element of NAT st J = goto (i1,R) or ex a being Data-Location of R ex i1 being Element of NAT st J = a =0_goto i1 or ex a being Data-Location of R ex r being Element of R st J = a := r ) ; ::_thesis: verum end; end; end; thus ( ( J = [0,{},{}] or ex a, b being Data-Location of R st J = a := b or ex a, b being Data-Location of R st J = AddTo (a,b) or ex a, b being Data-Location of R st J = SubFrom (a,b) or ex a, b being Data-Location of R st J = MultBy (a,b) or ex i1 being Element of NAT st J = goto (i1,R) or ex a being Data-Location of R ex i1 being Element of NAT st J = a =0_goto i1 or ex a being Data-Location of R ex r being Element of R st J = a := r ) implies J is Instruction of (SCM R) ) by A1, SCMRINGI:6; ::_thesis: verum end; registration let R be Ring; cluster SCM R -> IC-Ins-separated strict ; coherence SCM R is IC-Ins-separated proof A1: the_Values_of (SCM R) = (SCM-VAL R) * SCM-OK by Lm1; IC = NAT by Def1; then Values (IC ) = NAT by A1, SCMRING1:2; hence SCM R is IC-Ins-separated by MEMSTR_0:def_6; ::_thesis: verum end; end; theorem :: SCMRING2:8 for R being Ring holds IC = NAT by Def1; theorem :: SCMRING2:9 for R being Ring for s being State of (SCM R) for S being SCM-State of R st S = s holds IC s = IC S by Def1; theorem Th10: :: SCMRING2:10 for R being Ring for s being State of (SCM R) for I being Instruction of (SCM R) for i being Element of SCM-Instr R st i = I holds for S being SCM-State of R st S = s holds Exec (I,s) = SCM-Exec-Res (i,S) proof let R be Ring; ::_thesis: for s being State of (SCM R) for I being Instruction of (SCM R) for i being Element of SCM-Instr R st i = I holds for S being SCM-State of R st S = s holds Exec (I,s) = SCM-Exec-Res (i,S) let s be State of (SCM R); ::_thesis: for I being Instruction of (SCM R) for i being Element of SCM-Instr R st i = I holds for S being SCM-State of R st S = s holds Exec (I,s) = SCM-Exec-Res (i,S) let I be Instruction of (SCM R); ::_thesis: for i being Element of SCM-Instr R st i = I holds for S being SCM-State of R st S = s holds Exec (I,s) = SCM-Exec-Res (i,S) let i be Element of SCM-Instr R; ::_thesis: ( i = I implies for S being SCM-State of R st S = s holds Exec (I,s) = SCM-Exec-Res (i,S) ) assume A1: i = I ; ::_thesis: for S being SCM-State of R st S = s holds Exec (I,s) = SCM-Exec-Res (i,S) let S be SCM-State of R; ::_thesis: ( S = s implies Exec (I,s) = SCM-Exec-Res (i,S) ) assume S = s ; ::_thesis: Exec (I,s) = SCM-Exec-Res (i,S) hence Exec (I,s) = ((SCM-Exec R) . i) . S by A1, Def1 .= SCM-Exec-Res (i,S) by SCMRING1:def_15 ; ::_thesis: verum end; begin theorem Th11: :: SCMRING2:11 for R being Ring for a, b being Data-Location of R for s being State of (SCM R) holds ( (Exec ((a := b),s)) . (IC ) = succ (IC s) & (Exec ((a := b),s)) . a = s . b & ( for c being Data-Location of R st c <> a holds (Exec ((a := b),s)) . c = s . c ) ) proof let R be Ring; ::_thesis: for a, b being Data-Location of R for s being State of (SCM R) holds ( (Exec ((a := b),s)) . (IC ) = succ (IC s) & (Exec ((a := b),s)) . a = s . b & ( for c being Data-Location of R st c <> a holds (Exec ((a := b),s)) . c = s . c ) ) let a, b be Data-Location of R; ::_thesis: for s being State of (SCM R) holds ( (Exec ((a := b),s)) . (IC ) = succ (IC s) & (Exec ((a := b),s)) . a = s . b & ( for c being Data-Location of R st c <> a holds (Exec ((a := b),s)) . c = s . c ) ) let s be State of (SCM R); ::_thesis: ( (Exec ((a := b),s)) . (IC ) = succ (IC s) & (Exec ((a := b),s)) . a = s . b & ( for c being Data-Location of R st c <> a holds (Exec ((a := b),s)) . c = s . c ) ) A1: a is Element of Data-Locations by Th1; A2: the_Values_of (SCM R) = (SCM-VAL R) * SCM-OK by Lm1; reconsider S = s as SCM-State of R by A2, CARD_3:107; reconsider I = a := b as Element of SCM-Instr R by Def1; set S1 = SCM-Chg (S,(I address_1),(S . (I address_2))); reconsider i = 1 as Element of Segm 8 by NAT_1:44; A3: IC s = IC S by Def1; A4: b is Element of Data-Locations by Th1; A5: Exec ((a := b),s) = SCM-Exec-Res (I,S) by Th10 .= SCM-Chg ((SCM-Chg (S,(I address_1),(S . (I address_2)))),(succ (IC S))) by A1, A4, AMI_3:27, SCMRING1:def_14 ; A6: I = [i,{},<*a,b*>] ; then A7: I address_1 = a by A1, A4, AMI_3:27, SCMRINGI:1; A8: I address_2 = b by A6, A1, A4, AMI_3:27, SCMRINGI:1; thus (Exec ((a := b),s)) . (IC ) = (Exec ((a := b),s)) . NAT by Def1 .= succ (IC s) by A3, A5, SCMRING1:7 ; ::_thesis: ( (Exec ((a := b),s)) . a = s . b & ( for c being Data-Location of R st c <> a holds (Exec ((a := b),s)) . c = s . c ) ) thus (Exec ((a := b),s)) . a = (SCM-Chg (S,(I address_1),(S . (I address_2)))) . a by A1, A5, AMI_3:27, SCMRING1:8 .= s . b by A7, A8, SCMRING1:11 ; ::_thesis: for c being Data-Location of R st c <> a holds (Exec ((a := b),s)) . c = s . c let c be Data-Location of R; ::_thesis: ( c <> a implies (Exec ((a := b),s)) . c = s . c ) assume A9: c <> a ; ::_thesis: (Exec ((a := b),s)) . c = s . c A10: c is Element of Data-Locations by Th1; hence (Exec ((a := b),s)) . c = (SCM-Chg (S,(I address_1),(S . (I address_2)))) . c by A5, AMI_3:27, SCMRING1:8 .= s . c by A7, A9, A10, AMI_3:27, SCMRING1:12 ; ::_thesis: verum end; theorem Th12: :: SCMRING2:12 for R being Ring for a, b being Data-Location of R for s being State of (SCM R) holds ( (Exec ((AddTo (a,b)),s)) . (IC ) = succ (IC s) & (Exec ((AddTo (a,b)),s)) . a = (s . a) + (s . b) & ( for c being Data-Location of R st c <> a holds (Exec ((AddTo (a,b)),s)) . c = s . c ) ) proof let R be Ring; ::_thesis: for a, b being Data-Location of R for s being State of (SCM R) holds ( (Exec ((AddTo (a,b)),s)) . (IC ) = succ (IC s) & (Exec ((AddTo (a,b)),s)) . a = (s . a) + (s . b) & ( for c being Data-Location of R st c <> a holds (Exec ((AddTo (a,b)),s)) . c = s . c ) ) let a, b be Data-Location of R; ::_thesis: for s being State of (SCM R) holds ( (Exec ((AddTo (a,b)),s)) . (IC ) = succ (IC s) & (Exec ((AddTo (a,b)),s)) . a = (s . a) + (s . b) & ( for c being Data-Location of R st c <> a holds (Exec ((AddTo (a,b)),s)) . c = s . c ) ) let s be State of (SCM R); ::_thesis: ( (Exec ((AddTo (a,b)),s)) . (IC ) = succ (IC s) & (Exec ((AddTo (a,b)),s)) . a = (s . a) + (s . b) & ( for c being Data-Location of R st c <> a holds (Exec ((AddTo (a,b)),s)) . c = s . c ) ) A1: a is Element of Data-Locations by Th1; A2: the_Values_of (SCM R) = (SCM-VAL R) * SCM-OK by Lm1; reconsider S = s as SCM-State of R by A2, CARD_3:107; reconsider I = AddTo (a,b) as Element of SCM-Instr R by Def1; set S1 = SCM-Chg (S,(I address_1),((S . (I address_1)) + (S . (I address_2)))); reconsider i = 2 as Element of Segm 8 by NAT_1:44; A3: IC s = IC S by Def1; A4: b is Element of Data-Locations by Th1; A5: Exec ((AddTo (a,b)),s) = SCM-Exec-Res (I,S) by Th10 .= SCM-Chg ((SCM-Chg (S,(I address_1),((S . (I address_1)) + (S . (I address_2))))),(succ (IC S))) by A1, A4, AMI_3:27, SCMRING1:def_14 ; A6: I = [i,{},<*a,b*>] ; then A7: I address_1 = a by A1, A4, AMI_3:27, SCMRINGI:1; A8: I address_2 = b by A6, A1, A4, AMI_3:27, SCMRINGI:1; thus (Exec ((AddTo (a,b)),s)) . (IC ) = (Exec ((AddTo (a,b)),s)) . NAT by Def1 .= succ (IC s) by A3, A5, SCMRING1:7 ; ::_thesis: ( (Exec ((AddTo (a,b)),s)) . a = (s . a) + (s . b) & ( for c being Data-Location of R st c <> a holds (Exec ((AddTo (a,b)),s)) . c = s . c ) ) thus (Exec ((AddTo (a,b)),s)) . a = (SCM-Chg (S,(I address_1),((S . (I address_1)) + (S . (I address_2))))) . a by A1, A5, AMI_3:27, SCMRING1:8 .= (s . a) + (s . b) by A7, A8, SCMRING1:11 ; ::_thesis: for c being Data-Location of R st c <> a holds (Exec ((AddTo (a,b)),s)) . c = s . c let c be Data-Location of R; ::_thesis: ( c <> a implies (Exec ((AddTo (a,b)),s)) . c = s . c ) assume A9: c <> a ; ::_thesis: (Exec ((AddTo (a,b)),s)) . c = s . c A10: c is Element of Data-Locations by Th1; hence (Exec ((AddTo (a,b)),s)) . c = (SCM-Chg (S,(I address_1),((S . (I address_1)) + (S . (I address_2))))) . c by A5, AMI_3:27, SCMRING1:8 .= s . c by A7, A9, A10, AMI_3:27, SCMRING1:12 ; ::_thesis: verum end; theorem Th13: :: SCMRING2:13 for R being Ring for a, b being Data-Location of R for s being State of (SCM R) holds ( (Exec ((SubFrom (a,b)),s)) . (IC ) = succ (IC s) & (Exec ((SubFrom (a,b)),s)) . a = (s . a) - (s . b) & ( for c being Data-Location of R st c <> a holds (Exec ((SubFrom (a,b)),s)) . c = s . c ) ) proof let R be Ring; ::_thesis: for a, b being Data-Location of R for s being State of (SCM R) holds ( (Exec ((SubFrom (a,b)),s)) . (IC ) = succ (IC s) & (Exec ((SubFrom (a,b)),s)) . a = (s . a) - (s . b) & ( for c being Data-Location of R st c <> a holds (Exec ((SubFrom (a,b)),s)) . c = s . c ) ) let a, b be Data-Location of R; ::_thesis: for s being State of (SCM R) holds ( (Exec ((SubFrom (a,b)),s)) . (IC ) = succ (IC s) & (Exec ((SubFrom (a,b)),s)) . a = (s . a) - (s . b) & ( for c being Data-Location of R st c <> a holds (Exec ((SubFrom (a,b)),s)) . c = s . c ) ) let s be State of (SCM R); ::_thesis: ( (Exec ((SubFrom (a,b)),s)) . (IC ) = succ (IC s) & (Exec ((SubFrom (a,b)),s)) . a = (s . a) - (s . b) & ( for c being Data-Location of R st c <> a holds (Exec ((SubFrom (a,b)),s)) . c = s . c ) ) A1: a is Element of Data-Locations by Th1; A2: the_Values_of (SCM R) = (SCM-VAL R) * SCM-OK by Lm1; reconsider S = s as SCM-State of R by A2, CARD_3:107; reconsider I = SubFrom (a,b) as Element of SCM-Instr R by Def1; set S1 = SCM-Chg (S,(I address_1),((S . (I address_1)) - (S . (I address_2)))); reconsider i = 3 as Element of Segm 8 by NAT_1:44; A3: IC s = IC S by Def1; A4: b is Element of Data-Locations by Th1; A5: Exec ((SubFrom (a,b)),s) = SCM-Exec-Res (I,S) by Th10 .= SCM-Chg ((SCM-Chg (S,(I address_1),((S . (I address_1)) - (S . (I address_2))))),(succ (IC S))) by A1, A4, AMI_3:27, SCMRING1:def_14 ; A6: I = [i,{},<*a,b*>] ; then A7: I address_1 = a by A1, A4, AMI_3:27, SCMRINGI:1; A8: I address_2 = b by A6, A1, A4, AMI_3:27, SCMRINGI:1; thus (Exec ((SubFrom (a,b)),s)) . (IC ) = (Exec ((SubFrom (a,b)),s)) . NAT by Def1 .= succ (IC s) by A3, A5, SCMRING1:7 ; ::_thesis: ( (Exec ((SubFrom (a,b)),s)) . a = (s . a) - (s . b) & ( for c being Data-Location of R st c <> a holds (Exec ((SubFrom (a,b)),s)) . c = s . c ) ) thus (Exec ((SubFrom (a,b)),s)) . a = (SCM-Chg (S,(I address_1),((S . (I address_1)) - (S . (I address_2))))) . a by A1, A5, AMI_3:27, SCMRING1:8 .= (s . a) - (s . b) by A7, A8, SCMRING1:11 ; ::_thesis: for c being Data-Location of R st c <> a holds (Exec ((SubFrom (a,b)),s)) . c = s . c let c be Data-Location of R; ::_thesis: ( c <> a implies (Exec ((SubFrom (a,b)),s)) . c = s . c ) assume A9: c <> a ; ::_thesis: (Exec ((SubFrom (a,b)),s)) . c = s . c A10: c is Element of Data-Locations by Th1; hence (Exec ((SubFrom (a,b)),s)) . c = (SCM-Chg (S,(I address_1),((S . (I address_1)) - (S . (I address_2))))) . c by A5, AMI_3:27, SCMRING1:8 .= s . c by A7, A9, A10, AMI_3:27, SCMRING1:12 ; ::_thesis: verum end; theorem Th14: :: SCMRING2:14 for R being Ring for a, b being Data-Location of R for s being State of (SCM R) holds ( (Exec ((MultBy (a,b)),s)) . (IC ) = succ (IC s) & (Exec ((MultBy (a,b)),s)) . a = (s . a) * (s . b) & ( for c being Data-Location of R st c <> a holds (Exec ((MultBy (a,b)),s)) . c = s . c ) ) proof let R be Ring; ::_thesis: for a, b being Data-Location of R for s being State of (SCM R) holds ( (Exec ((MultBy (a,b)),s)) . (IC ) = succ (IC s) & (Exec ((MultBy (a,b)),s)) . a = (s . a) * (s . b) & ( for c being Data-Location of R st c <> a holds (Exec ((MultBy (a,b)),s)) . c = s . c ) ) let a, b be Data-Location of R; ::_thesis: for s being State of (SCM R) holds ( (Exec ((MultBy (a,b)),s)) . (IC ) = succ (IC s) & (Exec ((MultBy (a,b)),s)) . a = (s . a) * (s . b) & ( for c being Data-Location of R st c <> a holds (Exec ((MultBy (a,b)),s)) . c = s . c ) ) let s be State of (SCM R); ::_thesis: ( (Exec ((MultBy (a,b)),s)) . (IC ) = succ (IC s) & (Exec ((MultBy (a,b)),s)) . a = (s . a) * (s . b) & ( for c being Data-Location of R st c <> a holds (Exec ((MultBy (a,b)),s)) . c = s . c ) ) A1: a is Element of Data-Locations by Th1; A2: the_Values_of (SCM R) = (SCM-VAL R) * SCM-OK by Lm1; reconsider S = s as SCM-State of R by A2, CARD_3:107; reconsider I = MultBy (a,b) as Element of SCM-Instr R by Def1; set S1 = SCM-Chg (S,(I address_1),((S . (I address_1)) * (S . (I address_2)))); reconsider i = 4 as Element of Segm 8 by NAT_1:44; A3: IC s = IC S by Def1; A4: b is Element of Data-Locations by Th1; A5: Exec ((MultBy (a,b)),s) = SCM-Exec-Res (I,S) by Th10 .= SCM-Chg ((SCM-Chg (S,(I address_1),((S . (I address_1)) * (S . (I address_2))))),(succ (IC S))) by A1, A4, AMI_3:27, SCMRING1:def_14 ; A6: I = [i,{},<*a,b*>] ; then A7: I address_1 = a by A1, A4, AMI_3:27, SCMRINGI:1; A8: I address_2 = b by A6, A1, A4, AMI_3:27, SCMRINGI:1; thus (Exec ((MultBy (a,b)),s)) . (IC ) = (Exec ((MultBy (a,b)),s)) . NAT by Def1 .= succ (IC s) by A3, A5, SCMRING1:7 ; ::_thesis: ( (Exec ((MultBy (a,b)),s)) . a = (s . a) * (s . b) & ( for c being Data-Location of R st c <> a holds (Exec ((MultBy (a,b)),s)) . c = s . c ) ) thus (Exec ((MultBy (a,b)),s)) . a = (SCM-Chg (S,(I address_1),((S . (I address_1)) * (S . (I address_2))))) . a by A1, A5, AMI_3:27, SCMRING1:8 .= (s . a) * (s . b) by A7, A8, SCMRING1:11 ; ::_thesis: for c being Data-Location of R st c <> a holds (Exec ((MultBy (a,b)),s)) . c = s . c let c be Data-Location of R; ::_thesis: ( c <> a implies (Exec ((MultBy (a,b)),s)) . c = s . c ) assume A9: c <> a ; ::_thesis: (Exec ((MultBy (a,b)),s)) . c = s . c A10: c is Element of Data-Locations by Th1; hence (Exec ((MultBy (a,b)),s)) . c = (SCM-Chg (S,(I address_1),((S . (I address_1)) * (S . (I address_2))))) . c by A5, AMI_3:27, SCMRING1:8 .= s . c by A7, A9, A10, AMI_3:27, SCMRING1:12 ; ::_thesis: verum end; theorem :: SCMRING2:15 for R being Ring for c being Data-Location of R for i1 being Element of NAT for s being State of (SCM R) holds ( (Exec ((goto (i1,R)),s)) . (IC ) = i1 & (Exec ((goto (i1,R)),s)) . c = s . c ) proof let R be Ring; ::_thesis: for c being Data-Location of R for i1 being Element of NAT for s being State of (SCM R) holds ( (Exec ((goto (i1,R)),s)) . (IC ) = i1 & (Exec ((goto (i1,R)),s)) . c = s . c ) let c be Data-Location of R; ::_thesis: for i1 being Element of NAT for s being State of (SCM R) holds ( (Exec ((goto (i1,R)),s)) . (IC ) = i1 & (Exec ((goto (i1,R)),s)) . c = s . c ) let i1 be Element of NAT ; ::_thesis: for s being State of (SCM R) holds ( (Exec ((goto (i1,R)),s)) . (IC ) = i1 & (Exec ((goto (i1,R)),s)) . c = s . c ) let s be State of (SCM R); ::_thesis: ( (Exec ((goto (i1,R)),s)) . (IC ) = i1 & (Exec ((goto (i1,R)),s)) . c = s . c ) A1: the_Values_of (SCM R) = (SCM-VAL R) * SCM-OK by Lm1; reconsider S = s as SCM-State of R by A1, CARD_3:107; reconsider i = 6 as Element of Segm 8 by NAT_1:44; reconsider I = goto (i1,R) as Element of SCM-Instr R by Def1; I = [i,<*i1*>,{}] ; then A2: I jump_address = i1 by SCMRINGI:2; A3: Exec ((goto (i1,R)),s) = SCM-Exec-Res (I,S) by Th10 .= SCM-Chg (S,(I jump_address)) by SCMRING1:def_14 ; thus (Exec ((goto (i1,R)),s)) . (IC ) = (Exec ((goto (i1,R)),s)) . NAT by Def1 .= i1 by A3, A2, SCMRING1:7 ; ::_thesis: (Exec ((goto (i1,R)),s)) . c = s . c c is Element of Data-Locations by Th1; hence (Exec ((goto (i1,R)),s)) . c = s . c by A3, AMI_3:27, SCMRING1:8; ::_thesis: verum end; theorem Th16: :: SCMRING2:16 for R being Ring for a, c being Data-Location of R for i1 being Element of NAT for s being State of (SCM R) holds ( ( s . a = 0. R implies (Exec ((a =0_goto i1),s)) . (IC ) = i1 ) & ( s . a <> 0. R implies (Exec ((a =0_goto i1),s)) . (IC ) = succ (IC s) ) & (Exec ((a =0_goto i1),s)) . c = s . c ) proof let R be Ring; ::_thesis: for a, c being Data-Location of R for i1 being Element of NAT for s being State of (SCM R) holds ( ( s . a = 0. R implies (Exec ((a =0_goto i1),s)) . (IC ) = i1 ) & ( s . a <> 0. R implies (Exec ((a =0_goto i1),s)) . (IC ) = succ (IC s) ) & (Exec ((a =0_goto i1),s)) . c = s . c ) let a, c be Data-Location of R; ::_thesis: for i1 being Element of NAT for s being State of (SCM R) holds ( ( s . a = 0. R implies (Exec ((a =0_goto i1),s)) . (IC ) = i1 ) & ( s . a <> 0. R implies (Exec ((a =0_goto i1),s)) . (IC ) = succ (IC s) ) & (Exec ((a =0_goto i1),s)) . c = s . c ) let i1 be Element of NAT ; ::_thesis: for s being State of (SCM R) holds ( ( s . a = 0. R implies (Exec ((a =0_goto i1),s)) . (IC ) = i1 ) & ( s . a <> 0. R implies (Exec ((a =0_goto i1),s)) . (IC ) = succ (IC s) ) & (Exec ((a =0_goto i1),s)) . c = s . c ) let s be State of (SCM R); ::_thesis: ( ( s . a = 0. R implies (Exec ((a =0_goto i1),s)) . (IC ) = i1 ) & ( s . a <> 0. R implies (Exec ((a =0_goto i1),s)) . (IC ) = succ (IC s) ) & (Exec ((a =0_goto i1),s)) . c = s . c ) A1: the_Values_of (SCM R) = (SCM-VAL R) * SCM-OK by Lm1; reconsider S = s as SCM-State of R by A1, CARD_3:107; reconsider I = a =0_goto i1 as Element of SCM-Instr R by Def1; reconsider i = 7 as Element of Segm 8 by NAT_1:44; A2: ( a is Element of Data-Locations & i1 is Element of NAT ) by Th1; A3: Exec ((a =0_goto i1),s) = SCM-Exec-Res (I,S) by Th10 .= SCM-Chg (S,(IFEQ ((S . (I cond_address)),(0. R),(I cjump_address),(succ (IC S))))) by A2, AMI_3:27, SCMRING1:def_14 ; A4: I = [i,<*i1*>,<*a*>] ; thus ( s . a = 0. R implies (Exec ((a =0_goto i1),s)) . (IC ) = i1 ) ::_thesis: ( ( s . a <> 0. R implies (Exec ((a =0_goto i1),s)) . (IC ) = succ (IC s) ) & (Exec ((a =0_goto i1),s)) . c = s . c ) proof assume s . a = 0. R ; ::_thesis: (Exec ((a =0_goto i1),s)) . (IC ) = i1 then A5: S . (I cond_address) = 0. R by A4, A2, AMI_3:27, SCMRINGI:3; thus (Exec ((a =0_goto i1),s)) . (IC ) = (Exec ((a =0_goto i1),s)) . NAT by Def1 .= IFEQ ((S . (I cond_address)),(0. R),(I cjump_address),(succ (IC S))) by A3, SCMRING1:7 .= I cjump_address by A5, FUNCOP_1:def_8 .= i1 by A4, A2, AMI_3:27, SCMRINGI:3 ; ::_thesis: verum end; A6: IC s = IC S by Def1; thus ( s . a <> 0. R implies (Exec ((a =0_goto i1),s)) . (IC ) = succ (IC s) ) ::_thesis: (Exec ((a =0_goto i1),s)) . c = s . c proof assume s . a <> 0. R ; ::_thesis: (Exec ((a =0_goto i1),s)) . (IC ) = succ (IC s) then A7: S . (I cond_address) <> 0. R by A4, A2, AMI_3:27, SCMRINGI:3; thus (Exec ((a =0_goto i1),s)) . (IC ) = (Exec ((a =0_goto i1),s)) . NAT by Def1 .= IFEQ ((S . (I cond_address)),(0. R),(I cjump_address),(succ (IC S))) by A3, SCMRING1:7 .= succ (IC s) by A6, A7, FUNCOP_1:def_8 ; ::_thesis: verum end; c is Element of Data-Locations by Th1; hence (Exec ((a =0_goto i1),s)) . c = s . c by A3, AMI_3:27, SCMRING1:8; ::_thesis: verum end; theorem Th17: :: SCMRING2:17 for R being Ring for r being Element of R for a being Data-Location of R for s being State of (SCM R) holds ( (Exec ((a := r),s)) . (IC ) = succ (IC s) & (Exec ((a := r),s)) . a = r & ( for c being Data-Location of R st c <> a holds (Exec ((a := r),s)) . c = s . c ) ) proof let R be Ring; ::_thesis: for r being Element of R for a being Data-Location of R for s being State of (SCM R) holds ( (Exec ((a := r),s)) . (IC ) = succ (IC s) & (Exec ((a := r),s)) . a = r & ( for c being Data-Location of R st c <> a holds (Exec ((a := r),s)) . c = s . c ) ) let r be Element of R; ::_thesis: for a being Data-Location of R for s being State of (SCM R) holds ( (Exec ((a := r),s)) . (IC ) = succ (IC s) & (Exec ((a := r),s)) . a = r & ( for c being Data-Location of R st c <> a holds (Exec ((a := r),s)) . c = s . c ) ) let a be Data-Location of R; ::_thesis: for s being State of (SCM R) holds ( (Exec ((a := r),s)) . (IC ) = succ (IC s) & (Exec ((a := r),s)) . a = r & ( for c being Data-Location of R st c <> a holds (Exec ((a := r),s)) . c = s . c ) ) let s be State of (SCM R); ::_thesis: ( (Exec ((a := r),s)) . (IC ) = succ (IC s) & (Exec ((a := r),s)) . a = r & ( for c being Data-Location of R st c <> a holds (Exec ((a := r),s)) . c = s . c ) ) A1: a is Element of Data-Locations by Th1; A2: the_Values_of (SCM R) = (SCM-VAL R) * SCM-OK by Lm1; reconsider S = s as SCM-State of R by A2, CARD_3:107; reconsider I = a := r as Element of SCM-Instr R by Def1; set S1 = SCM-Chg (S,(I const_address),(I const_value)); reconsider i = 5 as Element of Segm 8 by NAT_1:44; A3: IC s = IC S by Def1; A4: I = [i,{},<*a,r*>] ; then A5: I const_address = a by A1, AMI_3:27, SCMRINGI:4; A6: I const_value = r by A4, A1, AMI_3:27, SCMRINGI:4; A7: Exec ((a := r),s) = SCM-Exec-Res (I,S) by Th10 .= SCM-Chg ((SCM-Chg (S,(I const_address),(I const_value))),(succ (IC S))) by A1, AMI_3:27, SCMRING1:def_14 ; thus (Exec ((a := r),s)) . (IC ) = (Exec ((a := r),s)) . NAT by Def1 .= succ (IC s) by A3, A7, SCMRING1:7 ; ::_thesis: ( (Exec ((a := r),s)) . a = r & ( for c being Data-Location of R st c <> a holds (Exec ((a := r),s)) . c = s . c ) ) thus (Exec ((a := r),s)) . a = (SCM-Chg (S,(I const_address),(I const_value))) . a by A1, A7, AMI_3:27, SCMRING1:8 .= r by A5, A6, SCMRING1:11 ; ::_thesis: for c being Data-Location of R st c <> a holds (Exec ((a := r),s)) . c = s . c let c be Data-Location of R; ::_thesis: ( c <> a implies (Exec ((a := r),s)) . c = s . c ) assume A8: c <> a ; ::_thesis: (Exec ((a := r),s)) . c = s . c A9: c is Element of Data-Locations by Th1; hence (Exec ((a := r),s)) . c = (SCM-Chg (S,(I const_address),(I const_value))) . c by A7, AMI_3:27, SCMRING1:8 .= s . c by A5, A8, A9, AMI_3:27, SCMRING1:12 ; ::_thesis: verum end; begin theorem Th18: :: SCMRING2:18 for R being Ring for I being Instruction of (SCM R) st ex s being State of (SCM R) st (Exec (I,s)) . (IC ) = succ (IC s) holds not I is halting proof let R be Ring; ::_thesis: for I being Instruction of (SCM R) st ex s being State of (SCM R) st (Exec (I,s)) . (IC ) = succ (IC s) holds not I is halting let I be Instruction of (SCM R); ::_thesis: ( ex s being State of (SCM R) st (Exec (I,s)) . (IC ) = succ (IC s) implies not I is halting ) given s being State of (SCM R) such that A1: (Exec (I,s)) . (IC ) = succ (IC s) ; ::_thesis: not I is halting A2: the_Values_of (SCM R) = (SCM-VAL R) * SCM-OK by Lm1; reconsider t = s as SCM-State of R by A2, CARD_3:107; IC t = t . NAT ; then reconsider w = t . NAT as Element of NAT ; A3: (Exec (I,s)) . (IC ) = succ w by A1, Def1; assume A4: I is halting ; ::_thesis: contradiction IC t = IC s by Def1; then (Exec (I,s)) . (IC ) = t . NAT by A4, EXTPRO_1:def_3; hence contradiction by A3; ::_thesis: verum end; theorem Th19: :: SCMRING2:19 for R being Ring for I being Instruction of (SCM R) st I = [0,{},{}] holds I is halting proof let R be Ring; ::_thesis: for I being Instruction of (SCM R) st I = [0,{},{}] holds I is halting let I be Instruction of (SCM R); ::_thesis: ( I = [0,{},{}] implies I is halting ) assume A1: I = [0,{},{}] ; ::_thesis: I is halting A2: I `3_3 = {} by A1, RECDEF_2:def_3; then A3: ( ( for mk, ml being Element of Data-Locations holds not I = [1,{},<*mk,ml*>] ) & ( for mk, ml being Element of Data-Locations holds not I = [2,{},<*mk,ml*>] ) ) by RECDEF_2:def_3; A4: for mk being Element of Data-Locations for r being Element of R holds not I = [5,{},<*mk,r*>] by A2, RECDEF_2:def_3; I `2_3 = {} by A1, RECDEF_2:def_2; then A5: ( ( for mk being Element of NAT holds not I = [6,<*mk*>,{}] ) & ( for mk being Element of NAT for ml being Element of Data-Locations holds not I = [7,<*mk*>,<*ml*>] ) ) by RECDEF_2:def_2; reconsider L = I as Element of SCM-Instr R by A1, SCMRINGI:6; let s be State of (SCM R); :: according to EXTPRO_1:def_3 ::_thesis: Exec (I,s) = s A6: the_Values_of (SCM R) = (SCM-VAL R) * SCM-OK by Lm1; reconsider t = s as SCM-State of R by A6, CARD_3:107; A7: ( ( for mk, ml being Element of Data-Locations holds not I = [3,{},<*mk,ml*>] ) & ( for mk, ml being Element of Data-Locations holds not I = [4,{},<*mk,ml*>] ) ) by A2, RECDEF_2:def_3; thus Exec (I,s) = SCM-Exec-Res (L,t) by Th10 .= s by A3, A7, A5, A4, AMI_3:27, SCMRING1:def_14 ; ::_thesis: verum end; Lm3: for R being Ring for a, b being Data-Location of R holds not a := b is halting proof let R be Ring; ::_thesis: for a, b being Data-Location of R holds not a := b is halting let a, b be Data-Location of R; ::_thesis: not a := b is halting set s = the State of (SCM R); (Exec ((a := b), the State of (SCM R))) . (IC ) = succ (IC the State of (SCM R)) by Th11; hence not a := b is halting by Th18; ::_thesis: verum end; Lm4: for R being Ring for a, b being Data-Location of R holds not AddTo (a,b) is halting proof let R be Ring; ::_thesis: for a, b being Data-Location of R holds not AddTo (a,b) is halting let a, b be Data-Location of R; ::_thesis: not AddTo (a,b) is halting set s = the State of (SCM R); (Exec ((AddTo (a,b)), the State of (SCM R))) . (IC ) = succ (IC the State of (SCM R)) by Th12; hence not AddTo (a,b) is halting by Th18; ::_thesis: verum end; Lm5: for R being Ring for a, b being Data-Location of R holds not SubFrom (a,b) is halting proof let R be Ring; ::_thesis: for a, b being Data-Location of R holds not SubFrom (a,b) is halting let a, b be Data-Location of R; ::_thesis: not SubFrom (a,b) is halting set s = the State of (SCM R); (Exec ((SubFrom (a,b)), the State of (SCM R))) . (IC ) = succ (IC the State of (SCM R)) by Th13; hence not SubFrom (a,b) is halting by Th18; ::_thesis: verum end; Lm6: for R being Ring for a, b being Data-Location of R holds not MultBy (a,b) is halting proof let R be Ring; ::_thesis: for a, b being Data-Location of R holds not MultBy (a,b) is halting let a, b be Data-Location of R; ::_thesis: not MultBy (a,b) is halting set s = the State of (SCM R); (Exec ((MultBy (a,b)), the State of (SCM R))) . (IC ) = succ (IC the State of (SCM R)) by Th14; hence not MultBy (a,b) is halting by Th18; ::_thesis: verum end; Lm7: for R being Ring for i1 being Element of NAT holds not goto (i1,R) is halting proof let R be Ring; ::_thesis: for i1 being Element of NAT holds not goto (i1,R) is halting let i1 be Element of NAT ; ::_thesis: not goto (i1,R) is halting reconsider i5 = i1 as Element of NAT ; set s = the SCM-State of R; set t = the SCM-State of R +* (NAT .--> (succ i1)); set f = the_Values_of (SCM R); A1: {NAT} c= SCM-Memory by AMI_2:22, ZFMISC_1:31; A2: dom ( the SCM-State of R +* (NAT .--> (succ i1))) = (dom the SCM-State of R) \/ (dom (NAT .--> (succ i1))) by FUNCT_4:def_1 .= SCM-Memory \/ (dom (NAT .--> (succ i1))) by SCMRING1:19 .= SCM-Memory \/ {NAT} by FUNCOP_1:13 .= SCM-Memory by A1, XBOOLE_1:12 ; A3: the_Values_of (SCM R) = (SCM-VAL R) * SCM-OK by Lm1; A4: dom (NAT .--> (succ i1)) = {NAT} by FUNCOP_1:13; then NAT in dom (NAT .--> (succ i1)) by TARSKI:def_1; then A5: ( the SCM-State of R +* (NAT .--> (succ i1))) . NAT = (NAT .--> (succ i1)) . NAT by FUNCT_4:13 .= succ i5 by FUNCOP_1:72 ; A6: dom ( the SCM-State of R +* (NAT .--> (succ i1))) = the carrier of (SCM R) by A2, Def1 .= dom (the_Values_of (SCM R)) by PARTFUN1:def_2 ; A7: for x being set st x in dom ( the SCM-State of R +* (NAT .--> (succ i1))) holds ( the SCM-State of R +* (NAT .--> (succ i1))) . x in (the_Values_of (SCM R)) . x proof let x be set ; ::_thesis: ( x in dom ( the SCM-State of R +* (NAT .--> (succ i1))) implies ( the SCM-State of R +* (NAT .--> (succ i1))) . x in (the_Values_of (SCM R)) . x ) assume A8: x in dom ( the SCM-State of R +* (NAT .--> (succ i1))) ; ::_thesis: ( the SCM-State of R +* (NAT .--> (succ i1))) . x in (the_Values_of (SCM R)) . x percases ( x = NAT or x <> NAT ) ; supposeA9: x = NAT ; ::_thesis: ( the SCM-State of R +* (NAT .--> (succ i1))) . x in (the_Values_of (SCM R)) . x then (the_Values_of (SCM R)) . x = NAT by A3, SCMRING1:2; hence ( the SCM-State of R +* (NAT .--> (succ i1))) . x in (the_Values_of (SCM R)) . x by A5, A9; ::_thesis: verum end; suppose x <> NAT ; ::_thesis: ( the SCM-State of R +* (NAT .--> (succ i1))) . x in (the_Values_of (SCM R)) . x then not x in dom (NAT .--> (succ i1)) by A4, TARSKI:def_1; then ( the SCM-State of R +* (NAT .--> (succ i1))) . x = the SCM-State of R . x by FUNCT_4:11; hence ( the SCM-State of R +* (NAT .--> (succ i1))) . x in (the_Values_of (SCM R)) . x by A3, A8, A6, CARD_3:9; ::_thesis: verum end; end; end; A10: the_Values_of (SCM R) = (SCM-VAL R) * SCM-OK by Lm1; dom ( the SCM-State of R +* (NAT .--> (succ i1))) = the carrier of (SCM R) by A2, Def1; then reconsider t = the SCM-State of R +* (NAT .--> (succ i1)) as PartState of (SCM R) by A7, FUNCT_1:def_14, RELAT_1:def_18; dom t = the carrier of (SCM R) by A2, Def1; then reconsider t = t as State of (SCM R) by PARTFUN1:def_2; reconsider w = t as SCM-State of R by A10, CARD_3:107; dom (NAT .--> i1) = {NAT} by FUNCOP_1:13; then NAT in dom (NAT .--> i1) by TARSKI:def_1; then A11: (w +* (NAT .--> i1)) . NAT = (NAT .--> i1) . NAT by FUNCT_4:13 .= i1 by FUNCOP_1:72 ; reconsider V = goto (i1,R) as Element of SCM-Instr R by Def1; assume A12: goto (i1,R) is halting ; ::_thesis: contradiction A13: 6 is Element of Segm 8 by NAT_1:44; w +* (NAT .--> i1) = SCM-Chg (w,i5) .= SCM-Chg (w,(V jump_address)) by A13, SCMRINGI:2 .= SCM-Exec-Res (V,w) by SCMRING1:def_14 .= Exec ((goto (i1,R)),t) by Th10 .= t by A12, EXTPRO_1:def_3 ; hence contradiction by A5, A11; ::_thesis: verum end; Lm8: for R being Ring for a being Data-Location of R for i1 being Element of NAT holds not a =0_goto i1 is halting proof let R be Ring; ::_thesis: for a being Data-Location of R for i1 being Element of NAT holds not a =0_goto i1 is halting let a be Data-Location of R; ::_thesis: for i1 being Element of NAT holds not a =0_goto i1 is halting let i1 be Element of NAT ; ::_thesis: not a =0_goto i1 is halting reconsider i5 = i1 as Element of NAT ; set s = the SCM-State of R; set t = the SCM-State of R +* (NAT .--> (succ i1)); set f = the_Values_of (SCM R); reconsider V = a =0_goto i1 as Element of SCM-Instr R by Def1; A1: {NAT} c= SCM-Memory by AMI_2:22, ZFMISC_1:31; A2: dom ( the SCM-State of R +* (NAT .--> (succ i1))) = (dom the SCM-State of R) \/ (dom (NAT .--> (succ i1))) by FUNCT_4:def_1 .= SCM-Memory \/ (dom (NAT .--> (succ i1))) by SCMRING1:19 .= SCM-Memory \/ {NAT} by FUNCOP_1:13 .= SCM-Memory by A1, XBOOLE_1:12 ; A3: the_Values_of (SCM R) = (SCM-VAL R) * SCM-OK by Lm1; A4: dom (NAT .--> (succ i1)) = {NAT} by FUNCOP_1:13; then NAT in dom (NAT .--> (succ i1)) by TARSKI:def_1; then A5: ( the SCM-State of R +* (NAT .--> (succ i1))) . NAT = (NAT .--> (succ i1)) . NAT by FUNCT_4:13 .= succ i5 by FUNCOP_1:72 ; A6: dom ( the SCM-State of R +* (NAT .--> (succ i1))) = the carrier of (SCM R) by A2, Def1 .= dom (the_Values_of (SCM R)) by PARTFUN1:def_2 ; A7: for x being set st x in dom ( the SCM-State of R +* (NAT .--> (succ i1))) holds ( the SCM-State of R +* (NAT .--> (succ i1))) . x in (the_Values_of (SCM R)) . x proof let x be set ; ::_thesis: ( x in dom ( the SCM-State of R +* (NAT .--> (succ i1))) implies ( the SCM-State of R +* (NAT .--> (succ i1))) . x in (the_Values_of (SCM R)) . x ) assume A8: x in dom ( the SCM-State of R +* (NAT .--> (succ i1))) ; ::_thesis: ( the SCM-State of R +* (NAT .--> (succ i1))) . x in (the_Values_of (SCM R)) . x percases ( x = NAT or x <> NAT ) ; supposeA9: x = NAT ; ::_thesis: ( the SCM-State of R +* (NAT .--> (succ i1))) . x in (the_Values_of (SCM R)) . x then (the_Values_of (SCM R)) . x = NAT by A3, SCMRING1:2; hence ( the SCM-State of R +* (NAT .--> (succ i1))) . x in (the_Values_of (SCM R)) . x by A5, A9; ::_thesis: verum end; suppose x <> NAT ; ::_thesis: ( the SCM-State of R +* (NAT .--> (succ i1))) . x in (the_Values_of (SCM R)) . x then not x in dom (NAT .--> (succ i1)) by A4, TARSKI:def_1; then ( the SCM-State of R +* (NAT .--> (succ i1))) . x = the SCM-State of R . x by FUNCT_4:11; hence ( the SCM-State of R +* (NAT .--> (succ i1))) . x in (the_Values_of (SCM R)) . x by A3, A8, A6, CARD_3:9; ::_thesis: verum end; end; end; dom ( the SCM-State of R +* (NAT .--> (succ i1))) = the carrier of (SCM R) by A2, Def1; then reconsider t = the SCM-State of R +* (NAT .--> (succ i1)) as PartState of (SCM R) by A7, FUNCT_1:def_14, RELAT_1:def_18; dom t = the carrier of (SCM R) by A2, Def1; then reconsider t = t as State of (SCM R) by PARTFUN1:def_2; A10: the_Values_of (SCM R) = (SCM-VAL R) * SCM-OK by Lm1; reconsider w = t as SCM-State of R by A10, CARD_3:107; dom (NAT .--> i1) = {NAT} by FUNCOP_1:13; then NAT in dom (NAT .--> i1) by TARSKI:def_1; then A11: (w +* (NAT .--> i1)) . NAT = (NAT .--> i1) . NAT by FUNCT_4:13 .= i1 by FUNCOP_1:72 ; A12: 7 is Element of Segm 8 by NAT_1:44; A13: a is Element of Data-Locations by Th1; assume A14: a =0_goto i1 is halting ; ::_thesis: contradiction percases ( w . (V cond_address) <> 0. R or w . (V cond_address) = 0. R ) ; supposeA15: w . (V cond_address) <> 0. R ; ::_thesis: contradiction IC w = w . NAT ; then reconsider e = w . NAT as Element of NAT ; A16: IC t = IC w by Def1; then A17: (Exec ((a =0_goto i1),t)) . (IC ) = w . NAT by A14, EXTPRO_1:def_3; a is Element of Data-Locations by Th1; then t . a <> 0. R by A12, A15, AMI_3:27, SCMRINGI:3; then (Exec ((a =0_goto i1),t)) . (IC ) = succ e by A16, Th16; hence contradiction by A17; ::_thesis: verum end; supposeA18: w . (V cond_address) = 0. R ; ::_thesis: contradiction w +* (NAT .--> i1) = SCM-Chg (w,i5) .= SCM-Chg (w,(V cjump_address)) by A12, A13, AMI_3:27, SCMRINGI:3 .= SCM-Chg (w,(IFEQ ((w . (V cond_address)),(0. R),(V cjump_address),(succ (IC w))))) by A18, FUNCOP_1:def_8 .= SCM-Exec-Res (V,w) by A13, AMI_3:27, SCMRING1:def_14 .= Exec ((a =0_goto i1),t) by Th10 .= t by A14, EXTPRO_1:def_3 ; hence contradiction by A5, A11; ::_thesis: verum end; end; end; Lm9: for R being Ring for r being Element of R for a being Data-Location of R holds not a := r is halting proof let R be Ring; ::_thesis: for r being Element of R for a being Data-Location of R holds not a := r is halting let r be Element of R; ::_thesis: for a being Data-Location of R holds not a := r is halting let a be Data-Location of R; ::_thesis: not a := r is halting set s = the State of (SCM R); (Exec ((a := r), the State of (SCM R))) . (IC ) = succ (IC the State of (SCM R)) by Th17; hence not a := r is halting by Th18; ::_thesis: verum end; registration let R be Ring; let a, b be Data-Location of R; clustera := b -> non halting ; coherence not a := b is halting by Lm3; cluster AddTo (a,b) -> non halting ; coherence not AddTo (a,b) is halting by Lm4; cluster SubFrom (a,b) -> non halting ; coherence not SubFrom (a,b) is halting by Lm5; cluster MultBy (a,b) -> non halting ; coherence not MultBy (a,b) is halting by Lm6; end; registration let R be Ring; let i1 be Element of NAT ; cluster goto (i1,R) -> non halting ; coherence not goto (i1,R) is halting by Lm7; end; registration let R be Ring; let a be Data-Location of R; let i1 be Element of NAT ; clustera =0_goto i1 -> non halting ; coherence not a =0_goto i1 is halting by Lm8; end; registration let R be Ring; let a be Data-Location of R; let r be Element of R; clustera := r -> non halting ; coherence not a := r is halting by Lm9; end; Lm10: for R being Ring for W being Instruction of (SCM R) st W is halting holds W = [0,{},{}] proof let R be Ring; ::_thesis: for W being Instruction of (SCM R) st W is halting holds W = [0,{},{}] set I = [0,{},{}]; let W be Instruction of (SCM R); ::_thesis: ( W is halting implies W = [0,{},{}] ) assume A1: W is halting ; ::_thesis: W = [0,{},{}] assume A2: [0,{},{}] <> W ; ::_thesis: contradiction percases ( W = [0,{},{}] or ex a, b being Data-Location of R st W = a := b or ex a, b being Data-Location of R st W = AddTo (a,b) or ex a, b being Data-Location of R st W = SubFrom (a,b) or ex a, b being Data-Location of R st W = MultBy (a,b) or ex i1 being Element of NAT st W = goto (i1,R) or ex a being Data-Location of R ex i1 being Element of NAT st W = a =0_goto i1 or ex a being Data-Location of R ex r being Element of R st W = a := r ) by Th7; suppose W = [0,{},{}] ; ::_thesis: contradiction hence contradiction by A2; ::_thesis: verum end; suppose ex a, b being Data-Location of R st W = a := b ; ::_thesis: contradiction hence contradiction by A1; ::_thesis: verum end; suppose ex a, b being Data-Location of R st W = AddTo (a,b) ; ::_thesis: contradiction hence contradiction by A1; ::_thesis: verum end; suppose ex a, b being Data-Location of R st W = SubFrom (a,b) ; ::_thesis: contradiction hence contradiction by A1; ::_thesis: verum end; suppose ex a, b being Data-Location of R st W = MultBy (a,b) ; ::_thesis: contradiction hence contradiction by A1; ::_thesis: verum end; suppose ex i1 being Element of NAT st W = goto (i1,R) ; ::_thesis: contradiction hence contradiction by A1; ::_thesis: verum end; suppose ex a being Data-Location of R ex i1 being Element of NAT st W = a =0_goto i1 ; ::_thesis: contradiction hence contradiction by A1; ::_thesis: verum end; suppose ex a being Data-Location of R ex r being Element of R st W = a := r ; ::_thesis: contradiction hence contradiction by A1; ::_thesis: verum end; end; end; registration let R be Ring; cluster SCM R -> strict halting ; coherence SCM R is halting proof thus halt (SCM R) is halting by Th19; :: according to EXTPRO_1:def_4 ::_thesis: verum end; end; theorem :: SCMRING2:20 for R being Ring for I being Instruction of (SCM R) st I is halting holds I = halt (SCM R) by Lm10; theorem :: SCMRING2:21 for R being Ring holds halt (SCM R) = [0,{},{}] ; theorem Th22: :: SCMRING2:22 for R being Ring holds Data-Locations = Data-Locations proof let R be Ring; ::_thesis: Data-Locations = Data-Locations Data-Locations misses {NAT} by AMI_2:20, AMI_3:27, ZFMISC_1:50; then A1: Data-Locations misses {NAT} ; thus Data-Locations = SCM-Memory \ {(IC )} by Def1 .= SCM-Memory \ {NAT} by Def1 .= ((Data-Locations ) \/ {NAT}) \ {NAT} by AMI_3:27 .= (Data-Locations ) \ {NAT} by XBOOLE_1:40 .= Data-Locations by A1, XBOOLE_1:83 ; ::_thesis: verum end; theorem :: SCMRING2:23 for x being set for R being Ring holds ( x is Data-Location of R iff x in Data-Locations ) proof let x be set ; ::_thesis: for R being Ring holds ( x is Data-Location of R iff x in Data-Locations ) let R be Ring; ::_thesis: ( x is Data-Location of R iff x in Data-Locations ) Data-Locations = Data-Locations by Th22; hence ( x is Data-Location of R iff x in Data-Locations ) by Th1; ::_thesis: verum end; theorem :: SCMRING2:24 for R being Ring holds the_Values_of (SCM R) = (SCM-VAL R) * SCM-OK by Lm1; theorem :: SCMRING2:25 for R being Ring holds the carrier of (SCM R) \ {NAT} = SCM-Data-Loc by Lm2;