let I be Program of SCM+FSA; :: thesis: ( I is keepInt0_1 implies I is InitClosed )
assume A10: 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 P being Instruction-Sequence of SCM+FSA st I c= P holds
for n being Element of NAT st Initialize ((intloc 0) .--> 1) c= s holds
IC (Comput (P,s,n)) in dom I
let p be Instruction-Sequence of SCM+FSA; :: thesis: ( I c= p implies for n being Element of NAT st Initialize ((intloc 0) .--> 1) c= s holds
IC (Comput (p,s,n)) in dom I )
assume A11: I c= p ; :: thesis: for n being Element of NAT st Initialize ((intloc 0) .--> 1) c= s holds
IC (Comput (p,s,n)) in dom I
let n be Element of NAT ; :: thesis: ( Initialize ((intloc 0) .--> 1) c= s implies IC (Comput (p,s,n)) in dom I )
assume A12: Initialize ((intloc 0) .--> 1) c= s ; :: thesis: IC (Comput (p,s,n)) in dom I
then A13: Start-At (0,SCM+FSA) c= s by Lm2, XBOOLE_1:1;
defpred S₁[ Nat] means not IC (Comput (p,s,c₁)) in dom I;
assume not IC (Comput (p,s,n)) in dom I ; :: thesis: contradiction
then A14: ex n being Nat st S₁[n] ;
consider n being Nat such that
A15: S₁[n] and
A16: for m being Nat st S₁[m] holds
n <= m from NAT_1:sch 5(A14);
reconsider n = n as Element of NAT by ORDINAL1:def 12;
set s2 = Comput (p,s,n);
set p0 = p +* ((IC (Comput (p,s,n))),((intloc 0) := (FirstNotUsed I)));
set s0 = s +* ((FirstNotUsed I),((s . (intloc 0)) + 1));
reconsider s = s as State of SCM+FSA ;
reconsider s0 = s +* ((FirstNotUsed I),((s . (intloc 0)) + 1)) as State of SCM+FSA ;
not I is keepInt0_1

proof

FirstNotUsed I <> IC by SCMFSA_2:56;
then A17: not FirstNotUsed I in {(IC )} by TARSKI:def 1;
set s02 = Comput ((p +* ((IC (Comput (p,s,n))),((intloc 0) := (FirstNotUsed I)))),s0,n);
set iIC = {(intloc 0)} \/ {(IC )};
take s0 ; :: according to SCM_HALT:def 3 :: thesis: ( Initialize ((intloc 0) .--> 1) c= s0 & ex p being Instruction-Sequence of SCM+FSA st
( I c= p & not for k being Element of NAT holds (Comput (p,s0,k)) . (intloc 0) = 1 ) )
FirstNotUsed I in dom s by SCMFSA_2:42;
then A18: s0 . (FirstNotUsed I) = (s . (intloc 0)) + 1 by FUNCT_7:31;
A19: s . (intloc 0) = 1 by A12, SCMFSA_M:30;
A20: not FirstNotUsed I in UsedIntLoc I by SF_MASTR:50;
not FirstNotUsed I in {(intloc 0)} by TARSKI:def 1;
then not FirstNotUsed I in dom (Initialize ((intloc 0) .--> 1)) by Lm3, A17, XBOOLE_0:def 3;
hence Initialize ((intloc 0) .--> 1) c= s0 by A12, FUNCT_7:89; :: thesis: ex p being Instruction-Sequence of SCM+FSA st
( I c= p & not for k being Element of NAT holds (Comput (p,s0,k)) . (intloc 0) = 1 )
then A21: Start-At (0,SCM+FSA) c= s0 by Lm2, XBOOLE_1:1;
take p +* ((IC (Comput (p,s,n))),((intloc 0) := (FirstNotUsed I))) ; :: thesis: ( I c= p +* ((IC (Comput (p,s,n))),((intloc 0) := (FirstNotUsed I))) & not for k being Element of NAT holds (Comput ((p +* ((IC (Comput (p,s,n))),((intloc 0) := (FirstNotUsed I)))),s0,k)) . (intloc 0) = 1 )
thus A22: I c= p +* ((IC (Comput (p,s,n))),((intloc 0) := (FirstNotUsed I))) by A11, A15, FUNCT_7:89; :: thesis: not for k being Element of NAT holds (Comput ((p +* ((IC (Comput (p,s,n))),((intloc 0) := (FirstNotUsed I)))),s0,k)) . (intloc 0) = 1
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:def 5;
hence contradiction by SCMFSA_2:58; :: thesis: verum

end;

then A23: s0 | (UsedInt*Loc I) = s | (UsedInt*Loc I) by FUNCT_7:92;
A24: s0 | (UsedIntLoc I) = s | (UsedIntLoc I) by FUNCT_7:92, SF_MASTR:50;
A25: for m being Element of NAT st m < n holds
IC (Comput (p,s,m)) in dom I by A16;
A26: IC (Comput ((p +* ((IC (Comput (p,s,n))),((intloc 0) := (FirstNotUsed I)))),s0,n)) = IC (Comput (p,s,n)) by A24, A23, A11, A22, A21, A25, A13, SF_MASTR:65;
take k = n + 1; :: thesis: not (Comput ((p +* ((IC (Comput (p,s,n))),((intloc 0) := (FirstNotUsed I)))),s0,k)) . (intloc 0) = 1
IC (Comput (p,s,n)) in NAT ;
then A27: IC (Comput (p,s,n)) in dom p by PARTFUN1:def 2;
A28: (p +* ((IC (Comput (p,s,n))),((intloc 0) := (FirstNotUsed I)))) . (IC (Comput (p,s,n))) = (intloc 0) := (FirstNotUsed I) by A27, FUNCT_7:31;
A29: Comput ((p +* ((IC (Comput (p,s,n))),((intloc 0) := (FirstNotUsed I)))),s0,k) = Following ((p +* ((IC (Comput (p,s,n))),((intloc 0) := (FirstNotUsed I)))),(Comput ((p +* ((IC (Comput (p,s,n))),((intloc 0) := (FirstNotUsed I)))),s0,n))) by EXTPRO_1:3
.= Exec (((intloc 0) := (FirstNotUsed I)),(Comput ((p +* ((IC (Comput (p,s,n))),((intloc 0) := (FirstNotUsed I)))),s0,n))) by A26, A28, PBOOLE:143 ;
for m being Element of NAT st m < n holds
IC (Comput ((p +* ((IC (Comput (p,s,n))),((intloc 0) := (FirstNotUsed I)))),s0,m)) in dom I by A25, A24, A23, A11, A22, A21, A13, SF_MASTR:65;
then (Comput ((p +* ((IC (Comput (p,s,n))),((intloc 0) := (FirstNotUsed I)))),s0,n)) . (FirstNotUsed I) = 1 + 1 by A20, A18, A11, A15, A19, FUNCT_7:89, SF_MASTR:61;
hence not (Comput ((p +* ((IC (Comput (p,s,n))),((intloc 0) := (FirstNotUsed I)))),s0,k)) . (intloc 0) = 1 by A29, SCMFSA_2:63; :: thesis: verum

end;

hence contradiction by A10; :: thesis: verum