:: by Andrzej Trybulec and Yatsuka Nakamura

::

:: Received February 7, 1996

:: Copyright (c) 1996-2019 Association of Mizar Users

theorem :: SCMFSA_3:3

for s being State of SCM+FSA

for iloc being Nat

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

for iloc being Nat

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

proof end;

theorem :: SCMFSA_3:4

for s being State of SCM+FSA

for iloc being Nat

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

for iloc being Nat

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

proof end;

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

end;
let a be Integer;

:: original: .-->

redefine func la .--> a -> FinPartState of SCM+FSA;

coherence

la .--> a is FinPartState of SCM+FSA

proof end;

registration
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 b_{1} -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 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

for p being non empty b

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 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

proof end;

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 b_{1} -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 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)

for p being non empty b

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 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)

proof end;

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 b_{1} -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 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)

for p being non empty b

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 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)

proof end;

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 b_{1} -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 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)

for p being non empty b

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 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)

proof end;

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 b_{1} -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 Nat

for da, db being Int-Location st CurInstr (P1,(Comput (P1,s1,i))) = Divide (da,db) & da in dom p & 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)

for p being non empty b

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 Nat

for da, db being Int-Location st CurInstr (P1,(Comput (P1,s1,i))) = Divide (da,db) & da in dom p & 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)

proof end;

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 b_{1} -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 Nat

for da, db being Int-Location st CurInstr (P1,(Comput (P1,s1,i))) = Divide (da,db) & 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)

for p being non empty b

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 Nat

for da, db being Int-Location st CurInstr (P1,(Comput (P1,s1,i))) = Divide (da,db) & 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)

proof end;

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 b_{1} -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 Nat

for da being Int-Location

for loc being Nat st CurInstr (P1,(Comput (P1,s1,i))) = da =0_goto loc & loc <> (IC (Comput (P1,s1,i))) + 1 holds

( (Comput (P1,s1,i)) . da = 0 iff (Comput (P2,s2,i)) . da = 0 )

for p being non empty b

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 Nat

for da being Int-Location

for loc being Nat st CurInstr (P1,(Comput (P1,s1,i))) = da =0_goto loc & loc <> (IC (Comput (P1,s1,i))) + 1 holds

( (Comput (P1,s1,i)) . da = 0 iff (Comput (P2,s2,i)) . da = 0 )

proof end;

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 b_{1} -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 Nat

for da being Int-Location

for loc being Nat st CurInstr (P1,(Comput (P1,s1,i))) = da >0_goto loc & loc <> (IC (Comput (P1,s1,i))) + 1 holds

( (Comput (P1,s1,i)) . da > 0 iff (Comput (P2,s2,i)) . da > 0 )

for p being non empty b

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 Nat

for da being Int-Location

for loc being Nat st CurInstr (P1,(Comput (P1,s1,i))) = da >0_goto loc & loc <> (IC (Comput (P1,s1,i))) + 1 holds

( (Comput (P1,s1,i)) . da > 0 iff (Comput (P2,s2,i)) . da > 0 )

proof end;

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 b_{1} -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 Nat

for da, db being Int-Location

for f being FinSeq-Location st CurInstr (P1,(Comput (P1,s1,i))) = da := (f,db) & da in dom p holds

for k1, k2 being Element of NAT st k1 = |.((Comput (P1,s1,i)) . db).| & k2 = |.((Comput (P2,s2,i)) . db).| holds

((Comput (P1,s1,i)) . f) /. k1 = ((Comput (P2,s2,i)) . f) /. k2

for p being non empty b

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 Nat

for da, db being Int-Location

for f being FinSeq-Location st CurInstr (P1,(Comput (P1,s1,i))) = da := (f,db) & da in dom p holds

for k1, k2 being Element of NAT st k1 = |.((Comput (P1,s1,i)) . db).| & k2 = |.((Comput (P2,s2,i)) . db).| holds

((Comput (P1,s1,i)) . f) /. k1 = ((Comput (P2,s2,i)) . f) /. k2

proof end;

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 b_{1} -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 Nat

for da, db being Int-Location

for f being FinSeq-Location st CurInstr (P1,(Comput (P1,s1,i))) = (f,db) := da & f in dom p holds

for k1, k2 being Nat st k1 = |.((Comput (P1,s1,i)) . db).| & k2 = |.((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))

for p being non empty b

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 Nat

for da, db being Int-Location

for f being FinSeq-Location st CurInstr (P1,(Comput (P1,s1,i))) = (f,db) := da & f in dom p holds

for k1, k2 being Nat st k1 = |.((Comput (P1,s1,i)) . db).| & k2 = |.((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))

proof end;

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 b_{1} -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 Nat

for da being Int-Location

for f being FinSeq-Location st CurInstr (P1,(Comput (P1,s1,i))) = da :=len f & da in dom p holds

len ((Comput (P1,s1,i)) . f) = len ((Comput (P2,s2,i)) . f)

for p being non empty b

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 Nat

for da being Int-Location

for f being FinSeq-Location st CurInstr (P1,(Comput (P1,s1,i))) = da :=len f & da in dom p holds

len ((Comput (P1,s1,i)) . f) = len ((Comput (P2,s2,i)) . f)

proof end;

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 b_{1} -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 Nat

for da being Int-Location

for f being FinSeq-Location st CurInstr (P1,(Comput (P1,s1,i))) = f :=<0,...,0> da & f in dom p holds

for k1, k2 being Nat st k1 = |.((Comput (P1,s1,i)) . da).| & k2 = |.((Comput (P2,s2,i)) . da).| holds

k1 |-> 0 = k2 |-> 0

for p being non empty b

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 Nat

for da being Int-Location

for f being FinSeq-Location st CurInstr (P1,(Comput (P1,s1,i))) = f :=<0,...,0> da & f in dom p holds

for k1, k2 being Nat st k1 = |.((Comput (P1,s1,i)) . da).| & k2 = |.((Comput (P2,s2,i)) . da).| holds

k1 |-> 0 = k2 |-> 0

proof end;