let P1, P2 be Instruction-Sequence of SCM+FSA; :: thesis: for s1, s2 being 0 -started State of SCM+FSA
for I being Program of SCM+FSA st I is_closed_on s1,P1 & I is_halting_on s1,P1 & I c= P1 & I c= P2 & ex k being Element of NAT st Comput (P1,s1,k) = s2 holds
Result (P1,s1) = Result (P2,s2)
let s1, s2 be 0 -started State of SCM+FSA; :: thesis: for I being Program of SCM+FSA st I is_closed_on s1,P1 & I is_halting_on s1,P1 & I c= P1 & I c= P2 & ex k being Element of NAT st Comput (P1,s1,k) = s2 holds
Result (P1,s1) = Result (P2,s2)
set D = Data-Locations ;
let I be Program of SCM+FSA; :: thesis: ( I is_closed_on s1,P1 & I is_halting_on s1,P1 & I c= P1 & I c= P2 & ex k being Element of NAT st Comput (P1,s1,k) = s2 implies Result (P1,s1) = Result (P2,s2) )
assume A1: I is_closed_on s1,P1 ; :: thesis: ( not I is_halting_on s1,P1 or not I c= P1 or not I c= P2 or for k being Element of NAT holds not Comput (P1,s1,k) = s2 or Result (P1,s1) = Result (P2,s2) )
assume A2: I is_halting_on s1,P1 ; :: thesis: ( not I c= P1 or not I c= P2 or for k being Element of NAT holds not Comput (P1,s1,k) = s2 or Result (P1,s1) = Result (P2,s2) )
A3: Start-At (0,SCM+FSA) c= s1 by MEMSTR_0:29;
A4: s2 = Initialize s2 by MEMSTR_0:44;
assume I c= P1 ; :: thesis: ( not I c= P2 or for k being Element of NAT holds not Comput (P1,s1,k) = s2 or Result (P1,s1) = Result (P2,s2) )
then A5: P1 = P1 +* I by FUNCT_4:98;
assume I c= P2 ; :: thesis: ( for k being Element of NAT holds not Comput (P1,s1,k) = s2 or Result (P1,s1) = Result (P2,s2) )
then A6: P2 = P2 +* I by FUNCT_4:98;
A7: s1 = Initialize s1 by A3, FUNCT_4:98;
then A8: P1 halts_on s1 by A2, A5, SCMFSA7B:def 7;
then consider n being Element of NAT such that
A9: CurInstr (P1,(Comput (P1,s1,n))) = halt SCM+FSA by EXTPRO_1:29;
given k being Element of NAT such that A10: Comput (P1,s1,k) = s2 ; :: thesis: Result (P1,s1) = Result (P2,s2)
set s3 = Comput (P1,s1,k);
set P3 = P1;
A11: IC in dom (Comput (P1,s1,k)) by MEMSTR_0:2;
IC (Comput (P1,s1,k)) = IC s2 by A10
.= IC (Initialize s2) by A4
.= 0 by FUNCT_4:113 ;
then (IC ) .--> 0 c= Comput (P1,s1,k) by A11, FUNCOP_1:73;
then Start-At (0,SCM+FSA) c= Comput (P1,s1,k) ;
then A12: Comput (P1,s1,k) = Initialize (Comput (P1,s1,k)) by FUNCT_4:98;

A13: now :: thesis: for n being Element of NAT holds IC (Comput (P1,(Comput (P1,s1,k)),n)) in dom I

let n be Element of NAT ; :: thesis: IC (Comput (P1,(Comput (P1,s1,k)),n)) in dom I
IC (Comput (P1,(Comput (P1,s1,k)),n)) = IC (Comput (P1,s1,(k + n))) by EXTPRO_1:4;
hence IC (Comput (P1,(Comput (P1,s1,k)),n)) in dom I by A1, A7, A5, SCMFSA7B:def 6; :: thesis: verum

end;

A14: Comput (P1,s1,(n + k)) = Comput (P1,(Comput (P1,s1,k)),n) by EXTPRO_1:4;
A15: Comput (P1,s1,(n + k)) = Comput (P1,s1,n) by A9, EXTPRO_1:5, NAT_1:11;
P1 halts_on Comput (P1,s1,k) by A9, A15, A14, EXTPRO_1:29;
then A16: I is_halting_on Comput (P1,s1,k),P1 by A12, A5, SCMFSA7B:def 7;
A17: DataPart (Comput (P1,s1,k)) = DataPart s2 by A10;
consider k being Element of NAT such that
A18: CurInstr (P1,(Comput (P1,s1,k))) = halt SCM+FSA by A8, EXTPRO_1:29;
A19: P1 . (IC (Comput (P1,s1,k))) = halt SCM+FSA by A18, PBOOLE:143;
I is_closed_on Comput (P1,s1,k),P1 by A12, A13, A5, SCMFSA7B:def 6;
then Result (P1,(Comput (P1,s1,k))) = Result (P2,s2) by A4, A17, A12, A16, Th72, A5, A6;
hence Result (P1,s1) = Result (P2,s2) by A19, EXTPRO_1:8; :: thesis: verum