let s1, s2 be State of ; :: thesis: for I being parahalting Program of st Initialized (stop I) c= s1 & Initialized (stop I) c= s2 & s1,s2 equal_outside NAT holds
for k being Element of NAT holds
( Computation s1,k, Computation s2,k equal_outside NAT & CurInstr (Computation s1,k) = CurInstr (Computation s2,k) )
let I be parahalting Program of ; :: thesis: ( Initialized (stop I) c= s1 & Initialized (stop I) c= s2 & s1,s2 equal_outside NAT implies for k being Element of NAT holds
( Computation s1,k, Computation s2,k equal_outside NAT & CurInstr (Computation s1,k) = CurInstr (Computation s2,k) ) )
set SI = stop I;
assume that
A1: Initialized (stop I) c= s1 and
A2: Initialized (stop I) c= s2 and
A3: s1,s2 equal_outside NAT ; :: thesis: for k being Element of NAT holds
( Computation s1,k, Computation s2,k equal_outside NAT & CurInstr (Computation s1,k) = CurInstr (Computation s2,k) )
A4: stop I c= s2 by A2, SCMPDS_4:57;
A5: stop I c= s1 by A1, SCMPDS_4:57;

hereby :: thesis: verum

let k be Element of NAT ; :: thesis: ( Computation s1,k, Computation s2,k equal_outside NAT & CurInstr (Computation s2,k) = CurInstr (Computation s1,k) )
A6: IC (Computation s1,k) in dom (stop I) by A1, SCMPDS_4:def 9;
A7: IC (Computation s2,k) in dom (stop I) by A2, SCMPDS_4:def 9;
for m being Element of NAT st m < k holds
IC (Computation s2,m) in dom (stop I) by A2, SCMPDS_4:def 9;
hence Computation s1,k, Computation s2,k equal_outside NAT by A3, A5, A4, SCMPDS_4:67; :: thesis: CurInstr (Computation s2,k) = CurInstr (Computation s1,k)
then A8: IC (Computation s1,k) = IC (Computation s2,k) by AMI_1:121;
thus CurInstr (Computation s2,k) = s2 . (IC (Computation s2,k)) by AMI_1:54
.= (stop I) . (IC (Computation s2,k)) by A4, A7, GRFUNC_1:8
.= s1 . (IC (Computation s1,k)) by A5, A8, A6, GRFUNC_1:8
.= CurInstr (Computation s1,k) by AMI_1:54 ; :: thesis: verum

end;