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 AMI_1:13;
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 AMI_1:13;
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] )
T: 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) by AMI_1:123;
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 AMI_1:14
.= 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 AMI_1:14
.= 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, T, 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 ;
w: DataPart (Comput (ProgramPart (s1 +* (I +* (Start-At 0 ,SCM+FSA )))),(s1 +* (I +* (Start-At 0 ,SCM+FSA ))),k) = DataPart (Comput (ProgramPart (s2 +* (I +* (Start-At 0 ,SCM+FSA )))),(s2 +* (I +* (Start-At 0 ,SCM+FSA ))),k) by A16, SCMFSA6A:39;
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, A19, A13, A20, TX1, TX2, w, 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 AMI_1:146;
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 AMI_1:146;
hence I is_halting_on s2 by SCMFSA7B:def 8; :: thesis: verum