:: SCMRING2 semantic presentation

definition

let c₁ be good Ring;
func SCM c₁ -> strict AMI-Struct of {the carrier of a₁} means :Def1: :: SCMRING2:def 1
( the carrier of a₂ = NAT & the Instruction-Counter of a₂ = 0 & the Instruction-Locations of a₂ = SCM-Instr-Loc & the Instruction-Codes of a₂ = Segm 8 & the Instructions of a₂ = SCM-Instr a₁ & the Object-Kind of a₂ = SCM-OK a₁ & the Execution of a₂ = SCM-Exec a₁ );
existence

proof end;

uniqueness ;

end;

:: deftheorem Def1 defines SCM SCMRING2:def 1 :

registration

let c₁ be good Ring;
cluster SCM a₁ -> non empty strict non void ;
coherence

proof end;

end;

definition

let c₁ be good Ring;
let c₂ be State of (SCM c₁);
let c₃ be Element of SCM-Data-Loc ;
redefine func . as c₂ . c₃ -> Element of a₁;
coherence

proof end;

end;

definition

let c₁ be good Ring;
mode Data-Location of c₁ -> Object of (SCM a₁) means :Def2: :: SCMRING2:def 2
a₂ in the carrier of (SCM a₁) \ (SCM-Instr-Loc \/ {0});
existence

proof end;

end;

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

theorem Th1: :: SCMRING2:1

for b₁ being set
for b₂ being good Ring holds
( b₁ is Data-Location of b₂ iff b₁ in SCM-Data-Loc )

proof end;

definition

let c₁ be good Ring;
let c₂ be State of (SCM c₁);
let c₃ be Data-Location of c₁;
redefine func . as c₂ . c₃ -> Element of a₁;
coherence

proof end;

end;

theorem Th2: :: SCMRING2:2

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

proof end;

theorem Th3: :: SCMRING2:3

for b₁ being good Ring holds [0,{} ] is Instruction of (SCM b₁)

proof end;

theorem Th4: :: SCMRING2:4

for b₁ being non empty 1-sorted
for b₂ being set
for b₃ being good Ring
for b₄, b₅ being Data-Location of b₃ st b₂ in {1,2,3,4} holds
[b₂,<*b₄,b₅*>] in SCM-Instr b₁

proof end;

theorem Th5: :: SCMRING2:5

for b₁ being non empty 1-sorted
for b₂ being Element of b₁
for b₃ being good Ring
for b₄ being Data-Location of b₃ holds [5,<*b₄,b₂*>] in SCM-Instr b₁

proof end;

theorem Th6: :: SCMRING2:6

for b₁ being non empty 1-sorted
for b₂ being good Ring
for b₃ being Instruction-Location of (SCM b₂) holds [6,<*b₃*>] in SCM-Instr b₁

proof end;

theorem Th7: :: SCMRING2:7

for b₁ being non empty 1-sorted
for b₂ being good Ring
for b₃ being Data-Location of b₂
for b₄ being Instruction-Location of (SCM b₂) holds [7,<*b₄,b₃*>] in SCM-Instr b₁

proof end;

definition

let c₁ be good Ring;
let c₂, c₃ be Data-Location of c₁;
func c₂ := c₃ -> Instruction of (SCM a₁) equals :: SCMRING2:def 3
[1,<*a₂,a₃*>];
coherence

proof end;

func AddTo c₂,c₃ -> Instruction of (SCM a₁) equals :: SCMRING2:def 4
[2,<*a₂,a₃*>];
coherence

proof end;

func SubFrom c₂,c₃ -> Instruction of (SCM a₁) equals :: SCMRING2:def 5
[3,<*a₂,a₃*>];
coherence

proof end;

func MultBy c₂,c₃ -> Instruction of (SCM a₁) equals :: SCMRING2:def 6
[4,<*a₂,a₃*>];
coherence

proof end;

end;

:: deftheorem Def3 defines := SCMRING2:def 3 :

:: deftheorem Def4 defines AddTo SCMRING2:def 4 :

:: deftheorem Def5 defines SubFrom SCMRING2:def 5 :

:: deftheorem Def6 defines MultBy SCMRING2:def 6 :

definition

let c₁ be good Ring;
let c₂ be Data-Location of c₁;
let c₃ be Element of c₁;
func c₂ := c₃ -> Instruction of (SCM a₁) equals :: SCMRING2:def 7
[5,<*a₂,a₃*>];
coherence

proof end;

end;

:: deftheorem Def7 defines := SCMRING2:def 7 :

definition

let c₁ be good Ring;
let c₂ be Instruction-Location of (SCM c₁);
func goto c₂ -> Instruction of (SCM a₁) equals :: SCMRING2:def 8
[6,<*a₂*>];
coherence

proof end;

end;

:: deftheorem Def8 defines goto SCMRING2:def 8 :

definition

let c₁ be good Ring;
let c₂ be Instruction-Location of (SCM c₁);
let c₃ be Data-Location of c₁;
func c₃ =0_goto c₂ -> Instruction of (SCM a₁) equals :: SCMRING2:def 9
[7,<*a₂,a₃*>];
coherence

proof end;

end;

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

theorem Th8: :: SCMRING2:8

for b₁ being good Ring
for b₂ being set holds
( b₂ is Instruction of (SCM b₁) iff ( b₂ = [0,{} ] or ex b₃, b₄ being Data-Location of b₁ st b₂ = b₃ := b₄ or ex b₃, b₄ being Data-Location of b₁ st b₂ = AddTo b₃,b₄ or ex b₃, b₄ being Data-Location of b₁ st b₂ = SubFrom b₃,b₄ or ex b₃, b₄ being Data-Location of b₁ st b₂ = MultBy b₃,b₄ or ex b₃ being Instruction-Location of (SCM b₁) st b₂ = goto b₃ or ex b₃ being Data-Location of b₁ex b₄ being Instruction-Location of (SCM b₁) st b₂ = b₃ =0_goto b₄ or ex b₃ being Data-Location of b₁ex b₄ being Element of b₁ st b₂ = b₃ := b₄ ) )

proof end;

registration

let c₁ be good Ring;
cluster SCM a₁ -> non empty strict non void IC-Ins-separated ;
coherence

proof end;

end;

theorem Th9: :: SCMRING2:9

for b₁ being good Ring holds IC (SCM b₁) = 0 by Def1;

theorem Th10: :: SCMRING2:10

for b₁ being good Ring
for b₂ being State of (SCM b₁)
for b₃ being SCM-State of b₁ st b₃ = b₂ holds
IC b₂ = IC b₃

proof end;

definition

let c₁ be good Ring;
let c₂ be Instruction-Location of (SCM c₁);
func Next c₂ -> Instruction-Location of (SCM a₁) means :Def10: :: SCMRING2:def 10
ex b₁ being Element of SCM-Instr-Loc st
( b₁ = a₂ & a₃ = Next b₁ );
existence

proof end;

uniqueness ;

end;

:: deftheorem Def10 defines Next SCMRING2:def 10 :

theorem Th11: :: SCMRING2:11

for b₁ being good Ring
for b₂ being Instruction-Location of (SCM b₁)
for b₃ being Element of SCM-Instr-Loc st b₃ = b₂ holds
Next b₃ = Next b₂

proof end;

theorem Th12: :: SCMRING2:12

for b₁ being good Ring
for b₂ being State of (SCM b₁)
for b₃ being Instruction of (SCM b₁)
for b₄ being Element of SCM-Instr b₁ st b₄ = b₃ holds
for b₅ being SCM-State of b₁ st b₅ = b₂ holds
Exec b₃,b₂ = SCM-Exec-Res b₄,b₅

proof end;

theorem Th13: :: SCMRING2:13

for b₁ being good Ring
for b₂, b₃ being Data-Location of b₁
for b₄ being State of (SCM b₁) holds
( (Exec (b₂ := b₃),b₄) . (IC (SCM b₁)) = Next (IC b₄) & (Exec (b₂ := b₃),b₄) . b₂ = b₄ . b₃ & ( for b₅ being Data-Location of b₁ st b₅ <> b₂ holds
(Exec (b₂ := b₃),b₄) . b₅ = b₄ . b₅ ) )

proof end;

theorem Th14: :: SCMRING2:14

for b₁ being good Ring
for b₂, b₃ being Data-Location of b₁
for b₄ being State of (SCM b₁) holds
( (Exec (AddTo b₂,b₃),b₄) . (IC (SCM b₁)) = Next (IC b₄) & (Exec (AddTo b₂,b₃),b₄) . b₂ = (b₄ . b₂) + (b₄ . b₃) & ( for b₅ being Data-Location of b₁ st b₅ <> b₂ holds
(Exec (AddTo b₂,b₃),b₄) . b₅ = b₄ . b₅ ) )

proof end;

theorem Th15: :: SCMRING2:15

for b₁ being good Ring
for b₂, b₃ being Data-Location of b₁
for b₄ being State of (SCM b₁) holds
( (Exec (SubFrom b₂,b₃),b₄) . (IC (SCM b₁)) = Next (IC b₄) & (Exec (SubFrom b₂,b₃),b₄) . b₂ = (b₄ . b₂) - (b₄ . b₃) & ( for b₅ being Data-Location of b₁ st b₅ <> b₂ holds
(Exec (SubFrom b₂,b₃),b₄) . b₅ = b₄ . b₅ ) )

proof end;

theorem Th16: :: SCMRING2:16

for b₁ being good Ring
for b₂, b₃ being Data-Location of b₁
for b₄ being State of (SCM b₁) holds
( (Exec (MultBy b₂,b₃),b₄) . (IC (SCM b₁)) = Next (IC b₄) & (Exec (MultBy b₂,b₃),b₄) . b₂ = (b₄ . b₂) * (b₄ . b₃) & ( for b₅ being Data-Location of b₁ st b₅ <> b₂ holds
(Exec (MultBy b₂,b₃),b₄) . b₅ = b₄ . b₅ ) )

proof end;

theorem Th17: :: SCMRING2:17

for b₁ being good Ring
for b₂ being Data-Location of b₁
for b₃ being Instruction-Location of (SCM b₁)
for b₄ being State of (SCM b₁) holds
( (Exec (goto b₃),b₄) . (IC (SCM b₁)) = b₃ & (Exec (goto b₃),b₄) . b₂ = b₄ . b₂ )

proof end;

theorem Th18: :: SCMRING2:18

for b₁ being good Ring
for b₂, b₃ being Data-Location of b₁
for b₄ being Instruction-Location of (SCM b₁)
for b₅ being State of (SCM b₁) holds
( ( b₅ . b₂ = 0. b₁ implies (Exec (b₂ =0_goto b₄),b₅) . (IC (SCM b₁)) = b₄ ) & ( b₅ . b₂ <> 0. b₁ implies (Exec (b₂ =0_goto b₄),b₅) . (IC (SCM b₁)) = Next (IC b₅) ) & (Exec (b₂ =0_goto b₄),b₅) . b₃ = b₅ . b₃ )

proof end;

theorem Th19: :: SCMRING2:19

for b₁ being good Ring
for b₂ being Element of b₁
for b₃ being Data-Location of b₁
for b₄ being State of (SCM b₁) holds
( (Exec (b₃ := b₂),b₄) . (IC (SCM b₁)) = Next (IC b₄) & (Exec (b₃ := b₂),b₄) . b₃ = b₂ & ( for b₅ being Data-Location of b₁ st b₅ <> b₃ holds
(Exec (b₃ := b₂),b₄) . b₅ = b₄ . b₅ ) )

proof end;

theorem Th20: :: SCMRING2:20

for b₁ being good Ring
for b₂ being Instruction of (SCM b₁) st ex b₃ being State of (SCM b₁) st (Exec b₂,b₃) . (IC (SCM b₁)) = Next (IC b₃) holds
not b₂ is halting

proof end;

theorem Th21: :: SCMRING2:21

for b₁ being good Ring
for b₂ being Instruction of (SCM b₁) st b₂ = [0,{} ] holds
b₂ is halting

proof end;

Lemma24: for b₁ being good Ring
for b₂, b₃ being Data-Location of b₁ holds not b₂ := b₃ is halting

proof end;

Lemma25: for b₁ being good Ring
for b₂, b₃ being Data-Location of b₁ holds not AddTo b₂,b₃ is halting

proof end;

Lemma26: for b₁ being good Ring
for b₂, b₃ being Data-Location of b₁ holds not SubFrom b₂,b₃ is halting

proof end;

Lemma27: for b₁ being good Ring
for b₂, b₃ being Data-Location of b₁ holds not MultBy b₂,b₃ is halting

proof end;

Lemma28: for b₁ being good Ring
for b₂ being Instruction-Location of (SCM b₁) holds not goto b₂ is halting

proof end;

Lemma29: for b₁ being good Ring
for b₂ being Data-Location of b₁
for b₃ being Instruction-Location of (SCM b₁) holds not b₂ =0_goto b₃ is halting

proof end;

Lemma30: for b₁ being good Ring
for b₂ being Element of b₁
for b₃ being Data-Location of b₁ holds not b₃ := b₂ is halting

proof end;

registration

let c₁ be good Ring;
let c₂, c₃ be Data-Location of c₁;
cluster a₂ := a₃ -> non halting ;
coherence by Lemma24;
cluster AddTo a₂,a₃ -> non halting ;
coherence by Lemma25;
cluster SubFrom a₂,a₃ -> non halting ;
coherence by Lemma26;
cluster MultBy a₂,a₃ -> non halting ;
coherence by Lemma27;

end;

registration

let c₁ be good Ring;
let c₂ be Instruction-Location of (SCM c₁);
cluster goto a₂ -> non halting ;
coherence by Lemma28;

end;

registration

let c₁ be good Ring;
let c₂ be Data-Location of c₁;
let c₃ be Instruction-Location of (SCM c₁);
cluster a₂ =0_goto a₃ -> non halting ;
coherence by Lemma29;

end;

registration

let c₁ be good Ring;
let c₂ be Data-Location of c₁;
let c₃ be Element of c₁;
cluster a₂ := a₃ -> non halting ;
coherence by Lemma30;

end;

registration

let c₁ be good Ring;
cluster SCM a₁ -> non empty strict non void halting IC-Ins-separated data-oriented steady-programmed definite realistic ;
coherence

proof end;

end;

theorem Th22: :: SCMRING2:22

canceled;

theorem Th23: :: SCMRING2:23

canceled;

theorem Th24: :: SCMRING2:24

canceled;

theorem Th25: :: SCMRING2:25

canceled;

theorem Th26: :: SCMRING2:26

canceled;

theorem Th27: :: SCMRING2:27

canceled;

theorem Th28: :: SCMRING2:28

canceled;

theorem Th29: :: SCMRING2:29

for b₁ being good Ring
for b₂ being Instruction of (SCM b₁) st b₂ is halting holds
b₂ = halt (SCM b₁)

proof end;

theorem Th30: :: SCMRING2:30

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

proof end;