let s be State of SCMPDS; :: thesis: for I being halt-free shiftable Program of SCMPDS
for a being Int_position
for i being Integer
for X being set
for f being Function of (product the Object-Kind of SCMPDS),NAT st card I > 0 & ( for t being State of SCMPDS st f . (Dstate t) = 0 holds
t . (DataLoc ((s . a),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 & f . (Dstate (IExec (I,t))) < f . (Dstate t) & 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; :: thesis: for a being Int_position
for i being Integer
for X being set
for f being Function of (product the Object-Kind of SCMPDS),NAT st card I > 0 & ( for t being State of SCMPDS st f . (Dstate t) = 0 holds
t . (DataLoc ((s . a),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 & f . (Dstate (IExec (I,t))) < f . (Dstate t) & 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 ; :: thesis: for i being Integer
for X being set
for f being Function of (product the Object-Kind of SCMPDS),NAT st card I > 0 & ( for t being State of SCMPDS st f . (Dstate t) = 0 holds
t . (DataLoc ((s . a),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 & f . (Dstate (IExec (I,t))) < f . (Dstate t) & 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; :: thesis: for X being set
for f being Function of (product the Object-Kind of SCMPDS),NAT st card I > 0 & ( for t being State of SCMPDS st f . (Dstate t) = 0 holds
t . (DataLoc ((s . a),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 & f . (Dstate (IExec (I,t))) < f . (Dstate t) & 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 ; :: thesis: for f being Function of (product the Object-Kind of SCMPDS),NAT st card I > 0 & ( for t being State of SCMPDS st f . (Dstate t) = 0 holds
t . (DataLoc ((s . a),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 & f . (Dstate (IExec (I,t))) < f . (Dstate t) & 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 f be Function of (product the Object-Kind of SCMPDS),NAT; :: thesis: ( card I > 0 & ( for t being State of SCMPDS st f . (Dstate t) = 0 holds
t . (DataLoc ((s . a),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 & f . (Dstate (IExec (I,t))) < f . (Dstate t) & 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 ; :: thesis: ( ex t being State of SCMPDS st
( f . (Dstate t) = 0 & not t . (DataLoc ((s . a),i)) >= 0 ) or 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 & f . (Dstate (IExec (I,t))) < f . (Dstate t) & 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 f . (Dstate t) <= $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 f . (Dstate t) = 0 holds
t . (DataLoc ((s . a),i)) >= 0 ; :: thesis: ( 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 & f . (Dstate (IExec (I,t))) < f . (Dstate t) & 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 ) )
assume A3: 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 & f . (Dstate (IExec (I,t))) < f . (Dstate t) & 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 ) ) ; :: thesis: ( while<0 (a,i,I) is_closed_on s & while<0 (a,i,I) is_halting_on s )
A4: for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be Element of NAT ; :: thesis: ( S1[k] implies S1[k + 1] )
assume A5: S1[k] ; :: thesis: S1[k + 1]
now
let t be State of SCMPDS; :: thesis: ( f . (Dstate t) <= 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: f . (Dstate t) <= k + 1 ; :: thesis: ( ( 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: for x being Int_position st x in X holds
t . x = s . x ; :: thesis: ( t . a = s . a implies ( while<0 (a,i,I) is_closed_on b1 & while<0 (a,i,I) is_halting_on b1 ) )
assume A8: t . a = s . a ; :: thesis: ( 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 t . (DataLoc ((s . a),i)) >= 0 ; :: thesis: ( while<0 (a,i,I) is_closed_on b1 & while<0 (a,i,I) is_halting_on b1 )
hence ( while<0 (a,i,I) is_closed_on t & while<0 (a,i,I) is_halting_on t ) by A8, Th9; :: thesis: verum
end;
suppose A9: t . (DataLoc ((s . a),i)) < 0 ; :: thesis: ( while<0 (a,i,I) is_closed_on b1 & while<0 (a,i,I) is_halting_on b1 )
A10: dom (ProgramPart t) = NAT by COMPOS_1:34;
A11: not a in dom (t | NAT) by A10, SCMPDS_2:53;
A12: (IExec (I,t)) . a = t . a by A3, A7, A8, A9;
A13: 0 in dom (stop (while<0 (a,i,I))) by COMPOS_1:135;
A14: not DataLoc ((s . a),i) in dom (Initialize (stop (while<0 (a,i,I)))) by SCMPDS_4:31;
A15: while<0 (a,i,I) = ((a,i) >=0_goto ((card I) + 2)) ';' (I ';' (goto (- ((card I) + 1)))) by SCMPDS_4:51;
A16: f . (Dstate (IExec (I,t))) < f . (Dstate t) by A3, A7, A8, A9;
A17: dom (ProgramPart t) = NAT by COMPOS_1:34;
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);
I1: (Initialize t) +* (stop I) = t +* (Initialize (stop I)) by COMPOS_1:125;
I2: (Initialize t) +* (stop (while<0 (a,i,I))) = t +* (Initialize (stop (while<0 (a,i,I)))) by COMPOS_1:125;
A18: Initialize (stop I) c= (Initialize t) +* (stop I) by I1, FUNCT_4:26;
A19: 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 EXTPRO_1:4
.= Following ((ProgramPart ((Initialize t) +* (stop (while<0 (a,i,I))))),((Initialize t) +* (stop (while<0 (a,i,I))))) by EXTPRO_1:3
.= Exec (((a,i) >=0_goto ((card I) + 2)),((Initialize t) +* (stop (while<0 (a,i,I))))) by A15, I2, SCMPDS_6:22 ;
A20: DataPart ((Initialize t) +* (stop I)) = DataPart ((Initialize t) +* (stop (while<0 (a,i,I)))) by COMPOS_1:138, FUNCT_7:134;
now
let a be Int_position ; :: thesis: ((Initialize t) +* (stop I)) . a = (Comput ((ProgramPart ((Initialize t) +* (stop (while<0 (a,i,I))))),((Initialize t) +* (stop (while<0 (a,i,I)))),1)) . a
thus ((Initialize t) +* (stop I)) . a = ((Initialize t) +* (stop (while<0 (a,i,I)))) . a by A20, SCMPDS_4:23
.= (Comput ((ProgramPart ((Initialize t) +* (stop (while<0 (a,i,I))))),((Initialize t) +* (stop (while<0 (a,i,I)))),1)) . a by A19, SCMPDS_2:69 ; :: thesis: verum
end;
then A21: 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 I2, FUNCT_4:26, SCMPDS_6:17;
then A22: 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 A22, XBOOLE_1:1;
then A23: 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;
A24: 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 A25: (card I) + 1 in dom (while<0 (a,i,I)) by Th7;
A26: I is_closed_on t by A3, A7, A8, A9;
then A27: I is_closed_on (Initialize t) +* (stop I) by SCMPDS_6:38;
I is_halting_on t by A3, A7, A8, A9;
then A28: ProgramPart ((Initialize t) +* (stop I)) halts_on (Initialize t) +* (stop I) by SCMPDS_6:def 3;
I3: (Initialize ((Initialize t) +* (stop I))) +* (stop I) = ((Initialize t) +* (stop I)) +* (Initialize (stop I)) by COMPOS_1:125;
(Initialize t) +* (stop I) = (Initialize ((Initialize t) +* (stop I))) +* (stop I) by A18, I3, 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 A8, I2, FUNCT_4:12
.= t . (DataLoc ((s . a),i)) by A14, I2, 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 A9, A19, SCMPDS_2:69
.= 0 + 1 by A24 ;
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, A18, A29, A27, A21, A23, 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 EXTPRO_1:5;
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, A18, A29, A27, A30, A21, A23, 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 A25, A22, 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, A18, A29, A27, A30, A21, A23, SCMPDS_7:36;
then A35: 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)))))) = DataPart (Result ((ProgramPart ((Initialize t) +* (stop I))),((Initialize t) +* (stop I)))) by A28, EXTPRO_1:23
.= DataPart ((Result ((ProgramPart ((Initialize t) +* (stop I))),((Initialize t) +* (stop I)))) +* (t | NAT)) by A17, AMI_2:29, FUNCT_4:76, SCMPDS_2:100
.= DataPart (IExec (I,t)) by SCMPDS_4:def 8 ;
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 EXTPRO_1:4
.= 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: IExec (I,t) = (Result ((ProgramPart ((Initialize t) +* (stop I))),((Initialize t) +* (stop I)))) +* (t | NAT) by SCMPDS_4:def 8;
A39: now
let x be Int_position ; :: thesis: ( 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 A40: x in X ; :: thesis: (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
A41: not x in dom (t | NAT) by A10, 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, EXTPRO_1:23
.= (IExec (I,t)) . x by A38, A41, FUNCT_4:12
.= t . x by A3, A7, A8, A9, A40
.= s . x by A7, A40 ;
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; :: thesis: verum
end;
InsCode (goto (- ((card I) + 1))) = 0 by SCMPDS_2:21;
then InsCode (goto (- ((card I) + 1))) in {0,4,5,6} by ENUMSET1:def 2;
then A42: Dstate (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))) = Dstate (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 A36, Th3
.= Dstate (IExec (I,t)) by A35, A32, Th2 ;
A43: now
assume A44: f . (Dstate (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)))) > k ; :: thesis: contradiction
f . (Dstate (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)))) < k + 1 by A6, A16, A42, XXREAL_0:2;
hence contradiction by A44, INT_1:20; :: thesis: verum
end;
A45: (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 A34, SCMPDS_4:23
.= (Result ((ProgramPart ((Initialize t) +* (stop I))),((Initialize t) +* (stop I)))) . a by A28, EXTPRO_1:23
.= s . a by A8, A12, A38, A11, FUNCT_4:12 ;
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;
A46: (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 A45, T1, EXTPRO_1:5 ;
then A47: 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 A5, A39, A43;
now
let k be Element of NAT ; :: thesis: 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 ; :: thesis: 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 A48: k <= (LifeSpan ((ProgramPart ((Initialize t) +* (stop I))),((Initialize t) +* (stop I)))) + 1 by INT_1:20;
hereby :: thesis: 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 A48, NAT_1:8;
suppose A49: k <= LifeSpan ((ProgramPart ((Initialize t) +* (stop I))),((Initialize t) +* (stop I))) ; :: thesis: 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 :: thesis: verum
per cases ( k = 0 or k <> 0 ) ;
suppose k = 0 ; :: thesis: 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, A24, EXTPRO_1:3; :: thesis: verum
end;
suppose k <> 0 ; :: thesis: 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
A50: 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 A50, XREAL_1:31;
then kn < LifeSpan ((ProgramPart ((Initialize t) +* (stop I))),((Initialize t) +* (stop I))) by A49, 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, A18, A29, A27, A30, A21, A23, SCMPDS_7:34;
then A51: IC (Comput ((ProgramPart ((Initialize t) +* (stop (while<0 (a,i,I))))),((Initialize t) +* (stop (while<0 (a,i,I)))),k)) = lm + 1 by A50, t, EXTPRO_1:5;
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 A52: 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 A52, 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 A51, AFINSQ_1:70; :: thesis: verum
end;
end;
end;
end;
suppose A53: k = (LifeSpan ((ProgramPart ((Initialize t) +* (stop I))),((Initialize t) +* (stop I)))) + 1 ; :: thesis: 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 A25, 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, A18, A29, A27, A30, A21, A23, A32, A53, SCMPDS_7:36; :: thesis: verum
end;
end;
end;
end;
suppose k >= ((LifeSpan ((ProgramPart ((Initialize t) +* (stop I))),((Initialize t) +* (stop I)))) + 1) + 1 ; :: thesis: 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
A54: 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, A54, EXTPRO_1:5;
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 A47, SCMPDS_6:def 2; :: thesis: verum
end;
end;
end;
hence while<0 (a,i,I) is_closed_on t by SCMPDS_6:def 2; :: thesis: 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 A5, A46, A39, A43;
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 EXTPRO_1:22;
hence while<0 (a,i,I) is_halting_on t by SCMPDS_6:def 3; :: thesis: verum
end;
end;
end;
hence S1[k + 1] ; :: thesis: verum
end;
set n = f . (Dstate s);
A55: S1[ 0 ]
proof
let t be State of SCMPDS; :: thesis: ( f . (Dstate t) <= 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 f . (Dstate t) <= 0 ; :: thesis: ( 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 f . (Dstate t) = 0 ;
then A56: t . (DataLoc ((s . a),i)) >= 0 by A2;
assume for x being Int_position st x in X holds
t . x = s . x ; :: thesis: ( 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 ; :: thesis: ( 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 A56, Th9; :: thesis: verum
end;
for k being Element of NAT holds S1[k] from NAT_1:sch 1(A55, A4);
 then A57: S1[f . (Dstate s)] ;
for x being Int_position st x in X holds
s . x = s . x ;
hence ( while<0 (a,i,I) is_closed_on s & while<0 (a,i,I) is_halting_on s ) by A57; :: thesis: verum