let s be State of SCM+FSA; for P being Instruction-Sequence of SCM+FSA
for I, J being Program of SCM+FSA st I is_pseudo-closed_on s,P holds
for k being Nat st k <= pseudo-LifeSpan (s,P,I) holds
Comput ((P +* I),(Initialize s),k) = Comput ((P +* (I ";" J)),(Initialize s),k)
let P be Instruction-Sequence of SCM+FSA; for I, J being Program of SCM+FSA st I is_pseudo-closed_on s,P holds
for k being Nat st k <= pseudo-LifeSpan (s,P,I) holds
Comput ((P +* I),(Initialize s),k) = Comput ((P +* (I ";" J)),(Initialize s),k)
let I, J be Program of SCM+FSA; ( I is_pseudo-closed_on s,P implies for k being Nat st k <= pseudo-LifeSpan (s,P,I) holds
Comput ((P +* I),(Initialize s),k) = Comput ((P +* (I ";" J)),(Initialize s),k) )
set s1 = Initialize s;
set s2 = Initialize s;
defpred S1[ Nat] means ( $1 <= pseudo-LifeSpan (s,P,I) implies Comput ((P +* I),(Initialize s),$1) = Comput ((P +* (I ";" J)),(Initialize s),$1) );
A1:
dom (P +* I) = NAT
by PARTFUN1:def 2;
A2:
dom (P +* (I ";" J)) = NAT
by PARTFUN1:def 2;
assume A3:
I is_pseudo-closed_on s,P
; for k being Nat st k <= pseudo-LifeSpan (s,P,I) holds
Comput ((P +* I),(Initialize s),k) = Comput ((P +* (I ";" J)),(Initialize s),k)
A4:
now for k being Nat st S1[k] holds
S1[k + 1]let k be
Nat;
( S1[k] implies S1[k + 1] )assume A5:
S1[
k]
;
S1[k + 1]thus
S1[
k + 1]
verumproof
A6:
Comput (
(P +* (I ";" J)),
(Initialize s),
(k + 1)) =
Following (
(P +* (I ";" J)),
(Comput ((P +* (I ";" J)),(Initialize s),k)))
by EXTPRO_1:3
.=
Exec (
(CurInstr ((P +* (I ";" J)),(Comput ((P +* (I ";" J)),(Initialize s),k)))),
(Comput ((P +* (I ";" J)),(Initialize s),k)))
;
A7:
Comput (
(P +* I),
(Initialize s),
(k + 1)) =
Following (
(P +* I),
(Comput ((P +* I),(Initialize s),k)))
by EXTPRO_1:3
.=
Exec (
(CurInstr ((P +* I),(Comput ((P +* I),(Initialize s),k)))),
(Comput ((P +* I),(Initialize s),k)))
;
A8:
dom I c= dom (I ";" J)
by SCMFSA6A:17;
A9:
k + 0 < k + 1
by XREAL_1:6;
assume A10:
k + 1
<= pseudo-LifeSpan (
s,
P,
I)
;
Comput ((P +* I),(Initialize s),(k + 1)) = Comput ((P +* (I ";" J)),(Initialize s),(k + 1))
then A11:
k < pseudo-LifeSpan (
s,
P,
I)
by A9, XXREAL_0:2;
then A12:
IC (Comput ((P +* I),(Initialize s),k)) in dom I
by A3, Th10;
A13:
I c= P +* I
by FUNCT_4:25;
A14:
I ";" J c= P +* (I ";" J)
by FUNCT_4:25;
A15:
CurInstr (
(P +* I),
(Comput ((P +* I),(Initialize s),k))) =
(P +* I) . (IC (Comput ((P +* I),(Initialize s),k)))
by A1, PARTFUN1:def 6
.=
I . (IC (Comput ((P +* I),(Initialize s),k)))
by A12, A13, GRFUNC_1:2
;
then
I . (IC (Comput ((P +* I),(Initialize s),k))) <> halt SCM+FSA
by A3, A11, Th10;
then CurInstr (
(P +* I),
(Comput ((P +* I),(Initialize s),k))) =
(I ";" J) . (IC (Comput ((P +* I),(Initialize s),k)))
by A12, A15, SCMFSA6A:15
.=
(P +* (I ";" J)) . (IC (Comput ((P +* I),(Initialize s),k)))
by A12, A8, A14, GRFUNC_1:2
.=
(P +* (I ";" J)) . (IC (Comput ((P +* (I ";" J)),(Initialize s),k)))
by A5, A10, A9, XXREAL_0:2
.=
CurInstr (
(P +* (I ";" J)),
(Comput ((P +* (I ";" J)),(Initialize s),k)))
by A2, PARTFUN1:def 6
;
hence
Comput (
(P +* I),
(Initialize s),
(k + 1))
= Comput (
(P +* (I ";" J)),
(Initialize s),
(k + 1))
by A5, A10, A9, A7, A6, XXREAL_0:2;
verum
end; end;
A16:
S1[ 0 ]
;
thus
for k being Nat holds S1[k]
from NAT_1:sch 2(A16, A4); verum