:: AMI_5 semantic presentation

theorem Th1: :: AMI_5:1

canceled;

theorem Th2: :: AMI_5:2

canceled;

theorem Th3: :: AMI_5:3

canceled;

theorem Th4: :: AMI_5:4

canceled;

theorem Th5: :: AMI_5:5

canceled;

theorem Th6: :: AMI_5:6

canceled;

theorem Th7: :: AMI_5:7

canceled;

theorem Th8: :: AMI_5:8

canceled;

theorem Th9: :: AMI_5:9

canceled;

theorem Th10: :: AMI_5:10

canceled;

theorem Th11: :: AMI_5:11

canceled;

theorem Th12: :: AMI_5:12

canceled;

theorem Th13: :: AMI_5:13

canceled;

theorem Th14: :: AMI_5:14

canceled;

theorem Th15: :: AMI_5:15

for b₁ being Data-Location
for b₂ being State of SCM holds
( (Exec (Divide b₁,b₁),b₂) . (IC SCM ) = Next (IC b₂) & (Exec (Divide b₁,b₁),b₂) . b₁ = (b₂ . b₁) mod (b₂ . b₁) & ( for b₃ being Data-Location st b₃ <> b₁ holds
(Exec (Divide b₁,b₁),b₂) . b₃ = b₂ . b₃ ) ) by AMI_3:12;

theorem Th16: :: AMI_5:16

for b₁ being set st b₁ in SCM-Data-Loc holds
b₁ is Data-Location by AMI_3:def 1, AMI_3:def 2;

theorem Th17: :: AMI_5:17

canceled;

theorem Th18: :: AMI_5:18

for b₁ being Data-Location ex b₂ being Nat st b₁ = dl. b₂

proof end;

theorem Th19: :: AMI_5:19

for b₁ being Instruction-Location of SCM ex b₂ being Nat st b₁ = il. b₂

proof end;

theorem Th20: :: AMI_5:20

for b₁ being Data-Location holds b₁ <> IC SCM

proof end;

theorem Th21: :: AMI_5:21

canceled;

theorem Th22: :: AMI_5:22

for b₁ being Instruction-Location of SCM
for b₂ being Data-Location holds b₁ <> b₂

proof end;

theorem Th23: :: AMI_5:23

the carrier of SCM = ({(IC SCM )} \/ SCM-Data-Loc ) \/ SCM-Instr-Loc

proof end;

theorem Th24: :: AMI_5:24

for b₁ being State of SCM
for b₂ being Data-Location
for b₃ being Instruction-Location of SCM holds
( b₂ in dom b₁ & b₃ in dom b₁ )

proof end;

theorem Th25: :: AMI_5:25

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 State of b₂ holds IC b₂ in dom b₃

proof end;

theorem Th26: :: AMI_5:26

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

proof end;

theorem Th27: :: AMI_5:27

for b₁ being State of SCM holds SCM-Data-Loc c= dom b₁

proof end;

theorem Th28: :: AMI_5:28

for b₁ being State of SCM holds SCM-Instr-Loc c= dom b₁

proof end;

theorem Th29: :: AMI_5:29

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

proof end;

theorem Th30: :: AMI_5:30

for b₁ being State of SCM holds dom (b₁ | SCM-Instr-Loc ) = SCM-Instr-Loc

proof end;

theorem Th31: :: AMI_5:31

not SCM-Data-Loc is finite

proof end;

theorem Th32: :: AMI_5:32

not the Instruction-Locations of SCM is finite

proof end;

registration

cluster SCM-Data-Loc -> infinite ;
coherence by Th31;
cluster the Instruction-Locations of SCM -> infinite ;
coherence by Th32;

end;

theorem Th33: :: AMI_5:33

SCM-Data-Loc misses SCM-Instr-Loc

proof end;

theorem Th34: :: AMI_5:34

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 State of b₂ holds Start-At (IC b₃) = b₃ | {(IC b₂)}

proof end;

theorem Th35: :: AMI_5:35

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 Instruction-Location of b₂ holds Start-At b₃ = {[(IC b₂),b₃]}

proof end;

definition

let c₁ be set ;
let c₂ be AMI-Struct of c₁;
let c₃ be Element of the Instructions of c₂;
func InsCode c₃ -> InsType of a₂ equals :: AMI_5:def 1
a₃ `1 ;
coherence

proof end;

end;

:: deftheorem Def1 defines InsCode AMI_5:def 1 :

registration

let c₁ be Instruction of SCM ;
cluster InsCode a₁ -> natural ;
coherence

proof end;

end;

definition

let c₁ be Instruction of SCM ;
func @ c₁ -> Element of SCM-Instr equals :: AMI_5:def 2
a₁;
coherence by AMI_3:def 1;

end;

:: deftheorem Def2 defines @ AMI_5:def 2 :

definition

let c₁ be Element of SCM-Instr-Loc ;
func c₁ @ -> Instruction-Location of SCM equals :: AMI_5:def 3
a₁;
coherence by AMI_3:def 1;

end;

:: deftheorem Def3 defines @ AMI_5:def 3 :

definition

let c₁ be Element of SCM-Data-Loc ;
func c₁ @ -> Data-Location equals :: AMI_5:def 4
a₁;
coherence by AMI_3:def 1, AMI_3:def 2;

end;

:: deftheorem Def4 defines @ AMI_5:def 4 :

theorem Th36: :: AMI_5:36

for b₁ being Instruction of SCM holds InsCode b₁ <= 8

proof end;

theorem Th37: :: AMI_5:37

InsCode (halt SCM ) = 0 by AMI_3:71, MCART_1:7;

theorem Th38: :: AMI_5:38

for b₁, b₂ being Data-Location holds InsCode (b₁ := b₂) = 1 by MCART_1:7;

theorem Th39: :: AMI_5:39

for b₁, b₂ being Data-Location holds InsCode (AddTo b₁,b₂) = 2 by MCART_1:7;

theorem Th40: :: AMI_5:40

for b₁, b₂ being Data-Location holds InsCode (SubFrom b₁,b₂) = 3 by MCART_1:7;

theorem Th41: :: AMI_5:41

for b₁, b₂ being Data-Location holds InsCode (MultBy b₁,b₂) = 4 by MCART_1:7;

theorem Th42: :: AMI_5:42

for b₁, b₂ being Data-Location holds InsCode (Divide b₁,b₂) = 5 by MCART_1:7;

theorem Th43: :: AMI_5:43

for b₁ being Instruction-Location of SCM holds InsCode (goto b₁) = 6 by MCART_1:7;

theorem Th44: :: AMI_5:44

for b₁ being Data-Location
for b₂ being Instruction-Location of SCM holds InsCode (b₁ =0_goto b₂) = 7 by MCART_1:7;

theorem Th45: :: AMI_5:45

for b₁ being Data-Location
for b₂ being Instruction-Location of SCM holds InsCode (b₁ >0_goto b₂) = 8 by MCART_1:7;

theorem Th46: :: AMI_5:46

for b₁ being Instruction of SCM st InsCode b₁ = 0 holds
b₁ = halt SCM

proof end;

theorem Th47: :: AMI_5:47

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

proof end;

theorem Th48: :: AMI_5:48

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

proof end;

theorem Th49: :: AMI_5:49

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

proof end;

theorem Th50: :: AMI_5:50

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

proof end;

theorem Th51: :: AMI_5:51

for b₁ being Instruction of SCM st InsCode b₁ = 5 holds
ex b₂, b₃ being Data-Location st b₁ = Divide b₂,b₃

proof end;

theorem Th52: :: AMI_5:52

for b₁ being Instruction of SCM st InsCode b₁ = 6 holds
ex b₂ being Instruction-Location of SCM st b₁ = goto b₂

proof end;

theorem Th53: :: AMI_5:53

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

proof end;

theorem Th54: :: AMI_5:54

for b₁ being Instruction of SCM st InsCode b₁ = 8 holds
ex b₂ being Instruction-Location of SCM ex b₃ being Data-Location st b₁ = b₃ >0_goto b₂

proof end;

theorem Th55: :: AMI_5:55

for b₁ being Instruction-Location of SCM holds (@ (goto b₁)) jump_address = b₁

proof end;

theorem Th56: :: AMI_5:56

for b₁ being Instruction-Location of SCM
for b₂ being Data-Location holds
( (@ (b₂ =0_goto b₁)) cjump_address = b₁ & (@ (b₂ =0_goto b₁)) cond_address = b₂ )

proof end;

theorem Th57: :: AMI_5:57

for b₁ being Instruction-Location of SCM
for b₂ being Data-Location holds
( (@ (b₂ >0_goto b₁)) cjump_address = b₁ & (@ (b₂ >0_goto b₁)) cond_address = b₂ )

proof end;

theorem Th58: :: AMI_5:58

for b₁, b₂ being State of SCM st b₁ | (SCM-Data-Loc \/ {(IC SCM )}) = b₂ | (SCM-Data-Loc \/ {(IC SCM )}) holds
for b₃ being Instruction of SCM holds (Exec b₃,b₁) | (SCM-Data-Loc \/ {(IC SCM )}) = (Exec b₃,b₂) | (SCM-Data-Loc \/ {(IC SCM )})

proof end;

theorem Th59: :: AMI_5:59

for b₁ being Instruction of SCM
for b₂ being State of SCM holds (Exec b₁,b₂) | SCM-Instr-Loc = b₂ | SCM-Instr-Loc

proof end;

theorem Th60: :: AMI_5:60

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₂
for b₄ being State of b₂ st IC b₂ in dom b₃ & b₃ c= b₄ holds
IC b₃ = IC b₄

proof end;

definition

let c₁ be with_non-empty_elements set ;
let c₂ be non empty non void IC-Ins-separated definite AMI-Struct of c₁;
let c₃ be FinPartState of c₂;
let c₄ be Instruction-Location of c₂;
assume E29: c₄ in dom c₃ ;
func pi c₃,c₄ -> Instruction of a₂ equals :: AMI_5:def 5
a₃ . a₄;
coherence

proof end;

end;

:: deftheorem Def5 defines pi AMI_5:def 5 :

theorem Th61: :: AMI_5:61

for b₁ being set
for b₂ being AMI-Struct of b₁
for b₃ being set
for b₄ being FinPartState of b₂ st b₃ c= b₄ holds
b₃ is FinPartState of b₂

proof end;

definition

let c₁ be set ;
let c₂ be AMI-Struct of c₁;
let c₃ be FinPartState of c₂;
func ProgramPart c₃ -> programmed FinPartState of a₂ equals :: AMI_5:def 6
a₃ | the Instruction-Locations of a₂;
coherence

proof end;

end;

:: deftheorem Def6 defines ProgramPart AMI_5:def 6 :

definition

let c₁ be set ;
let c₂ be non empty AMI-Struct of c₁;
let c₃ be FinPartState of c₂;
func DataPart c₃ -> FinPartState of a₂ equals :: AMI_5:def 7
a₃ | (the carrier of a₂ \ ({(IC a₂)} \/ the Instruction-Locations of a₂));
coherence

proof end;

end;

:: deftheorem Def7 defines DataPart AMI_5:def 7 :

definition

let c₁ be set ;
let c₂ be non empty AMI-Struct of c₁;
let c₃ be FinPartState of c₂;
attr a₃ is data-only means :Def8: :: AMI_5:def 8
dom a₃ misses {(IC a₂)} \/ the Instruction-Locations of a₂;

end;

:: deftheorem Def8 defines data-only AMI_5:def 8 :

Lemma31: for b₁ being FinPartState of SCM holds DataPart b₁ = b₁ | SCM-Data-Loc

proof end;

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

proof end;

registration

let c₁ be set ;
let c₂ be non empty AMI-Struct of c₁;
cluster data-only FinPartState of a₂;
existence

proof end;

end;

theorem Th62: :: AMI_5:62

for b₁ being set
for b₂ being non empty AMI-Struct of b₁
for b₃ being FinPartState of b₂ holds DataPart b₃ c= b₃ by RELAT_1:88;

theorem Th63: :: AMI_5:63

for b₁ being set
for b₂ being AMI-Struct of b₁
for b₃ being FinPartState of b₂ holds ProgramPart b₃ c= b₃ by RELAT_1:88;

theorem Th64: :: AMI_5:64

for b₁ being with_non-empty_elements set
for b₂ being non empty non void IC-Ins-separated steady-programmed definite AMI-Struct of b₁
for b₃ being FinPartState of b₂
for b₄ being State of b₂ st b₃ c= b₄ holds
for b₅ being Nat holds ProgramPart b₃ c= (Computation b₄) . b₅

proof end;

theorem Th65: :: AMI_5:65

for b₁ being set
for b₂ being non empty AMI-Struct of b₁
for b₃ being FinPartState of b₂ holds not IC b₂ in dom (DataPart b₃)

proof end;

theorem Th66: :: AMI_5:66

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 not IC b₂ in dom (ProgramPart b₃)

proof end;

theorem Th67: :: AMI_5:67

for b₁ being set
for b₂ being non empty AMI-Struct of b₁
for b₃ being FinPartState of b₂ holds {(IC b₂)} misses dom (DataPart b₃)

proof end;

theorem Th68: :: AMI_5:68

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 {(IC b₂)} misses dom (ProgramPart b₃)

proof end;

theorem Th69: :: AMI_5:69

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

proof end;

theorem Th70: :: AMI_5:70

for b₁ being FinPartState of SCM holds dom (ProgramPart b₁) c= SCM-Instr-Loc by AMI_3:def 1, RELAT_1:87;

theorem Th71: :: AMI_5:71

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₃, b₄ being FinPartState of b₂ holds dom (DataPart b₃) misses dom (ProgramPart b₄)

proof end;

theorem Th72: :: AMI_5:72

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 programmed FinPartState of b₂ holds ProgramPart b₃ = b₃

proof end;

theorem Th73: :: AMI_5:73

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₂
for b₄ being Instruction-Location of b₂ st b₄ in dom b₃ holds
b₄ in dom (ProgramPart b₃)

proof end;

theorem Th74: :: AMI_5:74

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 data-only FinPartState of b₂
for b₄ being FinPartState of b₂ holds
( b₃ c= b₄ iff b₃ c= DataPart b₄ )

proof end;

theorem Th75: :: AMI_5:75

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₂ st IC b₂ in dom b₃ holds
b₃ = ((Start-At (IC b₃)) +* (ProgramPart b₃)) +* (DataPart b₃)

proof end;

definition

let c₁ be with_non-empty_elements set ;
let c₂ be non empty non void IC-Ins-separated definite AMI-Struct of c₁;
let c₃ be PartFunc of FinPartSt c₂, FinPartSt c₂;
attr a₃ is data-only means :: AMI_5:def 9
for b₁ being FinPartState of a₂ st b₁ in dom a₃ holds
( b₁ is data-only & ( for b₂ being FinPartState of a₂ st b₂ = a₃ . b₁ holds
b₂ is data-only ) );

end;

:: deftheorem Def9 defines data-only AMI_5:def 9 :

theorem Th76: :: AMI_5:76

proof end;

definition

let c₁ be with_non-empty_elements set ;
let c₂ be non void AMI-Struct of c₁;
let c₃ be State of c₂;
let c₄ be FinPartState of c₂;
redefine func +* as c₃ +* c₄ -> State of a₂;
coherence

proof end;

end;

theorem Th77: :: AMI_5:77

for b₁ being Instruction of SCM
for b₂ being State of SCM
for b₃ being programmed FinPartState of SCM holds Exec b₁,(b₂ +* b₃) = (Exec b₁,b₂) +* b₃

proof end;

theorem Th78: :: AMI_5:78

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₂ st IC b₂ in dom b₃ holds
Start-At (IC b₃) c= b₃

proof end;

theorem Th79: :: AMI_5:79

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 State of b₂
for b₄ being Instruction-Location of b₂ holds IC (b₃ +* (Start-At b₄)) = b₄

proof end;

theorem Th80: :: AMI_5:80

for b₁ being State of SCM
for b₂ being Instruction-Location of SCM
for b₃ being Data-Location holds b₁ . b₃ = (b₁ +* (Start-At b₂)) . b₃

proof end;

theorem Th81: :: AMI_5:81

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 State of b₂
for b₄, b₅ being Instruction-Location of b₂ holds b₃ . b₅ = (b₃ +* (Start-At b₄)) . b₅

proof end;

theorem Th82: :: AMI_5:82

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₃, b₄ being State of b₂
for b₅ being set holds b₃ +* (b₄ | b₅) is State of b₂

proof end;

theorem Th83: :: AMI_5:83

for b₁ being autonomic FinPartState of SCM st DataPart b₁ <> {} holds
IC SCM in dom b₁

proof end;

registration

cluster autonomic non programmed FinPartState of SCM ;
existence

proof end;

end;

theorem Th84: :: AMI_5:84

for b₁ being autonomic non programmed FinPartState of SCM holds IC SCM in dom b₁

proof end;

theorem Th85: :: AMI_5:85

for b₁ being autonomic FinPartState of SCM st IC SCM in dom b₁ holds
IC b₁ in dom b₁

proof end;

theorem Th86: :: AMI_5:86

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

proof end;

theorem Th87: :: AMI_5:87

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

proof end;

theorem Th88: :: AMI_5:88

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

proof end;

theorem Th89: :: AMI_5:89

for b₁ being autonomic non programmed FinPartState of SCM
for b₂, b₃ being State of SCM st b₁ c= b₂ & b₁ c= b₃ holds
for b₄ being Nat
for b₅, b₆ being Data-Location
for b₇ being Instruction of SCM st b₇ = CurInstr ((Computation b₂) . 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 Th90: :: AMI_5:90

for b₁ being autonomic non programmed FinPartState of SCM
for b₂, b₃ being State of SCM st b₁ c= b₂ & b₁ c= b₃ holds
for b₄ being Nat
for b₅, b₆ being Data-Location
for b₇ being Instruction of SCM st b₇ = CurInstr ((Computation b₂) . 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 Th91: :: AMI_5:91

for b₁ being autonomic non programmed FinPartState of SCM
for b₂, b₃ being State of SCM st b₁ c= b₂ & b₁ c= b₃ holds
for b₄ being Nat
for b₅, b₆ being Data-Location
for b₇ being Instruction of SCM st b₇ = CurInstr ((Computation b₂) . 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 Th92: :: AMI_5:92

for b₁ being autonomic non programmed FinPartState of SCM
for b₂, b₃ being State of SCM st b₁ c= b₂ & b₁ c= b₃ holds
for b₄ being Nat
for b₅, b₆ being Data-Location
for b₇ being Instruction of SCM st b₇ = CurInstr ((Computation b₂) . b₄) & b₇ = Divide b₅,b₆ & b₅ in dom b₁ & b₅ <> b₆ holds
(((Computation b₂) . b₄) . b₅) div (((Computation b₂) . b₄) . b₆) = (((Computation b₃) . b₄) . b₅) div (((Computation b₃) . b₄) . b₆)

proof end;

theorem Th93: :: AMI_5:93

for b₁ being autonomic non programmed FinPartState of SCM
for b₂, b₃ being State of SCM st b₁ c= b₂ & b₁ c= b₃ holds
for b₄ being Nat
for b₅, b₆ being Data-Location
for b₇ being Instruction of SCM st b₇ = CurInstr ((Computation b₂) . b₄) & b₇ = Divide b₅,b₆ & b₆ in dom b₁ & b₅ <> b₆ holds
(((Computation b₂) . b₄) . b₅) mod (((Computation b₂) . b₄) . b₆) = (((Computation b₃) . b₄) . b₅) mod (((Computation b₃) . b₄) . b₆)

proof end;

theorem Th94: :: AMI_5:94

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

proof end;

theorem Th95: :: AMI_5:95

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

proof end;

theorem Th96: :: AMI_5:96

for b₁ being FinPartState of SCM holds DataPart b₁ = b₁ | SCM-Data-Loc by Lemma31;

theorem Th97: :: AMI_5:97

for b₁ being FinPartState of SCM holds
( b₁ is data-only iff dom b₁ c= SCM-Data-Loc ) by Lemma32;