let s1, s2 be State of SCM+FSA; :: thesis: for p1, p2 being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for I being InitHalting Program of SCM+FSA st Initialized I c= s1 & Initialized I c= s2 & I c= p1 & I c= p2 & s1,s2 equal_outside NAT holds
for k being Element of NAT holds
( Comput (p1,s1,k), Comput (p2,s2,k) equal_outside NAT & CurInstr (p1,(Comput (p1,s1,k))) = CurInstr (p2,(Comput (p2,s2,k))) )
let p1, p2 be the Instructions of SCM+FSA -valued ManySortedSet of NAT ; :: thesis: for I being InitHalting Program of SCM+FSA st Initialized I c= s1 & Initialized I c= s2 & I c= p1 & I c= p2 & s1,s2 equal_outside NAT holds
for k being Element of NAT holds
( Comput (p1,s1,k), Comput (p2,s2,k) equal_outside NAT & CurInstr (p1,(Comput (p1,s1,k))) = CurInstr (p2,(Comput (p2,s2,k))) )
let I be InitHalting Program of SCM+FSA; :: thesis: ( Initialized I c= s1 & Initialized I c= s2 & I c= p1 & I c= p2 & s1,s2 equal_outside NAT implies for k being Element of NAT holds
( Comput (p1,s1,k), Comput (p2,s2,k) equal_outside NAT & CurInstr (p1,(Comput (p1,s1,k))) = CurInstr (p2,(Comput (p2,s2,k))) ) )
assume that
A1: Initialized I c= s1 and
A2: Initialized I c= s2 and
A3: I c= p1 and
A4: I c= p2 and
A5: s1,s2 equal_outside NAT ; :: thesis: for k being Element of NAT holds
( Comput (p1,s1,k), Comput (p2,s2,k) equal_outside NAT & CurInstr (p1,(Comput (p1,s1,k))) = CurInstr (p2,(Comput (p2,s2,k))) )
let k be Element of NAT ; :: thesis: ( Comput (p1,s1,k), Comput (p2,s2,k) equal_outside NAT & CurInstr (p1,(Comput (p1,s1,k))) = CurInstr (p2,(Comput (p2,s2,k))) )
A6: IC (Comput (p1,s1,k)) in dom I by A1, Def1, A3;
A7: IC (Comput (p2,s2,k)) in dom I by A2, Def1, A4;
for m being Element of NAT st m < k holds
IC (Comput (p2,s2,m)) in dom I by A2, Def1, A4;
hence Comput (p1,s1,k), Comput (p2,s2,k) equal_outside NAT by A5, AMISTD_2:66, A3, A4; :: thesis: CurInstr (p1,(Comput (p1,s1,k))) = CurInstr (p2,(Comput (p2,s2,k)))
then A8: IC (Comput (p1,s1,k)) = IC (Comput (p2,s2,k)) by COMPOS_1:24;
thus CurInstr (p2,(Comput (p2,s2,k))) = p2 . (IC (Comput (p2,s2,k))) by PBOOLE:158
.= I . (IC (Comput (p2,s2,k))) by A7, GRFUNC_1:8, A4
.= p1 . (IC (Comput (p1,s1,k))) by A8, A6, GRFUNC_1:8, A3
.= CurInstr (p1,(Comput (p1,s1,k))) by PBOOLE:158 ; :: thesis: verum