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 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 A18: 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 A19: Initialize ((intloc 0) .--> 1) c= s ; :: thesis: IC (Comput (p,s,n)) in dom I
then B19: Start-At (0,SCM+FSA) c= s by zSA0, 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 A20: ex n being Nat st S₁[n] ;
consider n being Nat such that
A21: S₁[n] and
A22: for m being Nat st S₁[m] holds
n <= m from NAT_1:sch 5(A20);
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 A25: 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 A27: s0 . (FirstNotUsed I) = (s . (intloc 0)) + 1 by FUNCT_7:31;
B29: s . (intloc 0) = 1 by A19, Th7;
A29: 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 diS, A25, XBOOLE_0:def 3;
hence Initialize ((intloc 0) .--> 1) c= s0 by A19, 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 B31: Start-At (0,SCM+FSA) c= s0 by zSA0, 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 A32: I c= p +* ((IC (Comput (p,s,n))),((intloc 0) := (FirstNotUsed I))) by A18, A21, 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:5;
hence contradiction by SCMFSA_2:58; :: thesis: verum

end;

then A34: s0 | (UsedInt*Loc I) = s | (UsedInt*Loc I) by FUNCT_7:92;
A36: s0 | (UsedIntLoc I) = s | (UsedIntLoc I) by FUNCT_7:92, SF_MASTR:50;
A37: for m being Element of NAT st m < n holds
IC (Comput (p,s,m)) in dom I by A22;
A38: IC (Comput ((p +* ((IC (Comput (p,s,n))),((intloc 0) := (FirstNotUsed I)))),s0,n)) = IC (Comput (p,s,n)) by A36, A34, A18, A32, B31, A37, B19, 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 A39: IC (Comput (p,s,n)) in dom p by PARTFUN1:def 2;
A40: (p +* ((IC (Comput (p,s,n))),((intloc 0) := (FirstNotUsed I)))) . (IC (Comput (p,s,n))) = (intloc 0) := (FirstNotUsed I) by A39, FUNCT_7:31;
A42: 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 A38, A40, 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 A37, A36, A34, A18, A32, B31, B19, SF_MASTR:65;
then (Comput ((p +* ((IC (Comput (p,s,n))),((intloc 0) := (FirstNotUsed I)))),s0,n)) . (FirstNotUsed I) = 1 + 1 by A29, A27, A18, A21, B29, 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 A42, SCMFSA_2:63; :: thesis: verum

end;

hence contradiction by A17; :: thesis: verum