let s1, s2 be State of SCM+FSA; :: thesis: for p1, p2 being Instruction-Sequence of SCM+FSA

for I being really-closed InitHalting Program of SCM+FSA st Initialize ((intloc 0) .--> 1) c= s1 & Initialize ((intloc 0) .--> 1) c= s2 & I c= p1 & I c= p2 & s1 = s2 holds

for k being Nat holds

( Comput (p1,s1,k) = Comput (p2,s2,k) & CurInstr (p1,(Comput (p1,s1,k))) = CurInstr (p2,(Comput (p2,s2,k))) )

let p1, p2 be Instruction-Sequence of SCM+FSA; :: thesis: for I being really-closed InitHalting Program of SCM+FSA st Initialize ((intloc 0) .--> 1) c= s1 & Initialize ((intloc 0) .--> 1) c= s2 & I c= p1 & I c= p2 & s1 = s2 holds

for k being Nat holds

( Comput (p1,s1,k) = Comput (p2,s2,k) & CurInstr (p1,(Comput (p1,s1,k))) = CurInstr (p2,(Comput (p2,s2,k))) )

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

( Comput (p1,s1,k) = Comput (p2,s2,k) & CurInstr (p1,(Comput (p1,s1,k))) = CurInstr (p2,(Comput (p2,s2,k))) ) )

assume that

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

A2: Initialize ((intloc 0) .--> 1) c= s2 and

A3: I c= p1 and

A4: I c= p2 and

A5: s1 = s2 ; :: thesis: for k being Nat holds

( Comput (p1,s1,k) = Comput (p2,s2,k) & CurInstr (p1,(Comput (p1,s1,k))) = CurInstr (p2,(Comput (p2,s2,k))) )

let k be Nat; :: thesis: ( Comput (p1,s1,k) = Comput (p2,s2,k) & CurInstr (p1,(Comput (p1,s1,k))) = CurInstr (p2,(Comput (p2,s2,k))) )

IC s1 = 0 by A1, MEMSTR_0:47;

then IC s1 in dom I by AFINSQ_1:65;

then A6: IC (Comput (p1,s1,k)) in dom I by AMISTD_1:21, A3;

IC s2 = 0 by A2, MEMSTR_0:47;

then A7: IC s2 in dom I by AFINSQ_1:65;

then A8: IC (Comput (p2,s2,k)) in dom I by AMISTD_1:21, A4;

for m being Nat st m < k holds

IC (Comput (p2,s2,m)) in dom I by AMISTD_1:21, A4, A7;

hence A9: Comput (p1,s1,k) = Comput (p2,s2,k) by A5, A3, A4, AMISTD_2:10; :: thesis: CurInstr (p1,(Comput (p1,s1,k))) = CurInstr (p2,(Comput (p2,s2,k)))

thus CurInstr (p2,(Comput (p2,s2,k))) = p2 . (IC (Comput (p2,s2,k))) by PBOOLE:143

.= I . (IC (Comput (p2,s2,k))) by A8, A4, GRFUNC_1:2

.= p1 . (IC (Comput (p1,s1,k))) by A9, A6, A3, GRFUNC_1:2

.= CurInstr (p1,(Comput (p1,s1,k))) by PBOOLE:143 ; :: thesis: verum

for I being really-closed InitHalting Program of SCM+FSA st Initialize ((intloc 0) .--> 1) c= s1 & Initialize ((intloc 0) .--> 1) c= s2 & I c= p1 & I c= p2 & s1 = s2 holds

for k being Nat holds

( Comput (p1,s1,k) = Comput (p2,s2,k) & CurInstr (p1,(Comput (p1,s1,k))) = CurInstr (p2,(Comput (p2,s2,k))) )

let p1, p2 be Instruction-Sequence of SCM+FSA; :: thesis: for I being really-closed InitHalting Program of SCM+FSA st Initialize ((intloc 0) .--> 1) c= s1 & Initialize ((intloc 0) .--> 1) c= s2 & I c= p1 & I c= p2 & s1 = s2 holds

for k being Nat holds

( Comput (p1,s1,k) = Comput (p2,s2,k) & CurInstr (p1,(Comput (p1,s1,k))) = CurInstr (p2,(Comput (p2,s2,k))) )

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

( Comput (p1,s1,k) = Comput (p2,s2,k) & CurInstr (p1,(Comput (p1,s1,k))) = CurInstr (p2,(Comput (p2,s2,k))) ) )

assume that

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

A2: Initialize ((intloc 0) .--> 1) c= s2 and

A3: I c= p1 and

A4: I c= p2 and

A5: s1 = s2 ; :: thesis: for k being Nat holds

( Comput (p1,s1,k) = Comput (p2,s2,k) & CurInstr (p1,(Comput (p1,s1,k))) = CurInstr (p2,(Comput (p2,s2,k))) )

let k be Nat; :: thesis: ( Comput (p1,s1,k) = Comput (p2,s2,k) & CurInstr (p1,(Comput (p1,s1,k))) = CurInstr (p2,(Comput (p2,s2,k))) )

IC s1 = 0 by A1, MEMSTR_0:47;

then IC s1 in dom I by AFINSQ_1:65;

then A6: IC (Comput (p1,s1,k)) in dom I by AMISTD_1:21, A3;

IC s2 = 0 by A2, MEMSTR_0:47;

then A7: IC s2 in dom I by AFINSQ_1:65;

then A8: IC (Comput (p2,s2,k)) in dom I by AMISTD_1:21, A4;

for m being Nat st m < k holds

IC (Comput (p2,s2,m)) in dom I by AMISTD_1:21, A4, A7;

hence A9: Comput (p1,s1,k) = Comput (p2,s2,k) by A5, A3, A4, AMISTD_2:10; :: thesis: CurInstr (p1,(Comput (p1,s1,k))) = CurInstr (p2,(Comput (p2,s2,k)))

thus CurInstr (p2,(Comput (p2,s2,k))) = p2 . (IC (Comput (p2,s2,k))) by PBOOLE:143

.= I . (IC (Comput (p2,s2,k))) by A8, A4, GRFUNC_1:2

.= p1 . (IC (Comput (p1,s1,k))) by A9, A6, A3, GRFUNC_1:2

.= CurInstr (p1,(Comput (p1,s1,k))) by PBOOLE:143 ; :: thesis: verum