:: by Yasushi Tanaka

::

:: Received November 23, 1993

:: Copyright (c) 1993-2021 Association of Mizar Users

registration
end;

Lm1: for b being Element of Data-Locations holds b is Data-Location

proof end;

::$CT

theorem :: AMI_5:8

for ins being Instruction of SCM st InsCode ins = 1 holds

ex da, db being Data-Location st ins = da := db

ex da, db being Data-Location st ins = da := db

proof end;

theorem :: AMI_5:9

for ins being Instruction of SCM st InsCode ins = 2 holds

ex da, db being Data-Location st ins = AddTo (da,db)

ex da, db being Data-Location st ins = AddTo (da,db)

proof end;

theorem :: AMI_5:10

for ins being Instruction of SCM st InsCode ins = 3 holds

ex da, db being Data-Location st ins = SubFrom (da,db)

ex da, db being Data-Location st ins = SubFrom (da,db)

proof end;

theorem :: AMI_5:11

for ins being Instruction of SCM st InsCode ins = 4 holds

ex da, db being Data-Location st ins = MultBy (da,db)

ex da, db being Data-Location st ins = MultBy (da,db)

proof end;

theorem :: AMI_5:12

for ins being Instruction of SCM st InsCode ins = 5 holds

ex da, db being Data-Location st ins = Divide (da,db)

ex da, db being Data-Location st ins = Divide (da,db)

proof end;

theorem :: AMI_5:14

for ins being Instruction of SCM st InsCode ins = 7 holds

ex loc being Nat ex da being Data-Location st ins = da =0_goto loc

ex loc being Nat ex da being Data-Location st ins = da =0_goto loc

proof end;

theorem :: AMI_5:15

for ins being Instruction of SCM st InsCode ins = 8 holds

ex loc being Nat ex da being Data-Location st ins = da >0_goto loc

ex loc being Nat ex da being Data-Location st ins = da >0_goto loc

proof end;

theorem :: AMI_5:16

for s being State of SCM

for iloc being Nat

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

for iloc being Nat

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

proof end;

theorem :: AMI_5:17

for q being NAT -defined the InstructionsF of SCM -valued finite non halt-free Function

for p being non empty b_{1} -autonomic FinPartState of SCM

for s1, s2 being State of SCM st p c= s1 & p c= s2 holds

for P1, P2 being Instruction-Sequence of SCM st q c= P1 & q c= P2 holds

for i being Nat

for da, db being Data-Location

for I being Instruction of SCM st I = CurInstr (P1,(Comput (P1,s1,i))) & 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 st p c= s1 & p c= s2 holds

for P1, P2 being Instruction-Sequence of SCM st q c= P1 & q c= P2 holds

for i being Nat

for da, db being Data-Location

for I being Instruction of SCM st I = CurInstr (P1,(Comput (P1,s1,i))) & I = da := db & da in dom p holds

(Comput (P1,s1,i)) . db = (Comput (P2,s2,i)) . db

proof end;

theorem :: AMI_5:18

for q being NAT -defined the InstructionsF of SCM -valued finite non halt-free Function

for p being non empty b_{1} -autonomic FinPartState of SCM

for s1, s2 being State of SCM st p c= s1 & p c= s2 holds

for P1, P2 being Instruction-Sequence of SCM st q c= P1 & q c= P2 holds

for i being Nat

for da, db being Data-Location

for I being Instruction of SCM st I = CurInstr (P1,(Comput (P1,s1,i))) & 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 st p c= s1 & p c= s2 holds

for P1, P2 being Instruction-Sequence of SCM st q c= P1 & q c= P2 holds

for i being Nat

for da, db being Data-Location

for I being Instruction of SCM st I = CurInstr (P1,(Comput (P1,s1,i))) & 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 :: AMI_5:19

for q being NAT -defined the InstructionsF of SCM -valued finite non halt-free Function

for p being non empty b_{1} -autonomic FinPartState of SCM

for s1, s2 being State of SCM st p c= s1 & p c= s2 holds

for P1, P2 being Instruction-Sequence of SCM st q c= P1 & q c= P2 holds

for i being Nat

for da, db being Data-Location

for I being Instruction of SCM st I = CurInstr (P1,(Comput (P1,s1,i))) & 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 st p c= s1 & p c= s2 holds

for P1, P2 being Instruction-Sequence of SCM st q c= P1 & q c= P2 holds

for i being Nat

for da, db being Data-Location

for I being Instruction of SCM st I = CurInstr (P1,(Comput (P1,s1,i))) & 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 :: AMI_5:20

for q being NAT -defined the InstructionsF of SCM -valued finite non halt-free Function

for p being non empty b_{1} -autonomic FinPartState of SCM

for s1, s2 being State of SCM st p c= s1 & p c= s2 holds

for P1, P2 being Instruction-Sequence of SCM st q c= P1 & q c= P2 holds

for i being Nat

for da, db being Data-Location

for I being Instruction of SCM st I = CurInstr (P1,(Comput (P1,s1,i))) & 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 st p c= s1 & p c= s2 holds

for P1, P2 being Instruction-Sequence of SCM st q c= P1 & q c= P2 holds

for i being Nat

for da, db being Data-Location

for I being Instruction of SCM st I = CurInstr (P1,(Comput (P1,s1,i))) & 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 :: AMI_5:21

for q being NAT -defined the InstructionsF of SCM -valued finite non halt-free Function

for p being non empty b_{1} -autonomic FinPartState of SCM

for s1, s2 being State of SCM st p c= s1 & p c= s2 holds

for P1, P2 being Instruction-Sequence of SCM st q c= P1 & q c= P2 holds

for i being Nat

for da, db being Data-Location

for I being Instruction of SCM st I = CurInstr (P1,(Comput (P1,s1,i))) & 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 st p c= s1 & p c= s2 holds

for P1, P2 being Instruction-Sequence of SCM st q c= P1 & q c= P2 holds

for i being Nat

for da, db being Data-Location

for I being Instruction of SCM st I = CurInstr (P1,(Comput (P1,s1,i))) & 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 :: AMI_5:22

for q being NAT -defined the InstructionsF of SCM -valued finite non halt-free Function

for p being non empty b_{1} -autonomic FinPartState of SCM

for s1, s2 being State of SCM st p c= s1 & p c= s2 holds

for P1, P2 being Instruction-Sequence of SCM st q c= P1 & q c= P2 holds

for i being Nat

for da, db being Data-Location

for I being Instruction of SCM st I = CurInstr (P1,(Comput (P1,s1,i))) & 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 st p c= s1 & p c= s2 holds

for P1, P2 being Instruction-Sequence of SCM st q c= P1 & q c= P2 holds

for i being Nat

for da, db being Data-Location

for I being Instruction of SCM st I = CurInstr (P1,(Comput (P1,s1,i))) & 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 :: AMI_5:23

for q being NAT -defined the InstructionsF of SCM -valued finite non halt-free Function

for p being non empty b_{1} -autonomic FinPartState of SCM

for s1, s2 being State of SCM st p c= s1 & p c= s2 holds

for P1, P2 being Instruction-Sequence of SCM st q c= P1 & q c= P2 holds

for i being Nat

for da being Data-Location

for loc being Nat

for I being Instruction of SCM st I = CurInstr (P1,(Comput (P1,s1,i))) & 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 st p c= s1 & p c= s2 holds

for P1, P2 being Instruction-Sequence of SCM st q c= P1 & q c= P2 holds

for i being Nat

for da being Data-Location

for loc being Nat

for I being Instruction of SCM st I = CurInstr (P1,(Comput (P1,s1,i))) & 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 :: AMI_5:24

for q being NAT -defined the InstructionsF of SCM -valued finite non halt-free Function

for p being non empty b_{1} -autonomic FinPartState of SCM

for s1, s2 being State of SCM st p c= s1 & p c= s2 holds

for P1, P2 being Instruction-Sequence of SCM st q c= P1 & q c= P2 holds

for i being Nat

for da being Data-Location

for loc being Nat

for I being Instruction of SCM st I = CurInstr (P1,(Comput (P1,s1,i))) & 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 st p c= s1 & p c= s2 holds

for P1, P2 being Instruction-Sequence of SCM st q c= P1 & q c= P2 holds

for i being Nat

for da being Data-Location

for loc being Nat

for I being Instruction of SCM st I = CurInstr (P1,(Comput (P1,s1,i))) & 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 :: AMI_5:25

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

s1 = s2

s1 = s2

proof end;