let I be Program of SCM+FSA ; :: thesis: ( I is keeping_0 implies I is paraclosed )
assume A18:
I is keeping_0
; :: thesis: I is paraclosed
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 A19:
I +* (Start-At (insloc 0 )) c= s
; :: thesis: IC (Computation s,n) in dom I
A20:
dom I c= NAT
by RELAT_1:def 18;
defpred S1[ Nat] means not IC (Computation s,c1) in dom I;
assume
not IC (Computation s,n) in dom I
; :: thesis: contradiction
then A21:
ex n being Nat st S1[n]
;
consider n being Nat such that
A22:
S1[n]
and
A23:
for m being Nat st S1[m] holds
n <= m
from NAT_1:sch 5(A21);
reconsider n = n as Element of NAT by ORDINAL1:def 13;
set FI = FirstNotUsed I;
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 ;
not I is keeping_0
proof
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 ) )
set IS =
I +* (Start-At (insloc 0 ));
A24:
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 A22, A24, XBOOLE_0:def 3;
then A25:
I +* (Start-At (insloc 0 )) c= s00
by A19, 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 B28:
not
FirstNotUsed I in dom (I +* (Start-At (insloc 0 )))
by A24, A26, XBOOLE_0:def 3;
hence A28:
I +* (Start-At (insloc 0 )) c= s0
by A25, 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 )
set s02 =
Computation s0,
n;
A29:
for
m being
Element of
NAT st
m < n holds
IC (Computation s,m) in dom I
by A23;
A30:
not
FirstNotUsed I in UsedIntLoc I
by SF_MASTR:54;
A31:
not
IC (Computation s,n) in UsedIntLoc I
A32:
s0 | (UsedIntLoc I) =
s00 | (UsedIntLoc I)
by FUNCT_7:94, SF_MASTR:54
.=
s | (UsedIntLoc I)
by A31, FUNCT_7:94
;
A33:
not
FirstNotUsed I in UsedInt*Loc I
A34:
not
IC (Computation s,n) in UsedInt*Loc I
A35:
s0 | (UsedInt*Loc I) =
s00 | (UsedInt*Loc I)
by A33, FUNCT_7:94
.=
s | (UsedInt*Loc I)
by A34, FUNCT_7:94
;
then A36:
for
m being
Element of
NAT st
m < n holds
IC (Computation s0,m) in dom I
by A19, A28, A29, A32, SF_MASTR:73;
A37:
IC (Computation s0,n) = IC (Computation s,n)
by A19, A28, A29, A32, A35, SF_MASTR:73;
FirstNotUsed I in dom s00
by SCMFSA_2:66;
then
s0 . (FirstNotUsed I) = (s . (intloc 0 )) + 1
by FUNCT_7:33;
then A38:
(Computation s0,n) . (FirstNotUsed I) = (s . (intloc 0 )) + 1
by B28, A30, A36, A25, FUNCT_7:91, SF_MASTR:69;
A39:
IC (Computation s,n) in dom s
by AMI_1:116;
(
IC (Computation s,n) <> FirstNotUsed I &
IC (Computation s,n) in dom s00 )
by AMI_1:116, SCMFSA_2:84;
then A40:
s0 . (IC (Computation s,n)) =
s00 . (IC (Computation s,n))
by FUNCT_7:34
.=
(intloc 0 ) := (FirstNotUsed I)
by A39, FUNCT_7:33
;
A42:
s0 . (intloc 0 ) =
s00 . (intloc 0 )
by FUNCT_7:34
.=
s . (intloc 0 )
by FUNCT_7:34, SCMFSA_2:84
;
A43:
s . (intloc 0 ) < (s . (intloc 0 )) + 1
by XREAL_1:31;
Computation s0,
k =
Following (Computation s0,n)
by AMI_1:14
.=
Exec ((intloc 0 ) := (FirstNotUsed I)),
(Computation s0,n)
by A37, A40, AMI_1:54
;
hence
not
(Computation s0,k) . (intloc 0 ) = s0 . (intloc 0 )
by A38, A42, A43, SCMFSA_2:89;
:: thesis: verum
end;
hence
contradiction
by A18; :: thesis: verum