let P1, P2 be Instruction-Sequence of SCM+FSA; :: thesis: for s1, s2 being State of SCM+FSA
for I being Program of SCM+FSA st DataPart s1 = DataPart s2 & I is_closed_on s1,P1 & I is_halting_on s1,P1 holds
( I is_closed_on s2,P2 & I is_halting_on s2,P2 )
let s1, s2 be State of SCM+FSA; :: thesis: for I being Program of SCM+FSA st DataPart s1 = DataPart s2 & I is_closed_on s1,P1 & I is_halting_on s1,P1 holds
( I is_closed_on s2,P2 & I is_halting_on s2,P2 )
let I be Program of SCM+FSA; :: thesis: ( DataPart s1 = DataPart s2 & I is_closed_on s1,P1 & I is_halting_on s1,P1 implies ( I is_closed_on s2,P2 & I is_halting_on s2,P2 ) )
set S1 = Initialize s1;
set S2 = Initialize s2;
defpred S₁[ Nat] means ( IC (Comput ((P1 +* I),(Initialize s1),$1)) = IC (Comput ((P2 +* I),(Initialize s2),$1)) & CurInstr ((P1 +* I),(Comput ((P1 +* I),(Initialize s1),$1))) = CurInstr ((P2 +* I),(Comput ((P2 +* I),(Initialize s2),$1))) & DataPart (Comput ((P1 +* I),(Initialize s1),$1)) = DataPart (Comput ((P2 +* I),(Initialize s2),$1)) );
A4: Comput ((P1 +* I),(Initialize s1),0) = Initialize s1 by EXTPRO_1:2;
C5: IC in dom (Start-At (0,SCM+FSA)) by MEMSTR_0:15;
A6: IC (Comput ((P1 +* I),(Initialize s1),0)) = IC (Start-At (0,SCM+FSA)) by A4, C5, FUNCT_4:13
.= 0 by FUNCOP_1:72 ;
A7: Comput ((P2 +* I),(Initialize s2),0) = Initialize s2 by EXTPRO_1:2;
then A8: IC (Comput ((P2 +* I),(Initialize s2),0)) = IC (Start-At (0,SCM+FSA)) by C5, FUNCT_4:13
.= 0 by FUNCOP_1:72 ;
assume DataPart s1 = DataPart s2 ; :: thesis: ( not I is_closed_on s1,P1 or not I is_halting_on s1,P1 or ( I is_closed_on s2,P2 & I is_halting_on s2,P2 ) )
then A9: Comput ((P1 +* I),(Initialize s1),0) = Comput ((P2 +* I),(Initialize s2),0) by A4, A7, Th7;
assume A10: I is_closed_on s1,P1 ; :: thesis: ( not I is_halting_on s1,P1 or ( I is_closed_on s2,P2 & I is_halting_on s2,P2 ) )

A11: now

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
A12: Comput ((P2 +* I),(Initialize s2),(k + 1)) = Following ((P2 +* I),(Comput ((P2 +* I),(Initialize s2),k))) by EXTPRO_1:3
.= Exec ((CurInstr ((P2 +* I),(Comput ((P2 +* I),(Initialize s2),k)))),(Comput ((P2 +* I),(Initialize s2),k))) ;
assume A13: S₁[k] ; :: thesis: S₁[k + 1]
then A14: for f being FinSeq-Location holds (Comput ((P1 +* I),(Initialize s1),k)) . f = (Comput ((P2 +* I),(Initialize s2),k)) . f by SCMFSA6A:7;
for a being Int-Location holds (Comput ((P1 +* I),(Initialize s1),k)) . a = (Comput ((P2 +* I),(Initialize s2),k)) . a by A13, SCMFSA6A:7;
then A15: Comput ((P1 +* I),(Initialize s1),k) = Comput ((P2 +* I),(Initialize s2),k) by A13, A14, SCMFSA_2:61;
A16: IC (Comput ((P1 +* I),(Initialize s1),(k + 1))) in dom I by A10, SCMFSA7B:def 6;
Comput ((P1 +* I),(Initialize s1),(k + 1)) = Following ((P1 +* I),(Comput ((P1 +* I),(Initialize s1),k))) by EXTPRO_1:3
.= Exec ((CurInstr ((P1 +* I),(Comput ((P1 +* I),(Initialize s1),k)))),(Comput ((P1 +* I),(Initialize s1),k))) ;
then A17: Comput ((P1 +* I),(Initialize s1),(k + 1)) = Comput ((P2 +* I),(Initialize s2),(k + 1)) by A13, A15, A12;
A18: IC (Comput ((P1 +* I),(Initialize s1),(k + 1))) = IC (Comput ((P2 +* I),(Initialize s2),(k + 1))) by A17;
A19: (P1 +* I) /. (IC (Comput ((P1 +* I),(Initialize s1),(k + 1)))) = (P1 +* I) . (IC (Comput ((P1 +* I),(Initialize s1),(k + 1)))) by PBOOLE:143;
A20: (P2 +* I) /. (IC (Comput ((P2 +* I),(Initialize s2),(k + 1)))) = (P2 +* I) . (IC (Comput ((P2 +* I),(Initialize s2),(k + 1)))) by PBOOLE:143;
A21: I c= P1 +* I by FUNCT_4:25;
A22: I c= P2 +* I by FUNCT_4:25;
CurInstr ((P1 +* I),(Comput ((P1 +* I),(Initialize s1),(k + 1)))) = I . (IC (Comput ((P1 +* I),(Initialize s1),(k + 1)))) by A16, A19, A21, GRFUNC_1:2
.= CurInstr ((P2 +* I),(Comput ((P2 +* I),(Initialize s2),(k + 1)))) by A18, A16, A20, A22, GRFUNC_1:2 ;
hence S₁[k + 1] by A17; :: thesis: verum

end;

assume I is_halting_on s1,P1 ; :: thesis: ( I is_closed_on s2,P2 & I is_halting_on s2,P2 )
then P1 +* I halts_on Initialize s1 by SCMFSA7B:def 7;
then consider m being Element of NAT such that
A23: CurInstr ((P1 +* I),(Comput ((P1 +* I),(Initialize s1),m))) = halt SCM+FSA by EXTPRO_1:29;
A24: (P1 +* I) /. (IC (Comput ((P1 +* I),(Initialize s1),0))) = (P1 +* I) . (IC (Comput ((P1 +* I),(Initialize s1),0))) by PBOOLE:143;
A25: (P2 +* I) /. (IC (Comput ((P2 +* I),(Initialize s2),0))) = (P2 +* I) . (IC (Comput ((P2 +* I),(Initialize s2),0))) by PBOOLE:143;
A26: 0 in dom I by A10, Th3;
then CurInstr ((P1 +* I),(Comput ((P1 +* I),(Initialize s1),0))) = I . 0 by A6, A24, FUNCT_4:13
.= CurInstr ((P2 +* I),(Comput ((P2 +* I),(Initialize s2),0))) by A8, A26, A25, FUNCT_4:13 ;
then A27: S₁[ 0 ] by A9;

now

let k be Element of NAT ; :: thesis: IC (Comput ((P2 +* I),(Initialize s2),k)) in dom I
A28: IC (Comput ((P1 +* I),(Initialize s1),k)) in dom I by A10, SCMFSA7B:def 6;
for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A27, A11);
hence IC (Comput ((P2 +* I),(Initialize s2),k)) in dom I by A28; :: thesis: verum

end;

hence I is_closed_on s2,P2 by SCMFSA7B:def 6; :: thesis: I is_halting_on s2,P2
for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A27, A11);
then CurInstr ((P2 +* I),(Comput ((P2 +* I),(Initialize s2),m))) = halt SCM+FSA by A23;
then P2 +* I halts_on Initialize s2 by EXTPRO_1:29;
hence I is_halting_on s2,P2 by SCMFSA7B:def 7; :: thesis: verum