:: SCMRING4 semantic presentation

Lemma1: for b₁, b₂ being set st b₂ /\ {b₁} <> {} holds
b₁ in b₂

proof end;

Lemma2: for b₁, b₂, b₃ being set holds not b₃ in b₁ \ ({b₃} \/ b₂)

proof end;

theorem Th1: :: SCMRING4:1

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

proof end;

registration

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

proof end;

end;

theorem Th2: :: SCMRING4:2

for b₁, b₂ being natural number
for b₃ being with_non-empty_elements set
for b₄ being non empty non void IC-Ins-separated definite standard AMI-Struct of b₃ holds (il. b₄,b₁) + b₂ = il. b₄,(b₁ + b₂)

proof end;

definition

let c₁ be with_non-empty_elements set ;
let c₂ be non empty non void IC-Ins-separated definite standard AMI-Struct of c₁;
let c₃ be Instruction-Location of c₂;
let c₄ be natural number ;
func c₃ -' c₄ -> Instruction-Location of a₂ equals :: SCMRING4:def 1
il. a₂,((locnum a₃) -' a₄);
coherence ;

end;

:: deftheorem Def1 defines -' SCMRING4:def 1 :

theorem Th3: :: SCMRING4:3

for b₁ being with_non-empty_elements set
for b₂ being non empty non void IC-Ins-separated definite standard AMI-Struct of b₁
for b₃ being Instruction-Location of b₂ holds b₃ -' 0 = b₃

proof end;

theorem Th4: :: SCMRING4:4

for b₁ being natural number
for b₂ being with_non-empty_elements set
for b₃ being non empty non void IC-Ins-separated definite standard AMI-Struct of b₂
for b₄ being Instruction-Location of b₃ holds (locnum b₄) -' b₁ = locnum (b₄ -' b₁) by AMISTD_1:def 13;

theorem Th5: :: SCMRING4:5

proof end;

theorem Th6: :: SCMRING4:6

for b₁, b₂ being natural number
for b₃ being with_non-empty_elements set
for b₄ being non empty non void IC-Ins-separated definite standard AMI-Struct of b₃ holds (il. b₄,b₁) -' b₂ = il. b₄,(b₁ -' b₂) by AMISTD_1:def 13;

theorem Th7: :: SCMRING4:7

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

proof end;

E7: now

let c₁ be with_non-empty_elements set ;
let c₂ be non empty AMI-Struct of c₁;
set c₃ = the carrier of c₂;
set c₄ = the Instruction-Locations of c₂;
set c₅ = the carrier of c₂ \ ({(IC c₂)} \/ the Instruction-Locations of c₂);
thus the Instruction-Locations of c₂ misses the carrier of c₂ \ ({(IC c₂)} \/ the Instruction-Locations of c₂)

proof

assume the Instruction-Locations of c₂ meets the carrier of c₂ \ ({(IC c₂)} \/ the Instruction-Locations of c₂) ;
then consider c₆ being set such that
E8: c₆ in the Instruction-Locations of c₂ and
E9: c₆ in the carrier of c₂ \ ({(IC c₂)} \/ the Instruction-Locations of c₂) by XBOOLE_0:3;
not c₆ in {(IC c₂)} \/ the Instruction-Locations of c₂ by E9, XBOOLE_0:def 4;
hence contradiction by E8, XBOOLE_0:def 2;

end;

Lemma8: for b₁, b₂, b₃ being set st b₁ c= b₃ & b₂ c= b₃ \ b₁ holds
b₃ = (b₁ \/ (b₃ \ (b₁ \/ b₂))) \/ b₂

proof end;

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

proof end;

theorem Th8: :: SCMRING4:8

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

proof end;

theorem Th9: :: SCMRING4:9

for b₁ being natural number
for b₂ being with_non-empty_elements set
for b₃ being non empty non void IC-Ins-separated definite standard AMI-Struct of b₂
for b₄, b₅ being Instruction-Location of b₃ holds
( Start-At (b₄ + b₁) = Start-At (b₅ + b₁) iff Start-At b₄ = Start-At b₅ )

proof end;

theorem Th10: :: SCMRING4:10

for b₁ being natural number
for b₂ being with_non-empty_elements set
for b₃ being non empty non void IC-Ins-separated definite standard AMI-Struct of b₂
for b₄, b₅ being Instruction-Location of b₃ st Start-At b₄ = Start-At b₅ holds
Start-At (b₄ -' b₁) = Start-At (b₅ -' b₁)

proof end;

theorem Th11: :: SCMRING4:11

for b₁ being natural number
for b₂ being with_non-empty_elements set
for b₃ being non empty non void IC-Ins-separated definite standard AMI-Struct of b₂
for b₄ being Instruction-Location of b₃
for b₅ being FinPartState of b₃ st b₄ in dom b₅ holds
(Shift b₅,b₁) . (b₄ + b₁) = b₅ . b₄

proof end;

theorem Th12: :: SCMRING4:12

for b₁ being natural number
for b₂ being with_non-empty_elements set
for b₃ being non empty non void IC-Ins-separated definite standard AMI-Struct of b₂
for b₄ being FinPartState of b₃ holds dom (Shift b₄,b₁) = { (b₅ + b₁) where B is Instruction-Location of b₃ : b₅ in dom b₄ }

proof end;

theorem Th13: :: SCMRING4:13

for b₁ being with_non-empty_elements set
for b₂ being non empty non void IC-Ins-separated steady-programmed definite realistic Exec-preserving AMI-Struct of b₁
for b₃ being State of b₂
for b₄ being Instruction of b₂
for b₅ being programmed FinPartState of b₂ holds Exec b₄,(b₃ +* b₅) = (Exec b₄,b₃) +* b₅

proof end;

theorem Th14: :: SCMRING4:14

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

proof end;

theorem Th15: :: SCMRING4:15

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

proof end;

theorem Th16: :: SCMRING4:16

for b₁ being Nat
for b₂ being good Ring holds dl. b₂,b₁ = (2 * b₁) + 1

proof end;

theorem Th17: :: SCMRING4:17

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

proof end;

theorem Th18: :: SCMRING4:18

for b₁ being good Ring
for b₂ being Data-Location of b₁ ex b₃ being Nat st b₂ = dl. b₁,b₃

proof end;

theorem Th19: :: SCMRING4:19

for b₁ being good Ring
for b₂, b₃ being Nat st b₂ <> b₃ holds
dl. b₁,b₂ <> dl. b₁,b₃

proof end;

theorem Th20: :: SCMRING4:20

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

proof end;

E18: now

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

end;

E19: now

let c₁ be State of SCM ;
let c₂ be good Ring;
let c₃ be State of (SCM c₂);
thus dom c₁ = the carrier of SCM by AMI_3:36
.= the carrier of (SCM c₂) by Lemma18
.= dom c₃ by AMI_3:36 ;

end;

theorem Th21: :: SCMRING4:21

for b₁ being good Ring
for b₂ being State of (SCM b₁) holds SCM-Data-Loc c= dom b₂

proof end;

theorem Th22: :: SCMRING4:22

for b₁ being good Ring
for b₂ being State of (SCM b₁) holds dom (b₂ | SCM-Data-Loc ) = SCM-Data-Loc

proof end;

theorem Th23: :: SCMRING4:23

for b₁ being good Ring
for b₂ being FinPartState of SCM b₁
for b₃ being FinPartState of SCM st b₂ = b₃ holds
DataPart b₂ = DataPart b₃

proof end;

theorem Th24: :: SCMRING4:24

for b₁ being good Ring
for b₂ being FinPartState of SCM b₁ holds DataPart b₂ = b₂ | SCM-Data-Loc

proof end;

theorem Th25: :: SCMRING4:25

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

proof end;

theorem Th26: :: SCMRING4:26

for b₁ being good Ring
for b₂ being FinPartState of SCM b₁ holds dom (DataPart b₂) c= SCM-Data-Loc

proof end;

theorem Th27: :: SCMRING4:27

for b₁ being good Ring
for b₂ being State of (SCM b₁) holds SCM-Instr-Loc c= dom b₂

proof end;

theorem Th28: :: SCMRING4:28

for b₁ being good Ring
for b₂ being FinPartState of SCM b₁
for b₃ being FinPartState of SCM st b₂ = b₃ holds
ProgramPart b₂ = ProgramPart b₃

proof end;

theorem Th29: :: SCMRING4:29

for b₁ being good Ring
for b₂ being FinPartState of SCM b₁ holds dom (ProgramPart b₂) c= SCM-Instr-Loc

proof end;

registration

let c₁ be good Ring;
let c₂ be Element of the Instructions of (SCM c₁);
cluster InsCode a₂ -> natural ;
coherence

proof end;

end;

theorem Th30: :: SCMRING4:30

for b₁ being good Ring
for b₂ being Instruction of (SCM b₁) holds InsCode b₂ <= 7

proof end;

theorem Th31: :: SCMRING4:31

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

proof end;

theorem Th32: :: SCMRING4:32

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

proof end;

theorem Th33: :: SCMRING4:33

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 b₄ . b₂ = (b₄ +* (Start-At b₃)) . b₂

proof end;

theorem Th34: :: SCMRING4:34

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

proof end;

theorem Th35: :: SCMRING4:35

for b₁ being natural number
for b₂ being good Ring
for b₃ being State of (SCM b₂) holds Exec (IncAddr (CurInstr b₃),b₁),(b₃ +* (Start-At ((IC b₃) + b₁))) = (Following b₃) +* (Start-At ((IC (Following b₃)) + b₁))

proof end;

theorem Th36: :: SCMRING4:36

for b₁, b₂ being natural number
for b₃ being good Ring
for b₄ being Instruction of (SCM b₃)
for b₅ being State of (SCM b₃) st IC b₅ = il. (SCM b₃),(b₁ + b₂) holds
Exec b₄,(b₅ +* (Start-At ((IC b₅) -' b₂))) = (Exec (IncAddr b₄,b₂),b₅) +* (Start-At ((IC (Exec (IncAddr b₄,b₂),b₅)) -' b₂))

proof end;

registration

let c₁ be good Ring;
cluster autonomic non programmed FinPartState of SCM a₁;
existence

proof end;

end;

definition

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

proof end;

end;

theorem Th37: :: SCMRING4:37

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

proof end;

theorem Th38: :: SCMRING4:38

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

proof end;

theorem Th39: :: SCMRING4:39

for b₁ being good Ring
for b₂ being autonomic FinPartState of SCM b₁ st IC (SCM b₁) in dom b₂ holds
IC b₂ in dom b₂

proof end;

theorem Th40: :: SCMRING4:40

for b₁ being Nat
for b₂ being good Ring
for b₃ being State of (SCM b₂) st not b₂ is trivial holds
for b₄ being autonomic non programmed FinPartState of SCM b₂ st b₄ c= b₃ holds
IC ((Computation b₃) . b₁) in dom (ProgramPart b₄)

proof end;

theorem Th41: :: SCMRING4:41

for b₁ being Nat
for b₂ being good Ring
for b₃, b₄ being State of (SCM b₂) st not b₂ is trivial holds
for b₅ being autonomic non programmed FinPartState of SCM b₂ st b₅ c= b₃ & b₅ c= b₄ holds
( IC ((Computation b₃) . b₁) = IC ((Computation b₄) . b₁) & CurInstr ((Computation b₃) . b₁) = CurInstr ((Computation b₄) . b₁) )

proof end;

theorem Th42: :: SCMRING4:42

for b₁ being Nat
for b₂ being good Ring
for b₃, b₄ being Data-Location of b₂
for b₅, b₆ being State of (SCM b₂) st not b₂ is trivial holds
for b₇ being autonomic non programmed FinPartState of SCM b₂ st b₇ c= b₅ & b₇ c= b₆ & CurInstr ((Computation b₅) . b₁) = b₃ := b₄ & b₃ in dom b₇ holds
((Computation b₅) . b₁) . b₄ = ((Computation b₆) . b₁) . b₄

proof end;

theorem Th43: :: SCMRING4:43

for b₁ being Nat
for b₂ being good Ring
for b₃, b₄ being Data-Location of b₂
for b₅, b₆ being State of (SCM b₂) st not b₂ is trivial holds
for b₇ being autonomic non programmed FinPartState of SCM b₂ st b₇ c= b₅ & b₇ c= b₆ & CurInstr ((Computation b₅) . b₁) = AddTo b₃,b₄ & b₃ in dom b₇ holds
(((Computation b₅) . b₁) . b₃) + (((Computation b₅) . b₁) . b₄) = (((Computation b₆) . b₁) . b₃) + (((Computation b₆) . b₁) . b₄)

proof end;

theorem Th44: :: SCMRING4:44

for b₁ being Nat
for b₂ being good Ring
for b₃, b₄ being Data-Location of b₂
for b₅, b₆ being State of (SCM b₂) st not b₂ is trivial holds
for b₇ being autonomic non programmed FinPartState of SCM b₂ st b₇ c= b₅ & b₇ c= b₆ & CurInstr ((Computation b₅) . b₁) = SubFrom b₃,b₄ & b₃ in dom b₇ holds
(((Computation b₅) . b₁) . b₃) - (((Computation b₅) . b₁) . b₄) = (((Computation b₆) . b₁) . b₃) - (((Computation b₆) . b₁) . b₄)

proof end;

theorem Th45: :: SCMRING4:45

for b₁ being Nat
for b₂ being good Ring
for b₃, b₄ being Data-Location of b₂
for b₅, b₆ being State of (SCM b₂) st not b₂ is trivial holds
for b₇ being autonomic non programmed FinPartState of SCM b₂ st b₇ c= b₅ & b₇ c= b₆ & CurInstr ((Computation b₅) . b₁) = MultBy b₃,b₄ & b₃ in dom b₇ holds
(((Computation b₅) . b₁) . b₃) * (((Computation b₅) . b₁) . b₄) = (((Computation b₆) . b₁) . b₃) * (((Computation b₆) . b₁) . b₄)

proof end;

theorem Th46: :: SCMRING4:46

for b₁ being Nat
for b₂ being good Ring
for b₃ being Data-Location of b₂
for b₄ being Instruction-Location of (SCM b₂)
for b₅, b₆ being State of (SCM b₂) st not b₂ is trivial holds
for b₇ being autonomic non programmed FinPartState of SCM b₂ st b₇ c= b₅ & b₇ c= b₆ & CurInstr ((Computation b₅) . b₁) = b₃ =0_goto b₄ & b₄ <> Next (IC ((Computation b₅) . b₁)) holds
( ((Computation b₅) . b₁) . b₃ = 0. b₂ iff ((Computation b₆) . b₁) . b₃ = 0. b₂ )

proof end;

definition

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

end;

:: deftheorem Def2 defines Relocated SCMRING4:def 2 :

theorem Th47: :: SCMRING4:47

proof end;

theorem Th48: :: SCMRING4:48

for b₁ being natural number
for b₂ being with_non-empty_elements set
for b₃ being non empty non void IC-Ins-separated definite standard regular AMI-Struct of b₂
for b₄ being FinPartState of b₃ st b₃ is realistic holds
ProgramPart (Relocated b₄,b₁) = IncAddr (Shift (ProgramPart b₄),b₁),b₁

proof end;

theorem Th49: :: SCMRING4:49

for b₁ being natural number
for b₂ being with_non-empty_elements set
for b₃ being non empty non void IC-Ins-separated definite standard regular AMI-Struct of b₂
for b₄ being FinPartState of b₃ st b₃ is realistic holds
dom (ProgramPart (Relocated b₄,b₁)) = { (il. b₃,(b₅ + b₁)) where B is Nat : il. b₃,b₅ in dom (ProgramPart b₄) }

proof end;

theorem Th50: :: SCMRING4:50

for b₁ being natural number
for b₂ being with_non-empty_elements set
for b₃ being non empty non void IC-Ins-separated definite standard regular AMI-Struct of b₂
for b₄ being FinPartState of b₃
for b₅ being Instruction-Location of b₃ st b₃ is realistic holds
( b₅ in dom b₄ iff b₅ + b₁ in dom (Relocated b₄,b₁) )

proof end;

theorem Th51: :: SCMRING4:51

proof end;

theorem Th52: :: SCMRING4:52

proof end;

theorem Th53: :: SCMRING4:53

for b₁ being natural number
for b₂ being with_non-empty_elements set
for b₃ being non empty non void IC-Ins-separated definite standard regular AMI-Struct of b₂
for b₄ being programmed FinPartState of b₃
for b₅ being Instruction-Location of b₃ st b₅ in dom b₄ holds
(IncAddr b₄,b₁) . b₅ = IncAddr (pi b₄,b₅),b₁

proof end;

theorem Th54: :: SCMRING4:54

for b₁ being natural number
for b₂ being with_non-empty_elements set
for b₃ being non empty non void IC-Ins-separated definite standard regular AMI-Struct of b₂
for b₄ being programmed FinPartState of b₃ holds Shift (IncAddr b₄,b₁),b₁ = IncAddr (Shift b₄,b₁),b₁

proof end;

theorem Th55: :: SCMRING4:55

for b₁ being natural number
for b₂ being with_non-empty_elements set
for b₃ being non empty non void IC-Ins-separated definite standard regular AMI-Struct of b₂
for b₄ being FinPartState of b₃
for b₅ being Instruction-Location of b₃ st b₃ is realistic holds
for b₆ being Instruction of b₃ st b₅ in dom (ProgramPart b₄) & b₆ = b₄ . b₅ holds
IncAddr b₆,b₁ = (Relocated b₄,b₁) . (b₅ + b₁)

proof end;

theorem Th56: :: SCMRING4:56

proof end;

theorem Th57: :: SCMRING4:57

for b₁ being natural number
for b₂ being with_non-empty_elements set
for b₃ being non empty non void IC-Ins-separated definite standard regular AMI-Struct of b₂
for b₄ being FinPartState of b₃ st b₃ is realistic holds
for b₅ being data-only FinPartState of b₃ st IC b₃ in dom b₄ holds
Relocated (b₄ +* b₅),b₁ = (Relocated b₄,b₁) +* b₅

proof end;

theorem Th58: :: SCMRING4:58

for b₁ being natural number
for b₂ being good Ring
for b₃, b₄ being State of (SCM b₂)
for b₅ being autonomic FinPartState of SCM b₂ st b₅ c= b₃ & Relocated b₅,b₁ c= b₄ holds
b₅ c= b₃ +* (b₄ | SCM-Data-Loc )

proof end;

theorem Th59: :: SCMRING4:59

for b₁ being natural number
for b₂ being good Ring
for b₃, b₄, b₅ being State of (SCM b₂) st not b₂ is trivial holds
for b₆ being autonomic FinPartState of SCM b₂ st IC (SCM b₂) in dom b₆ & b₆ c= b₃ & Relocated b₆,b₁ c= b₄ & b₅ = b₃ +* (b₄ | SCM-Data-Loc ) holds
for b₇ being Nat holds
( (IC ((Computation b₃) . b₇)) + b₁ = IC ((Computation b₄) . b₇) & IncAddr (CurInstr ((Computation b₃) . b₇)),b₁ = CurInstr ((Computation b₄) . b₇) & ((Computation b₃) . b₇) | (dom (DataPart b₆)) = ((Computation b₄) . b₇) | (dom (DataPart (Relocated b₆,b₁))) & ((Computation b₅) . b₇) | SCM-Data-Loc = ((Computation b₄) . b₇) | SCM-Data-Loc )

proof end;

theorem Th60: :: SCMRING4:60

for b₁ being natural number
for b₂ being good Ring st not b₂ is trivial holds
for b₃ being autonomic FinPartState of SCM b₂ st IC (SCM b₂) in dom b₃ holds
( b₃ is halting iff Relocated b₃,b₁ is halting )

proof end;

theorem Th61: :: SCMRING4:61

for b₁ being natural number
for b₂ being good Ring
for b₃ being State of (SCM b₂) st not b₂ is trivial holds
for b₄ being autonomic FinPartState of SCM b₂ st IC (SCM b₂) in dom b₄ & b₄ c= b₃ holds
for b₅ being Nat holds (Computation (b₃ +* (Relocated b₄,b₁))) . b₅ = (((Computation b₃) . b₅) +* (Start-At ((IC ((Computation b₃) . b₅)) + b₁))) +* (ProgramPart (Relocated b₄,b₁))

proof end;

theorem Th62: :: SCMRING4:62

for b₁ being natural number
for b₂ being good Ring
for b₃ being State of (SCM b₂) st not b₂ is trivial holds
for b₄ being autonomic FinPartState of SCM b₂ st IC (SCM b₂) in dom b₄ & Relocated b₄,b₁ c= b₃ holds
for b₅ being Nat holds (Computation b₃) . b₅ = ((((Computation (b₃ +* b₄)) . b₅) +* (Start-At ((IC ((Computation (b₃ +* b₄)) . b₅)) + b₁))) +* (b₃ | (dom (ProgramPart b₄)))) +* (ProgramPart (Relocated b₄,b₁))

proof end;

theorem Th63: :: SCMRING4:63

for b₁ being natural number
for b₂ being good Ring
for b₃ being FinPartState of SCM b₂
for b₄ being State of (SCM b₂) st not b₂ is trivial & IC (SCM b₂) in dom b₃ & b₃ c= b₄ & Relocated b₃,b₁ is autonomic holds
for b₅ being Nat holds (Computation b₄) . b₅ = ((((Computation (b₄ +* (Relocated b₃,b₁))) . b₅) +* (Start-At ((IC ((Computation (b₄ +* (Relocated b₃,b₁))) . b₅)) -' b₁))) +* (b₄ | (dom (ProgramPart (Relocated b₃,b₁))))) +* (ProgramPart b₃)

proof end;

theorem Th64: :: SCMRING4:64

for b₁ being natural number
for b₂ being good Ring
for b₃ being FinPartState of SCM b₂ st not b₂ is trivial & IC (SCM b₂) in dom b₃ holds
( b₃ is autonomic iff Relocated b₃,b₁ is autonomic )

proof end;

theorem Th65: :: SCMRING4:65

for b₁ being natural number
for b₂ being good Ring st not b₂ is trivial holds
for b₃ being autonomic halting FinPartState of SCM b₂ st IC (SCM b₂) in dom b₃ holds
DataPart (Result b₃) = DataPart (Result (Relocated b₃,b₁))

proof end;

theorem Th66: :: SCMRING4:66

for b₁ being natural number
for b₂ being good Ring
for b₃ being FinPartState of SCM b₂ st not b₂ is trivial holds
for b₄ being PartFunc of FinPartSt (SCM b₂), FinPartSt (SCM b₂) st IC (SCM b₂) in dom b₃ & b₄ is data-only holds
( b₃ computes b₄ iff Relocated b₃,b₁ computes b₄ )

proof end;