:: The Basic Properties of { \bf SCM } over Ring
:: by Artur Korni{\l}owicz
::
:: Received November 29, 1998
:: Copyright (c) 1998 Association of Mizar Users

begin

definition

let R be good Ring;
func SCM R -> strict AMI-Struct of {the carrier of R} means :Def1: :: SCMRING2:def 1
( the carrier of it = SCM-Memory & the Instruction-Counter of it = NAT & the Instructions of it = SCM-Instr R & the Object-Kind of it = SCM-OK R & the Execution of it = SCM-Exec R );
existence
ex b₁ being strict AMI-Struct of {the carrier of R} st
( the carrier of b₁ = SCM-Memory & the Instruction-Counter of b₁ = NAT & the Instructions of b₁ = SCM-Instr R & the Object-Kind of b₁ = SCM-OK R & the Execution of b₁ = SCM-Exec R )

proof end;

uniqueness
for b₁, b₂ being strict AMI-Struct of {the carrier of R} st the carrier of b₁ = SCM-Memory & the Instruction-Counter of b₁ = NAT & the Instructions of b₁ = SCM-Instr R & the Object-Kind of b₁ = SCM-OK R & the Execution of b₁ = SCM-Exec R & the carrier of b₂ = SCM-Memory & the Instruction-Counter of b₂ = NAT & the Instructions of b₂ = SCM-Instr R & the Object-Kind of b₂ = SCM-OK R & the Execution of b₂ = SCM-Exec R holds
b₁ = b₂ ;

end;

:: deftheorem Def1 defines SCM SCMRING2:def 1 :

for R being good Ring
for b₂ being strict AMI-Struct of {the carrier of R} holds
( b₂ = SCM R iff ( the carrier of b₂ = SCM-Memory & the Instruction-Counter of b₂ = NAT & the Instructions of b₂ = SCM-Instr R & the Object-Kind of b₂ = SCM-OK R & the Execution of b₂ = SCM-Exec R ) );

registration

let R be good Ring;
cluster SCM R -> non empty strict stored-program standard-ins ;
coherence
( not SCM R is empty & SCM R is stored-program & SCM R is standard-ins )

proof end;

end;

definition

let R be good Ring;
let s be State of ;
let a be Element of SCM-Data-Loc ;
:: original: .
redefine func s . a -> Element of ;
coherence
s . a is Element of

proof end;

end;

definition

let R be good Ring;
mode Data-Location of R -> Object of means :Def2: :: SCMRING2:def 2
it in the carrier of (SCM R) \ (NAT \/ {NAT });
existence
ex b₁ being Object of st b₁ in the carrier of (SCM R) \ (NAT \/ {NAT })

proof end;

end;

:: deftheorem Def2 defines Data-Location SCMRING2:def 2 :

for R being good Ring
for b₂ being Object of holds
( b₂ is Data-Location of R iff b₂ in the carrier of (SCM R) \ (NAT \/ {NAT }) );

theorem Th1: :: SCMRING2:1

for x being set
for R being good Ring holds
( x is Data-Location of R iff x in SCM-Data-Loc )

proof end;

definition

let R be good Ring;
let s be State of ;
let a be Data-Location of R;
:: original: .
redefine func s . a -> Element of ;
coherence
s . a is Element of

proof end;

end;

theorem Th2: :: SCMRING2:2

for S being non empty 1-sorted holds [0 ,{} ] in SCM-Instr S

proof end;

theorem Th3: :: SCMRING2:3

for R being good Ring holds [0 ,{} ] is Instruction of

proof end;

theorem Th4: :: SCMRING2:4

for S being non empty 1-sorted
for x being set
for R being good 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 Th5: :: SCMRING2:5

for S being non empty 1-sorted
for t being Element of
for R being good 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 good Ring
for i1 being Instruction-Location of SCM R holds [6,<*i1*>] in SCM-Instr S

proof end;

theorem Th7: :: SCMRING2:7

for S being non empty 1-sorted
for R being good Ring
for d1 being Data-Location of R
for i1 being Instruction-Location of SCM R holds [7,<*i1,d1*>] in SCM-Instr S

proof end;

definition

let R be good Ring;
let a, b be Data-Location of R;
func a := b -> Instruction of equals :: SCMRING2:def 3
[1,<*a,b*>];
coherence
[1,<*a,b*>] is Instruction of

proof end;

func AddTo a,b -> Instruction of equals :: SCMRING2:def 4
[2,<*a,b*>];
coherence
[2,<*a,b*>] is Instruction of

proof end;

func SubFrom a,b -> Instruction of equals :: SCMRING2:def 5
[3,<*a,b*>];
coherence
[3,<*a,b*>] is Instruction of

proof end;

func MultBy a,b -> Instruction of equals :: SCMRING2:def 6
[4,<*a,b*>];
coherence
[4,<*a,b*>] is Instruction of

proof end;

end;

:: deftheorem defines := SCMRING2:def 3 :

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

:: deftheorem defines AddTo SCMRING2:def 4 :

for R being good 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 good 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 good Ring
for a, b being Data-Location of R holds MultBy a,b = [4,<*a,b*>];

definition

let R be good Ring;
let a be Data-Location of R;
let r be Element of ;
func a := r -> Instruction of equals :: SCMRING2:def 7
[5,<*a,r*>];
coherence
[5,<*a,r*>] is Instruction of

proof end;

end;

:: deftheorem defines := SCMRING2:def 7 :

for R being good Ring
for a being Data-Location of R
for r being Element of holds a := r = [5,<*a,r*>];

definition

let R be good Ring;
let l be Instruction-Location of SCM R;
func goto l -> Instruction of equals :: SCMRING2:def 8
[6,<*l*>];
coherence
[6,<*l*>] is Instruction of

proof end;

end;

:: deftheorem defines goto SCMRING2:def 8 :

for R being good Ring
for l being Instruction-Location of SCM R holds goto l = [6,<*l*>];

definition

let R be good Ring;
let l be Instruction-Location of SCM R;
let a be Data-Location of R;
func a =0_goto l -> Instruction of equals :: SCMRING2:def 9
[7,<*l,a*>];
coherence
[7,<*l,a*>] is Instruction of

proof end;

end;

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

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

theorem Th8: :: SCMRING2:8

for R being good Ring
for I being set holds
( I is Instruction of 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 Instruction-Location of SCM R st I = goto i1 or ex a being Data-Location of R ex i1 being Instruction-Location of SCM R st I = a =0_goto i1 or ex a being Data-Location of R ex r being Element of st I = a := r ) )

proof end;

registration

let R be good Ring;
cluster SCM R -> strict IC-Ins-separated ;
coherence
SCM R is IC-Ins-separated

proof end;

end;

theorem :: SCMRING2:9

for R being good Ring holds IC (SCM R) = NAT by Def1;

theorem :: SCMRING2:10

for R being good Ring
for s being State of
for S being SCM-State of st S = s holds
IC s = IC S by Def1;

theorem :: SCMRING2:11

canceled;

theorem Th12: :: SCMRING2:12

for R being good Ring
for s being State of
for I being Instruction of
for i being Element of SCM-Instr R st i = I holds
for S being SCM-State of st S = s holds
Exec I,s = SCM-Exec-Res i,S

proof end;

begin

theorem Th13: :: SCMRING2:13

for R being good Ring
for a, b being Data-Location of R
for s being State of holds
( (Exec (a := b),s) . (IC (SCM R)) = Next & (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 Th14: :: SCMRING2:14

for R being good Ring
for a, b being Data-Location of R
for s being State of holds
( (Exec (AddTo a,b),s) . (IC (SCM R)) = Next & (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 Th15: :: SCMRING2:15

for R being good Ring
for a, b being Data-Location of R
for s being State of holds
( (Exec (SubFrom a,b),s) . (IC (SCM R)) = Next & (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 Th16: :: SCMRING2:16

for R being good Ring
for a, b being Data-Location of R
for s being State of holds
( (Exec (MultBy a,b),s) . (IC (SCM R)) = Next & (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:17

for R being good Ring
for c being Data-Location of R
for i1 being Instruction-Location of SCM R
for s being State of holds
( (Exec (goto i1),s) . (IC (SCM R)) = i1 & (Exec (goto i1),s) . c = s . c )

proof end;

theorem Th18: :: SCMRING2:18

for R being good Ring
for a, c being Data-Location of R
for i1 being Instruction-Location of SCM R
for s being State of holds
( ( s . a = 0. R implies (Exec (a =0_goto i1),s) . (IC (SCM R)) = i1 ) & ( s . a <> 0. R implies (Exec (a =0_goto i1),s) . (IC (SCM R)) = Next ) & (Exec (a =0_goto i1),s) . c = s . c )

proof end;

theorem Th19: :: SCMRING2:19

for R being good Ring
for r being Element of
for a being Data-Location of R
for s being State of holds
( (Exec (a := r),s) . (IC (SCM R)) = Next & (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;

begin

theorem Th20: :: SCMRING2:20

for R being good Ring
for I being Instruction of st ex s being State of st (Exec I,s) . (IC (SCM R)) = Next holds
not I is halting

proof end;

theorem Th21: :: SCMRING2:21

for R being good Ring
for I being Instruction of st I = [0 ,{} ] holds
I is halting

proof end;

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

proof end;

Lm2: for R being good Ring
for a, b being Data-Location of R holds not AddTo a,b is halting

proof end;

Lm3: for R being good Ring
for a, b being Data-Location of R holds not SubFrom a,b is halting

proof end;

Lm4: for R being good Ring
for a, b being Data-Location of R holds not MultBy a,b is halting

proof end;

Lm5: for R being good Ring
for i1 being Instruction-Location of SCM R holds not goto i1 is halting

proof end;

Lm6: for R being good Ring
for a being Data-Location of R
for i1 being Instruction-Location of SCM R holds not a =0_goto i1 is halting

proof end;

Lm7: for R being good Ring
for r being Element of
for a being Data-Location of R holds not a := r is halting

proof end;

registration

let R be good Ring;
let a, b be Data-Location of R;
cluster a := b -> non halting ;
coherence
not a := b is halting by Lm1;
cluster AddTo a,b -> non halting ;
coherence
not AddTo a,b is halting by Lm2;
cluster SubFrom a,b -> non halting ;
coherence
not SubFrom a,b is halting by Lm3;
cluster MultBy a,b -> non halting ;
coherence
not MultBy a,b is halting by Lm4;

end;

registration

let R be good Ring;
let i1 be Instruction-Location of SCM R;
cluster goto i1 -> non halting ;
coherence
not goto i1 is halting by Lm5;

end;

registration

let R be good Ring;
let a be Data-Location of R;
let i1 be Instruction-Location of SCM R;
cluster a =0_goto i1 -> non halting ;
coherence
not a =0_goto i1 is halting by Lm6;

end;

registration

let R be good Ring;
let a be Data-Location of R;
let r be Element of ;
cluster a := r -> non halting ;
coherence
not a := r is halting by Lm7;

end;

Lm8: for R being good Ring
for W being Instruction of st W is halting holds
W = [0 ,{} ]

proof end;

registration

let R be good Ring;
cluster SCM R -> strict halting steady-programmed definite realistic ;
coherence
( SCM R is halting & SCM R is definite & SCM R is steady-programmed & SCM R is realistic )

proof end;

end;

theorem :: SCMRING2:22

canceled;

theorem :: SCMRING2:23

canceled;

theorem :: SCMRING2:24

canceled;

theorem :: SCMRING2:25

canceled;

theorem :: SCMRING2:26

canceled;

theorem :: SCMRING2:27

canceled;

theorem :: SCMRING2:28

canceled;

theorem Th29: :: SCMRING2:29

for R being good Ring
for I being Instruction of st I is halting holds
I = halt (SCM R)

proof end;

theorem :: SCMRING2:30

for R being good Ring holds halt (SCM R) = [0 ,{} ]

proof end;

theorem :: SCMRING2:31

for R being good Ring holds Data-Locations (SCM R) = SCM-Data-Loc

proof end;