let P be Instruction-Sequence of SCM+FSA; for I, J being really-closed MacroInstruction of SCM+FSA
for a being read-write Int-Location
for s being State of SCM+FSA st s . a > 0 & 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 really-closed MacroInstruction of SCM+FSA ; for a being read-write Int-Location
for s being State of SCM+FSA st s . a > 0 & 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_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_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);
A1:
I ";" (Stop SCM+FSA) c= P +* (I ";" (Stop SCM+FSA))
by FUNCT_4:25;
A2:
if>0 (a,I,J) = (((a >0_goto ((card J) + 3)) ";" J) ";" (Goto ((card I) + 1))) ";" (I ";" (Stop SCM+FSA))
by SCMFSA6A:25;
A3:
0 in dom (if>0 (a,I,J))
by AFINSQ_1:65;
A4: (P +* (if>0 (a,I,J))) . 0 =
(if>0 (a,I,J)) . 0
by A3, FUNCT_4:13
.=
a >0_goto ((card J) + 3)
by Lm2
;
A5:
dom (Initialize ((intloc 0) .--> 1)) = {(intloc 0),(IC )}
by SCMFSA_M:11;
( a <> intloc 0 & a <> IC )
by SCMFSA_2:56;
then A6:
not a in dom (Initialize ((intloc 0) .--> 1))
by A5, TARSKI:def 2;
IC in dom (Initialize ((intloc 0) .--> 1))
by MEMSTR_0:48;
then A7: IC (Initialized s) =
IC (Initialize ((intloc 0) .--> 1))
by FUNCT_4:13
.=
0
by MEMSTR_0:def 11
;
A8: 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))
.=
Exec ((a >0_goto ((card J) + 3)),(Initialized s))
by A7, A4, PBOOLE:143
;
A9:
if>0 (a,I,J) c= P +* (if>0 (a,I,J))
by FUNCT_4:25;
assume
s . a > 0
; ( 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 A6, FUNCT_4:11;
then A10:
IC (Comput ((P +* (if>0 (a,I,J))),(Initialized s),1)) = (card J) + 3
by A8, SCMFSA_2:71;
A11:
for f being FinSeq-Location holds (Initialized s) . f = (Comput ((P +* (if>0 (a,I,J))),(Initialized s),1)) . f
by A8, SCMFSA_2:71;
for a being Int-Location holds (Initialized s) . a = (Comput ((P +* (if>0 (a,I,J))),(Initialized s),1)) . a
by A8, SCMFSA_2:71;
then A12:
DataPart (Initialized s) = DataPart (Comput ((P +* (if>0 (a,I,J))),(Initialized s),1))
by A11, SCMFSA_M:2;
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 A13:
Reloc ((I ";" (Stop SCM+FSA)),((card J) + 3)) c= if>0 (a,I,J)
by A2, SCMFSA6A:38;
A14:
Reloc ((I ";" (Stop SCM+FSA)),((card J) + 3)) c= P +* (if>0 (a,I,J))
by A13, A9, XBOOLE_1:1;
assume A15:
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 A16:
P +* (I ";" (Stop SCM+FSA)) halts_on Initialized s
by SCMFSA8A:34;
A17: 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 A10, A12, Th2, A14, A1
.=
IncAddr ((halt SCM+FSA),((card J) + 3))
by A16, EXTPRO_1:def 15
.=
halt SCM+FSA
by COMPOS_0:4
;
then A18:
P +* (if>0 (a,I,J)) halts_on Initialized s
by EXTPRO_1:29;
now for l being Nat st l < (LifeSpan ((P +* (I ";" (Stop SCM+FSA))),(Initialized s))) + 1 holds
CurInstr ((P +* (if>0 (a,I,J))),(Comput ((P +* (if>0 (a,I,J))),(Initialized s),l))) <> halt SCM+FSAlet l be
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 A19:
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+FSAper cases
( l = 0 or l <> 0 )
;
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 A20:
l = n + 1
by NAT_1:6;
assume A21:
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;
A22:
InsCode (halt SCM+FSA) = 0
by COMPOS_1:70;
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_0:def 9
.=
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 A10, A12, Th2, A14, A1
.=
0
by A20, A21, A22, EXTPRO_1:4
;
then A23:
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 A19, A20, XREAL_1:6;
hence
contradiction
by A16, A23, EXTPRO_1:def 15;
verum end; end; end;
then
for l being 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 A24:
LifeSpan ((P +* (if>0 (a,I,J))),(Initialized s)) = (LifeSpan ((P +* (I ";" (Stop SCM+FSA))),(Initialized s))) + 1
by A17, A18, EXTPRO_1:def 15;
A25: 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 A15, 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 A10, A12, Th2, A14, A1
.=
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 A18, A24, EXTPRO_1:23
;
A26:
now for x being object st x in dom (IExec ((if>0 (a,I,J)),P,s)) holds
(IExec ((if>0 (a,I,J)),P,s)) . x = ((IExec ((I ";" (Stop SCM+FSA)),P,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA))) . xlet x be
object ;
( 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 )A28:
IExec (
(if>0 (a,I,J)),
P,
s)
= Result (
(P +* (if>0 (a,I,J))),
(Initialized s))
by SCMFSA6B:def 1;
A29:
IExec (
(I ";" (Stop SCM+FSA)),
P,
s)
= Result (
(P +* (I ";" (Stop SCM+FSA))),
(Initialized s))
by SCMFSA6B:def 1;
assume A30:
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 A30, SCMFSA_M:1;
suppose A31:
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 A32:
not
x in dom (Start-At ((((card I) + (card J)) + 3),SCM+FSA))
by TARSKI:def 1;
thus (IExec ((if>0 (a,I,J)),P,s)) . x =
(Result ((P +* (if>0 (a,I,J))),(Initialized s))) . x
by A28
.=
(Result ((P +* (I ";" (Stop SCM+FSA))),(Initialized s))) . x
by A25, A31, SCMFSA_M:2
.=
(IExec ((I ";" (Stop SCM+FSA)),P,s)) . x
by A29
.=
((IExec ((I ";" (Stop SCM+FSA)),P,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA))) . x
by A32, FUNCT_4:11
;
verum end; suppose A33:
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 A34:
not
x in dom (Start-At ((((card I) + (card J)) + 3),SCM+FSA))
by TARSKI:def 1;
thus (IExec ((if>0 (a,I,J)),P,s)) . x =
(Result ((P +* (if>0 (a,I,J))),(Initialized s))) . x
by A28
.=
(Result ((P +* (I ";" (Stop SCM+FSA))),(Initialized s))) . x
by A25, A33, SCMFSA_M:2
.=
(IExec ((I ";" (Stop SCM+FSA)),P,s)) . x
by A29
.=
((IExec ((I ";" (Stop SCM+FSA)),P,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA))) . x
by A34, FUNCT_4:11
;
verum end; suppose A35:
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 A36:
x in dom (Start-At ((((card I) + (card J)) + 3),SCM+FSA))
by TARSKI:def 1;
A37:
IC (Result ((P +* (I ";" (Stop SCM+FSA))),(Initialized s))) =
(IExec ((I ";" (Stop SCM+FSA)),P,s)) . (IC )
by A29
.=
IC ((IExec (I,P,s)) +* (Start-At ((card I),SCM+FSA)))
by A15, 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 A28
.=
(Comput ((P +* (if>0 (a,I,J))),(Initialized s),((LifeSpan ((P +* (I ";" (Stop SCM+FSA))),(Initialized s))) + 1))) . x
by A18, A24, 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 A35, EXTPRO_1:4
.=
(IC (Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialized s),(LifeSpan ((P +* (I ";" (Stop SCM+FSA))),(Initialized s)))))) + ((card J) + 3)
by A10, A12, Th2, A1, A14
.=
(IC (Result ((P +* (I ";" (Stop SCM+FSA))),(Initialized s)))) + ((card J) + 3)
by A15, EXTPRO_1:23, SCMFSA8A:34
.=
(Start-At (((card I) + ((card J) + 3)),SCM+FSA)) . (IC )
by A37, FUNCOP_1:72
.=
((IExec ((I ";" (Stop SCM+FSA)),P,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA))) . x
by A35, A36, FUNCT_4:13
;
verum end; 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 A26, FUNCT_1:2
.=
((IExec (I,P,s)) +* (Start-At ((card I),SCM+FSA))) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA))
by A15, SCMFSA8A:36
.=
(IExec (I,P,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA))
by FUNCT_4:114
;
verum