let I be Program of ; :: thesis: ( I is keeping_0 implies I is paraclosed )
assume A16: I is keeping_0 ; :: thesis: I is paraclosed
set FI = FirstNotUsed I;
let s be 0 -started State of SCM+FSA; :: according to AMISTD_1:def 10 :: thesis: for b₁ being set holds
( not I c= b₁ or for b₂ being Element of NAT holds IC (Comput (b₁,s,b₂)) in K325(NAT,I) )
let P be Instruction-Sequence of SCM+FSA; :: thesis: ( not I c= P or for b₁ being Element of NAT holds IC (Comput (P,s,b₁)) in K325(NAT,I) )
assume A17: I c= P ; :: thesis: for b₁ being Element of NAT holds IC (Comput (P,s,b₁)) in K325(NAT,I)
let n be Element of NAT ; :: thesis: IC (Comput (P,s,n)) in K325(NAT,I)
A18: Start-At (0,SCM+FSA) c= s by MEMSTR_0:29;
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 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 12;
set s2 = Comput (P,s,n);
set s00 = s;
reconsider s0 = s +* ((FirstNotUsed I),((s . (intloc 0)) + 1)) as State of SCM+FSA ;
set Q = P +* ((IC (Comput (P,s,n))),((intloc 0) := (FirstNotUsed I)));
A23: dom (P +* ((IC (Comput (P,s,n))),((intloc 0) := (FirstNotUsed I)))) = NAT by PARTFUN1:def 2;
not I is keeping_0

proof

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 A25: s0 | (UsedInt*Loc I) = s | (UsedInt*Loc I) by FUNCT_7:92;
A27: s . (intloc 0) < (s . (intloc 0)) + 1 by XREAL_1:29;
A28: dom P = NAT by PARTFUN1:def 2;
A29: (P +* ((IC (Comput (P,s,n))),((intloc 0) := (FirstNotUsed I)))) . (IC (Comput (P,s,n))) = (intloc 0) := (FirstNotUsed I) by A28, FUNCT_7:31;
A30: s0 . (intloc 0) = s . (intloc 0) by FUNCT_7:32;
FirstNotUsed I in dom s by SCMFSA_2:42;
then A31: s0 . (FirstNotUsed I) = (s . (intloc 0)) + 1 by FUNCT_7:31;
set s02 = Comput ((P +* ((IC (Comput (P,s,n))),((intloc 0) := (FirstNotUsed I)))),s0,n);
FirstNotUsed I <> IC by SCMFSA_2:56;
then not FirstNotUsed I in {(IC )} by TARSKI:def 1;
then not FirstNotUsed I in dom (Start-At (0,SCM+FSA)) by FUNCOP_1:13;
then B35: Start-At (0,SCM+FSA) c= s0 by A18, FUNCT_7:89;
then reconsider s0 = s0 as 0 -started State of SCM+FSA by MEMSTR_0:29;
take s0 ; :: according to SCMFSA6B:def 4 :: 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) = s0 . (intloc 0) )
A36: I c= P +* ((IC (Comput (P,s,n))),((intloc 0) := (FirstNotUsed I))) by A17, A20, FUNCT_7:138;
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) = s0 . (intloc 0) )
thus I c= P +* ((IC (Comput (P,s,n))),((intloc 0) := (FirstNotUsed I))) by A17, A20, FUNCT_7:138; :: thesis: not for k being Element of NAT holds (Comput ((P +* ((IC (Comput (P,s,n))),((intloc 0) := (FirstNotUsed I)))),s0,k)) . (intloc 0) = s0 . (intloc 0)
take k = n + 1; :: thesis: not (Comput ((P +* ((IC (Comput (P,s,n))),((intloc 0) := (FirstNotUsed I)))),s0,k)) . (intloc 0) = s0 . (intloc 0)
A38: s0 | (UsedIntLoc I) = s | (UsedIntLoc I) by FUNCT_7:92, SF_MASTR:50;
A39: for m being Element of NAT st m < n holds
IC (Comput (P,s,m)) in dom I by A21;
A40: ( not FirstNotUsed I in UsedIntLoc I & ( 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 A39, A38, A25, A17, A36, A18, B35, SF_MASTR:50, SF_MASTR:65;
A41: (Comput ((P +* ((IC (Comput (P,s,n))),((intloc 0) := (FirstNotUsed I)))),s0,n)) . (FirstNotUsed I) = (s . (intloc 0)) + 1 by A31, A40, A36, SF_MASTR:61;
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 (((P +* ((IC (Comput (P,s,n))),((intloc 0) := (FirstNotUsed I)))) . (IC (Comput ((P +* ((IC (Comput (P,s,n))),((intloc 0) := (FirstNotUsed I)))),s0,n)))),(Comput ((P +* ((IC (Comput (P,s,n))),((intloc 0) := (FirstNotUsed I)))),s0,n))) by A23, PARTFUN1:def 6
.= Exec (((intloc 0) := (FirstNotUsed I)),(Comput ((P +* ((IC (Comput (P,s,n))),((intloc 0) := (FirstNotUsed I)))),s0,n))) by A38, A25, A17, A36, A39, A29, A18, B35, SF_MASTR:65 ;
hence not (Comput ((P +* ((IC (Comput (P,s,n))),((intloc 0) := (FirstNotUsed I)))),s0,k)) . (intloc 0) = s0 . (intloc 0) by A41, A30, A27, SCMFSA_2:63; :: thesis: verum

end;

hence contradiction by A16; :: thesis: verum