:: SCMRING4 semantic presentation

Lm1: for a, A being set st A /\ {a} <> {} holds
a in A

proof end;

Lm2: for a, b, c being set holds not c in a \ ({c} \/ b)

proof end;

theorem Th1: :: SCMRING4:1

for N being with_non-empty_elements set
for S being non empty non void IC-Ins-separated definite standard AMI-Struct of N holds NAT ,the Instruction-Locations of S are_equipotent

proof end;

registration

let N be with_non-empty_elements set ;
let S be non empty non void IC-Ins-separated definite standard AMI-Struct of N;
cluster the Instruction-Locations of S -> infinite ;
coherence

proof end;

end;

theorem Th2: :: SCMRING4:2

for i, j being natural number
for N being with_non-empty_elements set
for S being non empty non void IC-Ins-separated definite standard AMI-Struct of N holds (il. S,i) + j = il. S,(i + j)

proof end;

definition

let N be with_non-empty_elements set ;
let S be non empty non void IC-Ins-separated definite standard AMI-Struct of N;
let loc be Instruction-Location of S;
let k be natural number ;
func loc -' k -> Instruction-Location of S equals :: SCMRING4:def 1
il. S,((locnum loc) -' k);
coherence ;

end;

:: deftheorem defines -' SCMRING4:def 1 :

theorem :: SCMRING4:3

for N being with_non-empty_elements set
for S being non empty non void IC-Ins-separated definite standard AMI-Struct of N
for l being Instruction-Location of S holds l -' 0 = l

proof end;

theorem :: SCMRING4:4

for k being natural number
for N being with_non-empty_elements set
for S being non empty non void IC-Ins-separated definite standard AMI-Struct of N
for l being Instruction-Location of S holds (locnum l) -' k = locnum (l -' k) by AMISTD_1:def 13;

theorem Th5: :: SCMRING4:5

proof end;

theorem :: SCMRING4:6

for i, j being natural number
for N being with_non-empty_elements set
for S being non empty non void IC-Ins-separated definite standard AMI-Struct of N holds (il. S,i) -' j = il. S,(i -' j) by AMISTD_1:def 13;

theorem Th7: :: SCMRING4:7

for N being with_non-empty_elements set
for S being non empty non void IC-Ins-separated definite AMI-Struct of N
for p being FinPartState of S holds dom (DataPart p) c= the carrier of S \ ({(IC S)} \/ the Instruction-Locations of S)

proof end;

Lm3: now

let N be with_non-empty_elements set ; :: thesis:
let S be non empty AMI-Struct of N; :: thesis:
set C = the carrier of S;
set I = the Instruction-Locations of S;
set B = the carrier of S \ ({(IC S)} \/ the Instruction-Locations of S);
thus the Instruction-Locations of S misses the carrier of S \ ({(IC S)} \/ the Instruction-Locations of S) :: thesis:

proof

assume the Instruction-Locations of S meets the carrier of S \ ({(IC S)} \/ the Instruction-Locations of S) ; :: thesis:
then consider o being set such that
A1: o in the Instruction-Locations of S and
A2: o in the carrier of S \ ({(IC S)} \/ the Instruction-Locations of S) by XBOOLE_0:3;
not o in {(IC S)} \/ the Instruction-Locations of S by A2, XBOOLE_0:def 4;
hence contradiction by A1, XBOOLE_0:def 2; :: thesis:

end;

Lm4: for a, b, c being set st a c= c & b c= c \ a holds
c = (a \/ (c \ (a \/ b))) \/ b

proof end;

Lm5: for N being with_non-empty_elements set
for S being non empty non void IC-Ins-separated definite realistic AMI-Struct of N holds the Instruction-Locations of S c= the carrier of S \ {(IC S)}

proof end;

theorem Th8: :: SCMRING4:8

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 p being FinPartState of S holds
( p is data-only iff dom p c= the carrier of S \ ({(IC S)} \/ the Instruction-Locations of S) )

proof end;

theorem Th9: :: SCMRING4:9

for k being natural number
for N being with_non-empty_elements set
for S being non empty non void IC-Ins-separated definite standard AMI-Struct of N
for l1, l2 being Instruction-Location of S holds
( Start-At (l1 + k) = Start-At (l2 + k) iff Start-At l1 = Start-At l2 )

proof end;

theorem Th10: :: SCMRING4:10

for k being natural number
for N being with_non-empty_elements set
for S being non empty non void IC-Ins-separated definite standard AMI-Struct of N
for l1, l2 being Instruction-Location of S st Start-At l1 = Start-At l2 holds
Start-At (l1 -' k) = Start-At (l2 -' k)

proof end;

theorem Th11: :: SCMRING4:11

for k being natural number
for N being with_non-empty_elements set
for S being non empty non void IC-Ins-separated definite standard AMI-Struct of N
for l being Instruction-Location of S
for f being FinPartState of S st l in dom f holds
(Shift f,k) . (l + k) = f . l

proof end;

theorem :: SCMRING4:12

for k being natural number
for N being with_non-empty_elements set
for S being non empty non void IC-Ins-separated definite standard AMI-Struct of N
for f being FinPartState of S holds dom (Shift f,k) = { (il + k) where il is Instruction-Location of S : il in dom f }

proof end;

theorem Th13: :: SCMRING4:13

for N being with_non-empty_elements set
for S being non empty non void IC-Ins-separated steady-programmed definite realistic Exec-preserving AMI-Struct of N
for s being State of S
for i being Instruction of S
for p being programmed FinPartState of S holds Exec i,(s +* p) = (Exec i,s) +* p

proof end;

theorem Th14: :: SCMRING4:14

for R being good Ring holds the carrier of (SCM R) = ({(IC (SCM R))} \/ SCM-Data-Loc ) \/ SCM-Instr-Loc

proof end;

theorem :: SCMRING4:15

for R being good Ring
for loc being Instruction-Location of (SCM R) holds ObjectKind loc = SCM-Instr R

proof end;

theorem Th16: :: SCMRING4:16

for n being Nat
for R being good Ring holds dl. R,n = (2 * n) + 1

proof end;

theorem :: SCMRING4:17

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

proof end;

theorem :: SCMRING4:18

for R being good Ring
for dl being Data-Location of R ex i being Nat st dl = dl. R,i

proof end;

theorem :: SCMRING4:19

for R being good Ring
for i, j being Nat st i <> j holds
dl. R,i <> dl. R,j

proof end;

theorem Th20: :: SCMRING4:20

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

proof end;

Lm6: now

let R be good Ring; :: thesis:
thus the carrier of SCM = ({(IC (SCM R))} \/ SCM-Data-Loc ) \/ SCM-Instr-Loc by AMI_3:4, AMI_5:23, SCMRING2:9
.= the carrier of (SCM R) by Th14 ; :: thesis:

end;

Lm7: now

let a be State of SCM ; :: thesis:
let R be good Ring; :: thesis:
let s be State of (SCM R); :: thesis:
thus dom a = the carrier of SCM by AMI_3:36
.= the carrier of (SCM R) by Lm6
.= dom s by AMI_3:36 ; :: thesis:

end;

theorem Th21: :: SCMRING4:21

for R being good Ring
for s being State of (SCM R) holds SCM-Data-Loc c= dom s

proof end;

theorem Th22: :: SCMRING4:22

for R being good Ring
for s being State of (SCM R) holds dom (s | SCM-Data-Loc ) = SCM-Data-Loc

proof end;

theorem :: SCMRING4:23

for R being good Ring
for p being FinPartState of SCM R
for q being FinPartState of SCM st p = q holds
DataPart p = DataPart q

proof end;

theorem Th24: :: SCMRING4:24

for R being good Ring
for p being FinPartState of SCM R holds DataPart p = p | SCM-Data-Loc

proof end;

theorem :: SCMRING4:25

for R being good Ring
for p being FinPartState of SCM R holds
( p is data-only iff dom p c= SCM-Data-Loc )

proof end;

theorem Th26: :: SCMRING4:26

for R being good Ring
for p being FinPartState of SCM R holds dom (DataPart p) c= SCM-Data-Loc

proof end;

theorem :: SCMRING4:27

for R being good Ring
for s being State of (SCM R) holds SCM-Instr-Loc c= dom s

proof end;

theorem :: SCMRING4:28

for R being good Ring
for p being FinPartState of SCM R
for q being FinPartState of SCM st p = q holds
ProgramPart p = ProgramPart q

proof end;

theorem Th29: :: SCMRING4:29

for R being good Ring
for p being FinPartState of SCM R holds dom (ProgramPart p) c= SCM-Instr-Loc

proof end;

registration

let R be good Ring;
let I be Element of the Instructions of (SCM R);
cluster InsCode I -> natural ;
coherence

proof end;

end;

theorem Th30: :: SCMRING4:30

for R being good Ring
for I being Instruction of (SCM R) holds InsCode I <= 7

proof end;

theorem Th31: :: SCMRING4:31

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

proof end;

theorem Th32: :: SCMRING4:32

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

proof end;

theorem Th33: :: SCMRING4:33

for R being good Ring
for a being Data-Location of R
for loc being Instruction-Location of (SCM R)
for s being State of (SCM R) holds s . a = (s +* (Start-At loc)) . a

proof end;

theorem Th34: :: SCMRING4:34

for R being good Ring
for s1, s2 being State of (SCM R) st IC s1 = IC s2 & ( for a being Data-Location of R holds s1 . a = s2 . a ) & ( for i being Instruction-Location of (SCM R) holds s1 . i = s2 . i ) holds
s1 = s2

proof end;

theorem Th35: :: SCMRING4:35

for k being natural number
for R being good Ring
for s being State of (SCM R) holds Exec (IncAddr (CurInstr s),k),(s +* (Start-At ((IC s) + k))) = (Following s) +* (Start-At ((IC (Following s)) + k))

proof end;

theorem Th36: :: SCMRING4:36

for j, k being natural number
for R being good Ring
for I being Instruction of (SCM R)
for s being State of (SCM R) st IC s = il. (SCM R),(j + k) holds
Exec I,(s +* (Start-At ((IC s) -' k))) = (Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k))

proof end;

registration

let R be good Ring;
cluster autonomic non programmed FinPartState of SCM R;
existence

proof end;

end;

definition

let R be good Ring;
let a be Data-Location of R;
let r be Element of R;
:: original: .-->
redefine func a .--> r -> FinPartState of SCM R;
coherence

proof end;

end;

theorem Th37: :: SCMRING4:37

for R being good Ring st not R is trivial holds
for p being autonomic FinPartState of SCM R st DataPart p <> {} holds
IC (SCM R) in dom p

proof end;

theorem Th38: :: SCMRING4:38

for R being good Ring st not R is trivial holds
for p being autonomic non programmed FinPartState of SCM R holds IC (SCM R) in dom p

proof end;

theorem :: SCMRING4:39

for R being good Ring
for p being autonomic FinPartState of SCM R st IC (SCM R) in dom p holds
IC p in dom p

proof end;

theorem Th40: :: SCMRING4:40

for n being Nat
for R being good Ring
for s being State of (SCM R) st not R is trivial holds
for p being autonomic non programmed FinPartState of SCM R st p c= s holds
IC ((Computation s) . n) in dom (ProgramPart p)

proof end;

theorem Th41: :: SCMRING4:41

for n being Nat
for R being good Ring
for s1, s2 being State of (SCM R) st not R is trivial holds
for p being autonomic non programmed FinPartState of SCM R st p c= s1 & p c= s2 holds
( IC ((Computation s1) . n) = IC ((Computation s2) . n) & CurInstr ((Computation s1) . n) = CurInstr ((Computation s2) . n) )

proof end;

theorem Th42: :: SCMRING4:42

for n being Nat
for R being good Ring
for a, b being Data-Location of R
for s1, s2 being State of (SCM R) st not R is trivial holds
for p being autonomic non programmed FinPartState of SCM R st p c= s1 & p c= s2 & CurInstr ((Computation s1) . n) = a := b & a in dom p holds
((Computation s1) . n) . b = ((Computation s2) . n) . b

proof end;

theorem Th43: :: SCMRING4:43

for n being Nat
for R being good Ring
for a, b being Data-Location of R
for s1, s2 being State of (SCM R) st not R is trivial holds
for p being autonomic non programmed FinPartState of SCM R st p c= s1 & p c= s2 & CurInstr ((Computation s1) . n) = AddTo a,b & a in dom p holds
(((Computation s1) . n) . a) + (((Computation s1) . n) . b) = (((Computation s2) . n) . a) + (((Computation s2) . n) . b)

proof end;

theorem Th44: :: SCMRING4:44

for n being Nat
for R being good Ring
for a, b being Data-Location of R
for s1, s2 being State of (SCM R) st not R is trivial holds
for p being autonomic non programmed FinPartState of SCM R st p c= s1 & p c= s2 & CurInstr ((Computation s1) . n) = SubFrom a,b & a in dom p holds
(((Computation s1) . n) . a) - (((Computation s1) . n) . b) = (((Computation s2) . n) . a) - (((Computation s2) . n) . b)

proof end;

theorem Th45: :: SCMRING4:45

for n being Nat
for R being good Ring
for a, b being Data-Location of R
for s1, s2 being State of (SCM R) st not R is trivial holds
for p being autonomic non programmed FinPartState of SCM R st p c= s1 & p c= s2 & CurInstr ((Computation s1) . n) = MultBy a,b & a in dom p holds
(((Computation s1) . n) . a) * (((Computation s1) . n) . b) = (((Computation s2) . n) . a) * (((Computation s2) . n) . b)

proof end;

theorem Th46: :: SCMRING4:46

for n being Nat
for R being good Ring
for a being Data-Location of R
for loc being Instruction-Location of (SCM R)
for s1, s2 being State of (SCM R) st not R is trivial holds
for p being autonomic non programmed FinPartState of SCM R st p c= s1 & p c= s2 & CurInstr ((Computation s1) . n) = a =0_goto loc & loc <> Next (IC ((Computation s1) . n)) holds
( ((Computation s1) . n) . a = 0. R iff ((Computation s2) . n) . a = 0. R )

proof end;

definition

let N be with_non-empty_elements set ;
let S be non empty non void IC-Ins-separated definite standard regular AMI-Struct of N;
let k be natural number ;
let p be FinPartState of S;
func Relocated p,k -> FinPartState of S equals :: SCMRING4:def 2
((Start-At ((IC p) + k)) +* (IncAddr (Shift (ProgramPart p),k),k)) +* (DataPart p);
coherence ;

end;

:: deftheorem defines Relocated SCMRING4:def 2 :

theorem Th47: :: SCMRING4:47

proof end;

theorem Th48: :: SCMRING4:48

for k being natural number
for N being with_non-empty_elements set
for S being non empty non void IC-Ins-separated definite standard regular AMI-Struct of N
for g being FinPartState of S st S is realistic holds
ProgramPart (Relocated g,k) = IncAddr (Shift (ProgramPart g),k),k

proof end;

theorem Th49: :: SCMRING4:49

for k being natural number
for N being with_non-empty_elements set
for S being non empty non void IC-Ins-separated definite standard regular AMI-Struct of N
for g being FinPartState of S st S is realistic holds
dom (ProgramPart (Relocated g,k)) = { (il. S,(j + k)) where j is Nat : il. S,j in dom (ProgramPart g) }

proof end;

theorem Th50: :: SCMRING4:50

for k being natural number
for N being with_non-empty_elements set
for S being non empty non void IC-Ins-separated definite standard regular AMI-Struct of N
for g being FinPartState of S
for il being Instruction-Location of S st S is realistic holds
( il in dom g iff il + k in dom (Relocated g,k) )

proof end;

theorem Th51: :: SCMRING4:51

proof end;

theorem Th52: :: SCMRING4:52

proof end;

theorem Th53: :: SCMRING4:53

for k being natural number
for N being with_non-empty_elements set
for S being non empty non void IC-Ins-separated definite standard regular AMI-Struct of N
for p being programmed FinPartState of S
for l being Instruction-Location of S st l in dom p holds
(IncAddr p,k) . l = IncAddr (pi p,l),k

proof end;

theorem Th54: :: SCMRING4:54

for i being natural number
for N being with_non-empty_elements set
for S being non empty non void IC-Ins-separated definite standard regular AMI-Struct of N
for p being programmed FinPartState of S holds Shift (IncAddr p,i),i = IncAddr (Shift p,i),i

proof end;

theorem Th55: :: SCMRING4:55

for k being natural number
for N being with_non-empty_elements set
for S being non empty non void IC-Ins-separated definite standard regular AMI-Struct of N
for g being FinPartState of S
for il being Instruction-Location of S st S is realistic holds
for I being Instruction of S st il in dom (ProgramPart g) & I = g . il holds
IncAddr I,k = (Relocated g,k) . (il + k)

proof end;

theorem Th56: :: SCMRING4:56

proof end;

theorem Th57: :: SCMRING4:57

for k being natural number
for N being with_non-empty_elements set
for S being non empty non void IC-Ins-separated definite standard regular AMI-Struct of N
for g being FinPartState of S st S is realistic holds
for q being data-only FinPartState of S st IC S in dom g holds
Relocated (g +* q),k = (Relocated g,k) +* q

proof end;

theorem Th58: :: SCMRING4:58

for k being natural number
for R being good Ring
for s1, s2 being State of (SCM R)
for p being autonomic FinPartState of SCM R st p c= s1 & Relocated p,k c= s2 holds
p c= s1 +* (s2 | SCM-Data-Loc )

proof end;

theorem Th59: :: SCMRING4:59

for k being natural number
for R being good Ring
for s1, s2, s being State of (SCM R) st not R is trivial holds
for p being autonomic FinPartState of SCM R st IC (SCM R) in dom p & p c= s1 & Relocated p,k c= s2 & s = s1 +* (s2 | SCM-Data-Loc ) holds
for i being Nat holds
( (IC ((Computation s1) . i)) + k = IC ((Computation s2) . i) & IncAddr (CurInstr ((Computation s1) . i)),k = CurInstr ((Computation s2) . i) & ((Computation s1) . i) | (dom (DataPart p)) = ((Computation s2) . i) | (dom (DataPart (Relocated p,k))) & ((Computation s) . i) | SCM-Data-Loc = ((Computation s2) . i) | SCM-Data-Loc )

proof end;

theorem Th60: :: SCMRING4:60

for k being natural number
for R being good Ring st not R is trivial holds
for p being autonomic FinPartState of SCM R st IC (SCM R) in dom p holds
( p is halting iff Relocated p,k is halting )

proof end;

theorem :: SCMRING4:61

for k being natural number
for R being good Ring
for s being State of (SCM R) st not R is trivial holds
for p being autonomic FinPartState of SCM R st IC (SCM R) in dom p & p c= s holds
for i being Nat holds (Computation (s +* (Relocated p,k))) . i = (((Computation s) . i) +* (Start-At ((IC ((Computation s) . i)) + k))) +* (ProgramPart (Relocated p,k))

proof end;

theorem Th62: :: SCMRING4:62

for k being natural number
for R being good Ring
for s being State of (SCM R) st not R is trivial holds
for p being autonomic FinPartState of SCM R st IC (SCM R) in dom p & Relocated p,k c= s holds
for i being Nat holds (Computation s) . i = ((((Computation (s +* p)) . i) +* (Start-At ((IC ((Computation (s +* p)) . i)) + k))) +* (s | (dom (ProgramPart p)))) +* (ProgramPart (Relocated p,k))

proof end;

theorem Th63: :: SCMRING4:63

for k being natural number
for R being good Ring
for p being FinPartState of SCM R
for s being State of (SCM R) st not R is trivial & IC (SCM R) in dom p & p c= s & Relocated p,k is autonomic holds
for i being Nat holds (Computation s) . i = ((((Computation (s +* (Relocated p,k))) . i) +* (Start-At ((IC ((Computation (s +* (Relocated p,k))) . i)) -' k))) +* (s | (dom (ProgramPart (Relocated p,k))))) +* (ProgramPart p)

proof end;

theorem Th64: :: SCMRING4:64

for k being natural number
for R being good Ring
for p being FinPartState of SCM R st not R is trivial & IC (SCM R) in dom p holds
( p is autonomic iff Relocated p,k is autonomic )

proof end;

theorem Th65: :: SCMRING4:65

for k being natural number
for R being good Ring st not R is trivial holds
for p being autonomic halting FinPartState of SCM R st IC (SCM R) in dom p holds
DataPart (Result p) = DataPart (Result (Relocated p,k))

proof end;

theorem :: SCMRING4:66

for k being natural number
for R being good Ring
for p being FinPartState of SCM R st not R is trivial holds
for F being PartFunc of FinPartSt (SCM R), FinPartSt (SCM R) st IC (SCM R) in dom p & F is data-only holds
( p computes F iff Relocated p,k computes F )

proof end;