let p be non NAT -defined autonomic FinPartState of SCM+FSA ; :: thesis: for s1, s2 being State of SCM+FSA st p c= s1 & p c= s2 holds
for i being Element of NAT holds
( IC (Computation s1,i) = IC (Computation s2,i) & CurInstr (Computation s1,i) = CurInstr (Computation s2,i) )
let s1, s2 be State of SCM+FSA ; :: thesis: ( p c= s1 & p c= s2 implies for i being Element of NAT holds
( IC (Computation s1,i) = IC (Computation s2,i) & CurInstr (Computation s1,i) = CurInstr (Computation s2,i) ) )
assume that
A1:
p c= s1
and
A2:
p c= s2
; :: thesis: for i being Element of NAT holds
( IC (Computation s1,i) = IC (Computation s2,i) & CurInstr (Computation s1,i) = CurInstr (Computation s2,i) )
let i be Element of NAT ; :: thesis: ( IC (Computation s1,i) = IC (Computation s2,i) & CurInstr (Computation s1,i) = CurInstr (Computation s2,i) )
set Cs1i = Computation s1,i;
set Cs2i = Computation s2,i;
thus A3:
IC (Computation s1,i) = IC (Computation s2,i)
:: thesis: CurInstr (Computation s1,i) = CurInstr (Computation s2,i)proof
assume A4:
IC (Computation s1,i) <> IC (Computation s2,i)
;
:: thesis: contradiction
(
((Computation s1,i) | (dom p)) . (IC SCM+FSA ) = (Computation s1,i) . (IC SCM+FSA ) &
((Computation s2,i) | (dom p)) . (IC SCM+FSA ) = (Computation s2,i) . (IC SCM+FSA ) )
by Th15, FUNCT_1:72;
hence
contradiction
by A1, A2, A4, AMI_1:def 25;
:: thesis: verum
end;
set I = CurInstr (Computation s1,i);
thus
CurInstr (Computation s1,i) = CurInstr (Computation s2,i)
:: thesis: verumproof
ProgramPart p c= p
by RELAT_1:88;
then A5:
dom (ProgramPart p) c= dom p
by GRFUNC_1:8;
IC (Computation s2,i) in dom (ProgramPart p)
by A2, Th17;
then A6:
((Computation s2,i) | (dom p)) . (IC (Computation s2,i)) = (Computation s2,i) . (IC (Computation s2,i))
by A5, FUNCT_1:72;
IC (Computation s1,i) in dom (ProgramPart p)
by A1, Th17;
then A7:
((Computation s1,i) | (dom p)) . (IC (Computation s1,i)) = (Computation s1,i) . (IC (Computation s1,i))
by A5, FUNCT_1:72;
assume
CurInstr (Computation s1,i) <> CurInstr (Computation s2,i)
;
:: thesis: contradiction
hence
contradiction
by A1, A2, A3, A7, A6, AMI_1:def 25;
:: thesis: verum
end;