:: 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;