set i1 = (F4(),F5()) <=0_goto ((card F3()) + 3);
set J = F3() ';' (AddTo (F4(),F5(),(- F6())));
set i3 = goto (- ((card F3()) + 2));
set b = DataLoc ((F1() . F4()),F5());
set FOR = for-down (F4(),F5(),F6(),F3());
set pFOR = stop (for-down (F4(),F5(),F6(),F3()));
set pJ = stop (F3() ';' (AddTo (F4(),F5(),(- F6()))));
defpred S1[ Nat] means for t being 0 -started State of SCMPDS
for Q being Instruction-Sequence of SCMPDS st t . (DataLoc ((F1() . F4()),F5())) <= $1 & P1[t] & t . F4() = F1() . F4() holds
( for-down (F4(),F5(),F6(),F3()) is_closed_on t,Q & for-down (F4(),F5(),F6(),F3()) is_halting_on t,Q );
A4:
for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be
Nat;
( S1[k] implies S1[k + 1] )
assume A5:
S1[
k]
;
S1[k + 1]
now for t being 0 -started State of SCMPDS
for Q being Instruction-Sequence of SCMPDS st t . (DataLoc ((F1() . F4()),F5())) <= k + 1 & P1[t] & t . F4() = F1() . F4() holds
( for-down (F4(),F5(),F6(),F3()) is_closed_on t,Q & for-down (F4(),F5(),F6(),F3()) is_halting_on t,Q )let t be
0 -started State of
SCMPDS;
for Q being Instruction-Sequence of SCMPDS st t . (DataLoc ((F1() . F4()),F5())) <= k + 1 & P1[t] & t . F4() = F1() . F4() holds
( for-down (F4(),F5(),F6(),F3()) is_closed_on b2,b3 & for-down (F4(),F5(),F6(),F3()) is_halting_on b2,b3 )let Q be
Instruction-Sequence of
SCMPDS;
( t . (DataLoc ((F1() . F4()),F5())) <= k + 1 & P1[t] & t . F4() = F1() . F4() implies ( for-down (F4(),F5(),F6(),F3()) is_closed_on b1,b2 & for-down (F4(),F5(),F6(),F3()) is_halting_on b1,b2 ) )A6:
Initialize t = t
by MEMSTR_0:44;
assume A7:
t . (DataLoc ((F1() . F4()),F5())) <= k + 1
;
( P1[t] & t . F4() = F1() . F4() implies ( for-down (F4(),F5(),F6(),F3()) is_closed_on b1,b2 & for-down (F4(),F5(),F6(),F3()) is_halting_on b1,b2 ) )assume A8:
P1[
t]
;
( t . F4() = F1() . F4() implies ( for-down (F4(),F5(),F6(),F3()) is_closed_on b1,b2 & for-down (F4(),F5(),F6(),F3()) is_halting_on b1,b2 ) )assume A9:
t . F4()
= F1()
. F4()
;
( for-down (F4(),F5(),F6(),F3()) is_closed_on b1,b2 & for-down (F4(),F5(),F6(),F3()) is_halting_on b1,b2 )per cases
( t . (DataLoc ((F1() . F4()),F5())) <= 0 or t . (DataLoc ((F1() . F4()),F5())) > 0 )
;
suppose A10:
t . (DataLoc ((F1() . F4()),F5())) > 0
;
( for-down (F4(),F5(),F6(),F3()) is_closed_on b1,b2 & for-down (F4(),F5(),F6(),F3()) is_halting_on b1,b2 )A11:
0 in dom (stop (for-down (F4(),F5(),F6(),F3())))
by COMPOS_1:36;
- (- F6()) > 0
by A1;
then
- F6()
< 0
;
then
- F6()
<= - 1
by INT_1:8;
then A12:
(- F6()) + (t . (DataLoc ((F1() . F4()),F5()))) <= (- 1) + (t . (DataLoc ((F1() . F4()),F5())))
by XREAL_1:6;
(t . (DataLoc ((F1() . F4()),F5()))) - 1
<= k
by A7, XREAL_1:20;
then A13:
(- F6()) + (t . (DataLoc ((F1() . F4()),F5()))) <= k
by A12, XXREAL_0:2;
set Q2 =
Q +* (stop (F3() ';' (AddTo (F4(),F5(),(- F6())))));
set Q3 =
Q +* (stop (for-down (F4(),F5(),F6(),F3())));
set t4 =
Comput (
(Q +* (stop (for-down (F4(),F5(),F6(),F3())))),
t,1);
set Q4 =
Q +* (stop (for-down (F4(),F5(),F6(),F3())));
set Jt =
IExec (
(F3() ';' (AddTo (F4(),F5(),(- F6())))),
Q,
t);
A14:
stop (F3() ';' (AddTo (F4(),F5(),(- F6())))) c= Q +* (stop (F3() ';' (AddTo (F4(),F5(),(- F6())))))
by FUNCT_4:25;
A15:
for-down (
F4(),
F5(),
F6(),
F3())
= ((F4(),F5()) <=0_goto ((card F3()) + 3)) ';' ((F3() ';' (AddTo (F4(),F5(),(- F6())))) ';' (goto (- ((card F3()) + 2))))
by Lm2;
A16:
Comput (
(Q +* (stop (for-down (F4(),F5(),F6(),F3())))),
t,
(0 + 1)) =
Following (
(Q +* (stop (for-down (F4(),F5(),F6(),F3())))),
(Comput ((Q +* (stop (for-down (F4(),F5(),F6(),F3())))),t,0)))
by EXTPRO_1:3
.=
Following (
(Q +* (stop (for-down (F4(),F5(),F6(),F3())))),
t)
by EXTPRO_1:2
.=
Exec (
((F4(),F5()) <=0_goto ((card F3()) + 3)),
t)
by A15, A6, SCMPDS_6:11
;
for
x being
Int_position holds
t . x = (Comput ((Q +* (stop (for-down (F4(),F5(),F6(),F3())))),t,1)) . x
by A16, SCMPDS_2:56;
then A17:
DataPart t = DataPart (Comput ((Q +* (stop (for-down (F4(),F5(),F6(),F3())))),t,1))
by SCMPDS_4:8;
A18:
(IExec ((F3() ';' (AddTo (F4(),F5(),(- F6())))),Q,t)) . (DataLoc ((F1() . F4()),F5())) = (t . (DataLoc ((F1() . F4()),F5()))) - F6()
by A3, A8, A9, A10;
A19:
(IExec ((F3() ';' (AddTo (F4(),F5(),(- F6())))),Q,t)) . F4()
= t . F4()
by A3, A8, A9, A10;
set m2 =
LifeSpan (
(Q +* (stop (F3() ';' (AddTo (F4(),F5(),(- F6())))))),
t);
set t5 =
Comput (
(Q +* (stop (for-down (F4(),F5(),F6(),F3())))),
(Comput ((Q +* (stop (for-down (F4(),F5(),F6(),F3())))),t,1)),
(LifeSpan ((Q +* (stop (F3() ';' (AddTo (F4(),F5(),(- F6())))))),t)));
set Q5 =
Q +* (stop (for-down (F4(),F5(),F6(),F3())));
set l1 =
(card (F3() ';' (AddTo (F4(),F5(),(- F6()))))) + 1;
A20:
card (F3() ';' (AddTo (F4(),F5(),(- F6())))) = (card F3()) + 1
by SCMP_GCD:4;
A21:
t . (DataLoc ((t . F4()),F5())) = t . (DataLoc ((F1() . F4()),F5()))
by A9;
A22:
IC t = 0
by A6, MEMSTR_0:47;
A23:
(
F3()
is_closed_on t,
Q &
F3()
is_halting_on t,
Q )
by A3, A8, A9, A10;
then A24:
F3()
';' (AddTo (F4(),F5(),(- F6()))) is_closed_on t,
Q
by Th5;
then A25:
F3()
';' (AddTo (F4(),F5(),(- F6()))) is_closed_on t,
Q +* (stop (F3() ';' (AddTo (F4(),F5(),(- F6())))))
by A6, SCMPDS_6:24;
(card F3()) + 2
< (card F3()) + 3
by XREAL_1:6;
then A26:
(card (F3() ';' (AddTo (F4(),F5(),(- F6()))))) + 1
in dom (for-down (F4(),F5(),F6(),F3()))
by A20, SCMPDS_7:42;
set m3 =
(LifeSpan ((Q +* (stop (F3() ';' (AddTo (F4(),F5(),(- F6())))))),t)) + 1;
set t6 =
Comput (
(Q +* (stop (for-down (F4(),F5(),F6(),F3())))),
t,
((LifeSpan ((Q +* (stop (F3() ';' (AddTo (F4(),F5(),(- F6())))))),t)) + 1));
set Q6 =
Q +* (stop (for-down (F4(),F5(),F6(),F3())));
A27:
Comput (
(Q +* (stop (for-down (F4(),F5(),F6(),F3())))),
t,
((LifeSpan ((Q +* (stop (F3() ';' (AddTo (F4(),F5(),(- F6())))))),t)) + 1))
= Comput (
(Q +* (stop (for-down (F4(),F5(),F6(),F3())))),
(Comput ((Q +* (stop (for-down (F4(),F5(),F6(),F3())))),t,1)),
(LifeSpan ((Q +* (stop (F3() ';' (AddTo (F4(),F5(),(- F6())))))),t)))
by EXTPRO_1:4;
A28:
F3()
';' (AddTo (F4(),F5(),(- F6()))) is_halting_on t,
Q
by A23, Th5;
then A29:
Q +* (stop (F3() ';' (AddTo (F4(),F5(),(- F6()))))) halts_on t
by A6, SCMPDS_6:def 3;
(Q +* (stop (F3() ';' (AddTo (F4(),F5(),(- F6())))))) +* (stop (F3() ';' (AddTo (F4(),F5(),(- F6()))))) halts_on t
by A28, A6, SCMPDS_6:def 3;
then A30:
F3()
';' (AddTo (F4(),F5(),(- F6()))) is_halting_on t,
Q +* (stop (F3() ';' (AddTo (F4(),F5(),(- F6())))))
by A6, SCMPDS_6:def 3;
set m4 =
((LifeSpan ((Q +* (stop (F3() ';' (AddTo (F4(),F5(),(- F6())))))),t)) + 1) + 1;
set t7 =
Comput (
(Q +* (stop (for-down (F4(),F5(),F6(),F3())))),
t,
(((LifeSpan ((Q +* (stop (F3() ';' (AddTo (F4(),F5(),(- F6())))))),t)) + 1) + 1));
set Q7 =
Q +* (stop (for-down (F4(),F5(),F6(),F3())));
A31:
stop (for-down (F4(),F5(),F6(),F3())) c= Q +* (stop (for-down (F4(),F5(),F6(),F3())))
by FUNCT_4:25;
A32:
for-down (
F4(),
F5(),
F6(),
F3())
c= stop (for-down (F4(),F5(),F6(),F3()))
by AFINSQ_1:74;
then A33:
for-down (
F4(),
F5(),
F6(),
F3())
c= Q +* (stop (for-down (F4(),F5(),F6(),F3())))
by A31, XBOOLE_1:1;
Shift (
(F3() ';' (AddTo (F4(),F5(),(- F6())))),1)
c= for-down (
F4(),
F5(),
F6(),
F3())
by Lm3;
then
Shift (
(F3() ';' (AddTo (F4(),F5(),(- F6())))),1)
c= stop (for-down (F4(),F5(),F6(),F3()))
by A32, XBOOLE_1:1;
then A34:
Shift (
(F3() ';' (AddTo (F4(),F5(),(- F6())))),1)
c= Q +* (stop (for-down (F4(),F5(),F6(),F3())))
by A31, XBOOLE_1:1;
A35:
IC (Comput ((Q +* (stop (for-down (F4(),F5(),F6(),F3())))),t,1)) =
(IC t) + 1
by A10, A16, A21, SCMPDS_2:56
.=
0 + 1
by A22
;
then A36:
DataPart (Comput ((Q +* (stop (F3() ';' (AddTo (F4(),F5(),(- F6())))))),t,(LifeSpan ((Q +* (stop (F3() ';' (AddTo (F4(),F5(),(- F6())))))),t)))) = DataPart (Comput ((Q +* (stop (for-down (F4(),F5(),F6(),F3())))),(Comput ((Q +* (stop (for-down (F4(),F5(),F6(),F3())))),t,1)),(LifeSpan ((Q +* (stop (F3() ';' (AddTo (F4(),F5(),(- F6())))))),t))))
by A14, A30, A25, A17, A34, SCMPDS_7:18;
then A37:
DataPart (Comput ((Q +* (stop (for-down (F4(),F5(),F6(),F3())))),(Comput ((Q +* (stop (for-down (F4(),F5(),F6(),F3())))),t,1)),(LifeSpan ((Q +* (stop (F3() ';' (AddTo (F4(),F5(),(- F6())))))),t)))) =
DataPart (Result ((Q +* (stop (F3() ';' (AddTo (F4(),F5(),(- F6())))))),t))
by A29, EXTPRO_1:23
.=
DataPart (IExec ((F3() ';' (AddTo (F4(),F5(),(- F6())))),Q,t))
by SCMPDS_4:def 5
;
A38:
IC (Comput ((Q +* (stop (for-down (F4(),F5(),F6(),F3())))),(Comput ((Q +* (stop (for-down (F4(),F5(),F6(),F3())))),t,1)),(LifeSpan ((Q +* (stop (F3() ';' (AddTo (F4(),F5(),(- F6())))))),t)))) = (card (F3() ';' (AddTo (F4(),F5(),(- F6()))))) + 1
by A14, A30, A25, A35, A17, A34, SCMPDS_7:18;
then A39:
CurInstr (
(Q +* (stop (for-down (F4(),F5(),F6(),F3())))),
(Comput ((Q +* (stop (for-down (F4(),F5(),F6(),F3())))),t,((LifeSpan ((Q +* (stop (F3() ';' (AddTo (F4(),F5(),(- F6())))))),t)) + 1)))) =
(Q +* (stop (for-down (F4(),F5(),F6(),F3())))) . ((card (F3() ';' (AddTo (F4(),F5(),(- F6()))))) + 1)
by A27, PBOOLE:143
.=
(for-down (F4(),F5(),F6(),F3())) . ((card (F3() ';' (AddTo (F4(),F5(),(- F6()))))) + 1)
by A26, A33, GRFUNC_1:2
.=
goto (- ((card F3()) + 2))
by A20, SCMPDS_7:43
;
A40:
Comput (
(Q +* (stop (for-down (F4(),F5(),F6(),F3())))),
t,
(((LifeSpan ((Q +* (stop (F3() ';' (AddTo (F4(),F5(),(- F6())))))),t)) + 1) + 1)) =
Following (
(Q +* (stop (for-down (F4(),F5(),F6(),F3())))),
(Comput ((Q +* (stop (for-down (F4(),F5(),F6(),F3())))),t,((LifeSpan ((Q +* (stop (F3() ';' (AddTo (F4(),F5(),(- F6())))))),t)) + 1))))
by EXTPRO_1:3
.=
Exec (
(goto (- ((card F3()) + 2))),
(Comput ((Q +* (stop (for-down (F4(),F5(),F6(),F3())))),t,((LifeSpan ((Q +* (stop (F3() ';' (AddTo (F4(),F5(),(- F6())))))),t)) + 1))))
by A39
;
IC (Comput ((Q +* (stop (for-down (F4(),F5(),F6(),F3())))),t,(((LifeSpan ((Q +* (stop (F3() ';' (AddTo (F4(),F5(),(- F6())))))),t)) + 1) + 1))) =
ICplusConst (
(Comput ((Q +* (stop (for-down (F4(),F5(),F6(),F3())))),t,((LifeSpan ((Q +* (stop (F3() ';' (AddTo (F4(),F5(),(- F6())))))),t)) + 1))),
(0 - ((card F3()) + 2)))
by A40, SCMPDS_2:54
.=
0
by A20, A38, A27, SCMPDS_7:1
;
then A41:
Initialize (Comput ((Q +* (stop (for-down (F4(),F5(),F6(),F3())))),t,(((LifeSpan ((Q +* (stop (F3() ';' (AddTo (F4(),F5(),(- F6())))))),t)) + 1) + 1))) = Comput (
(Q +* (stop (for-down (F4(),F5(),F6(),F3())))),
t,
(((LifeSpan ((Q +* (stop (F3() ';' (AddTo (F4(),F5(),(- F6())))))),t)) + 1) + 1))
by MEMSTR_0:46;
InsCode (goto (- ((card F3()) + 2))) = 14
by SCMPDS_2:12;
then
InsCode (goto (- ((card F3()) + 2))) in {0,4,5,6,14}
by ENUMSET1:def 3;
then Comput (
(Q +* (stop (for-down (F4(),F5(),F6(),F3())))),
t,
(((LifeSpan ((Q +* (stop (F3() ';' (AddTo (F4(),F5(),(- F6())))))),t)) + 1) + 1)) =
Initialize (Comput ((Q +* (stop (for-down (F4(),F5(),F6(),F3())))),t,((LifeSpan ((Q +* (stop (F3() ';' (AddTo (F4(),F5(),(- F6())))))),t)) + 1)))
by A40, A41, SCMPDS_8:3
.=
Initialize (IExec ((F3() ';' (AddTo (F4(),F5(),(- F6())))),Q,t))
by A37, A27, MEMSTR_0:80
;
then A42:
P1[
Comput (
(Q +* (stop (for-down (F4(),F5(),F6(),F3())))),
t,
(((LifeSpan ((Q +* (stop (F3() ';' (AddTo (F4(),F5(),(- F6())))))),t)) + 1) + 1))]
by A3, A8, A9, A10;
A43:
(Q +* (stop (for-down (F4(),F5(),F6(),F3())))) +* (stop (for-down (F4(),F5(),F6(),F3()))) = Q +* (stop (for-down (F4(),F5(),F6(),F3())))
;
(Comput ((Q +* (stop (for-down (F4(),F5(),F6(),F3())))),(Comput ((Q +* (stop (for-down (F4(),F5(),F6(),F3())))),t,1)),(LifeSpan ((Q +* (stop (F3() ';' (AddTo (F4(),F5(),(- F6())))))),t)))) . (DataLoc ((F1() . F4()),F5())) =
(Comput ((Q +* (stop (F3() ';' (AddTo (F4(),F5(),(- F6())))))),t,(LifeSpan ((Q +* (stop (F3() ';' (AddTo (F4(),F5(),(- F6())))))),t)))) . (DataLoc ((F1() . F4()),F5()))
by A36, SCMPDS_4:8
.=
(Result ((Q +* (stop (F3() ';' (AddTo (F4(),F5(),(- F6())))))),t)) . (DataLoc ((F1() . F4()),F5()))
by A29, EXTPRO_1:23
.=
(t . (DataLoc ((F1() . F4()),F5()))) - F6()
by A18, SCMPDS_4:def 5
;
then A44:
(Comput ((Q +* (stop (for-down (F4(),F5(),F6(),F3())))),t,(((LifeSpan ((Q +* (stop (F3() ';' (AddTo (F4(),F5(),(- F6())))))),t)) + 1) + 1))) . (DataLoc ((F1() . F4()),F5())) = (- F6()) + (t . (DataLoc ((F1() . F4()),F5())))
by A27, A40, SCMPDS_2:54;
(Comput ((Q +* (stop (for-down (F4(),F5(),F6(),F3())))),(Comput ((Q +* (stop (for-down (F4(),F5(),F6(),F3())))),t,1)),(LifeSpan ((Q +* (stop (F3() ';' (AddTo (F4(),F5(),(- F6())))))),t)))) . F4() =
(Comput ((Q +* (stop (F3() ';' (AddTo (F4(),F5(),(- F6())))))),t,(LifeSpan ((Q +* (stop (F3() ';' (AddTo (F4(),F5(),(- F6())))))),t)))) . F4()
by A36, SCMPDS_4:8
.=
(Result ((Q +* (stop (F3() ';' (AddTo (F4(),F5(),(- F6())))))),t)) . F4()
by A29, EXTPRO_1:23
.=
F1()
. F4()
by A9, A19, SCMPDS_4:def 5
;
then A45:
(Comput ((Q +* (stop (for-down (F4(),F5(),F6(),F3())))),t,(((LifeSpan ((Q +* (stop (F3() ';' (AddTo (F4(),F5(),(- F6())))))),t)) + 1) + 1))) . F4()
= F1()
. F4()
by A27, A40, SCMPDS_2:54;
then A46:
for-down (
F4(),
F5(),
F6(),
F3())
is_closed_on Comput (
(Q +* (stop (for-down (F4(),F5(),F6(),F3())))),
t,
(((LifeSpan ((Q +* (stop (F3() ';' (AddTo (F4(),F5(),(- F6())))))),t)) + 1) + 1)),
Q +* (stop (for-down (F4(),F5(),F6(),F3())))
by A5, A42, A44, A13, A41;
now for k being Nat holds IC (Comput ((Q +* (stop (for-down (F4(),F5(),F6(),F3())))),t,k)) in dom (stop (for-down (F4(),F5(),F6(),F3())))let k be
Nat;
IC (Comput ((Q +* (stop (for-down (F4(),F5(),F6(),F3())))),t,b1)) in dom (stop (for-down (F4(),F5(),F6(),F3())))per cases
( k < ((LifeSpan ((Q +* (stop (F3() ';' (AddTo (F4(),F5(),(- F6())))))),t)) + 1) + 1 or k >= ((LifeSpan ((Q +* (stop (F3() ';' (AddTo (F4(),F5(),(- F6())))))),t)) + 1) + 1 )
;
suppose
k < ((LifeSpan ((Q +* (stop (F3() ';' (AddTo (F4(),F5(),(- F6())))))),t)) + 1) + 1
;
IC (Comput ((Q +* (stop (for-down (F4(),F5(),F6(),F3())))),t,b1)) in dom (stop (for-down (F4(),F5(),F6(),F3())))then A47:
k <= (LifeSpan ((Q +* (stop (F3() ';' (AddTo (F4(),F5(),(- F6())))))),t)) + 1
by INT_1:7;
hereby verum
per cases
( k <= LifeSpan ((Q +* (stop (F3() ';' (AddTo (F4(),F5(),(- F6())))))),t) or k = (LifeSpan ((Q +* (stop (F3() ';' (AddTo (F4(),F5(),(- F6())))))),t)) + 1 )
by A47, NAT_1:8;
suppose A48:
k <= LifeSpan (
(Q +* (stop (F3() ';' (AddTo (F4(),F5(),(- F6())))))),
t)
;
IC (Comput ((Q +* (stop (for-down (F4(),F5(),F6(),F3())))),t,k)) in dom (stop (for-down (F4(),F5(),F6(),F3())))per cases
( k = 0 or k <> 0 )
;
suppose
k = 0
;
IC (Comput ((Q +* (stop (for-down (F4(),F5(),F6(),F3())))),t,k)) in dom (stop (for-down (F4(),F5(),F6(),F3())))hence
IC (Comput ((Q +* (stop (for-down (F4(),F5(),F6(),F3())))),t,k)) in dom (stop (for-down (F4(),F5(),F6(),F3())))
by A11, A22, EXTPRO_1:2;
verum end; suppose
k <> 0
;
IC (Comput ((Q +* (stop (for-down (F4(),F5(),F6(),F3())))),t,k)) in dom (stop (for-down (F4(),F5(),F6(),F3())))then consider kn being
Nat such that A49:
k = kn + 1
by NAT_1:6;
reconsider kn =
kn as
Nat ;
reconsider lm =
IC (Comput ((Q +* (stop (F3() ';' (AddTo (F4(),F5(),(- F6())))))),t,kn)) as
Element of
NAT ;
kn < k
by A49, XREAL_1:29;
then
kn < LifeSpan (
(Q +* (stop (F3() ';' (AddTo (F4(),F5(),(- F6())))))),
t)
by A48, XXREAL_0:2;
then
(IC (Comput ((Q +* (stop (F3() ';' (AddTo (F4(),F5(),(- F6())))))),t,kn))) + 1
= IC (Comput ((Q +* (stop (for-down (F4(),F5(),F6(),F3())))),(Comput ((Q +* (stop (for-down (F4(),F5(),F6(),F3())))),t,1)),kn))
by A14, A30, A25, A35, A17, A34, SCMPDS_7:16;
then A50:
IC (Comput ((Q +* (stop (for-down (F4(),F5(),F6(),F3())))),t,k)) = lm + 1
by A49, EXTPRO_1:4;
IC (Comput ((Q +* (stop (F3() ';' (AddTo (F4(),F5(),(- F6())))))),t,kn)) in dom (stop (F3() ';' (AddTo (F4(),F5(),(- F6())))))
by A24, A6, SCMPDS_6:def 2;
then
lm < card (stop (F3() ';' (AddTo (F4(),F5(),(- F6())))))
by AFINSQ_1:66;
then
lm < (card (F3() ';' (AddTo (F4(),F5(),(- F6()))))) + 1
by COMPOS_1:55;
then A51:
lm + 1
<= (card (F3() ';' (AddTo (F4(),F5(),(- F6()))))) + 1
by INT_1:7;
(card F3()) + 2
< (card F3()) + 4
by XREAL_1:6;
then
lm + 1
< (card F3()) + 4
by A20, A51, XXREAL_0:2;
then
lm + 1
< card (stop (for-down (F4(),F5(),F6(),F3())))
by Lm1;
hence
IC (Comput ((Q +* (stop (for-down (F4(),F5(),F6(),F3())))),t,k)) in dom (stop (for-down (F4(),F5(),F6(),F3())))
by A50, AFINSQ_1:66;
verum end; end; end; suppose A52:
k = (LifeSpan ((Q +* (stop (F3() ';' (AddTo (F4(),F5(),(- F6())))))),t)) + 1
;
IC (Comput ((Q +* (stop (for-down (F4(),F5(),F6(),F3())))),t,k)) in dom (stop (for-down (F4(),F5(),F6(),F3())))
(card (F3() ';' (AddTo (F4(),F5(),(- F6()))))) + 1
in dom (stop (for-down (F4(),F5(),F6(),F3())))
by A26, COMPOS_1:62;
hence
IC (Comput ((Q +* (stop (for-down (F4(),F5(),F6(),F3())))),t,k)) in dom (stop (for-down (F4(),F5(),F6(),F3())))
by A14, A30, A25, A35, A17, A34, A27, A52, SCMPDS_7:18;
verum end; end;
end; end; suppose
k >= ((LifeSpan ((Q +* (stop (F3() ';' (AddTo (F4(),F5(),(- F6())))))),t)) + 1) + 1
;
IC (Comput ((Q +* (stop (for-down (F4(),F5(),F6(),F3())))),t,b1)) in dom (stop (for-down (F4(),F5(),F6(),F3())))then consider nn being
Nat such that A53:
k = (((LifeSpan ((Q +* (stop (F3() ';' (AddTo (F4(),F5(),(- F6())))))),t)) + 1) + 1) + nn
by NAT_1:10;
reconsider nn =
nn as
Nat ;
Comput (
(Q +* (stop (for-down (F4(),F5(),F6(),F3())))),
t,
k) =
Comput (
(Q +* (stop (for-down (F4(),F5(),F6(),F3())))),
(Comput ((Q +* (stop (for-down (F4(),F5(),F6(),F3())))),t,(((LifeSpan ((Q +* (stop (F3() ';' (AddTo (F4(),F5(),(- F6())))))),t)) + 1) + 1))),
nn)
by A53, EXTPRO_1:4
.=
Comput (
((Q +* (stop (for-down (F4(),F5(),F6(),F3())))) +* (stop (for-down (F4(),F5(),F6(),F3())))),
(Comput ((Q +* (stop (for-down (F4(),F5(),F6(),F3())))),t,(((LifeSpan ((Q +* (stop (F3() ';' (AddTo (F4(),F5(),(- F6())))))),t)) + 1) + 1))),
nn)
;
hence
IC (Comput ((Q +* (stop (for-down (F4(),F5(),F6(),F3())))),t,k)) in dom (stop (for-down (F4(),F5(),F6(),F3())))
by A46, A41, SCMPDS_6:def 2;
verum end; end; end; hence
for-down (
F4(),
F5(),
F6(),
F3())
is_closed_on t,
Q
by A6, SCMPDS_6:def 2;
for-down (F4(),F5(),F6(),F3()) is_halting_on t,Q
for-down (
F4(),
F5(),
F6(),
F3())
is_halting_on Comput (
(Q +* (stop (for-down (F4(),F5(),F6(),F3())))),
t,
(((LifeSpan ((Q +* (stop (F3() ';' (AddTo (F4(),F5(),(- F6())))))),t)) + 1) + 1)),
Q +* (stop (for-down (F4(),F5(),F6(),F3())))
by A5, A45, A42, A44, A13, A41;
then
Q +* (stop (for-down (F4(),F5(),F6(),F3()))) halts_on Comput (
(Q +* (stop (for-down (F4(),F5(),F6(),F3())))),
t,
(((LifeSpan ((Q +* (stop (F3() ';' (AddTo (F4(),F5(),(- F6())))))),t)) + 1) + 1))
by A43, A41, SCMPDS_6:def 3;
then
Q +* (stop (for-down (F4(),F5(),F6(),F3()))) halts_on t
by EXTPRO_1:22;
hence
for-down (
F4(),
F5(),
F6(),
F3())
is_halting_on t,
Q
by A6, SCMPDS_6:def 3;
verum end; end; end;
hence
S1[
k + 1]
;
verum
end;
A54:
S1[ 0 ]
by SCMPDS_7:44;
A55:
for k being Nat holds S1[k]
from NAT_1:sch 2(A54, A4);