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 (insloc 0 )));
set S2 = s2 +* (I +* (Start-At (insloc 0 )));
assume A1: 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 ) )
assume A2: I is_closed_on s1 ; :: thesis: ( not I is_halting_on s1 or ( I is_closed_on s2 & I is_halting_on s2 ) )
assume I is_halting_on s1 ; :: thesis: ( I is_closed_on s2 & I is_halting_on s2 )
then s1 +* (I +* (Start-At (insloc 0 ))) is halting by SCMFSA7B:def 8;
then consider m being Element of NAT such that
A3: CurInstr (Computation (s1 +* (I +* (Start-At (insloc 0 )))),m) = halt SCM+FSA by AMI_1:def 20;
defpred S₁[ Element of NAT ] means ( IC (Computation (s1 +* (I +* (Start-At (insloc 0 )))),$1) = IC (Computation (s2 +* (I +* (Start-At (insloc 0 )))),$1) & CurInstr (Computation (s1 +* (I +* (Start-At (insloc 0 )))),$1) = CurInstr (Computation (s2 +* (I +* (Start-At (insloc 0 )))),$1) & DataPart (Computation (s1 +* (I +* (Start-At (insloc 0 )))),$1) = DataPart (Computation (s2 +* (I +* (Start-At (insloc 0 )))),$1) );
A4: ( IC SCM+FSA in {(IC SCM+FSA )} & {(IC SCM+FSA )} = dom (Start-At (insloc 0 )) ) by FUNCOP_1:19, TARSKI:def 1;
Start-At (insloc 0 ) c= I +* (Start-At (insloc 0 )) by FUNCT_4:26;
then A5: dom (Start-At (insloc 0 )) c= dom (I +* (Start-At (insloc 0 ))) by GRFUNC_1:8;
A6: ( Computation (s1 +* (I +* (Start-At (insloc 0 )))),0 = s1 +* (I +* (Start-At (insloc 0 ))) & Computation (s2 +* (I +* (Start-At (insloc 0 )))),0 = s2 +* (I +* (Start-At (insloc 0 ))) ) by AMI_1:13;
then A7: IC (Computation (s1 +* (I +* (Start-At (insloc 0 )))),0 ) = (I +* (Start-At (insloc 0 ))) . (IC SCM+FSA ) by A4, A5, FUNCT_4:14
.= (Start-At (insloc 0 )) . (IC SCM+FSA ) by A4, FUNCT_4:14
.= insloc 0 by FUNCOP_1:87 ;
A8: IC (Computation (s2 +* (I +* (Start-At (insloc 0 )))),0 ) = (I +* (Start-At (insloc 0 ))) . (IC SCM+FSA ) by A4, A5, A6, FUNCT_4:14
.= (Start-At (insloc 0 )) . (IC SCM+FSA ) by A4, FUNCT_4:14
.= insloc 0 by FUNCOP_1:87 ;
A9: I c= I +* (Start-At (insloc 0 )) by SCMFSA8A:9;
then A10: dom I c= dom (I +* (Start-At (insloc 0 ))) by GRFUNC_1:8;
A11: insloc 0 in dom I by A2, Th3;
then A12: CurInstr (Computation (s1 +* (I +* (Start-At (insloc 0 )))),0 ) = (I +* (Start-At (insloc 0 ))) . (insloc 0 ) by A6, A7, A10, FUNCT_4:14
.= CurInstr (Computation (s2 +* (I +* (Start-At (insloc 0 )))),0 ) by A6, A8, A10, A11, FUNCT_4:14 ;
Computation (s1 +* (I +* (Start-At (insloc 0 )))),0 , Computation (s2 +* (I +* (Start-At (insloc 0 )))),0 equal_outside NAT by A1, A6, Th7;
then A13: S₁[ 0 ] by A7, A8, A12, SCMFSA6A:39;

A14: now

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A15: S₁[k] ; :: thesis: S₁[k + 1]
then ( ( for a being Int-Location holds (Computation (s1 +* (I +* (Start-At (insloc 0 )))),k) . a = (Computation (s2 +* (I +* (Start-At (insloc 0 )))),k) . a ) & ( for f being FinSeq-Location holds (Computation (s1 +* (I +* (Start-At (insloc 0 )))),k) . f = (Computation (s2 +* (I +* (Start-At (insloc 0 )))),k) . f ) ) by SCMFSA6A:38;
then A16: Computation (s1 +* (I +* (Start-At (insloc 0 )))),k, Computation (s2 +* (I +* (Start-At (insloc 0 )))),k equal_outside NAT by A15, SCMFSA6A:28;
( I +* (Start-At (insloc 0 )) c= s1 +* (I +* (Start-At (insloc 0 ))) & I +* (Start-At (insloc 0 )) c= s2 +* (I +* (Start-At (insloc 0 ))) ) by FUNCT_4:26;
then ( I c= s1 +* (I +* (Start-At (insloc 0 ))) & I c= s2 +* (I +* (Start-At (insloc 0 ))) ) by A9, XBOOLE_1:1;
then A17: ( I c= Computation (s1 +* (I +* (Start-At (insloc 0 )))),(k + 1) & I c= Computation (s2 +* (I +* (Start-At (insloc 0 )))),(k + 1) ) by AMI_1:81;
A18: Computation (s1 +* (I +* (Start-At (insloc 0 )))),(k + 1) = Following (Computation (s1 +* (I +* (Start-At (insloc 0 )))),k) by AMI_1:14
.= Exec (CurInstr (Computation (s1 +* (I +* (Start-At (insloc 0 )))),k)),(Computation (s1 +* (I +* (Start-At (insloc 0 )))),k) ;
thus S₁[k + 1] :: thesis: verum

proof

A19: Computation (s2 +* (I +* (Start-At (insloc 0 )))),(k + 1) = Following (Computation (s2 +* (I +* (Start-At (insloc 0 )))),k) by AMI_1:14
.= Exec (CurInstr (Computation (s2 +* (I +* (Start-At (insloc 0 )))),k)),(Computation (s2 +* (I +* (Start-At (insloc 0 )))),k) ;
hence A20: IC (Computation (s1 +* (I +* (Start-At (insloc 0 )))),(k + 1)) = IC (Computation (s2 +* (I +* (Start-At (insloc 0 )))),(k + 1)) by A15, A16, A18, AMI_1:121, SCMFSA6A:32; :: thesis: ( CurInstr (Computation (s1 +* (I +* (Start-At (insloc 0 )))),(k + 1)) = CurInstr (Computation (s2 +* (I +* (Start-At (insloc 0 )))),(k + 1)) & DataPart (Computation (s1 +* (I +* (Start-At (insloc 0 )))),(k + 1)) = DataPart (Computation (s2 +* (I +* (Start-At (insloc 0 )))),(k + 1)) )
A21: IC (Computation (s1 +* (I +* (Start-At (insloc 0 )))),(k + 1)) in dom I by A2, SCMFSA7B:def 7;
hence CurInstr (Computation (s1 +* (I +* (Start-At (insloc 0 )))),(k + 1)) = I . (IC (Computation (s1 +* (I +* (Start-At (insloc 0 )))),(k + 1))) by A17, GRFUNC_1:8
.= CurInstr (Computation (s2 +* (I +* (Start-At (insloc 0 )))),(k + 1)) by A17, A20, A21, GRFUNC_1:8 ;
:: thesis: DataPart (Computation (s1 +* (I +* (Start-At (insloc 0 )))),(k + 1)) = DataPart (Computation (s2 +* (I +* (Start-At (insloc 0 )))),(k + 1))
thus DataPart (Computation (s1 +* (I +* (Start-At (insloc 0 )))),(k + 1)) = DataPart (Computation (s2 +* (I +* (Start-At (insloc 0 )))),(k + 1)) by A15, A16, A18, A19, SCMFSA6A:32, SCMFSA6A:39; :: thesis: verum

end;

end;

for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A13, A14);
then CurInstr (Computation (s2 +* (I +* (Start-At (insloc 0 )))),m) = halt SCM+FSA by A3;
then A22: s2 +* (I +* (Start-At (insloc 0 ))) is halting by AMI_1:def 20;

now

let k be Element of NAT ; :: thesis: IC (Computation (s2 +* (I +* (Start-At (insloc 0 )))),k) in dom I
A23: IC (Computation (s1 +* (I +* (Start-At (insloc 0 )))),k) in dom I by A2, SCMFSA7B:def 7;
for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A13, A14);
hence IC (Computation (s2 +* (I +* (Start-At (insloc 0 )))),k) in dom I by A23; :: thesis: verum

end;

hence I is_closed_on s2 by SCMFSA7B:def 7; :: thesis: I is_halting_on s2
thus I is_halting_on s2 by A22, SCMFSA7B:def 8; :: thesis: verum