:: SCMFSA8A semantic presentation

begin

  set A = NAT ;

set D = Data-Locations ;

set SA0 = Start-At (0,SCM+FSA);

set T = (intloc 0) .--> 1;

theorem :: SCMFSA8A:1
canceled;

theorem :: SCMFSA8A:2
canceled;

theorem :: SCMFSA8A:3
canceled;

theorem :: SCMFSA8A:4
canceled;

theorem :: SCMFSA8A:5
canceled;

theorem :: SCMFSA8A:6
canceled;

theorem :: SCMFSA8A:7
for P being preProgram of SCM+FSA
for l being Element of NAT
for x being set st x in dom P holds
( ( P . x = halt SCM+FSA implies (Directed (P,l)) . x = goto l ) & ( P . x <> halt SCM+FSA implies (Directed (P,l)) . x = P . x ) ) by FUNCT_4:105, FUNCT_4:106;

theorem Th8: :: SCMFSA8A:8
for i being Instruction of SCM+FSA
for a being Int-Location
for n being Element of NAT st not i destroys a holds
not IncAddr (i,n) destroys a
proof
let i be Instruction of SCM+FSA; ::_thesis: for a being Int-Location
for n being Element of NAT st not i destroys a holds
not IncAddr (i,n) destroys a
let a be Int-Location; ::_thesis: for n being Element of NAT st not i destroys a holds
not IncAddr (i,n) destroys a
let n be Element of NAT ; ::_thesis: ( not i destroys a implies not IncAddr (i,n) destroys a )
assume A1: not i destroys a ; ::_thesis: not IncAddr (i,n) destroys a
percases ( InsCode i = 0 or InsCode i = 1 or InsCode i = 2 or InsCode i = 3 or InsCode i = 4 or InsCode i = 5 or InsCode i = 6 or InsCode i = 7 or InsCode i = 8 or InsCode i = 9 or InsCode i = 10 or InsCode i = 11 or InsCode i = 12 ) by NAT_1:36, SCMFSA_2:16;
suppose InsCode i = 0 ; ::_thesis: not IncAddr (i,n) destroys a
then  i = halt SCM+FSA by SCMFSA_2:95;
then  IncAddr (i,n) = halt SCM+FSA by COMPOS_0:4;
hence  not IncAddr (i,n) destroys a by SCMFSA7B:5; ::_thesis: verum
end;
suppose InsCode i = 1 ; ::_thesis: not IncAddr (i,n) destroys a
then  ex da, db being Int-Location st i = da := db by SCMFSA_2:30;
hence  not IncAddr (i,n) destroys a by A1, COMPOS_0:4; ::_thesis: verum
end;
suppose InsCode i = 2 ; ::_thesis: not IncAddr (i,n) destroys a
then  ex da, db being Int-Location st i = AddTo (da,db) by SCMFSA_2:31;
hence  not IncAddr (i,n) destroys a by A1, COMPOS_0:4; ::_thesis: verum
end;
suppose InsCode i = 3 ; ::_thesis: not IncAddr (i,n) destroys a
then  ex da, db being Int-Location st i = SubFrom (da,db) by SCMFSA_2:32;
hence  not IncAddr (i,n) destroys a by A1, COMPOS_0:4; ::_thesis: verum
end;
suppose InsCode i = 4 ; ::_thesis: not IncAddr (i,n) destroys a
then  ex da, db being Int-Location st i = MultBy (da,db) by SCMFSA_2:33;
hence  not IncAddr (i,n) destroys a by A1, COMPOS_0:4; ::_thesis: verum
end;
suppose InsCode i = 5 ; ::_thesis: not IncAddr (i,n) destroys a
then  ex da, db being Int-Location st i = Divide (da,db) by SCMFSA_2:34;
hence  not IncAddr (i,n) destroys a by A1, COMPOS_0:4; ::_thesis: verum
end;
suppose InsCode i = 6 ; ::_thesis: not IncAddr (i,n) destroys a
then consider loc being Element of NAT  such that
A2: i = goto loc by SCMFSA_2:35;
 IncAddr (i,n) = goto (loc + n) by A2, SCMFSA_4:1;
hence  not IncAddr (i,n) destroys a by SCMFSA7B:11; ::_thesis: verum
end;
suppose InsCode i = 7 ; ::_thesis: not IncAddr (i,n) destroys a
then consider loc being Element of NAT , da being Int-Location such that
A3: i = da =0_goto loc by SCMFSA_2:36;
 IncAddr (i,n) = da =0_goto (loc + n) by A3, SCMFSA_4:2;
hence  not IncAddr (i,n) destroys a by SCMFSA7B:12; ::_thesis: verum
end;
suppose InsCode i = 8 ; ::_thesis: not IncAddr (i,n) destroys a
then consider loc being Element of NAT , da being Int-Location such that
A4: i = da >0_goto loc by SCMFSA_2:37;
 IncAddr (i,n) = da >0_goto (loc + n) by A4, SCMFSA_4:3;
hence  not IncAddr (i,n) destroys a by SCMFSA7B:13; ::_thesis: verum
end;
suppose InsCode i = 9 ; ::_thesis: not IncAddr (i,n) destroys a
then  ex db, da being Int-Location ex g being FinSeq-Location st i = da := (g,db) by SCMFSA_2:38;
hence  not IncAddr (i,n) destroys a by A1, COMPOS_0:4; ::_thesis: verum
end;
suppose InsCode i = 10 ; ::_thesis: not IncAddr (i,n) destroys a
then  ex db, da being Int-Location ex g being FinSeq-Location st i = (g,db) := da by SCMFSA_2:39;
hence  not IncAddr (i,n) destroys a by A1, COMPOS_0:4; ::_thesis: verum
end;
suppose InsCode i = 11 ; ::_thesis: not IncAddr (i,n) destroys a
then  ex da being Int-Location ex g being FinSeq-Location st i = da :=len g by SCMFSA_2:40;
hence  not IncAddr (i,n) destroys a by A1, COMPOS_0:4; ::_thesis: verum
end;
suppose InsCode i = 12 ; ::_thesis: not IncAddr (i,n) destroys a
then  ex da being Int-Location ex g being FinSeq-Location st i = g :=<0,...,0> da by SCMFSA_2:41;
hence  not IncAddr (i,n) destroys a by A1, COMPOS_0:4; ::_thesis: verum
end;
end;
end;

theorem Th9: :: SCMFSA8A:9
for P being preProgram of SCM+FSA
for n being Element of NAT
for a being Int-Location st not P destroys a holds
not Reloc (P,n) destroys a
proof
let I be preProgram of SCM+FSA; ::_thesis: for n being Element of NAT
for a being Int-Location st not I destroys a holds
not Reloc (I,n) destroys a
let n be Element of NAT ; ::_thesis: for a being Int-Location st not I destroys a holds
not Reloc (I,n) destroys a
let a be Int-Location; ::_thesis: ( not I destroys a implies not Reloc (I,n) destroys a )
A1: dom (IncAddr (I,n)) = dom I by COMPOS_1:def_21;
A2: dom (Shift ((IncAddr (I,n)),n)) =  {  (m + n) where m is Element of NAT : m in dom (IncAddr (I,n))  }  by VALUED_1:def_12;
assume A3: not I destroys a ; ::_thesis: not Reloc (I,n) destroys a
now__::_thesis:_for_i_being_Instruction_of_SCM+FSA_st_i_in_rng_(Reloc_(I,n))_holds_
not_i_destroys_a
let i be Instruction of SCM+FSA; ::_thesis: ( i in rng (Reloc (I,n)) implies not i destroys a )
assume  i in rng (Reloc (I,n)) ; ::_thesis: not i destroys a
then consider x being set  such that
A4: x in dom (Shift ((IncAddr (I,n)),n)) and
A5: i = (Shift ((IncAddr (I,n)),n)) . x by FUNCT_1:def_3;
consider m being Element of NAT  such that
A6: x = m + n and
A7: m in dom (IncAddr (I,n)) by A2, A4;
A8: I . m in rng I by A1, A7, FUNCT_1:def_3;
 rng I c= the InstructionsF of SCM+FSA by RELAT_1:def_19;
then reconsider ii = I . m as Instruction of SCM+FSA by A8;
A9: not ii destroys a by A3, A8, SCMFSA7B:def_4;
i = (IncAddr (I,n)) . m by A5, A6, A7, VALUED_1:def_12
.= IncAddr ((I /. m),n) by A1, A7, COMPOS_1:def_21
.= IncAddr (ii,n) by A1, A7, PARTFUN1:def_6 ;
hence  not i destroys a by A9, Th8; ::_thesis: verum
end;
hence  not Reloc (I,n) destroys a by SCMFSA7B:def_4; ::_thesis: verum
end;

theorem Th10: :: SCMFSA8A:10
for P being good preProgram of SCM+FSA
for n being Element of NAT holds Reloc (P,n) is good
proof
let I be good preProgram of SCM+FSA; ::_thesis: for n being Element of NAT holds Reloc (I,n) is good
let n be Element of NAT ; ::_thesis: Reloc (I,n) is good
 not I destroys intloc 0 by SCMFSA7B:def_5;
then  not Reloc (I,n) destroys intloc 0 by Th9;
hence  Reloc (I,n) is good by SCMFSA7B:def_5; ::_thesis: verum
end;

theorem Th11: :: SCMFSA8A:11
for I, J being preProgram of SCM+FSA
for a being Int-Location st not I destroys a & not J destroys a holds
not I +* J destroys a
proof
let I, J be preProgram of SCM+FSA; ::_thesis: for a being Int-Location st not I destroys a & not J destroys a holds
not I +* J destroys a
let a be Int-Location; ::_thesis: ( not I destroys a & not J destroys a implies not I +* J destroys a )
assume A1: not I destroys a ; ::_thesis: ( J destroys a or not I +* J destroys a )
assume A2: not J destroys a ; ::_thesis: not I +* J destroys a
now__::_thesis:_for_i_being_Instruction_of_SCM+FSA_st_i_in_rng_(I_+*_J)_holds_
not_i_destroys_a
let i be Instruction of SCM+FSA; ::_thesis: ( i in rng (I +* J) implies not b1 destroys a )
A3: rng (I +* J) c= (rng I) \/ (rng J) by FUNCT_4:17;
assume A4: i in rng (I +* J) ; ::_thesis: not b1 destroys a
percases ( i in rng I or i in rng J ) by A4, A3, XBOOLE_0:def_3;
suppose i in rng I ; ::_thesis: not b1 destroys a
hence  not i destroys a by A1, SCMFSA7B:def_4; ::_thesis: verum
end;
suppose i in rng J ; ::_thesis: not b1 destroys a
hence  not i destroys a by A2, SCMFSA7B:def_4; ::_thesis: verum
end;
end;
end;
hence  not I +* J destroys a by SCMFSA7B:def_4; ::_thesis: verum
end;

theorem Th12: :: SCMFSA8A:12
for I, J being good preProgram of SCM+FSA holds I +* J is good
proof
let I, J be good preProgram of SCM+FSA; ::_thesis: I +* J is good
 ( not I destroys intloc 0 & not J destroys intloc 0 ) by SCMFSA7B:def_5;
then  not I +* J destroys intloc 0 by Th11;
hence  I +* J is good by SCMFSA7B:def_5; ::_thesis: verum
end;

theorem Th13: :: SCMFSA8A:13
for I being preProgram of SCM+FSA
for l being Element of NAT
for a being Int-Location st not I destroys a holds
not Directed (I,l) destroys a
proof
let I be preProgram of SCM+FSA; ::_thesis: for l being Element of NAT
for a being Int-Location st not I destroys a holds
not Directed (I,l) destroys a
let l be Element of NAT ; ::_thesis: for a being Int-Location st not I destroys a holds
not Directed (I,l) destroys a
let a be Int-Location; ::_thesis: ( not I destroys a implies not Directed (I,l) destroys a )
assume A1: not I destroys a ; ::_thesis: not Directed (I,l) destroys a
now__::_thesis:_for_i_being_Instruction_of_SCM+FSA_st_i_in_rng_(Directed_(I,l))_holds_
not_i_destroys_a
let i be Instruction of SCM+FSA; ::_thesis: ( i in rng (Directed (I,l)) implies not b1 destroys a )
A2: dom (Directed (I,l)) = dom I by FUNCT_4:99;
assume  i in rng (Directed (I,l)) ; ::_thesis: not b1 destroys a
then consider x being set  such that
A3: x in dom (Directed (I,l)) and
A4: i = (Directed (I,l)) . x by FUNCT_1:def_3;
percases ( I . x <> halt SCM+FSA or I . x = halt SCM+FSA ) ;
suppose I . x <> halt SCM+FSA ; ::_thesis: not b1 destroys a
then  i = I . x by A4, FUNCT_4:105;
then  i in rng I by A3, A2, FUNCT_1:def_3;
hence  not i destroys a by A1, SCMFSA7B:def_4; ::_thesis: verum
end;
suppose I . x = halt SCM+FSA ; ::_thesis: not b1 destroys a
then  i = goto l by A3, A4, A2, FUNCT_4:106;
hence  not i destroys a by SCMFSA7B:11; ::_thesis: verum
end;
end;
end;
hence  not Directed (I,l) destroys a by SCMFSA7B:def_4; ::_thesis: verum
end;

registration
let I be good preProgram of SCM+FSA;
let l be Element of NAT ;
cluster Directed (I,l) ->  good ;
correctness
coherence
Directed (I,l) is good ;
proof
 not I destroys intloc 0 by SCMFSA7B:def_5;
then  not Directed (I,l) destroys intloc 0 by Th13;
hence  Directed (I,l) is good by SCMFSA7B:def_5; ::_thesis: verum
end;
end;

registration
let I be good Program of SCM+FSA;
cluster Directed I ->  good ;
correctness
coherence
Directed I is good ;
;
end;

registration
let I be Program of SCM+FSA;
let l be Element of NAT ;
cluster Directed (I,l) ->  initial ;
correctness
coherence
Directed (I,l) is initial ;
proof
now__::_thesis:_for_m,_n_being_Nat_st_n_in_dom_(Directed_(I,l))_&_m_<_n_holds_
m_in_dom_(Directed_(I,l))
let m, n be Nat; ::_thesis: ( n in dom (Directed (I,l)) & m < n implies m in dom (Directed (I,l)) )
assume  n in dom (Directed (I,l)) ; ::_thesis: ( m < n implies m in dom (Directed (I,l)) )
then A1: n in dom I by FUNCT_4:99;
assume  m < n ; ::_thesis: m in dom (Directed (I,l))
then  m in dom I by A1, AFINSQ_1:def_12;
hence  m in dom (Directed (I,l)) by FUNCT_4:99; ::_thesis: verum
end;
hence  Directed (I,l) is initial by AFINSQ_1:def_12; ::_thesis: verum
end;
end;

registration
let I, J be good Program of SCM+FSA;
clusterI ";" J ->  good ;
coherence
 I ";" J is good
proof
 Reloc (J,(card I)) is good by Th10;
hence  I ";" J is good by Th12; ::_thesis: verum
end;
end;

Lm1:  for l being Element of NAT holds
( dom (0 .--> (goto l)) = {0} & 0 in dom (0 .--> (goto l)) & (0 .--> (goto l)) . 0 = goto l & card (0 .--> (goto l)) = 1 & not halt SCM+FSA in rng (0 .--> (goto l)) )
proof
let l be Element of NAT ; ::_thesis: ( dom (0 .--> (goto l)) = {0} & 0 in dom (0 .--> (goto l)) & (0 .--> (goto l)) . 0 = goto l & card (0 .--> (goto l)) = 1 & not halt SCM+FSA in rng (0 .--> (goto l)) )
thus  dom (0 .--> (goto l)) = {0} by FUNCOP_1:13; ::_thesis: ( 0 in dom (0 .--> (goto l)) & (0 .--> (goto l)) . 0 = goto l & card (0 .--> (goto l)) = 1 & not halt SCM+FSA in rng (0 .--> (goto l)) )
hence  0 in dom (0 .--> (goto l)) by TARSKI:def_1; ::_thesis: ( (0 .--> (goto l)) . 0 = goto l & card (0 .--> (goto l)) = 1 & not halt SCM+FSA in rng (0 .--> (goto l)) )
thus  (0 .--> (goto l)) . 0 = goto l by FUNCOP_1:72; ::_thesis: ( card (0 .--> (goto l)) = 1 & not halt SCM+FSA in rng (0 .--> (goto l)) )
thus  card (0 .--> (goto l)) = card <%(goto l)%> by AFINSQ_1:def_1
.= 1 by AFINSQ_1:34 ; ::_thesis: not halt SCM+FSA in rng (0 .--> (goto l))
now__::_thesis:_not_halt_SCM+FSA_in_rng_(0_.-->_(goto_l))
A1: rng (0 .--> (goto l)) = {(goto l)} by FUNCOP_1:8;
assume  halt SCM+FSA in rng (0 .--> (goto l)) ; ::_thesis: contradiction
hence  contradiction by A1, TARSKI:def_1; ::_thesis: verum
end;
hence  not halt SCM+FSA in rng (0 .--> (goto l)) ; ::_thesis: verum
end;

definition
let l be Element of NAT ;
func Goto l ->  Program of SCM+FSA equals :: SCMFSA8A:def 1
0 .--> (goto l);
coherence
 0 .--> (goto l) is Program of SCM+FSA
proof
 0 .--> (goto l) = <%(goto l)%> by AFINSQ_1:def_1;
then reconsider I = 0 .--> (goto l) as Program of SCM+FSA ;
reconsider I = I as Program of SCM+FSA ;
now__::_thesis:_for_x_being_Instruction_of_SCM+FSA_st_x_in_rng_(0_.-->_(goto_l))_holds_
not_x_destroys_intloc_0
let x be Instruction of SCM+FSA; ::_thesis: ( x in rng (0 .--> (goto l)) implies not x destroys intloc 0 )
A1: rng (0 .--> (goto l)) = {(goto l)} by FUNCOP_1:8;
assume  x in rng (0 .--> (goto l)) ; ::_thesis: not x destroys intloc 0
then  x = goto l by A1, TARSKI:def_1;
hence  not x destroys intloc 0 by SCMFSA7B:11; ::_thesis: verum
end;
then  not I destroys intloc 0 by SCMFSA7B:def_4;
hence  0 .--> (goto l) is Program of SCM+FSA ; ::_thesis: verum
end;
end;

:: deftheorem  defines Goto SCMFSA8A:def_1_:_
 for l being Element of NAT holds Goto l = 0 .--> (goto l);

registration
let l be Element of NAT ;
cluster Goto l ->  halt-free good ;
coherence
 ( Goto l is halt-free & Goto l is good )
proof
 0 .--> (goto l) = <%(goto l)%> by AFINSQ_1:def_1;
then reconsider I = 0 .--> (goto l) as Program of SCM+FSA ;
 not halt SCM+FSA in rng I by Lm1;
hence  Goto l is halt-free by COMPOS_1:def_11; ::_thesis: Goto l is good
reconsider I = I as Program of SCM+FSA ;
now__::_thesis:_for_x_being_Instruction_of_SCM+FSA_st_x_in_rng_(0_.-->_(goto_l))_holds_
not_x_destroys_intloc_0
let x be Instruction of SCM+FSA; ::_thesis: ( x in rng (0 .--> (goto l)) implies not x destroys intloc 0 )
A1: rng (0 .--> (goto l)) = {(goto l)} by FUNCOP_1:8;
assume  x in rng (0 .--> (goto l)) ; ::_thesis: not x destroys intloc 0
then  x = goto l by A1, TARSKI:def_1;
hence  not x destroys intloc 0 by SCMFSA7B:11; ::_thesis: verum
end;
then  not I destroys intloc 0 by SCMFSA7B:def_4;
hence  Goto l is good by SCMFSA7B:def_5; ::_thesis: verum
end;
end;

registration
cluster non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like T-Sequence-like V28() initial halt-free good for set ;
existence
 ex b1 being Program of SCM+FSA st
( b1 is halt-free & b1 is good )
proof
take  Goto 0 ; ::_thesis: ( Goto 0 is halt-free & Goto 0 is good )
thus  ( Goto 0 is halt-free & Goto 0 is good ) ; ::_thesis: verum
end;
end;

definition
let s be State of SCM+FSA;
let P be Instruction-Sequence of SCM+FSA;
let I be Program of SCM+FSA;
predI is_pseudo-closed_on s,P means :Def2: :: SCMFSA8A:def 2
 ex k being Element of NAT st
( IC (Comput ((P +* I),(Initialize s),k)) = card I & ( for n being Element of NAT st n < k holds
IC (Comput ((P +* I),(Initialize s),n)) in dom I ) );
end;

:: deftheorem Def2 defines is_pseudo-closed_on SCMFSA8A:def_2_:_
 for s being State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA
for I being Program of SCM+FSA holds
( I is_pseudo-closed_on s,P iff ex k being Element of NAT st
( IC (Comput ((P +* I),(Initialize s),k)) = card I & ( for n being Element of NAT st n < k holds
IC (Comput ((P +* I),(Initialize s),n)) in dom I ) ) );

registration
cluster with_explicit_jumps IC-relocable sequential for Element of the InstructionsF of SCM+FSA;
existence
 ex b1 being Instruction of SCM+FSA st b1 is sequential
proof
take  (intloc 0) := (intloc 0) ; ::_thesis: (intloc 0) := (intloc 0) is sequential
thus  (intloc 0) := (intloc 0) is sequential ; ::_thesis: verum
end;
end;

definition
canceled;
let s be State of SCM+FSA;
let P be Instruction-Sequence of SCM+FSA;
let I be Program of SCM+FSA;
assume X1: I is_pseudo-closed_on s,P ;
func pseudo-LifeSpan (s,P,I) ->  Element of NAT  means :Def4: :: SCMFSA8A:def 4
( IC (Comput ((P +* I),(Initialize s),it)) = card I & ( for n being Element of NAT st not IC (Comput ((P +* I),(Initialize s),n)) in dom I holds
it <= n ) );
existence
 ex b1 being Element of NAT st
( IC (Comput ((P +* I),(Initialize s),b1)) = card I & ( for n being Element of NAT st not IC (Comput ((P +* I),(Initialize s),n)) in dom I holds
b1 <= n ) )
proof
consider k being Element of NAT  such that
A1: ( IC (Comput ((P +* I),(Initialize s),k)) = card I & ( for n being Element of NAT st n < k holds
IC (Comput ((P +* I),(Initialize s),n)) in dom I ) ) by X1, Def2;
take  k ; ::_thesis: ( IC (Comput ((P +* I),(Initialize s),k)) = card I & ( for n being Element of NAT st not IC (Comput ((P +* I),(Initialize s),n)) in dom I holds
k <= n ) )
thus  ( IC (Comput ((P +* I),(Initialize s),k)) = card I & ( for n being Element of NAT st not IC (Comput ((P +* I),(Initialize s),n)) in dom I holds
k <= n ) ) by A1; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Element of NAT st IC (Comput ((P +* I),(Initialize s),b1)) = card I & ( for n being Element of NAT st not IC (Comput ((P +* I),(Initialize s),n)) in dom I holds
b1 <= n ) & IC (Comput ((P +* I),(Initialize s),b2)) = card I & ( for n being Element of NAT st not IC (Comput ((P +* I),(Initialize s),n)) in dom I holds
b2 <= n ) holds
b1 = b2
proof
reconsider II = I as initial preProgram of SCM+FSA ;
let k1, k2 be Element of NAT ; ::_thesis: ( IC (Comput ((P +* I),(Initialize s),k1)) = card I & ( for n being Element of NAT st not IC (Comput ((P +* I),(Initialize s),n)) in dom I holds
k1 <= n ) & IC (Comput ((P +* I),(Initialize s),k2)) = card I & ( for n being Element of NAT st not IC (Comput ((P +* I),(Initialize s),n)) in dom I holds
k2 <= n ) implies k1 = k2 )
assume that
A2: IC (Comput ((P +* I),(Initialize s),k1)) = card I and
A3: ( ( for n being Element of NAT st not IC (Comput ((P +* I),(Initialize s),n)) in dom I holds
k1 <= n ) & IC (Comput ((P +* I),(Initialize s),k2)) = card I ) and
A4: for n being Element of NAT st not IC (Comput ((P +* I),(Initialize s),n)) in dom I holds
k2 <= n ; ::_thesis: k1 = k2
A5: now__::_thesis:_not_k2_<_k1
assume  k2 < k1 ; ::_thesis: contradiction
then  card II in dom II by A3;
hence  contradiction ; ::_thesis: verum
end;
now__::_thesis:_not_k1_<_k2
assume  k1 < k2 ; ::_thesis: contradiction
then  card II in dom II by A2, A4;
hence  contradiction ; ::_thesis: verum
end;
hence  k1 = k2 by A5, XXREAL_0:1; ::_thesis: verum
end;
end;

:: deftheorem  SCMFSA8A:def_3_:_
canceled;

:: deftheorem Def4 defines pseudo-LifeSpan SCMFSA8A:def_4_:_
 for s being State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA
for I being Program of SCM+FSA st I is_pseudo-closed_on s,P holds
for b4 being Element of NAT holds
( b4 = pseudo-LifeSpan (s,P,I) iff ( IC (Comput ((P +* I),(Initialize s),b4)) = card I & ( for n being Element of NAT st not IC (Comput ((P +* I),(Initialize s),n)) in dom I holds
b4 <= n ) ) );

theorem Th14: :: SCMFSA8A:14
for I, J being Program of SCM+FSA
for x being set st x in dom I holds
(I ";" J) . x = (Directed I) . x
proof
let I, J be Program of SCM+FSA; ::_thesis: for x being set st x in dom I holds
(I ";" J) . x = (Directed I) . x
let x be set ; ::_thesis: ( x in dom I implies (I ";" J) . x = (Directed I) . x )
assume  x in dom I ; ::_thesis: (I ";" J) . x = (Directed I) . x
then A1: x in dom (Directed I) by FUNCT_4:99;
 Directed I c= I ";" J by SCMFSA6A:16;
hence  (I ";" J) . x = (Directed I) . x by A1, GRFUNC_1:2; ::_thesis: verum
end;

theorem :: SCMFSA8A:15
for l being Element of NAT holds card (Goto l) = 1 by Lm1;

theorem :: SCMFSA8A:16
for P being preProgram of SCM+FSA
for x being set st x in dom P holds
( ( P . x = halt SCM+FSA implies (Directed P) . x = goto (card P) ) & ( P . x <> halt SCM+FSA implies (Directed P) . x = P . x ) ) by FUNCT_4:105, FUNCT_4:106;

theorem Th17: :: SCMFSA8A:17
for s being State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA
for I being Program of SCM+FSA st I is_pseudo-closed_on s,P holds
for n being Element of NAT st n < pseudo-LifeSpan (s,P,I) holds
( IC (Comput ((P +* I),(Initialize s),n)) in dom I & CurInstr ((P +* I),(Comput ((P +* I),(Initialize s),n))) <> halt SCM+FSA )
proof
let s be State of SCM+FSA; ::_thesis: for P being Instruction-Sequence of SCM+FSA
for I being Program of SCM+FSA st I is_pseudo-closed_on s,P holds
for n being Element of NAT st n < pseudo-LifeSpan (s,P,I) holds
( IC (Comput ((P +* I),(Initialize s),n)) in dom I & CurInstr ((P +* I),(Comput ((P +* I),(Initialize s),n))) <> halt SCM+FSA )
let P be Instruction-Sequence of SCM+FSA; ::_thesis: for I being Program of SCM+FSA st I is_pseudo-closed_on s,P holds
for n being Element of NAT st n < pseudo-LifeSpan (s,P,I) holds
( IC (Comput ((P +* I),(Initialize s),n)) in dom I & CurInstr ((P +* I),(Comput ((P +* I),(Initialize s),n))) <> halt SCM+FSA )
let I be Program of SCM+FSA; ::_thesis: ( I is_pseudo-closed_on s,P implies for n being Element of NAT st n < pseudo-LifeSpan (s,P,I) holds
( IC (Comput ((P +* I),(Initialize s),n)) in dom I & CurInstr ((P +* I),(Comput ((P +* I),(Initialize s),n))) <> halt SCM+FSA ) )
set k = pseudo-LifeSpan (s,P,I);
assume A1: I is_pseudo-closed_on s,P ; ::_thesis: for n being Element of NAT st n < pseudo-LifeSpan (s,P,I) holds
( IC (Comput ((P +* I),(Initialize s),n)) in dom I & CurInstr ((P +* I),(Comput ((P +* I),(Initialize s),n))) <> halt SCM+FSA )
then A2: IC (Comput ((P +* I),(Initialize s),(pseudo-LifeSpan (s,P,I)))) = card I by Def4;
hereby  ::_thesis: verum
let n be Element of NAT ; ::_thesis: ( n < pseudo-LifeSpan (s,P,I) implies ( IC (Comput ((P +* I),(Initialize s),n)) in dom I & not CurInstr ((P +* I),(Comput ((P +* I),(Initialize s),n))) = halt SCM+FSA ) )
assume A3: n < pseudo-LifeSpan (s,P,I) ; ::_thesis: ( IC (Comput ((P +* I),(Initialize s),n)) in dom I & not CurInstr ((P +* I),(Comput ((P +* I),(Initialize s),n))) = halt SCM+FSA )
hence A4: IC (Comput ((P +* I),(Initialize s),n)) in dom I by A1, Def4; ::_thesis: not CurInstr ((P +* I),(Comput ((P +* I),(Initialize s),n))) = halt SCM+FSA
assume  CurInstr ((P +* I),(Comput ((P +* I),(Initialize s),n))) = halt SCM+FSA ; ::_thesis: contradiction
then  IC (Comput ((P +* I),(Initialize s),(pseudo-LifeSpan (s,P,I)))) = IC (Comput ((P +* I),(Initialize s),n)) by A3, EXTPRO_1:5;
hence  contradiction by A2, A4; ::_thesis: verum
end;
end;

theorem Th18: :: SCMFSA8A:18
for s being 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 Element of NAT st k <= pseudo-LifeSpan (s,P,I) holds
Comput ((P +* I),(Initialize s),k) = Comput ((P +* (I ";" J)),(Initialize s),k)
proof
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 Element of 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 Element of 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 Element of 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 ; ::_thesis: for k being Element of 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_Element_of_NAT_st_S1[k]_holds_
S1[k_+_1]
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A5: S1[k] ; ::_thesis: S1[k + 1]
thus  S1[k + 1] ::_thesis: verum
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, Th17;
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, Th17;
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;
end;
A16: S1[ 0 ] ;
thus  for k being Element of NAT holds S1[k] from NAT_1:sch_1(A16, A4); ::_thesis: verum
end;

theorem Th19: :: SCMFSA8A:19
for I being preProgram of SCM+FSA
for l being Element of NAT holds card (Directed (I,l)) = card I
proof
let I be preProgram of SCM+FSA; ::_thesis: for l being Element of NAT holds card (Directed (I,l)) = card I
let l be Element of NAT ; ::_thesis: card (Directed (I,l)) = card I
thus  card (Directed (I,l)) = card (dom (Directed (I,l))) by CARD_1:62
.= card (dom I) by FUNCT_4:99
.= card I by CARD_1:62 ; ::_thesis: verum
end;

theorem :: SCMFSA8A:20
for I being Program of SCM+FSA holds card (Directed I) = card I by Th19;

theorem Th21: :: SCMFSA8A:21
for s being State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA
for I being Program of SCM+FSA st I is_closed_on s,P & I is_halting_on s,P holds
for k being Element of NAT st k <= LifeSpan ((P +* I),(Initialize s)) holds
( Comput ((P +* I),(Initialize s),k) = Comput ((P +* (Directed I)),(Initialize s),k) & CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(Initialize s),k))) <> halt SCM+FSA )
proof
let s be State of SCM+FSA; ::_thesis: for P being Instruction-Sequence of SCM+FSA
for I being Program of SCM+FSA st I is_closed_on s,P & I is_halting_on s,P holds
for k being Element of NAT st k <= LifeSpan ((P +* I),(Initialize s)) holds
( Comput ((P +* I),(Initialize s),k) = Comput ((P +* (Directed I)),(Initialize s),k) & CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(Initialize s),k))) <> halt SCM+FSA )
let P be Instruction-Sequence of SCM+FSA; ::_thesis: for I being Program of SCM+FSA st I is_closed_on s,P & I is_halting_on s,P holds
for k being Element of NAT st k <= LifeSpan ((P +* I),(Initialize s)) holds
( Comput ((P +* I),(Initialize s),k) = Comput ((P +* (Directed I)),(Initialize s),k) & CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(Initialize s),k))) <> halt SCM+FSA )
let I be Program of SCM+FSA; ::_thesis: ( I is_closed_on s,P & I is_halting_on s,P implies for k being Element of NAT st k <= LifeSpan ((P +* I),(Initialize s)) holds
( Comput ((P +* I),(Initialize s),k) = Comput ((P +* (Directed I)),(Initialize s),k) & CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(Initialize s),k))) <> halt SCM+FSA ) )
assume that
A1: I is_closed_on s,P and
A2: I is_halting_on s,P ; ::_thesis: for k being Element of NAT st k <= LifeSpan ((P +* I),(Initialize s)) holds
( Comput ((P +* I),(Initialize s),k) = Comput ((P +* (Directed I)),(Initialize s),k) & CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(Initialize s),k))) <> halt SCM+FSA )
A3: dom (P +* (Directed I)) = NAT by PARTFUN1:def_2;
A4: dom (P +* I) = NAT by PARTFUN1:def_2;
set s2 = Initialize s;
set s1 = Initialize s;
defpred S1[ Nat] means ( $1 <= LifeSpan ((P +* I),(Initialize s)) implies ( Comput ((P +* I),(Initialize s),$1) = Comput ((P +* (Directed I)),(Initialize s),$1) & CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(Initialize s),$1))) <> halt SCM+FSA ) );
A5: now__::_thesis:_for_k_being_Element_of_NAT_st_Comput_((P_+*_I),(Initialize_s),k)_=_Comput_((P_+*_(Directed_I)),(Initialize_s),k)_holds_
not_CurInstr_((P_+*_(Directed_I)),(Comput_((P_+*_(Directed_I)),(Initialize_s),k)))_=_halt_SCM+FSA
let k be Element of NAT ; ::_thesis: ( Comput ((P +* I),(Initialize s),k) = Comput ((P +* (Directed I)),(Initialize s),k) implies not CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(Initialize s),k))) = halt SCM+FSA )
 dom (Directed I) = dom I by FUNCT_4:99;
then A6: IC (Comput ((P +* I),(Initialize s),k)) in dom (Directed I) by A1, SCMFSA7B:def_6;
A7: (P +* (Directed I)) /. (IC (Comput ((P +* (Directed I)),(Initialize s),k))) = (P +* (Directed I)) . (IC (Comput ((P +* (Directed I)),(Initialize s),k))) by A3, PARTFUN1:def_6;
A8: Directed I c= P +* (Directed I) by FUNCT_4:25;
assume  Comput ((P +* I),(Initialize s),k) = Comput ((P +* (Directed I)),(Initialize s),k) ; ::_thesis: not CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(Initialize s),k))) = halt SCM+FSA
then  CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(Initialize s),k))) = (P +* (Directed I)) . (IC (Comput ((P +* I),(Initialize s),k))) by A7
.= (Directed I) . (IC (Comput ((P +* I),(Initialize s),k))) by A6, A8, GRFUNC_1:2 ;
then A9: CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(Initialize s),k))) in rng (Directed I) by A6, FUNCT_1:def_3;
assume  CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(Initialize s),k))) = halt SCM+FSA ; ::_thesis: contradiction
hence  contradiction by A9, SCMFSA6A:1; ::_thesis: verum
end;
now__::_thesis:_for_k_being_Element_of_NAT_st_(_k_<=_LifeSpan_((P_+*_I),(Initialize_s))_implies_Comput_((P_+*_I),(Initialize_s),k)_=_Comput_((P_+*_(Directed_I)),(Initialize_s),k)_)_&_k_+_1_<=_LifeSpan_((P_+*_I),(Initialize_s))_holds_
(_Comput_((P_+*_I),(Initialize_s),(k_+_1))_=_Comput_((P_+*_(Directed_I)),(Initialize_s),(k_+_1))_&_CurInstr_((P_+*_(Directed_I)),(Comput_((P_+*_(Directed_I)),(Initialize_s),(k_+_1))))_<>_halt_SCM+FSA_)
A10: P +* I halts_on Initialize s by A2, SCMFSA7B:def_7;
A11: dom I c= dom (Directed I) by FUNCT_4:99;
let k be Element of NAT ; ::_thesis: ( ( k <= LifeSpan ((P +* I),(Initialize s)) implies Comput ((P +* I),(Initialize s),k) = Comput ((P +* (Directed I)),(Initialize s),k) ) & k + 1 <= LifeSpan ((P +* I),(Initialize s)) implies ( Comput ((P +* I),(Initialize s),(k + 1)) = Comput ((P +* (Directed I)),(Initialize s),(k + 1)) & CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(Initialize s),(k + 1)))) <> halt SCM+FSA ) )
assume A12: ( k <= LifeSpan ((P +* I),(Initialize s)) implies Comput ((P +* I),(Initialize s),k) = Comput ((P +* (Directed I)),(Initialize s),k) ) ; ::_thesis: ( k + 1 <= LifeSpan ((P +* I),(Initialize s)) implies ( Comput ((P +* I),(Initialize s),(k + 1)) = Comput ((P +* (Directed I)),(Initialize s),(k + 1)) & CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(Initialize s),(k + 1)))) <> halt SCM+FSA ) )
A13: Comput ((P +* (Directed I)),(Initialize s),(k + 1)) = Following ((P +* (Directed I)),(Comput ((P +* (Directed I)),(Initialize s),k))) by EXTPRO_1:3
.= Exec ((CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(Initialize s),k)))),(Comput ((P +* (Directed I)),(Initialize s),k))) ;
A14: IC (Comput ((P +* I),(Initialize s),k)) in dom I by A1, SCMFSA7B:def_6;
A15: I c= P +* I by FUNCT_4:25;
A16: CurInstr ((P +* I),(Comput ((P +* I),(Initialize s),k))) = (P +* I) . (IC (Comput ((P +* I),(Initialize s),k))) by A4, PARTFUN1:def_6
.= I . (IC (Comput ((P +* I),(Initialize s),k))) by A14, A15, GRFUNC_1:2 ;
A17: k + 0 < k + 1 by XREAL_1:6;
A18: (P +* (Directed I)) /. (IC (Comput ((P +* (Directed I)),(Initialize s),k))) = (P +* (Directed I)) . (IC (Comput ((P +* (Directed I)),(Initialize s),k))) by A3, PARTFUN1:def_6;
A19: Directed I c= P +* (Directed I) by FUNCT_4:25;
assume A20: k + 1 <= LifeSpan ((P +* I),(Initialize s)) ; ::_thesis: ( Comput ((P +* I),(Initialize s),(k + 1)) = Comput ((P +* (Directed I)),(Initialize s),(k + 1)) & CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(Initialize s),(k + 1)))) <> halt SCM+FSA )
then  k < LifeSpan ((P +* I),(Initialize s)) by A17, XXREAL_0:2;
then  I . (IC (Comput ((P +* I),(Initialize s),k))) <> halt SCM+FSA by A16, A10, EXTPRO_1:def_15;
then A21: CurInstr ((P +* I),(Comput ((P +* I),(Initialize s),k))) = (Directed I) . (IC (Comput ((P +* I),(Initialize s),k))) by A16, FUNCT_4:105
.= (P +* (Directed I)) . (IC (Comput ((P +* I),(Initialize s),k))) by A14, A11, A19, GRFUNC_1:2
.= CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(Initialize s),k))) by A12, A20, A17, A18, XXREAL_0:2 ;
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))) ;
hence  Comput ((P +* I),(Initialize s),(k + 1)) = Comput ((P +* (Directed I)),(Initialize s),(k + 1)) by A12, A20, A17, A21, A13, XXREAL_0:2; ::_thesis: CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(Initialize s),(k + 1)))) <> halt SCM+FSA
hence  CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(Initialize s),(k + 1)))) <> halt SCM+FSA by A5; ::_thesis: verum
end;
then A22: for k being Element of NAT st S1[k] holds
S1[k + 1] ;
now__::_thesis:_(_0_<=_LifeSpan_((P_+*_I),(Initialize_s))_implies_(_Comput_((P_+*_I),(Initialize_s),0)_=_Comput_((P_+*_(Directed_I)),(Initialize_s),0)_&_CurInstr_((P_+*_(Directed_I)),(Comput_((P_+*_(Directed_I)),(Initialize_s),0)))_<>_halt_SCM+FSA_)_)
assume  0 <= LifeSpan ((P +* I),(Initialize s)) ; ::_thesis: ( Comput ((P +* I),(Initialize s),0) = Comput ((P +* (Directed I)),(Initialize s),0) & CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(Initialize s),0))) <> halt SCM+FSA )
thus  Comput ((P +* I),(Initialize s),0) = Comput ((P +* (Directed I)),(Initialize s),0) ; ::_thesis: CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(Initialize s),0))) <> halt SCM+FSA
hence  CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(Initialize s),0))) <> halt SCM+FSA by A5; ::_thesis: verum
end;
then A23: S1[ 0 ] ;
thus  for k being Element of NAT holds S1[k] from NAT_1:sch_1(A23, A22); ::_thesis: verum
end;

theorem Th22: :: SCMFSA8A:22
for s being State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA
for I being Program of SCM+FSA st I is_closed_on s,P & I is_halting_on s,P holds
( IC (Comput ((P +* (Directed I)),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) = card I & DataPart (Comput ((P +* I),(Initialize s),(LifeSpan ((P +* I),(Initialize s))))) = DataPart (Comput ((P +* (Directed I)),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) )
proof
let s be State of SCM+FSA; ::_thesis: for P being Instruction-Sequence of SCM+FSA
for I being Program of SCM+FSA st I is_closed_on s,P & I is_halting_on s,P holds
( IC (Comput ((P +* (Directed I)),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) = card I & DataPart (Comput ((P +* I),(Initialize s),(LifeSpan ((P +* I),(Initialize s))))) = DataPart (Comput ((P +* (Directed I)),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) )
let P be Instruction-Sequence of SCM+FSA; ::_thesis: for I being Program of SCM+FSA st I is_closed_on s,P & I is_halting_on s,P holds
( IC (Comput ((P +* (Directed I)),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) = card I & DataPart (Comput ((P +* I),(Initialize s),(LifeSpan ((P +* I),(Initialize s))))) = DataPart (Comput ((P +* (Directed I)),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) )
let I be Program of SCM+FSA; ::_thesis: ( I is_closed_on s,P & I is_halting_on s,P implies ( IC (Comput ((P +* (Directed I)),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) = card I & DataPart (Comput ((P +* I),(Initialize s),(LifeSpan ((P +* I),(Initialize s))))) = DataPart (Comput ((P +* (Directed I)),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) ) )
set s1 = Initialize s;
set s2 = Initialize s;
set m1 = LifeSpan ((P +* I),(Initialize s));
A1: dom (P +* I) = NAT by PARTFUN1:def_2;
A2: dom (P +* (Directed I)) = NAT by PARTFUN1:def_2;
assume that
A3: I is_closed_on s,P and
A4: I is_halting_on s,P ; ::_thesis: ( IC (Comput ((P +* (Directed I)),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) = card I & DataPart (Comput ((P +* I),(Initialize s),(LifeSpan ((P +* I),(Initialize s))))) = DataPart (Comput ((P +* (Directed I)),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) )
A5: P +* I halts_on Initialize s by A4, SCMFSA7B:def_7;
set l1 = IC (Comput ((P +* I),(Initialize s),(LifeSpan ((P +* I),(Initialize s)))));
A6: IC (Comput ((P +* I),(Initialize s),(LifeSpan ((P +* I),(Initialize s))))) in dom I by A3, SCMFSA7B:def_6;
A7: Comput ((P +* I),(Initialize s),(LifeSpan ((P +* I),(Initialize s)))) = Comput ((P +* (Directed I)),(Initialize s),(LifeSpan ((P +* I),(Initialize s)))) by A3, A4, Th21;
then  IC (Comput ((P +* (Directed I)),(Initialize s),(LifeSpan ((P +* I),(Initialize s))))) in dom I by A6;
then A8: IC (Comput ((P +* (Directed I)),(Initialize s),(LifeSpan ((P +* I),(Initialize s))))) in dom (Directed I) by FUNCT_4:99;
 I c= P +* I by FUNCT_4:25;
then A9: I . (IC (Comput ((P +* I),(Initialize s),(LifeSpan ((P +* I),(Initialize s)))))) = (P +* I) . (IC (Comput ((P +* I),(Initialize s),(LifeSpan ((P +* I),(Initialize s)))))) by A6, GRFUNC_1:2
.= CurInstr ((P +* I),(Comput ((P +* I),(Initialize s),(LifeSpan ((P +* I),(Initialize s)))))) by A1, PARTFUN1:def_6
.= halt SCM+FSA by A5, EXTPRO_1:def_15 ;
 IC (Comput ((P +* I),(Initialize s),(LifeSpan ((P +* I),(Initialize s))))) = IC (Comput ((P +* (Directed I)),(Initialize s),(LifeSpan ((P +* I),(Initialize s))))) by A7;
then A10: (P +* (Directed I)) . (IC (Comput ((P +* I),(Initialize s),(LifeSpan ((P +* I),(Initialize s)))))) = (Directed I) . (IC (Comput ((P +* I),(Initialize s),(LifeSpan ((P +* I),(Initialize s)))))) by A8, FUNCT_4:13
.= goto (card I) by A6, A9, FUNCT_4:106 ;
A11: CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(Initialize s),(LifeSpan ((P +* I),(Initialize s)))))) = (P +* (Directed I)) . (IC (Comput ((P +* (Directed I)),(Initialize s),(LifeSpan ((P +* I),(Initialize s)))))) by A2, PARTFUN1:def_6
.= goto (card I) by A10, A7 ;
A12: Comput ((P +* (Directed I)),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1)) = Following ((P +* (Directed I)),(Comput ((P +* (Directed I)),(Initialize s),(LifeSpan ((P +* I),(Initialize s)))))) by EXTPRO_1:3
.= Exec ((goto (card I)),(Comput ((P +* (Directed I)),(Initialize s),(LifeSpan ((P +* I),(Initialize s)))))) by A11 ;
hence  IC (Comput ((P +* (Directed I)),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) = card I by SCMFSA_2:69; ::_thesis: DataPart (Comput ((P +* I),(Initialize s),(LifeSpan ((P +* I),(Initialize s))))) = DataPart (Comput ((P +* (Directed I)),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1)))
A13: ( ( for a being Int-Location holds (Comput ((P +* (Directed I)),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) . a = (Comput ((P +* (Directed I)),(Initialize s),(LifeSpan ((P +* I),(Initialize s))))) . a ) & ( for f being FinSeq-Location holds (Comput ((P +* (Directed I)),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) . f = (Comput ((P +* (Directed I)),(Initialize s),(LifeSpan ((P +* I),(Initialize s))))) . f ) ) by A12, SCMFSA_2:69;
 DataPart (Comput ((P +* I),(Initialize s),(LifeSpan ((P +* I),(Initialize s))))) = DataPart (Comput ((P +* (Directed I)),(Initialize s),(LifeSpan ((P +* I),(Initialize s))))) by A7;
hence  DataPart (Comput ((P +* I),(Initialize s),(LifeSpan ((P +* I),(Initialize s))))) = DataPart (Comput ((P +* (Directed I)),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) by A13, SCMFSA_M:2; ::_thesis: verum
end;

Lm2:  for s being State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA
for I being Program of SCM+FSA st I is_closed_on s,P & I is_halting_on s,P holds
( Directed I is_pseudo-closed_on s,P & pseudo-LifeSpan (s,P,(Directed I)) = (LifeSpan ((P +* I),(Initialize s))) + 1 )
proof
let s be State of SCM+FSA; ::_thesis: for P being Instruction-Sequence of SCM+FSA
for I being Program of SCM+FSA st I is_closed_on s,P & I is_halting_on s,P holds
( Directed I is_pseudo-closed_on s,P & pseudo-LifeSpan (s,P,(Directed I)) = (LifeSpan ((P +* I),(Initialize s))) + 1 )
let P be Instruction-Sequence of SCM+FSA; ::_thesis: for I being Program of SCM+FSA st I is_closed_on s,P & I is_halting_on s,P holds
( Directed I is_pseudo-closed_on s,P & pseudo-LifeSpan (s,P,(Directed I)) = (LifeSpan ((P +* I),(Initialize s))) + 1 )
let I be Program of SCM+FSA; ::_thesis: ( I is_closed_on s,P & I is_halting_on s,P implies ( Directed I is_pseudo-closed_on s,P & pseudo-LifeSpan (s,P,(Directed I)) = (LifeSpan ((P +* I),(Initialize s))) + 1 ) )
set s1 = Initialize s;
set s2 = Initialize s;
set m1 = LifeSpan ((P +* I),(Initialize s));
assume that
A1: I is_closed_on s,P and
A2: I is_halting_on s,P ; ::_thesis: ( Directed I is_pseudo-closed_on s,P & pseudo-LifeSpan (s,P,(Directed I)) = (LifeSpan ((P +* I),(Initialize s))) + 1 )
A3: dom I = dom (Directed I) by FUNCT_4:99;
A4: now__::_thesis:_for_n_being_Element_of_NAT_st_n_<_(LifeSpan_((P_+*_I),(Initialize_s)))_+_1_holds_
IC_(Comput_((P_+*_(Directed_I)),(Initialize_s),n))_in_dom_(Directed_I)
let n be Element of NAT ; ::_thesis: ( n < (LifeSpan ((P +* I),(Initialize s))) + 1 implies IC (Comput ((P +* (Directed I)),(Initialize s),n)) in dom (Directed I) )
assume  n < (LifeSpan ((P +* I),(Initialize s))) + 1 ; ::_thesis: IC (Comput ((P +* (Directed I)),(Initialize s),n)) in dom (Directed I)
then  n <= LifeSpan ((P +* I),(Initialize s)) by NAT_1:13;
then  Comput ((P +* I),(Initialize s),n) = Comput ((P +* (Directed I)),(Initialize s),n) by A1, A2, Th21;
then  IC (Comput ((P +* I),(Initialize s),n)) = IC (Comput ((P +* (Directed I)),(Initialize s),n)) ;
hence  IC (Comput ((P +* (Directed I)),(Initialize s),n)) in dom (Directed I) by A1, A3, SCMFSA7B:def_6; ::_thesis: verum
end;
 card I = card (Directed I) by Th19;
then A5: IC (Comput ((P +* (Directed I)),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) = card (Directed I) by A1, A2, Th22;
hence A6: Directed I is_pseudo-closed_on s,P by A4, Def2; ::_thesis: pseudo-LifeSpan (s,P,(Directed I)) = (LifeSpan ((P +* I),(Initialize s))) + 1
 for n being Element of NAT st not IC (Comput ((P +* (Directed I)),(Initialize s),n)) in dom (Directed I) holds
(LifeSpan ((P +* I),(Initialize s))) + 1 <= n by A4;
hence  pseudo-LifeSpan (s,P,(Directed I)) = (LifeSpan ((P +* I),(Initialize s))) + 1 by A5, A6, Def4; ::_thesis: verum
end;

theorem :: SCMFSA8A:23
for s being State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA
for I being Program of SCM+FSA st I is_closed_on s,P & I is_halting_on s,P holds
Directed I is_pseudo-closed_on s,P by Lm2;

theorem :: SCMFSA8A:24
for s being State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA
for I being Program of SCM+FSA st I is_closed_on s,P & I is_halting_on s,P holds
pseudo-LifeSpan (s,P,(Directed I)) = (LifeSpan ((P +* I),(Initialize s))) + 1 by Lm2;

theorem Th25: :: SCMFSA8A:25
for I, J being Program of SCM+FSA holds (Directed I) ";" J = I ";" J
proof
let I, J be Program of SCM+FSA; ::_thesis: (Directed I) ";" J = I ";" J
thus (Directed I) ";" J = (Directed I) +* (Reloc (J,(card (Directed I)))) by SCMFSA6A:22
.= I ";" J by Th19 ; ::_thesis: verum
end;

theorem Th26: :: SCMFSA8A:26
for s being State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA
for I, J being Program of SCM+FSA st I is_closed_on s,P & I is_halting_on s,P holds
( ( for k being Element of NAT st k <= LifeSpan ((P +* I),(Initialize s)) holds
( IC (Comput ((P +* (Directed I)),(Initialize s),k)) = IC (Comput ((P +* (I ";" J)),(Initialize s),k)) & CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(Initialize s),k))) = CurInstr ((P +* (I ";" J)),(Comput ((P +* (I ";" J)),(Initialize s),k))) ) ) & DataPart (Comput ((P +* (Directed I)),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) = DataPart (Comput ((P +* (I ";" J)),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) & IC (Comput ((P +* (Directed I)),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) = IC (Comput ((P +* (I ";" J)),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) )
proof
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_closed_on s,P & I is_halting_on s,P holds
( ( for k being Element of NAT st k <= LifeSpan ((P +* I),(Initialize s)) holds
( IC (Comput ((P +* (Directed I)),(Initialize s),k)) = IC (Comput ((P +* (I ";" J)),(Initialize s),k)) & CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(Initialize s),k))) = CurInstr ((P +* (I ";" J)),(Comput ((P +* (I ";" J)),(Initialize s),k))) ) ) & DataPart (Comput ((P +* (Directed I)),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) = DataPart (Comput ((P +* (I ";" J)),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) & IC (Comput ((P +* (Directed I)),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) = IC (Comput ((P +* (I ";" J)),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) )
let P be Instruction-Sequence of SCM+FSA; ::_thesis: for I, J being Program of SCM+FSA st I is_closed_on s,P & I is_halting_on s,P holds
( ( for k being Element of NAT st k <= LifeSpan ((P +* I),(Initialize s)) holds
( IC (Comput ((P +* (Directed I)),(Initialize s),k)) = IC (Comput ((P +* (I ";" J)),(Initialize s),k)) & CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(Initialize s),k))) = CurInstr ((P +* (I ";" J)),(Comput ((P +* (I ";" J)),(Initialize s),k))) ) ) & DataPart (Comput ((P +* (Directed I)),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) = DataPart (Comput ((P +* (I ";" J)),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) & IC (Comput ((P +* (Directed I)),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) = IC (Comput ((P +* (I ";" J)),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) )
let I, J be Program of SCM+FSA; ::_thesis: ( I is_closed_on s,P & I is_halting_on s,P implies ( ( for k being Element of NAT st k <= LifeSpan ((P +* I),(Initialize s)) holds
( IC (Comput ((P +* (Directed I)),(Initialize s),k)) = IC (Comput ((P +* (I ";" J)),(Initialize s),k)) & CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(Initialize s),k))) = CurInstr ((P +* (I ";" J)),(Comput ((P +* (I ";" J)),(Initialize s),k))) ) ) & DataPart (Comput ((P +* (Directed I)),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) = DataPart (Comput ((P +* (I ";" J)),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) & IC (Comput ((P +* (Directed I)),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) = IC (Comput ((P +* (I ";" J)),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) ) )
A1: dom (P +* (Directed I)) = NAT by PARTFUN1:def_2;
A2: dom (P +* (I ";" J)) = NAT by PARTFUN1:def_2;
assume A3: I is_closed_on s,P ; ::_thesis: ( not I is_halting_on s,P or ( ( for k being Element of NAT st k <= LifeSpan ((P +* I),(Initialize s)) holds
( IC (Comput ((P +* (Directed I)),(Initialize s),k)) = IC (Comput ((P +* (I ";" J)),(Initialize s),k)) & CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(Initialize s),k))) = CurInstr ((P +* (I ";" J)),(Comput ((P +* (I ";" J)),(Initialize s),k))) ) ) & DataPart (Comput ((P +* (Directed I)),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) = DataPart (Comput ((P +* (I ";" J)),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) & IC (Comput ((P +* (Directed I)),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) = IC (Comput ((P +* (I ";" J)),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) ) )
set s2 = Initialize s;
A4: (Directed I) ";" J = I ";" J by Th25;
set s1 = Initialize s;
assume A5: I is_halting_on s,P ; ::_thesis: ( ( for k being Element of NAT st k <= LifeSpan ((P +* I),(Initialize s)) holds
( IC (Comput ((P +* (Directed I)),(Initialize s),k)) = IC (Comput ((P +* (I ";" J)),(Initialize s),k)) & CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(Initialize s),k))) = CurInstr ((P +* (I ";" J)),(Comput ((P +* (I ";" J)),(Initialize s),k))) ) ) & DataPart (Comput ((P +* (Directed I)),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) = DataPart (Comput ((P +* (I ";" J)),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) & IC (Comput ((P +* (Directed I)),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) = IC (Comput ((P +* (I ";" J)),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) )
then A6: (LifeSpan ((P +* I),(Initialize s))) + 1 = pseudo-LifeSpan (s,P,(Directed I)) by A3, Lm2;
A7: Directed I is_pseudo-closed_on s,P by A3, A5, Lm2;
hereby  ::_thesis: ( DataPart (Comput ((P +* (Directed I)),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) = DataPart (Comput ((P +* (I ";" J)),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) & IC (Comput ((P +* (Directed I)),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) = IC (Comput ((P +* (I ";" J)),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) )
let k be Element of NAT ; ::_thesis: ( k <= LifeSpan ((P +* I),(Initialize s)) implies ( IC (Comput ((P +* (Directed I)),(Initialize s),k)) = IC (Comput ((P +* (I ";" J)),(Initialize s),k)) & CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(Initialize s),k))) = CurInstr ((P +* (I ";" J)),(Comput ((P +* (I ";" J)),(Initialize s),k))) ) )
assume  k <= LifeSpan ((P +* I),(Initialize s)) ; ::_thesis: ( IC (Comput ((P +* (Directed I)),(Initialize s),k)) = IC (Comput ((P +* (I ";" J)),(Initialize s),k)) & CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(Initialize s),k))) = CurInstr ((P +* (I ";" J)),(Comput ((P +* (I ";" J)),(Initialize s),k))) )
then A8: k < pseudo-LifeSpan (s,P,(Directed I)) by A6, NAT_1:13;
then A9: IC (Comput ((P +* (Directed I)),(Initialize s),k)) in dom (Directed I) by A7, Def4;
 Comput ((P +* (Directed I)),(Initialize s),k) = Comput ((P +* (I ";" J)),(Initialize s),k) by A4, A3, A5, Lm2, A8, Th18;
hence A10: IC (Comput ((P +* (Directed I)),(Initialize s),k)) = IC (Comput ((P +* (I ";" J)),(Initialize s),k)) ; ::_thesis: CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(Initialize s),k))) = CurInstr ((P +* (I ";" J)),(Comput ((P +* (I ";" J)),(Initialize s),k)))
A11: Directed I c= I ";" J by SCMFSA6A:16;
then A12: dom (Directed I) c= dom (I ";" J) by GRFUNC_1:2;
thus  CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(Initialize s),k))) = (P +* (Directed I)) . (IC (Comput ((P +* (Directed I)),(Initialize s),k))) by A1, PARTFUN1:def_6
.= (Directed I) . (IC (Comput ((P +* (Directed I)),(Initialize s),k))) by A9, FUNCT_4:13
.= (I ";" J) . (IC (Comput ((P +* (Directed I)),(Initialize s),k))) by A9, A11, GRFUNC_1:2
.= (P +* (I ";" J)) . (IC (Comput ((P +* (I ";" J)),(Initialize s),k))) by A10, A12, A9, FUNCT_4:13
.= CurInstr ((P +* (I ";" J)),(Comput ((P +* (I ";" J)),(Initialize s),k))) by A2, PARTFUN1:def_6 ; ::_thesis: verum
end;
 Comput ((P +* (Directed I)),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1)) = Comput ((P +* (I ";" J)),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1)) by A3, A5, A4, A6, Lm2, Th18;
hence  ( DataPart (Comput ((P +* (Directed I)),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) = DataPart (Comput ((P +* (I ";" J)),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) & IC (Comput ((P +* (Directed I)),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) = IC (Comput ((P +* (I ";" J)),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) ) ; ::_thesis: verum
end;

theorem Th27: :: SCMFSA8A:27
for s being State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA
for I, J being Program of SCM+FSA st I is_closed_on Initialized s,P & I is_halting_on Initialized s,P holds
( ( for k being Element of NAT st k <= LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1)))) holds
( IC (Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),k)) = IC (Comput ((P +* (I ";" J)),(s +* (Initialize ((intloc 0) .--> 1))),k)) & CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),k))) = CurInstr ((P +* (I ";" J)),(Comput ((P +* (I ";" J)),(s +* (Initialize ((intloc 0) .--> 1))),k))) ) ) & DataPart (Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1))) = DataPart (Comput ((P +* (I ";" J)),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1))) & IC (Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1))) = IC (Comput ((P +* (I ";" J)),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1))) )
proof
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_closed_on Initialized s,P & I is_halting_on Initialized s,P holds
( ( for k being Element of NAT st k <= LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1)))) holds
( IC (Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),k)) = IC (Comput ((P +* (I ";" J)),(s +* (Initialize ((intloc 0) .--> 1))),k)) & CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),k))) = CurInstr ((P +* (I ";" J)),(Comput ((P +* (I ";" J)),(s +* (Initialize ((intloc 0) .--> 1))),k))) ) ) & DataPart (Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1))) = DataPart (Comput ((P +* (I ";" J)),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1))) & IC (Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1))) = IC (Comput ((P +* (I ";" J)),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1))) )
let P be Instruction-Sequence of SCM+FSA; ::_thesis: for I, J being Program of SCM+FSA st I is_closed_on Initialized s,P & I is_halting_on Initialized s,P holds
( ( for k being Element of NAT st k <= LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1)))) holds
( IC (Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),k)) = IC (Comput ((P +* (I ";" J)),(s +* (Initialize ((intloc 0) .--> 1))),k)) & CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),k))) = CurInstr ((P +* (I ";" J)),(Comput ((P +* (I ";" J)),(s +* (Initialize ((intloc 0) .--> 1))),k))) ) ) & DataPart (Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1))) = DataPart (Comput ((P +* (I ";" J)),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1))) & IC (Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1))) = IC (Comput ((P +* (I ";" J)),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1))) )
let I, J be Program of SCM+FSA; ::_thesis: ( I is_closed_on Initialized s,P & I is_halting_on Initialized s,P implies ( ( for k being Element of NAT st k <= LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1)))) holds
( IC (Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),k)) = IC (Comput ((P +* (I ";" J)),(s +* (Initialize ((intloc 0) .--> 1))),k)) & CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),k))) = CurInstr ((P +* (I ";" J)),(Comput ((P +* (I ";" J)),(s +* (Initialize ((intloc 0) .--> 1))),k))) ) ) & DataPart (Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1))) = DataPart (Comput ((P +* (I ";" J)),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1))) & IC (Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1))) = IC (Comput ((P +* (I ";" J)),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1))) ) )
A1: dom (P +* (I ";" J)) = NAT by PARTFUN1:def_2;
A2: dom (P +* (Directed I)) = NAT by PARTFUN1:def_2;
assume A3: I is_closed_on Initialized s,P ; ::_thesis: ( not I is_halting_on Initialized s,P or ( ( for k being Element of NAT st k <= LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1)))) holds
( IC (Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),k)) = IC (Comput ((P +* (I ";" J)),(s +* (Initialize ((intloc 0) .--> 1))),k)) & CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),k))) = CurInstr ((P +* (I ";" J)),(Comput ((P +* (I ";" J)),(s +* (Initialize ((intloc 0) .--> 1))),k))) ) ) & DataPart (Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1))) = DataPart (Comput ((P +* (I ";" J)),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1))) & IC (Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1))) = IC (Comput ((P +* (I ";" J)),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1))) ) )
set s2 = s +* (Initialize ((intloc 0) .--> 1));
A4: ( s +* (Initialize ((intloc 0) .--> 1)) = Initialize (Initialized s) & s +* (Initialize ((intloc 0) .--> 1)) = Initialize (Initialized s) ) by MEMSTR_0:44;
A5: (Directed I) ";" J = I ";" J by Th25;
set s1 = s +* (Initialize ((intloc 0) .--> 1));
assume A6: I is_halting_on Initialized s,P ; ::_thesis: ( ( for k being Element of NAT st k <= LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1)))) holds
( IC (Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),k)) = IC (Comput ((P +* (I ";" J)),(s +* (Initialize ((intloc 0) .--> 1))),k)) & CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),k))) = CurInstr ((P +* (I ";" J)),(Comput ((P +* (I ";" J)),(s +* (Initialize ((intloc 0) .--> 1))),k))) ) ) & DataPart (Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1))) = DataPart (Comput ((P +* (I ";" J)),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1))) & IC (Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1))) = IC (Comput ((P +* (I ";" J)),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1))) )
 s +* (Initialize ((intloc 0) .--> 1)) = Initialize (Initialized s) by MEMSTR_0:44;
then A7: (LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1 = pseudo-LifeSpan ((Initialized s),P,(Directed I)) by A3, A6, Lm2;
A8: Directed I is_pseudo-closed_on Initialized s,P by A3, A6, Lm2;
hereby  ::_thesis: ( DataPart (Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1))) = DataPart (Comput ((P +* (I ";" J)),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1))) & IC (Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1))) = IC (Comput ((P +* (I ";" J)),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1))) )
let k be Element of NAT ; ::_thesis: ( k <= LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1)))) implies ( IC (Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),k)) = IC (Comput ((P +* (I ";" J)),(s +* (Initialize ((intloc 0) .--> 1))),k)) & CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),k))) = CurInstr ((P +* (I ";" J)),(Comput ((P +* (I ";" J)),(s +* (Initialize ((intloc 0) .--> 1))),k))) ) )
assume  k <= LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1)))) ; ::_thesis: ( IC (Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),k)) = IC (Comput ((P +* (I ";" J)),(s +* (Initialize ((intloc 0) .--> 1))),k)) & CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),k))) = CurInstr ((P +* (I ";" J)),(Comput ((P +* (I ";" J)),(s +* (Initialize ((intloc 0) .--> 1))),k))) )
then A9: k < pseudo-LifeSpan ((Initialized s),P,(Directed I)) by A7, NAT_1:13;
then  Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),k) = Comput ((P +* (I ";" J)),(s +* (Initialize ((intloc 0) .--> 1))),k) by A4, A5, A3, A6, Lm2, Th18;
hence A10: IC (Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),k)) = IC (Comput ((P +* (I ";" J)),(s +* (Initialize ((intloc 0) .--> 1))),k)) ; ::_thesis: CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),k))) = CurInstr ((P +* (I ";" J)),(Comput ((P +* (I ";" J)),(s +* (Initialize ((intloc 0) .--> 1))),k)))
 s +* (Initialize ((intloc 0) .--> 1)) = Initialize (Initialized s) by MEMSTR_0:44;
then A11: IC (Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),k)) in dom (Directed I) by A8, A9, Def4;
A12: Directed I c= I ";" J by SCMFSA6A:16;
then A13: dom (Directed I) c= dom (I ";" J) by GRFUNC_1:2;
thus  CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),k))) = (P +* (Directed I)) . (IC (Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),k))) by A2, PARTFUN1:def_6
.= (Directed I) . (IC (Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),k))) by A11, FUNCT_4:13
.= (I ";" J) . (IC (Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),k))) by A11, A12, GRFUNC_1:2
.= (P +* (I ";" J)) . (IC (Comput ((P +* (I ";" J)),(s +* (Initialize ((intloc 0) .--> 1))),k))) by A10, A13, A11, FUNCT_4:13
.= CurInstr ((P +* (I ";" J)),(Comput ((P +* (I ";" J)),(s +* (Initialize ((intloc 0) .--> 1))),k))) by A1, PARTFUN1:def_6 ; ::_thesis: verum
end;
 Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1)) = Comput ((P +* (I ";" J)),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1)) by A3, A6, A4, A5, A7, Lm2, Th18;
hence  ( DataPart (Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1))) = DataPart (Comput ((P +* (I ";" J)),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1))) & IC (Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1))) = IC (Comput ((P +* (I ";" J)),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1))) ) ; ::_thesis: verum
end;

theorem Th28: :: SCMFSA8A:28
for s being State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA
for I being Program of SCM+FSA st I is_closed_on Initialized s,P & I is_halting_on Initialized s,P holds
for k being Element of NAT st k <= LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1)))) holds
( Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),k) = Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),k) & CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),k))) <> halt SCM+FSA )
proof
let s be State of SCM+FSA; ::_thesis: for P being Instruction-Sequence of SCM+FSA
for I being Program of SCM+FSA st I is_closed_on Initialized s,P & I is_halting_on Initialized s,P holds
for k being Element of NAT st k <= LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1)))) holds
( Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),k) = Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),k) & CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),k))) <> halt SCM+FSA )
let P be Instruction-Sequence of SCM+FSA; ::_thesis: for I being Program of SCM+FSA st I is_closed_on Initialized s,P & I is_halting_on Initialized s,P holds
for k being Element of NAT st k <= LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1)))) holds
( Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),k) = Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),k) & CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),k))) <> halt SCM+FSA )
let I be Program of SCM+FSA; ::_thesis: ( I is_closed_on Initialized s,P & I is_halting_on Initialized s,P implies for k being Element of NAT st k <= LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1)))) holds
( Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),k) = Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),k) & CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),k))) <> halt SCM+FSA ) )
set s1 = s +* (Initialize ((intloc 0) .--> 1));
set s2 = s +* (Initialize ((intloc 0) .--> 1));
A1: dom (P +* (Directed I)) = NAT by PARTFUN1:def_2;
A2: dom (P +* I) = NAT by PARTFUN1:def_2;
A3: Directed I c= P +* (Directed I) by FUNCT_4:25;
defpred S1[ Nat] means ( $1 <= LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1)))) implies ( Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),$1) = Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),$1) & CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),$1))) <> halt SCM+FSA ) );
A4: s +* (Initialize ((intloc 0) .--> 1)) = Initialize (Initialized s) by MEMSTR_0:44;
assume A5: I is_closed_on Initialized s,P ; ::_thesis: ( not I is_halting_on Initialized s,P or for k being Element of NAT st k <= LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1)))) holds
( Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),k) = Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),k) & CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),k))) <> halt SCM+FSA ) )
A6: now__::_thesis:_for_k_being_Element_of_NAT_st_Comput_((P_+*_I),(s_+*_(Initialize_((intloc_0)_.-->_1))),k)_=_Comput_((P_+*_(Directed_I)),(s_+*_(Initialize_((intloc_0)_.-->_1))),k)_holds_
not_CurInstr_((P_+*_(Directed_I)),(Comput_((P_+*_(Directed_I)),(s_+*_(Initialize_((intloc_0)_.-->_1))),k)))_=_halt_SCM+FSA
let k be Element of NAT ; ::_thesis: ( Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),k) = Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),k) implies not CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),k))) = halt SCM+FSA )
 dom (Directed I) = dom I by FUNCT_4:99;
then A7: IC (Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),k)) in dom (Directed I) by A5, A4, SCMFSA7B:def_6;
A8: (P +* (Directed I)) /. (IC (Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),k))) = (P +* (Directed I)) . (IC (Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),k))) by A1, PARTFUN1:def_6;
assume  Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),k) = Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),k) ; ::_thesis: not CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),k))) = halt SCM+FSA
then  CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),k))) = (P +* (Directed I)) . (IC (Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),k))) by A8
.= (Directed I) . (IC (Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),k))) by A7, A3, GRFUNC_1:2 ;
then A9: CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),k))) in rng (Directed I) by A7, FUNCT_1:def_3;
assume  CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),k))) = halt SCM+FSA ; ::_thesis: contradiction
hence  contradiction by A9, SCMFSA6A:1; ::_thesis: verum
end;
assume A10: I is_halting_on Initialized s,P ; ::_thesis: for k being Element of NAT st k <= LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1)))) holds
( Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),k) = Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),k) & CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),k))) <> halt SCM+FSA )
now__::_thesis:_for_k_being_Element_of_NAT_st_(_k_<=_LifeSpan_((P_+*_I),(s_+*_(Initialize_((intloc_0)_.-->_1))))_implies_Comput_((P_+*_I),(s_+*_(Initialize_((intloc_0)_.-->_1))),k)_=_Comput_((P_+*_(Directed_I)),(s_+*_(Initialize_((intloc_0)_.-->_1))),k)_)_&_k_+_1_<=_LifeSpan_((P_+*_I),(s_+*_(Initialize_((intloc_0)_.-->_1))))_holds_
(_Comput_((P_+*_I),(s_+*_(Initialize_((intloc_0)_.-->_1))),(k_+_1))_=_Comput_((P_+*_(Directed_I)),(s_+*_(Initialize_((intloc_0)_.-->_1))),(k_+_1))_&_CurInstr_((P_+*_(Directed_I)),(Comput_((P_+*_(Directed_I)),(s_+*_(Initialize_((intloc_0)_.-->_1))),(k_+_1))))_<>_halt_SCM+FSA_)
A11: P +* I halts_on s +* (Initialize ((intloc 0) .--> 1)) by A10, A4, SCMFSA7B:def_7;
A12: dom I c= dom (Directed I) by FUNCT_4:99;
let k be Element of NAT ; ::_thesis: ( ( k <= LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1)))) implies Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),k) = Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),k) ) & k + 1 <= LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1)))) implies ( Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(k + 1)) = Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),(k + 1)) & CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),(k + 1)))) <> halt SCM+FSA ) )
assume A13: ( k <= LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1)))) implies Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),k) = Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),k) ) ; ::_thesis: ( k + 1 <= LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1)))) implies ( Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(k + 1)) = Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),(k + 1)) & CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),(k + 1)))) <> halt SCM+FSA ) )
A14: Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),(k + 1)) = Following ((P +* (Directed I)),(Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),k))) by EXTPRO_1:3
.= Exec ((CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),k)))),(Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),k))) ;
A15: IC (Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),k)) in dom I by A5, A4, SCMFSA7B:def_6;
A16: I c= P +* I by FUNCT_4:25;
A17: CurInstr ((P +* I),(Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),k))) = (P +* I) . (IC (Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),k))) by A2, PARTFUN1:def_6
.= I . (IC (Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),k))) by A15, A16, GRFUNC_1:2 ;
A18: k + 0 < k + 1 by XREAL_1:6;
assume A19: k + 1 <= LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1)))) ; ::_thesis: ( Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(k + 1)) = Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),(k + 1)) & CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),(k + 1)))) <> halt SCM+FSA )
then  k < LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1)))) by A18, XXREAL_0:2;
then  I . (IC (Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),k))) <> halt SCM+FSA by A17, A11, EXTPRO_1:def_15;
then A20: CurInstr ((P +* I),(Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),k))) = (Directed I) . (IC (Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),k))) by A17, FUNCT_4:105
.= (P +* (Directed I)) . (IC (Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),k))) by A3, A15, A12, GRFUNC_1:2
.= (P +* (Directed I)) . (IC (Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),k))) by A13, A19, A18, XXREAL_0:2
.= CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),k))) by A1, PARTFUN1:def_6 ;
Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(k + 1)) = Following ((P +* I),(Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),k))) by EXTPRO_1:3
.= Exec ((CurInstr ((P +* I),(Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),k)))),(Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),k))) ;
hence  Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(k + 1)) = Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),(k + 1)) by A13, A19, A18, A20, A14, XXREAL_0:2; ::_thesis: CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),(k + 1)))) <> halt SCM+FSA
hence  CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),(k + 1)))) <> halt SCM+FSA by A6; ::_thesis: verum
end;
then A21: for k being Element of NAT st S1[k] holds
S1[k + 1] ;
now__::_thesis:_(_0_<=_LifeSpan_((P_+*_I),(s_+*_(Initialize_((intloc_0)_.-->_1))))_implies_(_Comput_((P_+*_I),(s_+*_(Initialize_((intloc_0)_.-->_1))),0)_=_Comput_((P_+*_(Directed_I)),(s_+*_(Initialize_((intloc_0)_.-->_1))),0)_&_CurInstr_((P_+*_(Directed_I)),(Comput_((P_+*_(Directed_I)),(s_+*_(Initialize_((intloc_0)_.-->_1))),0)))_<>_halt_SCM+FSA_)_)
assume  0 <= LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1)))) ; ::_thesis: ( Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),0) = Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),0) & CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),0))) <> halt SCM+FSA )
thus  Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),0) = Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),0) ; ::_thesis: CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),0))) <> halt SCM+FSA
hence  CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),0))) <> halt SCM+FSA by A6; ::_thesis: verum
end;
then A22: S1[ 0 ] ;
thus  for k being Element of NAT holds S1[k] from NAT_1:sch_1(A22, A21); ::_thesis: verum
end;

theorem Th29: :: SCMFSA8A:29
for s being State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA
for I being Program of SCM+FSA st I is_closed_on Initialized s,P & I is_halting_on Initialized s,P holds
( IC (Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1))) = card I & DataPart (Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) = DataPart (Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1))) )
proof
let s be State of SCM+FSA; ::_thesis: for P being Instruction-Sequence of SCM+FSA
for I being Program of SCM+FSA st I is_closed_on Initialized s,P & I is_halting_on Initialized s,P holds
( IC (Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1))) = card I & DataPart (Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) = DataPart (Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1))) )
let P be Instruction-Sequence of SCM+FSA; ::_thesis: for I being Program of SCM+FSA st I is_closed_on Initialized s,P & I is_halting_on Initialized s,P holds
( IC (Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1))) = card I & DataPart (Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) = DataPart (Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1))) )
let I be Program of SCM+FSA; ::_thesis: ( I is_closed_on Initialized s,P & I is_halting_on Initialized s,P implies ( IC (Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1))) = card I & DataPart (Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) = DataPart (Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1))) ) )
set s1 = s +* (Initialize ((intloc 0) .--> 1));
set s2 = s +* (Initialize ((intloc 0) .--> 1));
set m1 = LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))));
A1: dom (P +* I) = NAT by PARTFUN1:def_2;
A2: dom (P +* (Directed I)) = NAT by PARTFUN1:def_2;
assume A3: I is_closed_on Initialized s,P ; ::_thesis: ( not I is_halting_on Initialized s,P or ( IC (Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1))) = card I & DataPart (Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) = DataPart (Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1))) ) )
set l1 = IC (Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1)))))));
A4: s +* (Initialize ((intloc 0) .--> 1)) = Initialize (Initialized s) by MEMSTR_0:44;
then A5: IC (Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) in dom I by A3, SCMFSA7B:def_6;
assume A6: I is_halting_on Initialized s,P ; ::_thesis: ( IC (Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1))) = card I & DataPart (Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) = DataPart (Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1))) )
then A7: Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1)))))) = Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1)))))) by A3, Th28;
then  IC (Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) in dom I by A5;
then A8: IC (Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) in dom (Directed I) by FUNCT_4:99;
A9: P +* I halts_on s +* (Initialize ((intloc 0) .--> 1)) by A6, A4, SCMFSA7B:def_7;
A10: I c= P +* I by FUNCT_4:25;
A11: I . (IC (Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1)))))))) = (P +* I) . (IC (Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1)))))))) by A5, A10, GRFUNC_1:2
.= CurInstr ((P +* I),(Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1)))))))) by A1, PARTFUN1:def_6
.= halt SCM+FSA by A9, EXTPRO_1:def_15 ;
 IC (Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) = IC (Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) by A7;
then A12: (P +* (Directed I)) . (IC (Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1)))))))) = (Directed I) . (IC (Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1)))))))) by A8, FUNCT_4:13
.= goto (card I) by A5, A11, FUNCT_4:106 ;
A13: (P +* (Directed I)) /. (IC (Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1)))))))) = (P +* (Directed I)) . (IC (Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1)))))))) by A2, PARTFUN1:def_6;
A14: Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1)) = Following ((P +* (Directed I)),(Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1)))))))) by EXTPRO_1:3
.= Exec ((goto (card I)),(Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1)))))))) by A12, A13, A7 ;
hence  IC (Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1))) = card I by SCMFSA_2:69; ::_thesis: DataPart (Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) = DataPart (Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1)))
A15: ( ( for a being Int-Location holds (Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1))) . a = (Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) . a ) & ( for f being FinSeq-Location holds (Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1))) . f = (Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) . f ) ) by A14, SCMFSA_2:69;
 DataPart (Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) = DataPart (Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) by A7;
hence  DataPart (Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) = DataPart (Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1))) by A15, SCMFSA_M:2; ::_thesis: verum
end;

Lm3:  for I being Program of SCM+FSA
for P being Instruction-Sequence of SCM+FSA
for s being State of SCM+FSA st I is_closed_on s,P & I is_halting_on s,P holds
( IC (Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) = card I & DataPart (Comput ((P +* I),(Initialize s),(LifeSpan ((P +* I),(Initialize s))))) = DataPart (Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) & P +* (I ";" (Stop SCM+FSA)) halts_on Initialize s & LifeSpan ((P +* (I ";" (Stop SCM+FSA))),(Initialize s)) = (LifeSpan ((P +* I),(Initialize s))) + 1 & I ";" (Stop SCM+FSA) is_closed_on s,P & I ";" (Stop SCM+FSA) is_halting_on s,P )
proof
let I be Program of SCM+FSA; ::_thesis: for P being Instruction-Sequence of SCM+FSA
for s being State of SCM+FSA st I is_closed_on s,P & I is_halting_on s,P holds
( IC (Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) = card I & DataPart (Comput ((P +* I),(Initialize s),(LifeSpan ((P +* I),(Initialize s))))) = DataPart (Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) & P +* (I ";" (Stop SCM+FSA)) halts_on Initialize s & LifeSpan ((P +* (I ";" (Stop SCM+FSA))),(Initialize s)) = (LifeSpan ((P +* I),(Initialize s))) + 1 & I ";" (Stop SCM+FSA) is_closed_on s,P & I ";" (Stop SCM+FSA) is_halting_on s,P )
let P be Instruction-Sequence of SCM+FSA; ::_thesis: for s being State of SCM+FSA st I is_closed_on s,P & I is_halting_on s,P holds
( IC (Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) = card I & DataPart (Comput ((P +* I),(Initialize s),(LifeSpan ((P +* I),(Initialize s))))) = DataPart (Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) & P +* (I ";" (Stop SCM+FSA)) halts_on Initialize s & LifeSpan ((P +* (I ";" (Stop SCM+FSA))),(Initialize s)) = (LifeSpan ((P +* I),(Initialize s))) + 1 & I ";" (Stop SCM+FSA) is_closed_on s,P & I ";" (Stop SCM+FSA) is_halting_on s,P )
let s be State of SCM+FSA; ::_thesis: ( I is_closed_on s,P & I is_halting_on s,P implies ( IC (Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) = card I & DataPart (Comput ((P +* I),(Initialize s),(LifeSpan ((P +* I),(Initialize s))))) = DataPart (Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) & P +* (I ";" (Stop SCM+FSA)) halts_on Initialize s & LifeSpan ((P +* (I ";" (Stop SCM+FSA))),(Initialize s)) = (LifeSpan ((P +* I),(Initialize s))) + 1 & I ";" (Stop SCM+FSA) is_closed_on s,P & I ";" (Stop SCM+FSA) is_halting_on s,P ) )
assume A1: I is_closed_on s,P ; ::_thesis: ( not I is_halting_on s,P or ( IC (Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) = card I & DataPart (Comput ((P +* I),(Initialize s),(LifeSpan ((P +* I),(Initialize s))))) = DataPart (Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) & P +* (I ";" (Stop SCM+FSA)) halts_on Initialize s & LifeSpan ((P +* (I ";" (Stop SCM+FSA))),(Initialize s)) = (LifeSpan ((P +* I),(Initialize s))) + 1 & I ";" (Stop SCM+FSA) is_closed_on s,P & I ";" (Stop SCM+FSA) is_halting_on s,P ) )
 card (Stop SCM+FSA) = 1 by COMPOS_1:4;
then  card (I ";" (Stop SCM+FSA)) = (card I) + 1 by SCMFSA6A:21;
then  card I < card (I ";" (Stop SCM+FSA)) by NAT_1:13;
then A2: card I in dom (I ";" (Stop SCM+FSA)) by AFINSQ_1:66;
A3: 0 in dom (Stop SCM+FSA) by COMPOS_1:3;
 0 + (card I) in  {  (m + (card I)) where m is Element of NAT : m in dom (Stop SCM+FSA)  }  by A3;
then A4: 0 + (card I) in dom (Reloc ((Stop SCM+FSA),(card I))) by COMPOS_1:33;
set s2 = Initialize s;
set s1 = Initialize s;
A5: 0 in dom (Stop SCM+FSA) by COMPOS_1:3;
A6: (Stop SCM+FSA) . 0 = halt SCM+FSA by AFINSQ_1:34;
assume A7: I is_halting_on s,P ; ::_thesis: ( IC (Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) = card I & DataPart (Comput ((P +* I),(Initialize s),(LifeSpan ((P +* I),(Initialize s))))) = DataPart (Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) & P +* (I ";" (Stop SCM+FSA)) halts_on Initialize s & LifeSpan ((P +* (I ";" (Stop SCM+FSA))),(Initialize s)) = (LifeSpan ((P +* I),(Initialize s))) + 1 & I ";" (Stop SCM+FSA) is_closed_on s,P & I ";" (Stop SCM+FSA) is_halting_on s,P )
then A8: IC (Comput ((P +* (Directed I)),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) = IC (Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) by A1, Th26;
A9: (P +* (I ";" (Stop SCM+FSA))) . (card I) = (I ";" (Stop SCM+FSA)) . (card I) by A2, FUNCT_4:13
.= (Reloc ((Stop SCM+FSA),(card I))) . (0 + (card I)) by A4, FUNCT_4:13
.= IncAddr ((halt SCM+FSA),(card I)) by A6, A5, COMPOS_1:35
.= halt SCM+FSA by COMPOS_0:4 ;
 DataPart (Comput ((P +* (Directed I)),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) = DataPart (Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) by A1, A7, Th26;
hence  ( IC (Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) = card I & DataPart (Comput ((P +* I),(Initialize s),(LifeSpan ((P +* I),(Initialize s))))) = DataPart (Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) ) by A1, A7, A8, Th22; ::_thesis: ( P +* (I ";" (Stop SCM+FSA)) halts_on Initialize s & LifeSpan ((P +* (I ";" (Stop SCM+FSA))),(Initialize s)) = (LifeSpan ((P +* I),(Initialize s))) + 1 & I ";" (Stop SCM+FSA) is_closed_on s,P & I ";" (Stop SCM+FSA) is_halting_on s,P )
 dom (P +* (I ";" (Stop SCM+FSA))) = NAT by PARTFUN1:def_2;
then A10: (P +* (I ";" (Stop SCM+FSA))) /. (IC (Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1)))) = (P +* (I ";" (Stop SCM+FSA))) . (IC (Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1)))) by PARTFUN1:def_6;
A11: CurInstr ((P +* (I ";" (Stop SCM+FSA))),(Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1)))) = halt SCM+FSA by A9, A1, A7, A8, Th22, A10;
hence A12: P +* (I ";" (Stop SCM+FSA)) halts_on Initialize s by EXTPRO_1:29; ::_thesis: ( LifeSpan ((P +* (I ";" (Stop SCM+FSA))),(Initialize s)) = (LifeSpan ((P +* I),(Initialize s))) + 1 & I ";" (Stop SCM+FSA) is_closed_on s,P & I ";" (Stop SCM+FSA) is_halting_on s,P )
A13: now__::_thesis:_for_k_being_Element_of_NAT_st_k_<=_LifeSpan_((P_+*_I),(Initialize_s))_holds_
IC_(Comput_((P_+*_(I_";"_(Stop_SCM+FSA))),(Initialize_s),k))_in_dom_(I_";"_(Stop_SCM+FSA))
let k be Element of NAT ; ::_thesis: ( k <= LifeSpan ((P +* I),(Initialize s)) implies IC (Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),k)) in dom (I ";" (Stop SCM+FSA)) )
assume A14: k <= LifeSpan ((P +* I),(Initialize s)) ; ::_thesis: IC (Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),k)) in dom (I ";" (Stop SCM+FSA))
then  Comput ((P +* I),(Initialize s),k) = Comput ((P +* (Directed I)),(Initialize s),k) by A1, A7, Th21;
then  IC (Comput ((P +* I),(Initialize s),k)) = IC (Comput ((P +* (Directed I)),(Initialize s),k)) ;
then A15: IC (Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),k)) = IC (Comput ((P +* I),(Initialize s),k)) by A1, A7, A14, Th26;
A16: IC (Comput ((P +* I),(Initialize s),k)) in dom I by A1, SCMFSA7B:def_6;
 dom I c= dom (I ";" (Stop SCM+FSA)) by SCMFSA6A:17;
hence  IC (Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),k)) in dom (I ";" (Stop SCM+FSA)) by A15, A16; ::_thesis: verum
end;
defpred S1[ Nat] means ( ( LifeSpan ((P +* I),(Initialize s)) < $1 implies IC (Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),$1)) = card I ) & IC (Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),$1)) in dom (I ";" (Stop SCM+FSA)) );
 card (Stop SCM+FSA) = 1 by COMPOS_1:4;
then  card (I ";" (Stop SCM+FSA)) = (card I) + 1 by SCMFSA6A:21;
then A17: (card I) + 0 < card (I ";" (Stop SCM+FSA)) by XREAL_1:6;
then A18: card I in dom (I ";" (Stop SCM+FSA)) by AFINSQ_1:66;
A19: now__::_thesis:_for_k_being_Element_of_NAT_st_S1[k]_holds_
S1[k_+_1]
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[b1 + 1] )
assume A20: S1[k] ; ::_thesis: S1[b1 + 1]
percases ( k < LifeSpan ((P +* I),(Initialize s)) or k = LifeSpan ((P +* I),(Initialize s)) or k > LifeSpan ((P +* I),(Initialize s)) ) by XXREAL_0:1;
suppose k < LifeSpan ((P +* I),(Initialize s)) ; ::_thesis: S1[b1 + 1]
then  k + 1 <= LifeSpan ((P +* I),(Initialize s)) by NAT_1:13;
hence  S1[k + 1] by A13; ::_thesis: verum
end;
suppose k = LifeSpan ((P +* I),(Initialize s)) ; ::_thesis: S1[b1 + 1]
hence  S1[k + 1] by A1, A7, A8, A18, Th22; ::_thesis: verum
end;
supposeA21: k > LifeSpan ((P +* I),(Initialize s)) ; ::_thesis: S1[b1 + 1]
A22: now__::_thesis:_(_k_+_1_>_LifeSpan_((P_+*_I),(Initialize_s))_implies_IC_(Comput_((P_+*_(I_";"_(Stop_SCM+FSA))),(Initialize_s),(k_+_1)))_=_card_I_)
assume  k + 1 > LifeSpan ((P +* I),(Initialize s)) ; ::_thesis: IC (Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),(k + 1))) = card I
A23: dom (P +* (I ";" (Stop SCM+FSA))) = NAT by PARTFUN1:def_2;
A24: CurInstr ((P +* (I ";" (Stop SCM+FSA))),(Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),k))) = halt SCM+FSA by A9, A20, A21, A23, PARTFUN1:def_6;
thus  IC (Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),(k + 1))) = IC (Following ((P +* (I ";" (Stop SCM+FSA))),(Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),k)))) by EXTPRO_1:3
.= card I by A20, A21, A24, EXTPRO_1:def_3 ; ::_thesis: verum
end;
 k + 1 > k + 0 by XREAL_1:6;
hence  S1[k + 1] by A17, A21, A22, AFINSQ_1:66, XXREAL_0:2; ::_thesis: verum
end;
end;
end;
now__::_thesis:_for_k_being_Element_of_NAT_st_k_<_(LifeSpan_((P_+*_I),(Initialize_s)))_+_1_holds_
CurInstr_((P_+*_(I_";"_(Stop_SCM+FSA))),(Comput_((P_+*_(I_";"_(Stop_SCM+FSA))),(Initialize_s),k)))_<>_halt_SCM+FSA
let k be Element of NAT ; ::_thesis: ( k < (LifeSpan ((P +* I),(Initialize s))) + 1 implies CurInstr ((P +* (I ";" (Stop SCM+FSA))),(Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),k))) <> halt SCM+FSA )
assume  k < (LifeSpan ((P +* I),(Initialize s))) + 1 ; ::_thesis: CurInstr ((P +* (I ";" (Stop SCM+FSA))),(Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),k))) <> halt SCM+FSA
then A25: k <= LifeSpan ((P +* I),(Initialize s)) by NAT_1:13;
then  CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(Initialize s),k))) <> halt SCM+FSA by A1, A7, Th21;
hence  CurInstr ((P +* (I ";" (Stop SCM+FSA))),(Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),k))) <> halt SCM+FSA by A1, A7, A25, Th26; ::_thesis: verum
end;
then  for k being Element of NAT st CurInstr ((P +* (I ";" (Stop SCM+FSA))),(Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),k))) = halt SCM+FSA holds
(LifeSpan ((P +* I),(Initialize s))) + 1 <= k ;
hence  LifeSpan ((P +* (I ";" (Stop SCM+FSA))),(Initialize s)) = (LifeSpan ((P +* I),(Initialize s))) + 1 by A11, A12, EXTPRO_1:def_15; ::_thesis: ( I ";" (Stop SCM+FSA) is_closed_on s,P & I ";" (Stop SCM+FSA) is_halting_on s,P )
A26: S1[ 0 ] by A13, NAT_1:2;
 for k being Element of NAT holds S1[k] from NAT_1:sch_1(A26, A19);
hence  I ";" (Stop SCM+FSA) is_closed_on s,P by SCMFSA7B:def_6; ::_thesis: I ";" (Stop SCM+FSA) is_halting_on s,P
thus  I ";" (Stop SCM+FSA) is_halting_on s,P by A12, SCMFSA7B:def_7; ::_thesis: verum
end;

theorem :: SCMFSA8A:30
for I being Program of SCM+FSA
for P being Instruction-Sequence of SCM+FSA
for s being State of SCM+FSA st I is_closed_on s,P & I is_halting_on s,P holds
( I ";" (Stop SCM+FSA) is_closed_on s,P & I ";" (Stop SCM+FSA) is_halting_on s,P ) by Lm3;

theorem :: SCMFSA8A:31
for l being Element of NAT holds
( 0 in dom (Goto l) & (Goto l) . 0 = goto l ) by Lm1;

Lm4:  for I being Program of SCM+FSA
for s being State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA st I is_closed_on Initialized s,P & I is_halting_on Initialized s,P holds
( IC (Comput ((P +* (I ";" (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1))) = card I & DataPart (Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) = DataPart (Comput ((P +* (I ";" (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1))) & P +* (I ";" (Stop SCM+FSA)) halts_on s +* (Initialize ((intloc 0) .--> 1)) & LifeSpan ((P +* (I ";" (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1)))) = (LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1 )
proof
let I be Program of SCM+FSA; ::_thesis: for s being State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA st I is_closed_on Initialized s,P & I is_halting_on Initialized s,P holds
( IC (Comput ((P +* (I ";" (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1))) = card I & DataPart (Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) = DataPart (Comput ((P +* (I ";" (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1))) & P +* (I ";" (Stop SCM+FSA)) halts_on s +* (Initialize ((intloc 0) .--> 1)) & LifeSpan ((P +* (I ";" (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1)))) = (LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1 )
let s be State of SCM+FSA; ::_thesis: for P being Instruction-Sequence of SCM+FSA st I is_closed_on Initialized s,P & I is_halting_on Initialized s,P holds
( IC (Comput ((P +* (I ";" (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1))) = card I & DataPart (Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) = DataPart (Comput ((P +* (I ";" (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1))) & P +* (I ";" (Stop SCM+FSA)) halts_on s +* (Initialize ((intloc 0) .--> 1)) & LifeSpan ((P +* (I ";" (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1)))) = (LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1 )
let P be Instruction-Sequence of SCM+FSA; ::_thesis: ( I is_closed_on Initialized s,P & I is_halting_on Initialized s,P implies ( IC (Comput ((P +* (I ";" (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1))) = card I & DataPart (Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) = DataPart (Comput ((P +* (I ";" (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1))) & P +* (I ";" (Stop SCM+FSA)) halts_on s +* (Initialize ((intloc 0) .--> 1)) & LifeSpan ((P +* (I ";" (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1)))) = (LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1 ) )
assume A1: I is_closed_on Initialized s,P ; ::_thesis: ( not I is_halting_on Initialized s,P or ( IC (Comput ((P +* (I ";" (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1))) = card I & DataPart (Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) = DataPart (Comput ((P +* (I ";" (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1))) & P +* (I ";" (Stop SCM+FSA)) halts_on s +* (Initialize ((intloc 0) .--> 1)) & LifeSpan ((P +* (I ";" (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1)))) = (LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1 ) )
 card (Stop SCM+FSA) = 1 by COMPOS_1:4;
then  card (I ";" (Stop SCM+FSA)) = (card I) + 1 by SCMFSA6A:21;
then  card I < card (I ";" (Stop SCM+FSA)) by NAT_1:13;
then A2: card I in dom (I ";" (Stop SCM+FSA)) by AFINSQ_1:66;
A3: 0 in dom (Stop SCM+FSA) by COMPOS_1:3;
 0 + (card I) in  {  (m + (card I)) where m is Element of NAT : m in dom (Stop SCM+FSA)  }  by A3;
then A4: 0 + (card I) in dom (Reloc ((Stop SCM+FSA),(card I))) by COMPOS_1:33;
set s2 = s +* (Initialize ((intloc 0) .--> 1));
set s1 = s +* (Initialize ((intloc 0) .--> 1));
assume A5: I is_halting_on Initialized s,P ; ::_thesis: ( IC (Comput ((P +* (I ";" (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1))) = card I & DataPart (Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) = DataPart (Comput ((P +* (I ";" (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1))) & P +* (I ";" (Stop SCM+FSA)) halts_on s +* (Initialize ((intloc 0) .--> 1)) & LifeSpan ((P +* (I ";" (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1)))) = (LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1 )
then A6: IC (Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1))) = IC (Comput ((P +* (I ";" (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1))) by A1, Th27;
A7: 0 in dom (Stop SCM+FSA) by COMPOS_1:3;
A8: (Stop SCM+FSA) . 0 = halt SCM+FSA by AFINSQ_1:34;
A9: (P +* (I ";" (Stop SCM+FSA))) . (card I) = (I ";" (Stop SCM+FSA)) . (card I) by A2, FUNCT_4:13
.= (Reloc ((Stop SCM+FSA),(card I))) . (0 + (card I)) by A4, FUNCT_4:13
.= IncAddr ((halt SCM+FSA),(card I)) by A8, A7, COMPOS_1:35
.= halt SCM+FSA by COMPOS_0:4 ;
 DataPart (Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1))) = DataPart (Comput ((P +* (I ";" (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1))) by A1, A5, Th27;
hence  ( IC (Comput ((P +* (I ";" (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1))) = card I & DataPart (Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) = DataPart (Comput ((P +* (I ";" (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1))) ) by A1, A5, A6, Th29; ::_thesis: ( P +* (I ";" (Stop SCM+FSA)) halts_on s +* (Initialize ((intloc 0) .--> 1)) & LifeSpan ((P +* (I ";" (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1)))) = (LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1 )
 dom (P +* (I ";" (Stop SCM+FSA))) = NAT by PARTFUN1:def_2;
then A10: (P +* (I ";" (Stop SCM+FSA))) /. (IC (Comput ((P +* (I ";" (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1)))) = (P +* (I ";" (Stop SCM+FSA))) . (IC (Comput ((P +* (I ";" (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1)))) by PARTFUN1:def_6;
A11: CurInstr ((P +* (I ";" (Stop SCM+FSA))),(Comput ((P +* (I ";" (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1)))) = halt SCM+FSA by A9, A1, A5, A6, Th29, A10;
hence A12: P +* (I ";" (Stop SCM+FSA)) halts_on s +* (Initialize ((intloc 0) .--> 1)) by EXTPRO_1:29; ::_thesis: LifeSpan ((P +* (I ";" (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1)))) = (LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1
now__::_thesis:_for_k_being_Element_of_NAT_st_k_<_(LifeSpan_((P_+*_I),(s_+*_(Initialize_((intloc_0)_.-->_1)))))_+_1_holds_
CurInstr_((P_+*_(I_";"_(Stop_SCM+FSA))),(Comput_((P_+*_(I_";"_(Stop_SCM+FSA))),(s_+*_(Initialize_((intloc_0)_.-->_1))),k)))_<>_halt_SCM+FSA
let k be Element of NAT ; ::_thesis: ( k < (LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1 implies CurInstr ((P +* (I ";" (Stop SCM+FSA))),(Comput ((P +* (I ";" (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1))),k))) <> halt SCM+FSA )
assume  k < (LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1 ; ::_thesis: CurInstr ((P +* (I ";" (Stop SCM+FSA))),(Comput ((P +* (I ";" (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1))),k))) <> halt SCM+FSA
then A13: k <= LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1)))) by NAT_1:13;
then  CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),k))) <> halt SCM+FSA by A1, A5, Th28;
hence  CurInstr ((P +* (I ";" (Stop SCM+FSA))),(Comput ((P +* (I ";" (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1))),k))) <> halt SCM+FSA by A1, A5, A13, Th27; ::_thesis: verum
end;
then  for k being Element of NAT st CurInstr ((P +* (I ";" (Stop SCM+FSA))),(Comput ((P +* (I ";" (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1))),k))) = halt SCM+FSA holds
(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1 <= k ;
hence  LifeSpan ((P +* (I ";" (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1)))) = (LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1 by A11, A12, EXTPRO_1:def_15; ::_thesis: verum
end;

theorem :: SCMFSA8A:32
for I being Program of SCM+FSA
for s being State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA st I is_closed_on Initialized s,P & I is_halting_on Initialized s,P holds
IC (Comput ((P +* (I ";" (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1))) = card I by Lm4;

theorem :: SCMFSA8A:33
for I being Program of SCM+FSA
for s being State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA st I is_closed_on Initialized s,P & I is_halting_on Initialized s,P holds
DataPart (Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) = DataPart (Comput ((P +* (I ";" (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1))) by Lm4;

theorem :: SCMFSA8A:34
for I being Program of SCM+FSA
for s being State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA st I is_closed_on Initialized s,P & I is_halting_on Initialized s,P holds
P +* (I ";" (Stop SCM+FSA)) halts_on s +* (Initialize ((intloc 0) .--> 1)) by Lm4;

theorem :: SCMFSA8A:35
for I being Program of SCM+FSA
for s being State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA st I is_closed_on Initialized s,P & I is_halting_on Initialized s,P holds
LifeSpan ((P +* (I ";" (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1)))) = (LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1 by Lm4;

theorem :: SCMFSA8A:36
for s being State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA
for I being Program of SCM+FSA st I is_closed_on Initialized s,P & I is_halting_on Initialized s,P holds
IExec ((I ";" (Stop SCM+FSA)),P,s) = (IExec (I,P,s)) +* (Start-At ((card I),SCM+FSA))
proof
let s be State of SCM+FSA; ::_thesis: for P being Instruction-Sequence of SCM+FSA
for I being Program of SCM+FSA st I is_closed_on Initialized s,P & I is_halting_on Initialized s,P holds
IExec ((I ";" (Stop SCM+FSA)),P,s) = (IExec (I,P,s)) +* (Start-At ((card I),SCM+FSA))
let P be Instruction-Sequence of SCM+FSA; ::_thesis: for I being Program of SCM+FSA st I is_closed_on Initialized s,P & I is_halting_on Initialized s,P holds
IExec ((I ";" (Stop SCM+FSA)),P,s) = (IExec (I,P,s)) +* (Start-At ((card I),SCM+FSA))
let I be Program of SCM+FSA; ::_thesis: ( I is_closed_on Initialized s,P & I is_halting_on Initialized s,P implies IExec ((I ";" (Stop SCM+FSA)),P,s) = (IExec (I,P,s)) +* (Start-At ((card I),SCM+FSA)) )
assume A1: I is_closed_on Initialized s,P ; ::_thesis: ( not I is_halting_on Initialized s,P or IExec ((I ";" (Stop SCM+FSA)),P,s) = (IExec (I,P,s)) +* (Start-At ((card I),SCM+FSA)) )
set s1 = Initialized s;
assume A2: I is_halting_on Initialized s,P ; ::_thesis: IExec ((I ";" (Stop SCM+FSA)),P,s) = (IExec (I,P,s)) +* (Start-At ((card I),SCM+FSA))
 Initialized s = Initialize (Initialized s) by MEMSTR_0:44;
then A3: P +* I halts_on Initialized s by A2, SCMFSA7B:def_7;
 ( P +* (I ";" (Stop SCM+FSA)) halts_on Initialized s & LifeSpan ((P +* (I ";" (Stop SCM+FSA))),(Initialized s)) = (LifeSpan ((P +* I),(Initialized s))) + 1 ) by A1, A2, Lm4;
then A4: Result ((P +* (I ";" (Stop SCM+FSA))),(Initialized s)) = Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialized s),((LifeSpan ((P +* I),(Initialized s))) + 1)) by EXTPRO_1:23;
then  DataPart (Result ((P +* (I ";" (Stop SCM+FSA))),(Initialized s))) = DataPart (Comput ((P +* I),(Initialized s),(LifeSpan ((P +* I),(Initialized s))))) by A1, A2, Lm4;
then A5: DataPart (Result ((P +* (I ";" (Stop SCM+FSA))),(Initialized s))) = DataPart (Result ((P +* I),(Initialized s))) by A3, EXTPRO_1:23
.= DataPart ((Result ((P +* I),(Initialized s))) +* (Start-At ((card I),SCM+FSA))) by MEMSTR_0:79 ;
IC (Result ((P +* (I ";" (Stop SCM+FSA))),(Initialized s))) = card I by A1, A2, A4, Lm4
.= IC ((Result ((P +* I),(Initialized s))) +* (Start-At ((card I),SCM+FSA))) by FUNCT_4:113 ;
then A6: Result ((P +* (I ";" (Stop SCM+FSA))),(Initialized s)) = (Result ((P +* I),(Initialized s))) +* (Start-At ((card I),SCM+FSA)) by A5, MEMSTR_0:78;
A7: Result ((P +* (I ";" (Stop SCM+FSA))),(Initialized s)) = (Result ((P +* I),(Initialized s))) +* (Start-At ((card I),SCM+FSA)) by A6;
thus  IExec ((I ";" (Stop SCM+FSA)),P,s) = Result ((P +* (I ";" (Stop SCM+FSA))),(Initialized s)) by SCMFSA6B:def_1
.= (Result ((P +* I),(Initialized s))) +* (Start-At ((card I),SCM+FSA)) by A7
.= (Result ((P +* I),(Initialized s))) +* (Start-At ((card I),SCM+FSA))
.= (Result ((P +* I),(Initialized s))) +* (Start-At ((card I),SCM+FSA))
.= (IExec (I,P,s)) +* (Start-At ((card I),SCM+FSA)) by SCMFSA6B:def_1 ; ::_thesis: verum
end;

Lm5:  for P being Instruction-Sequence of SCM+FSA
for I, J being Program of SCM+FSA
for s being State of SCM+FSA st I is_closed_on s,P & I is_halting_on s,P holds
( IC (Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 2))) = ((card I) + (card J)) + 1 & DataPart (Comput ((P +* I),(Initialize s),(LifeSpan ((P +* I),(Initialize s))))) = DataPart (Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 2))) & ( for k being Element of NAT st k < (LifeSpan ((P +* I),(Initialize s))) + 2 holds
CurInstr ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Initialize s),k))) <> halt SCM+FSA ) & ( for k being Element of NAT st k <= LifeSpan ((P +* I),(Initialize s)) holds
IC (Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Initialize s),k)) = IC (Comput ((P +* I),(Initialize s),k)) ) & IC (Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) = card I & P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA)) halts_on Initialize s & LifeSpan ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Initialize s)) = (LifeSpan ((P +* I),(Initialize s))) + 2 )
proof
let P be Instruction-Sequence of SCM+FSA; ::_thesis: for I, J being Program of SCM+FSA
for s being State of SCM+FSA st I is_closed_on s,P & I is_halting_on s,P holds
( IC (Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 2))) = ((card I) + (card J)) + 1 & DataPart (Comput ((P +* I),(Initialize s),(LifeSpan ((P +* I),(Initialize s))))) = DataPart (Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 2))) & ( for k being Element of NAT st k < (LifeSpan ((P +* I),(Initialize s))) + 2 holds
CurInstr ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Initialize s),k))) <> halt SCM+FSA ) & ( for k being Element of NAT st k <= LifeSpan ((P +* I),(Initialize s)) holds
IC (Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Initialize s),k)) = IC (Comput ((P +* I),(Initialize s),k)) ) & IC (Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) = card I & P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA)) halts_on Initialize s & LifeSpan ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Initialize s)) = (LifeSpan ((P +* I),(Initialize s))) + 2 )
let I, J be Program of SCM+FSA; ::_thesis: for s being State of SCM+FSA st I is_closed_on s,P & I is_halting_on s,P holds
( IC (Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 2))) = ((card I) + (card J)) + 1 & DataPart (Comput ((P +* I),(Initialize s),(LifeSpan ((P +* I),(Initialize s))))) = DataPart (Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 2))) & ( for k being Element of NAT st k < (LifeSpan ((P +* I),(Initialize s))) + 2 holds
CurInstr ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Initialize s),k))) <> halt SCM+FSA ) & ( for k being Element of NAT st k <= LifeSpan ((P +* I),(Initialize s)) holds
IC (Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Initialize s),k)) = IC (Comput ((P +* I),(Initialize s),k)) ) & IC (Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) = card I & P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA)) halts_on Initialize s & LifeSpan ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Initialize s)) = (LifeSpan ((P +* I),(Initialize s))) + 2 )
let s be State of SCM+FSA; ::_thesis: ( I is_closed_on s,P & I is_halting_on s,P implies ( IC (Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 2))) = ((card I) + (card J)) + 1 & DataPart (Comput ((P +* I),(Initialize s),(LifeSpan ((P +* I),(Initialize s))))) = DataPart (Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 2))) & ( for k being Element of NAT st k < (LifeSpan ((P +* I),(Initialize s))) + 2 holds
CurInstr ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Initialize s),k))) <> halt SCM+FSA ) & ( for k being Element of NAT st k <= LifeSpan ((P +* I),(Initialize s)) holds
IC (Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Initialize s),k)) = IC (Comput ((P +* I),(Initialize s),k)) ) & IC (Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) = card I & P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA)) halts_on Initialize s & LifeSpan ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Initialize s)) = (LifeSpan ((P +* I),(Initialize s))) + 2 ) )
assume A1: I is_closed_on s,P ; ::_thesis: ( not I is_halting_on s,P or ( IC (Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 2))) = ((card I) + (card J)) + 1 & DataPart (Comput ((P +* I),(Initialize s),(LifeSpan ((P +* I),(Initialize s))))) = DataPart (Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 2))) & ( for k being Element of NAT st k < (LifeSpan ((P +* I),(Initialize s))) + 2 holds
CurInstr ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Initialize s),k))) <> halt SCM+FSA ) & ( for k being Element of NAT st k <= LifeSpan ((P +* I),(Initialize s)) holds
IC (Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Initialize s),k)) = IC (Comput ((P +* I),(Initialize s),k)) ) & IC (Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) = card I & P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA)) halts_on Initialize s & LifeSpan ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Initialize s)) = (LifeSpan ((P +* I),(Initialize s))) + 2 ) )
A2: card ((Goto ((card J) + 1)) ";" J) = (card (Goto ((card J) + 1))) + (card J) by SCMFSA6A:21
.= 1 + (card J) by Lm1 ;
A3: card ((Goto ((card J) + 1)) ";" J) = (card (Goto ((card J) + 1))) + (card J) by SCMFSA6A:21
.= (card J) + 1 by Lm1 ;
A4: ((card I) + (card J)) + 1 = ((card J) + 1) + (card I) ;
A5: 0 in dom (Stop SCM+FSA) by COMPOS_1:3;
set J2 = (Goto ((card J) + 1)) ";" (J ";" (Stop SCM+FSA));
set s2 = Initialize s;
set P2 = P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA));
set s1 = Initialize s;
assume A6: I is_halting_on s,P ; ::_thesis: ( IC (Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 2))) = ((card I) + (card J)) + 1 & DataPart (Comput ((P +* I),(Initialize s),(LifeSpan ((P +* I),(Initialize s))))) = DataPart (Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 2))) & ( for k being Element of NAT st k < (LifeSpan ((P +* I),(Initialize s))) + 2 holds
CurInstr ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Initialize s),k))) <> halt SCM+FSA ) & ( for k being Element of NAT st k <= LifeSpan ((P +* I),(Initialize s)) holds
IC (Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Initialize s),k)) = IC (Comput ((P +* I),(Initialize s),k)) ) & IC (Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) = card I & P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA)) halts_on Initialize s & LifeSpan ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Initialize s)) = (LifeSpan ((P +* I),(Initialize s))) + 2 )
 dom (Reloc ((Stop SCM+FSA),((card J) + 1))) =  {  (m + ((card J) + 1)) where m is Element of NAT : m in dom (Stop SCM+FSA)  }  by COMPOS_1:33;
then A7: 0 + ((card J) + 1) in dom (Reloc ((Stop SCM+FSA),((card J) + 1))) by A5;
A8: dom (Goto ((card J) + 1)) c= dom ((Goto ((card J) + 1)) ";" J) by SCMFSA6A:17;
A9: 0 in dom (Goto ((card J) + 1)) by Lm1;
A10: ((Goto ((card J) + 1)) ";" (J ";" (Stop SCM+FSA))) . 0 = (((Goto ((card J) + 1)) ";" J) ";" (Stop SCM+FSA)) . 0 by SCMFSA6A:25
.= (Directed ((Goto ((card J) + 1)) ";" J)) . 0 by A9, A8, Th14
.= ((Goto ((card J) + 1)) ";" (Directed J)) . 0 by SCMFSA6A:24
.= (Directed (Goto ((card J) + 1))) . 0 by A9, Th14
.= (Goto ((card J) + 1)) . 0 by SCMFSA6A:22
.= goto ((card J) + 1) by Lm1 ;
A11: ((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA) = (I ";" (Goto ((card J) + 1))) ";" (J ";" (Stop SCM+FSA)) by SCMFSA6A:25
.= I ";" ((Goto ((card J) + 1)) ";" (J ";" (Stop SCM+FSA))) by SCMFSA6A:25 ;
then A12: DataPart (Comput ((P +* (Directed I)),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) = DataPart (Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) by A1, A6, Th26;
A13: card ((Goto ((card J) + 1)) ";" (J ";" (Stop SCM+FSA))) = (card (Goto ((card J) + 1))) + (card (J ";" (Stop SCM+FSA))) by SCMFSA6A:21
.= 1 + (card (J ";" (Stop SCM+FSA))) by Lm1 ;
then A14: 0 + 1 <= card ((Goto ((card J) + 1)) ";" (J ";" (Stop SCM+FSA))) by NAT_1:11;
A15: card (I ";" ((Goto ((card J) + 1)) ";" (J ";" (Stop SCM+FSA)))) = (card I) + (card ((Goto ((card J) + 1)) ";" (J ";" (Stop SCM+FSA)))) by SCMFSA6A:21;
then  (card I) + 0 < card (I ";" ((Goto ((card J) + 1)) ";" (J ";" (Stop SCM+FSA)))) by A14, XREAL_1:6;
then A16: card I in dom (I ";" ((Goto ((card J) + 1)) ";" (J ";" (Stop SCM+FSA)))) by AFINSQ_1:66;
A17: card (Stop SCM+FSA) = 1 by COMPOS_1:4;
card (I ";" ((Goto ((card J) + 1)) ";" (J ";" (Stop SCM+FSA)))) = (card I) + (card (((Goto ((card J) + 1)) ";" J) ";" (Stop SCM+FSA))) by A15, SCMFSA6A:25
.= (card I) + (((card J) + 1) + 1) by A3, A17, SCMFSA6A:21
.= (((card I) + (card J)) + 1) + 1 ;
then  ((card I) + (card J)) + 1 < card (I ";" ((Goto ((card J) + 1)) ";" (J ";" (Stop SCM+FSA)))) by NAT_1:13;
then A18: ((card I) + (card J)) + 1 in dom (I ";" ((Goto ((card J) + 1)) ";" (J ";" (Stop SCM+FSA)))) by AFINSQ_1:66;
A19: 0 in dom ((Goto ((card J) + 1)) ";" (J ";" (Stop SCM+FSA))) by A14, AFINSQ_1:66;
then  0 + (card I) in  {  (m + (card I)) where m is Element of NAT : m in dom ((Goto ((card J) + 1)) ";" (J ";" (Stop SCM+FSA)))  }  ;
then A20: 0 + (card I) in dom (Reloc (((Goto ((card J) + 1)) ";" (J ";" (Stop SCM+FSA))),(card I))) by COMPOS_1:33;
A21: card (Stop SCM+FSA) = 1 by COMPOS_1:4;
A22: (Stop SCM+FSA) . 0 = halt SCM+FSA by AFINSQ_1:34;
card ((Goto ((card J) + 1)) ";" (J ";" (Stop SCM+FSA))) = 1 + ((card J) + (card (Stop SCM+FSA))) by A13, SCMFSA6A:21
.= (card J) + (1 + (card (Stop SCM+FSA))) ;
then  (card J) + 1 < card ((Goto ((card J) + 1)) ";" (J ";" (Stop SCM+FSA))) by A21, XREAL_1:6;
then A23: (card J) + 1 in dom ((Goto ((card J) + 1)) ";" (J ";" (Stop SCM+FSA))) by AFINSQ_1:66;
A24: ((Goto ((card J) + 1)) ";" (J ";" (Stop SCM+FSA))) . ((card J) + 1) = (((Goto ((card J) + 1)) ";" J) ";" (Stop SCM+FSA)) . ((card J) + 1) by SCMFSA6A:25
.= (Reloc ((Stop SCM+FSA),((card J) + 1))) . (0 + ((card J) + 1)) by A2, A7, FUNCT_4:13
.= IncAddr ((halt SCM+FSA),((card J) + 1)) by A5, A22, COMPOS_1:35
.= halt SCM+FSA by COMPOS_0:4 ;
 dom (Reloc (((Goto ((card J) + 1)) ";" (J ";" (Stop SCM+FSA))),(card I))) =  {  (m + (card I)) where m is Element of NAT : m in dom ((Goto ((card J) + 1)) ";" (J ";" (Stop SCM+FSA)))  }  by COMPOS_1:33;
then A25: ((card I) + (card J)) + 1 in dom (Reloc (((Goto ((card J) + 1)) ";" (J ";" (Stop SCM+FSA))),(card I))) by A23, A4;
A26: IC (Comput ((P +* (Directed I)),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) = IC (Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) by A1, A6, A11, Th26;
A27: CurInstr ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1)))) = (P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))) . (IC (Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1)))) by PBOOLE:143
.= (P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))) . (IC (Comput ((P +* (Directed I)),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1)))) by A1, A6, A11, Th26
.= (P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))) . (card I) by A1, A6, Th22
.= (I ";" ((Goto ((card J) + 1)) ";" (J ";" (Stop SCM+FSA)))) . (card I) by A11, A16, FUNCT_4:13
.= (Reloc (((Goto ((card J) + 1)) ";" (J ";" (Stop SCM+FSA))),(card I))) . (0 + (card I)) by A20, FUNCT_4:13
.= IncAddr ((goto ((card J) + 1)),(card I)) by A19, A10, COMPOS_1:35
.= goto (((card J) + 1) + (card I)) by SCMFSA_4:1
.= goto (((card I) + (card J)) + 1) ;
A28: now__::_thesis:_for_f_being_FinSeq-Location_holds_(Comput_((P_+*_(((I_";"_(Goto_((card_J)_+_1)))_";"_J)_";"_(Stop_SCM+FSA))),(Initialize_s),((LifeSpan_((P_+*_I),(Initialize_s)))_+_(1_+_1))))_._f_=_(Comput_((P_+*_(((I_";"_(Goto_((card_J)_+_1)))_";"_J)_";"_(Stop_SCM+FSA))),(Initialize_s),((LifeSpan_((P_+*_I),(Initialize_s)))_+_1)))_._f
let f be FinSeq-Location ; ::_thesis: (Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + (1 + 1)))) . f = (Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) . f
thus (Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + (1 + 1)))) . f = (Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Initialize s),(((LifeSpan ((P +* I),(Initialize s))) + 1) + 1))) . f
.= (Following ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))))) . f by EXTPRO_1:3
.= (Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) . f by A27, SCMFSA_2:69 ; ::_thesis: verum
end;
thus  IC (Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 2))) = IC (Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Initialize s),(((LifeSpan ((P +* I),(Initialize s))) + 1) + 1)))
.= IC (Following ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))))) by EXTPRO_1:3
.= ((card I) + (card J)) + 1 by A27, SCMFSA_2:69 ; ::_thesis: ( DataPart (Comput ((P +* I),(Initialize s),(LifeSpan ((P +* I),(Initialize s))))) = DataPart (Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 2))) & ( for k being Element of NAT st k < (LifeSpan ((P +* I),(Initialize s))) + 2 holds
CurInstr ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Initialize s),k))) <> halt SCM+FSA ) & ( for k being Element of NAT st k <= LifeSpan ((P +* I),(Initialize s)) holds
IC (Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Initialize s),k)) = IC (Comput ((P +* I),(Initialize s),k)) ) & IC (Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) = card I & P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA)) halts_on Initialize s & LifeSpan ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Initialize s)) = (LifeSpan ((P +* I),(Initialize s))) + 2 )
then A29: CurInstr ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 2)))) = (P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))) . (((card I) + (card J)) + 1) by PBOOLE:143
.= (I ";" ((Goto ((card J) + 1)) ";" (J ";" (Stop SCM+FSA)))) . (((card I) + (card J)) + 1) by A11, A18, FUNCT_4:13
.= (Reloc (((Goto ((card J) + 1)) ";" (J ";" (Stop SCM+FSA))),(card I))) . (((card J) + 1) + (card I)) by A25, FUNCT_4:13
.= IncAddr ((halt SCM+FSA),(card I)) by A23, A24, COMPOS_1:35
.= halt SCM+FSA by COMPOS_0:4 ;
now__::_thesis:_for_a_being_Int-Location_holds_(Comput_((P_+*_(((I_";"_(Goto_((card_J)_+_1)))_";"_J)_";"_(Stop_SCM+FSA))),(Initialize_s),((LifeSpan_((P_+*_I),(Initialize_s)))_+_(1_+_1))))_._a_=_(Comput_((P_+*_(((I_";"_(Goto_((card_J)_+_1)))_";"_J)_";"_(Stop_SCM+FSA))),(Initialize_s),((LifeSpan_((P_+*_I),(Initialize_s)))_+_1)))_._a
let a be Int-Location; ::_thesis: (Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + (1 + 1)))) . a = (Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) . a
thus (Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + (1 + 1)))) . a = (Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Initialize s),(((LifeSpan ((P +* I),(Initialize s))) + 1) + 1))) . a
.= (Following ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))))) . a by EXTPRO_1:3
.= (Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) . a by A27, SCMFSA_2:69 ; ::_thesis: verum
end;
then  DataPart (Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) = DataPart (Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 2))) by A28, SCMFSA_M:2;
hence  DataPart (Comput ((P +* I),(Initialize s),(LifeSpan ((P +* I),(Initialize s))))) = DataPart (Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 2))) by A1, A6, A12, Th22; ::_thesis: ( ( for k being Element of NAT st k < (LifeSpan ((P +* I),(Initialize s))) + 2 holds
CurInstr ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Initialize s),k))) <> halt SCM+FSA ) & ( for k being Element of NAT st k <= LifeSpan ((P +* I),(Initialize s)) holds
IC (Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Initialize s),k)) = IC (Comput ((P +* I),(Initialize s),k)) ) & IC (Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) = card I & P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA)) halts_on Initialize s & LifeSpan ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Initialize s)) = (LifeSpan ((P +* I),(Initialize s))) + 2 )
hereby  ::_thesis: ( ( for k being Element of NAT st k <= LifeSpan ((P +* I),(Initialize s)) holds
IC (Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Initialize s),k)) = IC (Comput ((P +* I),(Initialize s),k)) ) & IC (Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) = card I & P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA)) halts_on Initialize s & LifeSpan ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Initialize s)) = (LifeSpan ((P +* I),(Initialize s))) + 2 )
let k be Element of NAT ; ::_thesis: ( k < (LifeSpan ((P +* I),(Initialize s))) + 2 implies CurInstr ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Initialize s),b1))) <> halt SCM+FSA )
assume A31: k < (LifeSpan ((P +* I),(Initialize s))) + 2 ; ::_thesis: CurInstr ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Initialize s),b1))) <> halt SCM+FSA
percases ( k <= LifeSpan ((P +* I),(Initialize s)) or LifeSpan ((P +* I),(Initialize s)) < k ) ;
supposeA32: k <= LifeSpan ((P +* I),(Initialize s)) ; ::_thesis: CurInstr ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Initialize s),b1))) <> halt SCM+FSA
then  CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(Initialize s),k))) <> halt SCM+FSA by A1, A6, Th21;
hence  CurInstr ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Initialize s),k))) <> halt SCM+FSA by A1, A6, A11, A32, Th26; ::_thesis: verum
end;
supposeA33: LifeSpan ((P +* I),(Initialize s)) < k ; ::_thesis: CurInstr ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Initialize s),b1))) <> halt SCM+FSA
 k < ((LifeSpan ((P +* I),(Initialize s))) + 1) + 1 by A31;
then A34: k <= (LifeSpan ((P +* I),(Initialize s))) + 1 by NAT_1:13;
 (LifeSpan ((P +* I),(Initialize s))) + 1 <= k by A33, NAT_1:13;
hence  CurInstr ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Initialize s),k))) <> halt SCM+FSA by A27, A34, XXREAL_0:1; ::_thesis: verum
end;
end;
end;
hereby  ::_thesis: ( IC (Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) = card I & P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA)) halts_on Initialize s & LifeSpan ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Initialize s)) = (LifeSpan ((P +* I),(Initialize s))) + 2 )
let k be Element of NAT ; ::_thesis: ( k <= LifeSpan ((P +* I),(Initialize s)) implies IC (Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Initialize s),k)) = IC (Comput ((P +* I),(Initialize s),k)) )
assume A35: k <= LifeSpan ((P +* I),(Initialize s)) ; ::_thesis: IC (Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Initialize s),k)) = IC (Comput ((P +* I),(Initialize s),k))
then  Comput ((P +* I),(Initialize s),k) = Comput ((P +* (Directed I)),(Initialize s),k) by A1, A6, Th21;
then  IC (Comput ((P +* I),(Initialize s),k)) = IC (Comput ((P +* (Directed I)),(Initialize s),k)) ;
hence  IC (Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Initialize s),k)) = IC (Comput ((P +* I),(Initialize s),k)) by A1, A6, A11, A35, Th26; ::_thesis: verum
end;
thus  IC (Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) = card I by A1, A6, A26, Th22; ::_thesis: ( P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA)) halts_on Initialize s & LifeSpan ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Initialize s)) = (LifeSpan ((P +* I),(Initialize s))) + 2 )
thus A36: P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA)) halts_on Initialize s by A29, EXTPRO_1:29; ::_thesis: LifeSpan ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Initialize s)) = (LifeSpan ((P +* I),(Initialize s))) + 2
 for k being Element of NAT st CurInstr ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Initialize s),k))) = halt SCM+FSA holds
(LifeSpan ((P +* I),(Initialize s))) + 2 <= k by A30;
hence  LifeSpan ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Initialize s)) = (LifeSpan ((P +* I),(Initialize s))) + 2 by A29, A36, EXTPRO_1:def_15; ::_thesis: verum
end;

theorem :: SCMFSA8A:37
for P being Instruction-Sequence of SCM+FSA
for I, J being Program of SCM+FSA
for s being State of SCM+FSA st I is_closed_on s,P & I is_halting_on s,P holds
( ((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA) is_closed_on s,P & ((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA) is_halting_on s,P )
proof
let P be Instruction-Sequence of SCM+FSA; ::_thesis: for I, J being Program of SCM+FSA
for s being State of SCM+FSA st I is_closed_on s,P & I is_halting_on s,P holds
( ((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA) is_closed_on s,P & ((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA) is_halting_on s,P )
let I, J be Program of SCM+FSA; ::_thesis: for s being State of SCM+FSA st I is_closed_on s,P & I is_halting_on s,P holds
( ((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA) is_closed_on s,P & ((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA) is_halting_on s,P )
let s be State of SCM+FSA; ::_thesis: ( I is_closed_on s,P & I is_halting_on s,P implies ( ((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA) is_closed_on s,P & ((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA) is_halting_on s,P ) )
set IJ2 = ((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA);
assume A1: I is_closed_on s,P ; ::_thesis: ( not I is_halting_on s,P or ( ((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA) is_closed_on s,P & ((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA) is_halting_on s,P ) )
set s1 = Initialize s;
set s2 = Initialize s;
set P2 = P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA));
assume A2: I is_halting_on s,P ; ::_thesis: ( ((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA) is_closed_on s,P & ((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA) is_halting_on s,P )
then A3: P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA)) halts_on Initialize s by A1, Lm5;
A4: LifeSpan ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Initialize s)) = (LifeSpan ((P +* I),(Initialize s))) + 2 by A1, A2, Lm5;
now__::_thesis:_for_k_being_Element_of_NAT_holds_IC_(Comput_((P_+*_(((I_";"_(Goto_((card_J)_+_1)))_";"_J)_";"_(Stop_SCM+FSA))),(Initialize_s),k))_in_dom_(((I_";"_(Goto_((card_J)_+_1)))_";"_J)_";"_(Stop_SCM+FSA))
let k be Element of NAT ; ::_thesis: IC (Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Initialize s),b1)) in dom (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))
 ( k <= LifeSpan ((P +* I),(Initialize s)) or k >= (LifeSpan ((P +* I),(Initialize s))) + 1 ) by NAT_1:13;
then  ( k <= LifeSpan ((P +* I),(Initialize s)) or k = (LifeSpan ((P +* I),(Initialize s))) + 1 or k > (LifeSpan ((P +* I),(Initialize s))) + 1 ) by XXREAL_0:1;
then A5: ( k <= LifeSpan ((P +* I),(Initialize s)) or k = (LifeSpan ((P +* I),(Initialize s))) + 1 or k >= ((LifeSpan ((P +* I),(Initialize s))) + 1) + 1 ) by NAT_1:13;
 card (Stop SCM+FSA) = 1 by COMPOS_1:4;
then A6: card (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA)) = (card ((I ";" (Goto ((card J) + 1))) ";" J)) + 1 by SCMFSA6A:21
.= ((card (I ";" (Goto ((card J) + 1)))) + (card J)) + 1 by SCMFSA6A:21
.= (((card I) + (card (Goto ((card J) + 1)))) + (card J)) + 1 by SCMFSA6A:21
.= (((card I) + 1) + (card J)) + 1 by Lm1
.= (card I) + (((card J) + 1) + 1) ;
 0 <= (card J) + 1 by NAT_1:2;
then  0 + 0 < ((card J) + 1) + 1 by XREAL_1:8;
then A7: (card I) + 0 < card (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA)) by A6, XREAL_1:6;
percases ( k <= LifeSpan ((P +* I),(Initialize s)) or k = (LifeSpan ((P +* I),(Initialize s))) + 1 or k >= (LifeSpan ((P +* I),(Initialize s))) + 2 ) by A5;
supposeA8: k <= LifeSpan ((P +* I),(Initialize s)) ; ::_thesis: IC (Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Initialize s),b1)) in dom (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))
reconsider n = IC (Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Initialize s),k)) as Element of NAT ;
 IC (Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Initialize s),k)) = IC (Comput ((P +* I),(Initialize s),k)) by A1, A2, A8, Lm5;
then  IC (Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Initialize s),k)) in dom I by A1, SCMFSA7B:def_6;
then  n < card I by AFINSQ_1:66;
then  n < card (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA)) by A7, XXREAL_0:2;
hence  IC (Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Initialize s),k)) in dom (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA)) by AFINSQ_1:66; ::_thesis: verum
end;
suppose k = (LifeSpan ((P +* I),(Initialize s))) + 1 ; ::_thesis: IC (Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Initialize s),b1)) in dom (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))
then  IC (Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Initialize s),k)) = card I by A1, A2, Lm5;
hence  IC (Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Initialize s),k)) in dom (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA)) by A7, AFINSQ_1:66; ::_thesis: verum
end;
supposeA9: k >= (LifeSpan ((P +* I),(Initialize s))) + 2 ; ::_thesis: IC (Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Initialize s),b1)) in dom (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))
 card (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA)) = (((card I) + (card J)) + 1) + 1 by A6;
then A10: (((card I) + (card J)) + 1) + 0 < card (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA)) by XREAL_1:6;
 k >= LifeSpan ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Initialize s)) by A1, A2, A9, Lm5;
then  IC (Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Initialize s),k)) = IC (Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Initialize s),(LifeSpan ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Initialize s))))) by A3, EXTPRO_1:25
.= ((card I) + (card J)) + 1 by A1, A2, A4, Lm5 ;
hence  IC (Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Initialize s),k)) in dom (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA)) by A10, AFINSQ_1:66; ::_thesis: verum
end;
end;
end;
hence  ((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA) is_closed_on s,P by SCMFSA7B:def_6; ::_thesis: ((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA) is_halting_on s,P
thus  ((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA) is_halting_on s,P by A3, SCMFSA7B:def_7; ::_thesis: verum
end;

theorem :: SCMFSA8A:38
for I, J being Program of SCM+FSA
for s being State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA st I is_closed_on s,P & I is_halting_on s,P holds
P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA)) halts_on Initialize s by Lm5;

Lm6:  for P being Instruction-Sequence of SCM+FSA
for I, J being Program of SCM+FSA
for s being State of SCM+FSA st I is_closed_on Initialized s,P & I is_halting_on Initialized s,P holds
( IC (Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 2))) = ((card I) + (card J)) + 1 & DataPart (Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) = DataPart (Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 2))) & ( for k being Element of NAT st k < (LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 2 holds
CurInstr ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1))),k))) <> halt SCM+FSA ) & ( for k being Element of NAT st k <= LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1)))) holds
IC (Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1))),k)) = IC (Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),k)) ) & IC (Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1))) = card I & P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA)) halts_on s +* (Initialize ((intloc 0) .--> 1)) & LifeSpan ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1)))) = (LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 2 )
proof
let P be Instruction-Sequence of SCM+FSA; ::_thesis: for I, J being Program of SCM+FSA
for s being State of SCM+FSA st I is_closed_on Initialized s,P & I is_halting_on Initialized s,P holds
( IC (Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 2))) = ((card I) + (card J)) + 1 & DataPart (Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) = DataPart (Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 2))) & ( for k being Element of NAT st k < (LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 2 holds
CurInstr ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1))),k))) <> halt SCM+FSA ) & ( for k being Element of NAT st k <= LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1)))) holds
IC (Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1))),k)) = IC (Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),k)) ) & IC (Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1))) = card I & P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA)) halts_on s +* (Initialize ((intloc 0) .--> 1)) & LifeSpan ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1)))) = (LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 2 )
let I, J be Program of SCM+FSA; ::_thesis: for s being State of SCM+FSA st I is_closed_on Initialized s,P & I is_halting_on Initialized s,P holds
( IC (Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 2))) = ((card I) + (card J)) + 1 & DataPart (Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) = DataPart (Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 2))) & ( for k being Element of NAT st k < (LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 2 holds
CurInstr ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1))),k))) <> halt SCM+FSA ) & ( for k being Element of NAT st k <= LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1)))) holds
IC (Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1))),k)) = IC (Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),k)) ) & IC (Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1))) = card I & P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA)) halts_on s +* (Initialize ((intloc 0) .--> 1)) & LifeSpan ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1)))) = (LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 2 )
let s be State of SCM+FSA; ::_thesis: ( I is_closed_on Initialized s,P & I is_halting_on Initialized s,P implies ( IC (Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 2))) = ((card I) + (card J)) + 1 & DataPart (Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) = DataPart (Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 2))) & ( for k being Element of NAT st k < (LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 2 holds
CurInstr ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1))),k))) <> halt SCM+FSA ) & ( for k being Element of NAT st k <= LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1)))) holds
IC (Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1))),k)) = IC (Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),k)) ) & IC (Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1))) = card I & P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA)) halts_on s +* (Initialize ((intloc 0) .--> 1)) & LifeSpan ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1)))) = (LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 2 ) )
assume A1: I is_closed_on Initialized s,P ; ::_thesis: ( not I is_halting_on Initialized s,P or ( IC (Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 2))) = ((card I) + (card J)) + 1 & DataPart (Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) = DataPart (Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 2))) & ( for k being Element of NAT st k < (LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 2 holds
CurInstr ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1))),k))) <> halt SCM+FSA ) & ( for k being Element of NAT st k <= LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1)))) holds
IC (Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1))),k)) = IC (Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),k)) ) & IC (Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1))) = card I & P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA)) halts_on s +* (Initialize ((intloc 0) .--> 1)) & LifeSpan ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1)))) = (LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 2 ) )
A2: card ((Goto ((card J) + 1)) ";" J) = (card (Goto ((card J) + 1))) + (card J) by SCMFSA6A:21
.= 1 + (card J) by Lm1 ;
A3: card ((Goto ((card J) + 1)) ";" J) = (card (Goto ((card J) + 1))) + (card J) by SCMFSA6A:21
.= (card J) + 1 by Lm1 ;
A4: ((card I) + (card J)) + 1 = ((card J) + 1) + (card I) ;
A5: 0 in dom (Stop SCM+FSA) by COMPOS_1:3;
set J2 = (Goto ((card J) + 1)) ";" (J ";" (Stop SCM+FSA));
set s2 = s +* (Initialize ((intloc 0) .--> 1));
set P2 = P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA));
set s1 = s +* (Initialize ((intloc 0) .--> 1));
assume A6: I is_halting_on Initialized s,P ; ::_thesis: ( IC (Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 2))) = ((card I) + (card J)) + 1 & DataPart (Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) = DataPart (Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 2))) & ( for k being Element of NAT st k < (LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 2 holds
CurInstr ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1))),k))) <> halt SCM+FSA ) & ( for k being Element of NAT st k <= LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1)))) holds
IC (Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1))),k)) = IC (Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),k)) ) & IC (Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1))) = card I & P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA)) halts_on s +* (Initialize ((intloc 0) .--> 1)) & LifeSpan ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1)))) = (LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 2 )
 dom (Reloc ((Stop SCM+FSA),((card J) + 1))) =  {  (m + ((card J) + 1)) where m is Element of NAT : m in dom (Stop SCM+FSA)  }  by COMPOS_1:33;
then A7: 0 + ((card J) + 1) in dom (Reloc ((Stop SCM+FSA),((card J) + 1))) by A5;
A8: dom (Goto ((card J) + 1)) c= dom ((Goto ((card J) + 1)) ";" J) by SCMFSA6A:17;
A9: 0 in dom (Goto ((card J) + 1)) by Lm1;
A10: ((Goto ((card J) + 1)) ";" (J ";" (Stop SCM+FSA))) . 0 = (((Goto ((card J) + 1)) ";" J) ";" (Stop SCM+FSA)) . 0 by SCMFSA6A:25
.= (Directed ((Goto ((card J) + 1)) ";" J)) . 0 by A9, A8, Th14
.= ((Goto ((card J) + 1)) ";" (Directed J)) . 0 by SCMFSA6A:24
.= (Directed (Goto ((card J) + 1))) . 0 by A9, Th14
.= (Goto ((card J) + 1)) . 0 by SCMFSA6A:22
.= goto ((card J) + 1) by Lm1 ;
A11: ((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA) = (I ";" (Goto ((card J) + 1))) ";" (J ";" (Stop SCM+FSA)) by SCMFSA6A:25
.= I ";" ((Goto ((card J) + 1)) ";" (J ";" (Stop SCM+FSA))) by SCMFSA6A:25 ;
then A12: DataPart (Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1))) = DataPart (Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1))) by A1, A6, Th27;
A13: card ((Goto ((card J) + 1)) ";" (J ";" (Stop SCM+FSA))) = (card (Goto ((card J) + 1))) + (card (J ";" (Stop SCM+FSA))) by SCMFSA6A:21
.= 1 + (card (J ";" (Stop SCM+FSA))) by Lm1 ;
then A14: 0 + 1 <= card ((Goto ((card J) + 1)) ";" (J ";" (Stop SCM+FSA))) by NAT_1:11;
A15: card (I ";" ((Goto ((card J) + 1)) ";" (J ";" (Stop SCM+FSA)))) = (card I) + (card ((Goto ((card J) + 1)) ";" (J ";" (Stop SCM+FSA)))) by SCMFSA6A:21;
then  (card I) + 0 < card (I ";" ((Goto ((card J) + 1)) ";" (J ";" (Stop SCM+FSA)))) by A14, XREAL_1:6;
then A16: card I in dom (I ";" ((Goto ((card J) + 1)) ";" (J ";" (Stop SCM+FSA)))) by AFINSQ_1:66;
A17: card (Stop SCM+FSA) = 1 by COMPOS_1:4;
card (I ";" ((Goto ((card J) + 1)) ";" (J ";" (Stop SCM+FSA)))) = (card I) + (card (((Goto ((card J) + 1)) ";" J) ";" (Stop SCM+FSA))) by A15, SCMFSA6A:25
.= (card I) + (((card J) + 1) + 1) by A3, A17, SCMFSA6A:21
.= (((card I) + (card J)) + 1) + 1 ;
then  ((card I) + (card J)) + 1 < card (I ";" ((Goto ((card J) + 1)) ";" (J ";" (Stop SCM+FSA)))) by NAT_1:13;
then A18: ((card I) + (card J)) + 1 in dom (I ";" ((Goto ((card J) + 1)) ";" (J ";" (Stop SCM+FSA)))) by AFINSQ_1:66;
A19: 0 in dom ((Goto ((card J) + 1)) ";" (J ";" (Stop SCM+FSA))) by A14, AFINSQ_1:66;
then  0 + (card I) in  {  (m + (card I)) where m is Element of NAT : m in dom ((Goto ((card J) + 1)) ";" (J ";" (Stop SCM+FSA)))  }  ;
then A20: 0 + (card I) in dom (Reloc (((Goto ((card J) + 1)) ";" (J ";" (Stop SCM+FSA))),(card I))) by COMPOS_1:33;
A21: card (Stop SCM+FSA) = 1 by COMPOS_1:4;
A22: (Stop SCM+FSA) . 0 = halt SCM+FSA by AFINSQ_1:34;
card ((Goto ((card J) + 1)) ";" (J ";" (Stop SCM+FSA))) = 1 + ((card J) + (card (Stop SCM+FSA))) by A13, SCMFSA6A:21
.= (card J) + (1 + (card (Stop SCM+FSA))) ;
then  (card J) + 1 < card ((Goto ((card J) + 1)) ";" (J ";" (Stop SCM+FSA))) by A21, XREAL_1:6;
then A23: (card J) + 1 in dom ((Goto ((card J) + 1)) ";" (J ";" (Stop SCM+FSA))) by AFINSQ_1:66;
A24: (P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))) /. (IC (Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1)))) = (P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))) . (IC (Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1)))) by PBOOLE:143;
A25: ((Goto ((card J) + 1)) ";" (J ";" (Stop SCM+FSA))) . ((card J) + 1) = (((Goto ((card J) + 1)) ";" J) ";" (Stop SCM+FSA)) . ((card J) + 1) by SCMFSA6A:25
.= (Reloc ((Stop SCM+FSA),((card J) + 1))) . (0 + ((card J) + 1)) by A2, A7, FUNCT_4:13
.= IncAddr ((halt SCM+FSA),((card J) + 1)) by A5, A22, COMPOS_1:35
.= halt SCM+FSA by COMPOS_0:4 ;
 dom (Reloc (((Goto ((card J) + 1)) ";" (J ";" (Stop SCM+FSA))),(card I))) =  {  (m + (card I)) where m is Element of NAT : m in dom ((Goto ((card J) + 1)) ";" (J ";" (Stop SCM+FSA)))  }  by COMPOS_1:33;
then A26: ((card I) + (card J)) + 1 in dom (Reloc (((Goto ((card J) + 1)) ";" (J ";" (Stop SCM+FSA))),(card I))) by A23, A4;
A27: IC (Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1))) = IC (Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1))) by A1, A6, A11, Th27;
then A28: CurInstr ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1)))) = (P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))) . (card I) by A1, A6, Th29, A24
.= (I ";" ((Goto ((card J) + 1)) ";" (J ";" (Stop SCM+FSA)))) . (card I) by A11, A16, FUNCT_4:13
.= (Reloc (((Goto ((card J) + 1)) ";" (J ";" (Stop SCM+FSA))),(card I))) . (0 + (card I)) by A20, FUNCT_4:13
.= IncAddr ((goto ((card J) + 1)),(card I)) by A19, A10, COMPOS_1:35
.= goto (((card J) + 1) + (card I)) by SCMFSA_4:1
.= goto (((card I) + (card J)) + 1) ;
A29: now__::_thesis:_for_f_being_FinSeq-Location_holds_(Comput_((P_+*_(((I_";"_(Goto_((card_J)_+_1)))_";"_J)_";"_(Stop_SCM+FSA))),(s_+*_(Initialize_((intloc_0)_.-->_1))),((LifeSpan_((P_+*_I),(s_+*_(Initialize_((intloc_0)_.-->_1)))))_+_(1_+_1))))_._f_=_(Comput_((P_+*_(((I_";"_(Goto_((card_J)_+_1)))_";"_J)_";"_(Stop_SCM+FSA))),(s_+*_(Initialize_((intloc_0)_.-->_1))),((LifeSpan_((P_+*_I),(s_+*_(Initialize_((intloc_0)_.-->_1)))))_+_1)))_._f
let f be FinSeq-Location ; ::_thesis: (Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + (1 + 1)))) . f = (Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1))) . f
thus (Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + (1 + 1)))) . f = (Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1))),(((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1) + 1))) . f
.= (Following ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1))))) . f by EXTPRO_1:3
.= (Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1))) . f by A28, SCMFSA_2:69 ; ::_thesis: verum
end;
thus  IC (Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 2))) = IC (Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1))),(((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1) + 1)))
.= IC (Following ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1))))) by EXTPRO_1:3
.= ((card I) + (card J)) + 1 by A28, SCMFSA_2:69 ; ::_thesis: ( DataPart (Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) = DataPart (Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 2))) & ( for k being Element of NAT st k < (LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 2 holds
CurInstr ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1))),k))) <> halt SCM+FSA ) & ( for k being Element of NAT st k <= LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1)))) holds
IC (Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1))),k)) = IC (Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),k)) ) & IC (Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1))) = card I & P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA)) halts_on s +* (Initialize ((intloc 0) .--> 1)) & LifeSpan ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1)))) = (LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 2 )
then A30: CurInstr ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 2)))) = (P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))) . (((card I) + (card J)) + 1) by PBOOLE:143
.= (I ";" ((Goto ((card J) + 1)) ";" (J ";" (Stop SCM+FSA)))) . (((card I) + (card J)) + 1) by A11, A18, FUNCT_4:13
.= (Reloc (((Goto ((card J) + 1)) ";" (J ";" (Stop SCM+FSA))),(card I))) . (((card J) + 1) + (card I)) by A26, FUNCT_4:13
.= IncAddr ((halt SCM+FSA),(card I)) by A23, A25, COMPOS_1:35
.= halt SCM+FSA by COMPOS_0:4 ;
now__::_thesis:_for_a_being_Int-Location_holds_(Comput_((P_+*_(((I_";"_(Goto_((card_J)_+_1)))_";"_J)_";"_(Stop_SCM+FSA))),(s_+*_(Initialize_((intloc_0)_.-->_1))),((LifeSpan_((P_+*_I),(s_+*_(Initialize_((intloc_0)_.-->_1)))))_+_(1_+_1))))_._a_=_(Comput_((P_+*_(((I_";"_(Goto_((card_J)_+_1)))_";"_J)_";"_(Stop_SCM+FSA))),(s_+*_(Initialize_((intloc_0)_.-->_1))),((LifeSpan_((P_+*_I),(s_+*_(Initialize_((intloc_0)_.-->_1)))))_+_1)))_._a
let a be Int-Location; ::_thesis: (Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + (1 + 1)))) . a = (Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1))) . a
thus (Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + (1 + 1)))) . a = (Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1))),(((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1) + 1))) . a
.= (Following ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1))))) . a by EXTPRO_1:3
.= (Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1))) . a by A28, SCMFSA_2:69 ; ::_thesis: verum
end;
then  DataPart (Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1))) = DataPart (Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 2))) by A29, SCMFSA_M:2;
hence  DataPart (Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) = DataPart (Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 2))) by A1, A6, A12, Th29; ::_thesis: ( ( for k being Element of NAT st k < (LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 2 holds
CurInstr ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1))),k))) <> halt SCM+FSA ) & ( for k being Element of NAT st k <= LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1)))) holds
IC (Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1))),k)) = IC (Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),k)) ) & IC (Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1))) = card I & P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA)) halts_on s +* (Initialize ((intloc 0) .--> 1)) & LifeSpan ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1)))) = (LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 2 )
hereby  ::_thesis: ( ( for k being Element of NAT st k <= LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1)))) holds
IC (Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1))),k)) = IC (Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),k)) ) & IC (Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1))) = card I & P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA)) halts_on s +* (Initialize ((intloc 0) .--> 1)) & LifeSpan ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1)))) = (LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 2 )
let k be Element of NAT ; ::_thesis: ( k < (LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 2 implies CurInstr ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1))),b1))) <> halt SCM+FSA )
assume A32: k < (LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 2 ; ::_thesis: CurInstr ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1))),b1))) <> halt SCM+FSA
percases ( k <= LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1)))) or LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1)))) < k ) ;
supposeA33: k <= LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1)))) ; ::_thesis: CurInstr ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1))),b1))) <> halt SCM+FSA
then  CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),k))) <> halt SCM+FSA by A1, A6, Th28;
hence  CurInstr ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1))),k))) <> halt SCM+FSA by A1, A6, A11, A33, Th27; ::_thesis: verum
end;
supposeA34: LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1)))) < k ; ::_thesis: CurInstr ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1))),b1))) <> halt SCM+FSA
 k < ((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1) + 1 by A32;
then A35: k <= (LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1 by NAT_1:13;
 (LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1 <= k by A34, NAT_1:13;
hence  CurInstr ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1))),k))) <> halt SCM+FSA by A28, A35, XXREAL_0:1; ::_thesis: verum
end;
end;
end;
hereby  ::_thesis: ( IC (Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1))) = card I & P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA)) halts_on s +* (Initialize ((intloc 0) .--> 1)) & LifeSpan ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1)))) = (LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 2 )
let k be Element of NAT ; ::_thesis: ( k <= LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1)))) implies IC (Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1))),k)) = IC (Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),k)) )
assume A36: k <= LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1)))) ; ::_thesis: IC (Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1))),k)) = IC (Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),k))
then  Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),k) = Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),k) by A1, A6, Th28;
then  IC (Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),k)) = IC (Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),k)) ;
hence  IC (Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1))),k)) = IC (Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),k)) by A1, A6, A11, A36, Th27; ::_thesis: verum
end;
thus  IC (Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1))) = card I by A1, A6, A27, Th29; ::_thesis: ( P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA)) halts_on s +* (Initialize ((intloc 0) .--> 1)) & LifeSpan ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1)))) = (LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 2 )
thus A37: P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA)) halts_on s +* (Initialize ((intloc 0) .--> 1)) by A30, EXTPRO_1:29; ::_thesis: LifeSpan ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1)))) = (LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 2
 for k being Element of NAT st CurInstr ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1))),k))) = halt SCM+FSA holds
(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 2 <= k by A31;
hence  LifeSpan ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1)))) = (LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 2 by A30, A37, EXTPRO_1:def_15; ::_thesis: verum
end;

theorem :: SCMFSA8A:39
for P being Instruction-Sequence of SCM+FSA
for I, J being Program of SCM+FSA
for s being State of SCM+FSA st I is_closed_on Initialized s,P & I is_halting_on Initialized s,P holds
P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA)) halts_on s +* (Initialize ((intloc 0) .--> 1)) by Lm6;

theorem :: SCMFSA8A:40
for P being Instruction-Sequence of SCM+FSA
for I, J being Program of SCM+FSA
for s being State of SCM+FSA st I is_closed_on Initialized s,P & I is_halting_on Initialized s,P holds
IC (IExec ((((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA)),P,s)) = ((card I) + (card J)) + 1
proof
let P be Instruction-Sequence of SCM+FSA; ::_thesis: for I, J being Program of SCM+FSA
for s being State of SCM+FSA st I is_closed_on Initialized s,P & I is_halting_on Initialized s,P holds
IC (IExec ((((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA)),P,s)) = ((card I) + (card J)) + 1
let I, J be Program of SCM+FSA; ::_thesis: for s being State of SCM+FSA st I is_closed_on Initialized s,P & I is_halting_on Initialized s,P holds
IC (IExec ((((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA)),P,s)) = ((card I) + (card J)) + 1
let s be State of SCM+FSA; ::_thesis: ( I is_closed_on Initialized s,P & I is_halting_on Initialized s,P implies IC (IExec ((((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA)),P,s)) = ((card I) + (card J)) + 1 )
set s2 = Initialized s;
set P2 = P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA));
assume A1: ( I is_closed_on Initialized s,P & I is_halting_on Initialized s,P ) ; ::_thesis: IC (IExec ((((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA)),P,s)) = ((card I) + (card J)) + 1
then  ( P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA)) halts_on Initialized s & LifeSpan ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Initialized s)) = (LifeSpan ((P +* I),(Initialized s))) + 2 ) by Lm6;
then  IC (Result ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Initialized s))) = IC (Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Initialized s),((LifeSpan ((P +* I),(Initialized s))) + 2))) by EXTPRO_1:23
.= ((card I) + (card J)) + 1 by A1, Lm6 ;
hence  IC (IExec ((((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA)),P,s)) = ((card I) + (card J)) + 1 by SCMFSA6B:def_1; ::_thesis: verum
end;

theorem :: SCMFSA8A:41
for P being Instruction-Sequence of SCM+FSA
for I, J being Program of SCM+FSA
for s being State of SCM+FSA st I is_closed_on Initialized s,P & I is_halting_on Initialized s,P holds
IExec ((((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA)),P,s) = (IExec (I,P,s)) +* (Start-At ((((card I) + (card J)) + 1),SCM+FSA))
proof
let P be Instruction-Sequence of SCM+FSA; ::_thesis: for I, J being Program of SCM+FSA
for s being State of SCM+FSA st I is_closed_on Initialized s,P & I is_halting_on Initialized s,P holds
IExec ((((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA)),P,s) = (IExec (I,P,s)) +* (Start-At ((((card I) + (card J)) + 1),SCM+FSA))
let I, J be Program of SCM+FSA; ::_thesis: for s being State of SCM+FSA st I is_closed_on Initialized s,P & I is_halting_on Initialized s,P holds
IExec ((((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA)),P,s) = (IExec (I,P,s)) +* (Start-At ((((card I) + (card J)) + 1),SCM+FSA))
let s be State of SCM+FSA; ::_thesis: ( I is_closed_on Initialized s,P & I is_halting_on Initialized s,P implies IExec ((((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA)),P,s) = (IExec (I,P,s)) +* (Start-At ((((card I) + (card J)) + 1),SCM+FSA)) )
set s1 = Initialized s;
set P2 = P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA));
assume that
A1: I is_closed_on Initialized s,P and
A2: I is_halting_on Initialized s,P ; ::_thesis: IExec ((((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA)),P,s) = (IExec (I,P,s)) +* (Start-At ((((card I) + (card J)) + 1),SCM+FSA))
 Initialized s = Initialize (Initialized s) by MEMSTR_0:44;
then A3: P +* I halts_on Initialized s by A2, SCMFSA7B:def_7;
 ( P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA)) halts_on Initialized s & LifeSpan ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Initialized s)) = (LifeSpan ((P +* I),(Initialized s))) + 2 ) by A1, A2, Lm6;
then A4: Result ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Initialized s)) = Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Initialized s),((LifeSpan ((P +* I),(Initialized s))) + 2)) by EXTPRO_1:23;
then  DataPart (Result ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Initialized s))) = DataPart (Comput ((P +* I),(Initialized s),(LifeSpan ((P +* I),(Initialized s))))) by A1, A2, Lm6;
then A5: DataPart (Result ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Initialized s))) = DataPart (Result ((P +* I),(Initialized s))) by A3, EXTPRO_1:23
.= DataPart ((Result ((P +* I),(Initialized s))) +* (Start-At ((((card I) + (card J)) + 1),SCM+FSA))) by MEMSTR_0:79 ;
IC (Result ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Initialized s))) = ((card I) + (card J)) + 1 by A1, A2, A4, Lm6
.= IC ((Result ((P +* I),(Initialized s))) +* (Start-At ((((card I) + (card J)) + 1),SCM+FSA))) by FUNCT_4:113 ;
then A6: Result ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Initialized s)) = (Result ((P +* I),(Initialized s))) +* (Start-At ((((card I) + (card J)) + 1),SCM+FSA)) by A5, MEMSTR_0:78;
A7: Result ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Initialized s)) = (Result ((P +* I),(Initialized s))) +* (Start-At ((((card I) + (card J)) + 1),SCM+FSA)) by A6;
thus  IExec ((((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA)),P,s) = Result ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Initialized s)) by SCMFSA6B:def_1
.= (Result ((P +* I),(Initialized s))) +* (Start-At ((((card I) + (card J)) + 1),SCM+FSA)) by A7
.= (Result ((P +* I),(Initialized s))) +* (Start-At ((((card I) + (card J)) + 1),SCM+FSA))
.= (Result ((P +* I),(Initialized s))) +* (Start-At ((((card I) + (card J)) + 1),SCM+FSA))
.= (IExec (I,P,s)) +* (Start-At ((((card I) + (card J)) + 1),SCM+FSA)) by SCMFSA6B:def_1 ; ::_thesis: verum
end;