:: SCMFSA6B semantic presentation

begin

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

definition
let I be Program of ;
let s be State of SCM+FSA;
let P be Instruction-Sequence of SCM+FSA;
func IExec (I,P,s) ->  State of SCM+FSA equals :: SCMFSA6B:def 1
 Result ((P +* I),(Initialized s));
coherence
 Result ((P +* I),(Initialized s)) is State of SCM+FSA ;
end;

:: deftheorem  defines IExec SCMFSA6B:def_1_:_
 for I being Program of
for s being State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA holds IExec (I,P,s) = Result ((P +* I),(Initialized s));

definition
let I be Program of ;
canceled;
canceled;
attrI is keeping_0  means :Def4: :: SCMFSA6B:def 4
 for s being 0 -started State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA st I c= P holds
for k being Element of NAT holds (Comput (P,s,k)) . (intloc 0) = s . (intloc 0);
end;

:: deftheorem  SCMFSA6B:def_2_:_
canceled;

:: deftheorem  SCMFSA6B:def_3_:_
canceled;

:: deftheorem Def4 defines keeping_0 SCMFSA6B:def_4_:_
 for I being Program of holds
( I is keeping_0 iff for s being 0 -started State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA st I c= P holds
for k being Element of NAT holds (Comput (P,s,k)) . (intloc 0) = s . (intloc 0) );

registration
cluster Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like V33() V51() parahalting V144() keeping_0 for set ;
existence
 ex b1 being Program of st
( b1 is parahalting & b1 is keeping_0 )
proof
take  Macro (halt SCM+FSA) ; ::_thesis: ( Macro (halt SCM+FSA) is parahalting & Macro (halt SCM+FSA) is keeping_0 )
thus  Macro (halt SCM+FSA) is parahalting ::_thesis: Macro (halt SCM+FSA) is keeping_0
proof
let s be 0 -started State of SCM+FSA; :: according to AMISTD_1:def_11 ::_thesis: for b1 being set holds
( not Macro (halt SCM+FSA) c= b1 or b1 halts_on s )
set m = Macro (halt SCM+FSA);
A1: Start-At (0,SCM+FSA) c= s by MEMSTR_0:29;
let P be Instruction-Sequence of SCM+FSA; ::_thesis: ( not Macro (halt SCM+FSA) c= P or P halts_on s )
assume A2: Macro (halt SCM+FSA) c= P ; ::_thesis: P halts_on s
 dom (Start-At (0,SCM+FSA)) = {(IC )} by FUNCOP_1:13;
then A3: IC in dom (Start-At (0,SCM+FSA)) by TARSKI:def_1;
take  0 ; :: according to EXTPRO_1:def_8 ::_thesis: ( IC (Comput (P,s,0)) in dom P & CurInstr (P,(Comput (P,s,0))) = halt SCM+FSA )
 dom (Macro (halt SCM+FSA)) = {0,1} by COMPOS_1:61;
then A4: 0 in dom (Macro (halt SCM+FSA)) by TARSKI:def_2;
 dom P = NAT by PARTFUN1:def_2;
hence  IC (Comput (P,s,0)) in dom P ; ::_thesis: CurInstr (P,(Comput (P,s,0))) = halt SCM+FSA
 dom P = NAT by PARTFUN1:def_2;
then  CurInstr (P,(Comput (P,s,0))) = P . (IC s) by PARTFUN1:def_6
.= P . (IC (Start-At (0,SCM+FSA))) by A1, A3, GRFUNC_1:2
.= P . 0 by FUNCOP_1:72
.= (Macro (halt SCM+FSA)) . 0 by A2, A4, GRFUNC_1:2
.= halt SCM+FSA by COMPOS_1:58 ;
hence  CurInstr (P,(Comput (P,s,0))) = halt SCM+FSA ; ::_thesis: verum
end;
set Mi = Macro (halt SCM+FSA);
 dom (Macro (halt SCM+FSA)) = {0,1} by COMPOS_1:61;
then A5: 0 in dom (Macro (halt SCM+FSA)) by TARSKI:def_2;
let s be 0 -started State of SCM+FSA; :: according to SCMFSA6B:def_4 ::_thesis: for P being Instruction-Sequence of SCM+FSA st Macro (halt SCM+FSA) c= P holds
for k being Element of NAT holds (Comput (P,s,k)) . (intloc 0) = s . (intloc 0)
A6: Start-At (0,SCM+FSA) c= s by MEMSTR_0:29;
let P be Instruction-Sequence of SCM+FSA; ::_thesis: ( Macro (halt SCM+FSA) c= P implies for k being Element of NAT holds (Comput (P,s,k)) . (intloc 0) = s . (intloc 0) )
assume A7: Macro (halt SCM+FSA) c= P ; ::_thesis: for k being Element of NAT holds (Comput (P,s,k)) . (intloc 0) = s . (intloc 0)
let k be Element of NAT ; ::_thesis: (Comput (P,s,k)) . (intloc 0) = s . (intloc 0)
A8: s = Comput (P,s,0) ;
 dom P = NAT by PARTFUN1:def_2;
then A9: P /. (IC s) = P . (IC s) by PARTFUN1:def_6;
CurInstr (P,s) = P . 0 by A6, A9, MEMSTR_0:39
.= (Macro (halt SCM+FSA)) . 0 by A5, A7, GRFUNC_1:2
.= halt SCM+FSA by COMPOS_1:58 ;
hence  (Comput (P,s,k)) . (intloc 0) = s . (intloc 0) by A8, EXTPRO_1:5; ::_thesis: verum
end;
end;

theorem Th1: :: SCMFSA6B:1
for s being 0 -started State of SCM+FSA
for I being parahalting Program of
for P being Instruction-Sequence of SCM+FSA st I c= P holds
P halts_on s by AMISTD_1:def_11;

theorem Th2: :: SCMFSA6B:2
for s being State of SCM+FSA
for I being parahalting Program of st Initialize ((intloc 0) .--> 1) c= s holds
for P being Instruction-Sequence of SCM+FSA st I c= P holds
P halts_on s
proof
let s be State of SCM+FSA; ::_thesis: for I being parahalting Program of st Initialize ((intloc 0) .--> 1) c= s holds
for P being Instruction-Sequence of SCM+FSA st I c= P holds
P halts_on s
let I be parahalting Program of ; ::_thesis: ( Initialize ((intloc 0) .--> 1) c= s implies for P being Instruction-Sequence of SCM+FSA st I c= P holds
P halts_on s )
A1: Start-At (0,SCM+FSA) c= Initialize ((intloc 0) .--> 1) by FUNCT_4:25;
assume A2: Initialize ((intloc 0) .--> 1) c= s ; ::_thesis: for P being Instruction-Sequence of SCM+FSA st I c= P holds
P halts_on s
let P be Instruction-Sequence of SCM+FSA; ::_thesis: ( I c= P implies P halts_on s )
assume A3: I c= P ; ::_thesis: P halts_on s
 Start-At (0,SCM+FSA) c= s by A2, A1, XBOOLE_1:1;
then  s is 0 -started by MEMSTR_0:29;
hence  P halts_on s by A3, AMISTD_1:def_11; ::_thesis: verum
end;

Lm1:  for s being State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA holds not P +* ((IC s),(goto (IC s))) halts_on s
proof
let s be State of SCM+FSA; ::_thesis: for P being Instruction-Sequence of SCM+FSA holds not P +* ((IC s),(goto (IC s))) halts_on s
let P be Instruction-Sequence of SCM+FSA; ::_thesis: not P +* ((IC s),(goto (IC s))) halts_on s
set Q = P +* ((IC s),(goto (IC s)));
defpred S1[ Nat] means  IC (Comput ((P +* ((IC s),(goto (IC s)))),s,$1)) = IC s;
A1: dom P = NAT by PARTFUN1:def_2;
A2: dom P = dom (P +* ((IC s),(goto (IC s)))) by FUNCT_7:30;
A3: now__::_thesis:_for_n_being_Element_of_NAT_st_S1[n]_holds_
S1[n_+_1]
let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] )
assume  S1[n] ; ::_thesis: S1[n + 1]
then A4: CurInstr ((P +* ((IC s),(goto (IC s)))),(Comput ((P +* ((IC s),(goto (IC s)))),s,n))) = (P +* ((IC s),(goto (IC s)))) . (IC s) by A2, A1, PARTFUN1:def_6
.= goto (IC s) by A1, FUNCT_7:31 ;
IC (Comput ((P +* ((IC s),(goto (IC s)))),s,(n + 1))) = IC (Following ((P +* ((IC s),(goto (IC s)))),(Comput ((P +* ((IC s),(goto (IC s)))),s,n)))) by EXTPRO_1:3
.= IC s by A4, SCMFSA_2:69 ;
hence  S1[n + 1] ; ::_thesis: verum
end;
let n be Nat; :: according to EXTPRO_1:def_8 ::_thesis: ( not IC (Comput ((P +* ((IC s),(goto (IC s)))),s,n)) in dom (P +* ((IC s),(goto (IC s)))) or not CurInstr ((P +* ((IC s),(goto (IC s)))),(Comput ((P +* ((IC s),(goto (IC s)))),s,n))) = halt SCM+FSA )
A5: S1[ 0 ] ;
assume A6: IC (Comput ((P +* ((IC s),(goto (IC s)))),s,n)) in dom (P +* ((IC s),(goto (IC s)))) ; ::_thesis: not CurInstr ((P +* ((IC s),(goto (IC s)))),(Comput ((P +* ((IC s),(goto (IC s)))),s,n))) = halt SCM+FSA
reconsider n = n as Element of NAT by ORDINAL1:def_12;
A7: for n being Element of NAT holds S1[n] from NAT_1:sch_1(A5, A3);
CurInstr ((P +* ((IC s),(goto (IC s)))),(Comput ((P +* ((IC s),(goto (IC s)))),s,n))) = (P +* ((IC s),(goto (IC s)))) . (IC (Comput ((P +* ((IC s),(goto (IC s)))),s,n))) by A6, PARTFUN1:def_6
.= (P +* ((IC s),(goto (IC s)))) . (IC s) by A7
.= goto (IC s) by A1, FUNCT_7:31 ;
hence  not CurInstr ((P +* ((IC s),(goto (IC s)))),(Comput ((P +* ((IC s),(goto (IC s)))),s,n))) = halt SCM+FSA ; ::_thesis: verum
end;

registration
cluster Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like V33() V51() parahalting  ->  paraclosed for set ;
coherence
 for b1 being Program of st b1 is parahalting holds
b1 is paraclosed
proof
let I be Program of ; ::_thesis: ( I is parahalting implies I is paraclosed )
assume A1: I is parahalting ; ::_thesis: I is paraclosed
let s be 0 -started State of SCM+FSA; :: according to AMISTD_1:def_10 ::_thesis: for b1 being set holds
( not I c= b1 or for b2 being Element of NAT holds IC (Comput (b1,s,b2)) in K306(NAT,I) )
let P be Instruction-Sequence of SCM+FSA; ::_thesis: ( not I c= P or for b1 being Element of NAT holds IC (Comput (P,s,b1)) in K306(NAT,I) )
assume A2: I c= P ; ::_thesis: for b1 being Element of NAT holds IC (Comput (P,s,b1)) in K306(NAT,I)
let n be Element of NAT ; ::_thesis: IC (Comput (P,s,n)) in K306(NAT,I)
defpred S1[ Nat] means  not IC (Comput (P,s,c1)) in dom I;
assume  not IC (Comput (P,s,n)) in dom I ; ::_thesis: contradiction
then A3: ex n being Nat st S1[n] ;
consider n being Nat such that
A4: S1[n] and
A5: for m being Nat st S1[m] holds
n <= m from NAT_1:sch_5(A3);
reconsider n = n as Element of NAT by ORDINAL1:def_12;
A6: for m being Element of NAT st m < n holds
IC (Comput (P,s,m)) in dom I by A5;
set s2 = Comput (P,s,n);
set s0 = s;
set s1 = Comput (P,s,n);
set P0 = P +* ((IC (Comput (P,s,n))),(goto (IC (Comput (P,s,n)))));
A7: I c= P +* ((IC (Comput (P,s,n))),(goto (IC (Comput (P,s,n))))) by A4, A2, FUNCT_7:89;
then A8: Comput ((P +* ((IC (Comput (P,s,n))),(goto (IC (Comput (P,s,n)))))),s,n) = Comput (P,s,n) by A6, A2, AMISTD_2:10;
A9: not P +* ((IC (Comput (P,s,n))),(goto (IC (Comput (P,s,n))))) halts_on Comput ((P +* ((IC (Comput (P,s,n))),(goto (IC (Comput (P,s,n)))))),s,n) by A8, Lm1;
 P +* ((IC (Comput (P,s,n))),(goto (IC (Comput (P,s,n))))) halts_on s by A7, A1, AMISTD_1:def_11;
hence  contradiction by A9, EXTPRO_1:22; ::_thesis: verum
end;
cluster Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like V33() V51() keeping_0  ->  paraclosed for set ;
coherence
 for b1 being Program of st b1 is keeping_0 holds
b1 is paraclosed
proof
let I be Program of ; ::_thesis: ( I is keeping_0 implies I is paraclosed )
assume A10: I is keeping_0 ; ::_thesis: I is paraclosed
set FI = FirstNotUsed I;
let s be 0 -started State of SCM+FSA; :: according to AMISTD_1:def_10 ::_thesis: for b1 being set holds
( not I c= b1 or for b2 being Element of NAT holds IC (Comput (b1,s,b2)) in K306(NAT,I) )
let P be Instruction-Sequence of SCM+FSA; ::_thesis: ( not I c= P or for b1 being Element of NAT holds IC (Comput (P,s,b1)) in K306(NAT,I) )
assume A11: I c= P ; ::_thesis: for b1 being Element of NAT holds IC (Comput (P,s,b1)) in K306(NAT,I)
let n be Element of NAT ; ::_thesis: IC (Comput (P,s,n)) in K306(NAT,I)
A12: Start-At (0,SCM+FSA) c= s by MEMSTR_0:29;
defpred S1[ Nat] means  not IC (Comput (P,s,c1)) in dom I;
assume  not IC (Comput (P,s,n)) in dom I ; ::_thesis: contradiction
then A13: ex n being Nat st S1[n] ;
consider n being Nat such that
A14: S1[n] and
A15: for m being Nat st S1[m] holds
n <= m from NAT_1:sch_5(A13);
reconsider n = n as Element of NAT by ORDINAL1:def_12;
set s2 = Comput (P,s,n);
set s00 = s;
reconsider s0 = s +* ((FirstNotUsed I),((s . (intloc 0)) + 1)) as State of SCM+FSA ;
set Q = P +* ((IC (Comput (P,s,n))),((intloc 0) := (FirstNotUsed I)));
A16: dom (P +* ((IC (Comput (P,s,n))),((intloc 0) := (FirstNotUsed I)))) = NAT by PARTFUN1:def_2;
 not I is keeping_0
proof
 not FirstNotUsed I in UsedInt*Loc I
proof
assume  FirstNotUsed I in UsedInt*Loc I ; ::_thesis: contradiction
then  FirstNotUsed I in FinSeq-Locations ;
then  FirstNotUsed I is FinSeq-Location by SCMFSA_2:def_5;
hence  contradiction by SCMFSA_2:58; ::_thesis: verum
end;
then A17: s0 | (UsedInt*Loc I) = s | (UsedInt*Loc I) by FUNCT_7:92;
A18: s . (intloc 0) < (s . (intloc 0)) + 1 by XREAL_1:29;
A19: dom P = NAT by PARTFUN1:def_2;
A20: (P +* ((IC (Comput (P,s,n))),((intloc 0) := (FirstNotUsed I)))) . (IC (Comput (P,s,n))) = (intloc 0) := (FirstNotUsed I) by A19, FUNCT_7:31;
A21: s0 . (intloc 0) = s . (intloc 0) by FUNCT_7:32;
 FirstNotUsed I in dom s by SCMFSA_2:42;
then A22: s0 . (FirstNotUsed I) = (s . (intloc 0)) + 1 by FUNCT_7:31;
set s02 = Comput ((P +* ((IC (Comput (P,s,n))),((intloc 0) := (FirstNotUsed I)))),s0,n);
 FirstNotUsed I <> IC by SCMFSA_2:56;
then  not FirstNotUsed I in {(IC )} by TARSKI:def_1;
then  not FirstNotUsed I in dom (Start-At (0,SCM+FSA)) by FUNCOP_1:13;
then A23: Start-At (0,SCM+FSA) c= s0 by A12, FUNCT_7:89;
then reconsider s0 = s0 as 0 -started State of SCM+FSA by MEMSTR_0:29;
take  s0 ; :: according to SCMFSA6B:def_4 ::_thesis: ex P being Instruction-Sequence of SCM+FSA st
( I c= P & not  for k being Element of NAT holds (Comput (P,s0,k)) . (intloc 0) = s0 . (intloc 0) )
A24: I c= P +* ((IC (Comput (P,s,n))),((intloc 0) := (FirstNotUsed I))) by A11, A14, FUNCT_7:138;
take  P +* ((IC (Comput (P,s,n))),((intloc 0) := (FirstNotUsed I))) ; ::_thesis: ( I c= P +* ((IC (Comput (P,s,n))),((intloc 0) := (FirstNotUsed I))) & not  for k being Element of NAT holds (Comput ((P +* ((IC (Comput (P,s,n))),((intloc 0) := (FirstNotUsed I)))),s0,k)) . (intloc 0) = s0 . (intloc 0) )
thus  I c= P +* ((IC (Comput (P,s,n))),((intloc 0) := (FirstNotUsed I))) by A11, A14, FUNCT_7:138; ::_thesis: not  for k being Element of NAT holds (Comput ((P +* ((IC (Comput (P,s,n))),((intloc 0) := (FirstNotUsed I)))),s0,k)) . (intloc 0) = s0 . (intloc 0)
take k = n + 1; ::_thesis: not (Comput ((P +* ((IC (Comput (P,s,n))),((intloc 0) := (FirstNotUsed I)))),s0,k)) . (intloc 0) = s0 . (intloc 0)
A25: s0 | (UsedIntLoc I) = s | (UsedIntLoc I) by FUNCT_7:92, SF_MASTR:50;
A26: for m being Element of NAT st m < n holds
IC (Comput (P,s,m)) in dom I by A15;
A27: ( not FirstNotUsed I in UsedIntLoc I & ( for m being Element of NAT st m < n holds
IC (Comput ((P +* ((IC (Comput (P,s,n))),((intloc 0) := (FirstNotUsed I)))),s0,m)) in dom I ) ) by A26, A25, A17, A11, A24, A12, A23, SF_MASTR:50, SF_MASTR:65;
A28: (Comput ((P +* ((IC (Comput (P,s,n))),((intloc 0) := (FirstNotUsed I)))),s0,n)) . (FirstNotUsed I) = (s . (intloc 0)) + 1 by A22, A27, A24, SF_MASTR:61;
Comput ((P +* ((IC (Comput (P,s,n))),((intloc 0) := (FirstNotUsed I)))),s0,k) = Following ((P +* ((IC (Comput (P,s,n))),((intloc 0) := (FirstNotUsed I)))),(Comput ((P +* ((IC (Comput (P,s,n))),((intloc 0) := (FirstNotUsed I)))),s0,n))) by EXTPRO_1:3
.= Exec (((P +* ((IC (Comput (P,s,n))),((intloc 0) := (FirstNotUsed I)))) . (IC (Comput ((P +* ((IC (Comput (P,s,n))),((intloc 0) := (FirstNotUsed I)))),s0,n)))),(Comput ((P +* ((IC (Comput (P,s,n))),((intloc 0) := (FirstNotUsed I)))),s0,n))) by A16, PARTFUN1:def_6
.= Exec (((intloc 0) := (FirstNotUsed I)),(Comput ((P +* ((IC (Comput (P,s,n))),((intloc 0) := (FirstNotUsed I)))),s0,n))) by A25, A17, A11, A24, A26, A20, A12, A23, SF_MASTR:65 ;
hence  not (Comput ((P +* ((IC (Comput (P,s,n))),((intloc 0) := (FirstNotUsed I)))),s0,k)) . (intloc 0) = s0 . (intloc 0) by A28, A21, A18, SCMFSA_2:63; ::_thesis: verum
end;
hence  contradiction by A10; ::_thesis: verum
end;
end;

theorem :: SCMFSA6B:3
for s being State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA
for I being parahalting Program of
for a being read-write Int-Location st not a in UsedIntLoc I holds
(IExec (I,P,s)) . a = s . a
proof
let s be State of SCM+FSA; ::_thesis: for P being Instruction-Sequence of SCM+FSA
for I being parahalting Program of
for a being read-write Int-Location st not a in UsedIntLoc I holds
(IExec (I,P,s)) . a = s . a
let P be Instruction-Sequence of SCM+FSA; ::_thesis: for I being parahalting Program of
for a being read-write Int-Location st not a in UsedIntLoc I holds
(IExec (I,P,s)) . a = s . a
let I be parahalting Program of ; ::_thesis: for a being read-write Int-Location st not a in UsedIntLoc I holds
(IExec (I,P,s)) . a = s . a
let a be read-write Int-Location; ::_thesis: ( not a in UsedIntLoc I implies (IExec (I,P,s)) . a = s . a )
assume A1: not a in UsedIntLoc I ; ::_thesis: (IExec (I,P,s)) . a = s . a
A2: I c= P +* I by FUNCT_4:25;
 Initialize ((intloc 0) .--> 1) c= s +* (Initialize ((intloc 0) .--> 1)) by FUNCT_4:25;
then  P +* I halts_on s +* (Initialize ((intloc 0) .--> 1)) by Th2, A2;
then consider n being Element of NAT  such that
A3: Result ((P +* I),(s +* (Initialize ((intloc 0) .--> 1)))) = Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),n) and
 CurInstr ((P +* I),(Result ((P +* I),(s +* (Initialize ((intloc 0) .--> 1)))))) = halt SCM+FSA by EXTPRO_1:def_9;
A4: dom (Initialize ((intloc 0) .--> 1)) = (dom ((intloc 0) .--> 1)) \/ (dom (Start-At (0,SCM+FSA))) by FUNCT_4:def_1;
A5: not a in dom (Start-At (0,SCM+FSA)) by SCMFSA_2:102;
 not a in {(intloc 0)} by TARSKI:def_1;
then  not a in dom ((intloc 0) .--> 1) by FUNCOP_1:13;
then A6: not a in dom (Initialize ((intloc 0) .--> 1)) by A4, A5, XBOOLE_0:def_3;
 for m being Element of NAT st m < n holds
IC (Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),m)) in dom I by A2, AMISTD_1:def_10;
hence (IExec (I,P,s)) . a = (s +* (Initialize ((intloc 0) .--> 1))) . a by A1, A3, FUNCT_4:25, SF_MASTR:61
.= s . a by A6, FUNCT_4:11 ;
::_thesis: verum
end;

theorem :: SCMFSA6B:4
for f being FinSeq-Location
for s being State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA
for I being parahalting Program of st not f in UsedInt*Loc I holds
(IExec (I,P,s)) . f = s . f
proof
let f be FinSeq-Location ; ::_thesis: for s being State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA
for I being parahalting Program of st not f in UsedInt*Loc I holds
(IExec (I,P,s)) . f = s . f
let s be State of SCM+FSA; ::_thesis: for P being Instruction-Sequence of SCM+FSA
for I being parahalting Program of st not f in UsedInt*Loc I holds
(IExec (I,P,s)) . f = s . f
let P be Instruction-Sequence of SCM+FSA; ::_thesis: for I being parahalting Program of st not f in UsedInt*Loc I holds
(IExec (I,P,s)) . f = s . f
let I be parahalting Program of ; ::_thesis: ( not f in UsedInt*Loc I implies (IExec (I,P,s)) . f = s . f )
assume A1: not f in UsedInt*Loc I ; ::_thesis: (IExec (I,P,s)) . f = s . f
A2: I c= P +* I by FUNCT_4:25;
 Initialize ((intloc 0) .--> 1) c= s +* (Initialize ((intloc 0) .--> 1)) by FUNCT_4:25;
then  P +* I halts_on s +* (Initialize ((intloc 0) .--> 1)) by Th2, A2;
then consider n being Element of NAT  such that
A3: Result ((P +* I),(s +* (Initialize ((intloc 0) .--> 1)))) = Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),n) and
 CurInstr ((P +* I),(Result ((P +* I),(s +* (Initialize ((intloc 0) .--> 1)))))) = halt SCM+FSA by EXTPRO_1:def_9;
A4: dom (Initialize ((intloc 0) .--> 1)) = (dom ((intloc 0) .--> 1)) \/ (dom (Start-At (0,SCM+FSA))) by FUNCT_4:def_1;
A5: not f in dom (Start-At (0,SCM+FSA)) by SCMFSA_2:103;
 f <> intloc 0 by SCMFSA_2:58;
then  not f in {(intloc 0)} by TARSKI:def_1;
then  not f in dom ((intloc 0) .--> 1) by FUNCOP_1:13;
then A6: not f in dom (Initialize ((intloc 0) .--> 1)) by A4, A5, XBOOLE_0:def_3;
 for m being Element of NAT st m < n holds
IC (Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),m)) in dom I by A2, AMISTD_1:def_10;
hence (IExec (I,P,s)) . f = (s +* (Initialize ((intloc 0) .--> 1))) . f by A1, A3, FUNCT_4:25, SF_MASTR:63
.= s . f by A6, FUNCT_4:11 ;
::_thesis: verum
end;

theorem :: SCMFSA6B:5
for l being Element of NAT
for s being State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA st IC s = l & P . l = goto l holds
not P halts_on s
proof
let l be Element of NAT ; ::_thesis: for s being State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA st IC s = l & P . l = goto l holds
not P halts_on s
let s be State of SCM+FSA; ::_thesis: for P being Instruction-Sequence of SCM+FSA st IC s = l & P . l = goto l holds
not P halts_on s
let P be Instruction-Sequence of SCM+FSA; ::_thesis: ( IC s = l & P . l = goto l implies not P halts_on s )
assume that
A1: IC s = l and
A2: P . l = goto l ; ::_thesis: not P halts_on s
A3: P /. (IC s) = P . (IC s) by PBOOLE:143;
defpred S1[ Nat] means  Comput (P,s,$1) = s;
A4: for m being Element of NAT st S1[m] holds
S1[m + 1]
proof
let m be Element of NAT ; ::_thesis: ( S1[m] implies S1[m + 1] )
A5: for f being FinSeq-Location holds (Exec ((goto l),s)) . f = s . f by SCMFSA_2:69;
A6: ( IC (Exec ((goto l),s)) = IC s & ( for a being Int-Location holds (Exec ((goto l),s)) . a = s . a ) ) by A1, SCMFSA_2:69;
assume A7: Comput (P,s,m) = s ; ::_thesis: S1[m + 1]
thus  Comput (P,s,(m + 1)) = Following (P,s) by A7, EXTPRO_1:3
.= s by A1, A2, A6, A5, A3, SCMFSA_2:104 ; ::_thesis: verum
end;
let mm be Nat; :: according to EXTPRO_1:def_8 ::_thesis: ( not IC (Comput (P,s,mm)) in dom P or not CurInstr (P,(Comput (P,s,mm))) = halt SCM+FSA )
reconsider m = mm as Element of NAT by ORDINAL1:def_12;
A8: S1[ 0 ] ;
 for m being Element of NAT holds S1[m] from NAT_1:sch_1(A8, A4);
then A9: S1[m] ;
assume  IC (Comput (P,s,mm)) in dom P ; ::_thesis: not CurInstr (P,(Comput (P,s,mm))) = halt SCM+FSA
thus  CurInstr (P,(Comput (P,s,mm))) <> halt SCM+FSA by A1, A2, A9, PBOOLE:143; ::_thesis: verum
end;

registration
cluster Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like V33() V51() parahalting  ->  for set ;
coherence
 for b1 being Program of st b1 is parahalting holds
not b1 is empty ;
end;

theorem Th6: :: SCMFSA6B:6
for s2 being State of SCM+FSA
for s1 being 0 -started State of SCM+FSA
for P, Q being Instruction-Sequence of SCM+FSA
for J being parahalting Program of st J c= P holds
for n being Element of NAT st Reloc (J,n) c= Q & IC s2 = n & DataPart s1 = DataPart s2 holds
for i being Element of NAT holds
( (IC (Comput (P,s1,i))) + n = IC (Comput (Q,s2,i)) & IncAddr ((CurInstr (P,(Comput (P,s1,i)))),n) = CurInstr (Q,(Comput (Q,s2,i))) & DataPart (Comput (P,s1,i)) = DataPart (Comput (Q,s2,i)) )
proof
let s2 be State of SCM+FSA; ::_thesis: for s1 being 0 -started State of SCM+FSA
for P, Q being Instruction-Sequence of SCM+FSA
for J being parahalting Program of st J c= P holds
for n being Element of NAT st Reloc (J,n) c= Q & IC s2 = n & DataPart s1 = DataPart s2 holds
for i being Element of NAT holds
( (IC (Comput (P,s1,i))) + n = IC (Comput (Q,s2,i)) & IncAddr ((CurInstr (P,(Comput (P,s1,i)))),n) = CurInstr (Q,(Comput (Q,s2,i))) & DataPart (Comput (P,s1,i)) = DataPart (Comput (Q,s2,i)) )
let s1 be 0 -started State of SCM+FSA; ::_thesis: for P, Q being Instruction-Sequence of SCM+FSA
for J being parahalting Program of st J c= P holds
for n being Element of NAT st Reloc (J,n) c= Q & IC s2 = n & DataPart s1 = DataPart s2 holds
for i being Element of NAT holds
( (IC (Comput (P,s1,i))) + n = IC (Comput (Q,s2,i)) & IncAddr ((CurInstr (P,(Comput (P,s1,i)))),n) = CurInstr (Q,(Comput (Q,s2,i))) & DataPart (Comput (P,s1,i)) = DataPart (Comput (Q,s2,i)) )
let P, Q be Instruction-Sequence of SCM+FSA; ::_thesis: for J being parahalting Program of st J c= P holds
for n being Element of NAT st Reloc (J,n) c= Q & IC s2 = n & DataPart s1 = DataPart s2 holds
for i being Element of NAT holds
( (IC (Comput (P,s1,i))) + n = IC (Comput (Q,s2,i)) & IncAddr ((CurInstr (P,(Comput (P,s1,i)))),n) = CurInstr (Q,(Comput (Q,s2,i))) & DataPart (Comput (P,s1,i)) = DataPart (Comput (Q,s2,i)) )
let J be parahalting Program of ; ::_thesis: ( J c= P implies for n being Element of NAT st Reloc (J,n) c= Q & IC s2 = n & DataPart s1 = DataPart s2 holds
for i being Element of NAT holds
( (IC (Comput (P,s1,i))) + n = IC (Comput (Q,s2,i)) & IncAddr ((CurInstr (P,(Comput (P,s1,i)))),n) = CurInstr (Q,(Comput (Q,s2,i))) & DataPart (Comput (P,s1,i)) = DataPart (Comput (Q,s2,i)) ) )
A1: Start-At (0,SCM+FSA) c= s1 by MEMSTR_0:29;
assume A2: J c= P ; ::_thesis: for n being Element of NAT st Reloc (J,n) c= Q & IC s2 = n & DataPart s1 = DataPart s2 holds
for i being Element of NAT holds
( (IC (Comput (P,s1,i))) + n = IC (Comput (Q,s2,i)) & IncAddr ((CurInstr (P,(Comput (P,s1,i)))),n) = CurInstr (Q,(Comput (Q,s2,i))) & DataPart (Comput (P,s1,i)) = DataPart (Comput (Q,s2,i)) )
set JAt = Start-At (0,SCM+FSA);
A3: 0 in dom J by AFINSQ_1:65;
A4: IC in dom (Start-At (0,SCM+FSA)) by MEMSTR_0:15;
then A5: P . (IC s1) = P . (IC (Start-At (0,SCM+FSA))) by A1, GRFUNC_1:2
.= P . 0 by FUNCOP_1:72
.= J . 0 by A3, A2, GRFUNC_1:2 ;
A6: IC (Comput (P,s1,0)) = IC s1
.= IC (Start-At (0,SCM+FSA)) by A1, A4, GRFUNC_1:2
.= 0 by FUNCOP_1:72 ;
A7: 0 in dom J by AFINSQ_1:65;
let n be Element of NAT ; ::_thesis: ( Reloc (J,n) c= Q & IC s2 = n & DataPart s1 = DataPart s2 implies for i being Element of NAT holds
( (IC (Comput (P,s1,i))) + n = IC (Comput (Q,s2,i)) & IncAddr ((CurInstr (P,(Comput (P,s1,i)))),n) = CurInstr (Q,(Comput (Q,s2,i))) & DataPart (Comput (P,s1,i)) = DataPart (Comput (Q,s2,i)) ) )
assume that
A8: Reloc (J,n) c= Q and
A9: IC s2 = n and
A10: DataPart s1 = DataPart s2 ; ::_thesis: for i being Element of NAT holds
( (IC (Comput (P,s1,i))) + n = IC (Comput (Q,s2,i)) & IncAddr ((CurInstr (P,(Comput (P,s1,i)))),n) = CurInstr (Q,(Comput (Q,s2,i))) & DataPart (Comput (P,s1,i)) = DataPart (Comput (Q,s2,i)) )
A11: DataPart (Comput (P,s1,0)) = DataPart s2 by A10
.= DataPart (Comput (Q,s2,0)) ;
defpred S1[ Nat] means ( (IC (Comput (P,s1,$1))) + n = IC (Comput (Q,s2,$1)) & IncAddr ((CurInstr (P,(Comput (P,s1,$1)))),n) = CurInstr (Q,(Comput (Q,s2,$1))) & DataPart (Comput (P,s1,$1)) = DataPart (Comput (Q,s2,$1)) );
A12: for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
A13: Comput (P,s1,(k + 1)) = Following (P,(Comput (P,s1,k))) by EXTPRO_1:3
.= Exec ((CurInstr (P,(Comput (P,s1,k)))),(Comput (P,s1,k))) ;
reconsider l = IC (Comput (P,s1,(k + 1))) as Element of NAT ;
reconsider j = CurInstr (P,(Comput (P,s1,(k + 1)))) as Instruction of SCM+FSA ;
A14: Comput (Q,s2,(k + 1)) = Following (Q,(Comput (Q,s2,k))) by EXTPRO_1:3
.= Exec ((CurInstr (Q,(Comput (Q,s2,k)))),(Comput (Q,s2,k))) ;
A15: IC (Comput (P,s1,(k + 1))) in dom J by A2, AMISTD_1:def_10;
assume A16: S1[k] ; ::_thesis: S1[k + 1]
hence  (IC (Comput (P,s1,(k + 1)))) + n = IC (Comput (Q,s2,(k + 1))) by A13, A14, SCMFSA6A:8; ::_thesis: ( IncAddr ((CurInstr (P,(Comput (P,s1,(k + 1))))),n) = CurInstr (Q,(Comput (Q,s2,(k + 1)))) & DataPart (Comput (P,s1,(k + 1))) = DataPart (Comput (Q,s2,(k + 1))) )
then A17: IC (Comput (Q,s2,(k + 1))) in dom (Reloc (J,n)) by A15, COMPOS_1:46;
A18: l in dom J by A2, AMISTD_1:def_10;
A19: dom P = NAT by PARTFUN1:def_2;
A20: dom Q = NAT by PARTFUN1:def_2;
j = P . (IC (Comput (P,s1,(k + 1)))) by A19, PARTFUN1:def_6
.= J . l by A15, A2, GRFUNC_1:2 ;
hence  IncAddr ((CurInstr (P,(Comput (P,s1,(k + 1))))),n) = (Reloc (J,n)) . (l + n) by A18, COMPOS_1:35
.= (Reloc (J,n)) . (IC (Comput (Q,s2,(k + 1)))) by A16, A13, A14, SCMFSA6A:8
.= Q . (IC (Comput (Q,s2,(k + 1)))) by A17, A8, GRFUNC_1:2
.= CurInstr (Q,(Comput (Q,s2,(k + 1)))) by A20, PARTFUN1:def_6 ;
::_thesis: DataPart (Comput (P,s1,(k + 1))) = DataPart (Comput (Q,s2,(k + 1)))
thus  DataPart (Comput (P,s1,(k + 1))) = DataPart (Comput (Q,s2,(k + 1))) by A16, A13, A14, SCMFSA6A:8; ::_thesis: verum
end;
let i be Element of NAT ; ::_thesis: ( (IC (Comput (P,s1,i))) + n = IC (Comput (Q,s2,i)) & IncAddr ((CurInstr (P,(Comput (P,s1,i)))),n) = CurInstr (Q,(Comput (Q,s2,i))) & DataPart (Comput (P,s1,i)) = DataPart (Comput (Q,s2,i)) )
 0 in dom J by AFINSQ_1:65;
then A21: 0 + n in dom (Reloc (J,n)) by COMPOS_1:46;
A22: dom Q = NAT by PARTFUN1:def_2;
 dom P = NAT by PARTFUN1:def_2;
then  IncAddr ((CurInstr (P,(Comput (P,s1,0)))),n) = (Reloc (J,n)) . (0 + n) by A5, A7, COMPOS_1:35, PARTFUN1:def_6
.= Q . (IC (Comput (Q,s2,0))) by A9, A21, A8, GRFUNC_1:2
.= CurInstr (Q,(Comput (Q,s2,0))) by A22, PARTFUN1:def_6 ;
then A23: S1[ 0 ] by A9, A6, A11;
 for k being Element of NAT holds S1[k] from NAT_1:sch_1(A23, A12);
hence  ( (IC (Comput (P,s1,i))) + n = IC (Comput (Q,s2,i)) & IncAddr ((CurInstr (P,(Comput (P,s1,i)))),n) = CurInstr (Q,(Comput (Q,s2,i))) & DataPart (Comput (P,s1,i)) = DataPart (Comput (Q,s2,i)) ) ; ::_thesis: verum
end;

theorem Th7: :: SCMFSA6B:7
for P1, P2 being Instruction-Sequence of SCM+FSA
for s being 0 -started State of SCM+FSA
for I being parahalting Program of st I c= P1 & I c= P2 holds
for k being Element of NAT holds
( Comput (P1,s,k) = Comput (P2,s,k) & CurInstr (P1,(Comput (P1,s,k))) = CurInstr (P2,(Comput (P2,s,k))) )
proof
let P1, P2 be Instruction-Sequence of SCM+FSA; ::_thesis: for s being 0 -started State of SCM+FSA
for I being parahalting Program of st I c= P1 & I c= P2 holds
for k being Element of NAT holds
( Comput (P1,s,k) = Comput (P2,s,k) & CurInstr (P1,(Comput (P1,s,k))) = CurInstr (P2,(Comput (P2,s,k))) )
let s be 0 -started State of SCM+FSA; ::_thesis: for I being parahalting Program of st I c= P1 & I c= P2 holds
for k being Element of NAT holds
( Comput (P1,s,k) = Comput (P2,s,k) & CurInstr (P1,(Comput (P1,s,k))) = CurInstr (P2,(Comput (P2,s,k))) )
let I be parahalting Program of ; ::_thesis: ( I c= P1 & I c= P2 implies for k being Element of NAT holds
( Comput (P1,s,k) = Comput (P2,s,k) & CurInstr (P1,(Comput (P1,s,k))) = CurInstr (P2,(Comput (P2,s,k))) ) )
assume that
A1: I c= P1 and
A2: I c= P2 ; ::_thesis: for k being Element of NAT holds
( Comput (P1,s,k) = Comput (P2,s,k) & CurInstr (P1,(Comput (P1,s,k))) = CurInstr (P2,(Comput (P2,s,k))) )
hereby  ::_thesis: verum
let k be Element of NAT ; ::_thesis: ( Comput (P1,s,k) = Comput (P2,s,k) & CurInstr (P2,(Comput (P2,s,k))) = CurInstr (P1,(Comput (P1,s,k))) )
A3: IC (Comput (P1,s,k)) in dom I by A1, AMISTD_1:def_10;
A4: IC (Comput (P2,s,k)) in dom I by A2, AMISTD_1:def_10;
 for m being Element of NAT st m < k holds
IC (Comput (P2,s,m)) in dom I by A2, AMISTD_1:def_10;
hence A5: Comput (P1,s,k) = Comput (P2,s,k) by A1, A2, AMISTD_2:10; ::_thesis: CurInstr (P2,(Comput (P2,s,k))) = CurInstr (P1,(Comput (P1,s,k)))
thus  CurInstr (P2,(Comput (P2,s,k))) = P2 . (IC (Comput (P2,s,k))) by PBOOLE:143
.= I . (IC (Comput (P2,s,k))) by A4, A2, GRFUNC_1:2
.= P1 . (IC (Comput (P1,s,k))) by A5, A3, A1, GRFUNC_1:2
.= CurInstr (P1,(Comput (P1,s,k))) by PBOOLE:143 ; ::_thesis: verum
end;
end;

theorem Th8: :: SCMFSA6B:8
for P1, P2 being Instruction-Sequence of SCM+FSA
for s being 0 -started State of SCM+FSA
for I being parahalting Program of st I c= P1 & I c= P2 holds
( LifeSpan (P1,s) = LifeSpan (P2,s) & Result (P1,s) = Result (P2,s) )
proof
let P1, P2 be Instruction-Sequence of SCM+FSA; ::_thesis: for s being 0 -started State of SCM+FSA
for I being parahalting Program of st I c= P1 & I c= P2 holds
( LifeSpan (P1,s) = LifeSpan (P2,s) & Result (P1,s) = Result (P2,s) )
let s be 0 -started State of SCM+FSA; ::_thesis: for I being parahalting Program of st I c= P1 & I c= P2 holds
( LifeSpan (P1,s) = LifeSpan (P2,s) & Result (P1,s) = Result (P2,s) )
let I be parahalting Program of ; ::_thesis: ( I c= P1 & I c= P2 implies ( LifeSpan (P1,s) = LifeSpan (P2,s) & Result (P1,s) = Result (P2,s) ) )
assume that
A1: I c= P1 and
A2: I c= P2 ; ::_thesis: ( LifeSpan (P1,s) = LifeSpan (P2,s) & Result (P1,s) = Result (P2,s) )
A3: P2 halts_on s by A2, AMISTD_1:def_11;
A4: P1 halts_on s by A1, AMISTD_1:def_11;
A5: now__::_thesis:_for_l_being_Element_of_NAT_st_CurInstr_(P2,(Comput_(P2,s,l)))_=_halt_SCM+FSA_holds_
LifeSpan_(P1,s)_<=_l
let l be Element of NAT ; ::_thesis: ( CurInstr (P2,(Comput (P2,s,l))) = halt SCM+FSA implies LifeSpan (P1,s) <= l )
assume A6: CurInstr (P2,(Comput (P2,s,l))) = halt SCM+FSA ; ::_thesis: LifeSpan (P1,s) <= l
 CurInstr (P1,(Comput (P1,s,l))) = CurInstr (P2,(Comput (P2,s,l))) by Th7, A1, A2;
hence  LifeSpan (P1,s) <= l by A4, A6, EXTPRO_1:def_15; ::_thesis: verum
end;
CurInstr (P2,(Comput (P2,s,(LifeSpan (P1,s))))) = CurInstr (P1,(Comput (P1,s,(LifeSpan (P1,s))))) by Th7, A1, A2
.= halt SCM+FSA by A4, EXTPRO_1:def_15 ;
hence A7: LifeSpan (P1,s) = LifeSpan (P2,s) by A5, A3, EXTPRO_1:def_15; ::_thesis: Result (P1,s) = Result (P2,s)
A8: Result (P2,s) = Comput (P2,s,(LifeSpan (P1,s))) by A7, Th1, A2, EXTPRO_1:23;
 Result (P1,s) = Comput (P1,s,(LifeSpan (P1,s))) by Th1, A1, EXTPRO_1:23;
hence  Result (P1,s) = Result (P2,s) by A8, Th7, A1, A2; ::_thesis: verum
end;

theorem :: SCMFSA6B:9
canceled;

theorem :: SCMFSA6B:10
canceled;

theorem :: SCMFSA6B:11
for s being State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA
for I being parahalting keeping_0 Program of holds (IExec (I,P,s)) . (intloc 0) = 1
proof
let s be State of SCM+FSA; ::_thesis: for P being Instruction-Sequence of SCM+FSA
for I being parahalting keeping_0 Program of holds (IExec (I,P,s)) . (intloc 0) = 1
let P be Instruction-Sequence of SCM+FSA; ::_thesis: for I being parahalting keeping_0 Program of holds (IExec (I,P,s)) . (intloc 0) = 1
let I be parahalting keeping_0 Program of ; ::_thesis: (IExec (I,P,s)) . (intloc 0) = 1
A1: Initialize ((intloc 0) .--> 1) c= s +* (Initialize ((intloc 0) .--> 1)) by FUNCT_4:25;
A2: I c= P +* I by FUNCT_4:25;
 P +* I halts_on s +* (Initialize ((intloc 0) .--> 1)) by Th2, A2, A1;
then A3: ex n being Element of NAT st
( Result ((P +* I),(s +* (Initialize ((intloc 0) .--> 1)))) = Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),n) & CurInstr ((P +* I),(Result ((P +* I),(s +* (Initialize ((intloc 0) .--> 1)))))) = halt SCM+FSA ) by EXTPRO_1:def_9;
thus (IExec (I,P,s)) . (intloc 0) = (Initialized s) . (intloc 0) by A3, Def4, A2
.= 1 by SCMFSA_M:9 ; ::_thesis: verum
end;

begin

registration
cluster Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like V33() V51() paraclosed V144() for set ;
existence
 ex b1 being Program of st b1 is paraclosed
proof
take  the parahalting Program of ; ::_thesis: the parahalting Program of is paraclosed
thus  the parahalting Program of is paraclosed ; ::_thesis: verum
end;
end;

theorem Th12: :: SCMFSA6B:12
for s being 0 -started State of SCM+FSA
for I being paraclosed Program of
for J being Program of
for P being Instruction-Sequence of SCM+FSA st I c= P & P halts_on s holds
for m being Element of NAT st m <= LifeSpan (P,s) holds
Comput (P,s,m) = Comput ((P +* (I ";" J)),s,m)
proof
let s be 0 -started State of SCM+FSA; ::_thesis: for I being paraclosed Program of
for J being Program of
for P being Instruction-Sequence of SCM+FSA st I c= P & P halts_on s holds
for m being Element of NAT st m <= LifeSpan (P,s) holds
Comput (P,s,m) = Comput ((P +* (I ";" J)),s,m)
let I be paraclosed Program of ; ::_thesis: for J being Program of
for P being Instruction-Sequence of SCM+FSA st I c= P & P halts_on s holds
for m being Element of NAT st m <= LifeSpan (P,s) holds
Comput (P,s,m) = Comput ((P +* (I ";" J)),s,m)
let J be Program of ; ::_thesis: for P being Instruction-Sequence of SCM+FSA st I c= P & P halts_on s holds
for m being Element of NAT st m <= LifeSpan (P,s) holds
Comput (P,s,m) = Comput ((P +* (I ";" J)),s,m)
let P be Instruction-Sequence of SCM+FSA; ::_thesis: ( I c= P & P halts_on s implies for m being Element of NAT st m <= LifeSpan (P,s) holds
Comput (P,s,m) = Comput ((P +* (I ";" J)),s,m) )
assume A1: I c= P ; ::_thesis: ( not P halts_on s or for m being Element of NAT st m <= LifeSpan (P,s) holds
Comput (P,s,m) = Comput ((P +* (I ";" J)),s,m) )
assume A2: P halts_on s ; ::_thesis: for m being Element of NAT st m <= LifeSpan (P,s) holds
Comput (P,s,m) = Comput ((P +* (I ";" J)),s,m)
defpred S1[ Nat] means ( $1 <= LifeSpan (P,s) implies Comput (P,s,$1) = Comput ((P +* (I ";" J)),s,$1) );
A3: for m being Element of NAT st S1[m] holds
S1[m + 1]
proof
let m be Element of NAT ; ::_thesis: ( S1[m] implies S1[m + 1] )
assume A4: ( m <= LifeSpan (P,s) implies Comput (P,s,m) = Comput ((P +* (I ";" J)),s,m) ) ; ::_thesis: S1[m + 1]
A5: dom (I ";" J) = (dom (Directed I)) \/ (dom (Reloc (J,(card I)))) by FUNCT_4:def_1
.= (dom I) \/ (dom (Reloc (J,(card I)))) by FUNCT_4:99 ;
A6: ( {} c= Comput ((P +* (I ";" J)),s,m) & dom I c= dom (I ";" J) ) by A5, XBOOLE_1:2, XBOOLE_1:7;
A7: Comput (P,s,(m + 1)) = Following (P,(Comput (P,s,m))) by EXTPRO_1:3;
A8: Comput ((P +* (I ";" J)),s,(m + 1)) = Following ((P +* (I ";" J)),(Comput ((P +* (I ";" J)),s,m))) by EXTPRO_1:3;
A9: IC (Comput (P,s,m)) in dom I by A1, AMISTD_1:def_10;
 dom P = NAT by PARTFUN1:def_2;
then A10: CurInstr (P,(Comput (P,s,m))) = P . (IC (Comput (P,s,m))) by PARTFUN1:def_6
.= I . (IC (Comput (P,s,m))) by A9, A1, GRFUNC_1:2 ;
assume A11: m + 1 <= LifeSpan (P,s) ; ::_thesis: Comput (P,s,(m + 1)) = Comput ((P +* (I ";" J)),s,(m + 1))
A12: I ";" J c= P +* (I ";" J) by FUNCT_4:25;
A13: dom (P +* (I ";" J)) = NAT by PARTFUN1:def_2;
 m < LifeSpan (P,s) by A11, NAT_1:13;
then  I . (IC (Comput (P,s,m))) <> halt SCM+FSA by A2, A10, EXTPRO_1:def_15;
then  CurInstr (P,(Comput (P,s,m))) = (I ";" J) . (IC (Comput (P,s,m))) by A9, A10, SCMFSA6A:15
.= (P +* (I ";" J)) . (IC (Comput (P,s,m))) by A9, A6, A12, GRFUNC_1:2
.= CurInstr ((P +* (I ";" J)),(Comput ((P +* (I ";" J)),s,m))) by A13, A11, A4, NAT_1:13, PARTFUN1:def_6 ;
hence  Comput (P,s,(m + 1)) = Comput ((P +* (I ";" J)),s,(m + 1)) by A7, A8, A4, A11, NAT_1:13; ::_thesis: verum
end;
A14: S1[ 0 ] ;
thus  for m being Element of NAT holds S1[m] from NAT_1:sch_1(A14, A3); ::_thesis: verum
end;

theorem Th13: :: SCMFSA6B:13
for s being 0 -started State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA
for I being paraclosed Program of st P +* I halts_on s & Directed I c= P holds
IC (Comput (P,s,((LifeSpan ((P +* I),s)) + 1))) = card I
proof
let s be 0 -started State of SCM+FSA; ::_thesis: for P being Instruction-Sequence of SCM+FSA
for I being paraclosed Program of st P +* I halts_on s & Directed I c= P holds
IC (Comput (P,s,((LifeSpan ((P +* I),s)) + 1))) = card I
let P be Instruction-Sequence of SCM+FSA; ::_thesis: for I being paraclosed Program of st P +* I halts_on s & Directed I c= P holds
IC (Comput (P,s,((LifeSpan ((P +* I),s)) + 1))) = card I
let I be paraclosed Program of ; ::_thesis: ( P +* I halts_on s & Directed I c= P implies IC (Comput (P,s,((LifeSpan ((P +* I),s)) + 1))) = card I )
assume that
A1: P +* I halts_on s and
A2: Directed I c= P ; ::_thesis: IC (Comput (P,s,((LifeSpan ((P +* I),s)) + 1))) = card I
A3: I c= P +* I by FUNCT_4:25;
set s2 = s;
set m = LifeSpan ((P +* I),s);
set l1 = IC (Comput ((P +* I),s,(LifeSpan ((P +* I),s))));
A4: I c= P +* I by FUNCT_4:25;
A5: IC (Comput ((P +* I),s,(LifeSpan ((P +* I),s)))) in dom I by A4, AMISTD_1:def_10;
set s1 = s;
A6: P +* (I ";" I) = P +* (I +* (I ";" I)) by SCMFSA6A:18
.= (P +* I) +* (I ";" I) by FUNCT_4:14 ;
now__::_thesis:_for_k_being_Element_of_NAT_st_k_<=_LifeSpan_((P_+*_I),s)_holds_
Comput_((P_+*_I),s,k)_=_Comput_((P_+*_(Directed_I)),s,k)
let k be Element of NAT ; ::_thesis: ( k <= LifeSpan ((P +* I),s) implies Comput ((P +* I),s,k) = Comput ((P +* (Directed I)),s,k) )
defpred S1[ Nat] means ( $1 <= k implies Comput ((P +* (I ";" I)),s,$1) = Comput ((P +* (Directed I)),s,$1) );
assume A7: k <= LifeSpan ((P +* I),s) ; ::_thesis: Comput ((P +* I),s,k) = Comput ((P +* (Directed I)),s,k)
A8: for n being Element of NAT st S1[n] holds
S1[n + 1]
proof
let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] )
assume A9: ( n <= k implies Comput ((P +* (I ";" I)),s,n) = Comput ((P +* (Directed I)),s,n) ) ; ::_thesis: S1[n + 1]
A10: Comput ((P +* (Directed I)),s,(n + 1)) = Following ((P +* (Directed I)),(Comput ((P +* (Directed I)),s,n))) by EXTPRO_1:3
.= Exec ((CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),s,n)))),(Comput ((P +* (Directed I)),s,n))) ;
A11: Comput ((P +* (I ";" I)),s,(n + 1)) = Following ((P +* (I ";" I)),(Comput ((P +* (I ";" I)),s,n))) by EXTPRO_1:3
.= Exec ((CurInstr ((P +* (I ";" I)),(Comput ((P +* (I ";" I)),s,n)))),(Comput ((P +* (I ";" I)),s,n))) ;
A12: n <= n + 1 by NAT_1:12;
assume A13: n + 1 <= k ; ::_thesis: Comput ((P +* (I ";" I)),s,(n + 1)) = Comput ((P +* (Directed I)),s,(n + 1))
 n <= k by A13, A12, XXREAL_0:2;
then  Comput ((P +* I),s,n) = Comput ((P +* (I ";" I)),s,n) by A3, Th12, A6, A1, A7, XXREAL_0:2;
then  IC (Comput ((P +* (I ";" I)),s,n)) in dom I by A3, AMISTD_1:def_10;
then A14: IC (Comput ((P +* (Directed I)),s,n)) in dom (Directed I) by A13, A9, A12, FUNCT_4:99, XXREAL_0:2;
 dom (P +* (Directed I)) = NAT by PARTFUN1:def_2;
then A15: (P +* (Directed I)) /. (IC (Comput ((P +* (Directed I)),s,n))) = (P +* (Directed I)) . (IC (Comput ((P +* (Directed I)),s,n))) by PARTFUN1:def_6;
A16: dom (P +* (I ";" I)) = NAT by PARTFUN1:def_2;
 Directed I c= P +* (Directed I) by FUNCT_4:25;
then A17: CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),s,n))) = (Directed I) . (IC (Comput ((P +* (Directed I)),s,n))) by A14, A15, GRFUNC_1:2;
A18: ( dom I c= dom (I ";" I) & CurInstr ((P +* (I ";" I)),(Comput ((P +* (I ";" I)),s,n))) = (P +* (I ";" I)) . (IC (Comput ((P +* (I ";" I)),s,n))) ) by A16, PARTFUN1:def_6, SCMFSA6A:17;
A19: Directed I c= I ";" I by SCMFSA6A:16;
 I ";" I c= P +* (I ";" I) by FUNCT_4:25;
then  Directed I c= P +* (I ";" I) by A19, XBOOLE_1:1;
hence  Comput ((P +* (I ";" I)),s,(n + 1)) = Comput ((P +* (Directed I)),s,(n + 1)) by A9, A13, A12, A17, A11, A10, A14, A18, GRFUNC_1:2, XXREAL_0:2; ::_thesis: verum
end;
A20: S1[ 0 ] ;
 for n being Element of NAT holds S1[n] from NAT_1:sch_1(A20, A8);
then  Comput ((P +* (I ";" I)),s,k) = Comput ((P +* (Directed I)),s,k) ;
hence  Comput ((P +* I),s,k) = Comput ((P +* (Directed I)),s,k) by A7, Th12, A6, A1, FUNCT_4:25; ::_thesis: verum
end;
then A21: Comput ((P +* I),s,(LifeSpan ((P +* I),s))) = Comput ((P +* (Directed I)),s,(LifeSpan ((P +* I),s))) ;
A22: dom (P +* I) = NAT by PARTFUN1:def_2;
 I c= P +* I by FUNCT_4:25;
then A23: I . (IC (Comput ((P +* I),s,(LifeSpan ((P +* I),s))))) = (P +* I) . (IC (Comput ((P +* I),s,(LifeSpan ((P +* I),s))))) by A5, GRFUNC_1:2
.= CurInstr ((P +* I),(Comput ((P +* I),s,(LifeSpan ((P +* I),s))))) by A22, PARTFUN1:def_6
.= halt SCM+FSA by A1, EXTPRO_1:def_15 ;
 IC (Comput ((P +* (Directed I)),s,(LifeSpan ((P +* I),s)))) in dom (Directed I) by A5, A21, FUNCT_4:99;
then A24: (P +* (Directed I)) . (IC (Comput ((P +* I),s,(LifeSpan ((P +* I),s))))) = (Directed I) . (IC (Comput ((P +* I),s,(LifeSpan ((P +* I),s))))) by A21, FUNCT_4:13
.= goto (card I) by A5, A23, FUNCT_4:106 ;
A25: P +* (Directed I) = P by A2, FUNCT_4:98;
A26: dom (P +* (Directed I)) = NAT by PARTFUN1:def_2;
Comput ((P +* (Directed I)),s,((LifeSpan ((P +* I),s)) + 1)) = Following ((P +* (Directed I)),(Comput ((P +* (Directed I)),s,(LifeSpan ((P +* I),s))))) by EXTPRO_1:3
.= Exec ((goto (card I)),(Comput ((P +* (Directed I)),s,(LifeSpan ((P +* I),s))))) by A26, A21, A24, PARTFUN1:def_6 ;
hence  IC (Comput (P,s,((LifeSpan ((P +* I),s)) + 1))) = card I by A25, SCMFSA_2:69; ::_thesis: verum
end;

theorem Th14: :: SCMFSA6B:14
for s being 0 -started State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA
for I being paraclosed Program of st P +* I halts_on s & Directed I c= P holds
DataPart (Comput (P,s,(LifeSpan ((P +* I),s)))) = DataPart (Comput (P,s,((LifeSpan ((P +* I),s)) + 1)))
proof
let s be 0 -started State of SCM+FSA; ::_thesis: for P being Instruction-Sequence of SCM+FSA
for I being paraclosed Program of st P +* I halts_on s & Directed I c= P holds
DataPart (Comput (P,s,(LifeSpan ((P +* I),s)))) = DataPart (Comput (P,s,((LifeSpan ((P +* I),s)) + 1)))
let P be Instruction-Sequence of SCM+FSA; ::_thesis: for I being paraclosed Program of st P +* I halts_on s & Directed I c= P holds
DataPart (Comput (P,s,(LifeSpan ((P +* I),s)))) = DataPart (Comput (P,s,((LifeSpan ((P +* I),s)) + 1)))
let I be paraclosed Program of ; ::_thesis: ( P +* I halts_on s & Directed I c= P implies DataPart (Comput (P,s,(LifeSpan ((P +* I),s)))) = DataPart (Comput (P,s,((LifeSpan ((P +* I),s)) + 1))) )
assume that
A1: P +* I halts_on s and
A2: Directed I c= P ; ::_thesis: DataPart (Comput (P,s,(LifeSpan ((P +* I),s)))) = DataPart (Comput (P,s,((LifeSpan ((P +* I),s)) + 1)))
A3: I c= P +* I by FUNCT_4:25;
set m = LifeSpan ((P +* I),s);
set l1 = IC (Comput ((P +* I),s,(LifeSpan ((P +* I),s))));
A4: IC (Comput ((P +* I),s,(LifeSpan ((P +* I),s)))) in dom I by A3, AMISTD_1:def_10;
now__::_thesis:_for_k_being_Element_of_NAT_st_k_<=_LifeSpan_((P_+*_I),s)_holds_
Comput_((P_+*_I),s,k)_=_Comput_(P,s,k)
let k be Element of NAT ; ::_thesis: ( k <= LifeSpan ((P +* I),s) implies Comput ((P +* I),s,k) = Comput (P,s,k) )
defpred S1[ Nat] means ( $1 <= k implies Comput (((P +* I) +* (I ";" I)),s,$1) = Comput (P,s,$1) );
assume A5: k <= LifeSpan ((P +* I),s) ; ::_thesis: Comput ((P +* I),s,k) = Comput (P,s,k)
A6: for n being Element of NAT st S1[n] holds
S1[n + 1]
proof
A7: Directed I c= I ";" I by SCMFSA6A:16;
let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] )
A8: dom I c= dom (I ";" I) by SCMFSA6A:17;
assume A9: ( n <= k implies Comput (((P +* I) +* (I ";" I)),s,n) = Comput (P,s,n) ) ; ::_thesis: S1[n + 1]
A10: Comput (P,s,(n + 1)) = Following (P,(Comput (P,s,n))) by EXTPRO_1:3
.= Exec ((CurInstr (P,(Comput (P,s,n)))),(Comput (P,s,n))) ;
A11: Comput (((P +* I) +* (I ";" I)),s,(n + 1)) = Following (((P +* I) +* (I ";" I)),(Comput (((P +* I) +* (I ";" I)),s,n))) by EXTPRO_1:3
.= Exec ((CurInstr (((P +* I) +* (I ";" I)),(Comput (((P +* I) +* (I ";" I)),s,n)))),(Comput (((P +* I) +* (I ";" I)),s,n))) ;
A12: n <= n + 1 by NAT_1:12;
assume A13: n + 1 <= k ; ::_thesis: Comput (((P +* I) +* (I ";" I)),s,(n + 1)) = Comput (P,s,(n + 1))
 n <= k by A13, A12, XXREAL_0:2;
then  Comput ((P +* I),s,n) = Comput (((P +* I) +* (I ";" I)),s,n) by Th12, A5, A3, A1, XXREAL_0:2;
then A14: IC (Comput (((P +* I) +* (I ";" I)),s,n)) in dom I by A3, AMISTD_1:def_10;
then A15: IC (Comput (P,s,n)) in dom (Directed I) by A13, A9, A12, FUNCT_4:99, XXREAL_0:2;
A16: dom P = NAT by PARTFUN1:def_2;
A17: CurInstr (P,(Comput (P,s,n))) = P . (IC (Comput (P,s,n))) by A16, PARTFUN1:def_6
.= (Directed I) . (IC (Comput (P,s,n))) by A15, A2, GRFUNC_1:2 ;
A18: dom ((P +* I) +* (I ";" I)) = NAT by PARTFUN1:def_2;
CurInstr (((P +* I) +* (I ";" I)),(Comput (((P +* I) +* (I ";" I)),s,n))) = ((P +* I) +* (I ";" I)) . (IC (Comput (((P +* I) +* (I ";" I)),s,n))) by A18, PARTFUN1:def_6
.= (I ";" I) . (IC (Comput (((P +* I) +* (I ";" I)),s,n))) by A8, A14, FUNCT_4:13
.= (Directed I) . (IC (Comput (((P +* I) +* (I ";" I)),s,n))) by A7, A13, A15, A9, A12, GRFUNC_1:2, XXREAL_0:2 ;
hence  Comput (((P +* I) +* (I ";" I)),s,(n + 1)) = Comput (P,s,(n + 1)) by A9, A13, A12, A17, A11, A10, XXREAL_0:2; ::_thesis: verum
end;
A19: S1[ 0 ] ;
 for n being Element of NAT holds S1[n] from NAT_1:sch_1(A19, A6);
then  Comput (((P +* I) +* (I ";" I)),s,k) = Comput (P,s,k) ;
hence  Comput ((P +* I),s,k) = Comput (P,s,k) by A5, A1, Th12, FUNCT_4:25; ::_thesis: verum
end;
then A20: Comput ((P +* I),s,(LifeSpan ((P +* I),s))) = Comput (P,s,(LifeSpan ((P +* I),s))) ;
A21: dom (P +* I) = NAT by PARTFUN1:def_2;
 I c= P +* I by FUNCT_4:25;
then A22: I . (IC (Comput ((P +* I),s,(LifeSpan ((P +* I),s))))) = (P +* I) . (IC (Comput ((P +* I),s,(LifeSpan ((P +* I),s))))) by A4, GRFUNC_1:2
.= CurInstr ((P +* I),(Comput ((P +* I),s,(LifeSpan ((P +* I),s))))) by A21, PARTFUN1:def_6
.= halt SCM+FSA by A1, EXTPRO_1:def_15 ;
 IC (Comput (P,s,(LifeSpan ((P +* I),s)))) in dom (Directed I) by A4, A20, FUNCT_4:99;
then A23: P . (IC (Comput ((P +* I),s,(LifeSpan ((P +* I),s))))) = (Directed I) . (IC (Comput ((P +* I),s,(LifeSpan ((P +* I),s))))) by A20, A2, GRFUNC_1:2
.= goto (card I) by A4, A22, FUNCT_4:106 ;
A24: dom P = NAT by PARTFUN1:def_2;
Comput (P,s,((LifeSpan ((P +* I),s)) + 1)) = Following (P,(Comput (P,s,(LifeSpan ((P +* I),s))))) by EXTPRO_1:3
.= Exec ((goto (card I)),(Comput (P,s,(LifeSpan ((P +* I),s))))) by A20, A23, A24, PARTFUN1:def_6 ;
then  ( ( for a being Int-Location holds (Comput (P,s,((LifeSpan ((P +* I),s)) + 1))) . a = (Comput (P,s,(LifeSpan ((P +* I),s)))) . a ) & ( for f being FinSeq-Location holds (Comput (P,s,((LifeSpan ((P +* I),s)) + 1))) . f = (Comput (P,s,(LifeSpan ((P +* I),s)))) . f ) ) by SCMFSA_2:69;
hence  DataPart (Comput (P,s,(LifeSpan ((P +* I),s)))) = DataPart (Comput (P,s,((LifeSpan ((P +* I),s)) + 1))) by SCMFSA_M:2; ::_thesis: verum
end;

theorem Th15: :: SCMFSA6B:15
for s being State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA
for I being parahalting Program of st I c= P & Initialize ((intloc 0) .--> 1) c= s holds
for k being Element of NAT st k <= LifeSpan (P,s) holds
CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),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 parahalting Program of st I c= P & Initialize ((intloc 0) .--> 1) c= s holds
for k being Element of NAT st k <= LifeSpan (P,s) holds
CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),s,k))) <> halt SCM+FSA
let P be Instruction-Sequence of SCM+FSA; ::_thesis: for I being parahalting Program of st I c= P & Initialize ((intloc 0) .--> 1) c= s holds
for k being Element of NAT st k <= LifeSpan (P,s) holds
CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),s,k))) <> halt SCM+FSA
let I be parahalting Program of ; ::_thesis: ( I c= P & Initialize ((intloc 0) .--> 1) c= s implies for k being Element of NAT st k <= LifeSpan (P,s) holds
CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),s,k))) <> halt SCM+FSA )
set m = LifeSpan (P,s);
assume that
A1: I c= P and
A2: Initialize ((intloc 0) .--> 1) c= s ; ::_thesis: for k being Element of NAT st k <= LifeSpan (P,s) holds
CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),s,k))) <> halt SCM+FSA
A3: Start-At (0,SCM+FSA) c= s by A2, MEMSTR_0:50;
then  s is 0 -started by MEMSTR_0:29;
then A4: P halts_on s by A1, AMISTD_1:def_11;
reconsider s1 = s as 0 -started State of SCM+FSA by A3, MEMSTR_0:29;
A5: now__::_thesis:_for_k_being_Element_of_NAT_st_k_<=_LifeSpan_(P,s)_holds_
Comput_(P,s,k)_=_Comput_((P_+*_(Directed_I)),s,k)
let k be Element of NAT ; ::_thesis: ( k <= LifeSpan (P,s) implies Comput (P,s,k) = Comput ((P +* (Directed I)),s,k) )
defpred S1[ Nat] means ( $1 <= k implies Comput ((P +* (I ";" I)),s1,$1) = Comput ((P +* (Directed I)),s,$1) );
assume A6: k <= LifeSpan (P,s) ; ::_thesis: Comput (P,s,k) = Comput ((P +* (Directed I)),s,k)
A7: for n being Element of NAT st S1[n] holds
S1[n + 1]
proof
A8: Directed I c= I ";" I by SCMFSA6A:16;
let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] )
A9: dom I c= dom (I ";" I) by SCMFSA6A:17;
assume A10: ( n <= k implies Comput ((P +* (I ";" I)),s1,n) = Comput ((P +* (Directed I)),s,n) ) ; ::_thesis: S1[n + 1]
A11: Comput ((P +* (Directed I)),s,(n + 1)) = Following ((P +* (Directed I)),(Comput ((P +* (Directed I)),s,n))) by EXTPRO_1:3
.= Exec ((CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),s,n)))),(Comput ((P +* (Directed I)),s,n))) ;
A12: Comput ((P +* (I ";" I)),s1,(n + 1)) = Following ((P +* (I ";" I)),(Comput ((P +* (I ";" I)),s1,n))) by EXTPRO_1:3
.= Exec ((CurInstr ((P +* (I ";" I)),(Comput ((P +* (I ";" I)),s1,n)))),(Comput ((P +* (I ";" I)),s1,n))) ;
A13: n <= n + 1 by NAT_1:12;
assume A14: n + 1 <= k ; ::_thesis: Comput ((P +* (I ";" I)),s1,(n + 1)) = Comput ((P +* (Directed I)),s,(n + 1))
 n <= k by A14, A13, XXREAL_0:2;
then  Comput (P,s,n) = Comput ((P +* (I ";" I)),s1,n) by A4, A1, Th12, A6, XXREAL_0:2;
then A15: IC (Comput ((P +* (I ";" I)),s1,n)) in dom I by A1, AMISTD_1:def_10;
then A16: IC (Comput ((P +* (Directed I)),s,n)) in dom (Directed I) by A14, A10, A13, FUNCT_4:99, XXREAL_0:2;
 dom (P +* (Directed I)) = NAT by PARTFUN1:def_2;
then A17: CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),s,n))) = (P +* (Directed I)) . (IC (Comput ((P +* (Directed I)),s,n))) by PARTFUN1:def_6
.= (Directed I) . (IC (Comput ((P +* (Directed I)),s,n))) by A16, FUNCT_4:13 ;
 dom (P +* (I ";" I)) = NAT by PARTFUN1:def_2;
then  CurInstr ((P +* (I ";" I)),(Comput ((P +* (I ";" I)),s1,n))) = (P +* (I ";" I)) . (IC (Comput ((P +* (I ";" I)),s1,n))) by PARTFUN1:def_6
.= (I ";" I) . (IC (Comput ((P +* (I ";" I)),s1,n))) by A9, A15, FUNCT_4:13
.= (Directed I) . (IC (Comput ((P +* (I ";" I)),s1,n))) by A8, A14, A10, A13, A16, GRFUNC_1:2, XXREAL_0:2 ;
hence  Comput ((P +* (I ";" I)),s1,(n + 1)) = Comput ((P +* (Directed I)),s,(n + 1)) by A10, A14, A13, A17, A12, A11, XXREAL_0:2; ::_thesis: verum
end;
A18: S1[ 0 ] ;
 for n being Element of NAT holds S1[n] from NAT_1:sch_1(A18, A7);
then  Comput ((P +* (I ";" I)),s1,k) = Comput ((P +* (Directed I)),s,k) ;
hence  Comput (P,s,k) = Comput ((P +* (Directed I)),s,k) by A4, A6, Th12, A1; ::_thesis: verum
end;
hereby  ::_thesis: verum
let k be Element of NAT ; ::_thesis: ( k <= LifeSpan (P,s) implies CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),s,k))) <> halt SCM+FSA )
set lk = IC (Comput (P,s,k));
A19: dom I = dom (Directed I) by FUNCT_4:99;
A20: IC (Comput (P,s1,k)) in dom I by A1, AMISTD_1:def_10;
then A21: (Directed I) . (IC (Comput (P,s,k))) in rng (Directed I) by A19, FUNCT_1:def_3;
A22: dom (P +* (Directed I)) = NAT by PARTFUN1:def_2;
assume  k <= LifeSpan (P,s) ; ::_thesis: CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),s,k))) <> halt SCM+FSA
then  IC (Comput (P,s,k)) = IC (Comput ((P +* (Directed I)),s,k)) by A5;
then A23: CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),s,k))) = (P +* (Directed I)) . (IC (Comput (P,s,k))) by A22, PARTFUN1:def_6
.= (Directed I) . (IC (Comput (P,s,k))) by A19, A20, FUNCT_4:13 ;
thus  CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),s,k))) <> halt SCM+FSA by A23, A21, SCMFSA6A:1; ::_thesis: verum
end;
end;

theorem Th16: :: SCMFSA6B:16
for s being 0 -started State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA
for I being paraclosed Program of st P +* I halts_on s holds
for J being Program of
for k being Element of NAT st k <= LifeSpan ((P +* I),s) holds
Comput ((P +* I),s,k) = Comput ((P +* (I ";" J)),s,k)
proof
let s be 0 -started State of SCM+FSA; ::_thesis: for P being Instruction-Sequence of SCM+FSA
for I being paraclosed Program of st P +* I halts_on s holds
for J being Program of
for k being Element of NAT st k <= LifeSpan ((P +* I),s) holds
Comput ((P +* I),s,k) = Comput ((P +* (I ";" J)),s,k)
let P be Instruction-Sequence of SCM+FSA; ::_thesis: for I being paraclosed Program of st P +* I halts_on s holds
for J being Program of
for k being Element of NAT st k <= LifeSpan ((P +* I),s) holds
Comput ((P +* I),s,k) = Comput ((P +* (I ";" J)),s,k)
let I be paraclosed Program of ; ::_thesis: ( P +* I halts_on s implies for J being Program of
for k being Element of NAT st k <= LifeSpan ((P +* I),s) holds
Comput ((P +* I),s,k) = Comput ((P +* (I ";" J)),s,k) )
assume A1: P +* I halts_on s ; ::_thesis: for J being Program of
for k being Element of NAT st k <= LifeSpan ((P +* I),s) holds
Comput ((P +* I),s,k) = Comput ((P +* (I ";" J)),s,k)
let J be Program of ; ::_thesis: for k being Element of NAT st k <= LifeSpan ((P +* I),s) holds
Comput ((P +* I),s,k) = Comput ((P +* (I ";" J)),s,k)
A2: I c= P +* I by FUNCT_4:25;
defpred S1[ Nat] means ( $1 <= LifeSpan ((P +* I),s) implies Comput ((P +* I),s,$1) = Comput ((P +* (I ";" J)),s,$1) );
A3: for m being Element of NAT st S1[m] holds
S1[m + 1]
proof
dom (I ";" J) = (dom (Directed I)) \/ (dom (Reloc (J,(card I)))) by FUNCT_4:def_1
.= (dom I) \/ (dom (Reloc (J,(card I)))) by FUNCT_4:99 ;
then A4: dom I c= dom (I ";" J) by XBOOLE_1:7;
let m be Element of NAT ; ::_thesis: ( S1[m] implies S1[m + 1] )
assume A5: ( m <= LifeSpan ((P +* I),s) implies Comput ((P +* I),s,m) = Comput ((P +* (I ";" J)),s,m) ) ; ::_thesis: S1[m + 1]
A6: Comput ((P +* I),s,(m + 1)) = Following ((P +* I),(Comput ((P +* I),s,m))) by EXTPRO_1:3
.= Exec ((CurInstr ((P +* I),(Comput ((P +* I),s,m)))),(Comput ((P +* I),s,m))) ;
A7: Comput ((P +* (I ";" J)),s,(m + 1)) = Following ((P +* (I ";" J)),(Comput ((P +* (I ";" J)),s,m))) by EXTPRO_1:3
.= Exec ((CurInstr ((P +* (I ";" J)),(Comput ((P +* (I ";" J)),s,m)))),(Comput ((P +* (I ";" J)),s,m))) ;
A8: IC (Comput ((P +* I),s,m)) in dom I by A2, AMISTD_1:def_10;
A9: I c= P +* I by FUNCT_4:25;
 dom (P +* I) = NAT by PARTFUN1:def_2;
then A10: CurInstr ((P +* I),(Comput ((P +* I),s,m))) = (P +* I) . (IC (Comput ((P +* I),s,m))) by PARTFUN1:def_6
.= I . (IC (Comput ((P +* I),s,m))) by A8, A9, GRFUNC_1:2 ;
assume A11: m + 1 <= LifeSpan ((P +* I),s) ; ::_thesis: Comput ((P +* I),s,(m + 1)) = Comput ((P +* (I ";" J)),s,(m + 1))
A12: I ";" J c= P +* (I ";" J) by FUNCT_4:25;
A13: dom (P +* (I ";" J)) = NAT by PARTFUN1:def_2;
 m < LifeSpan ((P +* I),s) by A11, NAT_1:13;
then  I . (IC (Comput ((P +* I),s,m))) <> halt SCM+FSA by A1, A10, EXTPRO_1:def_15;
then  CurInstr ((P +* I),(Comput ((P +* I),s,m))) = (I ";" J) . (IC (Comput ((P +* I),s,m))) by A8, A10, SCMFSA6A:15
.= (P +* (I ";" J)) . (IC (Comput ((P +* (I ";" J)),s,m))) by A11, A8, A4, A12, A5, GRFUNC_1:2, NAT_1:13
.= CurInstr ((P +* (I ";" J)),(Comput ((P +* (I ";" J)),s,m))) by A13, PARTFUN1:def_6 ;
hence  Comput ((P +* I),s,(m + 1)) = Comput ((P +* (I ";" J)),s,(m + 1)) by A6, A7, A5, A11, NAT_1:13; ::_thesis: verum
end;
A14: S1[ 0 ] ;
thus  for k being Element of NAT holds S1[k] from NAT_1:sch_1(A14, A3); ::_thesis: verum
end;

Lm2:  for P being Instruction-Sequence of SCM+FSA
for I being parahalting keeping_0 Program of
for J being parahalting Program of
for s being State of SCM+FSA st I ";" J c= P & Initialize ((intloc 0) .--> 1) c= s holds
( IC (Comput (P,s,((LifeSpan ((P +* I),s)) + 1))) = card I & DataPart (Comput (P,s,((LifeSpan ((P +* I),s)) + 1))) = DataPart ((Comput ((P +* I),s,(LifeSpan ((P +* I),s)))) +* (Initialize ((intloc 0) .--> 1))) & Reloc (J,(card I)) c= P & (Comput (P,s,((LifeSpan ((P +* I),s)) + 1))) . (intloc 0) = 1 & P halts_on s & LifeSpan (P,s) = ((LifeSpan ((P +* I),s)) + 1) + (LifeSpan (((P +* I) +* J),((Result ((P +* I),s)) +* (Initialize ((intloc 0) .--> 1))))) & ( J is keeping_0 implies (Result (P,s)) . (intloc 0) = 1 ) )
proof
let P be Instruction-Sequence of SCM+FSA; ::_thesis: for I being parahalting keeping_0 Program of
for J being parahalting Program of
for s being State of SCM+FSA st I ";" J c= P & Initialize ((intloc 0) .--> 1) c= s holds
( IC (Comput (P,s,((LifeSpan ((P +* I),s)) + 1))) = card I & DataPart (Comput (P,s,((LifeSpan ((P +* I),s)) + 1))) = DataPart ((Comput ((P +* I),s,(LifeSpan ((P +* I),s)))) +* (Initialize ((intloc 0) .--> 1))) & Reloc (J,(card I)) c= P & (Comput (P,s,((LifeSpan ((P +* I),s)) + 1))) . (intloc 0) = 1 & P halts_on s & LifeSpan (P,s) = ((LifeSpan ((P +* I),s)) + 1) + (LifeSpan (((P +* I) +* J),((Result ((P +* I),s)) +* (Initialize ((intloc 0) .--> 1))))) & ( J is keeping_0 implies (Result (P,s)) . (intloc 0) = 1 ) )
set D = Data-Locations ;
let I be parahalting keeping_0 Program of ; ::_thesis: for J being parahalting Program of
for s being State of SCM+FSA st I ";" J c= P & Initialize ((intloc 0) .--> 1) c= s holds
( IC (Comput (P,s,((LifeSpan ((P +* I),s)) + 1))) = card I & DataPart (Comput (P,s,((LifeSpan ((P +* I),s)) + 1))) = DataPart ((Comput ((P +* I),s,(LifeSpan ((P +* I),s)))) +* (Initialize ((intloc 0) .--> 1))) & Reloc (J,(card I)) c= P & (Comput (P,s,((LifeSpan ((P +* I),s)) + 1))) . (intloc 0) = 1 & P halts_on s & LifeSpan (P,s) = ((LifeSpan ((P +* I),s)) + 1) + (LifeSpan (((P +* I) +* J),((Result ((P +* I),s)) +* (Initialize ((intloc 0) .--> 1))))) & ( J is keeping_0 implies (Result (P,s)) . (intloc 0) = 1 ) )
let J be parahalting Program of ; ::_thesis: for s being State of SCM+FSA st I ";" J c= P & Initialize ((intloc 0) .--> 1) c= s holds
( IC (Comput (P,s,((LifeSpan ((P +* I),s)) + 1))) = card I & DataPart (Comput (P,s,((LifeSpan ((P +* I),s)) + 1))) = DataPart ((Comput ((P +* I),s,(LifeSpan ((P +* I),s)))) +* (Initialize ((intloc 0) .--> 1))) & Reloc (J,(card I)) c= P & (Comput (P,s,((LifeSpan ((P +* I),s)) + 1))) . (intloc 0) = 1 & P halts_on s & LifeSpan (P,s) = ((LifeSpan ((P +* I),s)) + 1) + (LifeSpan (((P +* I) +* J),((Result ((P +* I),s)) +* (Initialize ((intloc 0) .--> 1))))) & ( J is keeping_0 implies (Result (P,s)) . (intloc 0) = 1 ) )
let s be State of SCM+FSA; ::_thesis: ( I ";" J c= P & Initialize ((intloc 0) .--> 1) c= s implies ( IC (Comput (P,s,((LifeSpan ((P +* I),s)) + 1))) = card I & DataPart (Comput (P,s,((LifeSpan ((P +* I),s)) + 1))) = DataPart ((Comput ((P +* I),s,(LifeSpan ((P +* I),s)))) +* (Initialize ((intloc 0) .--> 1))) & Reloc (J,(card I)) c= P & (Comput (P,s,((LifeSpan ((P +* I),s)) + 1))) . (intloc 0) = 1 & P halts_on s & LifeSpan (P,s) = ((LifeSpan ((P +* I),s)) + 1) + (LifeSpan (((P +* I) +* J),((Result ((P +* I),s)) +* (Initialize ((intloc 0) .--> 1))))) & ( J is keeping_0 implies (Result (P,s)) . (intloc 0) = 1 ) ) )
set s3 = (Comput ((P +* I),s,(LifeSpan ((P +* I),s)))) +* (Initialize ((intloc 0) .--> 1));
set m1 = LifeSpan ((P +* I),s);
set m3 = LifeSpan (((P +* I) +* J),((Comput ((P +* I),s,(LifeSpan ((P +* I),s)))) +* (Initialize ((intloc 0) .--> 1))));
A1: dom (Directed I) = dom I by FUNCT_4:99;
assume that
A2: I ";" J c= P and
A3: Initialize ((intloc 0) .--> 1) c= s ; ::_thesis: ( IC (Comput (P,s,((LifeSpan ((P +* I),s)) + 1))) = card I & DataPart (Comput (P,s,((LifeSpan ((P +* I),s)) + 1))) = DataPart ((Comput ((P +* I),s,(LifeSpan ((P +* I),s)))) +* (Initialize ((intloc 0) .--> 1))) & Reloc (J,(card I)) c= P & (Comput (P,s,((LifeSpan ((P +* I),s)) + 1))) . (intloc 0) = 1 & P halts_on s & LifeSpan (P,s) = ((LifeSpan ((P +* I),s)) + 1) + (LifeSpan (((P +* I) +* J),((Result ((P +* I),s)) +* (Initialize ((intloc 0) .--> 1))))) & ( J is keeping_0 implies (Result (P,s)) . (intloc 0) = 1 ) )
A4: Start-At (0,SCM+FSA) c= Initialize ((intloc 0) .--> 1) by FUNCT_4:25;
then A5: Start-At (0,SCM+FSA) c= s by A3, XBOOLE_1:1;
A6: Directed I c= I ";" J by SCMFSA6A:16;
A7: P +* (Directed I) = P by A6, A2, FUNCT_4:98, XBOOLE_1:1;
A8: P = P +* (I ";" J) by A2, FUNCT_4:98;
A9: s is 0 -started State of SCM+FSA by A5, MEMSTR_0:29;
then A10: P +* I halts_on s by Th1, FUNCT_4:25;
hence A11: IC (Comput (P,s,((LifeSpan ((P +* I),s)) + 1))) = card I by Th13, A6, A2, A9, XBOOLE_1:1; ::_thesis: ( DataPart (Comput (P,s,((LifeSpan ((P +* I),s)) + 1))) = DataPart ((Comput ((P +* I),s,(LifeSpan ((P +* I),s)))) +* (Initialize ((intloc 0) .--> 1))) & Reloc (J,(card I)) c= P & (Comput (P,s,((LifeSpan ((P +* I),s)) + 1))) . (intloc 0) = 1 & P halts_on s & LifeSpan (P,s) = ((LifeSpan ((P +* I),s)) + 1) + (LifeSpan (((P +* I) +* J),((Result ((P +* I),s)) +* (Initialize ((intloc 0) .--> 1))))) & ( J is keeping_0 implies (Result (P,s)) . (intloc 0) = 1 ) )
A12: now__::_thesis:_for_x_being_set_st_x_in_dom_(DataPart_(Initialize_((intloc_0)_.-->_1)))_holds_
(DataPart_(Initialize_((intloc_0)_.-->_1)))_._x_=_(DataPart_(Comput_((P_+*_I),s,(LifeSpan_((P_+*_I),s)))))_._x
let x be set ; ::_thesis: ( x in dom (DataPart (Initialize ((intloc 0) .--> 1))) implies (DataPart (Initialize ((intloc 0) .--> 1))) . b1 = (DataPart (Comput ((P +* I),s,(LifeSpan ((P +* I),s))))) . b1 )
A13: dom (DataPart (Initialize ((intloc 0) .--> 1))) c= dom (Initialize ((intloc 0) .--> 1)) by RELAT_1:60;
assume A14: x in dom (DataPart (Initialize ((intloc 0) .--> 1))) ; ::_thesis: (DataPart (Initialize ((intloc 0) .--> 1))) . b1 = (DataPart (Comput ((P +* I),s,(LifeSpan ((P +* I),s))))) . b1
A15: x in Data-Locations by A14, RELAT_1:57;
A16: I c= P +* I by FUNCT_4:25;
percases ( x = intloc 0 or x = IC ) by A14, A13, SCMFSA_M:11, TARSKI:def_2;
supposeA17: x = intloc 0 ; ::_thesis: (DataPart (Initialize ((intloc 0) .--> 1))) . b1 = (DataPart (Comput ((P +* I),s,(LifeSpan ((P +* I),s))))) . b1
then A18: x in dom (Initialize ((intloc 0) .--> 1)) by SCMFSA_M:11, TARSKI:def_2;
thus (DataPart (Initialize ((intloc 0) .--> 1))) . x = 1 by A17, A15, FUNCT_1:49, SCMFSA_M:12
.= s . x by A3, A18, A17, GRFUNC_1:2, SCMFSA_M:12
.= (Comput ((P +* I),s,(LifeSpan ((P +* I),s)))) . x by A17, Def4, A16, A9
.= (DataPart (Comput ((P +* I),s,(LifeSpan ((P +* I),s))))) . x by A15, FUNCT_1:49 ; ::_thesis: verum
end;
suppose x = IC ; ::_thesis: (DataPart (Initialize ((intloc 0) .--> 1))) . b1 = (DataPart (Comput ((P +* I),s,(LifeSpan ((P +* I),s))))) . b1
then  not x in Data-Locations by STRUCT_0:3;
hence  (DataPart (Initialize ((intloc 0) .--> 1))) . x = (DataPart (Comput ((P +* I),s,(LifeSpan ((P +* I),s))))) . x by A14, RELAT_1:57; ::_thesis: verum
end;
end;
end;
set s4 = Comput (P,s,((LifeSpan ((P +* I),s)) + 1));
reconsider m = ((LifeSpan ((P +* I),s)) + 1) + (LifeSpan (((P +* I) +* J),((Comput ((P +* I),s,(LifeSpan ((P +* I),s)))) +* (Initialize ((intloc 0) .--> 1))))) as Element of NAT ;
A19: Initialize ((intloc 0) .--> 1) c= (Comput ((P +* I),s,(LifeSpan ((P +* I),s)))) +* (Initialize ((intloc 0) .--> 1)) by FUNCT_4:25;
 J c= (P +* I) +* J by FUNCT_4:25;
then A20: (P +* I) +* J halts_on (Comput ((P +* I),s,(LifeSpan ((P +* I),s)))) +* (Initialize ((intloc 0) .--> 1)) by A19, Th2;
A21: dom (Initialize ((intloc 0) .--> 1)) c= the carrier of SCM+FSA by RELAT_1:def_18;
 dom (DataPart (Initialize ((intloc 0) .--> 1))) = (dom (Initialize ((intloc 0) .--> 1))) /\ (Data-Locations ) by RELAT_1:61;
then  dom (DataPart (Initialize ((intloc 0) .--> 1))) c= the carrier of SCM+FSA /\ (Data-Locations ) by A21, XBOOLE_1:26;
then  dom (DataPart (Initialize ((intloc 0) .--> 1))) c= (dom (Comput ((P +* I),s,(LifeSpan ((P +* I),s))))) /\ (Data-Locations ) by PARTFUN1:def_2;
then  dom (DataPart (Initialize ((intloc 0) .--> 1))) c= dom (DataPart (Comput ((P +* I),s,(LifeSpan ((P +* I),s))))) by RELAT_1:61;
then  ( DataPart ((Comput ((P +* I),s,(LifeSpan ((P +* I),s)))) +* (Initialize ((intloc 0) .--> 1))) = (DataPart (Comput ((P +* I),s,(LifeSpan ((P +* I),s))))) +* (DataPart (Initialize ((intloc 0) .--> 1))) & DataPart (Initialize ((intloc 0) .--> 1)) c= DataPart (Comput ((P +* I),s,(LifeSpan ((P +* I),s)))) ) by A12, FUNCT_4:71, GRFUNC_1:2;
then A22: DataPart (Comput ((P +* I),s,(LifeSpan ((P +* I),s)))) = DataPart ((Comput ((P +* I),s,(LifeSpan ((P +* I),s)))) +* (Initialize ((intloc 0) .--> 1))) by FUNCT_4:98;
 s = s +* (Start-At (0,SCM+FSA)) by A4, A3, FUNCT_4:98, XBOOLE_1:1;
then  DataPart (Comput (P,s,(LifeSpan ((P +* I),s)))) = DataPart ((Comput ((P +* I),s,(LifeSpan ((P +* I),s)))) +* (Initialize ((intloc 0) .--> 1))) by A22, A8, Th16, A10;
hence A23: DataPart (Comput (P,s,((LifeSpan ((P +* I),s)) + 1))) = DataPart ((Comput ((P +* I),s,(LifeSpan ((P +* I),s)))) +* (Initialize ((intloc 0) .--> 1))) by A10, Th14, A6, A2, A9, XBOOLE_1:1; ::_thesis: ( Reloc (J,(card I)) c= P & (Comput (P,s,((LifeSpan ((P +* I),s)) + 1))) . (intloc 0) = 1 & P halts_on s & LifeSpan (P,s) = ((LifeSpan ((P +* I),s)) + 1) + (LifeSpan (((P +* I) +* J),((Result ((P +* I),s)) +* (Initialize ((intloc 0) .--> 1))))) & ( J is keeping_0 implies (Result (P,s)) . (intloc 0) = 1 ) )
 Reloc (J,(card I)) c= I ";" J by FUNCT_4:25;
hence A24: Reloc (J,(card I)) c= P by A2, XBOOLE_1:1; ::_thesis: ( (Comput (P,s,((LifeSpan ((P +* I),s)) + 1))) . (intloc 0) = 1 & P halts_on s & LifeSpan (P,s) = ((LifeSpan ((P +* I),s)) + 1) + (LifeSpan (((P +* I) +* J),((Result ((P +* I),s)) +* (Initialize ((intloc 0) .--> 1))))) & ( J is keeping_0 implies (Result (P,s)) . (intloc 0) = 1 ) )
 intloc 0 in Int-Locations by AMI_2:def_16;
then A25: intloc 0 in Data-Locations by SCMFSA_2:100, XBOOLE_0:def_3;
hence (Comput (P,s,((LifeSpan ((P +* I),s)) + 1))) . (intloc 0) = (DataPart ((Comput ((P +* I),s,(LifeSpan ((P +* I),s)))) +* (Initialize ((intloc 0) .--> 1)))) . (intloc 0) by A23, FUNCT_1:49
.= ((Comput ((P +* I),s,(LifeSpan ((P +* I),s)))) +* (Initialize ((intloc 0) .--> 1))) . (intloc 0) by A25, FUNCT_1:49
.= 1 by FUNCT_4:13, SCMFSA_M:10, SCMFSA_M:12 ;
::_thesis: ( P halts_on s & LifeSpan (P,s) = ((LifeSpan ((P +* I),s)) + 1) + (LifeSpan (((P +* I) +* J),((Result ((P +* I),s)) +* (Initialize ((intloc 0) .--> 1))))) & ( J is keeping_0 implies (Result (P,s)) . (intloc 0) = 1 ) )
A26: Comput (P,s,(((LifeSpan ((P +* I),s)) + 1) + (LifeSpan (((P +* I) +* J),((Comput ((P +* I),s,(LifeSpan ((P +* I),s)))) +* (Initialize ((intloc 0) .--> 1))))))) = Comput (P,(Comput (P,s,((LifeSpan ((P +* I),s)) + 1))),(LifeSpan (((P +* I) +* J),((Comput ((P +* I),s,(LifeSpan ((P +* I),s)))) +* (Initialize ((intloc 0) .--> 1)))))) by EXTPRO_1:4;
A27: J c= (P +* I) +* J by FUNCT_4:25;
then  IncAddr ((CurInstr (((P +* I) +* J),(Comput (((P +* I) +* J),((Comput ((P +* I),s,(LifeSpan ((P +* I),s)))) +* (Initialize ((intloc 0) .--> 1))),(LifeSpan (((P +* I) +* J),((Comput ((P +* I),s,(LifeSpan ((P +* I),s)))) +* (Initialize ((intloc 0) .--> 1))))))))),(card I)) = CurInstr (P,(Comput (P,(Comput (P,s,((LifeSpan ((P +* I),s)) + 1))),(LifeSpan (((P +* I) +* J),((Comput ((P +* I),s,(LifeSpan ((P +* I),s)))) +* (Initialize ((intloc 0) .--> 1)))))))) by A11, A23, Th6, A24;
then A28: CurInstr (P,(Comput (P,s,m))) = IncAddr ((halt SCM+FSA),(card I)) by A20, A26, EXTPRO_1:def_15
.= halt SCM+FSA by COMPOS_0:4 ;
hence A29: P halts_on s by EXTPRO_1:29; ::_thesis: ( LifeSpan (P,s) = ((LifeSpan ((P +* I),s)) + 1) + (LifeSpan (((P +* I) +* J),((Result ((P +* I),s)) +* (Initialize ((intloc 0) .--> 1))))) & ( J is keeping_0 implies (Result (P,s)) . (intloc 0) = 1 ) )
A30: now__::_thesis:_for_k_being_Element_of_NAT_st_((LifeSpan_((P_+*_I),s))_+_1)_+_k_<_m_holds_
not_CurInstr_(P,(Comput_(P,s,(((LifeSpan_((P_+*_I),s))_+_1)_+_k))))_=_halt_SCM+FSA
let k be Element of NAT ; ::_thesis: ( ((LifeSpan ((P +* I),s)) + 1) + k < m implies not CurInstr (P,(Comput (P,s,(((LifeSpan ((P +* I),s)) + 1) + k)))) = halt SCM+FSA )
assume  ((LifeSpan ((P +* I),s)) + 1) + k < m ; ::_thesis: not CurInstr (P,(Comput (P,s,(((LifeSpan ((P +* I),s)) + 1) + k)))) = halt SCM+FSA
then A31: k < LifeSpan (((P +* I) +* J),((Comput ((P +* I),s,(LifeSpan ((P +* I),s)))) +* (Initialize ((intloc 0) .--> 1)))) by XREAL_1:6;
assume A32: CurInstr (P,(Comput (P,s,(((LifeSpan ((P +* I),s)) + 1) + k)))) = halt SCM+FSA ; ::_thesis: contradiction
A33: InsCode (halt SCM+FSA) = 0 by COMPOS_1:70;
IncAddr ((CurInstr (((P +* I) +* J),(Comput (((P +* I) +* J),((Comput ((P +* I),s,(LifeSpan ((P +* I),s)))) +* (Initialize ((intloc 0) .--> 1))),k)))),(card I)) = CurInstr (P,(Comput (P,(Comput (P,s,((LifeSpan ((P +* I),s)) + 1))),k))) by A11, A23, Th6, A27, A24
.= halt SCM+FSA by A32, EXTPRO_1:4 ;
then  InsCode (CurInstr (((P +* I) +* J),(Comput (((P +* I) +* J),((Comput ((P +* I),s,(LifeSpan ((P +* I),s)))) +* (Initialize ((intloc 0) .--> 1))),k)))) = 0 by COMPOS_0:def_9, A33;
then  CurInstr (((P +* I) +* J),(Comput (((P +* I) +* J),((Comput ((P +* I),s,(LifeSpan ((P +* I),s)))) +* (Initialize ((intloc 0) .--> 1))),k))) = halt SCM+FSA by SCMFSA_2:95;
hence  contradiction by A20, A31, EXTPRO_1:def_15; ::_thesis: verum
end;
now__::_thesis:_for_k_being_Element_of_NAT_st_k_<_m_holds_
CurInstr_(P,(Comput_(P,s,k)))_<>_halt_SCM+FSA
let k be Element of NAT ; ::_thesis: ( k < m implies CurInstr (P,(Comput (P,s,b1))) <> halt SCM+FSA )
assume A34: k < m ; ::_thesis: CurInstr (P,(Comput (P,s,b1))) <> halt SCM+FSA
percases ( k <= LifeSpan ((P +* I),s) or LifeSpan ((P +* I),s) < k ) ;
supposeA35: k <= LifeSpan ((P +* I),s) ; ::_thesis: CurInstr (P,(Comput (P,s,b1))) <> halt SCM+FSA
 (P +* I) +* (Directed I) = P +* (Directed I) by A1, FUNCT_4:74;
hence  CurInstr (P,(Comput (P,s,k))) <> halt SCM+FSA by A3, Th15, A35, A7, FUNCT_4:25; ::_thesis: verum
end;
suppose LifeSpan ((P +* I),s) < k ; ::_thesis: CurInstr (P,(Comput (P,s,b1))) <> halt SCM+FSA
then  (LifeSpan ((P +* I),s)) + 1 <= k by NAT_1:13;
then consider kk being Nat such that
A36: ((LifeSpan ((P +* I),s)) + 1) + kk = k by NAT_1:10;
 kk in NAT by ORDINAL1:def_12;
hence  CurInstr (P,(Comput (P,s,k))) <> halt SCM+FSA by A30, A34, A36; ::_thesis: verum
end;
end;
end;
then A37: for k being Element of NAT st CurInstr (P,(Comput (P,s,k))) = halt SCM+FSA holds
m <= k ;
then A38: LifeSpan (P,s) = m by A28, A29, EXTPRO_1:def_15;
 P +* I halts_on s by Th2, A3, FUNCT_4:25;
then  Comput ((P +* I),s,(LifeSpan ((P +* I),s))) = Result ((P +* I),s) by EXTPRO_1:23;
hence  LifeSpan (P,s) = ((LifeSpan ((P +* I),s)) + 1) + (LifeSpan (((P +* I) +* J),((Result ((P +* I),s)) +* (Initialize ((intloc 0) .--> 1))))) by A37, A28, A29, EXTPRO_1:def_15; ::_thesis: ( J is keeping_0 implies (Result (P,s)) . (intloc 0) = 1 )
hereby  ::_thesis: verum
A39: DataPart (Comput (((P +* I) +* J),((Comput ((P +* I),s,(LifeSpan ((P +* I),s)))) +* (Initialize ((intloc 0) .--> 1))),(LifeSpan (((P +* I) +* J),((Comput ((P +* I),s,(LifeSpan ((P +* I),s)))) +* (Initialize ((intloc 0) .--> 1))))))) = DataPart (Comput (P,(Comput (P,s,((LifeSpan ((P +* I),s)) + 1))),(LifeSpan (((P +* I) +* J),((Comput ((P +* I),s,(LifeSpan ((P +* I),s)))) +* (Initialize ((intloc 0) .--> 1))))))) by A11, A23, Th6, A27, A24;
A40: J c= (P +* I) +* J by FUNCT_4:25;
assume A41: J is keeping_0 ; ::_thesis: (Result (P,s)) . (intloc 0) = 1
thus (Result (P,s)) . (intloc 0) = (Comput (P,s,m)) . (intloc 0) by A29, A38, EXTPRO_1:23
.= (Comput (P,(Comput (P,s,((LifeSpan ((P +* I),s)) + 1))),(LifeSpan (((P +* I) +* J),((Comput ((P +* I),s,(LifeSpan ((P +* I),s)))) +* (Initialize ((intloc 0) .--> 1))))))) . (intloc 0) by EXTPRO_1:4
.= (Comput (((P +* I) +* J),((Comput ((P +* I),s,(LifeSpan ((P +* I),s)))) +* (Initialize ((intloc 0) .--> 1))),(LifeSpan (((P +* I) +* J),((Comput ((P +* I),s,(LifeSpan ((P +* I),s)))) +* (Initialize ((intloc 0) .--> 1))))))) . (intloc 0) by A39, SCMFSA_M:2
.= ((Comput ((P +* I),s,(LifeSpan ((P +* I),s)))) +* (Initialize ((intloc 0) .--> 1))) . (intloc 0) by A41, Def4, A40
.= 1 by A19, GRFUNC_1:2, SCMFSA_M:10, SCMFSA_M:12 ; ::_thesis: verum
end;
end;

registration
let I, J be parahalting Program of ;
clusterI ";" J ->  parahalting ;
coherence
 I ";" J is parahalting
proof
set D = Data-Locations ;
let s be 0 -started State of SCM+FSA; :: according to AMISTD_1:def_11 ::_thesis: for b1 being set holds
( not I ";" J c= b1 or b1 halts_on s )
let P be Instruction-Sequence of SCM+FSA; ::_thesis: ( not I ";" J c= P or P halts_on s )
assume A1: I ";" J c= P ; ::_thesis: P halts_on s
set JAt = Start-At (0,SCM+FSA);
set s3 = Initialize (Comput ((P +* I),s,(LifeSpan ((P +* I),s))));
set m1 = LifeSpan ((P +* I),s);
set m3 = LifeSpan (((P +* I) +* J),(Initialize (Comput ((P +* I),s,(LifeSpan ((P +* I),s))))));
reconsider kk = DataPart (Start-At (0,SCM+FSA)) as Function ;
A2: now__::_thesis:_for_x_being_set_st_x_in_dom_(DataPart_(Start-At_(0,SCM+FSA)))_holds_
kk_._x_=_(DataPart_(Comput_((P_+*_I),s,(LifeSpan_((P_+*_I),s)))))_._x
let x be set ; ::_thesis: ( x in dom (DataPart (Start-At (0,SCM+FSA))) implies kk . x = (DataPart (Comput ((P +* I),s,(LifeSpan ((P +* I),s))))) . x )
assume  x in dom (DataPart (Start-At (0,SCM+FSA))) ; ::_thesis: kk . x = (DataPart (Comput ((P +* I),s,(LifeSpan ((P +* I),s))))) . x
then A3: x in (dom (Start-At (0,SCM+FSA))) /\ (Data-Locations ) by RELAT_1:61;
 x in dom (Start-At (0,SCM+FSA)) by A3, XBOOLE_0:def_4;
then  x in {(IC )} by FUNCOP_1:13;
then  x = IC by TARSKI:def_1;
then  not x in Data-Locations by STRUCT_0:3;
hence  kk . x = (DataPart (Comput ((P +* I),s,(LifeSpan ((P +* I),s))))) . x by A3, XBOOLE_0:def_4; ::_thesis: verum
end;
 Start-At (0,SCM+FSA) c= Initialize (Comput ((P +* I),s,(LifeSpan ((P +* I),s)))) by FUNCT_4:25;
then  dom (Start-At (0,SCM+FSA)) c= dom (Initialize (Comput ((P +* I),s,(LifeSpan ((P +* I),s))))) by GRFUNC_1:2;
then A4: dom (Start-At (0,SCM+FSA)) c= the carrier of SCM+FSA by PARTFUN1:def_2;
 dom (DataPart (Start-At (0,SCM+FSA))) = (dom (Start-At (0,SCM+FSA))) /\ (Data-Locations ) by RELAT_1:61;
then  dom (DataPart (Start-At (0,SCM+FSA))) c= the carrier of SCM+FSA /\ (Data-Locations ) by A4, XBOOLE_1:26;
then  dom (DataPart (Start-At (0,SCM+FSA))) c= (dom (Comput ((P +* I),s,(LifeSpan ((P +* I),s))))) /\ (Data-Locations ) by PARTFUN1:def_2;
then  dom (DataPart (Start-At (0,SCM+FSA))) c= dom (DataPart (Comput ((P +* I),s,(LifeSpan ((P +* I),s))))) by RELAT_1:61;
then  ( (Initialize (Comput ((P +* I),s,(LifeSpan ((P +* I),s))))) | (Data-Locations ) = (DataPart (Comput ((P +* I),s,(LifeSpan ((P +* I),s))))) +* kk & DataPart (Start-At (0,SCM+FSA)) c= DataPart (Comput ((P +* I),s,(LifeSpan ((P +* I),s)))) ) by A2, FUNCT_4:71, GRFUNC_1:2;
then A5: DataPart (Comput ((P +* I),s,(LifeSpan ((P +* I),s)))) = DataPart (Initialize (Comput ((P +* I),s,(LifeSpan ((P +* I),s))))) by FUNCT_4:98;
reconsider m = ((LifeSpan ((P +* I),s)) + 1) + (LifeSpan (((P +* I) +* J),(Initialize (Comput ((P +* I),s,(LifeSpan ((P +* I),s))))))) as Element of NAT ;
A6: Reloc (J,(card I)) c= I ";" J by FUNCT_4:25;
take  m ; :: according to EXTPRO_1:def_8 ::_thesis: ( IC (Comput (P,s,m)) in dom P & CurInstr (P,(Comput (P,s,m))) = halt SCM+FSA )
set s4 = Comput (P,s,((LifeSpan ((P +* I),s)) + 1));
A7: Directed I c= I ";" J by SCMFSA6A:16;
A8: P +* I halts_on s by Th1, FUNCT_4:25;
then A9: IC (Comput (P,s,((LifeSpan ((P +* I),s)) + 1))) = card I by Th13, A7, A1, XBOOLE_1:1;
A10: P +* (I ";" J) = P by A1, FUNCT_4:98;
A11: DataPart (Comput (P,s,(LifeSpan ((P +* I),s)))) = DataPart (Initialize (Comput ((P +* I),s,(LifeSpan ((P +* I),s))))) by A5, A10, Th16, A8;
A12: Comput (P,s,(((LifeSpan ((P +* I),s)) + 1) + (LifeSpan (((P +* I) +* J),(Initialize (Comput ((P +* I),s,(LifeSpan ((P +* I),s))))))))) = Comput (P,(Comput (P,s,((LifeSpan ((P +* I),s)) + 1))),(LifeSpan (((P +* I) +* J),(Initialize (Comput ((P +* I),s,(LifeSpan ((P +* I),s)))))))) by EXTPRO_1:4;
A13: DataPart (Comput (P,s,((LifeSpan ((P +* I),s)) + 1))) = DataPart (Initialize (Comput ((P +* I),s,(LifeSpan ((P +* I),s))))) by A11, Th14, A7, A8, A1, XBOOLE_1:1;
A14: J c= (P +* I) +* J by FUNCT_4:25;
A15: Reloc (J,(card I)) c= P by A6, A1, XBOOLE_1:1;
A16: IncAddr ((CurInstr (((P +* I) +* J),(Comput (((P +* I) +* J),(Initialize (Comput ((P +* I),s,(LifeSpan ((P +* I),s))))),(LifeSpan (((P +* I) +* J),(Initialize (Comput ((P +* I),s,(LifeSpan ((P +* I),s))))))))))),(card I)) = CurInstr (P,(Comput (P,(Comput (P,s,((LifeSpan ((P +* I),s)) + 1))),(LifeSpan (((P +* I) +* J),(Initialize (Comput ((P +* I),s,(LifeSpan ((P +* I),s)))))))))) by Th6, A14, A13, A9, A15;
 dom P = NAT by PARTFUN1:def_2;
hence  IC (Comput (P,s,m)) in dom P ; ::_thesis: CurInstr (P,(Comput (P,s,m))) = halt SCM+FSA
A17: J c= (P +* I) +* J by FUNCT_4:25;
 (P +* I) +* J halts_on Initialize (Comput ((P +* I),s,(LifeSpan ((P +* I),s)))) by A17, AMISTD_1:def_11;
then  CurInstr (P,(Comput (P,s,m))) = IncAddr ((halt SCM+FSA),(card I)) by A16, A12, EXTPRO_1:def_15
.= halt SCM+FSA by COMPOS_0:4 ;
hence  CurInstr (P,(Comput (P,s,m))) = halt SCM+FSA ; ::_thesis: verum
end;
end;

theorem Th17: :: SCMFSA6B:17
for P being Instruction-Sequence of SCM+FSA
for s being 0 -started State of SCM+FSA
for I being keeping_0 Program of st not P +* I halts_on s holds
for J being Program of
for k being Element of NAT holds Comput ((P +* I),s,k) = Comput ((P +* (I ";" J)),s,k)
proof
let P be Instruction-Sequence of SCM+FSA; ::_thesis: for s being 0 -started State of SCM+FSA
for I being keeping_0 Program of st not P +* I halts_on s holds
for J being Program of
for k being Element of NAT holds Comput ((P +* I),s,k) = Comput ((P +* (I ";" J)),s,k)
let s be 0 -started State of SCM+FSA; ::_thesis: for I being keeping_0 Program of st not P +* I halts_on s holds
for J being Program of
for k being Element of NAT holds Comput ((P +* I),s,k) = Comput ((P +* (I ";" J)),s,k)
let I be keeping_0 Program of ; ::_thesis: ( not P +* I halts_on s implies for J being Program of
for k being Element of NAT holds Comput ((P +* I),s,k) = Comput ((P +* (I ";" J)),s,k) )
assume A1: not P +* I halts_on s ; ::_thesis: for J being Program of
for k being Element of NAT holds Comput ((P +* I),s,k) = Comput ((P +* (I ";" J)),s,k)
let J be Program of ; ::_thesis: for k being Element of NAT holds Comput ((P +* I),s,k) = Comput ((P +* (I ";" J)),s,k)
defpred S1[ Nat] means  Comput ((P +* I),s,$1) = Comput ((P +* (I ";" J)),s,$1);
A2: for m being Element of NAT st S1[m] holds
S1[m + 1]
proof
dom (I ";" J) = (dom (Directed I)) \/ (dom (Reloc (J,(card I)))) by FUNCT_4:def_1
.= (dom I) \/ (dom (Reloc (J,(card I)))) by FUNCT_4:99 ;
then A3: dom I c= dom (I ";" J) by XBOOLE_1:7;
let m be Element of NAT ; ::_thesis: ( S1[m] implies S1[m + 1] )
A4: Comput ((P +* I),s,(m + 1)) = Following ((P +* I),(Comput ((P +* I),s,m))) by EXTPRO_1:3
.= Exec ((CurInstr ((P +* I),(Comput ((P +* I),s,m)))),(Comput ((P +* I),s,m))) ;
A5: Comput ((P +* (I ";" J)),s,(m + 1)) = Following ((P +* (I ";" J)),(Comput ((P +* (I ";" J)),s,m))) by EXTPRO_1:3
.= Exec ((CurInstr ((P +* (I ";" J)),(Comput ((P +* (I ";" J)),s,m)))),(Comput ((P +* (I ";" J)),s,m))) ;
A6: I c= P +* I by FUNCT_4:25;
then A7: IC (Comput ((P +* I),s,m)) in dom I by AMISTD_1:def_10;
assume A8: Comput ((P +* I),s,m) = Comput ((P +* (I ";" J)),s,m) ; ::_thesis: S1[m + 1]
 dom (P +* I) = NAT by PARTFUN1:def_2;
then A9: (P +* I) /. (IC (Comput ((P +* I),s,m))) = (P +* I) . (IC (Comput ((P +* I),s,m))) by PARTFUN1:def_6;
 dom (P +* (I ";" J)) = NAT by PARTFUN1:def_2;
then A10: (P +* (I ";" J)) /. (IC (Comput ((P +* (I ";" J)),s,m))) = (P +* (I ";" J)) . (IC (Comput ((P +* (I ";" J)),s,m))) by PARTFUN1:def_6;
A11: I ";" J c= P +* (I ";" J) by FUNCT_4:25;
A12: CurInstr ((P +* I),(Comput ((P +* I),s,m))) = I . (IC (Comput ((P +* I),s,m))) by A7, A9, A6, GRFUNC_1:2;
then  I . (IC (Comput ((P +* I),s,m))) <> halt SCM+FSA by A1, EXTPRO_1:29;
then  CurInstr ((P +* I),(Comput ((P +* I),s,m))) = (I ";" J) . (IC (Comput ((P +* I),s,m))) by A7, A12, SCMFSA6A:15
.= CurInstr ((P +* (I ";" J)),(Comput ((P +* (I ";" J)),s,m))) by A8, A7, A3, A10, A11, GRFUNC_1:2 ;
hence  S1[m + 1] by A8, A4, A5; ::_thesis: verum
end;
A13: S1[ 0 ] ;
thus  for k being Element of NAT holds S1[k] from NAT_1:sch_1(A13, A2); ::_thesis: verum
end;

theorem Th18: :: SCMFSA6B:18
for P being Instruction-Sequence of SCM+FSA
for s being 0 -started State of SCM+FSA
for I being keeping_0 Program of st P +* I halts_on s holds
for J being paraclosed Program of st I ";" J c= P holds
for k being Element of NAT holds IncIC ((Comput (((P +* I) +* J),(Initialize (Result ((P +* I),s))),k)),(card I)) = Comput ((P +* (I ";" J)),s,(((LifeSpan ((P +* I),s)) + 1) + k))
proof
let P be Instruction-Sequence of SCM+FSA; ::_thesis: for s being 0 -started State of SCM+FSA
for I being keeping_0 Program of st P +* I halts_on s holds
for J being paraclosed Program of st I ";" J c= P holds
for k being Element of NAT holds IncIC ((Comput (((P +* I) +* J),(Initialize (Result ((P +* I),s))),k)),(card I)) = Comput ((P +* (I ";" J)),s,(((LifeSpan ((P +* I),s)) + 1) + k))
let s be 0 -started State of SCM+FSA; ::_thesis: for I being keeping_0 Program of st P +* I halts_on s holds
for J being paraclosed Program of st I ";" J c= P holds
for k being Element of NAT holds IncIC ((Comput (((P +* I) +* J),(Initialize (Result ((P +* I),s))),k)),(card I)) = Comput ((P +* (I ";" J)),s,(((LifeSpan ((P +* I),s)) + 1) + k))
let I be keeping_0 Program of ; ::_thesis: ( P +* I halts_on s implies for J being paraclosed Program of st I ";" J c= P holds
for k being Element of NAT holds IncIC ((Comput (((P +* I) +* J),(Initialize (Result ((P +* I),s))),k)),(card I)) = Comput ((P +* (I ";" J)),s,(((LifeSpan ((P +* I),s)) + 1) + k)) )
assume A1: P +* I halts_on s ; ::_thesis: for J being paraclosed Program of st I ";" J c= P holds
for k being Element of NAT holds IncIC ((Comput (((P +* I) +* J),(Initialize (Result ((P +* I),s))),k)),(card I)) = Comput ((P +* (I ";" J)),s,(((LifeSpan ((P +* I),s)) + 1) + k))
let J be paraclosed Program of ; ::_thesis: ( I ";" J c= P implies for k being Element of NAT holds IncIC ((Comput (((P +* I) +* J),(Initialize (Result ((P +* I),s))),k)),(card I)) = Comput ((P +* (I ";" J)),s,(((LifeSpan ((P +* I),s)) + 1) + k)) )
set RI = Result ((P +* I),s);
set JSA0 = Start-At (0,SCM+FSA);
set RIJ = (Result ((P +* I),s)) +* (Start-At (0,SCM+FSA));
defpred S1[ Nat] means  IncIC ((Comput (((P +* I) +* J),((Result ((P +* I),s)) +* (Start-At (0,SCM+FSA))),$1)),(card I)) = Comput ((P +* (I ";" J)),s,(((LifeSpan ((P +* I),s)) + 1) + $1));
assume A2: I ";" J c= P ; ::_thesis: for k being Element of NAT holds IncIC ((Comput (((P +* I) +* J),(Initialize (Result ((P +* I),s))),k)),(card I)) = Comput ((P +* (I ";" J)),s,(((LifeSpan ((P +* I),s)) + 1) + k))
then A3: P +* (I ";" J) = P by FUNCT_4:98;
A4: for n being Element of NAT st S1[n] holds
S1[n + 1]
proof
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
set k1 = k + 1;
set CRk = Comput (((P +* I) +* J),((Result ((P +* I),s)) +* (Start-At (0,SCM+FSA))),k);
set CRSk = IncIC ((Comput (((P +* I) +* J),((Result ((P +* I),s)) +* (Start-At (0,SCM+FSA))),k)),(card I));
set CIJk = Comput ((P +* (I ";" J)),s,(((LifeSpan ((P +* I),s)) + 1) + k));
set CRk1 = Comput (((P +* I) +* J),((Result ((P +* I),s)) +* (Start-At (0,SCM+FSA))),(k + 1));
set CRSk1 = IncIC ((Comput (((P +* I) +* J),((Result ((P +* I),s)) +* (Start-At (0,SCM+FSA))),(k + 1))),(card I));
set CIJk1 = Comput ((P +* (I ";" J)),s,(((LifeSpan ((P +* I),s)) + 1) + (k + 1)));
assume A5: IncIC ((Comput (((P +* I) +* J),((Result ((P +* I),s)) +* (Start-At (0,SCM+FSA))),k)),(card I)) = Comput ((P +* (I ";" J)),s,(((LifeSpan ((P +* I),s)) + 1) + k)) ; ::_thesis: S1[k + 1]
A6: IncAddr ((CurInstr (((P +* I) +* J),(Comput (((P +* I) +* J),((Result ((P +* I),s)) +* (Start-At (0,SCM+FSA))),k)))),(card I)) = CurInstr ((P +* (I ";" J)),(Comput ((P +* (I ";" J)),s,(((LifeSpan ((P +* I),s)) + 1) + k))))
proof
A7: I ";" J c= P +* (I ";" J) by FUNCT_4:25;
 Reloc (J,(card I)) c= I ";" J by FUNCT_4:25;
then A8: Reloc (J,(card I)) c= P +* (I ";" J) by A7, XBOOLE_1:1;
A9: dom (P +* (I ";" J)) = NAT by PARTFUN1:def_2;
A10: CurInstr ((P +* (I ";" J)),(Comput ((P +* (I ";" J)),s,(((LifeSpan ((P +* I),s)) + 1) + k)))) = (P +* (I ";" J)) . (IC (IncIC ((Comput (((P +* I) +* J),((Result ((P +* I),s)) +* (Start-At (0,SCM+FSA))),k)),(card I)))) by A5, A9, PARTFUN1:def_6
.= (P +* (I ";" J)) . ((IC (Comput (((P +* I) +* J),((Result ((P +* I),s)) +* (Start-At (0,SCM+FSA))),k))) + (card I)) by FUNCT_4:113 ;
reconsider ii = IC (Comput (((P +* I) +* J),((Result ((P +* I),s)) +* (Start-At (0,SCM+FSA))),k)) as Element of NAT ;
 J c= (P +* I) +* J by FUNCT_4:25;
then A11: IC (Comput (((P +* I) +* J),((Result ((P +* I),s)) +* (Start-At (0,SCM+FSA))),k)) in dom J by AMISTD_1:def_10;
then A12: IC (Comput (((P +* I) +* J),((Result ((P +* I),s)) +* (Start-At (0,SCM+FSA))),k)) in dom (IncAddr (J,(card I))) by COMPOS_1:def_21;
then A13: (Shift ((IncAddr (J,(card I))),(card I))) . ((IC (Comput (((P +* I) +* J),((Result ((P +* I),s)) +* (Start-At (0,SCM+FSA))),k))) + (card I)) = (IncAddr (J,(card I))) . ii by VALUED_1:def_12
.= IncAddr ((J /. ii),(card I)) by A11, COMPOS_1:def_21 ;
 dom (Shift ((IncAddr (J,(card I))),(card I))) =  {  (il + (card I)) where il is Element of NAT : il in dom (IncAddr (J,(card I)))  }  by VALUED_1:def_12;
then A14: ii + (card I) in dom (Shift ((IncAddr (J,(card I))),(card I))) by A12;
A15: J c= (P +* I) +* J by FUNCT_4:25;
A16: J /. ii = J . ii by A11, PARTFUN1:def_6;
thus  IncAddr ((CurInstr (((P +* I) +* J),(Comput (((P +* I) +* J),((Result ((P +* I),s)) +* (Start-At (0,SCM+FSA))),k)))),(card I)) = IncAddr ((((P +* I) +* J) . (IC (Comput (((P +* I) +* J),((Result ((P +* I),s)) +* (Start-At (0,SCM+FSA))),k)))),(card I)) by PBOOLE:143
.= (Reloc (J,(card I))) . ((IC (Comput (((P +* I) +* J),((Result ((P +* I),s)) +* (Start-At (0,SCM+FSA))),k))) + (card I)) by A13, A15, A16, A11, GRFUNC_1:2
.= CurInstr ((P +* (I ";" J)),(Comput ((P +* (I ";" J)),s,(((LifeSpan ((P +* I),s)) + 1) + k)))) by A10, A8, A14, GRFUNC_1:2 ; ::_thesis: verum
end;
A17: Exec ((CurInstr ((P +* (I ";" J)),(Comput ((P +* (I ";" J)),s,(((LifeSpan ((P +* I),s)) + 1) + k))))),(Comput ((P +* (I ";" J)),s,(((LifeSpan ((P +* I),s)) + 1) + k)))) = IncIC ((Following (((P +* I) +* J),(Comput (((P +* I) +* J),((Result ((P +* I),s)) +* (Start-At (0,SCM+FSA))),k)))),(card I)) by A6, A5, AMISTD_5:4;
 Comput ((P +* (I ";" J)),s,(((LifeSpan ((P +* I),s)) + 1) + (k + 1))) = Comput ((P +* (I ";" J)),s,((((LifeSpan ((P +* I),s)) + 1) + k) + 1)) ;
then A18: Comput ((P +* (I ";" J)),s,(((LifeSpan ((P +* I),s)) + 1) + (k + 1))) = Following ((P +* (I ";" J)),(Comput ((P +* (I ";" J)),s,(((LifeSpan ((P +* I),s)) + 1) + k)))) by EXTPRO_1:3;
A19: for a being Int-Location holds (IncIC ((Comput (((P +* I) +* J),((Result ((P +* I),s)) +* (Start-At (0,SCM+FSA))),(k + 1))),(card I))) . a = (Comput ((P +* (I ";" J)),s,(((LifeSpan ((P +* I),s)) + 1) + (k + 1)))) . a by A18, A17, EXTPRO_1:3;
A20: for f being FinSeq-Location holds (IncIC ((Comput (((P +* I) +* J),((Result ((P +* I),s)) +* (Start-At (0,SCM+FSA))),(k + 1))),(card I))) . f = (Comput ((P +* (I ";" J)),s,(((LifeSpan ((P +* I),s)) + 1) + (k + 1)))) . f by A18, A17, EXTPRO_1:3;
IC (IncIC ((Comput (((P +* I) +* J),((Result ((P +* I),s)) +* (Start-At (0,SCM+FSA))),(k + 1))),(card I))) = (IC (Comput (((P +* I) +* J),((Result ((P +* I),s)) +* (Start-At (0,SCM+FSA))),(k + 1)))) + (card I) by FUNCT_4:113
.= (IC (Following (((P +* I) +* J),(Comput (((P +* I) +* J),((Result ((P +* I),s)) +* (Start-At (0,SCM+FSA))),k))))) + (card I) by EXTPRO_1:3 ;
then  IC (IncIC ((Comput (((P +* I) +* J),((Result ((P +* I),s)) +* (Start-At (0,SCM+FSA))),(k + 1))),(card I))) = IC (Comput ((P +* (I ";" J)),s,(((LifeSpan ((P +* I),s)) + 1) + (k + 1)))) by A18, A17, FUNCT_4:113;
hence  S1[k + 1] by A19, A20, SCMFSA_2:61; ::_thesis: verum
end;
A21: Directed I c= I ";" J by SCMFSA6A:16;
A22: now__::_thesis:_(_IC_(IncIC_(((Result_((P_+*_I),s))_+*_(Start-At_(0,SCM+FSA))),(card_I)))_=_IC_(Comput_((P_+*_(I_";"_J)),s,(((LifeSpan_((P_+*_I),s))_+_1)_+_0)))_&_(_for_a_being_Int-Location_holds_(IncIC_(((Result_((P_+*_I),s))_+*_(Start-At_(0,SCM+FSA))),(card_I)))_._a_=_(Comput_((P_+*_(I_";"_J)),s,(((LifeSpan_((P_+*_I),s))_+_1)_+_0)))_._a_)_&_(_for_f_being_FinSeq-Location_holds_(IncIC_(((Result_((P_+*_I),s))_+*_(Start-At_(0,SCM+FSA))),(card_I)))_._f_=_(Comput_((P_+*_(I_";"_J)),s,(((LifeSpan_((P_+*_I),s))_+_1)_+_0)))_._f_)_)
set s2 = Comput ((P +* (I ";" J)),s,(((LifeSpan ((P +* I),s)) + 1) + 0));
set s1 = IncIC (((Result ((P +* I),s)) +* (Start-At (0,SCM+FSA))),(card I));
thus  IC (IncIC (((Result ((P +* I),s)) +* (Start-At (0,SCM+FSA))),(card I))) = (IC ((Result ((P +* I),s)) +* (Start-At (0,SCM+FSA)))) + (card I) by FUNCT_4:113
.= 0 + (card I) by FUNCT_4:113
.= IC (Comput ((P +* (I ";" J)),s,(((LifeSpan ((P +* I),s)) + 1) + 0))) by A1, A21, Th13, A3, A2, XBOOLE_1:1 ; ::_thesis: ( ( for a being Int-Location holds (IncIC (((Result ((P +* I),s)) +* (Start-At (0,SCM+FSA))),(card I))) . a = (Comput ((P +* (I ";" J)),s,(((LifeSpan ((P +* I),s)) + 1) + 0))) . a ) & ( for f being FinSeq-Location holds (IncIC (((Result ((P +* I),s)) +* (Start-At (0,SCM+FSA))),(card I))) . f = (Comput ((P +* (I ";" J)),s,(((LifeSpan ((P +* I),s)) + 1) + 0))) . f ) )
A23: DataPart (Comput (P,s,(LifeSpan ((P +* I),s)))) = DataPart (Comput (P,s,((LifeSpan ((P +* I),s)) + 1))) by A1, A21, Th14, A2, XBOOLE_1:1;
set o = LifeSpan ((P +* I),s);
hereby  ::_thesis: for f being FinSeq-Location holds (IncIC (((Result ((P +* I),s)) +* (Start-At (0,SCM+FSA))),(card I))) . f = (Comput ((P +* (I ";" J)),s,(((LifeSpan ((P +* I),s)) + 1) + 0))) . f
let a be Int-Location; ::_thesis: (IncIC (((Result ((P +* I),s)) +* (Start-At (0,SCM+FSA))),(card I))) . a = (Comput ((P +* (I ";" J)),s,(((LifeSpan ((P +* I),s)) + 1) + 0))) . a
A24: not a in dom (Start-At (0,SCM+FSA)) by SCMFSA_2:102;
 not a in dom (Start-At (((IC ((Result ((P +* I),s)) +* (Start-At (0,SCM+FSA)))) + (card I)),SCM+FSA)) by SCMFSA_2:102;
hence (IncIC (((Result ((P +* I),s)) +* (Start-At (0,SCM+FSA))),(card I))) . a = ((Result ((P +* I),s)) +* (Start-At (0,SCM+FSA))) . a by FUNCT_4:11
.= (Result ((P +* I),s)) . a by A24, FUNCT_4:11
.= (Comput ((P +* I),s,(LifeSpan ((P +* I),s)))) . a by A1, EXTPRO_1:23
.= (Comput ((P +* (I ";" J)),s,(LifeSpan ((P +* I),s)))) . a by Th16, A1
.= (Comput ((P +* (I ";" J)),s,(((LifeSpan ((P +* I),s)) + 1) + 0))) . a by A23, A3, SCMFSA_M:2 ;
::_thesis: verum
end;
let f be FinSeq-Location ; ::_thesis: (IncIC (((Result ((P +* I),s)) +* (Start-At (0,SCM+FSA))),(card I))) . f = (Comput ((P +* (I ";" J)),s,(((LifeSpan ((P +* I),s)) + 1) + 0))) . f
A25: not f in dom (Start-At (0,SCM+FSA)) by SCMFSA_2:103;
 not f in dom (Start-At (((IC ((Result ((P +* I),s)) +* (Start-At (0,SCM+FSA)))) + (card I)),SCM+FSA)) by SCMFSA_2:103;
hence (IncIC (((Result ((P +* I),s)) +* (Start-At (0,SCM+FSA))),(card I))) . f = ((Result ((P +* I),s)) +* (Start-At (0,SCM+FSA))) . f by FUNCT_4:11
.= (Result ((P +* I),s)) . f by A25, FUNCT_4:11
.= (Comput ((P +* I),s,(LifeSpan ((P +* I),s)))) . f by A1, EXTPRO_1:23
.= (Comput ((P +* (I ";" J)),s,(LifeSpan ((P +* I),s)))) . f by Th16, A1
.= (Comput ((P +* (I ";" J)),s,(((LifeSpan ((P +* I),s)) + 1) + 0))) . f by A23, A3, SCMFSA_M:2 ;
::_thesis: verum
end;
A26: S1[ 0 ] by A22, SCMFSA_2:61;
 for k being Element of NAT holds S1[k] from NAT_1:sch_1(A26, A4);
hence  for k being Element of NAT holds IncIC ((Comput (((P +* I) +* J),(Initialize (Result ((P +* I),s))),k)),(card I)) = Comput ((P +* (I ";" J)),s,(((LifeSpan ((P +* I),s)) + 1) + k)) ; ::_thesis: verum
end;

registration
let I, J be keeping_0 Program of ;
clusterI ";" J ->  keeping_0 ;
coherence
 I ";" J is keeping_0
proof
let s be 0 -started State of SCM+FSA; :: according to SCMFSA6B:def_4 ::_thesis: for P being Instruction-Sequence of SCM+FSA st I ";" J c= P holds
for k being Element of NAT holds (Comput (P,s,k)) . (intloc 0) = s . (intloc 0)
let P be Instruction-Sequence of SCM+FSA; ::_thesis: ( I ";" J c= P implies for k being Element of NAT holds (Comput (P,s,k)) . (intloc 0) = s . (intloc 0) )
assume A1: I ";" J c= P ; ::_thesis: for k being Element of NAT holds (Comput (P,s,k)) . (intloc 0) = s . (intloc 0)
A2: I c= P +* I by FUNCT_4:25;
A3: P = P +* (I ";" J) by A1, FUNCT_4:98;
percases ( P +* I halts_on s or not P +* I halts_on s ) ;
supposeA4: P +* I halts_on s ; ::_thesis: for k being Element of NAT holds (Comput (P,s,k)) . (intloc 0) = s . (intloc 0)
let k be Element of NAT ; ::_thesis: (Comput (P,s,k)) . (intloc 0) = s . (intloc 0)
hereby  ::_thesis: verum
percases ( k <= LifeSpan ((P +* I),s) or k > LifeSpan ((P +* I),s) ) ;
supposeA5: k <= LifeSpan ((P +* I),s) ; ::_thesis: (Comput (P,s,k)) . (intloc 0) = s . (intloc 0)
 (Comput ((P +* I),s,k)) . (intloc 0) = s . (intloc 0) by Def4, A2;
hence  (Comput (P,s,k)) . (intloc 0) = s . (intloc 0) by A3, Th16, A4, A5; ::_thesis: verum
end;
supposeA6: k > LifeSpan ((P +* I),s) ; ::_thesis: (Comput (P,s,k)) . (intloc 0) = s . (intloc 0)
set LS = LifeSpan ((P +* I),s);
consider p being Element of NAT  such that
A7: k = (LifeSpan ((P +* I),s)) + p and
A8: 1 <= p by A6, FINSEQ_4:84;
consider r being Nat such that
A9: p = 1 + r by A8, NAT_1:10;
 ( dom (Start-At (0,SCM+FSA)) = {(IC )} & intloc 0 <> IC ) by FUNCOP_1:13, SCMFSA_2:56;
then A10: not intloc 0 in dom (Start-At (0,SCM+FSA)) by TARSKI:def_1;
reconsider r = r as Element of NAT by ORDINAL1:def_12;
 ( dom (Start-At (((IC (Comput (((P +* I) +* J),(Initialize (Result ((P +* I),s))),r))) + (card I)),SCM+FSA)) = {(IC )} & intloc 0 <> IC ) by FUNCOP_1:13, SCMFSA_2:56;
then A11: not intloc 0 in dom (Start-At (((IC (Comput (((P +* I) +* J),(Initialize (Result ((P +* I),s))),r))) + (card I)),SCM+FSA)) by TARSKI:def_1;
A12: IncIC ((Comput (((P +* I) +* J),(Initialize (Result ((P +* I),s))),r)),(card I)) = Comput ((P +* (I ";" J)),s,(((LifeSpan ((P +* I),s)) + 1) + r)) by A4, Th18, A1;
A13: J c= (P +* I) +* J by FUNCT_4:25;
(Comput (((P +* I) +* J),(Initialize (Result ((P +* I),s))),r)) . (intloc 0) = (Initialize (Result ((P +* I),s))) . (intloc 0) by Def4, A13
.= (Result ((P +* I),s)) . (intloc 0) by A10, FUNCT_4:11
.= (Comput ((P +* I),s,(LifeSpan ((P +* I),s)))) . (intloc 0) by A4, EXTPRO_1:23
.= s . (intloc 0) by Def4, A2 ;
hence  (Comput (P,s,k)) . (intloc 0) = s . (intloc 0) by A7, A9, A12, A3, A11, FUNCT_4:11; ::_thesis: verum
end;
end;
end;
end;
supposeA14: not P +* I halts_on s ; ::_thesis: for k being Element of NAT holds (Comput (P,s,k)) . (intloc 0) = s . (intloc 0)
let k be Element of NAT ; ::_thesis: (Comput (P,s,k)) . (intloc 0) = s . (intloc 0)
 (Comput ((P +* I),s,k)) . (intloc 0) = s . (intloc 0) by Def4, A2;
hence  (Comput (P,s,k)) . (intloc 0) = s . (intloc 0) by A3, A14, Th17; ::_thesis: verum
end;
end;
end;
end;

theorem Th19: :: SCMFSA6B:19
for s being State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA
for I being parahalting keeping_0 Program of
for J being parahalting Program of holds LifeSpan ((P +* (I ";" J)),(s +* (Initialize ((intloc 0) .--> 1)))) = ((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1) + (LifeSpan (((P +* I) +* J),((Result ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) +* (Initialize ((intloc 0) .--> 1)))))
proof
let s be State of SCM+FSA; ::_thesis: for P being Instruction-Sequence of SCM+FSA
for I being parahalting keeping_0 Program of
for J being parahalting Program of holds LifeSpan ((P +* (I ";" J)),(s +* (Initialize ((intloc 0) .--> 1)))) = ((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1) + (LifeSpan (((P +* I) +* J),((Result ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) +* (Initialize ((intloc 0) .--> 1)))))
let P be Instruction-Sequence of SCM+FSA; ::_thesis: for I being parahalting keeping_0 Program of
for J being parahalting Program of holds LifeSpan ((P +* (I ";" J)),(s +* (Initialize ((intloc 0) .--> 1)))) = ((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1) + (LifeSpan (((P +* I) +* J),((Result ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) +* (Initialize ((intloc 0) .--> 1)))))
let I be parahalting keeping_0 Program of ; ::_thesis: for J being parahalting Program of holds LifeSpan ((P +* (I ";" J)),(s +* (Initialize ((intloc 0) .--> 1)))) = ((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1) + (LifeSpan (((P +* I) +* J),((Result ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) +* (Initialize ((intloc 0) .--> 1)))))
let J be parahalting Program of ; ::_thesis: LifeSpan ((P +* (I ";" J)),(s +* (Initialize ((intloc 0) .--> 1)))) = ((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1) + (LifeSpan (((P +* I) +* J),((Result ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) +* (Initialize ((intloc 0) .--> 1)))))
A1: I ";" J c= P +* (I ";" J) by FUNCT_4:25;
 Initialize ((intloc 0) .--> 1) c= s +* (Initialize ((intloc 0) .--> 1)) by FUNCT_4:25;
then A2: LifeSpan ((P +* (I ";" J)),(s +* (Initialize ((intloc 0) .--> 1)))) = ((LifeSpan (((P +* (I ";" J)) +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1) + (LifeSpan ((((P +* (I ";" J)) +* I) +* J),((Result (((P +* (I ";" J)) +* I),(s +* (Initialize ((intloc 0) .--> 1))))) +* (Initialize ((intloc 0) .--> 1))))) by Lm2, A1;
A3: J c= ((P +* (I ";" J)) +* I) +* J by FUNCT_4:25;
A4: J c= (P +* I) +* J by FUNCT_4:25;
A5: I c= (P +* (I ";" J)) +* I by FUNCT_4:25;
A6: I c= P +* I by FUNCT_4:25;
A7: (Result (((P +* (I ";" J)) +* I),(s +* (Initialize ((intloc 0) .--> 1))))) +* (Initialize ((intloc 0) .--> 1)) = (Result ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) +* (Initialize ((intloc 0) .--> 1)) by Th8, A5, A6;
A8: LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1)))) = LifeSpan (((P +* (I ";" J)) +* I),(s +* (Initialize ((intloc 0) .--> 1)))) by Th8, A5, A6;
thus  LifeSpan ((P +* (I ";" J)),(s +* (Initialize ((intloc 0) .--> 1)))) = ((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1) + (LifeSpan (((P +* I) +* J),((Result ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) +* (Initialize ((intloc 0) .--> 1))))) by A7, Th8, A3, A4, A2, A8; ::_thesis: verum
end;

theorem :: SCMFSA6B:20
for s being State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA
for I being parahalting keeping_0 Program of
for J being parahalting Program of holds IExec ((I ";" J),P,s) = IncIC ((IExec (J,P,(IExec (I,P,s)))),(card I))
proof
let s be State of SCM+FSA; ::_thesis: for P being Instruction-Sequence of SCM+FSA
for I being parahalting keeping_0 Program of
for J being parahalting Program of holds IExec ((I ";" J),P,s) = IncIC ((IExec (J,P,(IExec (I,P,s)))),(card I))
let P be Instruction-Sequence of SCM+FSA; ::_thesis: for I being parahalting keeping_0 Program of
for J being parahalting Program of holds IExec ((I ";" J),P,s) = IncIC ((IExec (J,P,(IExec (I,P,s)))),(card I))
set D = Int-Locations \/ FinSeq-Locations;
set A = NAT ;
let I be parahalting keeping_0 Program of ; ::_thesis: for J being parahalting Program of holds IExec ((I ";" J),P,s) = IncIC ((IExec (J,P,(IExec (I,P,s)))),(card I))
let J be parahalting Program of ; ::_thesis: IExec ((I ";" J),P,s) = IncIC ((IExec (J,P,(IExec (I,P,s)))),(card I))
set s1 = s +* (Initialize ((intloc 0) .--> 1));
set P1 = P +* I;
A1: I c= P +* I by FUNCT_4:25;
set s2 = s +* (Initialize ((intloc 0) .--> 1));
set P2 = P +* (I ";" J);
set s3 = (Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) +* (Initialize ((intloc 0) .--> 1));
set P3 = (P +* I) +* J;
set m1 = LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))));
set m3 = LifeSpan (((P +* I) +* J),((Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) +* (Initialize ((intloc 0) .--> 1))));
A2: Initialize ((intloc 0) .--> 1) c= s +* (Initialize ((intloc 0) .--> 1)) by FUNCT_4:25;
A3: I c= (P +* (I ";" J)) +* I by FUNCT_4:25;
A4: I ";" J c= P +* (I ";" J) by FUNCT_4:25;
A5: LifeSpan (((P +* (I ";" J)) +* I),(s +* (Initialize ((intloc 0) .--> 1)))) = LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1)))) by Th8, A1, A3;
A6: Reloc (J,(card I)) c= P +* (I ";" J) by A2, Lm2, A4;
A7: I c= P +* I by FUNCT_4:25;
A8: Initialize ((intloc 0) .--> 1) c= s +* (Initialize ((intloc 0) .--> 1)) by FUNCT_4:25;
A9: (Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) +* (Initialize ((intloc 0) .--> 1)) = (Result ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) +* (Initialize ((intloc 0) .--> 1)) by Th2, A7, A8, EXTPRO_1:23;
A10: ((P +* (I ";" J)) +* I) +* (I ";" J) = (P +* (I ";" J)) +* (I +* (I ";" J)) by FUNCT_4:14
.= P +* ((I ";" J) +* (I +* (I ";" J))) by FUNCT_4:14
.= P +* ((I ";" J) +* (I ";" J)) by SCMFSA6A:18 ;
A11: (P +* I) +* (I ";" J) = P +* (I +* (I ";" J)) by FUNCT_4:14
.= P +* ((I ";" J) +* (I ";" J)) by SCMFSA6A:18 ;
A12: (P +* (I ";" J)) +* I halts_on s +* (Initialize ((intloc 0) .--> 1)) by Th1, FUNCT_4:25;
DataPart (Comput (((P +* (I ";" J)) +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) = DataPart (Comput ((P +* ((I ";" J) +* (I ";" J))),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) by A10, A12, Th12, A5, FUNCT_4:25
.= DataPart (Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) by A11, A7, A8, Th12, Th2 ;
then A13: DataPart ((Comput (((P +* (I ";" J)) +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) +* (Initialize ((intloc 0) .--> 1))) = (DataPart (Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1)))))))) +* (DataPart (Initialize ((intloc 0) .--> 1))) by FUNCT_4:71
.= DataPart ((Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) +* (Initialize ((intloc 0) .--> 1))) by FUNCT_4:71 ;
A14: J c= (P +* I) +* J by FUNCT_4:25;
A15: IC (Comput ((P +* (I ";" J)),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1))) = card I by A2, A5, Lm2, A4;
A16: DataPart (Comput ((P +* (I ";" J)),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1))) = DataPart ((Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) +* (Initialize ((intloc 0) .--> 1))) by A13, A2, A5, Lm2, A4;
then A17: DataPart (Comput ((P +* (I ";" J)),(Comput ((P +* (I ";" J)),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1))),(LifeSpan (((P +* I) +* J),((Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) +* (Initialize ((intloc 0) .--> 1))))))) = DataPart (Comput (((P +* I) +* J),((Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) +* (Initialize ((intloc 0) .--> 1))),(LifeSpan (((P +* I) +* J),((Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) +* (Initialize ((intloc 0) .--> 1))))))) by Th6, A14, A6, A15;
A18: IC (Comput ((P +* (I ";" J)),(Comput ((P +* (I ";" J)),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1))),(LifeSpan (((P +* I) +* J),((Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) +* (Initialize ((intloc 0) .--> 1))))))) = (IC (Comput (((P +* I) +* J),((Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) +* (Initialize ((intloc 0) .--> 1))),(LifeSpan (((P +* I) +* J),((Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) +* (Initialize ((intloc 0) .--> 1)))))))) + (card I) by A15, Th6, A6, A14, A16;
A19: J c= (P +* I) +* J by FUNCT_4:25;
A20: Initialize ((intloc 0) .--> 1) c= (Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) +* (Initialize ((intloc 0) .--> 1)) by FUNCT_4:25;
A21: J c= (P +* I) +* J by FUNCT_4:25;
A22: J c= P +* J by FUNCT_4:25;
A23: Result ((P +* J),((IExec (I,P,s)) +* (Initialize ((intloc 0) .--> 1)))) = Result (((P +* I) +* J),((Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) +* (Initialize ((intloc 0) .--> 1)))) by Th8, A22, A19, A9;
A24: I ";" J c= P +* (I ";" J) by FUNCT_4:25;
then  IExec ((I ";" J),P,s) = Comput ((P +* (I ";" J)),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* (I ";" J)),(s +* (Initialize ((intloc 0) .--> 1)))))) by A2, Th2, EXTPRO_1:23
.= Comput ((P +* (I ";" J)),(s +* (Initialize ((intloc 0) .--> 1))),(((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1) + (LifeSpan (((P +* I) +* J),((Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) +* (Initialize ((intloc 0) .--> 1))))))) by A9, Th19 ;
then A25: DataPart (IExec ((I ";" J),P,s)) = DataPart (Comput (((P +* I) +* J),((Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) +* (Initialize ((intloc 0) .--> 1))),(LifeSpan (((P +* I) +* J),((Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) +* (Initialize ((intloc 0) .--> 1))))))) by A17, EXTPRO_1:4
.= DataPart (IExec (J,P,(IExec (I,P,s)))) by A20, A23, Th2, A19, EXTPRO_1:23 ;
A26: IC (IExec ((I ";" J),P,s)) = IC (Comput ((P +* (I ";" J)),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* (I ";" J)),(s +* (Initialize ((intloc 0) .--> 1))))))) by A24, A2, Th2, EXTPRO_1:23
.= IC (Comput ((P +* (I ";" J)),(s +* (Initialize ((intloc 0) .--> 1))),(((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1) + (LifeSpan (((P +* I) +* J),((Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) +* (Initialize ((intloc 0) .--> 1)))))))) by A9, Th19
.= (IC (Comput (((P +* I) +* J),((Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) +* (Initialize ((intloc 0) .--> 1))),(LifeSpan (((P +* I) +* J),((Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) +* (Initialize ((intloc 0) .--> 1)))))))) + (card I) by A18, EXTPRO_1:4
.= (IC (Result (((P +* I) +* J),((Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) +* (Initialize ((intloc 0) .--> 1)))))) + (card I) by A20, Th2, A19, EXTPRO_1:23
.= (IC (Result (((P +* I) +* J),((Result ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) +* (Initialize ((intloc 0) .--> 1)))))) + (card I) by A8, Th2, A7, EXTPRO_1:23
.= (IC (IExec (J,P,(IExec (I,P,s))))) + (card I) by A21, A22, Th8 ;
hereby  ::_thesis: verum
reconsider l = (IC (IExec (J,P,(IExec (I,P,s))))) + (card I) as Element of NAT ;
A27: dom (Start-At (l,SCM+FSA)) = {(IC )} by FUNCOP_1:13;
A28: now__::_thesis:_for_x_being_set_st_x_in_dom_(IExec_((I_";"_J),P,s))_holds_
(IExec_((I_";"_J),P,s))_._x_=_((IExec_(J,P,(IExec_(I,P,s))))_+*_(Start-At_(((IC_(IExec_(J,P,(IExec_(I,P,s)))))_+_(card_I)),SCM+FSA)))_._x
let x be set ; ::_thesis: ( x in dom (IExec ((I ";" J),P,s)) implies (IExec ((I ";" J),P,s)) . b1 = ((IExec (J,P,(IExec (I,P,s)))) +* (Start-At (((IC (IExec (J,P,(IExec (I,P,s))))) + (card I)),SCM+FSA))) . b1 )
assume A29: x in dom (IExec ((I ";" J),P,s)) ; ::_thesis: (IExec ((I ";" J),P,s)) . b1 = ((IExec (J,P,(IExec (I,P,s)))) +* (Start-At (((IC (IExec (J,P,(IExec (I,P,s))))) + (card I)),SCM+FSA))) . b1
percases ( x is Int-Location or x is FinSeq-Location or x = IC ) by A29, SCMFSA_M:1;
supposeA30: x is Int-Location ; ::_thesis: (IExec ((I ";" J),P,s)) . b1 = ((IExec (J,P,(IExec (I,P,s)))) +* (Start-At (((IC (IExec (J,P,(IExec (I,P,s))))) + (card I)),SCM+FSA))) . b1
then  x <> IC by SCMFSA_2:56;
then A31: not x in dom (Start-At (l,SCM+FSA)) by A27, TARSKI:def_1;
 (IExec ((I ";" J),P,s)) . x = (IExec (J,P,(IExec (I,P,s)))) . x by A25, A30, SCMFSA_M:2;
hence  (IExec ((I ";" J),P,s)) . x = ((IExec (J,P,(IExec (I,P,s)))) +* (Start-At (((IC (IExec (J,P,(IExec (I,P,s))))) + (card I)),SCM+FSA))) . x by A31, FUNCT_4:11; ::_thesis: verum
end;
supposeA32: x is FinSeq-Location ; ::_thesis: (IExec ((I ";" J),P,s)) . b1 = ((IExec (J,P,(IExec (I,P,s)))) +* (Start-At (((IC (IExec (J,P,(IExec (I,P,s))))) + (card I)),SCM+FSA))) . b1
then  x <> IC by SCMFSA_2:57;
then A33: not x in dom (Start-At (l,SCM+FSA)) by A27, TARSKI:def_1;
 (IExec ((I ";" J),P,s)) . x = (IExec (J,P,(IExec (I,P,s)))) . x by A25, A32, SCMFSA_M:2;
hence  (IExec ((I ";" J),P,s)) . x = ((IExec (J,P,(IExec (I,P,s)))) +* (Start-At (((IC (IExec (J,P,(IExec (I,P,s))))) + (card I)),SCM+FSA))) . x by A33, FUNCT_4:11; ::_thesis: verum
end;
supposeA34: x = IC ; ::_thesis: (IExec ((I ";" J),P,s)) . b1 = ((IExec (J,P,(IExec (I,P,s)))) +* (Start-At (((IC (IExec (J,P,(IExec (I,P,s))))) + (card I)),SCM+FSA))) . b1
then  x in {(IC )} by TARSKI:def_1;
then A35: x in dom (Start-At (l,SCM+FSA)) by FUNCOP_1:13;
thus (IExec ((I ";" J),P,s)) . x = (Start-At (l,SCM+FSA)) . (IC ) by A26, A34, FUNCOP_1:72
.= ((IExec (J,P,(IExec (I,P,s)))) +* (Start-At (((IC (IExec (J,P,(IExec (I,P,s))))) + (card I)),SCM+FSA))) . x by A34, A35, FUNCT_4:13 ; ::_thesis: verum
end;
end;
end;
dom (IExec ((I ";" J),P,s)) = the carrier of SCM+FSA by PARTFUN1:def_2
.= dom ((IExec (J,P,(IExec (I,P,s)))) +* (Start-At (((IC (IExec (J,P,(IExec (I,P,s))))) + (card I)),SCM+FSA))) by PARTFUN1:def_2 ;
hence  IExec ((I ";" J),P,s) = IncIC ((IExec (J,P,(IExec (I,P,s)))),(card I)) by A28, FUNCT_1:2; ::_thesis: verum
end;
end;

theorem :: SCMFSA6B:21
for s being State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA holds not P +* ((IC s),(goto (IC s))) halts_on s by Lm1;