:: AMI_5 semantic presentation

theorem :: AMI_5:1

canceled;

theorem :: AMI_5:2

canceled;

theorem :: AMI_5:3

canceled;

theorem :: AMI_5:4

canceled;

theorem :: AMI_5:5

canceled;

theorem :: AMI_5:6

canceled;

theorem :: AMI_5:7

canceled;

theorem :: AMI_5:8

canceled;

theorem :: AMI_5:9

canceled;

theorem :: AMI_5:10

canceled;

theorem :: AMI_5:11

canceled;

theorem :: AMI_5:12

canceled;

theorem :: AMI_5:13

canceled;

theorem :: AMI_5:14

canceled;

theorem Th15: :: AMI_5:15

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

theorem Th16: :: AMI_5:16

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

theorem :: AMI_5:17

canceled;

theorem Th18: :: AMI_5:18

for dl being Data-Location ex i being Nat st dl = dl. i

proof end;

theorem Th19: :: AMI_5:19

for il being Instruction-Location of SCM ex i being Nat st il = il. i

proof end;

theorem Th20: :: AMI_5:20

for dl being Data-Location holds dl <> IC SCM

proof end;

theorem :: AMI_5:21

canceled;

theorem Th22: :: AMI_5:22

for il being Instruction-Location of SCM
for dl being Data-Location holds il <> dl

proof end;

theorem Th23: :: AMI_5:23

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

proof end;

theorem :: AMI_5:24

for s being State of SCM
for d being Data-Location
for l being Instruction-Location of SCM holds
( d in dom s & l in dom s )

proof end;

theorem Th25: :: AMI_5:25

for N being with_non-empty_elements set
for S being non empty non void IC-Ins-separated definite AMI-Struct of N
for s being State of S holds IC S in dom s

proof end;

theorem :: AMI_5:26

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

proof end;

theorem Th27: :: AMI_5:27

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

proof end;

theorem Th28: :: AMI_5:28

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

proof end;

theorem :: AMI_5:29

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

proof end;

theorem :: AMI_5:30

for s being State of SCM holds dom (s | 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 :: AMI_5:34

for N being with_non-empty_elements set
for S being non empty non void IC-Ins-separated definite AMI-Struct of N
for s being State of S holds Start-At (IC s) = s | {(IC S)}

proof end;

theorem Th35: :: AMI_5:35

for N being with_non-empty_elements set
for S being non empty non void IC-Ins-separated definite AMI-Struct of N
for l being Instruction-Location of S holds Start-At l = {[(IC S),l]}

proof end;

definition

let N be set ;
let A be AMI-Struct of N;
let I be Element of the Instructions of A;
func InsCode I -> InsType of A equals :: AMI_5:def 1
I `1 ;
coherence

proof end;

end;

:: deftheorem defines InsCode AMI_5:def 1 :

registration

let I be Instruction of SCM ;
cluster InsCode I -> natural ;
coherence

proof end;

end;

definition

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

end;

:: deftheorem defines @ AMI_5:def 2 :

definition

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

end;

:: deftheorem defines @ AMI_5:def 3 :

definition

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

end;

:: deftheorem defines @ AMI_5:def 4 :

theorem Th36: :: AMI_5:36

for l being Instruction of SCM holds InsCode l <= 8

proof end;

theorem Th37: :: AMI_5:37

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

theorem :: AMI_5:38

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

theorem :: AMI_5:39

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

theorem :: AMI_5:40

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

theorem :: AMI_5:41

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

theorem :: AMI_5:42

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

theorem :: AMI_5:43

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

theorem :: AMI_5:44

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

theorem :: AMI_5:45

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

theorem Th46: :: AMI_5:46

for ins being Instruction of SCM st InsCode ins = 0 holds
ins = halt SCM

proof end;

theorem Th47: :: AMI_5:47

for ins being Instruction of SCM st InsCode ins = 1 holds
ex da, db being Data-Location st ins = da := db

proof end;

theorem Th48: :: AMI_5:48

for ins being Instruction of SCM st InsCode ins = 2 holds
ex da, db being Data-Location st ins = AddTo da,db

proof end;

theorem Th49: :: AMI_5:49

for ins being Instruction of SCM st InsCode ins = 3 holds
ex da, db being Data-Location st ins = SubFrom da,db

proof end;

theorem Th50: :: AMI_5:50

for ins being Instruction of SCM st InsCode ins = 4 holds
ex da, db being Data-Location st ins = MultBy da,db

proof end;

theorem Th51: :: AMI_5:51

for ins being Instruction of SCM st InsCode ins = 5 holds
ex da, db being Data-Location st ins = Divide da,db

proof end;

theorem Th52: :: AMI_5:52

for ins being Instruction of SCM st InsCode ins = 6 holds
ex loc being Instruction-Location of SCM st ins = goto loc

proof end;

theorem Th53: :: AMI_5:53

for ins being Instruction of SCM st InsCode ins = 7 holds
ex loc being Instruction-Location of SCM ex da being Data-Location st ins = da =0_goto loc

proof end;

theorem Th54: :: AMI_5:54

for ins being Instruction of SCM st InsCode ins = 8 holds
ex loc being Instruction-Location of SCM ex da being Data-Location st ins = da >0_goto loc

proof end;

theorem :: AMI_5:55

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

proof end;

theorem :: AMI_5:56

for loc being Instruction-Location of SCM
for a being Data-Location holds
( (@ (a =0_goto loc)) cjump_address = loc & (@ (a =0_goto loc)) cond_address = a )

proof end;

theorem :: AMI_5:57

for loc being Instruction-Location of SCM
for a being Data-Location holds
( (@ (a >0_goto loc)) cjump_address = loc & (@ (a >0_goto loc)) cond_address = a )

proof end;

theorem Th58: :: AMI_5:58

for s1, s2 being State of SCM st s1 | (SCM-Data-Loc \/ {(IC SCM )}) = s2 | (SCM-Data-Loc \/ {(IC SCM )}) holds
for l being Instruction of SCM holds (Exec l,s1) | (SCM-Data-Loc \/ {(IC SCM )}) = (Exec l,s2) | (SCM-Data-Loc \/ {(IC SCM )})

proof end;

theorem Th59: :: AMI_5:59

for i being Instruction of SCM
for s being State of SCM holds (Exec i,s) | SCM-Instr-Loc = s | SCM-Instr-Loc

proof end;

theorem Th60: :: AMI_5:60

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
for s being State of S st IC S in dom p & p c= s holds
IC p = IC s

proof end;

definition

let N be with_non-empty_elements set ;
let S be non empty non void IC-Ins-separated definite AMI-Struct of N;
let p be FinPartState of S;
let loc be Instruction-Location of S;
assume A1: loc in dom p ;
func pi p,loc -> Instruction of S equals :: AMI_5:def 5
p . loc;
coherence

proof end;

end;

:: deftheorem defines pi AMI_5:def 5 :

theorem Th61: :: AMI_5:61

for N being set
for S being AMI-Struct of N
for x being set
for p being FinPartState of S st x c= p holds
x is FinPartState of S

proof end;

definition

let N be set ;
let S be AMI-Struct of N;
let p be FinPartState of S;
func ProgramPart p -> programmed FinPartState of S equals :: AMI_5:def 6
p | the Instruction-Locations of S;
coherence

proof end;

end;

:: deftheorem defines ProgramPart AMI_5:def 6 :

definition

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

proof end;

end;

:: deftheorem defines DataPart AMI_5:def 7 :

definition

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

end;

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

Lm1: for p being FinPartState of SCM holds DataPart p = p | SCM-Data-Loc

proof end;

Lm2: for f being FinPartState of SCM holds
( f is data-only iff dom f c= SCM-Data-Loc )

proof end;

registration

let N be set ;
let S be non empty AMI-Struct of N;
cluster data-only FinPartState of S;
existence

proof end;

end;

theorem Th62: :: AMI_5:62

for N being set
for S being non empty AMI-Struct of N
for p being FinPartState of S holds DataPart p c= p by RELAT_1:88;

theorem Th63: :: AMI_5:63

for N being set
for S being AMI-Struct of N
for p being FinPartState of S holds ProgramPart p c= p by RELAT_1:88;

theorem :: AMI_5:64

for N being with_non-empty_elements set
for S being non empty non void IC-Ins-separated steady-programmed definite AMI-Struct of N
for p being FinPartState of S
for s being State of S st p c= s holds
for i being Nat holds ProgramPart p c= (Computation s) . i

proof end;

theorem Th65: :: AMI_5:65

for N being set
for S being non empty AMI-Struct of N
for p being FinPartState of S holds not IC S in dom (DataPart p)

proof end;

theorem Th66: :: AMI_5:66

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 not IC S in dom (ProgramPart p)

proof end;

theorem :: AMI_5:67

for N being set
for S being non empty AMI-Struct of N
for p being FinPartState of S holds {(IC S)} misses dom (DataPart p)

proof end;

theorem :: AMI_5:68

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 {(IC S)} misses dom (ProgramPart p)

proof end;

theorem :: AMI_5:69

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

proof end;

theorem :: AMI_5:70

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

theorem Th71: :: AMI_5:71

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, q being FinPartState of S holds dom (DataPart p) misses dom (ProgramPart q)

proof end;

theorem Th72: :: AMI_5:72

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 programmed FinPartState of S holds ProgramPart p = p

proof end;

theorem :: AMI_5:73

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
for l being Instruction-Location of S st l in dom p holds
l in dom (ProgramPart p)

proof end;

theorem :: AMI_5:74

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 data-only FinPartState of S
for q being FinPartState of S holds
( p c= q iff p c= DataPart q )

proof end;

theorem :: AMI_5:75

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

proof end;

definition

let N be with_non-empty_elements set ;
let S be non empty non void IC-Ins-separated definite AMI-Struct of N;
let IT be PartFunc of FinPartSt S, FinPartSt S;
attr IT is data-only means :: AMI_5:def 9
for p being FinPartState of S st p in dom IT holds
( p is data-only & ( for q being FinPartState of S st q = IT . p holds
q is data-only ) );

end;

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

theorem :: AMI_5:76

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 st IC S in dom p holds
not p is programmed

proof end;

definition

let N be with_non-empty_elements set ;
let S be non void AMI-Struct of N;
let s be State of S;
let p be FinPartState of S;
:: original: +*
redefine func s +* p -> State of S;
coherence

proof end;

end;

theorem :: AMI_5:77

for i being Instruction of SCM
for s being State of SCM
for p being programmed FinPartState of SCM holds Exec i,(s +* p) = (Exec i,s) +* p

proof end;

theorem :: AMI_5:78

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 st IC S in dom p holds
Start-At (IC p) c= p

proof end;

theorem :: AMI_5:79

for N being with_non-empty_elements set
for S being non empty non void IC-Ins-separated definite AMI-Struct of N
for s being State of S
for iloc being Instruction-Location of S holds IC (s +* (Start-At iloc)) = iloc

proof end;

theorem :: AMI_5:80

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

proof end;

theorem :: AMI_5:81

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 s being State of S
for iloc, a being Instruction-Location of S holds s . a = (s +* (Start-At iloc)) . a

proof end;

theorem :: AMI_5:82

for N being with_non-empty_elements set
for S being non empty non void IC-Ins-separated definite AMI-Struct of N
for s, t being State of S
for A being set holds s +* (t | A) is State of S

proof end;

theorem Th83: :: AMI_5:83

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

proof end;

registration

cluster autonomic non programmed FinPartState of SCM ;
existence

proof end;

end;

theorem Th84: :: AMI_5:84

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

proof end;

theorem :: AMI_5:85

for p being autonomic FinPartState of SCM st IC SCM in dom p holds
IC p in dom p

proof end;

theorem Th86: :: AMI_5:86

for p being autonomic non programmed FinPartState of SCM
for s being State of SCM st p c= s holds
for i being Nat holds IC ((Computation s) . i) in dom (ProgramPart p)

proof end;

theorem Th87: :: AMI_5:87

for p being autonomic non programmed FinPartState of SCM
for s1, s2 being State of SCM st p c= s1 & p c= s2 holds
for i being Nat
for I being Instruction of SCM st I = CurInstr ((Computation s1) . i) holds
( IC ((Computation s1) . i) = IC ((Computation s2) . i) & I = CurInstr ((Computation s2) . i) )

proof end;

theorem :: AMI_5:88

for p being autonomic non programmed FinPartState of SCM
for s1, s2 being State of SCM st p c= s1 & p c= s2 holds
for i being Nat
for da, db being Data-Location
for I being Instruction of SCM st I = CurInstr ((Computation s1) . i) & I = da := db & da in dom p holds
((Computation s1) . i) . db = ((Computation s2) . i) . db

proof end;

theorem :: AMI_5:89

for p being autonomic non programmed FinPartState of SCM
for s1, s2 being State of SCM st p c= s1 & p c= s2 holds
for i being Nat
for da, db being Data-Location
for I being Instruction of SCM st I = CurInstr ((Computation s1) . i) & I = AddTo da,db & da in dom p holds
(((Computation s1) . i) . da) + (((Computation s1) . i) . db) = (((Computation s2) . i) . da) + (((Computation s2) . i) . db)

proof end;

theorem :: AMI_5:90

for p being autonomic non programmed FinPartState of SCM
for s1, s2 being State of SCM st p c= s1 & p c= s2 holds
for i being Nat
for da, db being Data-Location
for I being Instruction of SCM st I = CurInstr ((Computation s1) . i) & I = SubFrom da,db & da in dom p holds
(((Computation s1) . i) . da) - (((Computation s1) . i) . db) = (((Computation s2) . i) . da) - (((Computation s2) . i) . db)

proof end;

theorem :: AMI_5:91

for p being autonomic non programmed FinPartState of SCM
for s1, s2 being State of SCM st p c= s1 & p c= s2 holds
for i being Nat
for da, db being Data-Location
for I being Instruction of SCM st I = CurInstr ((Computation s1) . i) & I = MultBy da,db & da in dom p holds
(((Computation s1) . i) . da) * (((Computation s1) . i) . db) = (((Computation s2) . i) . da) * (((Computation s2) . i) . db)

proof end;

theorem :: AMI_5:92

for p being autonomic non programmed FinPartState of SCM
for s1, s2 being State of SCM st p c= s1 & p c= s2 holds
for i being Nat
for da, db being Data-Location
for I being Instruction of SCM st I = CurInstr ((Computation s1) . i) & I = Divide da,db & da in dom p & da <> db holds
(((Computation s1) . i) . da) div (((Computation s1) . i) . db) = (((Computation s2) . i) . da) div (((Computation s2) . i) . db)

proof end;

theorem :: AMI_5:93

for p being autonomic non programmed FinPartState of SCM
for s1, s2 being State of SCM st p c= s1 & p c= s2 holds
for i being Nat
for da, db being Data-Location
for I being Instruction of SCM st I = CurInstr ((Computation s1) . i) & I = Divide da,db & db in dom p & da <> db holds
(((Computation s1) . i) . da) mod (((Computation s1) . i) . db) = (((Computation s2) . i) . da) mod (((Computation s2) . i) . db)

proof end;

theorem :: AMI_5:94

for p being autonomic non programmed FinPartState of SCM
for s1, s2 being State of SCM st p c= s1 & p c= s2 holds
for i being Nat
for da being Data-Location
for loc being Instruction-Location of SCM
for I being Instruction of SCM st I = CurInstr ((Computation s1) . i) & I = da =0_goto loc & loc <> Next (IC ((Computation s1) . i)) holds
( ((Computation s1) . i) . da = 0 iff ((Computation s2) . i) . da = 0 )

proof end;

theorem :: AMI_5:95

for p being autonomic non programmed FinPartState of SCM
for s1, s2 being State of SCM st p c= s1 & p c= s2 holds
for i being Nat
for da being Data-Location
for loc being Instruction-Location of SCM
for I being Instruction of SCM st I = CurInstr ((Computation s1) . i) & I = da >0_goto loc & loc <> Next (IC ((Computation s1) . i)) holds
( ((Computation s1) . i) . da > 0 iff ((Computation s2) . i) . da > 0 )

proof end;

theorem :: AMI_5:96

for p being FinPartState of SCM holds DataPart p = p | SCM-Data-Loc by Lm1;

theorem :: AMI_5:97

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