let s be State of SCM+FSA; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 S_{1}[ 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 ; :: thesis: 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)

_{1}[ 0 ]
;

thus for k being Nat holds S_{1}[k]
from NAT_1:sch 2(A16, A4); :: thesis: verum

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; :: thesis: 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; :: thesis: ( 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 S

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 ; :: thesis: 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 :: thesis: for k being Nat st S_{1}[k] holds

S_{1}[k + 1]

A16:
SS

let k be Nat; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

assume A5: S_{1}[k]
; :: thesis: S_{1}[k + 1]

thus S_{1}[k + 1]
:: thesis: verum

end;assume A5: S

thus S

proof

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) ; :: thesis: 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; :: thesis: verum

end;.= 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) ; :: thesis: 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; :: thesis: verum

thus for k being Nat holds S