let s be State of SCMPDS; :: thesis: for I, J being Program of SCMPDS
for k being Element of NAT st I is_closed_on s & I is_halting_on s & k <= LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) holds
Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),k), Comput ((ProgramPart ((Initialize s) +* (I ';' J))),((Initialize s) +* (I ';' J)),k) equal_outside NAT
let I, J be Program of SCMPDS; :: thesis: for k being Element of NAT st I is_closed_on s & I is_halting_on s & k <= LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) holds
Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),k), Comput ((ProgramPart ((Initialize s) +* (I ';' J))),((Initialize s) +* (I ';' J)),k) equal_outside NAT
let k be Element of NAT ; :: thesis: ( I is_closed_on s & I is_halting_on s & k <= LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) implies Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),k), Comput ((ProgramPart ((Initialize s) +* (I ';' J))),((Initialize s) +* (I ';' J)),k) equal_outside NAT )
set spI = stop I;
set s1 = (Initialize s) +* (stop I);
set s2 = (Initialize s) +* (I ';' J);
set n = LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)));
assume that
A1: I is_closed_on s and
A2: I is_halting_on s ; :: thesis: ( not k <= LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) or Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),k), Comput ((ProgramPart ((Initialize s) +* (I ';' J))),((Initialize s) +* (I ';' J)),k) equal_outside NAT )
assume A3: k <= LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) ; :: thesis: Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),k), Comput ((ProgramPart ((Initialize s) +* (I ';' J))),((Initialize s) +* (I ';' J)),k) equal_outside NAT
defpred S₁[ Element of NAT ] means ( $1 <= LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) implies Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),$1), Comput ((ProgramPart ((Initialize s) +* (I ';' J))),((Initialize s) +* (I ';' J)),$1) equal_outside NAT );
A4: for m being Element of NAT st S₁[m] holds
S₁[m + 1]

proof

let m be Element of NAT ; :: thesis: ( S₁[m] implies S₁[m + 1] )
assume A5: ( m <= LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) implies Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),m), Comput ((ProgramPart ((Initialize s) +* (I ';' J))),((Initialize s) +* (I ';' J)),m) equal_outside NAT ) ; :: thesis: S₁[m + 1]
A6: ProgramPart ((Initialize s) +* (stop I)) = ProgramPart (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),m)) by AMI_1:123;
A7: Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(m + 1)) = Following ((ProgramPart ((Initialize s) +* (stop I))),(Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),m))) by EXTPRO_1:4
.= Exec ((CurInstr ((ProgramPart (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),m))),(Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),m)))),(Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),m))) by A6 ;
A8: IC (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),m)) in dom (stop I) by A1, SCMPDS_6:def 2;
A9: ProgramPart ((Initialize s) +* (I ';' J)) = ProgramPart (Comput ((ProgramPart ((Initialize s) +* (I ';' J))),((Initialize s) +* (I ';' J)),m)) by AMI_1:123;
A10: Comput ((ProgramPart ((Initialize s) +* (I ';' J))),((Initialize s) +* (I ';' J)),(m + 1)) = Following ((ProgramPart ((Initialize s) +* (I ';' J))),(Comput ((ProgramPart ((Initialize s) +* (I ';' J))),((Initialize s) +* (I ';' J)),m))) by EXTPRO_1:4
.= Exec ((CurInstr ((ProgramPart (Comput ((ProgramPart ((Initialize s) +* (I ';' J))),((Initialize s) +* (I ';' J)),m))),(Comput ((ProgramPart ((Initialize s) +* (I ';' J))),((Initialize s) +* (I ';' J)),m)))),(Comput ((ProgramPart ((Initialize s) +* (I ';' J))),((Initialize s) +* (I ';' J)),m))) by A9 ;
assume A11: m + 1 <= LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) ; :: thesis: Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(m + 1)), Comput ((ProgramPart ((Initialize s) +* (I ';' J))),((Initialize s) +* (I ';' J)),(m + 1)) equal_outside NAT
then m < LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) by NAT_1:13;
then A12: IC (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),m)) in dom I by A1, A2, SCMPDS_6:40;
then A13: IC (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),m)) in dom (I ';' J) by FUNCT_4:13;
A14: (ProgramPart (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),m))) /. (IC (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),m))) = (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),m)) . (IC (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),m))) by COMPOS_1:38;
A15: (ProgramPart (Comput ((ProgramPart ((Initialize s) +* (I ';' J))),((Initialize s) +* (I ';' J)),m))) /. (IC (Comput ((ProgramPart ((Initialize s) +* (I ';' J))),((Initialize s) +* (I ';' J)),m))) = (Comput ((ProgramPart ((Initialize s) +* (I ';' J))),((Initialize s) +* (I ';' J)),m)) . (IC (Comput ((ProgramPart ((Initialize s) +* (I ';' J))),((Initialize s) +* (I ';' J)),m))) by COMPOS_1:38;
CurInstr ((ProgramPart (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),m))),(Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),m))) = ((Initialize s) +* (stop I)) . (IC (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),m))) by A14, AMI_1:54
.= (stop I) . (IC (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),m))) by A8, FUNCT_4:14
.= I . (IC (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),m))) by A12, AFINSQ_1:def 4
.= (I ';' J) . (IC (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),m))) by A12, AFINSQ_1:def 4
.= ((Initialize s) +* (I ';' J)) . (IC (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),m))) by A13, FUNCT_4:14
.= (Comput ((ProgramPart ((Initialize s) +* (I ';' J))),((Initialize s) +* (I ';' J)),m)) . (IC (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),m))) by AMI_1:54
.= CurInstr ((ProgramPart (Comput ((ProgramPart ((Initialize s) +* (I ';' J))),((Initialize s) +* (I ';' J)),m))),(Comput ((ProgramPart ((Initialize s) +* (I ';' J))),((Initialize s) +* (I ';' J)),m))) by A5, A11, A15, COMPOS_1:24, NAT_1:13 ;
hence Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(m + 1)), Comput ((ProgramPart ((Initialize s) +* (I ';' J))),((Initialize s) +* (I ';' J)),(m + 1)) equal_outside NAT by A5, A11, A10, A7, NAT_1:13, SCMPDS_4:15; :: thesis: verum

end;

A16: Comput ((ProgramPart ((Initialize s) +* (I ';' J))),((Initialize s) +* (I ';' J)),0) = (Initialize s) +* (I ';' J) by EXTPRO_1:3;
A17: Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),0) = (Initialize s) +* (stop I) by EXTPRO_1:3;
A18: Initialize s,(Initialize s) +* (I ';' J) equal_outside NAT by FUNCT_7:132;
(Initialize s) +* (stop I), Initialize s equal_outside NAT by FUNCT_7:28, FUNCT_7:132;
then A19: S₁[ 0 ] by A18, A17, A16, FUNCT_7:29;
for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A19, A4);
hence Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),k), Comput ((ProgramPart ((Initialize s) +* (I ';' J))),((Initialize s) +* (I ';' J)),k) equal_outside NAT by A3; :: thesis: verum