let s be State of SCMPDS; for P being Instruction-Sequence of SCMPDS
for I, J being Program of
for k being Nat st I is_closed_on s,P & I is_halting_on s,P & k <= LifeSpan ((P +* (stop I)),(Initialize s)) holds
Comput ((P +* (stop I)),(Initialize s),k) = Comput ((P +* (I ';' J)),(Initialize s),k)
let P be Instruction-Sequence of SCMPDS; for I, J being Program of
for k being Nat st I is_closed_on s,P & I is_halting_on s,P & k <= LifeSpan ((P +* (stop I)),(Initialize s)) holds
Comput ((P +* (stop I)),(Initialize s),k) = Comput ((P +* (I ';' J)),(Initialize s),k)
let I, J be Program of ; for k being Nat st I is_closed_on s,P & I is_halting_on s,P & k <= LifeSpan ((P +* (stop I)),(Initialize s)) holds
Comput ((P +* (stop I)),(Initialize s),k) = Comput ((P +* (I ';' J)),(Initialize s),k)
let k be Nat; ( I is_closed_on s,P & I is_halting_on s,P & k <= LifeSpan ((P +* (stop I)),(Initialize s)) implies Comput ((P +* (stop I)),(Initialize s),k) = Comput ((P +* (I ';' J)),(Initialize s),k) )
set spI = stop I;
set s1 = Initialize s;
set P1 = P +* (stop I);
set s2 = Initialize s;
set P2 = P +* (I ';' J);
set n = LifeSpan ((P +* (stop I)),(Initialize s));
assume that
A1:
I is_closed_on s,P
and
A2:
I is_halting_on s,P
; ( not k <= LifeSpan ((P +* (stop I)),(Initialize s)) or Comput ((P +* (stop I)),(Initialize s),k) = Comput ((P +* (I ';' J)),(Initialize s),k) )
assume A3:
k <= LifeSpan ((P +* (stop I)),(Initialize s))
; Comput ((P +* (stop I)),(Initialize s),k) = Comput ((P +* (I ';' J)),(Initialize s),k)
defpred S1[ Nat] means ( $1 <= LifeSpan ((P +* (stop I)),(Initialize s)) implies Comput ((P +* (stop I)),(Initialize s),$1) = Comput ((P +* (I ';' J)),(Initialize s),$1) );
A4:
for m being Nat st S1[m] holds
S1[m + 1]
proof
let m be
Nat;
( S1[m] implies S1[m + 1] )
assume A5:
(
m <= LifeSpan (
(P +* (stop I)),
(Initialize s)) implies
Comput (
(P +* (stop I)),
(Initialize s),
m)
= Comput (
(P +* (I ';' J)),
(Initialize s),
m) )
;
S1[m + 1]
A6:
Comput (
(P +* (stop I)),
(Initialize s),
(m + 1)) =
Following (
(P +* (stop I)),
(Comput ((P +* (stop I)),(Initialize s),m)))
by EXTPRO_1:3
.=
Exec (
(CurInstr ((P +* (stop I)),(Comput ((P +* (stop I)),(Initialize s),m)))),
(Comput ((P +* (stop I)),(Initialize s),m)))
;
A7:
IC (Comput ((P +* (stop I)),(Initialize s),m)) in dom (stop I)
by A1, SCMPDS_6:def 2;
A8:
Comput (
(P +* (I ';' J)),
(Initialize s),
(m + 1)) =
Following (
(P +* (I ';' J)),
(Comput ((P +* (I ';' J)),(Initialize s),m)))
by EXTPRO_1:3
.=
Exec (
(CurInstr ((P +* (I ';' J)),(Comput ((P +* (I ';' J)),(Initialize s),m)))),
(Comput ((P +* (I ';' J)),(Initialize s),m)))
;
assume A9:
m + 1
<= LifeSpan (
(P +* (stop I)),
(Initialize s))
;
Comput ((P +* (stop I)),(Initialize s),(m + 1)) = Comput ((P +* (I ';' J)),(Initialize s),(m + 1))
then
m < LifeSpan (
(P +* (stop I)),
(Initialize s))
by NAT_1:13;
then A10:
IC (Comput ((P +* (stop I)),(Initialize s),m)) in dom I
by A1, A2, SCMPDS_6:26;
then A11:
IC (Comput ((P +* (stop I)),(Initialize s),m)) in dom (I ';' J)
by FUNCT_4:12;
CurInstr (
(P +* (stop I)),
(Comput ((P +* (stop I)),(Initialize s),m))) =
(P +* (stop I)) . (IC (Comput ((P +* (stop I)),(Initialize s),m)))
by PBOOLE:143
.=
(stop I) . (IC (Comput ((P +* (stop I)),(Initialize s),m)))
by A7, FUNCT_4:13
.=
I . (IC (Comput ((P +* (stop I)),(Initialize s),m)))
by A10, AFINSQ_1:def 3
.=
(I ';' J) . (IC (Comput ((P +* (stop I)),(Initialize s),m)))
by A10, AFINSQ_1:def 3
.=
(P +* (I ';' J)) . (IC (Comput ((P +* (stop I)),(Initialize s),m)))
by A11, FUNCT_4:13
.=
CurInstr (
(P +* (I ';' J)),
(Comput ((P +* (I ';' J)),(Initialize s),m)))
by A5, A9, NAT_1:13, PBOOLE:143
;
hence
Comput (
(P +* (stop I)),
(Initialize s),
(m + 1))
= Comput (
(P +* (I ';' J)),
(Initialize s),
(m + 1))
by A5, A9, A8, A6, NAT_1:13;
verum
end;
A12:
S1[ 0 ]
;
for k being Nat holds S1[k]
from NAT_1:sch 2(A12, A4);
hence
Comput ((P +* (stop I)),(Initialize s),k) = Comput ((P +* (I ';' J)),(Initialize s),k)
by A3; verum