:: by Artur Korni{\l}owicz and Yasunari Shidama

::

:: Received February 6, 2004

:: Copyright (c) 2004-2016 Association of Mizar Users

theorem Th5: :: SCMRING4:5

for R being non trivial Ring

for a being Data-Location of R

for loc being Nat

for s being State of (SCM R) holds s . a = (s +* (Start-At (loc,(SCM R)))) . a

for a being Data-Location of R

for loc being Nat

for s being State of (SCM R) holds s . a = (s +* (Start-At (loc,(SCM R)))) . a

proof end;

theorem Th6: :: SCMRING4:6

for R being non trivial Ring

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

s1 = s2

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

s1 = s2

proof end;

registration
end;

definition

let R be non trivial Ring;

let a be Data-Location of R;

let r be Element of R;

:: original: .-->

redefine func a .--> r -> FinPartState of (SCM R);

coherence

a .--> r is FinPartState of (SCM R)

end;
let a be Data-Location of R;

let r be Element of R;

:: original: .-->

redefine func a .--> r -> FinPartState of (SCM R);

coherence

a .--> r is FinPartState of (SCM R)

proof end;

theorem Th7: :: SCMRING4:7

for n being Nat

for R being non trivial Ring

for a, b being Data-Location of R

for s1, s2 being State of (SCM R)

for P1, P2 being Instruction-Sequence of (SCM R)

for q being NAT -defined the InstructionsF of (SCM b_{2}) -valued finite non halt-free Function

for p being non empty b_{9} -autonomic FinPartState of (SCM R) st p c= s1 & p c= s2 & q c= P1 & q c= P2 & CurInstr (P1,(Comput (P1,s1,n))) = a := b & a in dom p holds

(Comput (P1,s1,n)) . b = (Comput (P2,s2,n)) . b

for R being non trivial Ring

for a, b being Data-Location of R

for s1, s2 being State of (SCM R)

for P1, P2 being Instruction-Sequence of (SCM R)

for q being NAT -defined the InstructionsF of (SCM b

for p being non empty b

(Comput (P1,s1,n)) . b = (Comput (P2,s2,n)) . b

proof end;

theorem Th8: :: SCMRING4:8

for n being Nat

for R being non trivial Ring

for a, b being Data-Location of R

for s1, s2 being State of (SCM R)

for P1, P2 being Instruction-Sequence of (SCM R)

for q being NAT -defined the InstructionsF of (SCM b_{2}) -valued finite non halt-free Function

for p being non empty b_{9} -autonomic FinPartState of (SCM R) st p c= s1 & p c= s2 & q c= P1 & q c= P2 & CurInstr (P1,(Comput (P1,s1,n))) = AddTo (a,b) & a in dom p holds

((Comput (P1,s1,n)) . a) + ((Comput (P1,s1,n)) . b) = ((Comput (P2,s2,n)) . a) + ((Comput (P2,s2,n)) . b)

for R being non trivial Ring

for a, b being Data-Location of R

for s1, s2 being State of (SCM R)

for P1, P2 being Instruction-Sequence of (SCM R)

for q being NAT -defined the InstructionsF of (SCM b

for p being non empty b

((Comput (P1,s1,n)) . a) + ((Comput (P1,s1,n)) . b) = ((Comput (P2,s2,n)) . a) + ((Comput (P2,s2,n)) . b)

proof end;

theorem Th9: :: SCMRING4:9

for n being Nat

for R being non trivial Ring

for a, b being Data-Location of R

for s1, s2 being State of (SCM R)

for P1, P2 being Instruction-Sequence of (SCM R)

for q being NAT -defined the InstructionsF of (SCM b_{2}) -valued finite non halt-free Function

for p being non empty b_{9} -autonomic FinPartState of (SCM R) st p c= s1 & p c= s2 & q c= P1 & q c= P2 & CurInstr (P1,(Comput (P1,s1,n))) = SubFrom (a,b) & a in dom p holds

((Comput (P1,s1,n)) . a) - ((Comput (P1,s1,n)) . b) = ((Comput (P2,s2,n)) . a) - ((Comput (P2,s2,n)) . b)

for R being non trivial Ring

for a, b being Data-Location of R

for s1, s2 being State of (SCM R)

for P1, P2 being Instruction-Sequence of (SCM R)

for q being NAT -defined the InstructionsF of (SCM b

for p being non empty b

((Comput (P1,s1,n)) . a) - ((Comput (P1,s1,n)) . b) = ((Comput (P2,s2,n)) . a) - ((Comput (P2,s2,n)) . b)

proof end;

theorem Th10: :: SCMRING4:10

for n being Nat

for R being non trivial Ring

for a, b being Data-Location of R

for s1, s2 being State of (SCM R)

for P1, P2 being Instruction-Sequence of (SCM R)

for q being NAT -defined the InstructionsF of (SCM b_{2}) -valued finite non halt-free Function

for p being non empty b_{9} -autonomic FinPartState of (SCM R) st p c= s1 & p c= s2 & q c= P1 & q c= P2 & CurInstr (P1,(Comput (P1,s1,n))) = MultBy (a,b) & a in dom p holds

((Comput (P1,s1,n)) . a) * ((Comput (P1,s1,n)) . b) = ((Comput (P2,s2,n)) . a) * ((Comput (P2,s2,n)) . b)

for R being non trivial Ring

for a, b being Data-Location of R

for s1, s2 being State of (SCM R)

for P1, P2 being Instruction-Sequence of (SCM R)

for q being NAT -defined the InstructionsF of (SCM b

for p being non empty b

((Comput (P1,s1,n)) . a) * ((Comput (P1,s1,n)) . b) = ((Comput (P2,s2,n)) . a) * ((Comput (P2,s2,n)) . b)

proof end;

theorem Th11: :: SCMRING4:11

for n being Nat

for R being non trivial Ring

for a being Data-Location of R

for loc being Nat

for s1, s2 being State of (SCM R)

for P1, P2 being Instruction-Sequence of (SCM R)

for q being NAT -defined the InstructionsF of (SCM b_{2}) -valued finite non halt-free Function

for p being non empty b_{9} -autonomic FinPartState of (SCM R) st p c= s1 & p c= s2 & q c= P1 & q c= P2 & CurInstr (P1,(Comput (P1,s1,n))) = a =0_goto loc & loc <> (IC (Comput (P1,s1,n))) + 1 holds

( (Comput (P1,s1,n)) . a = 0. R iff (Comput (P2,s2,n)) . a = 0. R )

for R being non trivial Ring

for a being Data-Location of R

for loc being Nat

for s1, s2 being State of (SCM R)

for P1, P2 being Instruction-Sequence of (SCM R)

for q being NAT -defined the InstructionsF of (SCM b

for p being non empty b

( (Comput (P1,s1,n)) . a = 0. R iff (Comput (P2,s2,n)) . a = 0. R )

proof end;

theorem Th12: :: SCMRING4:12

for k being Nat

for R being non trivial Ring

for s1, s2 being State of (SCM R)

for q being NAT -defined the InstructionsF of (SCM b_{2}) -valued finite non halt-free Function

for p being non empty b_{5} -autonomic FinPartState of (SCM R) st p c= s1 & IncIC (p,k) c= s2 holds

for P1, P2 being Instruction-Sequence of (SCM R) st q c= P1 & Reloc (q,k) c= P2 holds

for i being Nat holds

( (IC (Comput (P1,s1,i))) + k = IC (Comput (P2,s2,i)) & IncAddr ((CurInstr (P1,(Comput (P1,s1,i)))),k) = CurInstr (P2,(Comput (P2,s2,i))) & (Comput (P1,s1,i)) | (dom (DataPart p)) = (Comput (P2,s2,i)) | (dom (DataPart p)) & DataPart (Comput (P1,(s1 +* (DataPart s2)),i)) = DataPart (Comput (P2,s2,i)) )

for R being non trivial Ring

for s1, s2 being State of (SCM R)

for q being NAT -defined the InstructionsF of (SCM b

for p being non empty b

for P1, P2 being Instruction-Sequence of (SCM R) st q c= P1 & Reloc (q,k) c= P2 holds

for i being Nat holds

( (IC (Comput (P1,s1,i))) + k = IC (Comput (P2,s2,i)) & IncAddr ((CurInstr (P1,(Comput (P1,s1,i)))),k) = CurInstr (P2,(Comput (P2,s2,i))) & (Comput (P1,s1,i)) | (dom (DataPart p)) = (Comput (P2,s2,i)) | (dom (DataPart p)) & DataPart (Comput (P1,(s1 +* (DataPart s2)),i)) = DataPart (Comput (P2,s2,i)) )

proof end;

registration
end;