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 (insloc 0 )) c= s holds
IC (Computation s,n) in dom I
let n be Element of NAT ; :: thesis: ( I +* (Start-At (insloc 0 )) c= s implies IC (Computation s,n) in dom I )
assume A18:
I +* (Start-At (insloc 0 )) c= s
; :: thesis: IC (Computation s,n) in dom I
defpred S1[ Nat] means not IC (Computation s,c1) in dom I;
assume
not IC (Computation 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 = Computation s,n;
reconsider s00 = s +* (IC (Computation 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 (Computation s,n) in UsedInt*Loc I
not
FirstNotUsed I in UsedInt*Loc I
then A24:
s0 | (UsedInt*Loc I) =
s00 | (UsedInt*Loc I)
by FUNCT_7:94
.=
s | (UsedInt*Loc I)
by A23, FUNCT_7:94
;
A27:
s . (intloc 0 ) < (s . (intloc 0 )) + 1
by XREAL_1:31;
A28:
IC (Computation s,n) in dom s
by AMI_1:116;
IC (Computation s,n) <> FirstNotUsed I
by SCMFSA_2:84;
then A29:
s0 . (IC (Computation s,n)) =
s00 . (IC (Computation 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 =
Computation s0,
n;
set IS =
I +* (Start-At (insloc 0 ));
take
s0
;
:: according to SCMFSA6B:def 4 :: thesis: ( I +* (Start-At (insloc 0 )) c= s0 & not for k being Element of NAT holds (Computation s0,k) . (intloc 0 ) = s0 . (intloc 0 ) )
A32:
dom (I +* (Start-At (insloc 0 ))) =
(dom I) \/ (dom (Start-At (insloc 0 )))
by FUNCT_4:def 1
.=
(dom I) \/ {(IC SCM+FSA )}
by FUNCOP_1:19
;
IC (Computation s,n) <> IC SCM+FSA
by AMI_1:48;
then
not
IC (Computation s,n) in {(IC SCM+FSA )}
by TARSKI:def 1;
then
not
IC (Computation s,n) in dom (I +* (Start-At (insloc 0 )))
by A20, A32, XBOOLE_0:def 3;
then A33:
I +* (Start-At (insloc 0 )) 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 (insloc 0 )))
by A32, A25, XBOOLE_0:def 3;
hence A35:
I +* (Start-At (insloc 0 )) c= s0
by A33, FUNCT_7:91;
:: thesis: not for k being Element of NAT holds (Computation s0,k) . (intloc 0 ) = s0 . (intloc 0 )
take k =
n + 1;
:: thesis: not (Computation s0,k) . (intloc 0 ) = s0 . (intloc 0 )
A36:
not
IC (Computation s,n) in UsedIntLoc I
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 (Computation s,m) in dom I
by A21;
then A39:
IC (Computation s0,n) = IC (Computation 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 (Computation s0,m) in dom I ) )
by A18, A35, A38, A37, A24, SF_MASTR:54, SF_MASTR:73;
then A40:
(Computation s0,n) . (FirstNotUsed I) = (s . (intloc 0 )) + 1
by A33, A34, A31, FUNCT_7:91, SF_MASTR:69;
Computation s0,
k =
Following (Computation s0,n)
by AMI_1:14
.=
Exec ((intloc 0 ) := (FirstNotUsed I)),
(Computation s0,n)
by A39, A29, AMI_1:54
;
hence
not
(Computation s0,k) . (intloc 0 ) = s0 . (intloc 0 )
by A40, A30, A27, SCMFSA_2:89;
:: thesis: verum
end;
hence
contradiction
by A17; :: thesis: verum