let n be 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 b1) -valued finite non halt-free Function
for p being non empty b8 -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)
let R be 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 R) -valued finite non halt-free Function
for p being non empty b7 -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)
let a, b be 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 R) -valued finite non halt-free Function
for p being non empty b5 -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)
let s1, s2 be State of (SCM R); for P1, P2 being Instruction-Sequence of (SCM R)
for q being NAT -defined the InstructionsF of (SCM R) -valued finite non halt-free Function
for p being non empty b3 -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)
let P1, P2 be Instruction-Sequence of (SCM R); for q being NAT -defined the InstructionsF of (SCM R) -valued finite non halt-free Function
for p being non empty b1 -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)
set Cs2i1 = Comput (P2,s2,(n + 1));
set Cs1i1 = Comput (P1,s1,(n + 1));
set Cs2i = Comput (P2,s2,n);
set Cs1i = Comput (P1,s1,n);
set I = CurInstr (P1,(Comput (P1,s1,n)));
let q be NAT -defined the InstructionsF of (SCM R) -valued finite non halt-free Function; for p being non empty q -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)
let p be non empty q -autonomic FinPartState of (SCM R); ( 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 implies ((Comput (P1,s1,n)) . a) * ((Comput (P1,s1,n)) . b) = ((Comput (P2,s2,n)) . a) * ((Comput (P2,s2,n)) . b) )
assume that
A1:
( p c= s1 & p c= s2 )
and
A2:
( q c= P1 & q c= P2 )
; ( not CurInstr (P1,(Comput (P1,s1,n))) = MultBy (a,b) or not a in dom p or ((Comput (P1,s1,n)) . a) * ((Comput (P1,s1,n)) . b) = ((Comput (P2,s2,n)) . a) * ((Comput (P2,s2,n)) . b) )
A3:
( a in dom p implies ( ((Comput (P1,s1,(n + 1))) | (dom p)) . a = (Comput (P1,s1,(n + 1))) . a & ((Comput (P2,s2,(n + 1))) | (dom p)) . a = (Comput (P2,s2,(n + 1))) . a ) )
by FUNCT_1:49;
A4: Comput (P2,s2,(n + 1)) =
Following (P2,(Comput (P2,s2,n)))
by EXTPRO_1:3
.=
Exec ((CurInstr (P2,(Comput (P2,s2,n)))),(Comput (P2,s2,n)))
;
assume that
A5:
CurInstr (P1,(Comput (P1,s1,n))) = MultBy (a,b)
and
A6:
( a in dom p & ((Comput (P1,s1,n)) . a) * ((Comput (P1,s1,n)) . b) <> ((Comput (P2,s2,n)) . a) * ((Comput (P2,s2,n)) . b) )
; contradiction
Comput (P1,s1,(n + 1)) =
Following (P1,(Comput (P1,s1,n)))
by EXTPRO_1:3
.=
Exec ((CurInstr (P1,(Comput (P1,s1,n)))),(Comput (P1,s1,n)))
;
then A7:
(Comput (P1,s1,(n + 1))) . a = ((Comput (P1,s1,n)) . a) * ((Comput (P1,s1,n)) . b)
by A5, SCMRING2:14;
CurInstr (P1,(Comput (P1,s1,n))) = CurInstr (P2,(Comput (P2,s2,n)))
by A1, A2, AMISTD_5:7;
then
(Comput (P2,s2,(n + 1))) . a = ((Comput (P2,s2,n)) . a) * ((Comput (P2,s2,n)) . b)
by A4, A5, SCMRING2:14;
hence
contradiction
by A1, A3, A6, A7, A2, EXTPRO_1:def 10; verum