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 iFOR = Initialized (stop (for-down F3(),F4(),F5(),F2()));
set iJ = Initialized (stop (F2() ';' (AddTo F3(),F4(),(- F5()))));
set s1 = F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2())));
set ps = F1() | NAT ;
set sJ = F1() +* (Initialized (stop (F2() ';' (AddTo F3(),F4(),(- F5())))));
set mJ = LifeSpan (F1() +* (Initialized (stop (F2() ';' (AddTo F3(),F4(),(- F5()))))));
set m1 = (LifeSpan (F1() +* (Initialized (stop (F2() ';' (AddTo F3(),F4(),(- F5()))))))) + 2;
set s2 = (IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),F1()) +* (Initialized (stop (for-down F3(),F4(),F5(),F2())));
set m2 = LifeSpan ((IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),F1()) +* (Initialized (stop (for-down F3(),F4(),F5(),F2()))));
A5:
Initialized (stop (F2() ';' (AddTo F3(),F4(),(- F5())))) c= F1() +* (Initialized (stop (F2() ';' (AddTo F3(),F4(),(- F5())))))
by 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 F1() +* (Initialized (stop (F2() ';' (AddTo F3(),F4(),(- F5())))))
by SCMPDS_6:38;
F2() ';' (AddTo F3(),F4(),(- F5())) is_halting_on F1()
by A6, Th6;
then A8:
ProgramPart (F1() +* (Initialized (stop (F2() ';' (AddTo F3(),F4(),(- F5())))))) halts_on F1() +* (Initialized (stop (F2() ';' (AddTo F3(),F4(),(- F5())))))
by SCMPDS_6:def 3;
F1() +* (Initialized (stop (F2() ';' (AddTo F3(),F4(),(- F5()))))) = (F1() +* (Initialized (stop (F2() ';' (AddTo F3(),F4(),(- F5())))))) +* (Initialized (stop (F2() ';' (AddTo F3(),F4(),(- F5())))))
by A5, FUNCT_4:79;
then
ProgramPart ((F1() +* (Initialized (stop (F2() ';' (AddTo F3(),F4(),(- F5())))))) +* (Initialized (stop (F2() ';' (AddTo F3(),F4(),(- F5())))))) halts_on (F1() +* (Initialized (stop (F2() ';' (AddTo F3(),F4(),(- F5())))))) +* (Initialized (stop (F2() ';' (AddTo F3(),F4(),(- F5())))))
by A8;
then A9:
F2() ';' (AddTo F3(),F4(),(- F5())) is_halting_on F1() +* (Initialized (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;
then A11:
CurInstr (ProgramPart (F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2()))))),(F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2())))) = F3(),F4() <=0_goto ((card F2()) + 3)
by SCMPDS_6:22;
A12: Comput (ProgramPart (F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2()))))),(F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2())))),(0 + 1) =
Following (ProgramPart (F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2()))))),(Comput (ProgramPart (F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2()))))),(F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2())))),0 )
by AMI_1:14
.=
Following (ProgramPart (F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2()))))),(F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2()))))
by AMI_1:13
.=
Exec (F3(),F4() <=0_goto ((card F2()) + 3)),(F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2()))))
by A11, AMI_1:def 18
;
set m3 = (LifeSpan (F1() +* (Initialized (stop (F2() ';' (AddTo F3(),F4(),(- F5()))))))) + 1;
set s4 = Comput (ProgramPart (F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2()))))),(F1() +* (Initialized (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 (F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2()))))),(F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2())))),((LifeSpan (F1() +* (Initialized (stop (F2() ';' (AddTo F3(),F4(),(- F5()))))))) + 1);
A14:
not DataLoc (F1() . F3()),F4() in dom (Initialized (stop (for-down F3(),F4(),F5(),F2())))
by SCMPDS_4:31;
not F3() in dom (Initialized (stop (for-down F3(),F4(),F5(),F2())))
by SCMPDS_4:31;
then A15: (F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2())))) . (DataLoc ((F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2())))) . F3()),F4()) =
(F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2())))) . (DataLoc (F1() . F3()),F4())
by FUNCT_4:12
.=
F1() . (DataLoc (F1() . F3()),F4())
by A14, FUNCT_4:12
;
set s5 = Comput (ProgramPart (Comput (ProgramPart (F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2()))))),(F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2())))),1)),(Comput (ProgramPart (F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2()))))),(F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2())))),1),(LifeSpan (F1() +* (Initialized (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 (F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2())))) = ProgramPart (Comput (ProgramPart (F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2()))))),(F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2())))),1)
by AMI_1:144;
then A17:
Comput (ProgramPart (F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2()))))),(F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2())))),((LifeSpan (F1() +* (Initialized (stop (F2() ';' (AddTo F3(),F4(),(- F5()))))))) + 1) = Comput (ProgramPart (Comput (ProgramPart (F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2()))))),(F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2())))),1)),(Comput (ProgramPart (F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2()))))),(F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2())))),1),(LifeSpan (F1() +* (Initialized (stop (F2() ';' (AddTo F3(),F4(),(- F5())))))))
by AMI_1:51;
A18:
DataPart (F1() +* (Initialized (stop (F2() ';' (AddTo F3(),F4(),(- F5())))))) = DataPart (F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2()))))
by SCMPDS_4:24, SCMPDS_4:36;
now let x be
Int_position ;
(F1() +* (Initialized (stop (F2() ';' (AddTo F3(),F4(),(- F5())))))) . x = (Comput (ProgramPart (F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2()))))),(F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2())))),1) . xthus (F1() +* (Initialized (stop (F2() ';' (AddTo F3(),F4(),(- F5())))))) . x =
(F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2())))) . x
by A18, SCMPDS_4:23
.=
(Comput (ProgramPart (F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2()))))),(F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2())))),1) . x
by A12, SCMPDS_2:68
;
verum end;
then A19:
DataPart (F1() +* (Initialized (stop (F2() ';' (AddTo F3(),F4(),(- F5())))))) = DataPart (Comput (ProgramPart (F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2()))))),(F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2())))),1)
by SCMPDS_4:23;
A20:
IC (F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2())))) = 0
by SCMPDS_6:21;
( for-down F3(),F4(),F5(),F2() c= Initialized (stop (for-down F3(),F4(),F5(),F2())) & Initialized (stop (for-down F3(),F4(),F5(),F2())) c= F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2()))) )
by FUNCT_4:26, SCMPDS_6:17;
then A21:
for-down F3(),F4(),F5(),F2() c= F1() +* (Initialized (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= F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2())))
by A21, XBOOLE_1:1;
then A22:
Shift (F2() ';' (AddTo F3(),F4(),(- F5()))),1 c= Comput (ProgramPart (F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2()))))),(F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2())))),1
by AMI_1:81;
set m0 = LifeSpan (F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2()))));
A23:
IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),F1() = (Result (F1() +* (Initialized (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 (F1() | NAT ) = NAT
by SCMPDS_6:1;
set m4 = ((LifeSpan (F1() +* (Initialized (stop (F2() ';' (AddTo F3(),F4(),(- F5()))))))) + 1) + 1;
set s7 = Comput (ProgramPart (F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2()))))),(F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2())))),(((LifeSpan (F1() +* (Initialized (stop (F2() ';' (AddTo F3(),F4(),(- F5()))))))) + 1) + 1);
A25: dom (F1() | NAT ) =
(dom F1()) /\ NAT
by RELAT_1:90
.=
(({(IC SCMPDS )} \/ SCM-Data-Loc ) \/ NAT ) /\ NAT
by SCMPDS_4:19
.=
NAT
by XBOOLE_1:21
;
Y:
(ProgramPart (Comput (ProgramPart (F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2()))))),(F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2())))),((LifeSpan (F1() +* (Initialized (stop (F2() ';' (AddTo F3(),F4(),(- F5()))))))) + 1))) /. (IC (Comput (ProgramPart (F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2()))))),(F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2())))),((LifeSpan (F1() +* (Initialized (stop (F2() ';' (AddTo F3(),F4(),(- F5()))))))) + 1))) = (Comput (ProgramPart (F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2()))))),(F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2())))),((LifeSpan (F1() +* (Initialized (stop (F2() ';' (AddTo F3(),F4(),(- F5()))))))) + 1)) . (IC (Comput (ProgramPart (F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2()))))),(F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2())))),((LifeSpan (F1() +* (Initialized (stop (F2() ';' (AddTo F3(),F4(),(- F5()))))))) + 1)))
by AMI_1:150;
A26: IC (Comput (ProgramPart (F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2()))))),(F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2())))),1) =
(Comput (ProgramPart (F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2()))))),(F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2())))),1) . (IC SCMPDS )
by AMI_1:def 15
.=
succ (IC (F1() +* (Initialized (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 (F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2()))))),(F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2())))),1)),(Comput (ProgramPart (F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2()))))),(F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2())))),1),(LifeSpan (F1() +* (Initialized (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 (F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2()))))),(F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2())))),((LifeSpan (F1() +* (Initialized (stop (F2() ';' (AddTo F3(),F4(),(- F5()))))))) + 1))),(Comput (ProgramPart (F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2()))))),(F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2())))),((LifeSpan (F1() +* (Initialized (stop (F2() ';' (AddTo F3(),F4(),(- F5()))))))) + 1)) =
(Comput (ProgramPart (Comput (ProgramPart (F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2()))))),(F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2())))),1)),(Comput (ProgramPart (F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2()))))),(F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2())))),1),(LifeSpan (F1() +* (Initialized (stop (F2() ';' (AddTo F3(),F4(),(- F5())))))))) . ((card (F2() ';' (AddTo F3(),F4(),(- F5())))) + 1)
by A17, AMI_1:def 16, Y
.=
(Comput (ProgramPart (F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2()))))),(F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2())))),1) . ((card (F2() ';' (AddTo F3(),F4(),(- F5())))) + 1)
by AMI_1:54
.=
(F1() +* (Initialized (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
;
T:
ProgramPart (F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2())))) = ProgramPart (Comput (ProgramPart (F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2()))))),(F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2())))),((LifeSpan (F1() +* (Initialized (stop (F2() ';' (AddTo F3(),F4(),(- F5()))))))) + 1))
by AMI_1:144;
A29: Comput (ProgramPart (F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2()))))),(F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2())))),(((LifeSpan (F1() +* (Initialized (stop (F2() ';' (AddTo F3(),F4(),(- F5()))))))) + 1) + 1) =
Following (ProgramPart (F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2()))))),(Comput (ProgramPart (F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2()))))),(F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2())))),((LifeSpan (F1() +* (Initialized (stop (F2() ';' (AddTo F3(),F4(),(- F5()))))))) + 1))
by AMI_1:14
.=
Exec (goto (- ((card F2()) + 2))),(Comput (ProgramPart (F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2()))))),(F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2())))),((LifeSpan (F1() +* (Initialized (stop (F2() ';' (AddTo F3(),F4(),(- F5()))))))) + 1))
by A28, AMI_1:def 18, T
;
A30:
DataPart (Comput (ProgramPart (F1() +* (Initialized (stop (F2() ';' (AddTo F3(),F4(),(- F5()))))))),(F1() +* (Initialized (stop (F2() ';' (AddTo F3(),F4(),(- F5())))))),(LifeSpan (F1() +* (Initialized (stop (F2() ';' (AddTo F3(),F4(),(- F5())))))))) = DataPart (Comput (ProgramPart (Comput (ProgramPart (F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2()))))),(F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2())))),1)),(Comput (ProgramPart (F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2()))))),(F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2())))),1),(LifeSpan (F1() +* (Initialized (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 (F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2()))))),(F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2())))),(((LifeSpan (F1() +* (Initialized (stop (F2() ';' (AddTo F3(),F4(),(- F5()))))))) + 1) + 1)) . x = ((IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),F1()) +* (Initialized (stop (for-down F3(),F4(),F5(),F2())))) . x
not
x in dom (Initialized (stop (for-down F3(),F4(),F5(),F2())))
by SCMPDS_4:31;
then A31:
((IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),F1()) +* (Initialized (stop (for-down F3(),F4(),F5(),F2())))) . x = (IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),F1()) . x
by FUNCT_4:12;
A32:
not
x in dom (F1() | NAT )
by A24, SCMPDS_2:53;
(Comput (ProgramPart (Comput (ProgramPart (F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2()))))),(F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2())))),1)),(Comput (ProgramPart (F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2()))))),(F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2())))),1),(LifeSpan (F1() +* (Initialized (stop (F2() ';' (AddTo F3(),F4(),(- F5())))))))) . x =
(Comput (ProgramPart (F1() +* (Initialized (stop (F2() ';' (AddTo F3(),F4(),(- F5()))))))),(F1() +* (Initialized (stop (F2() ';' (AddTo F3(),F4(),(- F5())))))),(LifeSpan (F1() +* (Initialized (stop (F2() ';' (AddTo F3(),F4(),(- F5())))))))) . x
by A30, SCMPDS_4:23
.=
(Result (F1() +* (Initialized (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 (F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2()))))),(F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2())))),(((LifeSpan (F1() +* (Initialized (stop (F2() ';' (AddTo F3(),F4(),(- F5()))))))) + 1) + 1)) . x = ((IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),F1()) +* (Initialized (stop (for-down F3(),F4(),F5(),F2())))) . x
by A17, A29, A31, SCMPDS_2:66;
verum end;
then A33:
DataPart (Comput (ProgramPart (F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2()))))),(F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2())))),(((LifeSpan (F1() +* (Initialized (stop (F2() ';' (AddTo F3(),F4(),(- F5()))))))) + 1) + 1)) = DataPart ((IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),F1()) +* (Initialized (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 (F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2())))) halts_on F1() +* (Initialized (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 ((IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),F1()) +* (Initialized (stop (for-down F3(),F4(),F5(),F2())))) halts_on (IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),F1()) +* (Initialized (stop (for-down F3(),F4(),F5(),F2())))
by SCMPDS_6:def 3;
IC (Comput (ProgramPart (F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2()))))),(F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2())))),(((LifeSpan (F1() +* (Initialized (stop (F2() ';' (AddTo F3(),F4(),(- F5()))))))) + 1) + 1)) =
(Comput (ProgramPart (F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2()))))),(F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2())))),(((LifeSpan (F1() +* (Initialized (stop (F2() ';' (AddTo F3(),F4(),(- F5()))))))) + 1) + 1)) . (IC SCMPDS )
by AMI_1:def 15
.=
ICplusConst (Comput (ProgramPart (F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2()))))),(F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2())))),((LifeSpan (F1() +* (Initialized (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 ((IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),F1()) +* (Initialized (stop (for-down F3(),F4(),F5(),F2())))) = IC (Comput (ProgramPart (F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2()))))),(F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2())))),((LifeSpan (F1() +* (Initialized (stop (F2() ';' (AddTo F3(),F4(),(- F5()))))))) + 2))
by SCMPDS_6:21;
A41: (IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),F1()) | NAT =
((Result (F1() +* (Initialized (stop (F2() ';' (AddTo F3(),F4(),(- F5()))))))) +* (F1() | NAT )) | NAT
by SCMPDS_4:def 8
.=
F1() | NAT
by A25, FUNCT_4:24
;
((IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),F1()) +* (Initialized (stop (for-down F3(),F4(),F5(),F2())))) | NAT =
(((Result (F1() +* (Initialized (stop (F2() ';' (AddTo F3(),F4(),(- F5()))))))) +* (F1() | NAT )) +* (Initialized (stop (for-down F3(),F4(),F5(),F2())))) | NAT
by SCMPDS_4:def 8
.=
(((Result (F1() +* (Initialized (stop (F2() ';' (AddTo F3(),F4(),(- F5()))))))) +* (F1() | NAT )) | NAT ) +* ((Initialized (stop (for-down F3(),F4(),F5(),F2()))) | NAT )
by FUNCT_4:75
.=
(F1() | NAT ) +* ((Initialized (stop (for-down F3(),F4(),F5(),F2()))) | NAT )
by A25, FUNCT_4:24
.=
(F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2())))) | NAT
by FUNCT_4:75
.=
(Comput (ProgramPart (F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2()))))),(F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2())))),((LifeSpan (F1() +* (Initialized (stop (F2() ';' (AddTo F3(),F4(),(- F5()))))))) + 2)) | NAT
by SCMPDS_7:6
;
then A42:
Comput (ProgramPart (F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2()))))),(F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2())))),((LifeSpan (F1() +* (Initialized (stop (F2() ';' (AddTo F3(),F4(),(- F5()))))))) + 2) = (IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),F1()) +* (Initialized (stop (for-down F3(),F4(),F5(),F2())))
by A33, A40, SCMPDS_7:7;
then
CurInstr (ProgramPart (Comput (ProgramPart (F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2()))))),(F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2())))),((LifeSpan (F1() +* (Initialized (stop (F2() ';' (AddTo F3(),F4(),(- F5()))))))) + 2))),(Comput (ProgramPart (F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2()))))),(F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2())))),((LifeSpan (F1() +* (Initialized (stop (F2() ';' (AddTo F3(),F4(),(- F5()))))))) + 2)) = F3(),F4() <=0_goto ((card F2()) + 3)
by A10, SCMPDS_6:22;
then
LifeSpan (F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2())))) > (LifeSpan (F1() +* (Initialized (stop (F2() ';' (AddTo F3(),F4(),(- F5()))))))) + 2
by A36, SCMPDS_6:2, SCMPDS_6:30;
then consider nn being Nat such that
A43:
LifeSpan (F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2())))) = ((LifeSpan (F1() +* (Initialized (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 (F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2())))) = ProgramPart ((IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),F1()) +* (Initialized (stop (for-down F3(),F4(),F5(),F2()))))
by A42, AMI_1:144;
then
Comput (ProgramPart (F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2()))))),(F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2())))),(((LifeSpan (F1() +* (Initialized (stop (F2() ';' (AddTo F3(),F4(),(- F5()))))))) + 2) + (LifeSpan ((IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),F1()) +* (Initialized (stop (for-down F3(),F4(),F5(),F2())))))) = Comput (ProgramPart ((IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),F1()) +* (Initialized (stop (for-down F3(),F4(),F5(),F2()))))),((IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),F1()) +* (Initialized (stop (for-down F3(),F4(),F5(),F2())))),(LifeSpan ((IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),F1()) +* (Initialized (stop (for-down F3(),F4(),F5(),F2())))))
by A42, AMI_1:51;
then
CurInstr (ProgramPart (Comput (ProgramPart (F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2()))))),(F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2())))),(((LifeSpan (F1() +* (Initialized (stop (F2() ';' (AddTo F3(),F4(),(- F5()))))))) + 2) + (LifeSpan ((IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),F1()) +* (Initialized (stop (for-down F3(),F4(),F5(),F2())))))))),(Comput (ProgramPart (F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2()))))),(F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2())))),(((LifeSpan (F1() +* (Initialized (stop (F2() ';' (AddTo F3(),F4(),(- F5()))))))) + 2) + (LifeSpan ((IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),F1()) +* (Initialized (stop (for-down F3(),F4(),F5(),F2()))))))) = halt SCMPDS
by A39, AMI_1:def 46;
then
((LifeSpan (F1() +* (Initialized (stop (F2() ';' (AddTo F3(),F4(),(- F5()))))))) + 2) + (LifeSpan ((IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),F1()) +* (Initialized (stop (for-down F3(),F4(),F5(),F2()))))) >= LifeSpan (F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2()))))
by A36, AMI_1:def 46;
then A44:
LifeSpan ((IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),F1()) +* (Initialized (stop (for-down F3(),F4(),F5(),F2())))) >= nn
by A43, XREAL_1:8;
A45:
Comput (ProgramPart (F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2()))))),(F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2())))),(LifeSpan (F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2()))))) = Comput (ProgramPart ((IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),F1()) +* (Initialized (stop (for-down F3(),F4(),F5(),F2()))))),((IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),F1()) +* (Initialized (stop (for-down F3(),F4(),F5(),F2())))),nn
by A42, A43, AMI_1:51, T;
then
CurInstr (ProgramPart (Comput (ProgramPart ((IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),F1()) +* (Initialized (stop (for-down F3(),F4(),F5(),F2()))))),((IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),F1()) +* (Initialized (stop (for-down F3(),F4(),F5(),F2())))),nn)),(Comput (ProgramPart ((IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),F1()) +* (Initialized (stop (for-down F3(),F4(),F5(),F2()))))),((IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),F1()) +* (Initialized (stop (for-down F3(),F4(),F5(),F2())))),nn) = halt SCMPDS
by A36, AMI_1:def 46;
then
nn >= LifeSpan ((IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),F1()) +* (Initialized (stop (for-down F3(),F4(),F5(),F2()))))
by A39, AMI_1:def 46;
then
nn = LifeSpan ((IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),F1()) +* (Initialized (stop (for-down F3(),F4(),F5(),F2()))))
by A44, XXREAL_0:1;
then
Result (F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2())))) = Comput (ProgramPart ((IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),F1()) +* (Initialized (stop (for-down F3(),F4(),F5(),F2()))))),((IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),F1()) +* (Initialized (stop (for-down F3(),F4(),F5(),F2())))),(LifeSpan ((IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),F1()) +* (Initialized (stop (for-down F3(),F4(),F5(),F2())))))
by A36, A45, AMI_1:122;
hence IExec (for-down F3(),F4(),F5(),F2()),F1() =
(Comput (ProgramPart ((IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),F1()) +* (Initialized (stop (for-down F3(),F4(),F5(),F2()))))),((IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),F1()) +* (Initialized (stop (for-down F3(),F4(),F5(),F2())))),(LifeSpan ((IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),F1()) +* (Initialized (stop (for-down F3(),F4(),F5(),F2())))))) +* (F1() | NAT )
by SCMPDS_4:def 8
.=
(Result ((IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),F1()) +* (Initialized (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