let I be Program of SCM+FSA ; :: thesis: ( I is keepInt0_1 implies I is InitClosed )
assume A17: I is keepInt0_1 ; :: thesis: I is InitClosed
set FI = FirstNotUsed I;
let s be State of SCM+FSA ; :: according to SCM_HALT:def 1 :: thesis: for n being Element of NAT st Initialized I c= s holds
IC (Comput (ProgramPart s),s,n) in dom I
let n be Element of NAT ; :: thesis: ( Initialized I c= s implies IC (Comput (ProgramPart s),s,n) in dom I )
assume A18: Initialized I c= s ; :: thesis: IC (Comput (ProgramPart s),s,n) in dom I
defpred S1[ Nat] means not IC (Comput (ProgramPart s),s,c1) in dom I;
assume not IC (Comput (ProgramPart s),s,n) in dom I ; :: thesis: contradiction
then A19: ex n being Nat st S1[n] ;
consider n being Nat such that
A20: S1[n] and
A21: for m being Nat st S1[m] holds
n <= m from NAT_1:sch 5(A19);
 reconsider n = n as Element of NAT by ORDINAL1:def 13;
set s2 = Comput (ProgramPart s),s,n;
set s00 = s +* (IC (Comput (ProgramPart s),s,n)),((intloc 0 ) := (FirstNotUsed I));
set s0 = (s +* (IC (Comput (ProgramPart s),s,n)),((intloc 0 ) := (FirstNotUsed I))) +* (FirstNotUsed I),((s . (intloc 0 )) + 1);
reconsider s00 = s +* (IC (Comput (ProgramPart s),s,n)),((intloc 0 ) := (FirstNotUsed I)) as State of SCM+FSA ;
reconsider s0 = (s +* (IC (Comput (ProgramPart s),s,n)),((intloc 0 ) := (FirstNotUsed I))) +* (FirstNotUsed I),((s . (intloc 0 )) + 1) as State of SCM+FSA ;
A22: dom I c= NAT by RELAT_1:def 18;
not I is keepInt0_1
proof
A23: not FirstNotUsed I in dom I by A22, SCMFSA_2:84;
FirstNotUsed I <> IC SCM+FSA by SCMFSA_2:81;
then A24: not FirstNotUsed I in {(IC SCM+FSA )} by TARSKI:def 1;
set s02 = Comput (ProgramPart s0),s0,n;
set iIC = {(intloc 0 )} \/ {(IC SCM+FSA )};
set IS = Initialized I;
take s0 ; :: according to SCM_HALT:def 3 :: thesis: ( Initialized I c= s0 & not for k being Element of NAT holds (Comput (ProgramPart s0),s0,k) . (intloc 0 ) = 1 )
A25: dom (Initialized I) = ((dom I) \/ {(intloc 0 )}) \/ {(IC SCM+FSA )} by SCMFSA6A:43
.= (dom I) \/ ({(intloc 0 )} \/ {(IC SCM+FSA )}) by XBOOLE_1:4 ;
FirstNotUsed I in dom s00 by SCMFSA_2:66;
then A26: s0 . (FirstNotUsed I) = (s . (intloc 0 )) + 1 by FUNCT_7:33;
IC (Comput (ProgramPart s),s,n) <> intloc 0 by SCMFSA_2:84;
then A27: not IC (Comput (ProgramPart s),s,n) in {(intloc 0 )} by TARSKI:def 1;
A28: ( not FirstNotUsed I in UsedIntLoc I & s . (intloc 0 ) = 1 ) by A18, Th7, SF_MASTR:54;
IC (Comput (ProgramPart s),s,n) <> IC SCM+FSA by AMI_1:48;
then not IC (Comput (ProgramPart s),s,n) in {(IC SCM+FSA )} by TARSKI:def 1;
then not IC (Comput (ProgramPart s),s,n) in {(intloc 0 )} \/ {(IC SCM+FSA )} by A27, XBOOLE_0:def 3;
then not IC (Comput (ProgramPart s),s,n) in dom (Initialized I) by A20, A25, XBOOLE_0:def 3;
then A29: Initialized I c= s00 by A18, FUNCT_7:91;
not FirstNotUsed I in {(intloc 0 )} by TARSKI:def 1;
then not FirstNotUsed I in {(intloc 0 )} \/ {(IC SCM+FSA )} by A24, XBOOLE_0:def 3;
then not FirstNotUsed I in dom (Initialized I) by A25, A23, XBOOLE_0:def 3;
hence Initialized I c= s0 by A29, FUNCT_7:91; :: thesis: not for k being Element of NAT holds (Comput (ProgramPart s0),s0,k) . (intloc 0 ) = 1
then A30: I +* (Start-At 0 ,SCM+FSA ) c= s0 by SCMFSA6B:8;
A31: not IC (Comput (ProgramPart s),s,n) in UsedInt*Loc I
proof
assume IC (Comput (ProgramPart s),s,n) in UsedInt*Loc I ; :: thesis: contradiction
then IC (Comput (ProgramPart s),s,n) is FinSeq-Location by SCMFSA_2:12;
hence contradiction by SCMFSA_2:85; :: thesis: verum
end;
not FirstNotUsed I in UsedInt*Loc I
proof
assume FirstNotUsed I in UsedInt*Loc I ; :: thesis: contradiction
then FirstNotUsed I is FinSeq-Location by SCMFSA_2:12;
hence contradiction by SCMFSA_2:83; :: thesis: verum
end;
then A32: s0 | (UsedInt*Loc I) = s00 | (UsedInt*Loc I) by FUNCT_7:94
.= s | (UsedInt*Loc I) by A31, FUNCT_7:94 ;
A33: not IC (Comput (ProgramPart s),s,n) in UsedIntLoc I
proof
assume IC (Comput (ProgramPart s),s,n) in UsedIntLoc I ; :: thesis: contradiction
then IC (Comput (ProgramPart s),s,n) is Int-Location by SCMFSA_2:11;
hence contradiction by SCMFSA_2:84; :: thesis: verum
end;
A34: s0 | (UsedIntLoc I) = s00 | (UsedIntLoc I) by FUNCT_7:94, SF_MASTR:54
.= s | (UsedIntLoc I) by A33, FUNCT_7:94 ;
A35: ( I +* (Start-At 0 ,SCM+FSA ) c= s & ( for m being Element of NAT st m < n holds
IC (Comput (ProgramPart s),s,m) in dom I ) ) by A18, A21, SCMFSA6B:8;
then A36: IC (Comput (ProgramPart s0),s0,n) = IC (Comput (ProgramPart s),s,n) by A30, A34, A32, SF_MASTR:73;
take k = n + 1; :: thesis: not (Comput (ProgramPart s0),s0,k) . (intloc 0 ) = 1
A37: IC (Comput (ProgramPart s),s,n) in dom s by AMI_1:116;
IC (Comput (ProgramPart s),s,n) <> FirstNotUsed I by SCMFSA_2:84;
then A38: s0 . (IC (Comput (ProgramPart s),s,n)) = s00 . (IC (Comput (ProgramPart s),s,n)) by FUNCT_7:34
.= (intloc 0 ) := (FirstNotUsed I) by A37, FUNCT_7:33 ;
Y: (ProgramPart (Comput (ProgramPart s0),s0,n)) /. (IC (Comput (ProgramPart s0),s0,n)) = (Comput (ProgramPart s0),s0,n) . (IC (Comput (ProgramPart s0),s0,n)) by AMI_1:150;
T: ProgramPart s0 = ProgramPart (Comput (ProgramPart s0),s0,n) by AMI_1:144;
A39: Comput (ProgramPart s0),s0,k = Following (ProgramPart s0),(Comput (ProgramPart s0),s0,n) by AMI_1:14
.= Exec ((intloc 0 ) := (FirstNotUsed I)),(Comput (ProgramPart s0),s0,n) by A36, A38, AMI_1:54, Y, T ;
for m being Element of NAT st m < n holds
IC (Comput (ProgramPart s0),s0,m) in dom I by A30, A35, A34, A32, SF_MASTR:73;
then (Comput (ProgramPart s0),s0,n) . (FirstNotUsed I) = 1 + 1 by A30, A28, A26, SF_MASTR:69;
hence not (Comput (ProgramPart s0),s0,k) . (intloc 0 ) = 1 by A39, SCMFSA_2:89; :: thesis: verum
end;
hence contradiction by A17; :: thesis: verum