:: by Artur Korni{\l}owicz

::

:: Received November 29, 1998

:: Copyright (c) 1998-2017 Association of Mizar Users

definition

let R be Ring;

ex b_{1} being strict AMI-Struct over Segm 2 st

( the carrier of b_{1} = SCM-Memory & the ZeroF of b_{1} = NAT & the InstructionsF of b_{1} = SCM-Instr R & the Object-Kind of b_{1} = SCM-OK & the ValuesF of b_{1} = SCM-VAL R & the Execution of b_{1} = SCM-Exec R )

for b_{1}, b_{2} being strict AMI-Struct over Segm 2 st the carrier of b_{1} = SCM-Memory & the ZeroF of b_{1} = NAT & the InstructionsF of b_{1} = SCM-Instr R & the Object-Kind of b_{1} = SCM-OK & the ValuesF of b_{1} = SCM-VAL R & the Execution of b_{1} = SCM-Exec R & the carrier of b_{2} = SCM-Memory & the ZeroF of b_{2} = NAT & the InstructionsF of b_{2} = SCM-Instr R & the Object-Kind of b_{2} = SCM-OK & the ValuesF of b_{2} = SCM-VAL R & the Execution of b_{2} = SCM-Exec R holds

b_{1} = b_{2}
;

end;
func SCM R -> strict AMI-Struct over Segm 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 ( 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 );

ex b

( the carrier of b

proof end;

uniqueness for b

b

:: deftheorem Def1 defines SCM SCMRING2:def 1 :

for R being Ring

for b_{2} being strict AMI-Struct over Segm 2 holds

( b_{2} = SCM R iff ( the carrier of b_{2} = SCM-Memory & the ZeroF of b_{2} = NAT & the InstructionsF of b_{2} = SCM-Instr R & the Object-Kind of b_{2} = SCM-OK & the ValuesF of b_{2} = SCM-VAL R & the Execution of b_{2} = SCM-Exec R ) );

for R being Ring

for b

( b

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

Lm2: for R being Ring holds the carrier of (SCM R) \ {NAT} = SCM-Data-Loc

proof end;

registration
end;

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;

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 func s . a -> Element of R;

coherence

s . a is Element of R

end;
let s be State of (SCM R);

let a be Data-Location of R;

:: original: .

redefine func s . a -> Element of R;

coherence

s . a is Element of R

proof 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

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

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

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 Nat holds [7,<*i1*>,<*d1*>] in SCM-Instr S

for R being Ring

for d1 being Data-Location of R

for i1 being Nat holds [7,<*i1*>,<*d1*>] in SCM-Instr S

proof end;

definition

let R be Ring;

let a, b be Data-Location of R;

coherence

[1,{},<*a,b*>] is Instruction of (SCM R)

[2,{},<*a,b*>] is Instruction of (SCM R)

[3,{},<*a,b*>] is Instruction of (SCM R)

[4,{},<*a,b*>] is Instruction of (SCM R)

end;
let a, b be Data-Location of R;

coherence

[1,{},<*a,b*>] is Instruction of (SCM R)

proof end;

coherence [2,{},<*a,b*>] is Instruction of (SCM R)

proof end;

coherence [3,{},<*a,b*>] is Instruction of (SCM R)

proof end;

coherence [4,{},<*a,b*>] is Instruction of (SCM R)

proof end;

:: deftheorem defines := SCMRING2:def 3 :

for R being Ring

for a, b being Data-Location of R holds a := b = [1,{},<*a,b*>];

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*>];

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*>];

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*>];

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;

coherence

[5,{},<*a,r*>] is Instruction of (SCM R)

end;
let a be Data-Location of R;

let r be Element of R;

coherence

[5,{},<*a,r*>] is Instruction of (SCM R)

proof 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*>];

for R being Ring

for a being Data-Location of R

for r being Element of R holds a := r = [5,{},<*a,r*>];

definition
end;

:: deftheorem defines goto SCMRING2:def 8 :

for R being Ring

for l being Nat holds goto (l,R) = [6,<*l*>,{}];

for R being Ring

for l being Nat holds goto (l,R) = [6,<*l*>,{}];

definition

let R be Ring;

let l be Nat;

let a be Data-Location of R;

coherence

[7,<*l*>,<*a*>] is Instruction of (SCM R)

end;
let l be Nat;

let a be Data-Location of R;

coherence

[7,<*l*>,<*a*>] is Instruction of (SCM R)

proof end;

:: deftheorem defines =0_goto SCMRING2:def 9 :

for R being Ring

for l being Nat

for a being Data-Location of R holds a =0_goto l = [7,<*l*>,<*a*>];

for R being Ring

for l being 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 Nat st I = goto (i1,R) or ex a being Data-Location of R ex i1 being 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 ) )

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 Nat st I = goto (i1,R) or ex a being Data-Location of R ex i1 being 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 end;

theorem :: SCMRING2:9

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)

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

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 ) = (IC s) + 1 & (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 ) )

for a, b being Data-Location of R

for s being State of (SCM R) holds

( (Exec ((a := b),s)) . (IC ) = (IC s) + 1 & (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 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 ) = (IC s) + 1 & (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 ) )

for a, b being Data-Location of R

for s being State of (SCM R) holds

( (Exec ((AddTo (a,b)),s)) . (IC ) = (IC s) + 1 & (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 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 ) = (IC s) + 1 & (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 ) )

for a, b being Data-Location of R

for s being State of (SCM R) holds

( (Exec ((SubFrom (a,b)),s)) . (IC ) = (IC s) + 1 & (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 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 ) = (IC s) + 1 & (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 ) )

for a, b being Data-Location of R

for s being State of (SCM R) holds

( (Exec ((MultBy (a,b)),s)) . (IC ) = (IC s) + 1 & (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 end;

theorem :: SCMRING2:15

for R being Ring

for c being Data-Location of R

for i1 being Nat

for s being State of (SCM R) holds

( (Exec ((goto (i1,R)),s)) . (IC ) = i1 & (Exec ((goto (i1,R)),s)) . c = s . c )

for c being Data-Location of R

for i1 being 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 end;

theorem Th16: :: SCMRING2:16

for R being Ring

for a, c being Data-Location of R

for i1 being 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 ) = (IC s) + 1 ) & (Exec ((a =0_goto i1),s)) . c = s . c )

for a, c being Data-Location of R

for i1 being 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 ) = (IC s) + 1 ) & (Exec ((a =0_goto i1),s)) . c = s . c )

proof 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 ) = (IC s) + 1 & (Exec ((a := r),s)) . a = r & ( for c being Data-Location of R st c <> a holds

(Exec ((a := r),s)) . c = s . c ) )

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 ) = (IC s) + 1 & (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 end;

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 ) = (IC s) + 1 holds

not I is halting

for I being Instruction of (SCM R) st ex s being State of (SCM R) st (Exec (I,s)) . (IC ) = (IC s) + 1 holds

not I is halting

proof end;

Lm3: for R being Ring

for a, b being Data-Location of R holds not a := b is halting

proof end;

Lm4: for R being Ring

for a, b being Data-Location of R holds not AddTo (a,b) is halting

proof end;

Lm5: for R being Ring

for a, b being Data-Location of R holds not SubFrom (a,b) is halting

proof end;

Lm6: for R being Ring

for a, b being Data-Location of R holds not MultBy (a,b) is halting

proof end;

Lm7: for R being Ring

for i1 being Nat holds not goto (i1,R) is halting

proof end;

Lm8: for R being Ring

for a being Data-Location of R

for i1 being Nat holds not a =0_goto i1 is halting

proof 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 end;

registration

let R be Ring;

let a, b be Data-Location of R;

coherence

not a := b is halting by Lm3;

coherence

not AddTo (a,b) is halting by Lm4;

coherence

not SubFrom (a,b) is halting by Lm5;

coherence

not MultBy (a,b) is halting by Lm6;

end;
let a, b be Data-Location of R;

coherence

not a := b is halting by Lm3;

coherence

not AddTo (a,b) is halting by Lm4;

coherence

not SubFrom (a,b) is halting by Lm5;

coherence

not MultBy (a,b) is halting by Lm6;

registration

let R be Ring;

let a be Data-Location of R;

let i1 be Nat;

coherence

not a =0_goto i1 is halting by Lm8;

end;
let a be Data-Location of R;

let i1 be Nat;

coherence

not a =0_goto i1 is halting by Lm8;

registration

let R be Ring;

let a be Data-Location of R;

let r be Element of R;

coherence

not a := r is halting by Lm9;

end;
let a be Data-Location of R;

let r be Element of R;

coherence

not a := r is halting by Lm9;

Lm10: for R being Ring

for W being Instruction of (SCM R) st W is halting holds

W = [0,{},{}]

proof end;

registration
end;

theorem :: SCMRING2:20