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 S₁[ Nat] means not IC (Comput (ProgramPart s),s,c₁) in dom I;
assume not IC (Comput (ProgramPart s),s,n) in dom I ; :: thesis: contradiction
then A19: ex n being Nat st S₁[n] ;
consider n being Nat such that
A20: S₁[n] and
A21: for m being Nat st S₁[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 AMI_1:14
.= 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