let P be Instruction-Sequence of SCM+FSA; for I, J being Program of SCM+FSA
for a being read-write Int-Location
for s being State of SCM+FSA st s . a > 0 & I is_closed_on Initialized s,P & I is_halting_on Initialized s,P holds
IExec ((if>0 (a,I,J)),P,s) = (IExec (I,P,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA))
let I, J be Program of SCM+FSA; for a being read-write Int-Location
for s being State of SCM+FSA st s . a > 0 & I is_closed_on Initialized s,P & I is_halting_on Initialized s,P holds
IExec ((if>0 (a,I,J)),P,s) = (IExec (I,P,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA))
let a be read-write Int-Location ; for s being State of SCM+FSA st s . a > 0 & I is_closed_on Initialized s,P & I is_halting_on Initialized s,P holds
IExec ((if>0 (a,I,J)),P,s) = (IExec (I,P,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA))
let s be State of SCM+FSA; ( s . a > 0 & I is_closed_on Initialized s,P & I is_halting_on Initialized s,P implies IExec ((if>0 (a,I,J)),P,s) = (IExec (I,P,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA)) )
set I1 = I ';' (Stop SCM+FSA);
set s1 = Initialized s;
set P1 = P +* (I ';' (Stop SCM+FSA));
set P3 = P +* (if>0 (a,I,J));
set s4 = Comput ((P +* (if>0 (a,I,J))),(Initialized s),1);
set i = a >0_goto ((card J) + 3);
A2:
I ';' (Stop SCM+FSA) c= P +* (I ';' (Stop SCM+FSA))
by FUNCT_4:25;
A3:
if>0 (a,I,J) = (((a >0_goto ((card J) + 3)) ';' J) ';' (Goto ((card I) + 1))) ';' (I ';' (Stop SCM+FSA))
by SCMFSA6A:25;
A4:
0 in dom (if>0 (a,I,J))
by Lm2;
A5: (P +* (if>0 (a,I,J))) . 0 =
(if>0 (a,I,J)) . 0
by A4, FUNCT_4:13
.=
a >0_goto ((card J) + 3)
by Lm3
;
L1:
dom (Initialize ((intloc 0) .--> 1)) = {(intloc 0),(IC )}
by SCMFSA6A:42;
( a <> intloc 0 & a <> IC )
by SCMFSA_2:56;
then B11:
not a in dom (Initialize ((intloc 0) .--> 1))
by L1, TARSKI:def 2;
IC in dom (Initialize ((intloc 0) .--> 1))
by MEMSTR_0:48;
then A6: IC (Initialized s) =
IC (Initialize ((intloc 0) .--> 1))
by FUNCT_4:13
.=
0
by MEMSTR_0:def 8
;
A7: Comput ((P +* (if>0 (a,I,J))),(Initialized s),(0 + 1)) =
Following ((P +* (if>0 (a,I,J))),(Comput ((P +* (if>0 (a,I,J))),(Initialized s),0)))
by EXTPRO_1:3
.=
Following ((P +* (if>0 (a,I,J))),(Initialized s))
by EXTPRO_1:2
.=
Exec ((a >0_goto ((card J) + 3)),(Initialized s))
by A6, A5, PBOOLE:143
;
A10:
if>0 (a,I,J) c= P +* (if>0 (a,I,J))
by FUNCT_4:25;
assume
s . a > 0
; ( not I is_closed_on Initialized s,P or not I is_halting_on Initialized s,P or IExec ((if>0 (a,I,J)),P,s) = (IExec (I,P,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA)) )
then
(Initialized s) . a > 0
by B11, FUNCT_4:11;
then A13:
IC (Comput ((P +* (if>0 (a,I,J))),(Initialized s),1)) = (card J) + 3
by A7, SCMFSA_2:71;
A15:
for f being FinSeq-Location holds (Initialized s) . f = (Comput ((P +* (if>0 (a,I,J))),(Initialized s),1)) . f
by A7, SCMFSA_2:71;
for a being Int-Location holds (Initialized s) . a = (Comput ((P +* (if>0 (a,I,J))),(Initialized s),1)) . a
by A7, SCMFSA_2:71;
then A16:
DataPart (Initialized s) = DataPart (Comput ((P +* (if>0 (a,I,J))),(Initialized s),1))
by A15, SCMFSA6A:7;
card (((a >0_goto ((card J) + 3)) ';' J) ';' (Goto ((card I) + 1))) =
(card ((Macro (a >0_goto ((card J) + 3))) ';' J)) + (card (Goto ((card I) + 1)))
by SCMFSA6A:21
.=
(card ((Macro (a >0_goto ((card J) + 3))) ';' J)) + 1
by SCMFSA8A:15
.=
((card (Macro (a >0_goto ((card J) + 3)))) + (card J)) + 1
by SCMFSA6A:21
.=
((card J) + 2) + 1
by COMPOS_1:56
.=
(card J) + (2 + 1)
;
then A17:
Reloc ((I ';' (Stop SCM+FSA)),((card J) + 3)) c= if>0 (a,I,J)
by A3, Lm1;
A19:
Reloc ((I ';' (Stop SCM+FSA)),((card J) + 3)) c= P +* (if>0 (a,I,J))
by A17, A10, XBOOLE_1:1;
assume A20:
I is_closed_on Initialized s,P
; ( not I is_halting_on Initialized s,P or IExec ((if>0 (a,I,J)),P,s) = (IExec (I,P,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA)) )
assume A21:
I is_halting_on Initialized s,P
; IExec ((if>0 (a,I,J)),P,s) = (IExec (I,P,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA))
then A22:
P +* (I ';' (Stop SCM+FSA)) halts_on Initialized s
by A20, SCMFSA8A:34;
I ';' (Stop SCM+FSA) is_closed_on Initialized s,P
by A20, A21, SCMFSA8A:30;
then A23:
I ';' (Stop SCM+FSA) is_closed_on Initialized s,P +* (I ';' (Stop SCM+FSA))
by Th9;
A24: CurInstr ((P +* (if>0 (a,I,J))),(Comput ((P +* (if>0 (a,I,J))),(Initialized s),((LifeSpan ((P +* (I ';' (Stop SCM+FSA))),(Initialized s))) + 1)))) =
CurInstr ((P +* (if>0 (a,I,J))),(Comput ((P +* (if>0 (a,I,J))),(Comput ((P +* (if>0 (a,I,J))),(Initialized s),1)),(LifeSpan ((P +* (I ';' (Stop SCM+FSA))),(Initialized s))))))
by EXTPRO_1:4
.=
IncAddr ((CurInstr ((P +* (I ';' (Stop SCM+FSA))),(Comput ((P +* (I ';' (Stop SCM+FSA))),(Initialized s),(LifeSpan ((P +* (I ';' (Stop SCM+FSA))),(Initialized s))))))),((card J) + 3))
by A23, A13, A16, Th11, A19, A2
.=
IncAddr ((halt SCM+FSA),((card J) + 3))
by A22, EXTPRO_1:def 15
.=
halt SCM+FSA
by COMPOS_1:11
;
then A25:
P +* (if>0 (a,I,J)) halts_on Initialized s
by EXTPRO_1:29;
now let l be
Element of
NAT ;
( l < (LifeSpan ((P +* (I ';' (Stop SCM+FSA))),(Initialized s))) + 1 implies CurInstr ((P +* (if>0 (a,I,J))),(Comput ((P +* (if>0 (a,I,J))),(Initialized s),b1))) <> halt SCM+FSA )assume A26:
l < (LifeSpan ((P +* (I ';' (Stop SCM+FSA))),(Initialized s))) + 1
;
CurInstr ((P +* (if>0 (a,I,J))),(Comput ((P +* (if>0 (a,I,J))),(Initialized s),b1))) <> halt SCM+FSAA27:
Comput (
(P +* (if>0 (a,I,J))),
(Initialized s),
0)
= Initialized s
by EXTPRO_1:2;
per cases
( l = 0 or l <> 0 )
;
suppose
l = 0
;
CurInstr ((P +* (if>0 (a,I,J))),(Comput ((P +* (if>0 (a,I,J))),(Initialized s),b1))) <> halt SCM+FSAhence
CurInstr (
(P +* (if>0 (a,I,J))),
(Comput ((P +* (if>0 (a,I,J))),(Initialized s),l)))
<> halt SCM+FSA
by A6, A5, A27, PBOOLE:143;
verum end; suppose
l <> 0
;
not CurInstr ((P +* (if>0 (a,I,J))),(Comput ((P +* (if>0 (a,I,J))),(Initialized s),b1))) = halt SCM+FSAthen consider n being
Nat such that A28:
l = n + 1
by NAT_1:6;
assume A29:
CurInstr (
(P +* (if>0 (a,I,J))),
(Comput ((P +* (if>0 (a,I,J))),(Initialized s),l)))
= halt SCM+FSA
;
contradictionreconsider n =
n as
Element of
NAT by ORDINAL1:def 12;
InsCode (CurInstr ((P +* (I ';' (Stop SCM+FSA))),(Comput ((P +* (I ';' (Stop SCM+FSA))),(Initialized s),n)))) =
InsCode (IncAddr ((CurInstr ((P +* (I ';' (Stop SCM+FSA))),(Comput ((P +* (I ';' (Stop SCM+FSA))),(Initialized s),n)))),((card J) + 3)))
by COMPOS_1:def 17
.=
InsCode (CurInstr ((P +* (if>0 (a,I,J))),(Comput ((P +* (if>0 (a,I,J))),(Comput ((P +* (if>0 (a,I,J))),(Initialized s),1)),n))))
by A23, A13, A16, Th11, A19, A2
.=
0
by A28, A29, EXTPRO_1:4, SCMFSA_2:97
;
then A30:
CurInstr (
(P +* (I ';' (Stop SCM+FSA))),
(Comput ((P +* (I ';' (Stop SCM+FSA))),(Initialized s),n)))
= halt SCM+FSA
by SCMFSA_2:95;
n < LifeSpan (
(P +* (I ';' (Stop SCM+FSA))),
(Initialized s))
by A26, A28, XREAL_1:6;
hence
contradiction
by A22, A30, EXTPRO_1:def 15;
verum end; end;
then
for l being Element of NAT st CurInstr ((P +* (if>0 (a,I,J))),(Comput ((P +* (if>0 (a,I,J))),(Initialized s),l))) = halt SCM+FSA holds
(LifeSpan ((P +* (I ';' (Stop SCM+FSA))),(Initialized s))) + 1 <= l
;
then A31:
LifeSpan ((P +* (if>0 (a,I,J))),(Initialized s)) = (LifeSpan ((P +* (I ';' (Stop SCM+FSA))),(Initialized s))) + 1
by A24, A25, EXTPRO_1:def 15;
A32: DataPart (Result ((P +* (I ';' (Stop SCM+FSA))),(Initialized s))) =
DataPart (Comput ((P +* (I ';' (Stop SCM+FSA))),(Initialized s),(LifeSpan ((P +* (I ';' (Stop SCM+FSA))),(Initialized s)))))
by A20, A21, EXTPRO_1:23, SCMFSA8A:34
.=
DataPart (Comput ((P +* (if>0 (a,I,J))),(Comput ((P +* (if>0 (a,I,J))),(Initialized s),1)),(LifeSpan ((P +* (I ';' (Stop SCM+FSA))),(Initialized s)))))
by A23, A13, A16, Th11, A19, A2
.=
DataPart (Comput ((P +* (if>0 (a,I,J))),(Initialized s),((LifeSpan ((P +* (I ';' (Stop SCM+FSA))),(Initialized s))) + 1)))
by EXTPRO_1:4
.=
DataPart (Result ((P +* (if>0 (a,I,J))),(Initialized s)))
by A25, A31, EXTPRO_1:23
;
A33:
now let x be
set ;
( x in dom (IExec ((if>0 (a,I,J)),P,s)) implies (IExec ((if>0 (a,I,J)),P,s)) . b1 = ((IExec ((I ';' (Stop SCM+FSA)),P,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA))) . b1 )A34:
dom (Start-At ((((card I) + (card J)) + 3),SCM+FSA)) = {(IC )}
by FUNCOP_1:13;
A35:
IExec (
(if>0 (a,I,J)),
P,
s)
= Result (
(P +* (if>0 (a,I,J))),
(Initialized s))
by SCMFSA6B:def 1;
A36:
IExec (
(I ';' (Stop SCM+FSA)),
P,
s)
= Result (
(P +* (I ';' (Stop SCM+FSA))),
(Initialized s))
by SCMFSA6B:def 1;
assume A38:
x in dom (IExec ((if>0 (a,I,J)),P,s))
;
(IExec ((if>0 (a,I,J)),P,s)) . b1 = ((IExec ((I ';' (Stop SCM+FSA)),P,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA))) . b1per cases
( x is Int-Location or x is FinSeq-Location or x = IC )
by A38, SCMFSA6A:5;
suppose A39:
x is
Int-Location
;
(IExec ((if>0 (a,I,J)),P,s)) . b1 = ((IExec ((I ';' (Stop SCM+FSA)),P,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA))) . b1then
x <> IC
by SCMFSA_2:56;
then A40:
not
x in dom (Start-At ((((card I) + (card J)) + 3),SCM+FSA))
by A34, TARSKI:def 1;
thus (IExec ((if>0 (a,I,J)),P,s)) . x =
(Result ((P +* (if>0 (a,I,J))),(Initialized s))) . x
by A35
.=
(Result ((P +* (I ';' (Stop SCM+FSA))),(Initialized s))) . x
by A32, A39, SCMFSA6A:7
.=
(IExec ((I ';' (Stop SCM+FSA)),P,s)) . x
by A36
.=
((IExec ((I ';' (Stop SCM+FSA)),P,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA))) . x
by A40, FUNCT_4:11
;
verum end; suppose A41:
x is
FinSeq-Location
;
(IExec ((if>0 (a,I,J)),P,s)) . b1 = ((IExec ((I ';' (Stop SCM+FSA)),P,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA))) . b1then
x <> IC
by SCMFSA_2:57;
then A42:
not
x in dom (Start-At ((((card I) + (card J)) + 3),SCM+FSA))
by A34, TARSKI:def 1;
thus (IExec ((if>0 (a,I,J)),P,s)) . x =
(Result ((P +* (if>0 (a,I,J))),(Initialized s))) . x
by A35
.=
(Result ((P +* (I ';' (Stop SCM+FSA))),(Initialized s))) . x
by A32, A41, SCMFSA6A:7
.=
(IExec ((I ';' (Stop SCM+FSA)),P,s)) . x
by A36
.=
((IExec ((I ';' (Stop SCM+FSA)),P,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA))) . x
by A42, FUNCT_4:11
;
verum end; suppose A43:
x = IC
;
(IExec ((if>0 (a,I,J)),P,s)) . b1 = ((IExec ((I ';' (Stop SCM+FSA)),P,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA))) . b1then A44:
x in dom (Start-At ((((card I) + (card J)) + 3),SCM+FSA))
by A34, TARSKI:def 1;
A45:
IC (Result ((P +* (I ';' (Stop SCM+FSA))),(Initialized s))) =
(IExec ((I ';' (Stop SCM+FSA)),P,s)) . (IC )
by A36
.=
IC ((IExec (I,P,s)) +* (Start-At ((card I),SCM+FSA)))
by A20, A21, SCMFSA8A:36
.=
card I
by FUNCT_4:113
;
thus (IExec ((if>0 (a,I,J)),P,s)) . x =
(Result ((P +* (if>0 (a,I,J))),(Initialized s))) . x
by A35
.=
(Comput ((P +* (if>0 (a,I,J))),(Initialized s),((LifeSpan ((P +* (I ';' (Stop SCM+FSA))),(Initialized s))) + 1))) . x
by A25, A31, EXTPRO_1:23
.=
IC (Comput ((P +* (if>0 (a,I,J))),(Comput ((P +* (if>0 (a,I,J))),(Initialized s),1)),(LifeSpan ((P +* (I ';' (Stop SCM+FSA))),(Initialized s)))))
by A43, EXTPRO_1:4
.=
(IC (Comput ((P +* (I ';' (Stop SCM+FSA))),(Initialized s),(LifeSpan ((P +* (I ';' (Stop SCM+FSA))),(Initialized s)))))) + ((card J) + 3)
by A23, A13, A16, Th11, A2, A19
.=
(IC (Result ((P +* (I ';' (Stop SCM+FSA))),(Initialized s)))) + ((card J) + 3)
by A20, A21, EXTPRO_1:23, SCMFSA8A:34
.=
(Start-At (((card I) + ((card J) + 3)),SCM+FSA)) . (IC )
by A45, FUNCOP_1:72
.=
((IExec ((I ';' (Stop SCM+FSA)),P,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA))) . x
by A43, A44, FUNCT_4:13
;
verum end; end;
dom (IExec ((if>0 (a,I,J)),P,s)) =
the carrier of SCM+FSA
by PARTFUN1:def 2
.=
dom ((IExec ((I ';' (Stop SCM+FSA)),P,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA)))
by PARTFUN1:def 2
;
hence IExec ((if>0 (a,I,J)),P,s) =
(IExec ((I ';' (Stop SCM+FSA)),P,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA))
by A33, FUNCT_1:2
.=
((IExec (I,P,s)) +* (Start-At ((card I),SCM+FSA))) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA))
by A20, A21, SCMFSA8A:36
.=
(IExec (I,P,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA))
by FUNCT_4:114
;
verum