let s be State of SCMPDS ; :: thesis: for I being parahalting No-StopCode Program of SCMPDS
for J being parahalting shiftable Program of SCMPDS
for k being Element of NAT st Initialized (stop (I ';' J)) c= s holds
(Computation ((Result (s +* (Initialized (stop I)))) +* (Initialized (stop J))),k) +* (Start-At ((IC (Computation ((Result (s +* (Initialized (stop I)))) +* (Initialized (stop J))),k)) + (card I))), Computation (s +* (Initialized (stop (I ';' J)))),((LifeSpan (s +* (Initialized (stop I)))) + k) equal_outside NAT
let I be parahalting No-StopCode Program of SCMPDS ; :: thesis: for J being parahalting shiftable Program of SCMPDS
for k being Element of NAT st Initialized (stop (I ';' J)) c= s holds
(Computation ((Result (s +* (Initialized (stop I)))) +* (Initialized (stop J))),k) +* (Start-At ((IC (Computation ((Result (s +* (Initialized (stop I)))) +* (Initialized (stop J))),k)) + (card I))), Computation (s +* (Initialized (stop (I ';' J)))),((LifeSpan (s +* (Initialized (stop I)))) + k) equal_outside NAT
let J be parahalting shiftable Program of SCMPDS ; :: thesis: for k being Element of NAT st Initialized (stop (I ';' J)) c= s holds
(Computation ((Result (s +* (Initialized (stop I)))) +* (Initialized (stop J))),k) +* (Start-At ((IC (Computation ((Result (s +* (Initialized (stop I)))) +* (Initialized (stop J))),k)) + (card I))), Computation (s +* (Initialized (stop (I ';' J)))),((LifeSpan (s +* (Initialized (stop I)))) + k) equal_outside NAT
let k be Element of NAT ; :: thesis: ( Initialized (stop (I ';' J)) c= s implies (Computation ((Result (s +* (Initialized (stop I)))) +* (Initialized (stop J))),k) +* (Start-At ((IC (Computation ((Result (s +* (Initialized (stop I)))) +* (Initialized (stop J))),k)) + (card I))), Computation (s +* (Initialized (stop (I ';' J)))),((LifeSpan (s +* (Initialized (stop I)))) + k) equal_outside NAT )
set IsI = Initialized (stop I);
set sIsI = s +* (Initialized (stop I));
set RI = Result (s +* (Initialized (stop I)));
set pJ = stop J;
set IsJ = Initialized (stop J);
set RIJ = (Result (s +* (Initialized (stop I)))) +* (Initialized (stop J));
set pIJ = stop (I ';' J);
set IsIJ = Initialized (stop (I ';' J));
set sIsIJ = s +* (Initialized (stop (I ';' J)));
assume A1: Initialized (stop (I ';' J)) c= s ; :: thesis: (Computation ((Result (s +* (Initialized (stop I)))) +* (Initialized (stop J))),k) +* (Start-At ((IC (Computation ((Result (s +* (Initialized (stop I)))) +* (Initialized (stop J))),k)) + (card I))), Computation (s +* (Initialized (stop (I ';' J)))),((LifeSpan (s +* (Initialized (stop I)))) + k) equal_outside NAT
A2: Initialized (stop I) c= s +* (Initialized (stop I)) by FUNCT_4:26;
A3: stop (I ';' J) c= s +* (Initialized (stop (I ';' J))) by FUNCT_4:26, SCMPDS_4:57;
A4: s = s +* (Initialized (stop (I ';' J))) by A1, FUNCT_4:79;
A5: Initialized I c= Initialized (stop (I ';' J)) by Th15;
set SA0 = Start-At (inspos 0 );
set IL = NAT ;
set m1 = LifeSpan (s +* (Initialized (stop I)));
set s1 = ((Result (s +* (Initialized (stop I)))) +* (Initialized (stop J))) +* (Start-At ((IC ((Result (s +* (Initialized (stop I)))) +* (Initialized (stop J)))) + (card I)));
set s2 = Computation (s +* (Initialized (stop (I ';' J)))),((LifeSpan (s +* (Initialized (stop I)))) + 0 );
A6: now
thus IC (((Result (s +* (Initialized (stop I)))) +* (Initialized (stop J))) +* (Start-At ((IC ((Result (s +* (Initialized (stop I)))) +* (Initialized (stop J)))) + (card I)))) = (IC ((Result (s +* (Initialized (stop I)))) +* ((stop J) +* (Start-At (inspos 0 ))))) + (card I) by AMI_1:111
.= (IC (((Result (s +* (Initialized (stop I)))) +* (stop J)) +* (Start-At (inspos 0 )))) + (card I) by FUNCT_4:15
.= inspos (0 + (card I)) by AMI_1:111
.= IC (Computation (s +* (Initialized (stop (I ';' J)))),((LifeSpan (s +* (Initialized (stop I)))) + 0 )) by A1, A4, A5, Th30, XBOOLE_1:1 ; :: thesis: for a being Int_position holds (((Result (s +* (Initialized (stop I)))) +* (Initialized (stop J))) +* (Start-At ((IC ((Result (s +* (Initialized (stop I)))) +* (Initialized (stop J)))) + (card I)))) . a = (Computation (s +* (Initialized (stop (I ';' J)))),((LifeSpan (s +* (Initialized (stop I)))) + 0 )) . a
hereby :: thesis: verum
let a be Int_position ; :: thesis: (((Result (s +* (Initialized (stop I)))) +* (Initialized (stop J))) +* (Start-At ((IC ((Result (s +* (Initialized (stop I)))) +* (Initialized (stop J)))) + (card I)))) . a = (Computation (s +* (Initialized (stop (I ';' J)))),((LifeSpan (s +* (Initialized (stop I)))) + 0 )) . a
A7: not a in dom ((stop J) +* (Start-At (inspos 0 ))) by SCMPDS_4:61;
not a in dom (Start-At ((IC ((Result (s +* (Initialized (stop I)))) +* (Initialized (stop J)))) + (card I))) by SCMPDS_4:59;
hence (((Result (s +* (Initialized (stop I)))) +* (Initialized (stop J))) +* (Start-At ((IC ((Result (s +* (Initialized (stop I)))) +* (Initialized (stop J)))) + (card I)))) . a = ((Result (s +* (Initialized (stop I)))) +* (Initialized (stop J))) . a by FUNCT_4:12
.= (Result (s +* (Initialized (stop I)))) . a by A7, FUNCT_4:12
.= (Computation (s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) . a by A2, AMI_1:122, SCMPDS_4:63
.= (Computation (s +* (Initialized (stop (I ';' J)))),((LifeSpan (s +* (Initialized (stop I)))) + 0 )) . a by Th34, SCMPDS_4:13 ;
:: thesis: verum
end;
end;
defpred S1[ Element of NAT ] means (Computation ((Result (s +* (Initialized (stop I)))) +* (Initialized (stop J))),$1) +* (Start-At ((IC (Computation ((Result (s +* (Initialized (stop I)))) +* (Initialized (stop J))),$1)) + (card I))), Computation (s +* (Initialized (stop (I ';' J)))),((LifeSpan (s +* (Initialized (stop I)))) + $1) equal_outside NAT ;
Computation ((Result (s +* (Initialized (stop I)))) +* (Initialized (stop J))),0 = (Result (s +* (Initialized (stop I)))) +* (Initialized (stop J)) by AMI_1:13;
then A8: S1[ 0 ] by A6, SCMPDS_4:11;
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 = Computation ((Result (s +* (Initialized (stop I)))) +* (Initialized (stop J))),k;
set CRSk = (Computation ((Result (s +* (Initialized (stop I)))) +* (Initialized (stop J))),k) +* (Start-At ((IC (Computation ((Result (s +* (Initialized (stop I)))) +* (Initialized (stop J))),k)) + (card I)));
set CIJk = Computation (s +* (Initialized (stop (I ';' J)))),((LifeSpan (s +* (Initialized (stop I)))) + k);
set CRk1 = Computation ((Result (s +* (Initialized (stop I)))) +* (Initialized (stop J))),(k + 1);
set CRSk1 = (Computation ((Result (s +* (Initialized (stop I)))) +* (Initialized (stop J))),(k + 1)) +* (Start-At ((IC (Computation ((Result (s +* (Initialized (stop I)))) +* (Initialized (stop J))),(k + 1))) + (card I)));
set CIJk1 = Computation (s +* (Initialized (stop (I ';' J)))),((LifeSpan (s +* (Initialized (stop I)))) + (k + 1));
assume A10: (Computation ((Result (s +* (Initialized (stop I)))) +* (Initialized (stop J))),k) +* (Start-At ((IC (Computation ((Result (s +* (Initialized (stop I)))) +* (Initialized (stop J))),k)) + (card I))), Computation (s +* (Initialized (stop (I ';' J)))),((LifeSpan (s +* (Initialized (stop I)))) + k) equal_outside NAT ; :: thesis: S1[k + 1]
A11: CurInstr (Computation ((Result (s +* (Initialized (stop I)))) +* (Initialized (stop J))),k) = CurInstr (Computation (s +* (Initialized (stop (I ';' J)))),((LifeSpan (s +* (Initialized (stop I)))) + k))
proof
A12: CurInstr (Computation (s +* (Initialized (stop (I ';' J)))),((LifeSpan (s +* (Initialized (stop I)))) + k)) = (Computation (s +* (Initialized (stop (I ';' J)))),((LifeSpan (s +* (Initialized (stop I)))) + k)) . (IC ((Computation ((Result (s +* (Initialized (stop I)))) +* (Initialized (stop J))),k) +* (Start-At ((IC (Computation ((Result (s +* (Initialized (stop I)))) +* (Initialized (stop J))),k)) + (card I))))) by A10, AMI_1:121
.= (Computation (s +* (Initialized (stop (I ';' J)))),((LifeSpan (s +* (Initialized (stop I)))) + k)) . ((IC (Computation ((Result (s +* (Initialized (stop I)))) +* (Initialized (stop J))),k)) + (card I)) by AMI_1:111 ;
Initialized (stop J) c= (Result (s +* (Initialized (stop I)))) +* (Initialized (stop J)) by FUNCT_4:26;
then A13: IC (Computation ((Result (s +* (Initialized (stop I)))) +* (Initialized (stop J))),k) in dom (stop J) by SCMPDS_4:def 9;
A14: stop (I ';' J) = I ';' (stop J) by SCMPDS_4:46;
reconsider n = IC (Computation ((Result (s +* (Initialized (stop I)))) +* (Initialized (stop J))),k) as Element of NAT by ORDINAL1:def 13;
n < card (stop J) by A13, SCMPDS_4:1;
then n + (card I) < (card (stop J)) + (card I) by XREAL_1:8;
then n + (card I) < card (stop (I ';' J)) by A14, SCMPDS_4:45;
then A16: (IC (Computation ((Result (s +* (Initialized (stop I)))) +* (Initialized (stop J))),k)) + (card I) in dom (stop (I ';' J)) by SCMPDS_4:1;
(Result (s +* (Initialized (stop I)))) +* (Initialized (stop J)) = ((Result (s +* (Initialized (stop I)))) +* (stop J)) +* (Start-At (inspos 0 )) by FUNCT_4:15
.= ((Result (s +* (Initialized (stop I)))) +* (Start-At (inspos 0 ))) +* (stop J) by SCMPDS_4:62 ;
then stop J c= Computation ((Result (s +* (Initialized (stop I)))) +* (Initialized (stop J))),k by AMI_1:81, FUNCT_4:26;
hence CurInstr (Computation ((Result (s +* (Initialized (stop I)))) +* (Initialized (stop J))),k) = (stop J) . (IC (Computation ((Result (s +* (Initialized (stop I)))) +* (Initialized (stop J))),k)) by A13, GRFUNC_1:8
.= (stop (I ';' J)) . ((IC (Computation ((Result (s +* (Initialized (stop I)))) +* (Initialized (stop J))),k)) + (card I)) by A13, A14, SCMPDS_4:38
.= (s +* (Initialized (stop (I ';' J)))) . ((IC (Computation ((Result (s +* (Initialized (stop I)))) +* (Initialized (stop J))),k)) + (card I)) by A3, A16, GRFUNC_1:8
.= CurInstr (Computation (s +* (Initialized (stop (I ';' J)))),((LifeSpan (s +* (Initialized (stop I)))) + k)) by A12, AMI_1:54 ;
:: thesis: verum
end;
Computation (s +* (Initialized (stop (I ';' J)))),((LifeSpan (s +* (Initialized (stop I)))) + (k + 1)) = Computation (s +* (Initialized (stop (I ';' J)))),(((LifeSpan (s +* (Initialized (stop I)))) + k) + 1) ;
then A17: Computation (s +* (Initialized (stop (I ';' J)))),((LifeSpan (s +* (Initialized (stop I)))) + (k + 1)) = Following (Computation (s +* (Initialized (stop (I ';' J)))),((LifeSpan (s +* (Initialized (stop I)))) + k)) by AMI_1:14;
Computation (s +* (Initialized (stop (I ';' J)))),((LifeSpan (s +* (Initialized (stop I)))) + k),(Computation ((Result (s +* (Initialized (stop I)))) +* (Initialized (stop J))),k) +* (Start-At ((IC (Computation ((Result (s +* (Initialized (stop I)))) +* (Initialized (stop J))),k)) + (card I))) equal_outside NAT by A10, FUNCT_7:28;
then Exec (CurInstr (Computation (s +* (Initialized (stop (I ';' J)))),((LifeSpan (s +* (Initialized (stop I)))) + k))),(Computation (s +* (Initialized (stop (I ';' J)))),((LifeSpan (s +* (Initialized (stop I)))) + k)), Exec (CurInstr (Computation ((Result (s +* (Initialized (stop I)))) +* (Initialized (stop J))),k)),((Computation ((Result (s +* (Initialized (stop I)))) +* (Initialized (stop J))),k) +* (Start-At ((IC (Computation ((Result (s +* (Initialized (stop I)))) +* (Initialized (stop J))),k)) + (card I)))) equal_outside NAT by A11, SCMPDS_4:15;
then A18: Exec (CurInstr (Computation (s +* (Initialized (stop (I ';' J)))),((LifeSpan (s +* (Initialized (stop I)))) + k))),(Computation (s +* (Initialized (stop (I ';' J)))),((LifeSpan (s +* (Initialized (stop I)))) + k)),(Following (Computation ((Result (s +* (Initialized (stop I)))) +* (Initialized (stop J))),k)) +* (Start-At ((IC (Following (Computation ((Result (s +* (Initialized (stop I)))) +* (Initialized (stop J))),k))) + (card I))) equal_outside NAT by Th35;
IC ((Computation ((Result (s +* (Initialized (stop I)))) +* (Initialized (stop J))),(k + 1)) +* (Start-At ((IC (Computation ((Result (s +* (Initialized (stop I)))) +* (Initialized (stop J))),(k + 1))) + (card I)))) = (IC (Computation ((Result (s +* (Initialized (stop I)))) +* (Initialized (stop J))),(k + 1))) + (card I) by AMI_1:111
.= (IC (Following (Computation ((Result (s +* (Initialized (stop I)))) +* (Initialized (stop J))),k))) + (card I) by AMI_1:14 ;
then A19: IC ((Computation ((Result (s +* (Initialized (stop I)))) +* (Initialized (stop J))),(k + 1)) +* (Start-At ((IC (Computation ((Result (s +* (Initialized (stop I)))) +* (Initialized (stop J))),(k + 1))) + (card I)))) = IC ((Following (Computation ((Result (s +* (Initialized (stop I)))) +* (Initialized (stop J))),k)) +* (Start-At ((IC (Following (Computation ((Result (s +* (Initialized (stop I)))) +* (Initialized (stop J))),k))) + (card I)))) by AMI_1:111
.= IC (Computation (s +* (Initialized (stop (I ';' J)))),((LifeSpan (s +* (Initialized (stop I)))) + (k + 1))) by A17, A18, AMI_1:121 ;
now
let a be Int_position ; :: thesis: ((Computation ((Result (s +* (Initialized (stop I)))) +* (Initialized (stop J))),(k + 1)) +* (Start-At ((IC (Computation ((Result (s +* (Initialized (stop I)))) +* (Initialized (stop J))),(k + 1))) + (card I)))) . a = (Computation (s +* (Initialized (stop (I ';' J)))),((LifeSpan (s +* (Initialized (stop I)))) + (k + 1))) . a
thus ((Computation ((Result (s +* (Initialized (stop I)))) +* (Initialized (stop J))),(k + 1)) +* (Start-At ((IC (Computation ((Result (s +* (Initialized (stop I)))) +* (Initialized (stop J))),(k + 1))) + (card I)))) . a = (Computation ((Result (s +* (Initialized (stop I)))) +* (Initialized (stop J))),(k + 1)) . a by SCMPDS_3:14
.= (Following (Computation ((Result (s +* (Initialized (stop I)))) +* (Initialized (stop J))),k)) . a by AMI_1:14
.= ((Following (Computation ((Result (s +* (Initialized (stop I)))) +* (Initialized (stop J))),k)) +* (Start-At ((IC (Following (Computation ((Result (s +* (Initialized (stop I)))) +* (Initialized (stop J))),k))) + (card I)))) . a by SCMPDS_3:14
.= (Computation (s +* (Initialized (stop (I ';' J)))),((LifeSpan (s +* (Initialized (stop I)))) + (k + 1))) . a by A17, A18, SCMPDS_4:13 ; :: thesis: verum
end;
hence S1[k + 1] by A19, SCMPDS_4:11; :: thesis: verum
end;
for k being Element of NAT holds S1[k] from NAT_1:sch 1(A8, A9);
 hence (Computation ((Result (s +* (Initialized (stop I)))) +* (Initialized (stop J))),k) +* (Start-At ((IC (Computation ((Result (s +* (Initialized (stop I)))) +* (Initialized (stop J))),k)) + (card I))), Computation (s +* (Initialized (stop (I ';' J)))),((LifeSpan (s +* (Initialized (stop I)))) + k) equal_outside NAT ; :: thesis: verum