set WHL = while>0 (F5(),F6(),F4());
set pWHL = stop (while>0 (F5(),F6(),F4()));
set P1 = F3() +* (stop (while>0 (F5(),F6(),F4())));
set PI = F3() +* (stop F4());
set m1 = (LifeSpan ((F3() +* (stop F4())),F2())) + 2;
set s2 = Initialize (IExec (F4(),F3(),F2()));
set P2 = F3() +* (stop (while>0 (F5(),F6(),F4())));
set m2 = LifeSpan ((F3() +* (stop (while>0 (F5(),F6(),F4())))),(Initialize (IExec (F4(),F3(),F2()))));
A5:
Initialize F2() = F2()
by MEMSTR_0:44;
A6:
P1[F2()]
by A3;
A7:
stop F4() c= F3() +* (stop F4())
by FUNCT_4:25;
A8:
F4() is_closed_on F2(),F3() +* (stop F4())
by A1, A3, A4;
F4() is_halting_on F2(),F3()
by A1, A3, A4;
then A9:
F3() +* (stop F4()) halts_on F2()
by A5, SCMPDS_6:def 3;
(F3() +* (stop F4())) +* (stop F4()) halts_on F2()
by A9;
then A10:
F4() is_halting_on F2(),F3() +* (stop F4())
by A5, SCMPDS_6:def 3;
set Es = IExec (F4(),F3(),F2());
set bj = DataLoc (((Initialize (IExec (F4(),F3(),F2()))) . F5()),F6());
set EP = F3();
deffunc H1( State of SCMPDS) -> Nat = F1($1);
A11:
for t being 0 -started State of SCMPDS
for Q being Instruction-Sequence of SCMPDS st P1[t] & t . F5() = F2() . F5() & t . (DataLoc ((F2() . F5()),F6())) > 0 holds
( (IExec (F4(),Q,t)) . F5() = t . F5() & F4() is_closed_on t,Q & F4() is_halting_on t,Q & H1( Initialize (IExec (F4(),Q,t))) < H1(t) & P1[ Initialize (IExec (F4(),Q,t))] )
by A4;
A12:
for t being 0 -started State of SCMPDS st P1[t] & H1(t) = 0 holds
t . (DataLoc ((F2() . F5()),F6())) <= 0
by A2;
( while>0 (F5(),F6(),F4()) is_closed_on F2(),F3() & while>0 (F5(),F6(),F4()) is_halting_on F2(),F3() )
from SCMPDS_8:sch 3(A12, A6, A11);
then A13:
F3() +* (stop (while>0 (F5(),F6(),F4()))) halts_on F2()
by A5, SCMPDS_6:def 3;
deffunc H2( State of SCMPDS) -> Nat = F1($1);
A14: (Initialize (IExec (F4(),F3(),F2()))) . F5() =
(IExec (F4(),F3(),F2())) . F5()
by SCMPDS_5:15
.=
F2() . F5()
by A1, A3, A4
;
then A15:
for t being 0 -started State of SCMPDS st P1[t] & H2(t) = 0 holds
t . (DataLoc (((Initialize (IExec (F4(),F3(),F2()))) . F5()),F6())) <= 0
by A2;
A16:
for t being 0 -started State of SCMPDS
for Q being Instruction-Sequence of SCMPDS st P1[t] & t . F5() = (Initialize (IExec (F4(),F3(),F2()))) . F5() & t . (DataLoc (((Initialize (IExec (F4(),F3(),F2()))) . F5()),F6())) > 0 holds
( (IExec (F4(),Q,t)) . F5() = t . F5() & F4() is_closed_on t,Q & F4() is_halting_on t,Q & H2( Initialize (IExec (F4(),Q,t))) < H2(t) & P1[ Initialize (IExec (F4(),Q,t))] )
by A4, A14;
A17:
P1[ Initialize (IExec (F4(),F3(),F2()))]
by A1, A3, A4;
( while>0 (F5(),F6(),F4()) is_closed_on Initialize (IExec (F4(),F3(),F2())),F3() & while>0 (F5(),F6(),F4()) is_halting_on Initialize (IExec (F4(),F3(),F2())),F3() )
from SCMPDS_8:sch 3(A15, A17, A16);
then A18:
F3() +* (stop (while>0 (F5(),F6(),F4()))) halts_on Initialize (Initialize (IExec (F4(),F3(),F2())))
by SCMPDS_6:def 3;
set s4 = Comput ((F3() +* (stop (while>0 (F5(),F6(),F4())))),F2(),1);
set P4 = F3() +* (stop (while>0 (F5(),F6(),F4())));
set i1 = (F5(),F6()) <=0_goto ((card F4()) + 2);
set i2 = goto (- ((card F4()) + 1));
set b = DataLoc ((F2() . F5()),F6());
A19:
while>0 (F5(),F6(),F4()) = ((F5(),F6()) <=0_goto ((card F4()) + 2)) ';' (F4() ';' (goto (- ((card F4()) + 1))))
by SCMPDS_4:15;
set mI = LifeSpan ((F3() +* (stop F4())),F2());
set s5 = Comput ((F3() +* (stop (while>0 (F5(),F6(),F4())))),(Comput ((F3() +* (stop (while>0 (F5(),F6(),F4())))),F2(),1)),(LifeSpan ((F3() +* (stop F4())),F2())));
set P5 = F3() +* (stop (while>0 (F5(),F6(),F4())));
set l1 = (card F4()) + 1;
A20:
IC F2() = 0
by MEMSTR_0:def 11;
A21: Comput ((F3() +* (stop (while>0 (F5(),F6(),F4())))),F2(),(0 + 1)) =
Following ((F3() +* (stop (while>0 (F5(),F6(),F4())))),(Comput ((F3() +* (stop (while>0 (F5(),F6(),F4())))),F2(),0)))
by EXTPRO_1:3
.=
Following ((F3() +* (stop (while>0 (F5(),F6(),F4())))),F2())
.=
Exec (((F5(),F6()) <=0_goto ((card F4()) + 2)),F2())
by A19, A5, SCMPDS_6:11
;
for a being Int_position holds F2() . a = (Comput ((F3() +* (stop (while>0 (F5(),F6(),F4())))),F2(),1)) . a
by A21, SCMPDS_2:56;
then A22:
DataPart F2() = DataPart (Comput ((F3() +* (stop (while>0 (F5(),F6(),F4())))),F2(),1))
by SCMPDS_4:8;
set m3 = (LifeSpan ((F3() +* (stop F4())),F2())) + 1;
set s6 = Comput ((F3() +* (stop (while>0 (F5(),F6(),F4())))),F2(),((LifeSpan ((F3() +* (stop F4())),F2())) + 1));
set P6 = F3() +* (stop (while>0 (F5(),F6(),F4())));
(card F4()) + 1 < (card F4()) + 2
by XREAL_1:6;
then A23:
(card F4()) + 1 in dom (while>0 (F5(),F6(),F4()))
by Th16;
set m0 = LifeSpan ((F3() +* (stop (while>0 (F5(),F6(),F4())))),F2());
set s7 = Comput ((F3() +* (stop (while>0 (F5(),F6(),F4())))),F2(),(((LifeSpan ((F3() +* (stop F4())),F2())) + 1) + 1));
A24:
while>0 (F5(),F6(),F4()) c= stop (while>0 (F5(),F6(),F4()))
by AFINSQ_1:74;
stop (while>0 (F5(),F6(),F4())) c= F3() +* (stop (while>0 (F5(),F6(),F4())))
by FUNCT_4:25;
then A25:
while>0 (F5(),F6(),F4()) c= F3() +* (stop (while>0 (F5(),F6(),F4())))
by A24, XBOOLE_1:1;
Shift (F4(),1) c= while>0 (F5(),F6(),F4())
by Lm4;
then A26:
Shift (F4(),1) c= F3() +* (stop (while>0 (F5(),F6(),F4())))
by A25, XBOOLE_1:1;
A27: IC (Comput ((F3() +* (stop (while>0 (F5(),F6(),F4())))),F2(),1)) =
(IC F2()) + 1
by A1, A21, SCMPDS_2:56
.=
0 + 1
by A20
;
then A28:
IC (Comput ((F3() +* (stop (while>0 (F5(),F6(),F4())))),(Comput ((F3() +* (stop (while>0 (F5(),F6(),F4())))),F2(),1)),(LifeSpan ((F3() +* (stop F4())),F2())))) = (card F4()) + 1
by A7, A10, A8, A22, A26, SCMPDS_7:18;
A29:
(F3() +* (stop (while>0 (F5(),F6(),F4())))) /. (IC (Comput ((F3() +* (stop (while>0 (F5(),F6(),F4())))),F2(),((LifeSpan ((F3() +* (stop F4())),F2())) + 1)))) = (F3() +* (stop (while>0 (F5(),F6(),F4())))) . (IC (Comput ((F3() +* (stop (while>0 (F5(),F6(),F4())))),F2(),((LifeSpan ((F3() +* (stop F4())),F2())) + 1))))
by PBOOLE:143;
A30:
Comput ((F3() +* (stop (while>0 (F5(),F6(),F4())))),F2(),((LifeSpan ((F3() +* (stop F4())),F2())) + 1)) = Comput ((F3() +* (stop (while>0 (F5(),F6(),F4())))),(Comput ((F3() +* (stop (while>0 (F5(),F6(),F4())))),F2(),1)),(LifeSpan ((F3() +* (stop F4())),F2())))
by EXTPRO_1:4;
then A31: CurInstr ((F3() +* (stop (while>0 (F5(),F6(),F4())))),(Comput ((F3() +* (stop (while>0 (F5(),F6(),F4())))),F2(),((LifeSpan ((F3() +* (stop F4())),F2())) + 1)))) =
(F3() +* (stop (while>0 (F5(),F6(),F4())))) . ((card F4()) + 1)
by A7, A10, A8, A27, A22, A26, A29, SCMPDS_7:18
.=
(while>0 (F5(),F6(),F4())) . ((card F4()) + 1)
by A23, A25, GRFUNC_1:2
.=
goto (- ((card F4()) + 1))
by Th17
;
A32: Comput ((F3() +* (stop (while>0 (F5(),F6(),F4())))),F2(),(((LifeSpan ((F3() +* (stop F4())),F2())) + 1) + 1)) =
Following ((F3() +* (stop (while>0 (F5(),F6(),F4())))),(Comput ((F3() +* (stop (while>0 (F5(),F6(),F4())))),F2(),((LifeSpan ((F3() +* (stop F4())),F2())) + 1))))
by EXTPRO_1:3
.=
Exec ((goto (- ((card F4()) + 1))),(Comput ((F3() +* (stop (while>0 (F5(),F6(),F4())))),F2(),((LifeSpan ((F3() +* (stop F4())),F2())) + 1))))
by A31
;
then IC (Comput ((F3() +* (stop (while>0 (F5(),F6(),F4())))),F2(),(((LifeSpan ((F3() +* (stop F4())),F2())) + 1) + 1))) =
ICplusConst ((Comput ((F3() +* (stop (while>0 (F5(),F6(),F4())))),F2(),((LifeSpan ((F3() +* (stop F4())),F2())) + 1))),(0 - ((card F4()) + 1)))
by SCMPDS_2:54
.=
0
by A28, A30, SCMPDS_7:1
;
then A33:
IC (Initialize (IExec (F4(),F3(),F2()))) = IC (Comput ((F3() +* (stop (while>0 (F5(),F6(),F4())))),F2(),((LifeSpan ((F3() +* (stop F4())),F2())) + 2)))
by MEMSTR_0:def 11;
A34:
DataPart (Comput ((F3() +* (stop F4())),F2(),(LifeSpan ((F3() +* (stop F4())),F2())))) = DataPart (Comput ((F3() +* (stop (while>0 (F5(),F6(),F4())))),(Comput ((F3() +* (stop (while>0 (F5(),F6(),F4())))),F2(),1)),(LifeSpan ((F3() +* (stop F4())),F2()))))
by A7, A10, A8, A27, A22, A26, SCMPDS_7:18;
now for x being Int_position holds (Comput ((F3() +* (stop (while>0 (F5(),F6(),F4())))),F2(),(((LifeSpan ((F3() +* (stop F4())),F2())) + 1) + 1))) . x = (Initialize (IExec (F4(),F3(),F2()))) . xlet x be
Int_position;
(Comput ((F3() +* (stop (while>0 (F5(),F6(),F4())))),F2(),(((LifeSpan ((F3() +* (stop F4())),F2())) + 1) + 1))) . x = (Initialize (IExec (F4(),F3(),F2()))) . xA35:
not
x in dom (Start-At (0,SCMPDS))
by SCMPDS_4:18;
(Comput ((F3() +* (stop (while>0 (F5(),F6(),F4())))),(Comput ((F3() +* (stop (while>0 (F5(),F6(),F4())))),F2(),1)),(LifeSpan ((F3() +* (stop F4())),F2())))) . x =
(Comput ((F3() +* (stop F4())),F2(),(LifeSpan ((F3() +* (stop F4())),F2())))) . x
by A34, SCMPDS_4:8
.=
(Result ((F3() +* (stop F4())),F2())) . x
by A9, EXTPRO_1:23
.=
(IExec (F4(),F3(),F2())) . x
by SCMPDS_4:def 5
;
hence (Comput ((F3() +* (stop (while>0 (F5(),F6(),F4())))),F2(),(((LifeSpan ((F3() +* (stop F4())),F2())) + 1) + 1))) . x =
(IExec (F4(),F3(),F2())) . x
by A30, A32, SCMPDS_2:54
.=
(Initialize (IExec (F4(),F3(),F2()))) . x
by A35, FUNCT_4:11
;
verum end;
then A36:
DataPart (Comput ((F3() +* (stop (while>0 (F5(),F6(),F4())))),F2(),(((LifeSpan ((F3() +* (stop F4())),F2())) + 1) + 1))) = DataPart (Initialize (IExec (F4(),F3(),F2())))
by SCMPDS_4:8;
A37:
Comput ((F3() +* (stop (while>0 (F5(),F6(),F4())))),F2(),((LifeSpan ((F3() +* (stop F4())),F2())) + 2)) = Initialize (IExec (F4(),F3(),F2()))
by A36, A33, MEMSTR_0:78;
then
CurInstr ((F3() +* (stop (while>0 (F5(),F6(),F4())))),(Comput ((F3() +* (stop (while>0 (F5(),F6(),F4())))),F2(),((LifeSpan ((F3() +* (stop F4())),F2())) + 2)))) = (F5(),F6()) <=0_goto ((card F4()) + 2)
by A19, SCMPDS_6:11;
then
LifeSpan ((F3() +* (stop (while>0 (F5(),F6(),F4())))),F2()) > (LifeSpan ((F3() +* (stop F4())),F2())) + 2
by A13, EXTPRO_1:36, SCMPDS_6:17;
then consider nn being Nat such that
A38:
LifeSpan ((F3() +* (stop (while>0 (F5(),F6(),F4())))),F2()) = ((LifeSpan ((F3() +* (stop F4())),F2())) + 2) + nn
by NAT_1:10;
reconsider nn = nn as Nat ;
Comput ((F3() +* (stop (while>0 (F5(),F6(),F4())))),F2(),(((LifeSpan ((F3() +* (stop F4())),F2())) + 2) + (LifeSpan ((F3() +* (stop (while>0 (F5(),F6(),F4())))),(Initialize (IExec (F4(),F3(),F2()))))))) = Comput ((F3() +* (stop (while>0 (F5(),F6(),F4())))),(Initialize (IExec (F4(),F3(),F2()))),(LifeSpan ((F3() +* (stop (while>0 (F5(),F6(),F4())))),(Initialize (IExec (F4(),F3(),F2()))))))
by A37, EXTPRO_1:4;
then
CurInstr ((F3() +* (stop (while>0 (F5(),F6(),F4())))),(Comput ((F3() +* (stop (while>0 (F5(),F6(),F4())))),F2(),(((LifeSpan ((F3() +* (stop F4())),F2())) + 2) + (LifeSpan ((F3() +* (stop (while>0 (F5(),F6(),F4())))),(Initialize (IExec (F4(),F3(),F2()))))))))) = halt SCMPDS
by A18, EXTPRO_1:def 15;
then
((LifeSpan ((F3() +* (stop F4())),F2())) + 2) + (LifeSpan ((F3() +* (stop (while>0 (F5(),F6(),F4())))),(Initialize (IExec (F4(),F3(),F2()))))) >= LifeSpan ((F3() +* (stop (while>0 (F5(),F6(),F4())))),F2())
by A13, EXTPRO_1:def 15;
then A39:
LifeSpan ((F3() +* (stop (while>0 (F5(),F6(),F4())))),(Initialize (IExec (F4(),F3(),F2())))) >= nn
by A38, XREAL_1:6;
A40:
Comput ((F3() +* (stop (while>0 (F5(),F6(),F4())))),F2(),(LifeSpan ((F3() +* (stop (while>0 (F5(),F6(),F4())))),F2()))) = Comput ((F3() +* (stop (while>0 (F5(),F6(),F4())))),(Initialize (IExec (F4(),F3(),F2()))),nn)
by A37, A38, EXTPRO_1:4;
then
CurInstr ((F3() +* (stop (while>0 (F5(),F6(),F4())))),(Comput ((F3() +* (stop (while>0 (F5(),F6(),F4())))),(Initialize (IExec (F4(),F3(),F2()))),nn))) = halt SCMPDS
by A13, EXTPRO_1:def 15;
then
nn >= LifeSpan ((F3() +* (stop (while>0 (F5(),F6(),F4())))),(Initialize (IExec (F4(),F3(),F2()))))
by A18, EXTPRO_1:def 15;
then
nn = LifeSpan ((F3() +* (stop (while>0 (F5(),F6(),F4())))),(Initialize (IExec (F4(),F3(),F2()))))
by A39, XXREAL_0:1;
then
Result ((F3() +* (stop (while>0 (F5(),F6(),F4())))),F2()) = Comput ((F3() +* (stop (while>0 (F5(),F6(),F4())))),(Initialize (IExec (F4(),F3(),F2()))),(LifeSpan ((F3() +* (stop (while>0 (F5(),F6(),F4())))),(Initialize (IExec (F4(),F3(),F2()))))))
by A13, A40, EXTPRO_1:23;
hence IExec ((while>0 (F5(),F6(),F4())),F3(),F2()) =
Comput ((F3() +* (stop (while>0 (F5(),F6(),F4())))),(Initialize (IExec (F4(),F3(),F2()))),(LifeSpan ((F3() +* (stop (while>0 (F5(),F6(),F4())))),(Initialize (IExec (F4(),F3(),F2()))))))
by SCMPDS_4:def 5
.=
Result ((F3() +* (stop (while>0 (F5(),F6(),F4())))),(Initialize (IExec (F4(),F3(),F2()))))
by A18, EXTPRO_1:23
.=
IExec ((while>0 (F5(),F6(),F4())),F3(),(Initialize (IExec (F4(),F3(),F2()))))
by SCMPDS_4:def 5
;
verum