let I be Program of SCM+FSA; ( I is keeping_0 implies I is paraclosed )
assume A16:
I is keeping_0
; I is paraclosed
set FI = FirstNotUsed I;
let s be State of SCM+FSA; SCMFSA6B:def 2 for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT st I c= P holds
for n being Element of NAT st Start-At (0,SCM+FSA) c= s holds
IC (Comput (P,s,n)) in dom I
let P be the Instructions of SCM+FSA -valued ManySortedSet of NAT ; ( I c= P implies for n being Element of NAT st Start-At (0,SCM+FSA) c= s holds
IC (Comput (P,s,n)) in dom I )
assume A17:
I c= P
; for n being Element of NAT st Start-At (0,SCM+FSA) c= s holds
IC (Comput (P,s,n)) in dom I
let n be Element of NAT ; ( Start-At (0,SCM+FSA) c= s implies IC (Comput (P,s,n)) in dom I )
assume A18:
Start-At (0,SCM+FSA) c= s
; IC (Comput (P,s,n)) in dom I
defpred S1[ Nat] means not IC (Comput (P,s,c1)) in dom I;
assume
not IC (Comput (P,s,n)) in dom I
; 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 = Comput (P,s,n);
reconsider s00 = s +* ((IC (Comput (P,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 ;
set Q = P +* ((IC (Comput (P,s,n))),((intloc 0) := (FirstNotUsed I)));
A22:
dom I c= NAT
by RELAT_1:def 18;
A23:
dom (P +* ((IC (Comput (P,s,n))),((intloc 0) := (FirstNotUsed I)))) = NAT
by PARTFUN1:def 4;
not I is keeping_0
proof
A24:
not
IC (Comput (P,s,n)) in UsedInt*Loc I
not
FirstNotUsed I in UsedInt*Loc I
then A25:
s0 | (UsedInt*Loc I) =
s00 | (UsedInt*Loc I)
by FUNCT_7:94
.=
s | (UsedInt*Loc I)
by A24, FUNCT_7:94
;
A26:
not
FirstNotUsed I in dom I
by A22, SCMFSA_2:84;
A27:
s . (intloc 0) < (s . (intloc 0)) + 1
by XREAL_1:31;
A28:
dom P = NAT
by PARTFUN1:def 4;
A29:
(P +* ((IC (Comput (P,s,n))),((intloc 0) := (FirstNotUsed I)))) . (IC (Comput (P,s,n))) = (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 (
(P +* ((IC (Comput (P,s,n))),((intloc 0) := (FirstNotUsed I)))),
s0,
n);
set IS =
Start-At (
0,
SCM+FSA);
take
s0
;
SCMFSA6B:def 4 ( Start-At (0,SCM+FSA) c= s0 & ex P being the Instructions of SCM+FSA -valued ManySortedSet of NAT st
( I c= P & not for k being Element of NAT holds (Comput (P,s0,k)) . (intloc 0) = s0 . (intloc 0) ) )
A32:
dom (Initialize I) =
(dom I) \/ (dom (Start-At (0,SCM+FSA)))
by FUNCT_4:def 1
.=
(dom I) \/ {(IC )}
by FUNCOP_1:19
;
Start-At (
0,
SCM+FSA)
c= Initialize I
by FUNCT_4:26;
then yy:
dom (Start-At (0,SCM+FSA)) c= dom (Initialize I)
by RELAT_1:25;
dom (Start-At (0,SCM+FSA)) misses NAT
by COMPOS_1:211;
then
not
IC (Comput (P,s,n)) in dom (Start-At (0,SCM+FSA))
by XBOOLE_0:3;
then A33:
Start-At (
0,
SCM+FSA)
c= s00
by A18, FUNCT_7:91;
FirstNotUsed I <> IC
by SCMFSA_2:81;
then
not
FirstNotUsed I in {(IC )}
by TARSKI:def 1;
then
not
FirstNotUsed I in dom (Start-At (0,SCM+FSA))
by yy, A32, A26, XBOOLE_0:def 3;
hence B35:
Start-At (
0,
SCM+FSA)
c= s0
by A33, FUNCT_7:91;
ex P being the Instructions of SCM+FSA -valued ManySortedSet of NAT 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:140;
take
P +* (
(IC (Comput (P,s,n))),
((intloc 0) := (FirstNotUsed I)))
;
( 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:140;
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;
not (Comput ((P +* ((IC (Comput (P,s,n))),((intloc 0) := (FirstNotUsed I)))),s0,k)) . (intloc 0) = s0 . (intloc 0)
A37:
not
IC (Comput (P,s,n)) in UsedIntLoc I
A38:
s0 | (UsedIntLoc I) =
s00 | (UsedIntLoc I)
by FUNCT_7:94, SF_MASTR:54
.=
s | (UsedIntLoc I)
by A37, FUNCT_7:94
;
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:54, SF_MASTR:73;
A41:
(Comput ((P +* ((IC (Comput (P,s,n))),((intloc 0) := (FirstNotUsed I)))),s0,n)) . (FirstNotUsed I) = (s . (intloc 0)) + 1
by A31, A40, A36, B35, SF_MASTR:69;
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:4
.=
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 8
.=
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:73
;
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:89;
verum
end;
hence
contradiction
by A16; verum