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


begin

theorem :: SCMFSA_3:1
canceled;

theorem :: SCMFSA_3:2
canceled;

theorem :: SCMFSA_3:3
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
proofend;

theorem :: SCMFSA_3:4
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
proofend;

begin

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

registration
cluster SCM+FSA  ->  IC-recognized ;
coherence
 SCM+FSA is IC-recognized
proofend;
end;

registration
cluster SCM+FSA  ->  CurIns-recognized ;
coherence
 SCM+FSA is CurIns-recognized
proofend;
end;

theorem :: SCMFSA_3:5
for q being NAT -defined the InstructionsF of SCM+FSA -valued finite non halt-free Function
for p being non empty b1 -autonomic FinPartState of SCM+FSA
for s1, s2 being State of SCM+FSA st p c= s1 & p c= s2 holds
for P1, P2 being Instruction-Sequence of SCM+FSA st q c= P1 & q c= P2 holds
for i being Element of NAT
for da, db being Int-Location st CurInstr (P1,(Comput (P1,s1,i))) = da := db & da in dom p holds
(Comput (P1,s1,i)) . db = (Comput (P2,s2,i)) . db
proofend;

theorem :: SCMFSA_3:6
for q being NAT -defined the InstructionsF of SCM+FSA -valued finite non halt-free Function
for p being non empty b1 -autonomic FinPartState of SCM+FSA
for s1, s2 being State of SCM+FSA st p c= s1 & p c= s2 holds
for P1, P2 being Instruction-Sequence of SCM+FSA st q c= P1 & q c= P2 holds
for i being Element of NAT
for da, db being Int-Location st CurInstr (P1,(Comput (P1,s1,i))) = AddTo (da,db) & da in dom p holds
((Comput (P1,s1,i)) . da) + ((Comput (P1,s1,i)) . db) = ((Comput (P2,s2,i)) . da) + ((Comput (P2,s2,i)) . db)
proofend;

theorem :: SCMFSA_3:7
for q being NAT -defined the InstructionsF of SCM+FSA -valued finite non halt-free Function
for p being non empty b1 -autonomic FinPartState of SCM+FSA
for s1, s2 being State of SCM+FSA st p c= s1 & p c= s2 holds
for P1, P2 being Instruction-Sequence of SCM+FSA st q c= P1 & q c= P2 holds
for i being Element of NAT
for da, db being Int-Location st CurInstr (P1,(Comput (P1,s1,i))) = SubFrom (da,db) & da in dom p holds
((Comput (P1,s1,i)) . da) - ((Comput (P1,s1,i)) . db) = ((Comput (P2,s2,i)) . da) - ((Comput (P2,s2,i)) . db)
proofend;

theorem :: SCMFSA_3:8
for q being NAT -defined the InstructionsF of SCM+FSA -valued finite non halt-free Function
for p being non empty b1 -autonomic FinPartState of SCM+FSA
for s1, s2 being State of SCM+FSA st p c= s1 & p c= s2 holds
for P1, P2 being Instruction-Sequence of SCM+FSA st q c= P1 & q c= P2 holds
for i being Element of NAT
for da, db being Int-Location st CurInstr (P1,(Comput (P1,s1,i))) = MultBy (da,db) & da in dom p holds
((Comput (P1,s1,i)) . da) * ((Comput (P1,s1,i)) . db) = ((Comput (P2,s2,i)) . da) * ((Comput (P2,s2,i)) . db)
proofend;

theorem :: SCMFSA_3:9
for q being NAT -defined the InstructionsF of SCM+FSA -valued finite non halt-free Function
for p being non empty b1 -autonomic FinPartState of SCM+FSA
for s1, s2 being State of SCM+FSA st p c= s1 & p c= s2 holds
for P1, P2 being Instruction-Sequence of SCM+FSA st q c= P1 & q c= P2 holds
for i being Element of NAT
for da, db being Int-Location st CurInstr (P1,(Comput (P1,s1,i))) = Divide (da,db) &amp; da in dom p &amp; da <> db holds
((Comput (P1,s1,i)) . da) div ((Comput (P1,s1,i)) . db) = ((Comput (P2,s2,i)) . da) div ((Comput (P2,s2,i)) . db)
proofend;

theorem :: SCMFSA_3:10
for q being NAT -defined the InstructionsF of SCM+FSA -valued finite non halt-free Function
for p being non empty b1 -autonomic FinPartState of SCM+FSA
for s1, s2 being State of SCM+FSA st p c= s1 &amp; p c= s2 holds
for P1, P2 being Instruction-Sequence of SCM+FSA st q c= P1 &amp; q c= P2 holds
for i being Element of NAT
for da, db being Int-Location st CurInstr (P1,(Comput (P1,s1,i))) = Divide (da,db) &amp; db in dom p holds
((Comput (P1,s1,i)) . da) mod ((Comput (P1,s1,i)) . db) = ((Comput (P2,s2,i)) . da) mod ((Comput (P2,s2,i)) . db)
proofend;

theorem :: SCMFSA_3:11
for q being NAT -defined the InstructionsF of SCM+FSA -valued finite non halt-free Function
for p being non empty b1 -autonomic FinPartState of SCM+FSA
for s1, s2 being State of SCM+FSA st p c= s1 &amp; p c= s2 holds
for P1, P2 being Instruction-Sequence of SCM+FSA st q c= P1 &amp; q c= P2 holds
for i being Element of NAT
for da being Int-Location
for loc being Element of NAT st CurInstr (P1,(Comput (P1,s1,i))) = da =0_goto loc &amp; loc <> succ (IC (Comput (P1,s1,i))) holds
( (Comput (P1,s1,i)) . da = 0 iff (Comput (P2,s2,i)) . da = 0 )
proofend;

theorem :: SCMFSA_3:12
for q being NAT -defined the InstructionsF of SCM+FSA -valued finite non halt-free Function
for p being non empty b1 -autonomic FinPartState of SCM+FSA
for s1, s2 being State of SCM+FSA st p c= s1 &amp; p c= s2 holds
for P1, P2 being Instruction-Sequence of SCM+FSA st q c= P1 &amp; q c= P2 holds
for i being Element of NAT
for da being Int-Location
for loc being Element of NAT st CurInstr (P1,(Comput (P1,s1,i))) = da >0_goto loc &amp; loc <> succ (IC (Comput (P1,s1,i))) holds
( (Comput (P1,s1,i)) . da > 0 iff (Comput (P2,s2,i)) . da > 0 )
proofend;

theorem :: SCMFSA_3:13
for q being NAT -defined the InstructionsF of SCM+FSA -valued finite non halt-free Function
for p being non empty b1 -autonomic FinPartState of SCM+FSA
for s1, s2 being State of SCM+FSA st p c= s1 &amp; p c= s2 holds
for P1, P2 being Instruction-Sequence of SCM+FSA st q c= P1 &amp; q c= P2 holds
for i being Element of NAT
for da, db being Int-Location
for f being FinSeq-Location st CurInstr (P1,(Comput (P1,s1,i))) = da := (f,db) &amp; da in dom p holds
for k1, k2 being Element of NAT st k1 = abs ((Comput (P1,s1,i)) . db) &amp; k2 = abs ((Comput (P2,s2,i)) . db) holds
((Comput (P1,s1,i)) . f) /. k1 = ((Comput (P2,s2,i)) . f) /. k2
proofend;

theorem :: SCMFSA_3:14
for q being NAT -defined the InstructionsF of SCM+FSA -valued finite non halt-free Function
for p being non empty b1 -autonomic FinPartState of SCM+FSA
for s1, s2 being State of SCM+FSA st p c= s1 &amp; p c= s2 holds
for P1, P2 being Instruction-Sequence of SCM+FSA st q c= P1 &amp; q c= P2 holds
for i being Element of NAT
for da, db being Int-Location
for f being FinSeq-Location st CurInstr (P1,(Comput (P1,s1,i))) = (f,db) := da &amp; f in dom p holds
for k1, k2 being Element of NAT st k1 = abs ((Comput (P1,s1,i)) . db) &amp; k2 = abs ((Comput (P2,s2,i)) . db) holds
((Comput (P1,s1,i)) . f) +* (k1,((Comput (P1,s1,i)) . da)) = ((Comput (P2,s2,i)) . f) +* (k2,((Comput (P2,s2,i)) . da))
proofend;

theorem :: SCMFSA_3:15
for q being NAT -defined the InstructionsF of SCM+FSA -valued finite non halt-free Function
for p being non empty b1 -autonomic FinPartState of SCM+FSA
for s1, s2 being State of SCM+FSA st p c= s1 &amp; p c= s2 holds
for P1, P2 being Instruction-Sequence of SCM+FSA st q c= P1 &amp; q c= P2 holds
for i being Element of NAT
for da being Int-Location
for f being FinSeq-Location st CurInstr (P1,(Comput (P1,s1,i))) = da :=len f &amp; da in dom p holds
len ((Comput (P1,s1,i)) . f) = len ((Comput (P2,s2,i)) . f)
proofend;

theorem :: SCMFSA_3:16
for q being NAT -defined the InstructionsF of SCM+FSA -valued finite non halt-free Function
for p being non empty b1 -autonomic FinPartState of SCM+FSA
for s1, s2 being State of SCM+FSA st p c= s1 &amp; p c= s2 holds
for P1, P2 being Instruction-Sequence of SCM+FSA st q c= P1 &amp; q c= P2 holds
for i being Element of NAT
for da being Int-Location
for f being FinSeq-Location st CurInstr (P1,(Comput (P1,s1,i))) = f :=<0,...,0> da &amp; f in dom p holds
for k1, k2 being Element of NAT st k1 = abs ((Comput (P1,s1,i)) . da) &amp; k2 = abs ((Comput (P2,s2,i)) . da) holds
k1 |-> 0 = k2 |-> 0
proofend;