let s, sm be State of ; for I being shiftable No-StopCode Program of
for a being Int_position
for i being Integer
for m being Element of NAT st card I > 0 & I is_closed_on s & I is_halting_on s & s . (DataLoc (s . a),i) > 0 & m = (LifeSpan (s +* (Initialized (stop I)))) + 2 & sm = Computation (s +* (Initialized (stop (while>0 a,i,I)))),m holds
( DataPart sm = DataPart (IExec I,s) & sm +* (Initialized (stop (while>0 a,i,I))) = sm )
let I be shiftable No-StopCode Program of ; for a being Int_position
for i being Integer
for m being Element of NAT st card I > 0 & I is_closed_on s & I is_halting_on s & s . (DataLoc (s . a),i) > 0 & m = (LifeSpan (s +* (Initialized (stop I)))) + 2 & sm = Computation (s +* (Initialized (stop (while>0 a,i,I)))),m holds
( DataPart sm = DataPart (IExec I,s) & sm +* (Initialized (stop (while>0 a,i,I))) = sm )
let a be Int_position ; for i being Integer
for m being Element of NAT st card I > 0 & I is_closed_on s & I is_halting_on s & s . (DataLoc (s . a),i) > 0 & m = (LifeSpan (s +* (Initialized (stop I)))) + 2 & sm = Computation (s +* (Initialized (stop (while>0 a,i,I)))),m holds
( DataPart sm = DataPart (IExec I,s) & sm +* (Initialized (stop (while>0 a,i,I))) = sm )
let i be Integer; for m being Element of NAT st card I > 0 & I is_closed_on s & I is_halting_on s & s . (DataLoc (s . a),i) > 0 & m = (LifeSpan (s +* (Initialized (stop I)))) + 2 & sm = Computation (s +* (Initialized (stop (while>0 a,i,I)))),m holds
( DataPart sm = DataPart (IExec I,s) & sm +* (Initialized (stop (while>0 a,i,I))) = sm )
let m be Element of NAT ; ( card I > 0 & I is_closed_on s & I is_halting_on s & s . (DataLoc (s . a),i) > 0 & m = (LifeSpan (s +* (Initialized (stop I)))) + 2 & sm = Computation (s +* (Initialized (stop (while>0 a,i,I)))),m implies ( DataPart sm = DataPart (IExec I,s) & sm +* (Initialized (stop (while>0 a,i,I))) = sm ) )
set b = DataLoc (s . a),i;
set WH = while>0 a,i,I;
set iWH = Initialized (stop (while>0 a,i,I));
set IsI = Initialized (stop I);
set i1 = a,i <=0_goto ((card I) + 2);
set i2 = goto (- ((card I) + 1));
set s2 = s +* (Initialized (stop I));
set s3 = s +* (Initialized (stop (while>0 a,i,I)));
set s4 = Computation (s +* (Initialized (stop (while>0 a,i,I)))),1;
assume that
A1:
card I > 0
and
A2:
I is_closed_on s
and
A3:
I is_halting_on s
and
A4:
s . (DataLoc (s . a),i) > 0
and
A5:
m = (LifeSpan (s +* (Initialized (stop I)))) + 2
and
A6:
sm = Computation (s +* (Initialized (stop (while>0 a,i,I)))),m
; ( DataPart sm = DataPart (IExec I,s) & sm +* (Initialized (stop (while>0 a,i,I))) = sm )
A7:
Initialized (stop I) c= s +* (Initialized (stop I))
by FUNCT_4:26;
A8:
Initialized (stop (while>0 a,i,I)) c= s +* (Initialized (stop (while>0 a,i,I)))
by FUNCT_4:26;
while>0 a,i,I c= Initialized (stop (while>0 a,i,I))
by SCMPDS_6:17;
then A9:
while>0 a,i,I c= s +* (Initialized (stop (while>0 a,i,I)))
by A8, XBOOLE_1:1;
Shift I,1 c= while>0 a,i,I
by Lm3;
then
Shift I,1 c= s +* (Initialized (stop (while>0 a,i,I)))
by A9, XBOOLE_1:1;
then A10:
Shift I,1 c= Computation (s +* (Initialized (stop (while>0 a,i,I)))),1
by AMI_1:81;
while>0 a,i,I = (a,i <=0_goto ((card I) + 2)) ';' (I ';' (goto (- ((card I) + 1))))
by Lm2;
then A11:
CurInstr (s +* (Initialized (stop (while>0 a,i,I)))) = a,i <=0_goto ((card I) + 2)
by SCMPDS_6:22;
A12: Computation (s +* (Initialized (stop (while>0 a,i,I)))),(0 + 1) =
Following (Computation (s +* (Initialized (stop (while>0 a,i,I)))),0 )
by AMI_1:14
.=
Following (s +* (Initialized (stop (while>0 a,i,I))))
by AMI_1:13
.=
Exec (a,i <=0_goto ((card I) + 2)),(s +* (Initialized (stop (while>0 a,i,I))))
by A11, AMI_1:def 18
;
set m2 = LifeSpan (s +* (Initialized (stop I)));
set s5 = Computation (Computation (s +* (Initialized (stop (while>0 a,i,I)))),1),(LifeSpan (s +* (Initialized (stop I))));
set l1 = inspos ((card I) + 1);
A13:
IC (s +* (Initialized (stop (while>0 a,i,I)))) = inspos 0
by SCMPDS_6:21;
A14: (s +* (Initialized (stop (while>0 a,i,I)))) . (DataLoc ((s +* (Initialized (stop (while>0 a,i,I)))) . a),i) =
(s +* (Initialized (stop (while>0 a,i,I)))) . (DataLoc (s . a),i)
by SCMPDS_5:19
.=
s . (DataLoc (s . a),i)
by SCMPDS_5:19
;
set m3 = (LifeSpan (s +* (Initialized (stop I)))) + 1;
set s6 = Computation (s +* (Initialized (stop (while>0 a,i,I)))),((LifeSpan (s +* (Initialized (stop I)))) + 1);
A15:
Computation (s +* (Initialized (stop (while>0 a,i,I)))),((LifeSpan (s +* (Initialized (stop I)))) + 1) = Computation (Computation (s +* (Initialized (stop (while>0 a,i,I)))),1),(LifeSpan (s +* (Initialized (stop I))))
by AMI_1:51;
set s7 = Computation (s +* (Initialized (stop (while>0 a,i,I)))),(((LifeSpan (s +* (Initialized (stop I)))) + 1) + 1);
(card I) + 1 < (card I) + 2
by XREAL_1:8;
then A16:
inspos ((card I) + 1) in dom (while>0 a,i,I)
by SCMPDS_8:18;
A17:
dom (s | NAT ) = NAT
by SCMPDS_6:1;
A18:
I is_closed_on s +* (Initialized (stop I))
by A2, SCMPDS_6:38;
A19:
DataPart (s +* (Initialized (stop I))) = DataPart (s +* (Initialized (stop (while>0 a,i,I))))
by SCMPDS_4:24, SCMPDS_4:36;
now let x be
Int_position ;
(s +* (Initialized (stop I))) . x = (Computation (s +* (Initialized (stop (while>0 a,i,I)))),1) . xthus (s +* (Initialized (stop I))) . x =
(s +* (Initialized (stop (while>0 a,i,I)))) . x
by A19, SCMPDS_4:23
.=
(Computation (s +* (Initialized (stop (while>0 a,i,I)))),1) . x
by A12, SCMPDS_2:68
;
verum end;
then A20:
DataPart (s +* (Initialized (stop I))) = DataPart (Computation (s +* (Initialized (stop (while>0 a,i,I)))),1)
by SCMPDS_4:23;
A21:
ProgramPart (s +* (Initialized (stop I))) halts_on s +* (Initialized (stop I))
by A3, SCMPDS_6:def 3;
s +* (Initialized (stop I)) = (s +* (Initialized (stop I))) +* (Initialized (stop I))
by A7, FUNCT_4:79;
then
ProgramPart ((s +* (Initialized (stop I))) +* (Initialized (stop I))) halts_on (s +* (Initialized (stop I))) +* (Initialized (stop I))
by A7, FUNCT_4:79, A21;
then A22:
I is_halting_on s +* (Initialized (stop I))
by SCMPDS_6:def 3;
A23: IC (Computation (s +* (Initialized (stop (while>0 a,i,I)))),1) =
(Computation (s +* (Initialized (stop (while>0 a,i,I)))),1) . (IC SCMPDS )
by AMI_1:def 15
.=
Next (inspos 0 )
by A4, A13, A12, A14, SCMPDS_2:68
.=
inspos (0 + 1)
;
then
DataPart (Computation (s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) = DataPart (Computation (Computation (s +* (Initialized (stop (while>0 a,i,I)))),1),(LifeSpan (s +* (Initialized (stop I)))))
by A1, A7, A22, A18, A20, A10, SCMPDS_7:36;
then A24: DataPart (Computation (Computation (s +* (Initialized (stop (while>0 a,i,I)))),1),(LifeSpan (s +* (Initialized (stop I))))) =
DataPart (Result (s +* (Initialized (stop I))))
by A21, AMI_1:122
.=
DataPart ((Result (s +* (Initialized (stop I)))) +* (s | NAT ))
by A17, AMI_2:29, FUNCT_4:76, SCMPDS_2:100
.=
DataPart (IExec I,s)
by SCMPDS_4:def 8
;
A25:
IC (Computation (Computation (s +* (Initialized (stop (while>0 a,i,I)))),1),(LifeSpan (s +* (Initialized (stop I))))) = inspos ((card I) + 1)
by A1, A7, A22, A18, A23, A20, A10, SCMPDS_7:36;
then A26: CurInstr (Computation (s +* (Initialized (stop (while>0 a,i,I)))),((LifeSpan (s +* (Initialized (stop I)))) + 1)) =
(Computation (Computation (s +* (Initialized (stop (while>0 a,i,I)))),1),(LifeSpan (s +* (Initialized (stop I))))) . (inspos ((card I) + 1))
by A15, AMI_1:def 16
.=
(Computation (s +* (Initialized (stop (while>0 a,i,I)))),1) . (inspos ((card I) + 1))
by AMI_1:54
.=
(s +* (Initialized (stop (while>0 a,i,I)))) . (inspos ((card I) + 1))
by AMI_1:54
.=
(while>0 a,i,I) . (inspos ((card I) + 1))
by A16, A9, GRFUNC_1:8
.=
goto (- ((card I) + 1))
by SCMPDS_8:19
;
A27: Computation (s +* (Initialized (stop (while>0 a,i,I)))),(((LifeSpan (s +* (Initialized (stop I)))) + 1) + 1) =
Following (Computation (s +* (Initialized (stop (while>0 a,i,I)))),((LifeSpan (s +* (Initialized (stop I)))) + 1))
by AMI_1:14
.=
Exec (goto (- ((card I) + 1))),(Computation (s +* (Initialized (stop (while>0 a,i,I)))),((LifeSpan (s +* (Initialized (stop I)))) + 1))
by A26, AMI_1:def 18
;
now let x be
Int_position ;
sm . x = (Computation (Computation (s +* (Initialized (stop (while>0 a,i,I)))),1),(LifeSpan (s +* (Initialized (stop I))))) . xthus sm . x =
(Computation (s +* (Initialized (stop (while>0 a,i,I)))),((LifeSpan (s +* (Initialized (stop I)))) + 1)) . x
by A5, A6, A27, SCMPDS_2:66
.=
(Computation (Computation (s +* (Initialized (stop (while>0 a,i,I)))),1),(LifeSpan (s +* (Initialized (stop I))))) . x
by AMI_1:51
;
verum end;
hence
DataPart sm = DataPart (IExec I,s)
by A24, SCMPDS_4:23; sm +* (Initialized (stop (while>0 a,i,I))) = sm
IC (Computation (s +* (Initialized (stop (while>0 a,i,I)))),(((LifeSpan (s +* (Initialized (stop I)))) + 1) + 1)) =
(Computation (s +* (Initialized (stop (while>0 a,i,I)))),(((LifeSpan (s +* (Initialized (stop I)))) + 1) + 1)) . (IC SCMPDS )
by AMI_1:def 15
.=
ICplusConst (Computation (s +* (Initialized (stop (while>0 a,i,I)))),((LifeSpan (s +* (Initialized (stop I)))) + 1)),(0 - ((card I) + 1))
by A27, SCMPDS_2:66
.=
inspos 0
by A25, A15, SCMPDS_7:1
;
hence
sm +* (Initialized (stop (while>0 a,i,I))) = sm
by A5, A6, SCMPDS_7:37; verum