let s be State of SCMPDS ; for I being halt-free shiftable Program of SCMPDS
for a being Int_position
for i being Integer
for X being set st card I > 0 & ( for t being State of SCMPDS st ( for x being Int_position st x in X holds
t . x = s . x ) & t . a = s . a & t . (DataLoc (s . a),i) < 0 holds
( (IExec I,t) . a = t . a & (IExec I,t) . (DataLoc (s . a),i) > t . (DataLoc (s . a),i) & I is_closed_on t & I is_halting_on t & ( for x being Int_position st x in X holds
(IExec I,t) . x = t . x ) ) ) holds
( while<0 a,i,I is_closed_on s & while<0 a,i,I is_halting_on s )
let I be halt-free shiftable Program of SCMPDS ; for a being Int_position
for i being Integer
for X being set st card I > 0 & ( for t being State of SCMPDS st ( for x being Int_position st x in X holds
t . x = s . x ) & t . a = s . a & t . (DataLoc (s . a),i) < 0 holds
( (IExec I,t) . a = t . a & (IExec I,t) . (DataLoc (s . a),i) > t . (DataLoc (s . a),i) & I is_closed_on t & I is_halting_on t & ( for x being Int_position st x in X holds
(IExec I,t) . x = t . x ) ) ) holds
( while<0 a,i,I is_closed_on s & while<0 a,i,I is_halting_on s )
let a be Int_position ; for i being Integer
for X being set st card I > 0 & ( for t being State of SCMPDS st ( for x being Int_position st x in X holds
t . x = s . x ) & t . a = s . a & t . (DataLoc (s . a),i) < 0 holds
( (IExec I,t) . a = t . a & (IExec I,t) . (DataLoc (s . a),i) > t . (DataLoc (s . a),i) & I is_closed_on t & I is_halting_on t & ( for x being Int_position st x in X holds
(IExec I,t) . x = t . x ) ) ) holds
( while<0 a,i,I is_closed_on s & while<0 a,i,I is_halting_on s )
let i be Integer; for X being set st card I > 0 & ( for t being State of SCMPDS st ( for x being Int_position st x in X holds
t . x = s . x ) & t . a = s . a & t . (DataLoc (s . a),i) < 0 holds
( (IExec I,t) . a = t . a & (IExec I,t) . (DataLoc (s . a),i) > t . (DataLoc (s . a),i) & I is_closed_on t & I is_halting_on t & ( for x being Int_position st x in X holds
(IExec I,t) . x = t . x ) ) ) holds
( while<0 a,i,I is_closed_on s & while<0 a,i,I is_halting_on s )
let X be set ; ( card I > 0 & ( for t being State of SCMPDS st ( for x being Int_position st x in X holds
t . x = s . x ) & t . a = s . a & t . (DataLoc (s . a),i) < 0 holds
( (IExec I,t) . a = t . a & (IExec I,t) . (DataLoc (s . a),i) > t . (DataLoc (s . a),i) & I is_closed_on t & I is_halting_on t & ( for x being Int_position st x in X holds
(IExec I,t) . x = t . x ) ) ) implies ( while<0 a,i,I is_closed_on s & while<0 a,i,I is_halting_on s ) )
set b = DataLoc (s . a),i;
set WHL = while<0 a,i,I;
set pWHL = stop (while<0 a,i,I);
set pI = stop I;
set i1 = a,i >=0_goto ((card I) + 2);
set i2 = goto (- ((card I) + 1));
assume A1:
card I > 0
; ( ex t being State of SCMPDS st
( ( for x being Int_position st x in X holds
t . x = s . x ) & t . a = s . a & t . (DataLoc (s . a),i) < 0 & not ( (IExec I,t) . a = t . a & (IExec I,t) . (DataLoc (s . a),i) > t . (DataLoc (s . a),i) & I is_closed_on t & I is_halting_on t & ( for x being Int_position st x in X holds
(IExec I,t) . x = t . x ) ) ) or ( while<0 a,i,I is_closed_on s & while<0 a,i,I is_halting_on s ) )
defpred S1[ Element of NAT ] means for t being State of SCMPDS st - (t . (DataLoc (s . a),i)) <= $1 & ( for x being Int_position st x in X holds
t . x = s . x ) & t . a = s . a holds
( while<0 a,i,I is_closed_on t & while<0 a,i,I is_halting_on t );
assume A2:
for t being State of SCMPDS st ( for x being Int_position st x in X holds
t . x = s . x ) & t . a = s . a & t . (DataLoc (s . a),i) < 0 holds
( (IExec I,t) . a = t . a & (IExec I,t) . (DataLoc (s . a),i) > t . (DataLoc (s . a),i) & I is_closed_on t & I is_halting_on t & ( for x being Int_position st x in X holds
(IExec I,t) . x = t . x ) )
; ( while<0 a,i,I is_closed_on s & while<0 a,i,I is_halting_on s )
A3:
for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be
Element of
NAT ;
( S1[k] implies S1[k + 1] )
assume A4:
S1[
k]
;
S1[k + 1]
now let t be
State of
SCMPDS ;
( - (t . (DataLoc (s . a),i)) <= k + 1 & ( for x being Int_position st x in X holds
t . x = s . x ) & t . a = s . a implies ( while<0 a,i,I is_closed_on b1 & while<0 a,i,I is_halting_on b1 ) )assume A5:
- (t . (DataLoc (s . a),i)) <= k + 1
;
( ( for x being Int_position st x in X holds
t . x = s . x ) & t . a = s . a implies ( while<0 a,i,I is_closed_on b1 & while<0 a,i,I is_halting_on b1 ) )assume A6:
for
x being
Int_position st
x in X holds
t . x = s . x
;
( t . a = s . a implies ( while<0 a,i,I is_closed_on b1 & while<0 a,i,I is_halting_on b1 ) )assume A7:
t . a = s . a
;
( while<0 a,i,I is_closed_on b1 & while<0 a,i,I is_halting_on b1 )per cases
( t . (DataLoc (s . a),i) >= 0 or t . (DataLoc (s . a),i) < 0 )
;
suppose A8:
t . (DataLoc (s . a),i) < 0
;
( while<0 a,i,I is_closed_on b1 & while<0 a,i,I is_halting_on b1 )A9:
dom (ProgramPart t) = NAT
by COMPOS_1:34;
A10:
not
a in dom (t | NAT )
by A9, SCMPDS_2:53;
A11:
not
DataLoc (s . a),
i in dom (t | NAT )
by A9, SCMPDS_2:53;
A12:
(IExec I,t) . (DataLoc (s . a),i) > t . (DataLoc (s . a),i)
by A2, A6, A7, A8;
A13:
0 in dom (stop (while<0 a,i,I))
by SCMPDS_4:75;
A14:
(IExec I,t) . a = t . a
by A2, A6, A7, A8;
A15:
not
DataLoc (s . a),
i in dom (Initialize (stop (while<0 a,i,I)))
by SCMPDS_4:31;
A16:
while<0 a,
i,
I = (a,i >=0_goto ((card I) + 2)) ';' (I ';' (goto (- ((card I) + 1))))
by SCMPDS_4:51;
set t2 =
(Initialize t) +* (stop I);
set t3 =
(Initialize t) +* (stop (while<0 a,i,I));
set t4 =
Comput (ProgramPart ((Initialize t) +* (stop (while<0 a,i,I)))),
((Initialize t) +* (stop (while<0 a,i,I))),1;
I5:
(Initialize t) +* (stop I) = t +* (Initialize (stop I))
by SCMPDS_4:5;
I6:
(Initialize t) +* (stop (while<0 a,i,I)) = t +* (Initialize (stop (while<0 a,i,I)))
by SCMPDS_4:5;
A17:
Initialize (stop I) c= (Initialize t) +* (stop I)
by I5, FUNCT_4:26;
A18:
Comput (ProgramPart ((Initialize t) +* (stop (while<0 a,i,I)))),
((Initialize t) +* (stop (while<0 a,i,I))),
(0 + 1) =
Following (ProgramPart ((Initialize t) +* (stop (while<0 a,i,I)))),
(Comput (ProgramPart ((Initialize t) +* (stop (while<0 a,i,I)))),((Initialize t) +* (stop (while<0 a,i,I))),0 )
by AMI_1:14
.=
Following (ProgramPart ((Initialize t) +* (stop (while<0 a,i,I)))),
((Initialize t) +* (stop (while<0 a,i,I)))
by AMI_1:13
.=
Exec (a,i >=0_goto ((card I) + 2)),
((Initialize t) +* (stop (while<0 a,i,I)))
by A16, I6, SCMPDS_6:22
;
A19:
DataPart ((Initialize t) +* (stop I)) = DataPart ((Initialize t) +* (stop (while<0 a,i,I)))
by FUNCT_7:134, SCMPDS_4:24;
now let a be
Int_position ;
((Initialize t) +* (stop I)) . a = (Comput (ProgramPart ((Initialize t) +* (stop (while<0 a,i,I)))),((Initialize t) +* (stop (while<0 a,i,I))),1) . athus ((Initialize t) +* (stop I)) . a =
((Initialize t) +* (stop (while<0 a,i,I))) . a
by A19, SCMPDS_4:23
.=
(Comput (ProgramPart ((Initialize t) +* (stop (while<0 a,i,I)))),((Initialize t) +* (stop (while<0 a,i,I))),1) . a
by A18, SCMPDS_2:69
;
verum end; then A20:
DataPart ((Initialize t) +* (stop I)) = DataPart (Comput (ProgramPart ((Initialize t) +* (stop (while<0 a,i,I)))),((Initialize t) +* (stop (while<0 a,i,I))),1)
by SCMPDS_4:23;
(
while<0 a,
i,
I c= Initialize (stop (while<0 a,i,I)) &
Initialize (stop (while<0 a,i,I)) c= (Initialize t) +* (stop (while<0 a,i,I)) )
by I6, FUNCT_4:26, SCMPDS_6:17;
then A21:
while<0 a,
i,
I c= (Initialize t) +* (stop (while<0 a,i,I))
by XBOOLE_1:1;
Shift I,1
c= while<0 a,
i,
I
by Lm2;
then
Shift I,1
c= (Initialize t) +* (stop (while<0 a,i,I))
by A21, XBOOLE_1:1;
then A22:
Shift I,1
c= Comput (ProgramPart ((Initialize t) +* (stop (while<0 a,i,I)))),
((Initialize t) +* (stop (while<0 a,i,I))),1
by AMI_1:81;
set m2 =
LifeSpan (ProgramPart ((Initialize t) +* (stop I))),
((Initialize t) +* (stop I));
set t5 =
Comput (ProgramPart (Comput (ProgramPart ((Initialize t) +* (stop (while<0 a,i,I)))),((Initialize t) +* (stop (while<0 a,i,I))),1)),
(Comput (ProgramPart ((Initialize t) +* (stop (while<0 a,i,I)))),((Initialize t) +* (stop (while<0 a,i,I))),1),
(LifeSpan (ProgramPart ((Initialize t) +* (stop I))),((Initialize t) +* (stop I)));
set l1 =
(card I) + 1;
A23:
IC ((Initialize t) +* (stop (while<0 a,i,I))) = 0
by SCMPDS_6:21;
set m3 =
(LifeSpan (ProgramPart ((Initialize t) +* (stop I))),((Initialize t) +* (stop I))) + 1;
set t6 =
Comput (ProgramPart ((Initialize t) +* (stop (while<0 a,i,I)))),
((Initialize t) +* (stop (while<0 a,i,I))),
((LifeSpan (ProgramPart ((Initialize t) +* (stop I))),((Initialize t) +* (stop I))) + 1);
set t7 =
Comput (ProgramPart ((Initialize t) +* (stop (while<0 a,i,I)))),
((Initialize t) +* (stop (while<0 a,i,I))),
(((LifeSpan (ProgramPart ((Initialize t) +* (stop I))),((Initialize t) +* (stop I))) + 1) + 1);
(card I) + 1
< (card I) + 2
by XREAL_1:8;
then A24:
(card I) + 1
in dom (while<0 a,i,I)
by Th7;
A25:
IExec I,
t = (Result (ProgramPart ((Initialize t) +* (stop I))),((Initialize t) +* (stop I))) +* (t | NAT )
by SCMPDS_4:def 8;
A26:
I is_closed_on t
by A2, A6, A7, A8;
then A27:
I is_closed_on (Initialize t) +* (stop I)
by SCMPDS_6:38;
I is_halting_on t
by A2, A6, A7, A8;
then A28:
ProgramPart ((Initialize t) +* (stop I)) halts_on (Initialize t) +* (stop I)
by SCMPDS_6:def 3;
I7:
(Initialize ((Initialize t) +* (stop I))) +* (stop I) = ((Initialize t) +* (stop I)) +* (Initialize (stop I))
by SCMPDS_4:5;
(Initialize t) +* (stop I) = (Initialize ((Initialize t) +* (stop I))) +* (stop I)
by A17, I7, FUNCT_4:79;
then
ProgramPart ((Initialize ((Initialize t) +* (stop I))) +* (stop I)) halts_on (Initialize ((Initialize t) +* (stop I))) +* (stop I)
by A28;
then A29:
I is_halting_on (Initialize t) +* (stop I)
by SCMPDS_6:def 3;
not
a in dom (Initialize (stop (while<0 a,i,I)))
by SCMPDS_4:31;
then ((Initialize t) +* (stop (while<0 a,i,I))) . (DataLoc (((Initialize t) +* (stop (while<0 a,i,I))) . a),i) =
((Initialize t) +* (stop (while<0 a,i,I))) . (DataLoc (s . a),i)
by A7, I6, FUNCT_4:12
.=
t . (DataLoc (s . a),i)
by A15, I6, FUNCT_4:12
;
then A30:
IC (Comput (ProgramPart ((Initialize t) +* (stop (while<0 a,i,I)))),((Initialize t) +* (stop (while<0 a,i,I))),1) =
succ (IC ((Initialize t) +* (stop (while<0 a,i,I))))
by A8, A18, SCMPDS_2:69
.=
0 + 1
by A23
;
then A31:
IC (Comput (ProgramPart (Comput (ProgramPart ((Initialize t) +* (stop (while<0 a,i,I)))),((Initialize t) +* (stop (while<0 a,i,I))),1)),(Comput (ProgramPart ((Initialize t) +* (stop (while<0 a,i,I)))),((Initialize t) +* (stop (while<0 a,i,I))),1),(LifeSpan (ProgramPart ((Initialize t) +* (stop I))),((Initialize t) +* (stop I)))) = (card I) + 1
by A1, A17, A29, A27, A20, A22, SCMPDS_7:36;
Y:
(ProgramPart (Comput (ProgramPart ((Initialize t) +* (stop (while<0 a,i,I)))),((Initialize t) +* (stop (while<0 a,i,I))),((LifeSpan (ProgramPart ((Initialize t) +* (stop I))),((Initialize t) +* (stop I))) + 1))) /. (IC (Comput (ProgramPart ((Initialize t) +* (stop (while<0 a,i,I)))),((Initialize t) +* (stop (while<0 a,i,I))),((LifeSpan (ProgramPart ((Initialize t) +* (stop I))),((Initialize t) +* (stop I))) + 1))) = (Comput (ProgramPart ((Initialize t) +* (stop (while<0 a,i,I)))),((Initialize t) +* (stop (while<0 a,i,I))),((LifeSpan (ProgramPart ((Initialize t) +* (stop I))),((Initialize t) +* (stop I))) + 1)) . (IC (Comput (ProgramPart ((Initialize t) +* (stop (while<0 a,i,I)))),((Initialize t) +* (stop (while<0 a,i,I))),((LifeSpan (ProgramPart ((Initialize t) +* (stop I))),((Initialize t) +* (stop I))) + 1)))
by COMPOS_1:38;
ProgramPart ((Initialize t) +* (stop (while<0 a,i,I))) = ProgramPart (Comput (ProgramPart ((Initialize t) +* (stop (while<0 a,i,I)))),((Initialize t) +* (stop (while<0 a,i,I))),1)
by AMI_1:123;
then A32:
Comput (ProgramPart ((Initialize t) +* (stop (while<0 a,i,I)))),
((Initialize t) +* (stop (while<0 a,i,I))),
((LifeSpan (ProgramPart ((Initialize t) +* (stop I))),((Initialize t) +* (stop I))) + 1) = Comput (ProgramPart (Comput (ProgramPart ((Initialize t) +* (stop (while<0 a,i,I)))),((Initialize t) +* (stop (while<0 a,i,I))),1)),
(Comput (ProgramPart ((Initialize t) +* (stop (while<0 a,i,I)))),((Initialize t) +* (stop (while<0 a,i,I))),1),
(LifeSpan (ProgramPart ((Initialize t) +* (stop I))),((Initialize t) +* (stop I)))
by AMI_1:51;
then A33:
CurInstr (ProgramPart (Comput (ProgramPart ((Initialize t) +* (stop (while<0 a,i,I)))),((Initialize t) +* (stop (while<0 a,i,I))),((LifeSpan (ProgramPart ((Initialize t) +* (stop I))),((Initialize t) +* (stop I))) + 1))),
(Comput (ProgramPart ((Initialize t) +* (stop (while<0 a,i,I)))),((Initialize t) +* (stop (while<0 a,i,I))),((LifeSpan (ProgramPart ((Initialize t) +* (stop I))),((Initialize t) +* (stop I))) + 1)) =
(Comput (ProgramPart (Comput (ProgramPart ((Initialize t) +* (stop (while<0 a,i,I)))),((Initialize t) +* (stop (while<0 a,i,I))),1)),(Comput (ProgramPart ((Initialize t) +* (stop (while<0 a,i,I)))),((Initialize t) +* (stop (while<0 a,i,I))),1),(LifeSpan (ProgramPart ((Initialize t) +* (stop I))),((Initialize t) +* (stop I)))) . ((card I) + 1)
by A1, A17, A29, A27, A30, A20, A22, Y, SCMPDS_7:36
.=
(Comput (ProgramPart ((Initialize t) +* (stop (while<0 a,i,I)))),((Initialize t) +* (stop (while<0 a,i,I))),1) . ((card I) + 1)
by AMI_1:54
.=
((Initialize t) +* (stop (while<0 a,i,I))) . ((card I) + 1)
by AMI_1:54
.=
(while<0 a,i,I) . ((card I) + 1)
by A24, A21, GRFUNC_1:8
.=
goto (- ((card I) + 1))
by Th8
;
A34:
DataPart (Comput (ProgramPart ((Initialize t) +* (stop I))),((Initialize t) +* (stop I)),(LifeSpan (ProgramPart ((Initialize t) +* (stop I))),((Initialize t) +* (stop I)))) = DataPart (Comput (ProgramPart (Comput (ProgramPart ((Initialize t) +* (stop (while<0 a,i,I)))),((Initialize t) +* (stop (while<0 a,i,I))),1)),(Comput (ProgramPart ((Initialize t) +* (stop (while<0 a,i,I)))),((Initialize t) +* (stop (while<0 a,i,I))),1),(LifeSpan (ProgramPart ((Initialize t) +* (stop I))),((Initialize t) +* (stop I))))
by A1, A17, A29, A27, A30, A20, A22, SCMPDS_7:36;
then A35:
(Comput (ProgramPart (Comput (ProgramPart ((Initialize t) +* (stop (while<0 a,i,I)))),((Initialize t) +* (stop (while<0 a,i,I))),1)),(Comput (ProgramPart ((Initialize t) +* (stop (while<0 a,i,I)))),((Initialize t) +* (stop (while<0 a,i,I))),1),(LifeSpan (ProgramPart ((Initialize t) +* (stop I))),((Initialize t) +* (stop I)))) . a =
(Comput (ProgramPart ((Initialize t) +* (stop I))),((Initialize t) +* (stop I)),(LifeSpan (ProgramPart ((Initialize t) +* (stop I))),((Initialize t) +* (stop I)))) . a
by SCMPDS_4:23
.=
(Result (ProgramPart ((Initialize t) +* (stop I))),((Initialize t) +* (stop I))) . a
by A28, AMI_1:122
.=
s . a
by A7, A14, A25, A10, FUNCT_4:12
;
T:
ProgramPart ((Initialize t) +* (stop (while<0 a,i,I))) = ProgramPart (Comput (ProgramPart ((Initialize t) +* (stop (while<0 a,i,I)))),((Initialize t) +* (stop (while<0 a,i,I))),((LifeSpan (ProgramPart ((Initialize t) +* (stop I))),((Initialize t) +* (stop I))) + 1))
by AMI_1:123;
A36:
Comput (ProgramPart ((Initialize t) +* (stop (while<0 a,i,I)))),
((Initialize t) +* (stop (while<0 a,i,I))),
(((LifeSpan (ProgramPart ((Initialize t) +* (stop I))),((Initialize t) +* (stop I))) + 1) + 1) =
Following (ProgramPart ((Initialize t) +* (stop (while<0 a,i,I)))),
(Comput (ProgramPart ((Initialize t) +* (stop (while<0 a,i,I)))),((Initialize t) +* (stop (while<0 a,i,I))),((LifeSpan (ProgramPart ((Initialize t) +* (stop I))),((Initialize t) +* (stop I))) + 1))
by AMI_1:14
.=
Exec (goto (- ((card I) + 1))),
(Comput (ProgramPart ((Initialize t) +* (stop (while<0 a,i,I)))),((Initialize t) +* (stop (while<0 a,i,I))),((LifeSpan (ProgramPart ((Initialize t) +* (stop I))),((Initialize t) +* (stop I))) + 1))
by A33, T
;
then IC (Comput (ProgramPart ((Initialize t) +* (stop (while<0 a,i,I)))),((Initialize t) +* (stop (while<0 a,i,I))),(((LifeSpan (ProgramPart ((Initialize t) +* (stop I))),((Initialize t) +* (stop I))) + 1) + 1)) =
ICplusConst (Comput (ProgramPart ((Initialize t) +* (stop (while<0 a,i,I)))),((Initialize t) +* (stop (while<0 a,i,I))),((LifeSpan (ProgramPart ((Initialize t) +* (stop I))),((Initialize t) +* (stop I))) + 1)),
(0 - ((card I) + 1))
by SCMPDS_2:66
.=
0
by A31, A32, SCMPDS_7:1
;
then A37:
(Initialize (Comput (ProgramPart ((Initialize t) +* (stop (while<0 a,i,I)))),((Initialize t) +* (stop (while<0 a,i,I))),(((LifeSpan (ProgramPart ((Initialize t) +* (stop I))),((Initialize t) +* (stop I))) + 1) + 1))) +* (stop (while<0 a,i,I)) = Comput (ProgramPart ((Initialize t) +* (stop (while<0 a,i,I)))),
((Initialize t) +* (stop (while<0 a,i,I))),
(((LifeSpan (ProgramPart ((Initialize t) +* (stop I))),((Initialize t) +* (stop I))) + 1) + 1)
by SCMPDS_7:37;
A38:
now let x be
Int_position ;
( x in X implies (Comput (ProgramPart ((Initialize t) +* (stop (while<0 a,i,I)))),((Initialize t) +* (stop (while<0 a,i,I))),(((LifeSpan (ProgramPart ((Initialize t) +* (stop I))),((Initialize t) +* (stop I))) + 1) + 1)) . x = s . x )assume A39:
x in X
;
(Comput (ProgramPart ((Initialize t) +* (stop (while<0 a,i,I)))),((Initialize t) +* (stop (while<0 a,i,I))),(((LifeSpan (ProgramPart ((Initialize t) +* (stop I))),((Initialize t) +* (stop I))) + 1) + 1)) . x = s . xA40:
not
x in dom (t | NAT )
by A9, SCMPDS_2:53;
(Comput (ProgramPart (Comput (ProgramPart ((Initialize t) +* (stop (while<0 a,i,I)))),((Initialize t) +* (stop (while<0 a,i,I))),1)),(Comput (ProgramPart ((Initialize t) +* (stop (while<0 a,i,I)))),((Initialize t) +* (stop (while<0 a,i,I))),1),(LifeSpan (ProgramPart ((Initialize t) +* (stop I))),((Initialize t) +* (stop I)))) . x =
(Comput (ProgramPart ((Initialize t) +* (stop I))),((Initialize t) +* (stop I)),(LifeSpan (ProgramPart ((Initialize t) +* (stop I))),((Initialize t) +* (stop I)))) . x
by A34, SCMPDS_4:23
.=
(Result (ProgramPart ((Initialize t) +* (stop I))),((Initialize t) +* (stop I))) . x
by A28, AMI_1:122
.=
(IExec I,t) . x
by A25, A40, FUNCT_4:12
.=
t . x
by A2, A6, A7, A8, A39
.=
s . x
by A6, A39
;
hence
(Comput (ProgramPart ((Initialize t) +* (stop (while<0 a,i,I)))),((Initialize t) +* (stop (while<0 a,i,I))),(((LifeSpan (ProgramPart ((Initialize t) +* (stop I))),((Initialize t) +* (stop I))) + 1) + 1)) . x = s . x
by A32, A36, SCMPDS_2:66;
verum end; (Comput (ProgramPart (Comput (ProgramPart ((Initialize t) +* (stop (while<0 a,i,I)))),((Initialize t) +* (stop (while<0 a,i,I))),1)),(Comput (ProgramPart ((Initialize t) +* (stop (while<0 a,i,I)))),((Initialize t) +* (stop (while<0 a,i,I))),1),(LifeSpan (ProgramPart ((Initialize t) +* (stop I))),((Initialize t) +* (stop I)))) . (DataLoc (s . a),i) =
(Comput (ProgramPart ((Initialize t) +* (stop I))),((Initialize t) +* (stop I)),(LifeSpan (ProgramPart ((Initialize t) +* (stop I))),((Initialize t) +* (stop I)))) . (DataLoc (s . a),i)
by A34, SCMPDS_4:23
.=
(Result (ProgramPart ((Initialize t) +* (stop I))),((Initialize t) +* (stop I))) . (DataLoc (s . a),i)
by A28, AMI_1:122
.=
(IExec I,t) . (DataLoc (s . a),i)
by A25, A11, FUNCT_4:12
;
then A41:
(Comput (ProgramPart ((Initialize t) +* (stop (while<0 a,i,I)))),((Initialize t) +* (stop (while<0 a,i,I))),(((LifeSpan (ProgramPart ((Initialize t) +* (stop I))),((Initialize t) +* (stop I))) + 1) + 1)) . (DataLoc (s . a),i) = (IExec I,t) . (DataLoc (s . a),i)
by A32, A36, SCMPDS_2:66;
A42:
now
- ((Comput (ProgramPart ((Initialize t) +* (stop (while<0 a,i,I)))),((Initialize t) +* (stop (while<0 a,i,I))),(((LifeSpan (ProgramPart ((Initialize t) +* (stop I))),((Initialize t) +* (stop I))) + 1) + 1)) . (DataLoc (s . a),i)) < - (t . (DataLoc (s . a),i))
by A12, A41, XREAL_1:26;
then A43:
- ((Comput (ProgramPart ((Initialize t) +* (stop (while<0 a,i,I)))),((Initialize t) +* (stop (while<0 a,i,I))),(((LifeSpan (ProgramPart ((Initialize t) +* (stop I))),((Initialize t) +* (stop I))) + 1) + 1)) . (DataLoc (s . a),i)) < k + 1
by A5, XXREAL_0:2;
assume
- ((Comput (ProgramPart ((Initialize t) +* (stop (while<0 a,i,I)))),((Initialize t) +* (stop (while<0 a,i,I))),(((LifeSpan (ProgramPart ((Initialize t) +* (stop I))),((Initialize t) +* (stop I))) + 1) + 1)) . (DataLoc (s . a),i)) > k
;
contradictionhence
contradiction
by A43, INT_1:20;
verum end; T1:
ProgramPart (Comput (ProgramPart ((Initialize t) +* (stop (while<0 a,i,I)))),((Initialize t) +* (stop (while<0 a,i,I))),1) = ProgramPart ((Initialize t) +* (stop (while<0 a,i,I)))
by AMI_1:123;
A44:
(Comput (ProgramPart ((Initialize t) +* (stop (while<0 a,i,I)))),((Initialize t) +* (stop (while<0 a,i,I))),(((LifeSpan (ProgramPart ((Initialize t) +* (stop I))),((Initialize t) +* (stop I))) + 1) + 1)) . a =
(Comput (ProgramPart ((Initialize t) +* (stop (while<0 a,i,I)))),((Initialize t) +* (stop (while<0 a,i,I))),((LifeSpan (ProgramPart ((Initialize t) +* (stop I))),((Initialize t) +* (stop I))) + 1)) . a
by A36, SCMPDS_2:66
.=
s . a
by A35, T1, AMI_1:51
;
then A45:
while<0 a,
i,
I is_closed_on Comput (ProgramPart ((Initialize t) +* (stop (while<0 a,i,I)))),
((Initialize t) +* (stop (while<0 a,i,I))),
(((LifeSpan (ProgramPart ((Initialize t) +* (stop I))),((Initialize t) +* (stop I))) + 1) + 1)
by A4, A38, A42;
now let k be
Element of
NAT ;
IC (Comput (ProgramPart ((Initialize t) +* (stop (while<0 a,i,I)))),((Initialize t) +* (stop (while<0 a,i,I))),b1) in dom (stop (while<0 a,i,I))per cases
( k < ((LifeSpan (ProgramPart ((Initialize t) +* (stop I))),((Initialize t) +* (stop I))) + 1) + 1 or k >= ((LifeSpan (ProgramPart ((Initialize t) +* (stop I))),((Initialize t) +* (stop I))) + 1) + 1 )
;
suppose
k < ((LifeSpan (ProgramPart ((Initialize t) +* (stop I))),((Initialize t) +* (stop I))) + 1) + 1
;
IC (Comput (ProgramPart ((Initialize t) +* (stop (while<0 a,i,I)))),((Initialize t) +* (stop (while<0 a,i,I))),b1) in dom (stop (while<0 a,i,I))then A46:
k <= (LifeSpan (ProgramPart ((Initialize t) +* (stop I))),((Initialize t) +* (stop I))) + 1
by INT_1:20;
hereby verum
per cases
( k <= LifeSpan (ProgramPart ((Initialize t) +* (stop I))),((Initialize t) +* (stop I)) or k = (LifeSpan (ProgramPart ((Initialize t) +* (stop I))),((Initialize t) +* (stop I))) + 1 )
by A46, NAT_1:8;
suppose A47:
k <= LifeSpan (ProgramPart ((Initialize t) +* (stop I))),
((Initialize t) +* (stop I))
;
IC (Comput (ProgramPart ((Initialize t) +* (stop (while<0 a,i,I)))),((Initialize t) +* (stop (while<0 a,i,I))),k) in dom (stop (while<0 a,i,I))hereby verum
per cases
( k = 0 or k <> 0 )
;
suppose
k = 0
;
IC (Comput (ProgramPart ((Initialize t) +* (stop (while<0 a,i,I)))),((Initialize t) +* (stop (while<0 a,i,I))),k) in dom (stop (while<0 a,i,I))hence
IC (Comput (ProgramPart ((Initialize t) +* (stop (while<0 a,i,I)))),((Initialize t) +* (stop (while<0 a,i,I))),k) in dom (stop (while<0 a,i,I))
by A13, A23, AMI_1:13;
verum end; suppose
k <> 0
;
IC (Comput (ProgramPart ((Initialize t) +* (stop (while<0 a,i,I)))),((Initialize t) +* (stop (while<0 a,i,I))),k) in dom (stop (while<0 a,i,I))then consider kn being
Nat such that A48:
k = kn + 1
by NAT_1:6;
reconsider kn =
kn as
Element of
NAT by ORDINAL1:def 13;
reconsider lm =
IC (Comput (ProgramPart ((Initialize t) +* (stop I))),((Initialize t) +* (stop I)),kn) as
Element of
NAT ;
t:
ProgramPart ((Initialize t) +* (stop (while<0 a,i,I))) = ProgramPart (Comput (ProgramPart ((Initialize t) +* (stop (while<0 a,i,I)))),((Initialize t) +* (stop (while<0 a,i,I))),1)
by AMI_1:123;
kn < k
by A48, XREAL_1:31;
then
kn < LifeSpan (ProgramPart ((Initialize t) +* (stop I))),
((Initialize t) +* (stop I))
by A47, XXREAL_0:2;
then
(IC (Comput (ProgramPart ((Initialize t) +* (stop I))),((Initialize t) +* (stop I)),kn)) + 1
= IC (Comput (ProgramPart (Comput (ProgramPart ((Initialize t) +* (stop (while<0 a,i,I)))),((Initialize t) +* (stop (while<0 a,i,I))),1)),(Comput (ProgramPart ((Initialize t) +* (stop (while<0 a,i,I)))),((Initialize t) +* (stop (while<0 a,i,I))),1),kn)
by A1, A17, A29, A27, A30, A20, A22, SCMPDS_7:34;
then A49:
IC (Comput (ProgramPart ((Initialize t) +* (stop (while<0 a,i,I)))),((Initialize t) +* (stop (while<0 a,i,I))),k) = lm + 1
by A48, t, AMI_1:51;
IC (Comput (ProgramPart ((Initialize t) +* (stop I))),((Initialize t) +* (stop I)),kn) in dom (stop I)
by A26, SCMPDS_6:def 2;
then
lm < card (stop I)
by AFINSQ_1:70;
then
lm < (card I) + 1
by SCMPDS_5:7;
then A50:
lm + 1
<= (card I) + 1
by INT_1:20;
(card I) + 1
< (card I) + 3
by XREAL_1:8;
then
lm + 1
< (card I) + 3
by A50, XXREAL_0:2;
then
lm + 1
< card (stop (while<0 a,i,I))
by Lm1;
hence
IC (Comput (ProgramPart ((Initialize t) +* (stop (while<0 a,i,I)))),((Initialize t) +* (stop (while<0 a,i,I))),k) in dom (stop (while<0 a,i,I))
by A49, AFINSQ_1:70;
verum end; suppose A51:
k = (LifeSpan (ProgramPart ((Initialize t) +* (stop I))),((Initialize t) +* (stop I))) + 1
;
IC (Comput (ProgramPart ((Initialize t) +* (stop (while<0 a,i,I)))),((Initialize t) +* (stop (while<0 a,i,I))),k) in dom (stop (while<0 a,i,I))
(card I) + 1
in dom (stop (while<0 a,i,I))
by A24, SCMPDS_6:18;
hence
IC (Comput (ProgramPart ((Initialize t) +* (stop (while<0 a,i,I)))),((Initialize t) +* (stop (while<0 a,i,I))),k) in dom (stop (while<0 a,i,I))
by A1, A17, A29, A27, A30, A20, A22, A32, A51, SCMPDS_7:36;
verum end; end; suppose
k >= ((LifeSpan (ProgramPart ((Initialize t) +* (stop I))),((Initialize t) +* (stop I))) + 1) + 1
;
IC (Comput (ProgramPart ((Initialize t) +* (stop (while<0 a,i,I)))),((Initialize t) +* (stop (while<0 a,i,I))),b1) in dom (stop (while<0 a,i,I))then consider nn being
Nat such that A52:
k = (((LifeSpan (ProgramPart ((Initialize t) +* (stop I))),((Initialize t) +* (stop I))) + 1) + 1) + nn
by NAT_1:10;
reconsider nn =
nn as
Element of
NAT by ORDINAL1:def 13;
ProgramPart ((Initialize t) +* (stop (while<0 a,i,I))) = ProgramPart (Comput (ProgramPart ((Initialize t) +* (stop (while<0 a,i,I)))),((Initialize t) +* (stop (while<0 a,i,I))),(((LifeSpan (ProgramPart ((Initialize t) +* (stop I))),((Initialize t) +* (stop I))) + 1) + 1))
by AMI_1:123;
then
Comput (ProgramPart ((Initialize t) +* (stop (while<0 a,i,I)))),
((Initialize t) +* (stop (while<0 a,i,I))),
k = Comput (ProgramPart ((Initialize (Comput (ProgramPart ((Initialize t) +* (stop (while<0 a,i,I)))),((Initialize t) +* (stop (while<0 a,i,I))),(((LifeSpan (ProgramPart ((Initialize t) +* (stop I))),((Initialize t) +* (stop I))) + 1) + 1))) +* (stop (while<0 a,i,I)))),
((Initialize (Comput (ProgramPart ((Initialize t) +* (stop (while<0 a,i,I)))),((Initialize t) +* (stop (while<0 a,i,I))),(((LifeSpan (ProgramPart ((Initialize t) +* (stop I))),((Initialize t) +* (stop I))) + 1) + 1))) +* (stop (while<0 a,i,I))),
nn
by A37, A52, AMI_1:51;
hence
IC (Comput (ProgramPart ((Initialize t) +* (stop (while<0 a,i,I)))),((Initialize t) +* (stop (while<0 a,i,I))),k) in dom (stop (while<0 a,i,I))
by A45, SCMPDS_6:def 2;
verum end; end; hence
while<0 a,
i,
I is_closed_on t
by SCMPDS_6:def 2;
while<0 a,i,I is_halting_on t
while<0 a,
i,
I is_halting_on Comput (ProgramPart ((Initialize t) +* (stop (while<0 a,i,I)))),
((Initialize t) +* (stop (while<0 a,i,I))),
(((LifeSpan (ProgramPart ((Initialize t) +* (stop I))),((Initialize t) +* (stop I))) + 1) + 1)
by A4, A44, A38, A42;
then
ProgramPart (Comput (ProgramPart ((Initialize t) +* (stop (while<0 a,i,I)))),((Initialize t) +* (stop (while<0 a,i,I))),(((LifeSpan (ProgramPart ((Initialize t) +* (stop I))),((Initialize t) +* (stop I))) + 1) + 1)) halts_on Comput (ProgramPart ((Initialize t) +* (stop (while<0 a,i,I)))),
((Initialize t) +* (stop (while<0 a,i,I))),
(((LifeSpan (ProgramPart ((Initialize t) +* (stop I))),((Initialize t) +* (stop I))) + 1) + 1)
by A37, SCMPDS_6:def 3;
then
ProgramPart ((Initialize t) +* (stop (while<0 a,i,I))) halts_on Comput (ProgramPart ((Initialize t) +* (stop (while<0 a,i,I)))),
((Initialize t) +* (stop (while<0 a,i,I))),
(((LifeSpan (ProgramPart ((Initialize t) +* (stop I))),((Initialize t) +* (stop I))) + 1) + 1)
by AMI_1:123;
then
ProgramPart ((Initialize t) +* (stop (while<0 a,i,I))) halts_on (Initialize t) +* (stop (while<0 a,i,I))
by AMI_1:93;
hence
while<0 a,
i,
I is_halting_on t
by SCMPDS_6:def 3;
verum end; end;
hence
S1[
k + 1]
;
verum
end;
A53:
S1[ 0 ]
proof
let t be
State of
SCMPDS ;
( - (t . (DataLoc (s . a),i)) <= 0 & ( for x being Int_position st x in X holds
t . x = s . x ) & t . a = s . a implies ( while<0 a,i,I is_closed_on t & while<0 a,i,I is_halting_on t ) )
assume
- (t . (DataLoc (s . a),i)) <= 0
;
( ex x being Int_position st
( x in X & not t . x = s . x ) or not t . a = s . a or ( while<0 a,i,I is_closed_on t & while<0 a,i,I is_halting_on t ) )
then
- (t . (DataLoc (s . a),i)) <= - 0
;
then A54:
t . (DataLoc (s . a),i) >= 0
by XREAL_1:26;
assume
for
x being
Int_position st
x in X holds
t . x = s . x
;
( not t . a = s . a or ( while<0 a,i,I is_closed_on t & while<0 a,i,I is_halting_on t ) )
assume
t . a = s . a
;
( while<0 a,i,I is_closed_on t & while<0 a,i,I is_halting_on t )
hence
(
while<0 a,
i,
I is_closed_on t &
while<0 a,
i,
I is_halting_on t )
by A54, Th9;
verum
end;
A55:
for k being Element of NAT holds S1[k]
from NAT_1:sch 1(A53, A3);