let I be Program of SCM+FSA ; :: thesis: ( I is keepInt0_1 implies I is InitClosed )
assume A18:
I is keepInt0_1
; :: thesis: I is InitClosed
let s be State of SCM+FSA ; :: according to SCM_HALT:def 1 :: thesis: for n being Element of NAT st Initialized I c= s holds
IC (Computation s,n) in dom I
let n be Element of NAT ; :: thesis: ( Initialized I c= s implies IC (Computation s,n) in dom I )
assume A19:
Initialized I 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;
set s00 = s +* (IC (Computation s,n)),((intloc 0 ) := (FirstNotUsed I));
set s0 = (s +* (IC (Computation s,n)),((intloc 0 ) := (FirstNotUsed I))) +* (FirstNotUsed I),((s . (intloc 0 )) + 1);
reconsider s00 = s +* (IC (Computation s,n)),((intloc 0 ) := (FirstNotUsed I)) as State of SCM+FSA ;
reconsider s0 = (s +* (IC (Computation s,n)),((intloc 0 ) := (FirstNotUsed I))) +* (FirstNotUsed I),((s . (intloc 0 )) + 1) as State of SCM+FSA ;
not I is keepInt0_1
proof
take
s0
;
:: according to SCM_HALT:def 3 :: thesis: ( Initialized I c= s0 & not for k being Element of NAT holds (Computation s0,k) . (intloc 0 ) = 1 )
set IS =
Initialized I;
set iIC =
{(intloc 0 )} \/ {(IC SCM+FSA )};
A24:
dom (Initialized I) =
((dom I) \/ {(intloc 0 )}) \/ {(IC SCM+FSA )}
by SCMFSA6A:43
.=
(dom I) \/ ({(intloc 0 )} \/ {(IC SCM+FSA )})
by XBOOLE_1:4
;
IC (Computation s,n) <> IC SCM+FSA
by AMI_1:48;
then A25:
not
IC (Computation s,n) in {(IC SCM+FSA )}
by TARSKI:def 1;
IC (Computation s,n) <> intloc 0
by SCMFSA_2:84;
then
not
IC (Computation s,n) in {(intloc 0 )}
by TARSKI:def 1;
then
not
IC (Computation s,n) in {(intloc 0 )} \/ {(IC SCM+FSA )}
by A25, XBOOLE_0:def 3;
then
not
IC (Computation s,n) in dom (Initialized I)
by A22, A24, XBOOLE_0:def 3;
then A26:
Initialized I c= s00
by A19, FUNCT_7:91;
FirstNotUsed I <> IC SCM+FSA
by SCMFSA_2:81;
then A28:
not
FirstNotUsed I in {(IC SCM+FSA )}
by TARSKI:def 1;
not
FirstNotUsed I in {(intloc 0 )}
by TARSKI:def 1;
then
not
FirstNotUsed I in {(intloc 0 )} \/ {(IC SCM+FSA )}
by A28, XBOOLE_0:def 3;
then
not
FirstNotUsed I in dom (Initialized I)
by A24, A27, XBOOLE_0:def 3;
hence
Initialized I c= s0
by A26, FUNCT_7:91;
:: thesis: not for k being Element of NAT holds (Computation s0,k) . (intloc 0 ) = 1
then A29:
I +* (Start-At (insloc 0 )) c= s0
by SCMFSA6B:8;
A30:
I +* (Start-At (insloc 0 )) c= s
by A19, SCMFSA6B:8;
take k =
n + 1;
:: thesis: not (Computation s0,k) . (intloc 0 ) = 1
set s02 =
Computation s0,
n;
A31:
for
m being
Element of
NAT st
m < n holds
IC (Computation s,m) in dom I
by A23;
A32:
not
FirstNotUsed I in UsedIntLoc I
by SF_MASTR:54;
A33:
not
IC (Computation s,n) in UsedIntLoc I
A34:
s0 | (UsedIntLoc I) =
s00 | (UsedIntLoc I)
by FUNCT_7:94, SF_MASTR:54
.=
s | (UsedIntLoc I)
by A33, FUNCT_7:94
;
A35:
not
FirstNotUsed I in UsedInt*Loc I
A36:
not
IC (Computation s,n) in UsedInt*Loc I
A37:
s . (intloc 0 ) = 1
by A19, Th7;
A38:
s0 | (UsedInt*Loc I) =
s00 | (UsedInt*Loc I)
by A35, FUNCT_7:94
.=
s | (UsedInt*Loc I)
by A36, FUNCT_7:94
;
then A39:
for
m being
Element of
NAT st
m < n holds
IC (Computation s0,m) in dom I
by A29, A30, A31, A34, SF_MASTR:73;
A40:
IC (Computation s0,n) = IC (Computation s,n)
by A29, A30, A31, A34, A38, 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 A41:
(Computation s0,n) . (FirstNotUsed I) = 1
+ 1
by A29, A32, A37, A39, SF_MASTR:69;
A42:
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 A43:
s0 . (IC (Computation s,n)) =
s00 . (IC (Computation s,n))
by FUNCT_7:34
.=
(intloc 0 ) := (FirstNotUsed I)
by A42, FUNCT_7:33
;
Computation s0,
k =
Following (Computation s0,n)
by AMI_1:14
.=
Exec ((intloc 0 ) := (FirstNotUsed I)),
(Computation s0,n)
by A40, A43, AMI_1:54
;
hence
not
(Computation s0,k) . (intloc 0 ) = 1
by A41, SCMFSA_2:89;
:: thesis: verum
end;
hence
contradiction
by A18; :: thesis: verum