set i1 = F3(),F4() <=0_goto ((card F2()) + 3);
set J = F2() ';' (AddTo F3(),F4(),(- F5()));
set i3 = goto (- ((card F2()) + 2));
set FOR = for-down F3(),F4(),F5(),F2();
set pFOR = stop (for-down F3(),F4(),F5(),F2());
set s1 = (Initialize F1()) +* (stop (for-down F3(),F4(),F5(),F2()));
set ps = ProgramPart F1();
set sJ = (Initialize F1()) +* (stop (F2() ';' (AddTo F3(),F4(),(- F5()))));
set mJ = LifeSpan (ProgramPart ((Initialize F1()) +* (stop (F2() ';' (AddTo F3(),F4(),(- F5())))))),((Initialize F1()) +* (stop (F2() ';' (AddTo F3(),F4(),(- F5())))));
set m1 = (LifeSpan (ProgramPart ((Initialize F1()) +* (stop (F2() ';' (AddTo F3(),F4(),(- F5())))))),((Initialize F1()) +* (stop (F2() ';' (AddTo F3(),F4(),(- F5())))))) + 2;
set s2 = (Initialize (IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),F1())) +* (stop (for-down F3(),F4(),F5(),F2()));
set m2 = LifeSpan (ProgramPart ((Initialize (IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),F1())) +* (stop (for-down F3(),F4(),F5(),F2())))),((Initialize (IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),F1())) +* (stop (for-down F3(),F4(),F5(),F2())));
I1:
(Initialize F1()) +* (stop (F2() ';' (AddTo F3(),F4(),(- F5())))) = F1() +* (Initialize (stop (F2() ';' (AddTo F3(),F4(),(- F5())))))
by SCMPDS_4:5;
I2:
(Initialize (IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),F1())) +* (stop (for-down F3(),F4(),F5(),F2())) = (IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),F1()) +* (Initialize (stop (for-down F3(),F4(),F5(),F2())))
by SCMPDS_4:5;
I0:
(Initialize F1()) +* (stop (for-down F3(),F4(),F5(),F2())) = F1() +* (Initialize (stop (for-down F3(),F4(),F5(),F2())))
by SCMPDS_4:5;
A5:
Initialize (stop (F2() ';' (AddTo F3(),F4(),(- F5())))) c= (Initialize F1()) +* (stop (F2() ';' (AddTo F3(),F4(),(- F5()))))
by I1, FUNCT_4:26;
A6:
( F2() is_closed_on F1() & F2() is_halting_on F1() )
by A2, A3, A4;
then
F2() ';' (AddTo F3(),F4(),(- F5())) is_closed_on F1()
by Th6;
then A7:
F2() ';' (AddTo F3(),F4(),(- F5())) is_closed_on (Initialize F1()) +* (stop (F2() ';' (AddTo F3(),F4(),(- F5()))))
by SCMPDS_6:38;
B8:
F2() ';' (AddTo F3(),F4(),(- F5())) is_halting_on F1()
by A6, Th6;
then A8:
ProgramPart ((Initialize F1()) +* (stop (F2() ';' (AddTo F3(),F4(),(- F5()))))) halts_on (Initialize F1()) +* (stop (F2() ';' (AddTo F3(),F4(),(- F5()))))
by SCMPDS_6:def 3;
I5:
(Initialize ((Initialize F1()) +* (stop (F2() ';' (AddTo F3(),F4(),(- F5())))))) +* (stop (F2() ';' (AddTo F3(),F4(),(- F5())))) = ((Initialize F1()) +* (stop (F2() ';' (AddTo F3(),F4(),(- F5()))))) +* (Initialize (stop (F2() ';' (AddTo F3(),F4(),(- F5())))))
by SCMPDS_4:5;
(Initialize F1()) +* (stop (F2() ';' (AddTo F3(),F4(),(- F5())))) = (Initialize ((Initialize F1()) +* (stop (F2() ';' (AddTo F3(),F4(),(- F5())))))) +* (stop (F2() ';' (AddTo F3(),F4(),(- F5()))))
by A5, I5, FUNCT_4:79;
then
ProgramPart ((Initialize ((Initialize F1()) +* (stop (F2() ';' (AddTo F3(),F4(),(- F5())))))) +* (stop (F2() ';' (AddTo F3(),F4(),(- F5()))))) halts_on (Initialize ((Initialize F1()) +* (stop (F2() ';' (AddTo F3(),F4(),(- F5())))))) +* (stop (F2() ';' (AddTo F3(),F4(),(- F5()))))
by B8, SCMPDS_6:def 3;
then A9:
F2() ';' (AddTo F3(),F4(),(- F5())) is_halting_on (Initialize F1()) +* (stop (F2() ';' (AddTo F3(),F4(),(- F5()))))
by SCMPDS_6:def 3;
A10:
for-down F3(),F4(),F5(),F2() = (F3(),F4() <=0_goto ((card F2()) + 3)) ';' ((F2() ';' (AddTo F3(),F4(),(- F5()))) ';' (goto (- ((card F2()) + 2))))
by Lm3;
A12: Comput (ProgramPart ((Initialize F1()) +* (stop (for-down F3(),F4(),F5(),F2())))),((Initialize F1()) +* (stop (for-down F3(),F4(),F5(),F2()))),(0 + 1) =
Following (ProgramPart ((Initialize F1()) +* (stop (for-down F3(),F4(),F5(),F2())))),(Comput (ProgramPart ((Initialize F1()) +* (stop (for-down F3(),F4(),F5(),F2())))),((Initialize F1()) +* (stop (for-down F3(),F4(),F5(),F2()))),0 )
by AMI_1:14
.=
Following (ProgramPart ((Initialize F1()) +* (stop (for-down F3(),F4(),F5(),F2())))),((Initialize F1()) +* (stop (for-down F3(),F4(),F5(),F2())))
by AMI_1:13
.=
Exec (F3(),F4() <=0_goto ((card F2()) + 3)),((Initialize F1()) +* (stop (for-down F3(),F4(),F5(),F2())))
by A10, I0, SCMPDS_6:22
;
set m3 = (LifeSpan (ProgramPart ((Initialize F1()) +* (stop (F2() ';' (AddTo F3(),F4(),(- F5())))))),((Initialize F1()) +* (stop (F2() ';' (AddTo F3(),F4(),(- F5())))))) + 1;
set s4 = Comput (ProgramPart ((Initialize F1()) +* (stop (for-down F3(),F4(),F5(),F2())))),((Initialize F1()) +* (stop (for-down F3(),F4(),F5(),F2()))),1;
set b = DataLoc (F1() . F3()),F4();
A13:
card (F2() ';' (AddTo F3(),F4(),(- F5()))) = (card F2()) + 1
by SCMP_GCD:8;
set s6 = Comput (ProgramPart ((Initialize F1()) +* (stop (for-down F3(),F4(),F5(),F2())))),((Initialize F1()) +* (stop (for-down F3(),F4(),F5(),F2()))),((LifeSpan (ProgramPart ((Initialize F1()) +* (stop (F2() ';' (AddTo F3(),F4(),(- F5())))))),((Initialize F1()) +* (stop (F2() ';' (AddTo F3(),F4(),(- F5())))))) + 1);
A14:
not DataLoc (F1() . F3()),F4() in dom (Initialize (stop (for-down F3(),F4(),F5(),F2())))
by SCMPDS_4:31;
not F3() in dom (Initialize (stop (for-down F3(),F4(),F5(),F2())))
by SCMPDS_4:31;
then A15: ((Initialize F1()) +* (stop (for-down F3(),F4(),F5(),F2()))) . (DataLoc (((Initialize F1()) +* (stop (for-down F3(),F4(),F5(),F2()))) . F3()),F4()) =
((Initialize F1()) +* (stop (for-down F3(),F4(),F5(),F2()))) . (DataLoc (F1() . F3()),F4())
by I0, FUNCT_4:12
.=
F1() . (DataLoc (F1() . F3()),F4())
by A14, I0, FUNCT_4:12
;
set s5 = Comput (ProgramPart (Comput (ProgramPart ((Initialize F1()) +* (stop (for-down F3(),F4(),F5(),F2())))),((Initialize F1()) +* (stop (for-down F3(),F4(),F5(),F2()))),1)),(Comput (ProgramPart ((Initialize F1()) +* (stop (for-down F3(),F4(),F5(),F2())))),((Initialize F1()) +* (stop (for-down F3(),F4(),F5(),F2()))),1),(LifeSpan (ProgramPart ((Initialize F1()) +* (stop (F2() ';' (AddTo F3(),F4(),(- F5())))))),((Initialize F1()) +* (stop (F2() ';' (AddTo F3(),F4(),(- F5()))))));
set l1 = (card (F2() ';' (AddTo F3(),F4(),(- F5())))) + 1;
(card F2()) + 2 < (card F2()) + 3
by XREAL_1:8;
then A16:
(card (F2() ';' (AddTo F3(),F4(),(- F5())))) + 1 in dom (for-down F3(),F4(),F5(),F2())
by A13, SCMPDS_7:61;
ProgramPart ((Initialize F1()) +* (stop (for-down F3(),F4(),F5(),F2()))) = ProgramPart (Comput (ProgramPart ((Initialize F1()) +* (stop (for-down F3(),F4(),F5(),F2())))),((Initialize F1()) +* (stop (for-down F3(),F4(),F5(),F2()))),1)
by AMI_1:123;
then A17:
Comput (ProgramPart ((Initialize F1()) +* (stop (for-down F3(),F4(),F5(),F2())))),((Initialize F1()) +* (stop (for-down F3(),F4(),F5(),F2()))),((LifeSpan (ProgramPart ((Initialize F1()) +* (stop (F2() ';' (AddTo F3(),F4(),(- F5())))))),((Initialize F1()) +* (stop (F2() ';' (AddTo F3(),F4(),(- F5())))))) + 1) = Comput (ProgramPart (Comput (ProgramPart ((Initialize F1()) +* (stop (for-down F3(),F4(),F5(),F2())))),((Initialize F1()) +* (stop (for-down F3(),F4(),F5(),F2()))),1)),(Comput (ProgramPart ((Initialize F1()) +* (stop (for-down F3(),F4(),F5(),F2())))),((Initialize F1()) +* (stop (for-down F3(),F4(),F5(),F2()))),1),(LifeSpan (ProgramPart ((Initialize F1()) +* (stop (F2() ';' (AddTo F3(),F4(),(- F5())))))),((Initialize F1()) +* (stop (F2() ';' (AddTo F3(),F4(),(- F5()))))))
by AMI_1:51;
A18:
DataPart ((Initialize F1()) +* (stop (F2() ';' (AddTo F3(),F4(),(- F5()))))) = DataPart ((Initialize F1()) +* (stop (for-down F3(),F4(),F5(),F2())))
by FUNCT_7:134, SCMPDS_4:24;
now let x be
Int_position ;
((Initialize F1()) +* (stop (F2() ';' (AddTo F3(),F4(),(- F5()))))) . x = (Comput (ProgramPart ((Initialize F1()) +* (stop (for-down F3(),F4(),F5(),F2())))),((Initialize F1()) +* (stop (for-down F3(),F4(),F5(),F2()))),1) . xthus ((Initialize F1()) +* (stop (F2() ';' (AddTo F3(),F4(),(- F5()))))) . x =
((Initialize F1()) +* (stop (for-down F3(),F4(),F5(),F2()))) . x
by A18, SCMPDS_4:23
.=
(Comput (ProgramPart ((Initialize F1()) +* (stop (for-down F3(),F4(),F5(),F2())))),((Initialize F1()) +* (stop (for-down F3(),F4(),F5(),F2()))),1) . x
by A12, SCMPDS_2:68
;
verum end;
then A19:
DataPart ((Initialize F1()) +* (stop (F2() ';' (AddTo F3(),F4(),(- F5()))))) = DataPart (Comput (ProgramPart ((Initialize F1()) +* (stop (for-down F3(),F4(),F5(),F2())))),((Initialize F1()) +* (stop (for-down F3(),F4(),F5(),F2()))),1)
by SCMPDS_4:23;
A20:
IC ((Initialize F1()) +* (stop (for-down F3(),F4(),F5(),F2()))) = 0
by SCMPDS_6:21;
( for-down F3(),F4(),F5(),F2() c= Initialize (stop (for-down F3(),F4(),F5(),F2())) & Initialize (stop (for-down F3(),F4(),F5(),F2())) c= (Initialize F1()) +* (stop (for-down F3(),F4(),F5(),F2())) )
by I0, FUNCT_4:26, SCMPDS_6:17;
then A21:
for-down F3(),F4(),F5(),F2() c= (Initialize F1()) +* (stop (for-down F3(),F4(),F5(),F2()))
by XBOOLE_1:1;
Shift (F2() ';' (AddTo F3(),F4(),(- F5()))),1 c= for-down F3(),F4(),F5(),F2()
by Lm4;
then
Shift (F2() ';' (AddTo F3(),F4(),(- F5()))),1 c= (Initialize F1()) +* (stop (for-down F3(),F4(),F5(),F2()))
by A21, XBOOLE_1:1;
then A22:
Shift (F2() ';' (AddTo F3(),F4(),(- F5()))),1 c= Comput (ProgramPart ((Initialize F1()) +* (stop (for-down F3(),F4(),F5(),F2())))),((Initialize F1()) +* (stop (for-down F3(),F4(),F5(),F2()))),1
by AMI_1:81;
set m0 = LifeSpan (ProgramPart ((Initialize F1()) +* (stop (for-down F3(),F4(),F5(),F2())))),((Initialize F1()) +* (stop (for-down F3(),F4(),F5(),F2())));
A23:
IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),F1() = (Result (ProgramPart ((Initialize F1()) +* (stop (F2() ';' (AddTo F3(),F4(),(- F5())))))),((Initialize F1()) +* (stop (F2() ';' (AddTo F3(),F4(),(- F5())))))) +* (F1() | NAT )
by SCMPDS_4:def 8;
thus
( P1[F1()] or not P1[F1()] )
; IExec (for-down F3(),F4(),F5(),F2()),F1() = IExec (for-down F3(),F4(),F5(),F2()),(IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),F1())
A24:
dom (ProgramPart F1()) = NAT
by COMPOS_1:34;
set m4 = ((LifeSpan (ProgramPart ((Initialize F1()) +* (stop (F2() ';' (AddTo F3(),F4(),(- F5())))))),((Initialize F1()) +* (stop (F2() ';' (AddTo F3(),F4(),(- F5())))))) + 1) + 1;
set s7 = Comput (ProgramPart ((Initialize F1()) +* (stop (for-down F3(),F4(),F5(),F2())))),((Initialize F1()) +* (stop (for-down F3(),F4(),F5(),F2()))),(((LifeSpan (ProgramPart ((Initialize F1()) +* (stop (F2() ';' (AddTo F3(),F4(),(- F5())))))),((Initialize F1()) +* (stop (F2() ';' (AddTo F3(),F4(),(- F5())))))) + 1) + 1);
A25: dom (ProgramPart F1()) =
(dom F1()) /\ NAT
by RELAT_1:90
.=
(({(IC SCMPDS )} \/ SCM-Data-Loc ) \/ NAT ) /\ NAT
by SCMPDS_4:19
.=
NAT
by XBOOLE_1:21
;
A26: IC (Comput (ProgramPart ((Initialize F1()) +* (stop (for-down F3(),F4(),F5(),F2())))),((Initialize F1()) +* (stop (for-down F3(),F4(),F5(),F2()))),1) =
(Comput (ProgramPart ((Initialize F1()) +* (stop (for-down F3(),F4(),F5(),F2())))),((Initialize F1()) +* (stop (for-down F3(),F4(),F5(),F2()))),1) . (IC SCMPDS )
.=
succ (IC ((Initialize F1()) +* (stop (for-down F3(),F4(),F5(),F2()))))
by A2, A12, A15, SCMPDS_2:68
.=
0 + 1
by A20
;
then A27:
IC (Comput (ProgramPart (Comput (ProgramPart ((Initialize F1()) +* (stop (for-down F3(),F4(),F5(),F2())))),((Initialize F1()) +* (stop (for-down F3(),F4(),F5(),F2()))),1)),(Comput (ProgramPart ((Initialize F1()) +* (stop (for-down F3(),F4(),F5(),F2())))),((Initialize F1()) +* (stop (for-down F3(),F4(),F5(),F2()))),1),(LifeSpan (ProgramPart ((Initialize F1()) +* (stop (F2() ';' (AddTo F3(),F4(),(- F5())))))),((Initialize F1()) +* (stop (F2() ';' (AddTo F3(),F4(),(- F5()))))))) = (card (F2() ';' (AddTo F3(),F4(),(- F5())))) + 1
by A13, A5, A9, A7, A19, A22, SCMPDS_7:36;
then A28: CurInstr (ProgramPart (Comput (ProgramPart ((Initialize F1()) +* (stop (for-down F3(),F4(),F5(),F2())))),((Initialize F1()) +* (stop (for-down F3(),F4(),F5(),F2()))),((LifeSpan (ProgramPart ((Initialize F1()) +* (stop (F2() ';' (AddTo F3(),F4(),(- F5())))))),((Initialize F1()) +* (stop (F2() ';' (AddTo F3(),F4(),(- F5())))))) + 1))),(Comput (ProgramPart ((Initialize F1()) +* (stop (for-down F3(),F4(),F5(),F2())))),((Initialize F1()) +* (stop (for-down F3(),F4(),F5(),F2()))),((LifeSpan (ProgramPart ((Initialize F1()) +* (stop (F2() ';' (AddTo F3(),F4(),(- F5())))))),((Initialize F1()) +* (stop (F2() ';' (AddTo F3(),F4(),(- F5())))))) + 1)) =
(Comput (ProgramPart (Comput (ProgramPart ((Initialize F1()) +* (stop (for-down F3(),F4(),F5(),F2())))),((Initialize F1()) +* (stop (for-down F3(),F4(),F5(),F2()))),1)),(Comput (ProgramPart ((Initialize F1()) +* (stop (for-down F3(),F4(),F5(),F2())))),((Initialize F1()) +* (stop (for-down F3(),F4(),F5(),F2()))),1),(LifeSpan (ProgramPart ((Initialize F1()) +* (stop (F2() ';' (AddTo F3(),F4(),(- F5())))))),((Initialize F1()) +* (stop (F2() ';' (AddTo F3(),F4(),(- F5()))))))) . ((card (F2() ';' (AddTo F3(),F4(),(- F5())))) + 1)
by A17, COMPOS_1:38
.=
(Comput (ProgramPart ((Initialize F1()) +* (stop (for-down F3(),F4(),F5(),F2())))),((Initialize F1()) +* (stop (for-down F3(),F4(),F5(),F2()))),1) . ((card (F2() ';' (AddTo F3(),F4(),(- F5())))) + 1)
by AMI_1:54
.=
((Initialize F1()) +* (stop (for-down F3(),F4(),F5(),F2()))) . ((card (F2() ';' (AddTo F3(),F4(),(- F5())))) + 1)
by AMI_1:54
.=
(for-down F3(),F4(),F5(),F2()) . ((card (F2() ';' (AddTo F3(),F4(),(- F5())))) + 1)
by A16, A21, GRFUNC_1:8
.=
goto (- ((card F2()) + 2))
by A13, SCMPDS_7:62
;
A29: Comput (ProgramPart ((Initialize F1()) +* (stop (for-down F3(),F4(),F5(),F2())))),((Initialize F1()) +* (stop (for-down F3(),F4(),F5(),F2()))),(((LifeSpan (ProgramPart ((Initialize F1()) +* (stop (F2() ';' (AddTo F3(),F4(),(- F5())))))),((Initialize F1()) +* (stop (F2() ';' (AddTo F3(),F4(),(- F5())))))) + 1) + 1) =
Following (ProgramPart ((Initialize F1()) +* (stop (for-down F3(),F4(),F5(),F2())))),(Comput (ProgramPart ((Initialize F1()) +* (stop (for-down F3(),F4(),F5(),F2())))),((Initialize F1()) +* (stop (for-down F3(),F4(),F5(),F2()))),((LifeSpan (ProgramPart ((Initialize F1()) +* (stop (F2() ';' (AddTo F3(),F4(),(- F5())))))),((Initialize F1()) +* (stop (F2() ';' (AddTo F3(),F4(),(- F5())))))) + 1))
by AMI_1:14
.=
Exec (goto (- ((card F2()) + 2))),(Comput (ProgramPart ((Initialize F1()) +* (stop (for-down F3(),F4(),F5(),F2())))),((Initialize F1()) +* (stop (for-down F3(),F4(),F5(),F2()))),((LifeSpan (ProgramPart ((Initialize F1()) +* (stop (F2() ';' (AddTo F3(),F4(),(- F5())))))),((Initialize F1()) +* (stop (F2() ';' (AddTo F3(),F4(),(- F5())))))) + 1))
by A28, AMI_1:123
;
A30:
DataPart (Comput (ProgramPart ((Initialize F1()) +* (stop (F2() ';' (AddTo F3(),F4(),(- F5())))))),((Initialize F1()) +* (stop (F2() ';' (AddTo F3(),F4(),(- F5()))))),(LifeSpan (ProgramPart ((Initialize F1()) +* (stop (F2() ';' (AddTo F3(),F4(),(- F5())))))),((Initialize F1()) +* (stop (F2() ';' (AddTo F3(),F4(),(- F5()))))))) = DataPart (Comput (ProgramPart (Comput (ProgramPart ((Initialize F1()) +* (stop (for-down F3(),F4(),F5(),F2())))),((Initialize F1()) +* (stop (for-down F3(),F4(),F5(),F2()))),1)),(Comput (ProgramPart ((Initialize F1()) +* (stop (for-down F3(),F4(),F5(),F2())))),((Initialize F1()) +* (stop (for-down F3(),F4(),F5(),F2()))),1),(LifeSpan (ProgramPart ((Initialize F1()) +* (stop (F2() ';' (AddTo F3(),F4(),(- F5())))))),((Initialize F1()) +* (stop (F2() ';' (AddTo F3(),F4(),(- F5())))))))
by A13, A5, A9, A7, A26, A19, A22, SCMPDS_7:36;
now let x be
Int_position ;
(Comput (ProgramPart ((Initialize F1()) +* (stop (for-down F3(),F4(),F5(),F2())))),((Initialize F1()) +* (stop (for-down F3(),F4(),F5(),F2()))),(((LifeSpan (ProgramPart ((Initialize F1()) +* (stop (F2() ';' (AddTo F3(),F4(),(- F5())))))),((Initialize F1()) +* (stop (F2() ';' (AddTo F3(),F4(),(- F5())))))) + 1) + 1)) . x = ((Initialize (IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),F1())) +* (stop (for-down F3(),F4(),F5(),F2()))) . x
not
x in dom (Initialize (stop (for-down F3(),F4(),F5(),F2())))
by SCMPDS_4:31;
then A31:
((Initialize (IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),F1())) +* (stop (for-down F3(),F4(),F5(),F2()))) . x = (IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),F1()) . x
by I2, FUNCT_4:12;
A32:
not
x in dom (F1() | NAT )
by A24, SCMPDS_2:53;
(Comput (ProgramPart (Comput (ProgramPart ((Initialize F1()) +* (stop (for-down F3(),F4(),F5(),F2())))),((Initialize F1()) +* (stop (for-down F3(),F4(),F5(),F2()))),1)),(Comput (ProgramPart ((Initialize F1()) +* (stop (for-down F3(),F4(),F5(),F2())))),((Initialize F1()) +* (stop (for-down F3(),F4(),F5(),F2()))),1),(LifeSpan (ProgramPart ((Initialize F1()) +* (stop (F2() ';' (AddTo F3(),F4(),(- F5())))))),((Initialize F1()) +* (stop (F2() ';' (AddTo F3(),F4(),(- F5()))))))) . x =
(Comput (ProgramPart ((Initialize F1()) +* (stop (F2() ';' (AddTo F3(),F4(),(- F5())))))),((Initialize F1()) +* (stop (F2() ';' (AddTo F3(),F4(),(- F5()))))),(LifeSpan (ProgramPart ((Initialize F1()) +* (stop (F2() ';' (AddTo F3(),F4(),(- F5())))))),((Initialize F1()) +* (stop (F2() ';' (AddTo F3(),F4(),(- F5()))))))) . x
by A30, SCMPDS_4:23
.=
(Result (ProgramPart ((Initialize F1()) +* (stop (F2() ';' (AddTo F3(),F4(),(- F5())))))),((Initialize F1()) +* (stop (F2() ';' (AddTo F3(),F4(),(- F5())))))) . x
by A8, AMI_1:122
.=
(IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),F1()) . x
by A23, A32, FUNCT_4:12
;
hence
(Comput (ProgramPart ((Initialize F1()) +* (stop (for-down F3(),F4(),F5(),F2())))),((Initialize F1()) +* (stop (for-down F3(),F4(),F5(),F2()))),(((LifeSpan (ProgramPart ((Initialize F1()) +* (stop (F2() ';' (AddTo F3(),F4(),(- F5())))))),((Initialize F1()) +* (stop (F2() ';' (AddTo F3(),F4(),(- F5())))))) + 1) + 1)) . x = ((Initialize (IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),F1())) +* (stop (for-down F3(),F4(),F5(),F2()))) . x
by A17, A29, A31, SCMPDS_2:66;
verum end;
then A33:
DataPart (Comput (ProgramPart ((Initialize F1()) +* (stop (for-down F3(),F4(),F5(),F2())))),((Initialize F1()) +* (stop (for-down F3(),F4(),F5(),F2()))),(((LifeSpan (ProgramPart ((Initialize F1()) +* (stop (F2() ';' (AddTo F3(),F4(),(- F5())))))),((Initialize F1()) +* (stop (F2() ';' (AddTo F3(),F4(),(- F5())))))) + 1) + 1)) = DataPart ((Initialize (IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),F1())) +* (stop (for-down F3(),F4(),F5(),F2())))
by SCMPDS_4:23;
A34:
for t being State of SCMPDS st P1[ Dstate t] & t . F3() = F1() . F3() & t . (DataLoc (F1() . F3()),F4()) > 0 holds
( (IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),t) . F3() = t . F3() & (IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),t) . (DataLoc (F1() . F3()),F4()) = (t . (DataLoc (F1() . F3()),F4())) - F5() & F2() is_closed_on t & F2() is_halting_on t & P1[ Dstate (IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),t)] )
by A4;
A35:
P1[ Dstate F1()]
by A3;
( ( P1[F1()] or not P1[F1()] ) & for-down F3(),F4(),F5(),F2() is_closed_on F1() & for-down F3(),F4(),F5(),F2() is_halting_on F1() )
from SCPISORT:sch 1(A1, A35, A34);
then A36:
ProgramPart ((Initialize F1()) +* (stop (for-down F3(),F4(),F5(),F2()))) halts_on (Initialize F1()) +* (stop (for-down F3(),F4(),F5(),F2()))
by SCMPDS_6:def 3;
set Es = IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),F1();
set bj = DataLoc ((IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),F1()) . F3()),F4();
(IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),F1()) . F3() = F1() . F3()
by A2, A3, A4;
then A37:
for t being State of SCMPDS st P1[ Dstate t] & t . F3() = (IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),F1()) . F3() & t . (DataLoc ((IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),F1()) . F3()),F4()) > 0 holds
( (IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),t) . F3() = t . F3() & (IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),t) . (DataLoc ((IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),F1()) . F3()),F4()) = (t . (DataLoc ((IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),F1()) . F3()),F4())) - F5() & F2() is_closed_on t & F2() is_halting_on t & P1[ Dstate (IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),t)] )
by A4;
A38:
P1[ Dstate (IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),F1())]
by A2, A3, A4;
( ( P1[ IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),F1()] or not P1[ IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),F1()] ) & for-down F3(),F4(),F5(),F2() is_closed_on IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),F1() & for-down F3(),F4(),F5(),F2() is_halting_on IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),F1() )
from SCPISORT:sch 1(A1, A38, A37);
then A39:
ProgramPart ((Initialize (IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),F1())) +* (stop (for-down F3(),F4(),F5(),F2()))) halts_on (Initialize (IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),F1())) +* (stop (for-down F3(),F4(),F5(),F2()))
by SCMPDS_6:def 3;
IC (Comput (ProgramPart ((Initialize F1()) +* (stop (for-down F3(),F4(),F5(),F2())))),((Initialize F1()) +* (stop (for-down F3(),F4(),F5(),F2()))),(((LifeSpan (ProgramPart ((Initialize F1()) +* (stop (F2() ';' (AddTo F3(),F4(),(- F5())))))),((Initialize F1()) +* (stop (F2() ';' (AddTo F3(),F4(),(- F5())))))) + 1) + 1)) =
(Comput (ProgramPart ((Initialize F1()) +* (stop (for-down F3(),F4(),F5(),F2())))),((Initialize F1()) +* (stop (for-down F3(),F4(),F5(),F2()))),(((LifeSpan (ProgramPart ((Initialize F1()) +* (stop (F2() ';' (AddTo F3(),F4(),(- F5())))))),((Initialize F1()) +* (stop (F2() ';' (AddTo F3(),F4(),(- F5())))))) + 1) + 1)) . (IC SCMPDS )
.=
ICplusConst (Comput (ProgramPart ((Initialize F1()) +* (stop (for-down F3(),F4(),F5(),F2())))),((Initialize F1()) +* (stop (for-down F3(),F4(),F5(),F2()))),((LifeSpan (ProgramPart ((Initialize F1()) +* (stop (F2() ';' (AddTo F3(),F4(),(- F5())))))),((Initialize F1()) +* (stop (F2() ';' (AddTo F3(),F4(),(- F5())))))) + 1)),(0 - ((card F2()) + 2))
by A29, SCMPDS_2:66
.=
0
by A13, A27, A17, SCMPDS_7:1
;
then A40:
IC ((Initialize (IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),F1())) +* (stop (for-down F3(),F4(),F5(),F2()))) = IC (Comput (ProgramPart ((Initialize F1()) +* (stop (for-down F3(),F4(),F5(),F2())))),((Initialize F1()) +* (stop (for-down F3(),F4(),F5(),F2()))),((LifeSpan (ProgramPart ((Initialize F1()) +* (stop (F2() ';' (AddTo F3(),F4(),(- F5())))))),((Initialize F1()) +* (stop (F2() ';' (AddTo F3(),F4(),(- F5())))))) + 2))
by SCMPDS_6:21;
A41: (IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),F1()) | NAT =
((Result (ProgramPart ((Initialize F1()) +* (stop (F2() ';' (AddTo F3(),F4(),(- F5())))))),((Initialize F1()) +* (stop (F2() ';' (AddTo F3(),F4(),(- F5())))))) +* (ProgramPart F1())) | NAT
by SCMPDS_4:def 8
.=
ProgramPart F1()
by A25, FUNCT_4:24
;
NX:
ProgramPart ((Initialize F1()) +* (stop (for-down F3(),F4(),F5(),F2()))) = ProgramPart (Comput (ProgramPart ((Initialize F1()) +* (stop (for-down F3(),F4(),F5(),F2())))),((Initialize F1()) +* (stop (for-down F3(),F4(),F5(),F2()))),((LifeSpan (ProgramPart ((Initialize F1()) +* (stop (F2() ';' (AddTo F3(),F4(),(- F5())))))),((Initialize F1()) +* (stop (F2() ';' (AddTo F3(),F4(),(- F5())))))) + 2))
by AMI_1:123;
B42: ProgramPart ((Initialize (IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),F1())) +* (stop (for-down F3(),F4(),F5(),F2()))) =
ProgramPart (((Result (ProgramPart ((Initialize F1()) +* (stop (F2() ';' (AddTo F3(),F4(),(- F5())))))),((Initialize F1()) +* (stop (F2() ';' (AddTo F3(),F4(),(- F5())))))) +* (ProgramPart F1())) +* (Initialize (stop (for-down F3(),F4(),F5(),F2()))))
by I2, SCMPDS_4:def 8
.=
(ProgramPart ((Result (ProgramPart ((Initialize F1()) +* (stop (F2() ';' (AddTo F3(),F4(),(- F5())))))),((Initialize F1()) +* (stop (F2() ';' (AddTo F3(),F4(),(- F5())))))) +* (ProgramPart F1()))) +* (ProgramPart (Initialize (stop (for-down F3(),F4(),F5(),F2()))))
by FUNCT_4:75
.=
(ProgramPart F1()) +* (ProgramPart (Initialize (stop (for-down F3(),F4(),F5(),F2()))))
by A25, FUNCT_4:24
.=
ProgramPart ((Initialize F1()) +* (stop (for-down F3(),F4(),F5(),F2())))
by I0, FUNCT_4:75
.=
ProgramPart (Comput (ProgramPart ((Initialize F1()) +* (stop (for-down F3(),F4(),F5(),F2())))),((Initialize F1()) +* (stop (for-down F3(),F4(),F5(),F2()))),((LifeSpan (ProgramPart ((Initialize F1()) +* (stop (F2() ';' (AddTo F3(),F4(),(- F5())))))),((Initialize F1()) +* (stop (F2() ';' (AddTo F3(),F4(),(- F5())))))) + 2))
by AMI_1:123
;
then A42:
Comput (ProgramPart ((Initialize F1()) +* (stop (for-down F3(),F4(),F5(),F2())))),((Initialize F1()) +* (stop (for-down F3(),F4(),F5(),F2()))),((LifeSpan (ProgramPart ((Initialize F1()) +* (stop (F2() ';' (AddTo F3(),F4(),(- F5())))))),((Initialize F1()) +* (stop (F2() ';' (AddTo F3(),F4(),(- F5())))))) + 2) = (Initialize (IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),F1())) +* (stop (for-down F3(),F4(),F5(),F2()))
by A33, A40, SCMPDS_7:7;
then
CurInstr (ProgramPart ((Initialize F1()) +* (stop (for-down F3(),F4(),F5(),F2())))),(Comput (ProgramPart ((Initialize F1()) +* (stop (for-down F3(),F4(),F5(),F2())))),((Initialize F1()) +* (stop (for-down F3(),F4(),F5(),F2()))),((LifeSpan (ProgramPart ((Initialize F1()) +* (stop (F2() ';' (AddTo F3(),F4(),(- F5())))))),((Initialize F1()) +* (stop (F2() ';' (AddTo F3(),F4(),(- F5())))))) + 2)) = F3(),F4() <=0_goto ((card F2()) + 3)
by A10, NX, I2, SCMPDS_6:22;
then
LifeSpan (ProgramPart ((Initialize F1()) +* (stop (for-down F3(),F4(),F5(),F2())))),((Initialize F1()) +* (stop (for-down F3(),F4(),F5(),F2()))) > (LifeSpan (ProgramPart ((Initialize F1()) +* (stop (F2() ';' (AddTo F3(),F4(),(- F5())))))),((Initialize F1()) +* (stop (F2() ';' (AddTo F3(),F4(),(- F5())))))) + 2
by A36, SCMPDS_6:2, SCMPDS_6:30;
then consider nn being Nat such that
A43:
LifeSpan (ProgramPart ((Initialize F1()) +* (stop (for-down F3(),F4(),F5(),F2())))),((Initialize F1()) +* (stop (for-down F3(),F4(),F5(),F2()))) = ((LifeSpan (ProgramPart ((Initialize F1()) +* (stop (F2() ';' (AddTo F3(),F4(),(- F5())))))),((Initialize F1()) +* (stop (F2() ';' (AddTo F3(),F4(),(- F5())))))) + 2) + nn
by NAT_1:10;
reconsider nn = nn as Element of NAT by ORDINAL1:def 13;
T:
ProgramPart ((Initialize F1()) +* (stop (for-down F3(),F4(),F5(),F2()))) = ProgramPart ((Initialize (IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),F1())) +* (stop (for-down F3(),F4(),F5(),F2())))
by B42, AMI_1:123;
then
Comput (ProgramPart ((Initialize F1()) +* (stop (for-down F3(),F4(),F5(),F2())))),((Initialize F1()) +* (stop (for-down F3(),F4(),F5(),F2()))),(((LifeSpan (ProgramPart ((Initialize F1()) +* (stop (F2() ';' (AddTo F3(),F4(),(- F5())))))),((Initialize F1()) +* (stop (F2() ';' (AddTo F3(),F4(),(- F5())))))) + 2) + (LifeSpan (ProgramPart ((Initialize (IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),F1())) +* (stop (for-down F3(),F4(),F5(),F2())))),((Initialize (IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),F1())) +* (stop (for-down F3(),F4(),F5(),F2()))))) = Comput (ProgramPart ((Initialize (IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),F1())) +* (stop (for-down F3(),F4(),F5(),F2())))),((Initialize (IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),F1())) +* (stop (for-down F3(),F4(),F5(),F2()))),(LifeSpan (ProgramPart ((Initialize (IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),F1())) +* (stop (for-down F3(),F4(),F5(),F2())))),((Initialize (IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),F1())) +* (stop (for-down F3(),F4(),F5(),F2()))))
by A42, AMI_1:51;
then
CurInstr (ProgramPart ((Initialize F1()) +* (stop (for-down F3(),F4(),F5(),F2())))),(Comput (ProgramPart ((Initialize F1()) +* (stop (for-down F3(),F4(),F5(),F2())))),((Initialize F1()) +* (stop (for-down F3(),F4(),F5(),F2()))),(((LifeSpan (ProgramPart ((Initialize F1()) +* (stop (F2() ';' (AddTo F3(),F4(),(- F5())))))),((Initialize F1()) +* (stop (F2() ';' (AddTo F3(),F4(),(- F5())))))) + 2) + (LifeSpan (ProgramPart ((Initialize (IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),F1())) +* (stop (for-down F3(),F4(),F5(),F2())))),((Initialize (IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),F1())) +* (stop (for-down F3(),F4(),F5(),F2())))))) = halt SCMPDS
by A39, T, AMI_1:def 46;
then
((LifeSpan (ProgramPart ((Initialize F1()) +* (stop (F2() ';' (AddTo F3(),F4(),(- F5())))))),((Initialize F1()) +* (stop (F2() ';' (AddTo F3(),F4(),(- F5())))))) + 2) + (LifeSpan (ProgramPart ((Initialize (IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),F1())) +* (stop (for-down F3(),F4(),F5(),F2())))),((Initialize (IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),F1())) +* (stop (for-down F3(),F4(),F5(),F2())))) >= LifeSpan (ProgramPart ((Initialize F1()) +* (stop (for-down F3(),F4(),F5(),F2())))),((Initialize F1()) +* (stop (for-down F3(),F4(),F5(),F2())))
by A36, AMI_1:def 46;
then A44:
LifeSpan (ProgramPart ((Initialize (IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),F1())) +* (stop (for-down F3(),F4(),F5(),F2())))),((Initialize (IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),F1())) +* (stop (for-down F3(),F4(),F5(),F2()))) >= nn
by A43, XREAL_1:8;
A45:
Comput (ProgramPart ((Initialize F1()) +* (stop (for-down F3(),F4(),F5(),F2())))),((Initialize F1()) +* (stop (for-down F3(),F4(),F5(),F2()))),(LifeSpan (ProgramPart ((Initialize F1()) +* (stop (for-down F3(),F4(),F5(),F2())))),((Initialize F1()) +* (stop (for-down F3(),F4(),F5(),F2())))) = Comput (ProgramPart ((Initialize (IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),F1())) +* (stop (for-down F3(),F4(),F5(),F2())))),((Initialize (IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),F1())) +* (stop (for-down F3(),F4(),F5(),F2()))),nn
by A42, A43, T, AMI_1:51;
then
CurInstr (ProgramPart ((Initialize (IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),F1())) +* (stop (for-down F3(),F4(),F5(),F2())))),(Comput (ProgramPart ((Initialize (IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),F1())) +* (stop (for-down F3(),F4(),F5(),F2())))),((Initialize (IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),F1())) +* (stop (for-down F3(),F4(),F5(),F2()))),nn) = halt SCMPDS
by A36, T, AMI_1:def 46;
then
nn >= LifeSpan (ProgramPart ((Initialize (IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),F1())) +* (stop (for-down F3(),F4(),F5(),F2())))),((Initialize (IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),F1())) +* (stop (for-down F3(),F4(),F5(),F2())))
by A39, AMI_1:def 46;
then
nn = LifeSpan (ProgramPart ((Initialize (IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),F1())) +* (stop (for-down F3(),F4(),F5(),F2())))),((Initialize (IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),F1())) +* (stop (for-down F3(),F4(),F5(),F2())))
by A44, XXREAL_0:1;
then
Result (ProgramPart ((Initialize F1()) +* (stop (for-down F3(),F4(),F5(),F2())))),((Initialize F1()) +* (stop (for-down F3(),F4(),F5(),F2()))) = Comput (ProgramPart ((Initialize (IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),F1())) +* (stop (for-down F3(),F4(),F5(),F2())))),((Initialize (IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),F1())) +* (stop (for-down F3(),F4(),F5(),F2()))),(LifeSpan (ProgramPart ((Initialize (IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),F1())) +* (stop (for-down F3(),F4(),F5(),F2())))),((Initialize (IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),F1())) +* (stop (for-down F3(),F4(),F5(),F2()))))
by A36, A45, AMI_1:122;
hence IExec (for-down F3(),F4(),F5(),F2()),F1() =
(Comput (ProgramPart ((Initialize (IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),F1())) +* (stop (for-down F3(),F4(),F5(),F2())))),((Initialize (IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),F1())) +* (stop (for-down F3(),F4(),F5(),F2()))),(LifeSpan (ProgramPart ((Initialize (IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),F1())) +* (stop (for-down F3(),F4(),F5(),F2())))),((Initialize (IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),F1())) +* (stop (for-down F3(),F4(),F5(),F2()))))) +* (ProgramPart F1())
by SCMPDS_4:def 8
.=
(Result (ProgramPart ((Initialize (IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),F1())) +* (stop (for-down F3(),F4(),F5(),F2())))),((Initialize (IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),F1())) +* (stop (for-down F3(),F4(),F5(),F2())))) +* ((IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),F1()) | NAT )
by A39, A41, AMI_1:122
.=
IExec (for-down F3(),F4(),F5(),F2()),(IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),F1())
by SCMPDS_4:def 8
;
verum