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 COMPOS_1:3;
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 COMPOS_1:23;
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 COMPOS_1:38;
T: ProgramPart s0 = ProgramPart (Comput ((ProgramPart s0),s0,n)) by AMI_1:123;
A39: Comput ((ProgramPart s0),s0,k) = Following ((ProgramPart s0),(Comput ((ProgramPart s0),s0,n))) by EXTPRO_1:4
.= Exec (((intloc 0) := (FirstNotUsed I)),(Comput ((ProgramPart s0),s0,n))) by A36, A38, Y, T, AMI_1:54 ;
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