:: Computation in { \bf SCM_FSA }
:: by Andrzej Trybulec and Yatsuka Nakamura
::
:: Received February 7, 1996
:: Copyright (c) 1996 Association of Mizar Users

begin

theorem :: SCMFSA_3:1

not IC SCM+FSA in Int-Locations

proof end;

theorem :: 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) +* (NAT --> I) holds
Exec (i,s) = (s +* (Exec (I,S))) +* (s | NAT) by SCMFSA_2:75;

theorem :: 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;

begin

definition

let s be State of SCM+FSA;
let p be preProgram of SCM+FSA;
:: original: +*
redefine func s +* p -> State of SCM+FSA;
coherence
s +* p is State of SCM+FSA ;

end;

theorem :: SCMFSA_3:5

canceled;

theorem :: SCMFSA_3:6

canceled;

theorem :: SCMFSA_3:7

canceled;

theorem :: SCMFSA_3:8

canceled;

theorem :: SCMFSA_3:9

canceled;

theorem :: SCMFSA_3:10

canceled;

theorem :: SCMFSA_3:11

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

proof end;

theorem :: SCMFSA_3:12

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

proof end;

begin

definition

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

proof end;

end;

theorem :: SCMFSA_3:13

canceled;

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;

theorem Th15: :: SCMFSA_3:15

for p being non NAT -defined autonomic FinPartState of 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 non NAT -defined autonomic FinPartState of
for s being State of SCM+FSA st p c= s holds
for i being Element of NAT holds IC (Comput ((ProgramPart s),s,i)) in dom (ProgramPart p)

proof end;

theorem Th18: :: SCMFSA_3:18

for p being non NAT -defined autonomic FinPartState of
for s1, s2 being State of SCM+FSA st p c= s1 & p c= s2 holds
for i being Element of NAT holds
( IC (Comput ((ProgramPart s1),s1,i)) = IC (Comput ((ProgramPart s2),s2,i)) & CurInstr ((ProgramPart s1),(Comput ((ProgramPart s1),s1,i))) = CurInstr ((ProgramPart s2),(Comput ((ProgramPart s2),s2,i))) )

proof end;

theorem :: SCMFSA_3:19

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

proof end;

theorem :: SCMFSA_3:20

for p being non NAT -defined autonomic FinPartState of
for s1, s2 being State of SCM+FSA st p c= s1 & p c= s2 holds
for i being Element of NAT
for da, db being Int-Location st CurInstr ((ProgramPart s1),(Comput ((ProgramPart s1),s1,i))) = AddTo (da,db) & da in dom p holds
((Comput ((ProgramPart s1),s1,i)) . da) + ((Comput ((ProgramPart s1),s1,i)) . db) = ((Comput ((ProgramPart s2),s2,i)) . da) + ((Comput ((ProgramPart s2),s2,i)) . db)

proof end;

theorem :: SCMFSA_3:21

for p being non NAT -defined autonomic FinPartState of
for s1, s2 being State of SCM+FSA st p c= s1 & p c= s2 holds
for i being Element of NAT
for da, db being Int-Location st CurInstr ((ProgramPart s1),(Comput ((ProgramPart s1),s1,i))) = SubFrom (da,db) & da in dom p holds
((Comput ((ProgramPart s1),s1,i)) . da) - ((Comput ((ProgramPart s1),s1,i)) . db) = ((Comput ((ProgramPart s2),s2,i)) . da) - ((Comput ((ProgramPart s2),s2,i)) . db)

proof end;

theorem :: SCMFSA_3:22

for p being non NAT -defined autonomic FinPartState of
for s1, s2 being State of SCM+FSA st p c= s1 & p c= s2 holds
for i being Element of NAT
for da, db being Int-Location st CurInstr ((ProgramPart s1),(Comput ((ProgramPart s1),s1,i))) = MultBy (da,db) & da in dom p holds
((Comput ((ProgramPart s1),s1,i)) . da) * ((Comput ((ProgramPart s1),s1,i)) . db) = ((Comput ((ProgramPart s2),s2,i)) . da) * ((Comput ((ProgramPart s2),s2,i)) . db)

proof end;

theorem :: SCMFSA_3:23

for p being non NAT -defined autonomic FinPartState of
for s1, s2 being State of SCM+FSA st p c= s1 & p c= s2 holds
for i being Element of NAT
for da, db being Int-Location st CurInstr ((ProgramPart s1),(Comput ((ProgramPart s1),s1,i))) = Divide (da,db) & da in dom p & da <> db holds
((Comput ((ProgramPart s1),s1,i)) . da) div ((Comput ((ProgramPart s1),s1,i)) . db) = ((Comput ((ProgramPart s2),s2,i)) . da) div ((Comput ((ProgramPart s2),s2,i)) . db)

proof end;

theorem :: SCMFSA_3:24

for p being non NAT -defined autonomic FinPartState of
for s1, s2 being State of SCM+FSA st p c= s1 & p c= s2 holds
for i being Element of NAT
for da, db being Int-Location st CurInstr ((ProgramPart s1),(Comput ((ProgramPart s1),s1,i))) = Divide (da,db) & db in dom p holds
((Comput ((ProgramPart s1),s1,i)) . da) mod ((Comput ((ProgramPart s1),s1,i)) . db) = ((Comput ((ProgramPart s2),s2,i)) . da) mod ((Comput ((ProgramPart s2),s2,i)) . db)

proof end;

theorem :: SCMFSA_3:25

for p being non NAT -defined autonomic FinPartState of
for s1, s2 being State of SCM+FSA st p c= s1 & p c= s2 holds
for i being Element of NAT
for da being Int-Location
for loc being Element of NAT st CurInstr ((ProgramPart s1),(Comput ((ProgramPart s1),s1,i))) = da =0_goto loc & loc <> succ (IC (Comput ((ProgramPart s1),s1,i))) holds
( (Comput ((ProgramPart s1),s1,i)) . da = 0 iff (Comput ((ProgramPart s2),s2,i)) . da = 0 )

proof end;

theorem :: SCMFSA_3:26

for p being non NAT -defined autonomic FinPartState of
for s1, s2 being State of SCM+FSA st p c= s1 & p c= s2 holds
for i being Element of NAT
for da being Int-Location
for loc being Element of NAT st CurInstr ((ProgramPart s1),(Comput ((ProgramPart s1),s1,i))) = da >0_goto loc & loc <> succ (IC (Comput ((ProgramPart s1),s1,i))) holds
( (Comput ((ProgramPart s1),s1,i)) . da > 0 iff (Comput ((ProgramPart s2),s2,i)) . da > 0 )

proof end;

theorem :: SCMFSA_3:27

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

proof end;

theorem :: SCMFSA_3:28

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

proof end;

theorem :: SCMFSA_3:29

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

proof end;

theorem :: SCMFSA_3:30

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

proof end;