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 & I is_halting_on s1 holds
( I is_closed_on s2 & I is_halting_on s2 )
let I be Program of SCM+FSA; :: thesis: ( DataPart s1 = DataPart s2 & I is_closed_on s1 & I is_halting_on s1 implies ( I is_closed_on s2 & I is_halting_on s2 ) )
set S1 = s1 +* (I +* (Start-At (0,SCM+FSA)));
set S2 = s2 +* (I +* (Start-At (0,SCM+FSA)));
defpred S₁[ Nat] means ( IC (Comput ((ProgramPart (s1 +* (I +* (Start-At (0,SCM+FSA))))),(s1 +* (I +* (Start-At (0,SCM+FSA)))),$1)) = IC (Comput ((ProgramPart (s2 +* (I +* (Start-At (0,SCM+FSA))))),(s2 +* (I +* (Start-At (0,SCM+FSA)))),$1)) & CurInstr ((ProgramPart (s1 +* (I +* (Start-At (0,SCM+FSA))))),(Comput ((ProgramPart (s1 +* (I +* (Start-At (0,SCM+FSA))))),(s1 +* (I +* (Start-At (0,SCM+FSA)))),$1))) = CurInstr ((ProgramPart (s2 +* (I +* (Start-At (0,SCM+FSA))))),(Comput ((ProgramPart (s2 +* (I +* (Start-At (0,SCM+FSA))))),(s2 +* (I +* (Start-At (0,SCM+FSA)))),$1))) & DataPart (Comput ((ProgramPart (s1 +* (I +* (Start-At (0,SCM+FSA))))),(s1 +* (I +* (Start-At (0,SCM+FSA)))),$1)) = DataPart (Comput ((ProgramPart (s2 +* (I +* (Start-At (0,SCM+FSA))))),(s2 +* (I +* (Start-At (0,SCM+FSA)))),$1)) );
A1: IC SCM+FSA in {(IC SCM+FSA)} by TARSKI:def 1;
A2: I c= I +* (Start-At (0,SCM+FSA)) by SCMFSA8A:9;
then A3: dom I c= dom (I +* (Start-At (0,SCM+FSA))) by GRFUNC_1:8;
A4: {(IC SCM+FSA)} = dom (Start-At (0,SCM+FSA)) by FUNCOP_1:19;
A5: Comput ((ProgramPart (s1 +* (I +* (Start-At (0,SCM+FSA))))),(s1 +* (I +* (Start-At (0,SCM+FSA)))),0) = s1 +* (I +* (Start-At (0,SCM+FSA))) by EXTPRO_1:3;
Start-At (0,SCM+FSA) c= I +* (Start-At (0,SCM+FSA)) by FUNCT_4:26;
then A6: dom (Start-At (0,SCM+FSA)) c= dom (I +* (Start-At (0,SCM+FSA))) by GRFUNC_1:8;
then A7: IC (Comput ((ProgramPart (s1 +* (I +* (Start-At (0,SCM+FSA))))),(s1 +* (I +* (Start-At (0,SCM+FSA)))),0)) = (I +* (Start-At (0,SCM+FSA))) . (IC SCM+FSA) by A1, A4, A5, FUNCT_4:14
.= (Start-At (0,SCM+FSA)) . (IC SCM+FSA) by A1, A4, FUNCT_4:14
.= 0 by FUNCOP_1:87 ;
A8: Comput ((ProgramPart (s2 +* (I +* (Start-At (0,SCM+FSA))))),(s2 +* (I +* (Start-At (0,SCM+FSA)))),0) = s2 +* (I +* (Start-At (0,SCM+FSA))) by EXTPRO_1:3;
then A9: IC (Comput ((ProgramPart (s2 +* (I +* (Start-At (0,SCM+FSA))))),(s2 +* (I +* (Start-At (0,SCM+FSA)))),0)) = (I +* (Start-At (0,SCM+FSA))) . (IC SCM+FSA) by A1, A4, A6, FUNCT_4:14
.= (Start-At (0,SCM+FSA)) . (IC SCM+FSA) by A1, A4, FUNCT_4:14
.= 0 by FUNCOP_1:87 ;
assume DataPart s1 = DataPart s2 ; :: thesis: ( not I is_closed_on s1 or not I is_halting_on s1 or ( I is_closed_on s2 & I is_halting_on s2 ) )
then A10: Comput ((ProgramPart (s1 +* (I +* (Start-At (0,SCM+FSA))))),(s1 +* (I +* (Start-At (0,SCM+FSA)))),0), Comput ((ProgramPart (s2 +* (I +* (Start-At (0,SCM+FSA))))),(s2 +* (I +* (Start-At (0,SCM+FSA)))),0) equal_outside NAT by A5, A8, Th7;
assume A11: I is_closed_on s1 ; :: thesis: ( not I is_halting_on s1 or ( I is_closed_on s2 & I is_halting_on s2 ) )

A12: now

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
A13: Comput ((ProgramPart (s2 +* (I +* (Start-At (0,SCM+FSA))))),(s2 +* (I +* (Start-At (0,SCM+FSA)))),(k + 1)) = Following ((ProgramPart (s2 +* (I +* (Start-At (0,SCM+FSA))))),(Comput ((ProgramPart (s2 +* (I +* (Start-At (0,SCM+FSA))))),(s2 +* (I +* (Start-At (0,SCM+FSA)))),k))) by EXTPRO_1:4
.= Exec ((CurInstr ((ProgramPart (s2 +* (I +* (Start-At (0,SCM+FSA))))),(Comput ((ProgramPart (s2 +* (I +* (Start-At (0,SCM+FSA))))),(s2 +* (I +* (Start-At (0,SCM+FSA)))),k)))),(Comput ((ProgramPart (s2 +* (I +* (Start-At (0,SCM+FSA))))),(s2 +* (I +* (Start-At (0,SCM+FSA)))),k))) ;
assume A14: S₁[k] ; :: thesis: S₁[k + 1]
then A15: for f being FinSeq-Location holds (Comput ((ProgramPart (s1 +* (I +* (Start-At (0,SCM+FSA))))),(s1 +* (I +* (Start-At (0,SCM+FSA)))),k)) . f = (Comput ((ProgramPart (s2 +* (I +* (Start-At (0,SCM+FSA))))),(s2 +* (I +* (Start-At (0,SCM+FSA)))),k)) . f by SCMFSA6A:38;
for a being Int-Location holds (Comput ((ProgramPart (s1 +* (I +* (Start-At (0,SCM+FSA))))),(s1 +* (I +* (Start-At (0,SCM+FSA)))),k)) . a = (Comput ((ProgramPart (s2 +* (I +* (Start-At (0,SCM+FSA))))),(s2 +* (I +* (Start-At (0,SCM+FSA)))),k)) . a by A14, SCMFSA6A:38;
then A16: Comput ((ProgramPart (s1 +* (I +* (Start-At (0,SCM+FSA))))),(s1 +* (I +* (Start-At (0,SCM+FSA)))),k), Comput ((ProgramPart (s2 +* (I +* (Start-At (0,SCM+FSA))))),(s2 +* (I +* (Start-At (0,SCM+FSA)))),k) equal_outside NAT by A14, A15, SCMFSA10:91;
I +* (Start-At (0,SCM+FSA)) c= s2 +* (I +* (Start-At (0,SCM+FSA))) by FUNCT_4:26;
then I c= s2 +* (I +* (Start-At (0,SCM+FSA))) by A2, XBOOLE_1:1;
then A17: I c= Comput ((ProgramPart (s2 +* (I +* (Start-At (0,SCM+FSA))))),(s2 +* (I +* (Start-At (0,SCM+FSA)))),(k + 1)) by AMI_1:81;
A18: IC (Comput ((ProgramPart (s1 +* (I +* (Start-At (0,SCM+FSA))))),(s1 +* (I +* (Start-At (0,SCM+FSA)))),(k + 1))) in dom I by A11, SCMFSA7B:def 7;
A19: Comput ((ProgramPart (s1 +* (I +* (Start-At (0,SCM+FSA))))),(s1 +* (I +* (Start-At (0,SCM+FSA)))),(k + 1)) = Following ((ProgramPart (s1 +* (I +* (Start-At (0,SCM+FSA))))),(Comput ((ProgramPart (s1 +* (I +* (Start-At (0,SCM+FSA))))),(s1 +* (I +* (Start-At (0,SCM+FSA)))),k))) by EXTPRO_1:4
.= Exec ((CurInstr ((ProgramPart (s1 +* (I +* (Start-At (0,SCM+FSA))))),(Comput ((ProgramPart (s1 +* (I +* (Start-At (0,SCM+FSA))))),(s1 +* (I +* (Start-At (0,SCM+FSA)))),k)))),(Comput ((ProgramPart (s1 +* (I +* (Start-At (0,SCM+FSA))))),(s1 +* (I +* (Start-At (0,SCM+FSA)))),k))) ;
then A20: IC (Comput ((ProgramPart (s1 +* (I +* (Start-At (0,SCM+FSA))))),(s1 +* (I +* (Start-At (0,SCM+FSA)))),(k + 1))) = IC (Comput ((ProgramPart (s2 +* (I +* (Start-At (0,SCM+FSA))))),(s2 +* (I +* (Start-At (0,SCM+FSA)))),(k + 1))) by A14, A16, A13, COMPOS_1:24, SCMFSA6A:32;
Y: (ProgramPart (Comput ((ProgramPart (s1 +* (I +* (Start-At (0,SCM+FSA))))),(s1 +* (I +* (Start-At (0,SCM+FSA)))),(k + 1)))) /. (IC (Comput ((ProgramPart (s1 +* (I +* (Start-At (0,SCM+FSA))))),(s1 +* (I +* (Start-At (0,SCM+FSA)))),(k + 1)))) = (Comput ((ProgramPart (s1 +* (I +* (Start-At (0,SCM+FSA))))),(s1 +* (I +* (Start-At (0,SCM+FSA)))),(k + 1))) . (IC (Comput ((ProgramPart (s1 +* (I +* (Start-At (0,SCM+FSA))))),(s1 +* (I +* (Start-At (0,SCM+FSA)))),(k + 1)))) by COMPOS_1:38;
Z: (ProgramPart (Comput ((ProgramPart (s2 +* (I +* (Start-At (0,SCM+FSA))))),(s2 +* (I +* (Start-At (0,SCM+FSA)))),(k + 1)))) /. (IC (Comput ((ProgramPart (s2 +* (I +* (Start-At (0,SCM+FSA))))),(s2 +* (I +* (Start-At (0,SCM+FSA)))),(k + 1)))) = (Comput ((ProgramPart (s2 +* (I +* (Start-At (0,SCM+FSA))))),(s2 +* (I +* (Start-At (0,SCM+FSA)))),(k + 1))) . (IC (Comput ((ProgramPart (s2 +* (I +* (Start-At (0,SCM+FSA))))),(s2 +* (I +* (Start-At (0,SCM+FSA)))),(k + 1)))) by COMPOS_1:38;
TX2: ProgramPart (s2 +* (I +* (Start-At (0,SCM+FSA)))) = ProgramPart (Comput ((ProgramPart (s2 +* (I +* (Start-At (0,SCM+FSA))))),(s2 +* (I +* (Start-At (0,SCM+FSA)))),(k + 1))) by AMI_1:123;
TX1: ProgramPart (s1 +* (I +* (Start-At (0,SCM+FSA)))) = ProgramPart (Comput ((ProgramPart (s1 +* (I +* (Start-At (0,SCM+FSA))))),(s1 +* (I +* (Start-At (0,SCM+FSA)))),(k + 1))) by AMI_1:123;
I +* (Start-At (0,SCM+FSA)) c= s1 +* (I +* (Start-At (0,SCM+FSA))) by FUNCT_4:26;
then I c= s1 +* (I +* (Start-At (0,SCM+FSA))) by A2, XBOOLE_1:1;
then I c= Comput ((ProgramPart (s1 +* (I +* (Start-At (0,SCM+FSA))))),(s1 +* (I +* (Start-At (0,SCM+FSA)))),(k + 1)) by AMI_1:81;
then u: CurInstr ((ProgramPart (s1 +* (I +* (Start-At (0,SCM+FSA))))),(Comput ((ProgramPart (s1 +* (I +* (Start-At (0,SCM+FSA))))),(s1 +* (I +* (Start-At (0,SCM+FSA)))),(k + 1)))) = I . (IC (Comput ((ProgramPart (s1 +* (I +* (Start-At (0,SCM+FSA))))),(s1 +* (I +* (Start-At (0,SCM+FSA)))),(k + 1)))) by A18, Y, TX1, GRFUNC_1:8
.= CurInstr ((ProgramPart (s2 +* (I +* (Start-At (0,SCM+FSA))))),(Comput ((ProgramPart (s2 +* (I +* (Start-At (0,SCM+FSA))))),(s2 +* (I +* (Start-At (0,SCM+FSA)))),(k + 1)))) by A17, A20, A18, Z, TX2, GRFUNC_1:8 ;
DataPart (Comput ((ProgramPart (s1 +* (I +* (Start-At (0,SCM+FSA))))),(s1 +* (I +* (Start-At (0,SCM+FSA)))),(k + 1))) = DataPart (Exec ((CurInstr ((ProgramPart (s1 +* (I +* (Start-At (0,SCM+FSA))))),(Comput ((ProgramPart (s1 +* (I +* (Start-At (0,SCM+FSA))))),(s1 +* (I +* (Start-At (0,SCM+FSA)))),k)))),(Comput ((ProgramPart (s1 +* (I +* (Start-At (0,SCM+FSA))))),(s1 +* (I +* (Start-At (0,SCM+FSA)))),k)))) by A19
.= DataPart (Comput ((ProgramPart (s2 +* (I +* (Start-At (0,SCM+FSA))))),(s2 +* (I +* (Start-At (0,SCM+FSA)))),(k + 1))) by A14, A16, A13, SCMFSA6A:32, SCMFSA6A:39 ;
hence S₁[k + 1] by A20, u; :: thesis: verum

end;

assume I is_halting_on s1 ; :: thesis: ( I is_closed_on s2 & I is_halting_on s2 )
then ProgramPart (s1 +* (I +* (Start-At (0,SCM+FSA)))) halts_on s1 +* (I +* (Start-At (0,SCM+FSA))) by SCMFSA7B:def 8;
then consider m being Element of NAT such that
A21: CurInstr ((ProgramPart (s1 +* (I +* (Start-At (0,SCM+FSA))))),(Comput ((ProgramPart (s1 +* (I +* (Start-At (0,SCM+FSA))))),(s1 +* (I +* (Start-At (0,SCM+FSA)))),m))) = halt SCM+FSA by EXTPRO_1:30;
Y: (ProgramPart (Comput ((ProgramPart (s1 +* (I +* (Start-At (0,SCM+FSA))))),(s1 +* (I +* (Start-At (0,SCM+FSA)))),0))) /. (IC (Comput ((ProgramPart (s1 +* (I +* (Start-At (0,SCM+FSA))))),(s1 +* (I +* (Start-At (0,SCM+FSA)))),0))) = (Comput ((ProgramPart (s1 +* (I +* (Start-At (0,SCM+FSA))))),(s1 +* (I +* (Start-At (0,SCM+FSA)))),0)) . (IC (Comput ((ProgramPart (s1 +* (I +* (Start-At (0,SCM+FSA))))),(s1 +* (I +* (Start-At (0,SCM+FSA)))),0))) by COMPOS_1:38;
Z: (ProgramPart (Comput ((ProgramPart (s2 +* (I +* (Start-At (0,SCM+FSA))))),(s2 +* (I +* (Start-At (0,SCM+FSA)))),0))) /. (IC (Comput ((ProgramPart (s2 +* (I +* (Start-At (0,SCM+FSA))))),(s2 +* (I +* (Start-At (0,SCM+FSA)))),0))) = (Comput ((ProgramPart (s2 +* (I +* (Start-At (0,SCM+FSA))))),(s2 +* (I +* (Start-At (0,SCM+FSA)))),0)) . (IC (Comput ((ProgramPart (s2 +* (I +* (Start-At (0,SCM+FSA))))),(s2 +* (I +* (Start-At (0,SCM+FSA)))),0))) by COMPOS_1:38;
A22: 0 in dom I by A11, Th3;
then CurInstr ((ProgramPart (s1 +* (I +* (Start-At (0,SCM+FSA))))),(Comput ((ProgramPart (s1 +* (I +* (Start-At (0,SCM+FSA))))),(s1 +* (I +* (Start-At (0,SCM+FSA)))),0))) = (I +* (Start-At (0,SCM+FSA))) . 0 by A5, A7, A3, Y, FUNCT_4:14
.= CurInstr ((ProgramPart (s2 +* (I +* (Start-At (0,SCM+FSA))))),(Comput ((ProgramPart (s2 +* (I +* (Start-At (0,SCM+FSA))))),(s2 +* (I +* (Start-At (0,SCM+FSA)))),0))) by A8, A9, A3, A22, Z, FUNCT_4:14 ;
then A23: S₁[ 0 ] by A7, A9, A10, SCMFSA6A:39;

now

let k be Element of NAT ; :: thesis: IC (Comput ((ProgramPart (s2 +* (I +* (Start-At (0,SCM+FSA))))),(s2 +* (I +* (Start-At (0,SCM+FSA)))),k)) in dom I
A24: IC (Comput ((ProgramPart (s1 +* (I +* (Start-At (0,SCM+FSA))))),(s1 +* (I +* (Start-At (0,SCM+FSA)))),k)) in dom I by A11, SCMFSA7B:def 7;
for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A23, A12);
hence IC (Comput ((ProgramPart (s2 +* (I +* (Start-At (0,SCM+FSA))))),(s2 +* (I +* (Start-At (0,SCM+FSA)))),k)) in dom I by A24; :: thesis: verum

end;

hence I is_closed_on s2 by SCMFSA7B:def 7; :: thesis: I is_halting_on s2
for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A23, A12);
then CurInstr ((ProgramPart (s2 +* (I +* (Start-At (0,SCM+FSA))))),(Comput ((ProgramPart (s2 +* (I +* (Start-At (0,SCM+FSA))))),(s2 +* (I +* (Start-At (0,SCM+FSA)))),m))) = halt SCM+FSA by A21;
then ProgramPart (s2 +* (I +* (Start-At (0,SCM+FSA)))) halts_on s2 +* (I +* (Start-At (0,SCM+FSA))) by EXTPRO_1:30;
hence I is_halting_on s2 by SCMFSA7B:def 8; :: thesis: verum