A5:
Initialize F2() = F2()
by MEMSTR_0:44;
set WHL = while<>0 (F5(),F6(),F4());
set s1 = F2();
set P1 = F3() +* (stop (while<>0 (F5(),F6(),F4())));
set sI = F2();
set PI = F3() +* (stop F4());
set m1 = (LifeSpan ((F3() +* (stop F4())),F2())) + 2;
set s2 = Initialize (IExec (F4(),F3(),F2()));
set m2 = LifeSpan ((F3() +* (stop (while<>0 (F5(),F6(),F4())))),(Initialize (IExec (F4(),F3(),F2()))));
A6:
stop F4() c= F3() +* (stop F4())
by FUNCT_4:25;
F4() is_closed_on F2(),F3()
by A1, A3, A4;
then A7:
F4() is_closed_on F2(),F3() +* (stop F4())
by A5, SCMPDS_6:24;
F4() is_halting_on F2(),F3()
by A1, A3, A4;
then A8:
F3() +* (stop F4()) halts_on F2()
by A5, SCMPDS_6:def 3;
(F3() +* (stop F4())) +* (stop F4()) halts_on Initialize F2()
by A8, A5;
then A9:
F4() is_halting_on F2(),F3() +* (stop F4())
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 2;
set i2 = goto ((card F4()) + 2);
set i3 = goto (- ((card F4()) + 2));
set b = DataLoc ((F2() . F5()),F6());
A10:
IC F2() = 0
by A5, MEMSTR_0:47;
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 l2 = (card F4()) + 2;
A11:
while<>0 (F5(),F6(),F4()) = ((F5(),F6()) <>0_goto 2) ';' (((goto ((card F4()) + 2)) ';' F4()) ';' (goto (- ((card F4()) + 2))))
by Lm8;
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()) + 2 < (card F4()) + 3
by XREAL_1:6;
then A12:
(card F4()) + 2 in dom (while<>0 (F5(),F6(),F4()))
by Th9;
set s7 = Comput ((F3() +* (stop (while<>0 (F5(),F6(),F4())))),F2(),(((LifeSpan ((F3() +* (stop F4())),F2())) + 1) + 1));
set P7 = F3() +* (stop (while<>0 (F5(),F6(),F4())));
A13:
IExec (F4(),F3(),F2()) = Result ((F3() +* (stop F4())),F2())
by SCMPDS_4:def 5;
A14:
stop (while<>0 (F5(),F6(),F4())) c= F3() +* (stop (while<>0 (F5(),F6(),F4())))
by FUNCT_4:25;
while<>0 (F5(),F6(),F4()) c= stop (while<>0 (F5(),F6(),F4()))
by AFINSQ_1:74;
then A15:
while<>0 (F5(),F6(),F4()) c= F3() +* (stop (while<>0 (F5(),F6(),F4())))
by A14, XBOOLE_1:1;
deffunc H1( State of SCMPDS) -> Element of NAT = F1($1);
A16:
for t being 0 -started State of SCMPDS st P1[t] & H1(t) = 0 holds
t . (DataLoc ((F2() . F5()),F6())) = 0
by A2;
A17:
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;
A18: 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 2),F2())
by A11, A5, SCMPDS_6:11
;
Shift (F4(),2) c= while<>0 (F5(),F6(),F4())
by Lm9;
then
Shift (F4(),2) c= F3() +* (stop (while<>0 (F5(),F6(),F4())))
by A15, XBOOLE_1:1;
then A19:
Shift (F4(),2) c= F3() +* (stop (while<>0 (F5(),F6(),F4())))
;
for a being Int_position holds F2() . a = (Comput ((F3() +* (stop (while<>0 (F5(),F6(),F4())))),F2(),1)) . a
by A18, SCMPDS_2:55;
then A20:
DataPart F2() = DataPart (Comput ((F3() +* (stop (while<>0 (F5(),F6(),F4())))),F2(),1))
by SCMPDS_4:8;
A21: IC (Comput ((F3() +* (stop (while<>0 (F5(),F6(),F4())))),F2(),1)) =
ICplusConst (F2(),2)
by A1, A18, SCMPDS_2:55
.=
0 + 2
by A10, SCMPDS_6:12
;
then A22:
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()) + 2
by A6, A9, A7, A20, A19, SCMPDS_7:18;
A23:
(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;
A24:
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 A25: 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()) + 2)
by A6, A9, A7, A21, A20, A19, A23, SCMPDS_7:18
.=
(F3() +* (stop (while<>0 (F5(),F6(),F4())))) . ((card F4()) + 2)
.=
(F3() +* (stop (while<>0 (F5(),F6(),F4())))) . ((card F4()) + 2)
.=
(while<>0 (F5(),F6(),F4())) . ((card F4()) + 2)
by A12, A15, GRFUNC_1:2
.=
goto (- ((card F4()) + 2))
by Th11
;
A26: 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()) + 2))),(Comput ((F3() +* (stop (while<>0 (F5(),F6(),F4())))),F2(),((LifeSpan ((F3() +* (stop F4())),F2())) + 1))))
by A25
;
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()) + 2)))
by SCMPDS_2:54
.=
0
by A22, A24, SCMPDS_7:1
;
then A27:
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:47;
A28:
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 A6, A9, A7, A21, A20, A19, 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()))) . xA29:
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 A28, SCMPDS_4:8
.=
(Result ((F3() +* (stop F4())),F2())) . x
by A8, EXTPRO_1:23
.=
(IExec (F4(),F3(),F2())) . x
by A13
;
hence (Comput ((F3() +* (stop (while<>0 (F5(),F6(),F4())))),F2(),(((LifeSpan ((F3() +* (stop F4())),F2())) + 1) + 1))) . x =
(IExec (F4(),F3(),F2())) . x
by A24, A26, SCMPDS_2:54
.=
(Initialize (IExec (F4(),F3(),F2()))) . x
by A29, FUNCT_4:11
;
verum end;
then A30:
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;
set m0 = LifeSpan ((F3() +* (stop (while<>0 (F5(),F6(),F4())))),F2());
A31:
P1[F2()]
by A3;
( while<>0 (F5(),F6(),F4()) is_closed_on F2(),F3() & while<>0 (F5(),F6(),F4()) is_halting_on F2(),F3() )
from SCPINVAR:sch 3(A16, A31, A17);
then A32:
F3() +* (stop (while<>0 (F5(),F6(),F4()))) halts_on F2()
by A5, SCMPDS_6:def 3;
deffunc H2( State of SCMPDS) -> Element of NAT = H1($1);
set Es = IExec (F4(),F3(),F2());
set bj = DataLoc (((IExec (F4(),F3(),F2())) . F5()),F6());
set EP = F3();
A33:
(IExec (F4(),F3(),F2())) . F5() = F2() . F5()
by A1, A3, A4;
A34:
(Initialize (IExec (F4(),F3(),F2()))) . F5() = (IExec (F4(),F3(),F2())) . F5()
by SCMPDS_5:15;
A35:
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, A33, A34;
A36:
P1[ Initialize (IExec (F4(),F3(),F2()))]
by A1, A3, A4;
A37:
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, A33, A34;
A38:
( 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 SCPINVAR:sch 3(A35, A36, A37);
while<>0 (F5(),F6(),F4()) is_halting_on IExec (F4(),F3(),F2()),F3()
proof
F3()
+* (stop (while<>0 (F5(),F6(),F4()))) halts_on Initialize (Initialize (IExec (F4(),F3(),F2())))
by A38, SCMPDS_6:def 3;
hence
while<>0 (
F5(),
F6(),
F4())
is_halting_on IExec (
F4(),
F3(),
F2()),
F3()
by SCMPDS_6:def 3;
verum
end;
then A39:
F3() +* (stop (while<>0 (F5(),F6(),F4()))) halts_on Initialize (IExec (F4(),F3(),F2()))
by SCMPDS_6:def 3;
A40:
Comput ((F3() +* (stop (while<>0 (F5(),F6(),F4())))),F2(),((LifeSpan ((F3() +* (stop F4())),F2())) + 2)) = Initialize (IExec (F4(),F3(),F2()))
by A30, A27, 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 2
by A11, SCMPDS_6:11;
then
LifeSpan ((F3() +* (stop (while<>0 (F5(),F6(),F4())))),F2()) > (LifeSpan ((F3() +* (stop F4())),F2())) + 2
by A32, EXTPRO_1:36, SCMPDS_6:16;
then consider nn being Nat such that
A41:
LifeSpan ((F3() +* (stop (while<>0 (F5(),F6(),F4())))),F2()) = ((LifeSpan ((F3() +* (stop F4())),F2())) + 2) + nn
by NAT_1:10;
reconsider nn = nn as Element of NAT by ORDINAL1:def 12;
IC (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())))))))) = IC (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 A40, 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()))))))))) =
CurInstr ((F3() +* (stop (while<>0 (F5(),F6(),F4())))),(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()))))))))
.=
halt SCMPDS
by A39, 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 A32, EXTPRO_1:def 15;
then A42:
LifeSpan ((F3() +* (stop (while<>0 (F5(),F6(),F4())))),(Initialize (IExec (F4(),F3(),F2())))) >= nn
by A41, XREAL_1:6;
A43:
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 A40, A41, 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 A32, EXTPRO_1:def 15;
then
nn >= LifeSpan ((F3() +* (stop (while<>0 (F5(),F6(),F4())))),(Initialize (IExec (F4(),F3(),F2()))))
by A39, EXTPRO_1:def 15;
then
nn = LifeSpan ((F3() +* (stop (while<>0 (F5(),F6(),F4())))),(Initialize (IExec (F4(),F3(),F2()))))
by A42, 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 A32, A43, 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 A39, EXTPRO_1:23
.=
IExec ((while<>0 (F5(),F6(),F4())),F3(),(Initialize (IExec (F4(),F3(),F2()))))
by SCMPDS_4:def 5
;
verum