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
set SA0 = Start-At (inspos 0 );
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)));
A1: Initialized (stop I) c= s +* (Initialized (stop I)) by FUNCT_4:26;
set s2 = Computation (s +* (Initialized (stop (I ';' J)))),((LifeSpan (s +* (Initialized (stop I)))) + 0 );
set s1 = ((Result (s +* (Initialized (stop I)))) +* (Initialized (stop J))) +* (Start-At ((IC ((Result (s +* (Initialized (stop I)))) +* (Initialized (stop J)))) + (card I)));
set IL = NAT ;
set m1 = LifeSpan (s +* (Initialized (stop I)));
A2: Initialized I c= Initialized (stop (I ';' J)) by Th15;
assume A3: 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
then A4: s = s +* (Initialized (stop (I ';' J))) by FUNCT_4:79;

A5: 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 A3, A4, A2, 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
A6: 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 A6, FUNCT_4:12
.= (Computation (s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) . a by A1, 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 S₁[ 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 ;
A7: stop (I ';' J) c= s +* (Initialized (stop (I ';' J))) by FUNCT_4:26, SCMPDS_4:57;
A8: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

proof

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[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 A9: (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: S₁[k + 1]
A10: 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

A11: 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 A9, 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 ;
reconsider n = IC (Computation ((Result (s +* (Initialized (stop I)))) +* (Initialized (stop J))),k) as Element of NAT by ORDINAL1:def 13;
A12: stop (I ';' J) = I ';' (stop J) by SCMPDS_4:46;
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;
then n < card (stop J) by 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 A12, SCMPDS_4:45;
then A14: (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, A12, SCMPDS_4:38
.= (s +* (Initialized (stop (I ';' J)))) . ((IC (Computation ((Result (s +* (Initialized (stop I)))) +* (Initialized (stop J))),k)) + (card I)) by A7, A14, GRFUNC_1:8
.= CurInstr (Computation (s +* (Initialized (stop (I ';' J)))),((LifeSpan (s +* (Initialized (stop I)))) + k)) by A11, AMI_1:54 ;
:: thesis: verum

end;

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 A9, 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 A10, SCMPDS_4:15;
then A15: 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;
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 A16: 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;

A17: 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 A16, A15, SCMPDS_4:13 ; :: thesis: verum

end;

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 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 A16, A15, AMI_1:121 ;
hence S₁[k + 1] by A17, SCMPDS_4:11; :: thesis: verum

end;

Computation ((Result (s +* (Initialized (stop I)))) +* (Initialized (stop J))),0 = (Result (s +* (Initialized (stop I)))) +* (Initialized (stop J)) by AMI_1:13;
then A18: S₁[ 0 ] by A5, SCMPDS_4:11;
for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A18, A8);
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