:: SCMRING3 semantic presentation

registration

cluster INT -> infinite ;
coherence by FINSET_1:13, NUMBERS:17;

end;

registration

cluster INT.Ring -> infinite good ;
coherence

proof end;

end;

registration

cluster strict infinite 1-sorted ;
existence

proof end;

end;

registration

cluster infinite strict good L9();
existence

proof end;

end;

theorem Th1: :: SCMRING3:1

for b₁ being good Ring
for b₂ being Data-Location of b₁ holds ObjectKind b₂ = the carrier of b₁

proof end;

definition

let c₁ be good Ring;
let c₂, c₃ be Data-Location of c₁;
let c₄, c₅ be Element of c₁;
redefine func --> as c₂,c₃ --> c₄,c₅ -> FinPartState of SCM a₁;
coherence

proof end;

end;

theorem Th2: :: SCMRING3:2

for b₁ being good Ring
for b₂ being Data-Location of b₁ holds not b₂ in the Instruction-Locations of (SCM b₁)

proof end;

theorem Th3: :: SCMRING3:3

for b₁ being good Ring
for b₂ being Data-Location of b₁ holds b₂ <> IC (SCM b₁)

proof end;

theorem Th4: :: SCMRING3:4

for b₁ being good Ring holds SCM-Data-Loc <> the Instruction-Locations of (SCM b₁)

proof end;

theorem Th5: :: SCMRING3:5

for b₁ being good Ring
for b₂ being Object of (SCM b₁) holds
( b₂ = IC (SCM b₁) or b₂ in the Instruction-Locations of (SCM b₁) or b₂ is Data-Location of b₁ )

proof end;

theorem Th6: :: SCMRING3:6

for b₁ being good Ring
for b₂, b₃ being Instruction-Location of (SCM b₁) st b₂ <> b₃ holds
Next b₂ <> Next b₃

proof end;

theorem Th7: :: SCMRING3:7

for b₁ being good Ring
for b₂ being Data-Location of b₁
for b₃, b₄ being State of (SCM b₁) st b₃,b₄ equal_outside the Instruction-Locations of (SCM b₁) holds
b₃ . b₂ = b₄ . b₂

proof end;

theorem Th8: :: SCMRING3:8

for b₁ being good Ring holds InsCode (halt (SCM b₁)) = 0

proof end;

theorem Th9: :: SCMRING3:9

for b₁ being good Ring
for b₂, b₃ being Data-Location of b₁ holds InsCode (b₂ := b₃) = 1

proof end;

theorem Th10: :: SCMRING3:10

for b₁ being good Ring
for b₂, b₃ being Data-Location of b₁ holds InsCode (AddTo b₂,b₃) = 2

proof end;

theorem Th11: :: SCMRING3:11

for b₁ being good Ring
for b₂, b₃ being Data-Location of b₁ holds InsCode (SubFrom b₂,b₃) = 3

proof end;

theorem Th12: :: SCMRING3:12

for b₁ being good Ring
for b₂, b₃ being Data-Location of b₁ holds InsCode (MultBy b₂,b₃) = 4

proof end;

theorem Th13: :: SCMRING3:13

for b₁ being good Ring
for b₂ being Element of b₁
for b₃ being Data-Location of b₁ holds InsCode (b₃ := b₂) = 5

proof end;

theorem Th14: :: SCMRING3:14

for b₁ being good Ring
for b₂ being Instruction-Location of (SCM b₁) holds InsCode (goto b₂) = 6

proof end;

theorem Th15: :: SCMRING3:15

for b₁ being good Ring
for b₂ being Data-Location of b₁
for b₃ being Instruction-Location of (SCM b₁) holds InsCode (b₂ =0_goto b₃) = 7

proof end;

theorem Th16: :: SCMRING3:16

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

proof end;

theorem Th17: :: SCMRING3:17

for b₁ being good Ring
for b₂ being Instruction of (SCM b₁) st InsCode b₂ = 1 holds
ex b₃, b₄ being Data-Location of b₁ st b₂ = b₃ := b₄

proof end;

theorem Th18: :: SCMRING3:18

for b₁ being good Ring
for b₂ being Instruction of (SCM b₁) st InsCode b₂ = 2 holds
ex b₃, b₄ being Data-Location of b₁ st b₂ = AddTo b₃,b₄

proof end;

theorem Th19: :: SCMRING3:19

for b₁ being good Ring
for b₂ being Instruction of (SCM b₁) st InsCode b₂ = 3 holds
ex b₃, b₄ being Data-Location of b₁ st b₂ = SubFrom b₃,b₄

proof end;

theorem Th20: :: SCMRING3:20

for b₁ being good Ring
for b₂ being Instruction of (SCM b₁) st InsCode b₂ = 4 holds
ex b₃, b₄ being Data-Location of b₁ st b₂ = MultBy b₃,b₄

proof end;

theorem Th21: :: SCMRING3:21

for b₁ being good Ring
for b₂ being Instruction of (SCM b₁) st InsCode b₂ = 5 holds
ex b₃ being Data-Location of b₁ex b₄ being Element of b₁ st b₂ = b₃ := b₄

proof end;

theorem Th22: :: SCMRING3:22

for b₁ being good Ring
for b₂ being Instruction of (SCM b₁) st InsCode b₂ = 6 holds
ex b₃ being Instruction-Location of (SCM b₁) st b₂ = goto b₃

proof end;

theorem Th23: :: SCMRING3:23

for b₁ being good Ring
for b₂ being Instruction of (SCM b₁) st InsCode b₂ = 7 holds
ex b₃ being Data-Location of b₁ex b₄ being Instruction-Location of (SCM b₁) st b₂ = b₃ =0_goto b₄

proof end;

Lemma24: for b₁, b₂ being set st b₁ in dom <*b₂*> holds
b₁ = 1

proof end;

Lemma25: for b₁, b₂, b₃ being set holds
( not b₁ in dom <*b₂,b₃*> or b₁ = 1 or b₁ = 2 )

proof end;

Lemma26: for b₁ being good Ring
for b₂ being InsType of (SCM b₁) holds
( b₂ = 0 or b₂ = 1 or b₂ = 2 or b₂ = 3 or b₂ = 4 or b₂ = 5 or b₂ = 6 or b₂ = 7 )

proof end;

theorem Th24: :: SCMRING3:24

for b₁ being good Ring holds AddressPart (halt (SCM b₁)) = {}

proof end;

theorem Th25: :: SCMRING3:25

for b₁ being good Ring
for b₂, b₃ being Data-Location of b₁ holds AddressPart (b₂ := b₃) = <*b₂,b₃*> by MCART_1:def 2;

theorem Th26: :: SCMRING3:26

for b₁ being good Ring
for b₂, b₃ being Data-Location of b₁ holds AddressPart (AddTo b₂,b₃) = <*b₂,b₃*> by MCART_1:def 2;

theorem Th27: :: SCMRING3:27

for b₁ being good Ring
for b₂, b₃ being Data-Location of b₁ holds AddressPart (SubFrom b₂,b₃) = <*b₂,b₃*> by MCART_1:def 2;

theorem Th28: :: SCMRING3:28

for b₁ being good Ring
for b₂, b₃ being Data-Location of b₁ holds AddressPart (MultBy b₂,b₃) = <*b₂,b₃*> by MCART_1:def 2;

theorem Th29: :: SCMRING3:29

for b₁ being good Ring
for b₂ being Element of b₁
for b₃ being Data-Location of b₁ holds AddressPart (b₃ := b₂) = <*b₃,b₂*> by MCART_1:def 2;

theorem Th30: :: SCMRING3:30

for b₁ being good Ring
for b₂ being Instruction-Location of (SCM b₁) holds AddressPart (goto b₂) = <*b₂*> by MCART_1:def 2;

theorem Th31: :: SCMRING3:31

for b₁ being good Ring
for b₂ being Data-Location of b₁
for b₃ being Instruction-Location of (SCM b₁) holds AddressPart (b₂ =0_goto b₃) = <*b₃,b₂*> by MCART_1:def 2;

theorem Th32: :: SCMRING3:32

for b₁ being good Ring
for b₂ being InsType of (SCM b₁) st b₂ = 0 holds
AddressParts b₂ = {0}

proof end;

registration

let c₁ be good Ring;
let c₂ be InsType of (SCM c₁);
cluster AddressParts a₂ -> non empty ;
coherence

proof end;

end;

theorem Th33: :: SCMRING3:33

for b₁ being good Ring
for b₂ being InsType of (SCM b₁) st b₂ = 1 holds
dom (PA (AddressParts b₂)) = {1,2}

proof end;

theorem Th34: :: SCMRING3:34

for b₁ being good Ring
for b₂ being InsType of (SCM b₁) st b₂ = 2 holds
dom (PA (AddressParts b₂)) = {1,2}

proof end;

theorem Th35: :: SCMRING3:35

for b₁ being good Ring
for b₂ being InsType of (SCM b₁) st b₂ = 3 holds
dom (PA (AddressParts b₂)) = {1,2}

proof end;

theorem Th36: :: SCMRING3:36

for b₁ being good Ring
for b₂ being InsType of (SCM b₁) st b₂ = 4 holds
dom (PA (AddressParts b₂)) = {1,2}

proof end;

theorem Th37: :: SCMRING3:37

for b₁ being good Ring
for b₂ being InsType of (SCM b₁) st b₂ = 5 holds
dom (PA (AddressParts b₂)) = {1,2}

proof end;

theorem Th38: :: SCMRING3:38

for b₁ being good Ring
for b₂ being InsType of (SCM b₁) st b₂ = 6 holds
dom (PA (AddressParts b₂)) = {1}

proof end;

theorem Th39: :: SCMRING3:39

for b₁ being good Ring
for b₂ being InsType of (SCM b₁) st b₂ = 7 holds
dom (PA (AddressParts b₂)) = {1,2}

proof end;

theorem Th40: :: SCMRING3:40

for b₁ being good Ring
for b₂, b₃ being Data-Location of b₁ holds (PA (AddressParts (InsCode (b₂ := b₃)))) . 1 = SCM-Data-Loc

proof end;

theorem Th41: :: SCMRING3:41

for b₁ being good Ring
for b₂, b₃ being Data-Location of b₁ holds (PA (AddressParts (InsCode (b₂ := b₃)))) . 2 = SCM-Data-Loc

proof end;

theorem Th42: :: SCMRING3:42

for b₁ being good Ring
for b₂, b₃ being Data-Location of b₁ holds (PA (AddressParts (InsCode (AddTo b₂,b₃)))) . 1 = SCM-Data-Loc

proof end;

theorem Th43: :: SCMRING3:43

for b₁ being good Ring
for b₂, b₃ being Data-Location of b₁ holds (PA (AddressParts (InsCode (AddTo b₂,b₃)))) . 2 = SCM-Data-Loc

proof end;

theorem Th44: :: SCMRING3:44

for b₁ being good Ring
for b₂, b₃ being Data-Location of b₁ holds (PA (AddressParts (InsCode (SubFrom b₂,b₃)))) . 1 = SCM-Data-Loc

proof end;

theorem Th45: :: SCMRING3:45

for b₁ being good Ring
for b₂, b₃ being Data-Location of b₁ holds (PA (AddressParts (InsCode (SubFrom b₂,b₃)))) . 2 = SCM-Data-Loc

proof end;

theorem Th46: :: SCMRING3:46

for b₁ being good Ring
for b₂, b₃ being Data-Location of b₁ holds (PA (AddressParts (InsCode (MultBy b₂,b₃)))) . 1 = SCM-Data-Loc

proof end;

theorem Th47: :: SCMRING3:47

for b₁ being good Ring
for b₂, b₃ being Data-Location of b₁ holds (PA (AddressParts (InsCode (MultBy b₂,b₃)))) . 2 = SCM-Data-Loc

proof end;

theorem Th48: :: SCMRING3:48

for b₁ being good Ring
for b₂ being Element of b₁
for b₃ being Data-Location of b₁ holds (PA (AddressParts (InsCode (b₃ := b₂)))) . 1 = SCM-Data-Loc

proof end;

theorem Th49: :: SCMRING3:49

for b₁ being good Ring
for b₂ being Element of b₁
for b₃ being Data-Location of b₁ holds (PA (AddressParts (InsCode (b₃ := b₂)))) . 2 = the carrier of b₁

proof end;

theorem Th50: :: SCMRING3:50

for b₁ being good Ring
for b₂ being Instruction-Location of (SCM b₁) holds (PA (AddressParts (InsCode (goto b₂)))) . 1 = the Instruction-Locations of (SCM b₁)

proof end;

theorem Th51: :: SCMRING3:51

for b₁ being good Ring
for b₂ being Data-Location of b₁
for b₃ being Instruction-Location of (SCM b₁) holds (PA (AddressParts (InsCode (b₂ =0_goto b₃)))) . 1 = the Instruction-Locations of (SCM b₁)

proof end;

theorem Th52: :: SCMRING3:52

for b₁ being good Ring
for b₂ being Data-Location of b₁
for b₃ being Instruction-Location of (SCM b₁) holds (PA (AddressParts (InsCode (b₂ =0_goto b₃)))) . 2 = SCM-Data-Loc

proof end;

Lemma56: for b₁ being with_non-empty_elements set
for b₂ being non empty non void IC-Ins-separated definite realistic AMI-Struct of b₁
for b₃, b₄ being State of b₂
for b₅ being Instruction-Location of b₂
for b₆ being Element of ObjectKind (IC b₂)
for b₇ being Element of ObjectKind b₅ st b₆ = b₅ & b₄ = b₃ +* ((IC b₂),b₅ --> b₆,b₇) holds
( b₄ . b₅ = b₇ & IC b₄ = b₅ & IC (Following b₄) = (Exec (b₄ . (IC b₄)),b₄) . (IC b₂) )

proof end;

Lemma57: for b₁ being good Ring
for b₂ being Instruction-Location of (SCM b₁)
for b₃ being Instruction of (SCM b₁) st ( for b₄ being State of (SCM b₁) st IC b₄ = b₂ & b₄ . b₂ = b₃ holds
(Exec b₃,b₄) . (IC (SCM b₁)) = Next (IC b₄) ) holds
NIC b₃,b₂ = {(Next b₂)}

proof end;

Lemma58: for b₁ being good Ring
for b₂ being Instruction of (SCM b₁) st ( for b₃ being Instruction-Location of (SCM b₁) holds NIC b₂,b₃ = {(Next b₃)} ) holds
JUMP b₂ is empty

proof end;

theorem Th53: :: SCMRING3:53

for b₁ being good Ring
for b₂ being Instruction-Location of (SCM b₁) holds NIC (halt (SCM b₁)),b₂ = {b₂}

proof end;

registration

let c₁ be good Ring;
cluster JUMP (halt (SCM a₁)) -> empty ;
coherence

proof end;

end;

theorem Th54: :: SCMRING3:54

for b₁ being good Ring
for b₂, b₃ being Data-Location of b₁
for b₄ being Instruction-Location of (SCM b₁) holds NIC (b₂ := b₃),b₄ = {(Next b₄)}

proof end;

registration

let c₁ be good Ring;
let c₂, c₃ be Data-Location of c₁;
cluster JUMP (a₂ := a₃) -> empty ;
coherence

proof end;

end;

theorem Th55: :: SCMRING3:55

for b₁ being good Ring
for b₂, b₃ being Data-Location of b₁
for b₄ being Instruction-Location of (SCM b₁) holds NIC (AddTo b₂,b₃),b₄ = {(Next b₄)}

proof end;

registration

let c₁ be good Ring;
let c₂, c₃ be Data-Location of c₁;
cluster JUMP (AddTo a₂,a₃) -> empty ;
coherence

proof end;

end;

theorem Th56: :: SCMRING3:56

for b₁ being good Ring
for b₂, b₃ being Data-Location of b₁
for b₄ being Instruction-Location of (SCM b₁) holds NIC (SubFrom b₂,b₃),b₄ = {(Next b₄)}

proof end;

registration

let c₁ be good Ring;
let c₂, c₃ be Data-Location of c₁;
cluster JUMP (SubFrom a₂,a₃) -> empty ;
coherence

proof end;

end;

theorem Th57: :: SCMRING3:57

for b₁ being good Ring
for b₂, b₃ being Data-Location of b₁
for b₄ being Instruction-Location of (SCM b₁) holds NIC (MultBy b₂,b₃),b₄ = {(Next b₄)}

proof end;

registration

let c₁ be good Ring;
let c₂, c₃ be Data-Location of c₁;
cluster JUMP (MultBy a₂,a₃) -> empty ;
coherence

proof end;

end;

theorem Th58: :: SCMRING3:58

for b₁ being good Ring
for b₂ being Element of b₁
for b₃ being Data-Location of b₁
for b₄ being Instruction-Location of (SCM b₁) holds NIC (b₃ := b₂),b₄ = {(Next b₄)}

proof end;

registration

let c₁ be good Ring;
let c₂ be Data-Location of c₁;
let c₃ be Element of c₁;
cluster JUMP (a₂ := a₃) -> empty ;
coherence

proof end;

end;

theorem Th59: :: SCMRING3:59

for b₁ being good Ring
for b₂, b₃ being Instruction-Location of (SCM b₁) holds NIC (goto b₂),b₃ = {b₂}

proof end;

theorem Th60: :: SCMRING3:60

for b₁ being good Ring
for b₂ being Instruction-Location of (SCM b₁) holds JUMP (goto b₂) = {b₂}

proof end;

registration

let c₁ be good Ring;
let c₂ be Instruction-Location of (SCM c₁);
cluster JUMP (goto a₂) -> non empty trivial ;
coherence

proof end;

end;

theorem Th61: :: SCMRING3:61

for b₁ being good Ring
for b₂ being Data-Location of b₁
for b₃, b₄ being Instruction-Location of (SCM b₁) holds
( b₃ in NIC (b₂ =0_goto b₃),b₄ & NIC (b₂ =0_goto b₃),b₄ c= {b₃,(Next b₄)} )

proof end;

theorem Th62: :: SCMRING3:62

for b₁ being good non trivial Ring
for b₂ being Data-Location of b₁
for b₃, b₄ being Instruction-Location of (SCM b₁) holds NIC (b₂ =0_goto b₄),b₃ = {b₄,(Next b₃)}

proof end;

theorem Th63: :: SCMRING3:63

for b₁ being good Ring
for b₂ being Data-Location of b₁
for b₃ being Instruction-Location of (SCM b₁) holds JUMP (b₂ =0_goto b₃) = {b₃}

proof end;

registration

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

proof end;

end;

theorem Th64: :: SCMRING3:64

for b₁ being good Ring
for b₂ being Instruction-Location of (SCM b₁) holds SUCC b₂ = {b₂,(Next b₂)}

proof end;

theorem Th65: :: SCMRING3:65

for b₁ being good Ring
for b₂ being Function of NAT ,the Instruction-Locations of (SCM b₁) st ( for b₃ being Nat holds b₂ . b₃ = il. b₃ ) holds
( b₂ is bijective & ( for b₃ being Nat holds
( b₂ . (b₃ + 1) in SUCC (b₂ . b₃) & ( for b₄ being Nat st b₂ . b₄ in SUCC (b₂ . b₃) holds
b₃ <= b₄ ) ) ) )

proof end;

registration

let c₁ be good Ring;
cluster SCM a₁ -> standard ;
coherence

proof end;

end;

theorem Th66: :: SCMRING3:66

for b₁ being good Ring
for b₂ being natural number holds il. (SCM b₁),b₂ = il. b₂

proof end;

theorem Th67: :: SCMRING3:67

for b₁ being good Ring
for b₂ being natural number holds Next (il. (SCM b₁),b₂) = il. (SCM b₁),(b₂ + 1)

proof end;

theorem Th68: :: SCMRING3:68

for b₁ being good Ring
for b₂ being Instruction-Location of (SCM b₁) holds Next b₂ = NextLoc b₂

proof end;

definition

let c₁ be good Ring;
let c₂ be Nat;
func dl. c₁,c₂ -> Data-Location of a₁ equals :: SCMRING3:def 1
dl. a₂;
coherence

proof end;

end;

:: deftheorem Def1 defines dl. SCMRING3:def 1 :

registration

let c₁ be good Ring;
cluster InsCode (halt (SCM a₁)) -> jump-only ;
coherence

proof end;

end;

registration

let c₁ be good Ring;
cluster halt (SCM a₁) -> jump-only ;
coherence

proof end;

end;

registration

let c₁ be good Ring;
let c₂ be Instruction-Location of (SCM c₁);
cluster InsCode (goto a₂) -> jump-only ;
coherence

proof end;

end;

registration

let c₁ be good Ring;
let c₂ be Instruction-Location of (SCM c₁);
cluster goto a₂ -> jump-only ;
coherence

proof end;

end;

registration

let c₁ be good Ring;
let c₂ be Data-Location of c₁;
let c₃ be Instruction-Location of (SCM c₁);
cluster InsCode (a₂ =0_goto a₃) -> jump-only ;
coherence

proof end;

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₃ -> jump-only ;
coherence

proof end;

end;

registration

let c₁ be good non trivial Ring;
let c₂, c₃ be Data-Location of c₁;
cluster InsCode (a₂ := a₃) -> non jump-only ;
coherence

proof end;

end;

registration

let c₁ be good non trivial Ring;
let c₂, c₃ be Data-Location of c₁;
cluster a₂ := a₃ -> non jump-only ;
coherence

proof end;

end;

registration

let c₁ be good non trivial Ring;
let c₂, c₃ be Data-Location of c₁;
cluster InsCode (AddTo a₂,a₃) -> non jump-only ;
coherence

proof end;

end;

registration

let c₁ be good non trivial Ring;
let c₂, c₃ be Data-Location of c₁;
cluster AddTo a₂,a₃ -> non jump-only ;
coherence

proof end;

end;

registration

let c₁ be good non trivial Ring;
let c₂, c₃ be Data-Location of c₁;
cluster InsCode (SubFrom a₂,a₃) -> non jump-only ;
coherence

proof end;

end;

registration

let c₁ be good non trivial Ring;
let c₂, c₃ be Data-Location of c₁;
cluster SubFrom a₂,a₃ -> non jump-only ;
coherence

proof end;

end;

registration

let c₁ be good non trivial Ring;
let c₂, c₃ be Data-Location of c₁;
cluster InsCode (MultBy a₂,a₃) -> non jump-only ;
coherence

proof end;

end;

registration

let c₁ be good non trivial Ring;
let c₂, c₃ be Data-Location of c₁;
cluster MultBy a₂,a₃ -> non jump-only ;
coherence

proof end;

end;

registration

let c₁ be good non trivial Ring;
let c₂ be Data-Location of c₁;
let c₃ be Element of c₁;
cluster InsCode (a₂ := a₃) -> non jump-only ;
coherence

proof end;

end;

registration

let c₁ be good non trivial Ring;
let c₂ be Data-Location of c₁;
let c₃ be Element of c₁;
cluster a₂ := a₃ -> non jump-only ;
coherence

proof end;

end;

registration

let c₁ be good Ring;
let c₂, c₃ be Data-Location of c₁;
cluster a₂ := a₃ -> sequential ;
coherence

proof end;

end;

registration

let c₁ be good Ring;
let c₂, c₃ be Data-Location of c₁;
cluster AddTo a₂,a₃ -> sequential ;
coherence

proof end;

end;

registration

let c₁ be good Ring;
let c₂, c₃ be Data-Location of c₁;
cluster SubFrom a₂,a₃ -> sequential ;
coherence

proof end;

end;

registration

let c₁ be good Ring;
let c₂, c₃ be Data-Location of c₁;
cluster MultBy a₂,a₃ -> sequential ;
coherence

proof end;

end;

registration

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

proof end;

end;

registration

let c₁ be good Ring;
let c₂ be Instruction-Location of (SCM c₁);
cluster goto a₂ -> jump-only non sequential ;
coherence

proof end;

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₃ -> jump-only non sequential ;
coherence

proof end;

end;

registration

let c₁ be good Ring;
let c₂ be Instruction-Location of (SCM c₁);
cluster goto a₂ -> jump-only non sequential non ins-loc-free ;
coherence

proof end;

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₃ -> jump-only non sequential non ins-loc-free ;
coherence

proof end;

end;

registration

let c₁ be good Ring;
cluster SCM a₁ -> standard homogeneous with_explicit_jumps without_implicit_jumps ;
coherence

proof end;

end;

registration

let c₁ be good Ring;
cluster SCM a₁ -> standard homogeneous with_explicit_jumps without_implicit_jumps regular ;
coherence

proof end;

end;

theorem Th69: :: SCMRING3:69

for b₁ being good Ring
for b₂ being Instruction-Location of (SCM b₁)
for b₃ being natural number holds IncAddr (goto b₂),b₃ = goto (il. (SCM b₁),((locnum b₂) + b₃))

proof end;

theorem Th70: :: SCMRING3:70

for b₁ being good Ring
for b₂ being Data-Location of b₁
for b₃ being Instruction-Location of (SCM b₁)
for b₄ being natural number holds IncAddr (b₂ =0_goto b₃),b₄ = b₂ =0_goto (il. (SCM b₁),((locnum b₃) + b₄))

proof end;

registration

let c₁ be good Ring;
cluster SCM a₁ -> standard homogeneous with_explicit_jumps without_implicit_jumps regular IC-good Exec-preserving ;
coherence

proof end;

end;