let I be Program of SCM+FSA; :: thesis: ( I is keeping_0 implies I is paraclosed )
assume A17: I is keeping_0 ; :: thesis: I is paraclosed
set FI = FirstNotUsed I;
let s be State of SCM+FSA; :: according to SCMFSA6B:def 2 :: thesis: for n being Element of NAT st I +* (Start-At (0,SCM+FSA)) c= s holds
IC (Comput ((ProgramPart s),s,n)) in dom I
let n be Element of NAT ; :: thesis: ( I +* (Start-At (0,SCM+FSA)) c= s implies IC (Comput ((ProgramPart s),s,n)) in dom I )
assume A18: I +* (Start-At (0,SCM+FSA)) 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);
reconsider s00 = s +* ((IC (Comput ((ProgramPart s),s,n))),((intloc 0) := (FirstNotUsed I))) as State of SCM+FSA ;
reconsider s0 = s00 +* ((FirstNotUsed I),((s . (intloc 0)) + 1)) as State of SCM+FSA ;
A22: dom I c= NAT by RELAT_1:def 18;
not I is keeping_0
proof
A23: 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 A24: s0 | (UsedInt*Loc I) = s00 | (UsedInt*Loc I) by FUNCT_7:94
.= s | (UsedInt*Loc I) by A23, FUNCT_7:94 ;
A25: not FirstNotUsed I in dom I by A22, SCMFSA_2:84;
A27: s . (intloc 0) < (s . (intloc 0)) + 1 by XREAL_1:31;
A28: 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 A29: s0 . (IC (Comput ((ProgramPart s),s,n))) = s00 . (IC (Comput ((ProgramPart s),s,n))) by FUNCT_7:34
.= (intloc 0) := (FirstNotUsed I) by A28, FUNCT_7:33 ;
A30: s0 . (intloc 0) = s00 . (intloc 0) by FUNCT_7:34
.= s . (intloc 0) by FUNCT_7:34, SCMFSA_2:84 ;
FirstNotUsed I in dom s00 by SCMFSA_2:66;
then A31: s0 . (FirstNotUsed I) = (s . (intloc 0)) + 1 by FUNCT_7:33;
set s02 = Comput ((ProgramPart s0),s0,n);
set IS = I +* (Start-At (0,SCM+FSA));
take s0 ; :: according to SCMFSA6B:def 4 :: thesis: ( I +* (Start-At (0,SCM+FSA)) c= s0 & not for k being Element of NAT holds (Comput ((ProgramPart s0),s0,k)) . (intloc 0) = s0 . (intloc 0) )
A32: dom (I +* (Start-At (0,SCM+FSA))) = (dom I) \/ (dom (Start-At (0,SCM+FSA))) by FUNCT_4:def 1
.= (dom I) \/ {(IC SCM+FSA)} by FUNCOP_1:19 ;
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 dom (I +* (Start-At (0,SCM+FSA))) by A20, A32, XBOOLE_0:def 3;
then A33: I +* (Start-At (0,SCM+FSA)) c= s00 by A18, FUNCT_7:91;
FirstNotUsed I <> IC SCM+FSA by SCMFSA_2:81;
then not FirstNotUsed I in {(IC SCM+FSA)} by TARSKI:def 1;
then A34: not FirstNotUsed I in dom (I +* (Start-At (0,SCM+FSA))) by A32, A25, XBOOLE_0:def 3;
hence A35: I +* (Start-At (0,SCM+FSA)) c= s0 by A33, FUNCT_7:91; :: thesis: not for k being Element of NAT holds (Comput ((ProgramPart s0),s0,k)) . (intloc 0) = s0 . (intloc 0)
take k = n + 1; :: thesis: not (Comput ((ProgramPart s0),s0,k)) . (intloc 0) = s0 . (intloc 0)
A36: 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;
A37: s0 | (UsedIntLoc I) = s00 | (UsedIntLoc I) by FUNCT_7:94, SF_MASTR:54
.= s | (UsedIntLoc I) by A36, FUNCT_7:94 ;
A38: for m being Element of NAT st m < n holds
IC (Comput ((ProgramPart s),s,m)) in dom I by A21;
then A39: IC (Comput ((ProgramPart s0),s0,n)) = IC (Comput ((ProgramPart s),s,n)) by A18, A35, A37, A24, SF_MASTR:73;
( not FirstNotUsed I in UsedIntLoc I & ( for m being Element of NAT st m < n holds
IC (Comput ((ProgramPart s0),s0,m)) in dom I ) ) by A18, A35, A38, A37, A24, SF_MASTR:54, SF_MASTR:73;
then A40: (Comput ((ProgramPart s0),s0,n)) . (FirstNotUsed I) = (s . (intloc 0)) + 1 by A33, A34, A31, FUNCT_7:91, SF_MASTR:69;
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;
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 A39, A29, Y, T, AMI_1:54 ;
hence not (Comput ((ProgramPart s0),s0,k)) . (intloc 0) = s0 . (intloc 0) by A40, A30, A27, SCMFSA_2:89; :: thesis: verum
end;
hence contradiction by A17; :: thesis: verum