let P1, P2 be the Instructions of SCM+FSA -valued ManySortedSet of NAT ; :: thesis: for s1, s2 being State of SCM+FSA
for I being Program of SCM+FSA st I is_closed_on s1,P1 & I is_halting_on s1,P1 & Initialize I c= s1 & Initialize I c= s2 & I c= P1 & I c= P2 & ex k being Element of NAT st Comput (P1,s1,k),s2 equal_outside NAT holds
Result (P1,s1), Result (P2,s2) equal_outside NAT
let s1, s2 be 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 & Initialize I c= s1 & Initialize I c= s2 & I c= P1 & I c= P2 & ex k being Element of NAT st Comput (P1,s1,k),s2 equal_outside NAT holds
Result (P1,s1), Result (P2,s2) equal_outside NAT
set A = NAT ;
set D = Data-Locations SCM+FSA;
let I be Program of SCM+FSA; :: thesis: ( I is_closed_on s1,P1 & I is_halting_on s1,P1 & Initialize I c= s1 & Initialize I c= s2 & I c= P1 & I c= P2 & ex k being Element of NAT st Comput (P1,s1,k),s2 equal_outside NAT implies Result (P1,s1), Result (P2,s2) equal_outside NAT )
assume A1: I is_closed_on s1,P1 ; :: thesis: ( not I is_halting_on s1,P1 or not Initialize I c= s1 or not Initialize I c= s2 or not I c= P1 or not I c= P2 or for k being Element of NAT holds not Comput (P1,s1,k),s2 equal_outside NAT or Result (P1,s1), Result (P2,s2) equal_outside NAT )
A2: ProgramPart I = I by RELAT_1:209;
assume A3: I is_halting_on s1,P1 ; :: thesis: ( not Initialize I c= s1 or not Initialize I c= s2 or not I c= P1 or not I c= P2 or for k being Element of NAT holds not Comput (P1,s1,k),s2 equal_outside NAT or Result (P1,s1), Result (P2,s2) equal_outside NAT )
assume A4: Initialize I c= s1 ; :: thesis: ( not Initialize I c= s2 or not I c= P1 or not I c= P2 or for k being Element of NAT holds not Comput (P1,s1,k),s2 equal_outside NAT or Result (P1,s1), Result (P2,s2) equal_outside NAT )
assume Initialize I c= s2 ; :: thesis: ( not I c= P1 or not I c= P2 or for k being Element of NAT holds not Comput (P1,s1,k),s2 equal_outside NAT or Result (P1,s1), Result (P2,s2) equal_outside NAT )
then A5: s2 = s2 +* (Initialize I) by FUNCT_4:79;
assume I c= P1 ; :: thesis: ( not I c= P2 or for k being Element of NAT holds not Comput (P1,s1,k),s2 equal_outside NAT or Result (P1,s1), Result (P2,s2) equal_outside NAT )
then A6: P1 = P1 +* I by FUNCT_4:79;
assume I c= P2 ; :: thesis: ( for k being Element of NAT holds not Comput (P1,s1,k),s2 equal_outside NAT or Result (P1,s1), Result (P2,s2) equal_outside NAT )
then A7: P2 = P2 +* I by FUNCT_4:79;
A8: s1 = s1 +* (Initialize I) by FUNCT_4:79, A4;
then A9: P1 halts_on s1 by A3, SCMFSA7B:def 8, A2, A6;
then consider n being Element of NAT such that
A10: CurInstr (P1,(Comput (P1,s1,n))) = halt SCM+FSA by EXTPRO_1:30;
given k being Element of NAT such that A11: Comput (P1,s1,k),s2 equal_outside NAT ; :: thesis: Result (P1,s1), Result (P2,s2) equal_outside NAT
set s3 = Comput (P1,s1,k);
set P3 = P1;
A12: IC in dom (Comput (P1,s1,k)) by COMPOS_1:9;
I c= Initialize I by SCMFSA8A:9;
then I c= s1 by A4, XBOOLE_1:1;
then A13: I c= Comput (P1,s1,k) by AMI_1:86;
IC (Comput (P1,s1,k)) = IC s2 by A11, SCMFSA8A:6
.= IC (Initialize (s2 +* I)) by A5, FUNCT_4:15
.= 0 by FUNCT_4:121 ;
then (IC ) .--> 0 c= Comput (P1,s1,k) by A12, FUNCOP_1:88;
then Initialize I c= Comput (P1,s1,k) by A13, FUNCT_4:92;
then A14: Comput (P1,s1,k) = (Comput (P1,s1,k)) +* (Initialize I) by FUNCT_4:79;

A15: now

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:5;
hence IC (Comput (P1,(Comput (P1,s1,k)),n)) in dom I by A1, A8, SCMFSA7B:def 7, A2, A6; :: thesis: verum

end;

A16: Comput (P1,s1,(n + k)) = Comput (P1,(Comput (P1,s1,k)),n) by EXTPRO_1:5;
n <= n + k by NAT_1:11;
then A17: Comput (P1,s1,(n + k)) = Comput (P1,s1,n) by A10, EXTPRO_1:6;
CurInstr (P1,(Comput (P1,(Comput (P1,s1,k)),n))) = CurInstr (P1,(Comput (P1,s1,n))) by A17, A16;
then P1 halts_on Comput (P1,s1,k) by A10, EXTPRO_1:30;
then A18: I is_halting_on Comput (P1,s1,k),P1 by A14, SCMFSA7B:def 8, A2, A6;
A19: DataPart (Comput (P1,s1,k)) = DataPart s2 by A11, SCMFSA8A:6;
consider k being Element of NAT such that
A20: CurInstr (P1,(Comput (P1,s1,k))) = halt SCM+FSA by A9, EXTPRO_1:30;
A21: P1 /. (IC (Comput (P1,s1,k))) = P1 . (IC (Comput (P1,s1,k))) by PBOOLE:158;
A22: P1 . (IC (Comput (P1,s1,k))) = P1 . (IC (Comput (P1,s1,k)))
.= halt SCM+FSA by A20, A21 ;
I is_closed_on Comput (P1,s1,k),P1 by A14, A15, SCMFSA7B:def 7, A2, A6;
then Result (P1,(Comput (P1,s1,k))), Result (P2,s2) equal_outside NAT by A5, A19, A14, A18, Th101, A6, A7;
hence Result (P1,s1), Result (P2,s2) equal_outside NAT by A22, EXTPRO_1:9; :: thesis: verum