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 the Instructions of SCM+FSA -valued ManySortedSet of NAT st I c= P holds
for n being Element of NAT st Initialized I c= s holds
IC (Comput (P,s,n)) in dom I
let p be the Instructions of SCM+FSA -valued ManySortedSet of NAT ; :: thesis: ( I c= p implies for n being Element of NAT st Initialized I c= s holds
IC (Comput (p,s,n)) in dom I )
assume A18: I c= p ; :: thesis: for n being Element of NAT st Initialized I c= s holds
IC (Comput (p,s,n)) in dom I
let n be Element of NAT ; :: thesis: ( Initialized I c= s implies IC (Comput (p,s,n)) in dom I )
assume A19: Initialized I c= s ; :: thesis: IC (Comput (p,s,n)) in dom I
defpred S1[ Nat] means not IC (Comput (p,s,c1)) in dom I;
assume not IC (Comput (p,s,n)) in dom I ; :: thesis: contradiction
then A20: ex n being Nat st S1[n] ;
consider n being Nat such that
A21: S1[n] and
A22: for m being Nat st S1[m] holds
n <= m from NAT_1:sch 5(A20);
 reconsider n = n as Element of NAT by ORDINAL1:def 13;
set s2 = Comput (p,s,n);
set s00 = s +* ((IC (Comput (p,s,n))),((intloc 0) := (FirstNotUsed I)));
set p2 = p;
set p00 = p +* ((IC (Comput (p,s,n))),((intloc 0) := (FirstNotUsed I)));
set s0 = (s +* ((IC (Comput (p,s,n))),((intloc 0) := (FirstNotUsed I)))) +* ((FirstNotUsed I),((s . (intloc 0)) + 1));
set p0 = p +* ((IC (Comput (p,s,n))),((intloc 0) := (FirstNotUsed I)));
reconsider s00 = s +* ((IC (Comput (p,s,n))),((intloc 0) := (FirstNotUsed I))) as State of SCM+FSA ;
reconsider s0 = (s +* ((IC (Comput (p,s,n))),((intloc 0) := (FirstNotUsed I)))) +* ((FirstNotUsed I),((s . (intloc 0)) + 1)) as State of SCM+FSA ;
A23: dom I c= NAT by RELAT_1:def 18;
not I is keepInt0_1
proof
A24: not FirstNotUsed I in dom I by A23, SCMFSA_2:84;
FirstNotUsed I <> IC by SCMFSA_2:81;
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 )};
set IS = Initialized I;
take s0 ; :: according to SCM_HALT:def 3 :: thesis: ( Initialized I c= s0 & ex p being the Instructions of SCM+FSA -valued ManySortedSet of NAT st
( I c= p & not for k being Element of NAT holds (Comput (p,s0,k)) . (intloc 0) = 1 ) )
A26: dom (Initialized I) = ((dom I) \/ {(intloc 0)}) \/ {(IC )} by SCMFSA6A:43
.= (dom I) \/ ({(intloc 0)} \/ {(IC )}) by XBOOLE_1:4 ;
FirstNotUsed I in dom s00 by SCMFSA_2:66;
then A27: s0 . (FirstNotUsed I) = (s . (intloc 0)) + 1 by FUNCT_7:33;
IC (Comput (p,s,n)) <> intloc 0 by SCMFSA_2:84;
then A28: not IC (Comput (p,s,n)) in {(intloc 0)} by TARSKI:def 1;
A29: ( not FirstNotUsed I in UsedIntLoc I & s . (intloc 0) = 1 ) by A19, Th7, SF_MASTR:54;
IC (Comput (p,s,n)) <> IC by COMPOS_1:3;
then not IC (Comput (p,s,n)) in {(IC )} by TARSKI:def 1;
then not IC (Comput (p,s,n)) in {(intloc 0)} \/ {(IC )} by A28, XBOOLE_0:def 3;
then not IC (Comput (p,s,n)) in dom (Initialized I) by A21, A26, XBOOLE_0:def 3;
then A30: Initialized I c= s00 by A19, FUNCT_7:91;
not FirstNotUsed I in {(intloc 0)} by TARSKI:def 1;
then not FirstNotUsed I in {(intloc 0)} \/ {(IC )} by A25, XBOOLE_0:def 3;
then not FirstNotUsed I in dom (Initialized I) by A26, A24, XBOOLE_0:def 3;
hence Initialized I c= s0 by A30, FUNCT_7:91; :: thesis: ex p being the Instructions of SCM+FSA -valued ManySortedSet of NAT st
( I c= p & not for k being Element of NAT holds (Comput (p,s0,k)) . (intloc 0) = 1 )
then A31: Initialize I c= s0 by SCMFSA6B:8;
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 )
not IC (Comput (p,s,n)) in dom I by A21;
hence A32: I c= p +* ((IC (Comput (p,s,n))),((intloc 0) := (FirstNotUsed I))) by A18, FUNCT_7:91; :: 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
A33: not IC (Comput (p,s,n)) in UsedInt*Loc I
proof
assume IC (Comput (p,s,n)) in UsedInt*Loc I ; :: thesis: contradiction
then IC (Comput (p,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 A34: s0 | (UsedInt*Loc I) = s00 | (UsedInt*Loc I) by FUNCT_7:94
.= s | (UsedInt*Loc I) by A33, FUNCT_7:94 ;
A35: not IC (Comput (p,s,n)) in UsedIntLoc I
proof
assume IC (Comput (p,s,n)) in UsedIntLoc I ; :: thesis: contradiction
then IC (Comput (p,s,n)) is Int-Location by SCMFSA_2:11;
hence contradiction by SCMFSA_2:84; :: thesis: verum
end;
A36: s0 | (UsedIntLoc I) = s00 | (UsedIntLoc I) by FUNCT_7:94, SF_MASTR:54
.= s | (UsedIntLoc I) by A35, FUNCT_7:94 ;
A37: ( Initialize I c= s & ( for m being Element of NAT st m < n holds
IC (Comput (p,s,m)) in dom I ) ) by A19, A22, SCMFSA6B:8;
then A38: IC (Comput ((p +* ((IC (Comput (p,s,n))),((intloc 0) := (FirstNotUsed I)))),s0,n)) = IC (Comput (p,s,n)) by A31, A36, A34, SF_MASTR:73, A18, A32;
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 4;
A40: (p +* ((IC (Comput (p,s,n))),((intloc 0) := (FirstNotUsed I)))) . (IC (Comput (p,s,n))) = (p +* ((IC (Comput (p,s,n))),((intloc 0) := (FirstNotUsed I)))) . (IC (Comput (p,s,n)))
.= (intloc 0) := (FirstNotUsed I) by FUNCT_7:33, A39 ;
A41: CurInstr ((p +* ((IC (Comput (p,s,n))),((intloc 0) := (FirstNotUsed I)))),(Comput ((p +* ((IC (Comput (p,s,n))),((intloc 0) := (FirstNotUsed I)))),s0,n))) = (p +* ((IC (Comput (p,s,n))),((intloc 0) := (FirstNotUsed I)))) . (IC (Comput ((p +* ((IC (Comput (p,s,n))),((intloc 0) := (FirstNotUsed I)))),s0,n))) by PBOOLE:158
.= (intloc 0) := (FirstNotUsed I) by A38, A40 ;
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:4
.= Exec (((intloc 0) := (FirstNotUsed I)),(Comput ((p +* ((IC (Comput (p,s,n))),((intloc 0) := (FirstNotUsed I)))),s0,n))) by A41 ;
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 A31, A37, A36, A34, SF_MASTR:73, A18, A32;
then (Comput ((p +* ((IC (Comput (p,s,n))),((intloc 0) := (FirstNotUsed I)))),s0,n)) . (FirstNotUsed I) = 1 + 1 by A31, A29, A27, SF_MASTR:69, A32;
hence not (Comput ((p +* ((IC (Comput (p,s,n))),((intloc 0) := (FirstNotUsed I)))),s0,k)) . (intloc 0) = 1 by A42, SCMFSA_2:89; :: thesis: verum
end;
hence contradiction by A17; :: thesis: verum