let N be with_zero set ; for S being non empty with_non-empty_values IC-Ins-separated halting IC-recognized CurIns-recognized AMI-Struct over N
for q being NAT -defined the InstructionsF of b1 -valued finite non halt-free Function
for p being non empty b2 -autonomic FinPartState of S
for s1, s2 being State of S st p c= s1 & p c= s2 holds
for P1, P2 being Instruction-Sequence of S st q c= P1 & q c= P2 holds
for i being Nat holds
( IC (Comput (P1,s1,i)) = IC (Comput (P2,s2,i)) & CurInstr (P1,(Comput (P1,s1,i))) = CurInstr (P2,(Comput (P2,s2,i))) )
let S be non empty with_non-empty_values IC-Ins-separated halting IC-recognized CurIns-recognized AMI-Struct over N; for q being NAT -defined the InstructionsF of S -valued finite non halt-free Function
for p being non empty b1 -autonomic FinPartState of S
for s1, s2 being State of S st p c= s1 & p c= s2 holds
for P1, P2 being Instruction-Sequence of S st q c= P1 & q c= P2 holds
for i being Nat holds
( IC (Comput (P1,s1,i)) = IC (Comput (P2,s2,i)) & CurInstr (P1,(Comput (P1,s1,i))) = CurInstr (P2,(Comput (P2,s2,i))) )
let q be NAT -defined the InstructionsF of S -valued finite non halt-free Function; for p being non empty q -autonomic FinPartState of S
for s1, s2 being State of S st p c= s1 & p c= s2 holds
for P1, P2 being Instruction-Sequence of S st q c= P1 & q c= P2 holds
for i being Nat holds
( IC (Comput (P1,s1,i)) = IC (Comput (P2,s2,i)) & CurInstr (P1,(Comput (P1,s1,i))) = CurInstr (P2,(Comput (P2,s2,i))) )
let p be non empty q -autonomic FinPartState of S; for s1, s2 being State of S st p c= s1 & p c= s2 holds
for P1, P2 being Instruction-Sequence of S st q c= P1 & q c= P2 holds
for i being Nat holds
( IC (Comput (P1,s1,i)) = IC (Comput (P2,s2,i)) & CurInstr (P1,(Comput (P1,s1,i))) = CurInstr (P2,(Comput (P2,s2,i))) )
let s1, s2 be State of S; ( p c= s1 & p c= s2 implies for P1, P2 being Instruction-Sequence of S st q c= P1 & q c= P2 holds
for i being Nat holds
( IC (Comput (P1,s1,i)) = IC (Comput (P2,s2,i)) & CurInstr (P1,(Comput (P1,s1,i))) = CurInstr (P2,(Comput (P2,s2,i))) ) )
assume that
A1:
p c= s1
and
A2:
p c= s2
; for P1, P2 being Instruction-Sequence of S st q c= P1 & q c= P2 holds
for i being Nat holds
( IC (Comput (P1,s1,i)) = IC (Comput (P2,s2,i)) & CurInstr (P1,(Comput (P1,s1,i))) = CurInstr (P2,(Comput (P2,s2,i))) )
let P1, P2 be Instruction-Sequence of S; ( q c= P1 & q c= P2 implies for i being Nat holds
( IC (Comput (P1,s1,i)) = IC (Comput (P2,s2,i)) & CurInstr (P1,(Comput (P1,s1,i))) = CurInstr (P2,(Comput (P2,s2,i))) ) )
assume that
A3:
q c= P1
and
A4:
q c= P2
; for i being Nat holds
( IC (Comput (P1,s1,i)) = IC (Comput (P2,s2,i)) & CurInstr (P1,(Comput (P1,s1,i))) = CurInstr (P2,(Comput (P2,s2,i))) )
A5:
dom q c= dom P1
by A3, RELAT_1:11;
A6:
dom q c= dom P2
by A4, RELAT_1:11;
let i be Nat; ( IC (Comput (P1,s1,i)) = IC (Comput (P2,s2,i)) & CurInstr (P1,(Comput (P1,s1,i))) = CurInstr (P2,(Comput (P2,s2,i))) )
set Cs2i = Comput (P2,s2,i);
set Cs1i = Comput (P1,s1,i);
A7:
IC (Comput (P1,s1,i)) in dom q
by A3, Def4, A1;
A8:
IC (Comput (P2,s2,i)) in dom q
by A4, Def4, A2;
thus A9:
IC (Comput (P1,s1,i)) = IC (Comput (P2,s2,i))
CurInstr (P1,(Comput (P1,s1,i))) = CurInstr (P2,(Comput (P2,s2,i)))proof
assume A10:
IC (Comput (P1,s1,i)) <> IC (Comput (P2,s2,i))
;
contradiction
(
((Comput (P1,s1,i)) | (dom p)) . (IC ) = (Comput (P1,s1,i)) . (IC ) &
((Comput (P2,s2,i)) | (dom p)) . (IC ) = (Comput (P2,s2,i)) . (IC ) )
by Th6, FUNCT_1:49;
hence
contradiction
by A10, A3, A4, A1, A2, EXTPRO_1:def 10;
verum
end;
thus CurInstr (P1,(Comput (P1,s1,i))) =
P1 . (IC (Comput (P1,s1,i)))
by A7, A5, PARTFUN1:def 6
.=
q . (IC (Comput (P1,s1,i)))
by A7, A3, GRFUNC_1:2
.=
P2 . (IC (Comput (P2,s2,i)))
by A8, A4, A9, GRFUNC_1:2
.=
CurInstr (P2,(Comput (P2,s2,i)))
by A8, A6, PARTFUN1:def 6
; verum