let P be the Instructions of SCMPDS -valued ManySortedSet of NAT ; :: thesis: for s being 0 -started State of SCMPDS
for I being halt-free parahalting Program of SCMPDS
for J being parahalting shiftable Program of SCMPDS
for k being Element of NAT st stop (I ';' J) c= P holds
NPP (IncIC ((Comput (((P +* (stop I)) +* (stop J)),(Initialize (Result ((P +* (stop I)),s))),k)),(card I))) = NPP (Comput ((P +* (stop (I ';' J))),s,((LifeSpan ((P +* (stop I)),s)) + k)))
let s be 0 -started State of SCMPDS; :: thesis: for I being halt-free parahalting Program of SCMPDS
for J being parahalting shiftable Program of SCMPDS
for k being Element of NAT st stop (I ';' J) c= P holds
NPP (IncIC ((Comput (((P +* (stop I)) +* (stop J)),(Initialize (Result ((P +* (stop I)),s))),k)),(card I))) = NPP (Comput ((P +* (stop (I ';' J))),s,((LifeSpan ((P +* (stop I)),s)) + k)))
let I be halt-free parahalting Program of SCMPDS; :: thesis: for J being parahalting shiftable Program of SCMPDS
for k being Element of NAT st stop (I ';' J) c= P holds
NPP (IncIC ((Comput (((P +* (stop I)) +* (stop J)),(Initialize (Result ((P +* (stop I)),s))),k)),(card I))) = NPP (Comput ((P +* (stop (I ';' J))),s,((LifeSpan ((P +* (stop I)),s)) + k)))
let J be parahalting shiftable Program of SCMPDS; :: thesis: for k being Element of NAT st stop (I ';' J) c= P holds
NPP (IncIC ((Comput (((P +* (stop I)) +* (stop J)),(Initialize (Result ((P +* (stop I)),s))),k)),(card I))) = NPP (Comput ((P +* (stop (I ';' J))),s,((LifeSpan ((P +* (stop I)),s)) + k)))
let k be Element of NAT ; :: thesis: ( stop (I ';' J) c= P implies NPP (IncIC ((Comput (((P +* (stop I)) +* (stop J)),(Initialize (Result ((P +* (stop I)),s))),k)),(card I))) = NPP (Comput ((P +* (stop (I ';' J))),s,((LifeSpan ((P +* (stop I)),s)) + k))) )
set sIsI = s;
set PIPI = P +* (stop I);
set RI = Result ((P +* (stop I)),s);
set pJ = stop J;
set RIJ = Initialize (Result ((P +* (stop I)),s));
set PRIJ = (P +* (stop I)) +* (stop J);
set pIJ = stop (I ';' J);
set sIsIJ = s;
set PIPIJ = P +* (stop (I ';' J));
A2: P +* (stop I) halts_on s by FUNCT_4:26, SCMPDS_4:def 10;
set s2 = Comput ((P +* (stop (I ';' J))),s,((LifeSpan ((P +* (stop I)),s)) + 0));
set s1 = (Initialize (Result ((P +* (stop I)),s))) +* (Start-At (((IC (Initialize (Result ((P +* (stop I)),s)))) + (card I)),SCMPDS));
set m1 = LifeSpan ((P +* (stop I)),s);
A3: I c= stop (I ';' J) by Th15;
assume A4: stop (I ';' J) c= P ; :: thesis: NPP (IncIC ((Comput (((P +* (stop I)) +* (stop J)),(Initialize (Result ((P +* (stop I)),s))),k)),(card I))) = NPP (Comput ((P +* (stop (I ';' J))),s,((LifeSpan ((P +* (stop I)),s)) + k)))
B4: P +* (stop (I ';' J)) = P by A4, FUNCT_4:104;
A6: now
thus IC ((Initialize (Result ((P +* (stop I)),s))) +* (Start-At (((IC (Initialize (Result ((P +* (stop I)),s)))) + (card I)),SCMPDS))) = (IC (Initialize (Result ((P +* (stop I)),s)))) + (card I) by FUNCT_4:121
.= 0 + (card I) by FUNCT_4:121
.= IC (Comput ((P +* (stop (I ';' J))),s,((LifeSpan ((P +* (stop I)),s)) + 0))) by A4, A3, Th30, XBOOLE_1:1, B4 ; :: thesis: for a being Int_position holds ((Initialize (Result ((P +* (stop I)),s))) +* (Start-At (((IC (Initialize (Result ((P +* (stop I)),s)))) + (card I)),SCMPDS))) . a = (Comput ((P +* (stop (I ';' J))),s,((LifeSpan ((P +* (stop I)),s)) + 0))) . a
hereby :: thesis: verum
let a be Int_position ; :: thesis: ((Initialize (Result ((P +* (stop I)),s))) +* (Start-At (((IC (Initialize (Result ((P +* (stop I)),s)))) + (card I)),SCMPDS))) . a = (Comput ((P +* (stop (I ';' J))),s,((LifeSpan ((P +* (stop I)),s)) + 0))) . a
XX: NPP (Comput ((P +* (stop I)),s,(LifeSpan ((P +* (stop I)),s)))) = NPP (Comput ((P +* (stop (I ';' J))),s,(LifeSpan ((P +* (stop I)),s)))) by Th34;
YY: not a in dom (Start-At (0,SCMPDS)) by SCMPDS_4:59;
not a in dom (Start-At (((IC (Initialize (Result ((P +* (stop I)),s)))) + (card I)),SCMPDS)) by SCMPDS_4:59;
hence ((Initialize (Result ((P +* (stop I)),s))) +* (Start-At (((IC (Initialize (Result ((P +* (stop I)),s)))) + (card I)),SCMPDS))) . a = (Initialize (Result ((P +* (stop I)),s))) . a by FUNCT_4:12
.= (Result ((P +* (stop I)),s)) . a by FUNCT_4:12, YY
.= (Comput ((P +* (stop I)),s,(LifeSpan ((P +* (stop I)),s)))) . a by A2, EXTPRO_1:23
.= (Comput ((P +* (stop (I ';' J))),s,((LifeSpan ((P +* (stop I)),s)) + 0))) . a by XX, SCMPDS_4:13 ;
:: thesis: verum
end;
end;
defpred S1[ Element of NAT ] means NPP (IncIC ((Comput (((P +* (stop I)) +* (stop J)),(Initialize (Result ((P +* (stop I)),s))),$1)),(card I))) = NPP (Comput ((P +* (stop (I ';' J))),s,((LifeSpan ((P +* (stop I)),s)) + $1)));
A8: stop (I ';' J) c= P +* (stop (I ';' J)) by FUNCT_4:26;
A9: 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] )
set k1 = k + 1;
set CRk = Comput (((P +* (stop I)) +* (stop J)),(Initialize (Result ((P +* (stop I)),s))),k);
set PCRk = (P +* (stop I)) +* (stop J);
set CRSk = IncIC ((Comput (((P +* (stop I)) +* (stop J)),(Initialize (Result ((P +* (stop I)),s))),k)),(card I));
set CIJk = Comput ((P +* (stop (I ';' J))),s,((LifeSpan ((P +* (stop I)),s)) + k));
set PCIJk = P +* (stop (I ';' J));
set CRk1 = Comput (((P +* (stop I)) +* (stop J)),(Initialize (Result ((P +* (stop I)),s))),(k + 1));
set CRSk1 = (Comput (((P +* (stop I)) +* (stop J)),(Initialize (Result ((P +* (stop I)),s))),(k + 1))) +* (Start-At (((IC (Comput (((P +* (stop I)) +* (stop J)),(Initialize (Result ((P +* (stop I)),s))),(k + 1)))) + (card I)),SCMPDS));
set CIJk1 = Comput ((P +* (stop (I ';' J))),s,((LifeSpan ((P +* (stop I)),s)) + (k + 1)));
assume A10: NPP (IncIC ((Comput (((P +* (stop I)) +* (stop J)),(Initialize (Result ((P +* (stop I)),s))),k)),(card I))) = NPP (Comput ((P +* (stop (I ';' J))),s,((LifeSpan ((P +* (stop I)),s)) + k))) ; :: thesis: S1[k + 1]
A11: CurInstr (((P +* (stop I)) +* (stop J)),(Comput (((P +* (stop I)) +* (stop J)),(Initialize (Result ((P +* (stop I)),s))),k))) = CurInstr ((P +* (stop (I ';' J))),(Comput ((P +* (stop (I ';' J))),s,((LifeSpan ((P +* (stop I)),s)) + k))))
proof
A12: (P +* (stop (I ';' J))) /. (IC (Comput ((P +* (stop (I ';' J))),s,((LifeSpan ((P +* (stop I)),s)) + k)))) = (P +* (stop (I ';' J))) . (IC (Comput ((P +* (stop (I ';' J))),s,((LifeSpan ((P +* (stop I)),s)) + k)))) by PBOOLE:158;
A13: CurInstr ((P +* (stop (I ';' J))),(Comput ((P +* (stop (I ';' J))),s,((LifeSpan ((P +* (stop I)),s)) + k)))) = (P +* (stop (I ';' J))) . (IC (IncIC ((Comput (((P +* (stop I)) +* (stop J)),(Initialize (Result ((P +* (stop I)),s))),k)),(card I)))) by A10, A12, COMPOS_1:230
.= (P +* (stop (I ';' J))) . ((IC (Comput (((P +* (stop I)) +* (stop J)),(Initialize (Result ((P +* (stop I)),s))),k))) + (card I)) by FUNCT_4:121 ;
reconsider n = IC (Comput (((P +* (stop I)) +* (stop J)),(Initialize (Result ((P +* (stop I)),s))),k)) as Element of NAT ;
A14: stop (I ';' J) = I ';' (stop J) by AFINSQ_1:30;
A15: IC (Comput (((P +* (stop I)) +* (stop J)),(Initialize (Result ((P +* (stop I)),s))),k)) in dom (stop J) by FUNCT_4:26, SCMPDS_4:def 9;
then n < card (stop J) by AFINSQ_1:70;
then n + (card I) < (card (stop J)) + (card I) by XREAL_1:8;
then n + (card I) < card (stop (I ';' J)) by A14, AFINSQ_1:20;
then A16: (IC (Comput (((P +* (stop I)) +* (stop J)),(Initialize (Result ((P +* (stop I)),s))),k))) + (card I) in dom (stop (I ';' J)) by AFINSQ_1:70;
A17: ((P +* (stop I)) +* (stop J)) /. (IC (Comput (((P +* (stop I)) +* (stop J)),(Initialize (Result ((P +* (stop I)),s))),k))) = ((P +* (stop I)) +* (stop J)) . (IC (Comput (((P +* (stop I)) +* (stop J)),(Initialize (Result ((P +* (stop I)),s))),k))) by PBOOLE:158;
stop J c= (P +* (stop I)) +* (stop J) by FUNCT_4:26;
hence CurInstr (((P +* (stop I)) +* (stop J)),(Comput (((P +* (stop I)) +* (stop J)),(Initialize (Result ((P +* (stop I)),s))),k))) = (stop J) . (IC (Comput (((P +* (stop I)) +* (stop J)),(Initialize (Result ((P +* (stop I)),s))),k))) by A15, A17, GRFUNC_1:8
.= (stop (I ';' J)) . ((IC (Comput (((P +* (stop I)) +* (stop J)),(Initialize (Result ((P +* (stop I)),s))),k))) + (card I)) by A15, A14, AFINSQ_1:def 4
.= (P +* (stop (I ';' J))) . ((IC (Comput (((P +* (stop I)) +* (stop J)),(Initialize (Result ((P +* (stop I)),s))),k))) + (card I)) by A8, A16, GRFUNC_1:8
.= CurInstr ((P +* (stop (I ';' J))),(Comput ((P +* (stop (I ';' J))),s,((LifeSpan ((P +* (stop I)),s)) + k)))) by A13 ;
:: thesis: verum
end;
NPP (Comput ((P +* (stop (I ';' J))),s,((LifeSpan ((P +* (stop I)),s)) + k))) = NPP (IncIC ((Comput (((P +* (stop I)) +* (stop J)),(Initialize (Result ((P +* (stop I)),s))),k)),(card I))) by A10;
then xx: NPP (Exec ((CurInstr ((P +* (stop (I ';' J))),(Comput ((P +* (stop (I ';' J))),s,((LifeSpan ((P +* (stop I)),s)) + k))))),(Comput ((P +* (stop (I ';' J))),s,((LifeSpan ((P +* (stop I)),s)) + k))))) = NPP (Exec ((CurInstr (((P +* (stop I)) +* (stop J)),(Comput (((P +* (stop I)) +* (stop J)),(Initialize (Result ((P +* (stop I)),s))),k)))),(IncIC ((Comput (((P +* (stop I)) +* (stop J)),(Initialize (Result ((P +* (stop I)),s))),k)),(card I))))) by A11, SCMPDS_4:15;
stop J c= (P +* (stop I)) +* (stop J) by FUNCT_4:26;
then NPP (Exec ((CurInstr (((P +* (stop I)) +* (stop J)),(Comput (((P +* (stop I)) +* (stop J)),(Initialize (Result ((P +* (stop I)),s))),k)))),(IncIC ((Comput (((P +* (stop I)) +* (stop J)),(Initialize (Result ((P +* (stop I)),s))),k)),(card I))))) = NPP (IncIC ((Following (((P +* (stop I)) +* (stop J)),(Comput (((P +* (stop I)) +* (stop J)),(Initialize (Result ((P +* (stop I)),s))),k)))),(card I))) by Th35;
then A18: NPP (Exec ((CurInstr ((P +* (stop (I ';' J))),(Comput ((P +* (stop (I ';' J))),s,((LifeSpan ((P +* (stop I)),s)) + k))))),(Comput ((P +* (stop (I ';' J))),s,((LifeSpan ((P +* (stop I)),s)) + k))))) = NPP (IncIC ((Following (((P +* (stop I)) +* (stop J)),(Comput (((P +* (stop I)) +* (stop J)),(Initialize (Result ((P +* (stop I)),s))),k)))),(card I))) by xx;
Comput ((P +* (stop (I ';' J))),s,((LifeSpan ((P +* (stop I)),s)) + (k + 1))) = Comput ((P +* (stop (I ';' J))),s,(((LifeSpan ((P +* (stop I)),s)) + k) + 1)) ;
then A20: Comput ((P +* (stop (I ';' J))),s,((LifeSpan ((P +* (stop I)),s)) + (k + 1))) = Following ((P +* (stop (I ';' J))),(Comput ((P +* (stop (I ';' J))),s,((LifeSpan ((P +* (stop I)),s)) + k)))) by EXTPRO_1:4;
A21: now
let a be Int_position ; :: thesis: ((Comput (((P +* (stop I)) +* (stop J)),(Initialize (Result ((P +* (stop I)),s))),(k + 1))) +* (Start-At (((IC (Comput (((P +* (stop I)) +* (stop J)),(Initialize (Result ((P +* (stop I)),s))),(k + 1)))) + (card I)),SCMPDS))) . a = (Comput ((P +* (stop (I ';' J))),s,((LifeSpan ((P +* (stop I)),s)) + (k + 1)))) . a
thus ((Comput (((P +* (stop I)) +* (stop J)),(Initialize (Result ((P +* (stop I)),s))),(k + 1))) +* (Start-At (((IC (Comput (((P +* (stop I)) +* (stop J)),(Initialize (Result ((P +* (stop I)),s))),(k + 1)))) + (card I)),SCMPDS))) . a = (Comput (((P +* (stop I)) +* (stop J)),(Initialize (Result ((P +* (stop I)),s))),(k + 1))) . a by SCMPDS_3:14
.= (Following (((P +* (stop I)) +* (stop J)),(Comput (((P +* (stop I)) +* (stop J)),(Initialize (Result ((P +* (stop I)),s))),k)))) . a by EXTPRO_1:4
.= ((Following (((P +* (stop I)) +* (stop J)),(Comput (((P +* (stop I)) +* (stop J)),(Initialize (Result ((P +* (stop I)),s))),k)))) +* (Start-At (((IC (Following (((P +* (stop I)) +* (stop J)),(Comput (((P +* (stop I)) +* (stop J)),(Initialize (Result ((P +* (stop I)),s))),k))))) + (card I)),SCMPDS))) . a by SCMPDS_3:14
.= (Comput ((P +* (stop (I ';' J))),s,((LifeSpan ((P +* (stop I)),s)) + (k + 1)))) . a by A20, A18, SCMPDS_4:13 ; :: thesis: verum
end;
IC ((Comput (((P +* (stop I)) +* (stop J)),(Initialize (Result ((P +* (stop I)),s))),(k + 1))) +* (Start-At (((IC (Comput (((P +* (stop I)) +* (stop J)),(Initialize (Result ((P +* (stop I)),s))),(k + 1)))) + (card I)),SCMPDS))) = (IC (Comput (((P +* (stop I)) +* (stop J)),(Initialize (Result ((P +* (stop I)),s))),(k + 1)))) + (card I) by FUNCT_4:121
.= (IC (Following (((P +* (stop I)) +* (stop J)),(Comput (((P +* (stop I)) +* (stop J)),(Initialize (Result ((P +* (stop I)),s))),k))))) + (card I) by EXTPRO_1:4 ;
then IC ((Comput (((P +* (stop I)) +* (stop J)),(Initialize (Result ((P +* (stop I)),s))),(k + 1))) +* (Start-At (((IC (Comput (((P +* (stop I)) +* (stop J)),(Initialize (Result ((P +* (stop I)),s))),(k + 1)))) + (card I)),SCMPDS))) = IC ((Following (((P +* (stop I)) +* (stop J)),(Comput (((P +* (stop I)) +* (stop J)),(Initialize (Result ((P +* (stop I)),s))),k)))) +* (Start-At (((IC (Following (((P +* (stop I)) +* (stop J)),(Comput (((P +* (stop I)) +* (stop J)),(Initialize (Result ((P +* (stop I)),s))),k))))) + (card I)),SCMPDS))) by FUNCT_4:121
.= IC (Comput ((P +* (stop (I ';' J))),s,((LifeSpan ((P +* (stop I)),s)) + (k + 1)))) by A20, A18, COMPOS_1:230 ;
hence S1[k + 1] by A21, SCMPDS_4:11; :: thesis: verum
end;
Comput (((P +* (stop I)) +* (stop J)),(Initialize (Result ((P +* (stop I)),s))),0) = Initialize (Result ((P +* (stop I)),s)) by EXTPRO_1:3;
then A24: S1[ 0 ] by A6, SCMPDS_4:11;
for k being Element of NAT holds S1[k] from NAT_1:sch 1(A24, A9);
 hence NPP (IncIC ((Comput (((P +* (stop I)) +* (stop J)),(Initialize (Result ((P +* (stop I)),s))),k)),(card I))) = NPP (Comput ((P +* (stop (I ';' J))),s,((LifeSpan ((P +* (stop I)),s)) + k))) ; :: thesis: verum