:: SCMFSA_3 semantic presentation

theorem Th1: :: SCMFSA_3:1

not IC SCM+FSA in Int-Locations

proof end;

theorem Th2: :: SCMFSA_3:2

not IC SCM+FSA in FinSeq-Locations

proof end;

theorem :: SCMFSA_3:3

for i being Instruction of SCM+FSA
for I being Instruction of SCM st i = I holds
for s being State of SCM+FSA
for S being State of SCM st S = (s | the carrier of SCM ) +* (the Instruction-Locations of SCM --> I) holds
Exec i,s = (s +* (Exec I,S)) +* (s | the Instruction-Locations of SCM+FSA ) by AMI_3:def 1, SCMFSA_2:75, SCMFSA_2:def 1;

theorem Th4: :: SCMFSA_3:4

for s1, s2 being State of SCM+FSA st s1 | ((Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )}) = s2 | ((Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )}) holds
for l being Instruction of SCM+FSA holds (Exec l,s1) | ((Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )}) = (Exec l,s2) | ((Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )})

proof end;

theorem Th5: :: SCMFSA_3:5

for N being with_non-empty_elements set
for S being non empty non void steady-programmed AMI-Struct of N
for i being Instruction of S
for s being State of S holds (Exec i,s) | the Instruction-Locations of S = s | the Instruction-Locations of S

proof end;

theorem Th6: :: SCMFSA_3:6

for p being FinPartState of SCM+FSA holds DataPart p = p | (Int-Locations \/ FinSeq-Locations )

proof end;

theorem :: SCMFSA_3:7

for p being FinPartState of SCM+FSA holds
( p is data-only iff dom p c= Int-Locations \/ FinSeq-Locations )

proof end;

theorem :: SCMFSA_3:8

for p being FinPartState of SCM+FSA holds dom (DataPart p) c= Int-Locations \/ FinSeq-Locations

proof end;

theorem :: SCMFSA_3:9

canceled;

theorem :: SCMFSA_3:10

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

proof end;

theorem :: SCMFSA_3:11

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

proof end;

theorem :: SCMFSA_3:12

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

proof end;

theorem :: SCMFSA_3:13

for s, t being State of SCM+FSA holds s +* (t | (Int-Locations \/ FinSeq-Locations )) is State of SCM+FSA

proof end;

definition

let la be Int-Location ;
let a be Integer;
:: original: .-->
redefine func la .--> a -> FinPartState of SCM+FSA ;
coherence

proof end;

end;

theorem Th14: :: SCMFSA_3:14

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

proof end;

registration

cluster autonomic non programmed FinPartState of SCM+FSA ;
existence

proof end;

end;

theorem Th15: :: SCMFSA_3:15

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

proof end;

theorem :: SCMFSA_3:16

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

proof end;

theorem Th17: :: SCMFSA_3:17

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

proof end;

theorem Th18: :: SCMFSA_3:18

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

proof end;

theorem :: SCMFSA_3:19

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

proof end;

theorem :: SCMFSA_3:20

for p being autonomic non programmed FinPartState of SCM+FSA
for s1, s2 being State of SCM+FSA st p c= s1 & p c= s2 holds
for i being Nat
for da, db being Int-Location st CurInstr ((Computation s1) . 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 :: SCMFSA_3:21

for p being autonomic non programmed FinPartState of SCM+FSA
for s1, s2 being State of SCM+FSA st p c= s1 & p c= s2 holds
for i being Nat
for da, db being Int-Location st CurInstr ((Computation s1) . 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 :: SCMFSA_3:22

for p being autonomic non programmed FinPartState of SCM+FSA
for s1, s2 being State of SCM+FSA st p c= s1 & p c= s2 holds
for i being Nat
for da, db being Int-Location st CurInstr ((Computation s1) . 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 :: SCMFSA_3:23

for p being autonomic non programmed FinPartState of SCM+FSA
for s1, s2 being State of SCM+FSA st p c= s1 & p c= s2 holds
for i being Nat
for da, db being Int-Location st CurInstr ((Computation s1) . 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 :: SCMFSA_3:24

for p being autonomic non programmed FinPartState of SCM+FSA
for s1, s2 being State of SCM+FSA st p c= s1 & p c= s2 holds
for i being Nat
for da, db being Int-Location st CurInstr ((Computation s1) . 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 :: SCMFSA_3:25

for p being autonomic non programmed FinPartState of SCM+FSA
for s1, s2 being State of SCM+FSA st p c= s1 & p c= s2 holds
for i being Nat
for da being Int-Location
for loc being Instruction-Location of SCM+FSA st CurInstr ((Computation s1) . 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 :: SCMFSA_3:26

for p being autonomic non programmed FinPartState of SCM+FSA
for s1, s2 being State of SCM+FSA st p c= s1 & p c= s2 holds
for i being Nat
for da being Int-Location
for loc being Instruction-Location of SCM+FSA st CurInstr ((Computation s1) . 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 :: SCMFSA_3:27

for p being autonomic non programmed FinPartState of SCM+FSA
for s1, s2 being State of SCM+FSA st p c= s1 & p c= s2 holds
for i being Nat
for da, db being Int-Location
for f being FinSeq-Location st CurInstr ((Computation s1) . i) = da := f,db & da in dom p holds
for k1, k2 being Nat st k1 = abs (((Computation s1) . i) . db) & k2 = abs (((Computation s2) . i) . db) holds
(((Computation s1) . i) . f) /. k1 = (((Computation s2) . i) . f) /. k2

proof end;

theorem :: SCMFSA_3:28

for p being autonomic non programmed FinPartState of SCM+FSA
for s1, s2 being State of SCM+FSA st p c= s1 & p c= s2 holds
for i being Nat
for da, db being Int-Location
for f being FinSeq-Location st CurInstr ((Computation s1) . i) = f,db := da & f in dom p holds
for k1, k2 being Nat st k1 = abs (((Computation s1) . i) . db) & k2 = abs (((Computation s2) . i) . db) holds
(((Computation s1) . i) . f) +* k1,(((Computation s1) . i) . da) = (((Computation s2) . i) . f) +* k2,(((Computation s2) . i) . da)

proof end;

theorem :: SCMFSA_3:29

for p being autonomic non programmed FinPartState of SCM+FSA
for s1, s2 being State of SCM+FSA st p c= s1 & p c= s2 holds
for i being Nat
for da being Int-Location
for f being FinSeq-Location st CurInstr ((Computation s1) . i) = da :=len f & da in dom p holds
len (((Computation s1) . i) . f) = len (((Computation s2) . i) . f)

proof end;

theorem :: SCMFSA_3:30

for p being autonomic non programmed FinPartState of SCM+FSA
for s1, s2 being State of SCM+FSA st p c= s1 & p c= s2 holds
for i being Nat
for da being Int-Location
for f being FinSeq-Location st CurInstr ((Computation s1) . i) = f :=<0,...,0> da & f in dom p holds
for k1, k2 being Nat st k1 = abs (((Computation s1) . i) . da) & k2 = abs (((Computation s2) . i) . da) holds
k1 |-> 0 = k2 |-> 0

proof end;