let P1, P2 be Instruction-Sequence of SCM+FSA; :: thesis: for s being State of SCM+FSA

for I being really-closed InitHalting Program of SCM+FSA st Initialize ((intloc 0) .--> 1) c= s & I c= P1 & I c= P2 holds

for k being Nat holds

( Comput (P1,s,k) = Comput (P2,s,k) & CurInstr (P1,(Comput (P1,s,k))) = CurInstr (P2,(Comput (P2,s,k))) )

let s be State of SCM+FSA; :: thesis: for I being really-closed InitHalting Program of SCM+FSA st Initialize ((intloc 0) .--> 1) c= s & I c= P1 & I c= P2 holds

for k being Nat holds

( Comput (P1,s,k) = Comput (P2,s,k) & CurInstr (P1,(Comput (P1,s,k))) = CurInstr (P2,(Comput (P2,s,k))) )

let I be really-closed InitHalting Program of SCM+FSA; :: thesis: ( Initialize ((intloc 0) .--> 1) c= s & I c= P1 & I c= P2 implies for k being Nat holds

( Comput (P1,s,k) = Comput (P2,s,k) & CurInstr (P1,(Comput (P1,s,k))) = CurInstr (P2,(Comput (P2,s,k))) ) )

assume that

A1: Initialize ((intloc 0) .--> 1) c= s and

A2: I c= P1 and

A3: I c= P2 ; :: thesis: for k being Nat holds

( Comput (P1,s,k) = Comput (P2,s,k) & CurInstr (P1,(Comput (P1,s,k))) = CurInstr (P2,(Comput (P2,s,k))) )

let k be Nat; :: thesis: ( Comput (P1,s,k) = Comput (P2,s,k) & CurInstr (P1,(Comput (P1,s,k))) = CurInstr (P2,(Comput (P2,s,k))) )

IC s = 0 by A1, MEMSTR_0:47;

then A4: IC s in dom I by AFINSQ_1:65;

then A5: IC (Comput (P1,s,k)) in dom I by A2, AMISTD_1:21;

A6: IC (Comput (P2,s,k)) in dom I by A3, AMISTD_1:21, A4;

for m being Nat st m < k holds

IC (Comput (P2,s,m)) in dom I by A3, A4, AMISTD_1:21;

hence Comput (P1,s,k) = Comput (P2,s,k) by A2, A3, AMISTD_2:10; :: thesis: CurInstr (P1,(Comput (P1,s,k))) = CurInstr (P2,(Comput (P2,s,k)))

then A7: IC (Comput (P1,s,k)) = IC (Comput (P2,s,k)) ;

thus CurInstr (P2,(Comput (P2,s,k))) = P2 . (IC (Comput (P2,s,k))) by PBOOLE:143

.= I . (IC (Comput (P2,s,k))) by A6, A3, GRFUNC_1:2

.= P1 . (IC (Comput (P1,s,k))) by A7, A5, A2, GRFUNC_1:2

.= CurInstr (P1,(Comput (P1,s,k))) by PBOOLE:143 ; :: thesis: verum

for I being really-closed InitHalting Program of SCM+FSA st Initialize ((intloc 0) .--> 1) c= s & I c= P1 & I c= P2 holds

for k being Nat holds

( Comput (P1,s,k) = Comput (P2,s,k) & CurInstr (P1,(Comput (P1,s,k))) = CurInstr (P2,(Comput (P2,s,k))) )

let s be State of SCM+FSA; :: thesis: for I being really-closed InitHalting Program of SCM+FSA st Initialize ((intloc 0) .--> 1) c= s & I c= P1 & I c= P2 holds

for k being Nat holds

( Comput (P1,s,k) = Comput (P2,s,k) & CurInstr (P1,(Comput (P1,s,k))) = CurInstr (P2,(Comput (P2,s,k))) )

let I be really-closed InitHalting Program of SCM+FSA; :: thesis: ( Initialize ((intloc 0) .--> 1) c= s & I c= P1 & I c= P2 implies for k being Nat holds

( Comput (P1,s,k) = Comput (P2,s,k) & CurInstr (P1,(Comput (P1,s,k))) = CurInstr (P2,(Comput (P2,s,k))) ) )

assume that

A1: Initialize ((intloc 0) .--> 1) c= s and

A2: I c= P1 and

A3: I c= P2 ; :: thesis: for k being Nat holds

( Comput (P1,s,k) = Comput (P2,s,k) & CurInstr (P1,(Comput (P1,s,k))) = CurInstr (P2,(Comput (P2,s,k))) )

let k be Nat; :: thesis: ( Comput (P1,s,k) = Comput (P2,s,k) & CurInstr (P1,(Comput (P1,s,k))) = CurInstr (P2,(Comput (P2,s,k))) )

IC s = 0 by A1, MEMSTR_0:47;

then A4: IC s in dom I by AFINSQ_1:65;

then A5: IC (Comput (P1,s,k)) in dom I by A2, AMISTD_1:21;

A6: IC (Comput (P2,s,k)) in dom I by A3, AMISTD_1:21, A4;

for m being Nat st m < k holds

IC (Comput (P2,s,m)) in dom I by A3, A4, AMISTD_1:21;

hence Comput (P1,s,k) = Comput (P2,s,k) by A2, A3, AMISTD_2:10; :: thesis: CurInstr (P1,(Comput (P1,s,k))) = CurInstr (P2,(Comput (P2,s,k)))

then A7: IC (Comput (P1,s,k)) = IC (Comput (P2,s,k)) ;

thus CurInstr (P2,(Comput (P2,s,k))) = P2 . (IC (Comput (P2,s,k))) by PBOOLE:143

.= I . (IC (Comput (P2,s,k))) by A6, A3, GRFUNC_1:2

.= P1 . (IC (Comput (P1,s,k))) by A7, A5, A2, GRFUNC_1:2

.= CurInstr (P1,(Comput (P1,s,k))) by PBOOLE:143 ; :: thesis: verum