:: 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 R being good Ring
for a being Data-Location of R holds ObjectKind a = the carrier of R

proof end;

definition

let R be good Ring;
let la, lb be Data-Location of R;
let a, b be Element of R;
:: original: -->
redefine func la,lb --> a,b -> FinPartState of SCM R;
coherence

proof end;

end;

theorem Th2: :: SCMRING3:2

for R being good Ring
for a being Data-Location of R holds not a in the Instruction-Locations of (SCM R)

proof end;

theorem Th3: :: SCMRING3:3

for R being good Ring
for a being Data-Location of R holds a <> IC (SCM R)

proof end;

theorem Th4: :: SCMRING3:4

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

proof end;

theorem Th5: :: SCMRING3:5

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

proof end;

theorem Th6: :: SCMRING3:6

for R being good Ring
for i1, i2 being Instruction-Location of (SCM R) st i1 <> i2 holds
Next i1 <> Next i2

proof end;

theorem Th7: :: SCMRING3:7

for R being good Ring
for a being Data-Location of R
for s1, s2 being State of (SCM R) st s1,s2 equal_outside the Instruction-Locations of (SCM R) holds
s1 . a = s2 . a

proof end;

theorem Th8: :: SCMRING3:8

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

proof end;

theorem Th9: :: SCMRING3:9

for R being good Ring
for a, b being Data-Location of R holds InsCode (a := b) = 1

proof end;

theorem Th10: :: SCMRING3:10

for R being good Ring
for a, b being Data-Location of R holds InsCode (AddTo a,b) = 2

proof end;

theorem Th11: :: SCMRING3:11

for R being good Ring
for a, b being Data-Location of R holds InsCode (SubFrom a,b) = 3

proof end;

theorem Th12: :: SCMRING3:12

for R being good Ring
for a, b being Data-Location of R holds InsCode (MultBy a,b) = 4

proof end;

theorem Th13: :: SCMRING3:13

for R being good Ring
for r being Element of R
for a being Data-Location of R holds InsCode (a := r) = 5

proof end;

theorem Th14: :: SCMRING3:14

for R being good Ring
for i1 being Instruction-Location of (SCM R) holds InsCode (goto i1) = 6

proof end;

theorem Th15: :: SCMRING3:15

for R being good Ring
for a being Data-Location of R
for i1 being Instruction-Location of (SCM R) holds InsCode (a =0_goto i1) = 7

proof end;

theorem Th16: :: SCMRING3:16

for R being good Ring
for I being Instruction of (SCM R) st InsCode I = 0 holds
I = halt (SCM R)

proof end;

theorem Th17: :: SCMRING3:17

for R being good Ring
for I being Instruction of (SCM R) st InsCode I = 1 holds
ex a, b being Data-Location of R st I = a := b

proof end;

theorem Th18: :: SCMRING3:18

for R being good Ring
for I being Instruction of (SCM R) st InsCode I = 2 holds
ex a, b being Data-Location of R st I = AddTo a,b

proof end;

theorem Th19: :: SCMRING3:19

for R being good Ring
for I being Instruction of (SCM R) st InsCode I = 3 holds
ex a, b being Data-Location of R st I = SubFrom a,b

proof end;

theorem Th20: :: SCMRING3:20

for R being good Ring
for I being Instruction of (SCM R) st InsCode I = 4 holds
ex a, b being Data-Location of R st I = MultBy a,b

proof end;

theorem Th21: :: SCMRING3:21

for R being good Ring
for I being Instruction of (SCM R) st InsCode I = 5 holds
ex a being Data-Location of R ex r being Element of R st I = a := r

proof end;

theorem Th22: :: SCMRING3:22

for R being good Ring
for I being Instruction of (SCM R) st InsCode I = 6 holds
ex i2 being Instruction-Location of (SCM R) st I = goto i2

proof end;

theorem Th23: :: SCMRING3:23

for R being good Ring
for I being Instruction of (SCM R) st InsCode I = 7 holds
ex a being Data-Location of R ex i1 being Instruction-Location of (SCM R) st I = a =0_goto i1

proof end;

Lm1: for x, y being set st x in dom <*y*> holds
x = 1

proof end;

Lm2: for x, y, z being set holds
( not x in dom <*y,z*> or x = 1 or x = 2 )

proof end;

Lm3: for R being good Ring
for T being InsType of (SCM R) holds
( T = 0 or T = 1 or T = 2 or T = 3 or T = 4 or T = 5 or T = 6 or T = 7 )

proof end;

theorem Th24: :: SCMRING3:24

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

proof end;

theorem Th25: :: SCMRING3:25

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

theorem Th26: :: SCMRING3:26

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

theorem Th27: :: SCMRING3:27

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

theorem Th28: :: SCMRING3:28

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

theorem Th29: :: SCMRING3:29

for R being good Ring
for r being Element of R
for a being Data-Location of R holds AddressPart (a := r) = <*a,r*> by MCART_1:def 2;

theorem Th30: :: SCMRING3:30

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

theorem Th31: :: SCMRING3:31

for R being good Ring
for a being Data-Location of R
for i1 being Instruction-Location of (SCM R) holds AddressPart (a =0_goto i1) = <*i1,a*> by MCART_1:def 2;

theorem Th32: :: SCMRING3:32

for R being good Ring
for T being InsType of (SCM R) st T = 0 holds
AddressParts T = {0}

proof end;

registration

let R be good Ring;
let T be InsType of (SCM R);
cluster AddressParts T -> non empty ;
coherence

proof end;

end;

theorem Th33: :: SCMRING3:33

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

proof end;

theorem Th34: :: SCMRING3:34

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

proof end;

theorem Th35: :: SCMRING3:35

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

proof end;

theorem Th36: :: SCMRING3:36

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

proof end;

theorem Th37: :: SCMRING3:37

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

proof end;

theorem Th38: :: SCMRING3:38

for R being good Ring
for T being InsType of (SCM R) st T = 6 holds
dom (PA (AddressParts T)) = {1}

proof end;

theorem Th39: :: SCMRING3:39

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

proof end;

theorem Th40: :: SCMRING3:40

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

proof end;

theorem Th41: :: SCMRING3:41

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

proof end;

theorem Th42: :: SCMRING3:42

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

proof end;

theorem Th43: :: SCMRING3:43

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

proof end;

theorem Th44: :: SCMRING3:44

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

proof end;

theorem Th45: :: SCMRING3:45

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

proof end;

theorem Th46: :: SCMRING3:46

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

proof end;

theorem Th47: :: SCMRING3:47

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

proof end;

theorem Th48: :: SCMRING3:48

for R being good Ring
for r being Element of R
for a being Data-Location of R holds (PA (AddressParts (InsCode (a := r)))) . 1 = SCM-Data-Loc

proof end;

theorem Th49: :: SCMRING3:49

for R being good Ring
for r being Element of R
for a being Data-Location of R holds (PA (AddressParts (InsCode (a := r)))) . 2 = the carrier of R

proof end;

theorem Th50: :: SCMRING3:50

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

proof end;

theorem Th51: :: SCMRING3:51

for R being good Ring
for a being Data-Location of R
for i1 being Instruction-Location of (SCM R) holds (PA (AddressParts (InsCode (a =0_goto i1)))) . 1 = the Instruction-Locations of (SCM R)

proof end;

theorem Th52: :: SCMRING3:52

for R being good Ring
for a being Data-Location of R
for i1 being Instruction-Location of (SCM R) holds (PA (AddressParts (InsCode (a =0_goto i1)))) . 2 = SCM-Data-Loc

proof end;

Lm4: for N being with_non-empty_elements set
for S being non empty non void IC-Ins-separated definite realistic AMI-Struct of N
for t, u being State of S
for il being Instruction-Location of S
for e being Element of ObjectKind (IC S)
for I being Element of ObjectKind il st e = il & u = t +* ((IC S),il --> e,I) holds
( u . il = I & IC u = il & IC (Following u) = (Exec (u . (IC u)),u) . (IC S) )

proof end;

Lm5: for R being good Ring
for l being Instruction-Location of (SCM R)
for i being Instruction of (SCM R) st ( for s being State of (SCM R) st IC s = l & s . l = i holds
(Exec i,s) . (IC (SCM R)) = Next (IC s) ) holds
NIC i,l = {(Next l)}

proof end;

Lm6: for R being good Ring
for i being Instruction of (SCM R) st ( for l being Instruction-Location of (SCM R) holds NIC i,l = {(Next l)} ) holds
JUMP i is empty

proof end;

theorem Th53: :: SCMRING3:53

for R being good Ring
for il being Instruction-Location of (SCM R) holds NIC (halt (SCM R)),il = {il}

proof end;

registration

let R be good Ring;
cluster JUMP (halt (SCM R)) -> empty ;
coherence

proof end;

end;

theorem Th54: :: SCMRING3:54

for R being good Ring
for a, b being Data-Location of R
for il being Instruction-Location of (SCM R) holds NIC (a := b),il = {(Next il)}

proof end;

registration

let R be good Ring;
let a, b be Data-Location of R;
cluster JUMP (a := b) -> empty ;
coherence

proof end;

end;

theorem Th55: :: SCMRING3:55

for R being good Ring
for a, b being Data-Location of R
for il being Instruction-Location of (SCM R) holds NIC (AddTo a,b),il = {(Next il)}

proof end;

registration

let R be good Ring;
let a, b be Data-Location of R;
cluster JUMP (AddTo a,b) -> empty ;
coherence

proof end;

end;

theorem Th56: :: SCMRING3:56

for R being good Ring
for a, b being Data-Location of R
for il being Instruction-Location of (SCM R) holds NIC (SubFrom a,b),il = {(Next il)}

proof end;

registration

let R be good Ring;
let a, b be Data-Location of R;
cluster JUMP (SubFrom a,b) -> empty ;
coherence

proof end;

end;

theorem Th57: :: SCMRING3:57

for R being good Ring
for a, b being Data-Location of R
for il being Instruction-Location of (SCM R) holds NIC (MultBy a,b),il = {(Next il)}

proof end;

registration

let R be good Ring;
let a, b be Data-Location of R;
cluster JUMP (MultBy a,b) -> empty ;
coherence

proof end;

end;

theorem Th58: :: SCMRING3:58

for R being good Ring
for r being Element of R
for a being Data-Location of R
for il being Instruction-Location of (SCM R) holds NIC (a := r),il = {(Next il)}

proof end;

registration

let R be good Ring;
let a be Data-Location of R;
let r be Element of R;
cluster JUMP (a := r) -> empty ;
coherence

proof end;

end;

theorem Th59: :: SCMRING3:59

for R being good Ring
for i1, il being Instruction-Location of (SCM R) holds NIC (goto i1),il = {i1}

proof end;

theorem Th60: :: SCMRING3:60

for R being good Ring
for i1 being Instruction-Location of (SCM R) holds JUMP (goto i1) = {i1}

proof end;

registration

let R be good Ring;
let i1 be Instruction-Location of (SCM R);
cluster JUMP (goto i1) -> non empty trivial ;
coherence

proof end;

end;

theorem Th61: :: SCMRING3:61

for R being good Ring
for a being Data-Location of R
for i1, il being Instruction-Location of (SCM R) holds
( i1 in NIC (a =0_goto i1),il & NIC (a =0_goto i1),il c= {i1,(Next il)} )

proof end;

theorem :: SCMRING3:62

for R being good non trivial Ring
for a being Data-Location of R
for il, i1 being Instruction-Location of (SCM R) holds NIC (a =0_goto i1),il = {i1,(Next il)}

proof end;

theorem Th63: :: SCMRING3:63

for R being good Ring
for a being Data-Location of R
for i1 being Instruction-Location of (SCM R) holds JUMP (a =0_goto i1) = {i1}

proof end;

registration

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

proof end;

end;

theorem Th64: :: SCMRING3:64

for R being good Ring
for il being Instruction-Location of (SCM R) holds SUCC il = {il,(Next il)}

proof end;

theorem Th65: :: SCMRING3:65

for R being good Ring
for f being Function of NAT ,the Instruction-Locations of (SCM R) st ( for k being Nat holds f . k = il. k ) holds
( f is bijective & ( for k being Nat holds
( f . (k + 1) in SUCC (f . k) & ( for j being Nat st f . j in SUCC (f . k) holds
k <= j ) ) ) )

proof end;

registration

let R be good Ring;
cluster SCM R -> standard ;
coherence

proof end;

end;

theorem Th66: :: SCMRING3:66

for R being good Ring
for k being natural number holds il. (SCM R),k = il. k

proof end;

theorem Th67: :: SCMRING3:67

for R being good Ring
for k being natural number holds Next (il. (SCM R),k) = il. (SCM R),(k + 1)

proof end;

theorem Th68: :: SCMRING3:68

for R being good Ring
for il being Instruction-Location of (SCM R) holds Next il = NextLoc il

proof end;

definition

let R be good Ring;
let k be Nat;
func dl. R,k -> Data-Location of R equals :: SCMRING3:def 1
dl. k;
coherence

proof end;

end;

:: deftheorem defines dl. SCMRING3:def 1 :

registration

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

proof end;

end;

registration

let R be good Ring;
cluster halt (SCM R) -> jump-only ;
coherence

proof end;

end;

registration

let R be good Ring;
let i1 be Instruction-Location of (SCM R);
cluster InsCode (goto i1) -> jump-only ;
coherence

proof end;

end;

registration

let R be good Ring;
let i1 be Instruction-Location of (SCM R);
cluster goto i1 -> jump-only ;
coherence

proof end;

end;

registration

let R be good Ring;
let a be Data-Location of R;
let i1 be Instruction-Location of (SCM R);
cluster InsCode (a =0_goto i1) -> jump-only ;
coherence

proof end;

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

proof end;

end;

registration

let S be good non trivial Ring;
let p, q be Data-Location of S;
cluster InsCode (p := q) -> non jump-only ;
coherence

proof end;

end;

registration

let S be good non trivial Ring;
let p, q be Data-Location of S;
cluster p := q -> non jump-only ;
coherence

proof end;

end;

registration

let S be good non trivial Ring;
let p, q be Data-Location of S;
cluster InsCode (AddTo p,q) -> non jump-only ;
coherence

proof end;

end;

registration

let S be good non trivial Ring;
let p, q be Data-Location of S;
cluster AddTo p,q -> non jump-only ;
coherence

proof end;

end;

registration

let S be good non trivial Ring;
let p, q be Data-Location of S;
cluster InsCode (SubFrom p,q) -> non jump-only ;
coherence

proof end;

end;

registration

let S be good non trivial Ring;
let p, q be Data-Location of S;
cluster SubFrom p,q -> non jump-only ;
coherence

proof end;

end;

registration

let S be good non trivial Ring;
let p, q be Data-Location of S;
cluster InsCode (MultBy p,q) -> non jump-only ;
coherence

proof end;

end;

registration

let S be good non trivial Ring;
let p, q be Data-Location of S;
cluster MultBy p,q -> non jump-only ;
coherence

proof end;

end;

registration

let S be good non trivial Ring;
let p be Data-Location of S;
let w be Element of S;
cluster InsCode (p := w) -> non jump-only ;
coherence

proof end;

end;

registration

let S be good non trivial Ring;
let p be Data-Location of S;
let w be Element of S;
cluster p := w -> non jump-only ;
coherence

proof end;

end;

registration

let R be good Ring;
let a, b be Data-Location of R;
cluster a := b -> sequential ;
coherence

proof end;

end;

registration

let R be good Ring;
let a, b be Data-Location of R;
cluster AddTo a,b -> sequential ;
coherence

proof end;

end;

registration

let R be good Ring;
let a, b be Data-Location of R;
cluster SubFrom a,b -> sequential ;
coherence

proof end;

end;

registration

let R be good Ring;
let a, b be Data-Location of R;
cluster MultBy a,b -> sequential ;
coherence

proof end;

end;

registration

let R be good Ring;
let a be Data-Location of R;
let r be Element of R;
cluster a := r -> sequential ;
coherence

proof end;

end;

registration

let R be good Ring;
let i1 be Instruction-Location of (SCM R);
cluster goto i1 -> jump-only non sequential ;
coherence

proof end;

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

proof end;

end;

registration

let R be good Ring;
let i1 be Instruction-Location of (SCM R);
cluster goto i1 -> jump-only non sequential non ins-loc-free ;
coherence

proof end;

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

proof end;

end;

registration

let R be good Ring;
cluster SCM R -> standard homogeneous with_explicit_jumps without_implicit_jumps ;
coherence

proof end;

end;

registration

let R be good Ring;
cluster SCM R -> standard homogeneous with_explicit_jumps without_implicit_jumps regular ;
coherence

proof end;

end;

theorem Th69: :: SCMRING3:69

for R being good Ring
for i1 being Instruction-Location of (SCM R)
for k being natural number holds IncAddr (goto i1),k = goto (il. (SCM R),((locnum i1) + k))

proof end;

theorem Th70: :: SCMRING3:70

for R being good Ring
for a being Data-Location of R
for i1 being Instruction-Location of (SCM R)
for k being natural number holds IncAddr (a =0_goto i1),k = a =0_goto (il. (SCM R),((locnum i1) + k))

proof end;

registration

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

proof end;

end;