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 & J is_halting_on Initialized s,P holds
IExec ((if>0 (a,I,J)),P,s) = (IExec (J,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 & J is_halting_on Initialized s,P holds
IExec ((if>0 (a,I,J)),P,s) = (IExec (J,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 & J is_halting_on Initialized s,P holds
IExec ((if>0 (a,I,J)),P,s) = (IExec (J,P,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA))
let s be State of SCM+FSA; ( s . a <= 0 & J is_halting_on Initialized s,P implies IExec ((if>0 (a,I,J)),P,s) = (IExec (J,P,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA)) )
set I1 = I ";" (Stop SCM+FSA);
reconsider JI2 = ((J ";" (Goto ((card I) + 1))) ";" I) ";" (Stop SCM+FSA) as really-closed Program of SCM+FSA by Lm3;
set s2 = Initialized s;
set P2 = P +* JI2;
A1:
JI2 c= P +* JI2
by FUNCT_4:25;
set P3 = P +* (if>0 (a,I,J));
set s4 = Comput ((P +* (if>0 (a,I,J))),(Initialized s),1);
set s5 = Comput ((P +* (if>0 (a,I,J))),(Initialized s),2);
set i = a >0_goto ((card J) + 3);
0 in dom (if>0 (a,I,J))
by AFINSQ_1:65;
then A2: (P +* (if>0 (a,I,J))) . 0 =
(if>0 (a,I,J)) . 0
by FUNCT_4:13
.=
a >0_goto ((card J) + 3)
by Lm2
;
A3:
1 in dom (if>0 (a,I,J))
by Lm1;
A4: (P +* (if>0 (a,I,J))) . 1 =
(if>0 (a,I,J)) . 1
by A3, FUNCT_4:13
.=
goto 2
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
;
if>0 (a,I,J) =
(((a >0_goto ((card J) + 3)) ";" J) ";" (Goto ((card I) + 1))) ";" (I ";" (Stop SCM+FSA))
by SCMFSA6A:25
.=
((a >0_goto ((card J) + 3)) ";" J) ";" ((Goto ((card I) + 1)) ";" (I ";" (Stop SCM+FSA)))
by SCMFSA6A:25
.=
(a >0_goto ((card J) + 3)) ";" (J ";" ((Goto ((card I) + 1)) ";" (I ";" (Stop SCM+FSA))))
by SCMFSA6A:29
.=
(a >0_goto ((card J) + 3)) ";" ((J ";" (Goto ((card I) + 1))) ";" (I ";" (Stop SCM+FSA)))
by SCMFSA6A:25
.=
(Macro (a >0_goto ((card J) + 3))) ";" JI2
by SCMFSA6A:25
;
then
Reloc (JI2,(card (Macro (a >0_goto ((card J) + 3))))) c= if>0 (a,I,J)
by SCMFSA6A:38;
then A8:
Reloc (JI2,2) c= if>0 (a,I,J)
by COMPOS_1:56;
if>0 (a,I,J) c= P +* (if>0 (a,I,J))
by FUNCT_4:25;
then A9:
Reloc (JI2,2) c= P +* (if>0 (a,I,J))
by A8, XBOOLE_1:1;
A10: 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, A2, PBOOLE:143
;
assume
s . a <= 0
; ( not J is_halting_on Initialized s,P or IExec ((if>0 (a,I,J)),P,s) = (IExec (J,P,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA)) )
then
(Initialized s) . a <= 0
by A6, FUNCT_4:11;
then A11:
IC (Comput ((P +* (if>0 (a,I,J))),(Initialized s),1)) = 0 + 1
by A7, A10, SCMFSA_2:71;
A12: Comput ((P +* (if>0 (a,I,J))),(Initialized s),(1 + 1)) =
Following ((P +* (if>0 (a,I,J))),(Comput ((P +* (if>0 (a,I,J))),(Initialized s),1)))
by EXTPRO_1:3
.=
Exec ((goto 2),(Comput ((P +* (if>0 (a,I,J))),(Initialized s),1)))
by A11, A4, PBOOLE:143
;
then A13:
IC (Comput ((P +* (if>0 (a,I,J))),(Initialized s),2)) = 2
by SCMFSA_2:69;
A14:
now for f being FinSeq-Location holds (Initialized s) . f = (Comput ((P +* (if>0 (a,I,J))),(Initialized s),2)) . flet f be
FinSeq-Location ;
(Initialized s) . f = (Comput ((P +* (if>0 (a,I,J))),(Initialized s),2)) . fthus (Initialized s) . f =
(Comput ((P +* (if>0 (a,I,J))),(Initialized s),1)) . f
by A10, SCMFSA_2:71
.=
(Comput ((P +* (if>0 (a,I,J))),(Initialized s),2)) . f
by A12, SCMFSA_2:69
;
verum end;
now for a being Int-Location holds (Initialized s) . a = (Comput ((P +* (if>0 (a,I,J))),(Initialized s),2)) . alet a be
Int-Location;
(Initialized s) . a = (Comput ((P +* (if>0 (a,I,J))),(Initialized s),2)) . athus (Initialized s) . a =
(Comput ((P +* (if>0 (a,I,J))),(Initialized s),1)) . a
by A10, SCMFSA_2:71
.=
(Comput ((P +* (if>0 (a,I,J))),(Initialized s),2)) . a
by A12, SCMFSA_2:69
;
verum end;
then A15:
DataPart (Initialized s) = DataPart (Comput ((P +* (if>0 (a,I,J))),(Initialized s),2))
by A14, SCMFSA_M:2;
assume A16:
J is_halting_on Initialized s,P
; IExec ((if>0 (a,I,J)),P,s) = (IExec (J,P,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA))
then A17:
P +* JI2 halts_on Initialized s
by SCMFSA8A:39;
A18: CurInstr ((P +* (if>0 (a,I,J))),(Comput ((P +* (if>0 (a,I,J))),(Initialized s),((LifeSpan ((P +* JI2),(Initialized s))) + 2)))) =
CurInstr ((P +* (if>0 (a,I,J))),(Comput ((P +* (if>0 (a,I,J))),(Comput ((P +* (if>0 (a,I,J))),(Initialized s),2)),(LifeSpan ((P +* JI2),(Initialized s))))))
by EXTPRO_1:4
.=
IncAddr ((CurInstr ((P +* JI2),(Comput ((P +* JI2),(Initialized s),(LifeSpan ((P +* JI2),(Initialized s))))))),2)
by A13, A15, Th2, A9, A1
.=
IncAddr ((halt SCM+FSA),2)
by A17, EXTPRO_1:def 15
.=
halt SCM+FSA
by COMPOS_0:4
;
then A19:
P +* (if>0 (a,I,J)) halts_on Initialized s
by EXTPRO_1:29;
now for l being Nat st l < (LifeSpan ((P +* JI2),(Initialized s))) + 2 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 +* JI2),(Initialized s))) + 2 implies CurInstr ((P +* (if>0 (a,I,J))),(Comput ((P +* (if>0 (a,I,J))),(Initialized s),b1))) <> halt SCM+FSA )assume A20:
l < (LifeSpan ((P +* JI2),(Initialized s))) + 2
;
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 = 1 or ( l <> 0 & l <> 1 ) )
;
suppose A21:
(
l <> 0 &
l <> 1 )
;
not CurInstr ((P +* (if>0 (a,I,J))),(Comput ((P +* (if>0 (a,I,J))),(Initialized s),b1))) = halt SCM+FSAassume A22:
CurInstr (
(P +* (if>0 (a,I,J))),
(Comput ((P +* (if>0 (a,I,J))),(Initialized s),l)))
= halt SCM+FSA
;
contradictionconsider n being
Nat such that A23:
l = n + 1
by A21, NAT_1:6;
n <> 0
by A21, A23;
then consider l2 being
Nat such that A24:
n = l2 + 1
by NAT_1:6;
reconsider l2 =
l2 as
Element of
NAT by ORDINAL1:def 12;
InsCode (CurInstr ((P +* JI2),(Comput ((P +* JI2),(Initialized s),l2)))) =
InsCode (IncAddr ((CurInstr ((P +* JI2),(Comput ((P +* JI2),(Initialized s),l2)))),2))
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),2)),l2))))
by A13, A15, Th2, A9, A1
.=
InsCode (CurInstr ((P +* (if>0 (a,I,J))),(Comput ((P +* (if>0 (a,I,J))),(Initialized s),(l2 + (1 + 1))))))
by EXTPRO_1:4
.=
0
by A23, A24, A22, COMPOS_1:70
;
then A25:
CurInstr (
(P +* JI2),
(Comput ((P +* JI2),(Initialized s),l2)))
= halt SCM+FSA
by SCMFSA_2:95;
n + 1
< ((LifeSpan ((P +* JI2),(Initialized s))) + 1) + 1
by A20, A23;
then
n < (LifeSpan ((P +* JI2),(Initialized s))) + 1
by XREAL_1:6;
then
l2 < LifeSpan (
(P +* JI2),
(Initialized s))
by A24, XREAL_1:6;
hence
contradiction
by A17, A25, EXTPRO_1:def 15;
verum 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 +* JI2),(Initialized s))) + 2 <= l
;
then A26:
LifeSpan ((P +* (if>0 (a,I,J))),(Initialized s)) = (LifeSpan ((P +* JI2),(Initialized s))) + 2
by A18, A19, EXTPRO_1:def 15;
A27: DataPart (Result ((P +* JI2),(Initialized s))) =
DataPart (Comput ((P +* JI2),(Initialized s),(LifeSpan ((P +* JI2),(Initialized s)))))
by A16, EXTPRO_1:23, SCMFSA8A:39
.=
DataPart (Comput ((P +* (if>0 (a,I,J))),(Comput ((P +* (if>0 (a,I,J))),(Initialized s),2)),(LifeSpan ((P +* JI2),(Initialized s)))))
by A13, A15, Th2, A9, A1
.=
DataPart (Comput ((P +* (if>0 (a,I,J))),(Initialized s),((LifeSpan ((P +* JI2),(Initialized s))) + 2)))
by EXTPRO_1:4
.=
DataPart (Result ((P +* (if>0 (a,I,J))),(Initialized s)))
by A19, A26, EXTPRO_1:23
;
A28:
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 (JI2,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 (JI2,P,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA))) . b1 )A30:
IExec (
(if>0 (a,I,J)),
P,
s)
= Result (
(P +* (if>0 (a,I,J))),
(Initialized s))
by SCMFSA6B:def 1;
A31:
IExec (
JI2,
P,
s)
= Result (
(P +* JI2),
(Initialized s))
by SCMFSA6B:def 1;
assume A32:
x in dom (IExec ((if>0 (a,I,J)),P,s))
;
(IExec ((if>0 (a,I,J)),P,s)) . b1 = ((IExec (JI2,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 A32, SCMFSA_M:1;
suppose A33:
x is
Int-Location
;
(IExec ((if>0 (a,I,J)),P,s)) . b1 = ((IExec (JI2,P,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA))) . b1then
x <> IC
by SCMFSA_2:56;
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 A30
.=
(Result ((P +* JI2),(Initialized s))) . x
by A27, A33, SCMFSA_M:2
.=
(IExec (JI2,P,s)) . x
by A31
.=
((IExec (JI2,P,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA))) . x
by A34, FUNCT_4:11
;
verum end; suppose A35:
x is
FinSeq-Location
;
(IExec ((if>0 (a,I,J)),P,s)) . b1 = ((IExec (JI2,P,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA))) . b1then
x <> IC
by SCMFSA_2:57;
then A36:
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 A30
.=
(Result ((P +* JI2),(Initialized s))) . x
by A27, A35, SCMFSA_M:2
.=
(IExec (JI2,P,s)) . x
by A31
.=
((IExec (JI2,P,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA))) . x
by A36, FUNCT_4:11
;
verum end; suppose A37:
x = IC
;
(IExec ((if>0 (a,I,J)),P,s)) . b1 = ((IExec (JI2,P,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA))) . b1then A38:
x in dom (Start-At ((((card I) + (card J)) + 3),SCM+FSA))
by TARSKI:def 1;
A39:
IC (Result ((P +* JI2),(Initialized s))) =
IC (IExec (JI2,P,s))
by A31
.=
((card I) + (card J)) + 1
by A16, SCMFSA8A:40
;
thus (IExec ((if>0 (a,I,J)),P,s)) . x =
(Result ((P +* (if>0 (a,I,J))),(Initialized s))) . x
by A30
.=
(Comput ((P +* (if>0 (a,I,J))),(Initialized s),((LifeSpan ((P +* JI2),(Initialized s))) + 2))) . x
by A19, A26, EXTPRO_1:23
.=
IC (Comput ((P +* (if>0 (a,I,J))),(Comput ((P +* (if>0 (a,I,J))),(Initialized s),2)),(LifeSpan ((P +* JI2),(Initialized s)))))
by A37, EXTPRO_1:4
.=
(IC (Comput ((P +* JI2),(Initialized s),(LifeSpan ((P +* JI2),(Initialized s)))))) + 2
by A13, A15, Th2, A9, A1
.=
(IC (Result ((P +* JI2),(Initialized s)))) + 2
by A16, EXTPRO_1:23, SCMFSA8A:39
.=
(Start-At (((((card I) + (card J)) + 1) + 2),SCM+FSA)) . (IC )
by A39, FUNCOP_1:72
.=
((IExec (JI2,P,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA))) . x
by A37, A38, 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 (JI2,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 (JI2,P,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA))
by A28, FUNCT_1:2
.=
((IExec (J,P,s)) +* (Start-At ((((card I) + (card J)) + 1),SCM+FSA))) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA))
by A16, SCMFSA8A:41
.=
(IExec (J,P,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA))
by FUNCT_4:114
;
verum