:: EXTPRO_1 semantic presentation

begin

definition
let N be set ;
attrc2 is strict ;
struct AMI-Struct over N ->  Mem-Struct over N, COM-Struct ;
aggrAMI-Struct(# carrier, ZeroF, InstructionsF, Object-Kind, ValuesF, Execution #) ->  AMI-Struct over N;
sel Execution c2 ->  Action of the InstructionsF of c2,(product ( the ValuesF of c2 * the Object-Kind of c2));
end;

definition
let N be with_zero set ;
func Trivial-AMI N ->  strict AMI-Struct over N means :Def1: :: EXTPRO_1:def 1
( the carrier of it = {0} & the ZeroF of it = 0 & the InstructionsF of it = {[0,{},{}]} & the Object-Kind of it = 0 .--> 0 & the ValuesF of it = N --> NAT & the Execution of it = [0,{},{}] .--> (id (product ((N --> NAT) * (0 .--> 0)))) );
existence
 ex b1 being strict AMI-Struct over N st
( the carrier of b1 = {0} & the ZeroF of b1 = 0 & the InstructionsF of b1 = {[0,{},{}]} & the Object-Kind of b1 = 0 .--> 0 & the ValuesF of b1 = N --> NAT & the Execution of b1 = [0,{},{}] .--> (id (product ((N --> NAT) * (0 .--> 0)))) )
proof
set I = {[0,{},{}]};
reconsider i = [0,{},{}] as Element of {[0,{},{}]} by TARSKI:def_1;
set f = 0 .--> 0;
A1: dom (0 .--> 0) = dom (0 .--> 0)
.= {0} by FUNCOP_1:13 ;
A2: rng (0 .--> 0) c= {0} by FUNCOP_1:13;
 0 in N by MEASURE6:def_2;
then  {0} c= N by ZFMISC_1:31;
then  rng (0 .--> 0) c= N by A2, XBOOLE_1:1;
then reconsider f = 0 .--> 0 as Function of {0},N by A1, RELSET_1:4;
reconsider y = 0 as Element of {0} by TARSKI:def_1;
reconsider E = {[0,{},{}]} --> (id (product ((N --> NAT) * f))) as Action of {[0,{},{}]},(product ((N --> NAT) * f)) by FUNCOP_1:45, FUNCT_2:9;
take S = AMI-Struct(# {0},y,{[0,{},{}]},f,(N --> NAT),E #); ::_thesis: ( the carrier of S = {0} & the ZeroF of S = 0 & the InstructionsF of S = {[0,{},{}]} & the Object-Kind of S = 0 .--> 0 & the ValuesF of S = N --> NAT & the Execution of S = [0,{},{}] .--> (id (product ((N --> NAT) * (0 .--> 0)))) )
thus  ( the carrier of S = {0} & the ZeroF of S = 0 & the InstructionsF of S = {[0,{},{}]} & the Object-Kind of S = 0 .--> 0 & the ValuesF of S = N --> NAT & the Execution of S = [0,{},{}] .--> (id (product ((N --> NAT) * (0 .--> 0)))) ) ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being strict AMI-Struct over N st the carrier of b1 = {0} & the ZeroF of b1 = 0 & the InstructionsF of b1 = {[0,{},{}]} & the Object-Kind of b1 = 0 .--> 0 & the ValuesF of b1 = N --> NAT & the Execution of b1 = [0,{},{}] .--> (id (product ((N --> NAT) * (0 .--> 0)))) & the carrier of b2 = {0} & the ZeroF of b2 = 0 & the InstructionsF of b2 = {[0,{},{}]} & the Object-Kind of b2 = 0 .--> 0 & the ValuesF of b2 = N --> NAT & the Execution of b2 = [0,{},{}] .--> (id (product ((N --> NAT) * (0 .--> 0)))) holds
b1 = b2 ;
end;

:: deftheorem Def1 defines Trivial-AMI EXTPRO_1:def_1_:_
 for N being with_zero set
for b2 being strict AMI-Struct over N holds
( b2 = Trivial-AMI N iff ( the carrier of b2 = {0} & the ZeroF of b2 = 0 & the InstructionsF of b2 = {[0,{},{}]} & the Object-Kind of b2 = 0 .--> 0 & the ValuesF of b2 = N --> NAT & the Execution of b2 = [0,{},{}] .--> (id (product ((N --> NAT) * (0 .--> 0)))) ) );

registration
let N be with_zero set ;
cluster Trivial-AMI N -> 1 -element strict ;
coherence
 Trivial-AMI N is 1 -element
proof
set S = Trivial-AMI N;
thus  the carrier of (Trivial-AMI N) is 1 -element by Def1; :: according to STRUCT_0:def_19 ::_thesis: verum
end;
end;

registration
let N be with_zero set ;
cluster non empty for AMI-Struct over N;
existence
 not for b1 being AMI-Struct over N holds b1 is empty
proof
take  Trivial-AMI N ; ::_thesis: not Trivial-AMI N is empty
thus  not Trivial-AMI N is empty ; ::_thesis: verum
end;
end;

registration
let N be with_zero set ;
cluster Trivial-AMI N ->  with_non-empty_values strict ;
coherence
 Trivial-AMI N is with_non-empty_values
proof
let n be set ; :: according to FUNCT_1:def_9,MEMSTR_0:def_3 ::_thesis: ( not n in proj1 (the_Values_of (Trivial-AMI N)) or not (the_Values_of (Trivial-AMI N)) . n is empty )
set S = Trivial-AMI N;
set F = the_Values_of (Trivial-AMI N);
assume A1: n in dom (the_Values_of (Trivial-AMI N)) ; ::_thesis: not (the_Values_of (Trivial-AMI N)) . n is empty
then A2: the Object-Kind of (Trivial-AMI N) . n in dom the ValuesF of (Trivial-AMI N) by FUNCT_1:11;
A3: the ValuesF of (Trivial-AMI N) = N --> NAT by Def1;
then A4: the Object-Kind of (Trivial-AMI N) . n in N by A2, FUNCOP_1:13;
(the_Values_of (Trivial-AMI N)) . n = the ValuesF of (Trivial-AMI N) . ( the Object-Kind of (Trivial-AMI N) . n) by A1, FUNCT_1:12
.= NAT by A4, A3, FUNCOP_1:7 ;
hence  not (the_Values_of (Trivial-AMI N)) . n is empty ; ::_thesis: verum
end;
end;

registration
let N be with_zero set ;
cluster1 -element with_non-empty_values for AMI-Struct over N;
existence
 ex b1 being AMI-Struct over N st
( b1 is with_non-empty_values & b1 is 1 -element )
proof
take  Trivial-AMI N ; ::_thesis: ( Trivial-AMI N is with_non-empty_values & Trivial-AMI N is 1 -element )
thus  ( Trivial-AMI N is with_non-empty_values & Trivial-AMI N is 1 -element ) ; ::_thesis: verum
end;
end;

definition
let N be with_zero set ;
let S be with_non-empty_values AMI-Struct over N;
let I be Instruction of S;
let s be State of S;
func Exec (I,s) ->  State of S equals :: EXTPRO_1:def 2
( the Execution of S . I) . s;
coherence
 ( the Execution of S . I) . s is State of S
proof
consider f being Function such that
A1: ( the Execution of S . I = f & dom f = product (the_Values_of S) ) and
A2: rng f c= product (the_Values_of S) by FUNCT_2:def_2;
reconsider s = s as Element of product (the_Values_of S) by CARD_3:107;
 ( the Execution of S . I) . s in rng f by A1, FUNCT_1:def_3;
hence  ( the Execution of S . I) . s is State of S by A2; ::_thesis: verum
end;
end;

:: deftheorem  defines Exec EXTPRO_1:def_2_:_
 for N being with_zero set
for S being with_non-empty_values AMI-Struct over N
for I being Instruction of S
for s being State of S holds Exec (I,s) = ( the Execution of S . I) . s;

definition
let N be with_zero set ;
let S be with_non-empty_values AMI-Struct over N;
let I be Instruction of S;
attrI is halting  means :Def3: :: EXTPRO_1:def 3
 for s being State of S holds Exec (I,s) = s;
end;

:: deftheorem Def3 defines halting EXTPRO_1:def_3_:_
 for N being with_zero set
for S being with_non-empty_values AMI-Struct over N
for I being Instruction of S holds
( I is halting iff for s being State of S holds Exec (I,s) = s );

definition
let N be with_zero set ;
let S be with_non-empty_values AMI-Struct over N;
attrS is halting  means :Def4: :: EXTPRO_1:def 4
 halt S is halting ;
end;

:: deftheorem Def4 defines halting EXTPRO_1:def_4_:_
 for N being with_zero set
for S being with_non-empty_values AMI-Struct over N holds
( S is halting iff halt S is halting );

registration
let N be with_zero set ;
cluster Trivial-AMI N ->  strict halting ;
coherence
 Trivial-AMI N is halting
proof
set T = Trivial-AMI N;
set f = (N --> NAT) * (0 .--> 0);
A1: ( the Object-Kind of (Trivial-AMI N) = 0 .--> 0 & the ValuesF of (Trivial-AMI N) = N --> NAT ) by Def1;
set I = halt (Trivial-AMI N);
let s be State of (Trivial-AMI N); :: according to EXTPRO_1:def_3,EXTPRO_1:def_4 ::_thesis: Exec ((halt (Trivial-AMI N)),s) = s
reconsider ss = s as Element of product (the_Values_of (Trivial-AMI N)) by CARD_3:107;
 ((halt (Trivial-AMI N)) .--> (id (product ((N --> NAT) * (0 .--> 0))))) . (halt (Trivial-AMI N)) = id (product ((N --> NAT) * (0 .--> 0))) by FUNCOP_1:72;
hence  Exec ((halt (Trivial-AMI N)),s) = (id (product ((N --> NAT) * (0 .--> 0)))) . ss by Def1
.= s by A1, FUNCT_1:18 ;
::_thesis: verum
end;
end;

registration
let N be with_zero set ;
cluster non empty with_non-empty_values halting for AMI-Struct over N;
existence
 ex b1 being non empty with_non-empty_values AMI-Struct over N st b1 is halting
proof
take  Trivial-AMI N ; ::_thesis: Trivial-AMI N is halting
thus  Trivial-AMI N is halting ; ::_thesis: verum
end;
end;

registration
let N be with_zero set ;
let S be with_non-empty_values halting AMI-Struct over N;
cluster halt S ->  halting ;
coherence
 halt S is halting by Def4;
end;

registration
let N be with_zero set ;
let S be with_non-empty_values halting AMI-Struct over N;
cluster halting for Element of the InstructionsF of S;
existence
 ex b1 being Instruction of S st b1 is halting
proof
take  halt S ; ::_thesis: halt S is halting
thus  halt S is halting ; ::_thesis: verum
end;
end;

theorem :: EXTPRO_1:1
for N being with_zero set
for s being State of (Trivial-AMI N)
for i being Instruction of (Trivial-AMI N) holds Exec (i,s) = s
proof
let N be with_zero set ; ::_thesis: for s being State of (Trivial-AMI N)
for i being Instruction of (Trivial-AMI N) holds Exec (i,s) = s
set T = Trivial-AMI N;
let s be State of (Trivial-AMI N); ::_thesis: for i being Instruction of (Trivial-AMI N) holds Exec (i,s) = s
let i be Instruction of (Trivial-AMI N); ::_thesis: Exec (i,s) = s
set f = (N --> NAT) * (0 .--> 0);
A1: ( the Object-Kind of (Trivial-AMI N) = 0 .--> 0 & the ValuesF of (Trivial-AMI N) = N --> NAT ) by Def1;
reconsider ss = s as Element of product (the_Values_of (Trivial-AMI N)) by CARD_3:107;
 the InstructionsF of (Trivial-AMI N) = {[0,{},{}]} by Def1;
then  ( (i .--> (id (product ((N --> NAT) * (0 .--> 0))))) . i = id (product ((N --> NAT) * (0 .--> 0))) & i = [0,{},{}] ) by FUNCOP_1:72, TARSKI:def_1;
hence  Exec (i,s) = (id (product ((N --> NAT) * (0 .--> 0)))) . ss by Def1
.= s by A1, FUNCT_1:18 ;
::_thesis: verum
end;

registration
let E be with_zero set ;
cluster Trivial-AMI E ->  IC-Ins-separated strict ;
coherence
 Trivial-AMI E is IC-Ins-separated
proof
set S = Trivial-AMI E;
A1: ( the Object-Kind of (Trivial-AMI E) = 0 .--> 0 & the ValuesF of (Trivial-AMI E) = E --> NAT ) by Def1;
A2: 0 in E by MEASURE6:def_2;
A3: 0 in dom (0 .--> 0) by FUNCOP_1:73;
thus  Values (IC ) = (the_Values_of (Trivial-AMI E)) . 0 by Def1
.= ((E --> NAT) * (0 .--> 0)) . 0 by A1
.= (E --> NAT) . ((0 .--> 0) . 0) by A3, FUNCT_1:13
.= (E --> NAT) . 0 by FUNCOP_1:72
.= NAT by A2, FUNCOP_1:7 ; :: according to MEMSTR_0:def_6 ::_thesis: verum
end;
end;

registration
let M be with_zero set ;
cluster non empty trivial with_non-empty_values IC-Ins-separated strict for AMI-Struct over M;
existence
 ex b1 being non empty with_non-empty_values AMI-Struct over M st
( b1 is IC-Ins-separated & b1 is strict & b1 is trivial )
proof
take  Trivial-AMI M ; ::_thesis: ( Trivial-AMI M is IC-Ins-separated & Trivial-AMI M is strict & Trivial-AMI M is trivial )
thus  ( Trivial-AMI M is IC-Ins-separated & Trivial-AMI M is strict & Trivial-AMI M is trivial ) ; ::_thesis: verum
end;
end;

registration
let N be with_zero set ;
cluster non empty trivial finite 1 -element with_non-empty_values IC-Ins-separated strict halting for AMI-Struct over N;
existence
 ex b1 being 1 -element with_non-empty_values AMI-Struct over N st
( b1 is IC-Ins-separated & b1 is halting & b1 is strict )
proof
take  Trivial-AMI N ; ::_thesis: ( Trivial-AMI N is IC-Ins-separated & Trivial-AMI N is halting & Trivial-AMI N is strict )
thus  ( Trivial-AMI N is IC-Ins-separated & Trivial-AMI N is halting & Trivial-AMI N is strict ) ; ::_thesis: verum
end;
end;

begin


definition
let N be with_zero set ;
let S be non empty with_non-empty_values IC-Ins-separated AMI-Struct over N;
let p be the InstructionsF of S -valued Function;
let s be State of S;
func CurInstr (p,s) ->  Instruction of S equals :: EXTPRO_1:def 5
p /. (IC s);
coherence
 p /. (IC s) is Instruction of S ;
end;

:: deftheorem  defines CurInstr EXTPRO_1:def_5_:_
 for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N
for p being the InstructionsF of b2 -valued Function
for s being State of S holds CurInstr (p,s) = p /. (IC s);

definition
let N be with_zero set ;
let S be non empty with_non-empty_values IC-Ins-separated AMI-Struct over N;
let s be State of S;
let p be the InstructionsF of S -valued Function;
func Following (p,s) ->  State of S equals :: EXTPRO_1:def 6
 Exec ((CurInstr (p,s)),s);
correctness
coherence
Exec ((CurInstr (p,s)),s) is State of S;
;
end;

:: deftheorem  defines Following EXTPRO_1:def_6_:_
 for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N
for s being State of S
for p being the InstructionsF of b2 -valued Function holds Following (p,s) = Exec ((CurInstr (p,s)),s);

definition
let N be with_zero set ;
let S be non empty with_non-empty_values IC-Ins-separated AMI-Struct over N;
let p be NAT -defined the InstructionsF of S -valued Function;
deffunc H1( set , State of S) ->  Element of product (the_Values_of S) = down (Following (p,$2));
let s be State of S;
let k be Nat;
func Comput (p,s,k) ->  State of S means :Def7: :: EXTPRO_1:def 7
 ex f being Function of NAT,(product (the_Values_of S)) st
( it = f . k & f . 0 = s & ( for i being Nat holds f . (i + 1) = Following (p,(f . i)) ) );
existence
 ex b1 being State of S ex f being Function of NAT,(product (the_Values_of S)) st
( b1 = f . k & f . 0 = s & ( for i being Nat holds f . (i + 1) = Following (p,(f . i)) ) )
proof
reconsider ss = s as Element of product (the_Values_of S) by CARD_3:107;
consider f being Function of NAT,(product (the_Values_of S)) such that
A1: f . 0 = ss and
A2: for n being Nat holds f . (n + 1) = H1(n,f . n) from NAT_1:sch_12();
take  f . k ; ::_thesis: ex f being Function of NAT,(product (the_Values_of S)) st
( f . k = f . k & f . 0 = s & ( for i being Nat holds f . (i + 1) = Following (p,(f . i)) ) )
take  f ; ::_thesis: ( f . k = f . k & f . 0 = s & ( for i being Nat holds f . (i + 1) = Following (p,(f . i)) ) )
thus  f . k = f . k ; ::_thesis: ( f . 0 = s & ( for i being Nat holds f . (i + 1) = Following (p,(f . i)) ) )
thus  f . 0 = s by A1; ::_thesis: for i being Nat holds f . (i + 1) = Following (p,(f . i))
let i be Nat; ::_thesis: f . (i + 1) = Following (p,(f . i))
thus f . (i + 1) = H1(i,f . i) by A2
.= Following (p,(f . i)) ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being State of S st ex f being Function of NAT,(product (the_Values_of S)) st
( b1 = f . k & f . 0 = s & ( for i being Nat holds f . (i + 1) = Following (p,(f . i)) ) ) & ex f being Function of NAT,(product (the_Values_of S)) st
( b2 = f . k & f . 0 = s & ( for i being Nat holds f . (i + 1) = Following (p,(f . i)) ) ) holds
b1 = b2
proof
let s1, s2 be State of S; ::_thesis: ( ex f being Function of NAT,(product (the_Values_of S)) st
( s1 = f . k & f . 0 = s & ( for i being Nat holds f . (i + 1) = Following (p,(f . i)) ) ) & ex f being Function of NAT,(product (the_Values_of S)) st
( s2 = f . k & f . 0 = s & ( for i being Nat holds f . (i + 1) = Following (p,(f . i)) ) ) implies s1 = s2 )
given f1 being Function of NAT,(product (the_Values_of S)) such that A3: s1 = f1 . k and
A4: f1 . 0 = s and
A5: for i being Nat holds f1 . (i + 1) = Following (p,(f1 . i)) ; ::_thesis: ( for f being Function of NAT,(product (the_Values_of S)) holds
( not s2 = f . k or not f . 0 = s or ex i being Nat st not f . (i + 1) = Following (p,(f . i)) ) or s1 = s2 )
given f2 being Function of NAT,(product (the_Values_of S)) such that A6: s2 = f2 . k and
A7: f2 . 0 = s and
A8: for i being Nat holds f2 . (i + 1) = Following (p,(f2 . i)) ; ::_thesis: s1 = s2
reconsider s = s as Element of product (the_Values_of S) by CARD_3:107;
A9: f1 . 0 = s by A4;
A10: for i being Nat holds f1 . (i + 1) = H1(i,f1 . i) by A5;
A11: f2 . 0 = s by A7;
A12: for i being Nat holds f2 . (i + 1) = H1(i,f2 . i) by A8;
 f1 = f2 from NAT_1:sch_16(A9, A10, A11, A12);
hence  s1 = s2 by A3, A6; ::_thesis: verum
end;
end;

:: deftheorem Def7 defines Comput EXTPRO_1:def_7_:_
 for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N
for p being NAT -defined the InstructionsF of b2 -valued Function
for s being State of S
for k being Nat
for b6 being State of S holds
( b6 = Comput (p,s,k) iff ex f being Function of NAT,(product (the_Values_of S)) st
( b6 = f . k & f . 0 = s & ( for i being Nat holds f . (i + 1) = Following (p,(f . i)) ) ) );

definition
let N be with_zero set ;
let S be non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N;
let p be NAT -defined the InstructionsF of S -valued Function;
let s be State of S;
predp halts_on s means :Def8: :: EXTPRO_1:def 8
 ex k being Nat st
( IC (Comput (p,s,k)) in dom p & CurInstr (p,(Comput (p,s,k))) = halt S );
end;

:: deftheorem Def8 defines halts_on EXTPRO_1:def_8_:_
 for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N
for p being NAT -defined the InstructionsF of b2 -valued Function
for s being State of S holds
( p halts_on s iff ex k being Nat st
( IC (Comput (p,s,k)) in dom p & CurInstr (p,(Comput (p,s,k))) = halt S ) );

registration
let N be non empty with_zero set ;
let S be non empty with_non-empty_values IC-Ins-separated AMI-Struct over N;
let p be NAT -defined the InstructionsF of S -valued Function;
let s be State of S;
reduce Comput (p,s,0) to s;
reducibility
 Comput (p,s,0) = s
proof
 ex f being Function of NAT,(product (the_Values_of S)) st
( Comput (p,s,0) = f . 0 & f . 0 = s & ( for i being Nat holds f . (i + 1) = Following (p,(f . i)) ) ) by Def7;
hence  Comput (p,s,0) = s ; ::_thesis: verum
end;
end;

theorem :: EXTPRO_1:2
for N being non empty with_zero set
for S being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N
for p being NAT -defined the InstructionsF of b2 -valued Function
for s being State of S holds Comput (p,s,0) = s ;

theorem Th3: :: EXTPRO_1:3
for N being non empty with_zero set
for S being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N
for p being NAT -defined the InstructionsF of b2 -valued Function
for s being State of S
for k being Nat holds Comput (p,s,(k + 1)) = Following (p,(Comput (p,s,k)))
proof
let N be with_zero set ; ::_thesis: for S being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N
for p being NAT -defined the InstructionsF of b1 -valued Function
for s being State of S
for k being Nat holds Comput (p,s,(k + 1)) = Following (p,(Comput (p,s,k)))
let S be non empty with_non-empty_values IC-Ins-separated AMI-Struct over N; ::_thesis: for p being NAT -defined the InstructionsF of S -valued Function
for s being State of S
for k being Nat holds Comput (p,s,(k + 1)) = Following (p,(Comput (p,s,k)))
let p be NAT -defined the InstructionsF of S -valued Function; ::_thesis: for s being State of S
for k being Nat holds Comput (p,s,(k + 1)) = Following (p,(Comput (p,s,k)))
let s be State of S; ::_thesis: for k being Nat holds Comput (p,s,(k + 1)) = Following (p,(Comput (p,s,k)))
let k be Nat; ::_thesis: Comput (p,s,(k + 1)) = Following (p,(Comput (p,s,k)))
deffunc H1( set , State of S) ->  Element of product (the_Values_of S) = down (Following (p,$2));
reconsider s = s as Element of product (the_Values_of S) by CARD_3:107;
consider f being Function of NAT,(product (the_Values_of S)) such that
A1: Comput (p,s,(k + 1)) = f . (k + 1) and
A2: f . 0 = s and
A3: for i being Nat holds f . (i + 1) = Following (p,(f . i)) by Def7;
consider g being Function of NAT,(product (the_Values_of S)) such that
A4: Comput (p,s,k) = g . k and
A5: g . 0 = s and
A6: for i being Nat holds g . (i + 1) = Following (p,(g . i)) by Def7;
A7: for i being Nat holds f . (i + 1) = H1(i,f . i) by A3;
A8: for i being Nat holds g . (i + 1) = H1(i,g . i) by A6;
 f = g from NAT_1:sch_16(A2, A7, A5, A8);
hence  Comput (p,s,(k + 1)) = Following (p,(Comput (p,s,k))) by A1, A4, A6; ::_thesis: verum
end;


theorem Th4: :: EXTPRO_1:4
for i being Element of NAT
for N being non empty with_zero set
for S being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N
for s being State of S
for p being NAT -defined the InstructionsF of b3 -valued Function
for k being Element of NAT holds Comput (p,s,(i + k)) = Comput (p,(Comput (p,s,i)),k)
proof
let i be Element of NAT ; ::_thesis: for N being non empty with_zero set
for S being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N
for s being State of S
for p being NAT -defined the InstructionsF of b2 -valued Function
for k being Element of NAT holds Comput (p,s,(i + k)) = Comput (p,(Comput (p,s,i)),k)
let N be non empty with_zero set ; ::_thesis: for S being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N
for s being State of S
for p being NAT -defined the InstructionsF of b1 -valued Function
for k being Element of NAT holds Comput (p,s,(i + k)) = Comput (p,(Comput (p,s,i)),k)
let S be non empty with_non-empty_values IC-Ins-separated AMI-Struct over N; ::_thesis: for s being State of S
for p being NAT -defined the InstructionsF of S -valued Function
for k being Element of NAT holds Comput (p,s,(i + k)) = Comput (p,(Comput (p,s,i)),k)
let s be State of S; ::_thesis: for p being NAT -defined the InstructionsF of S -valued Function
for k being Element of NAT holds Comput (p,s,(i + k)) = Comput (p,(Comput (p,s,i)),k)
let p be NAT -defined the InstructionsF of S -valued Function; ::_thesis: for k being Element of NAT holds Comput (p,s,(i + k)) = Comput (p,(Comput (p,s,i)),k)
defpred S1[ Element of NAT ] means  Comput (p,s,(i + $1)) = Comput (p,(Comput (p,s,i)),$1);
A1: now__::_thesis:_for_k_being_Element_of_NAT_st_S1[k]_holds_
S1[k_+_1]
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A2: S1[k] ; ::_thesis: S1[k + 1]
Comput (p,s,(i + (k + 1))) = Comput (p,s,((i + k) + 1))
.= Following (p,(Comput (p,s,(i + k)))) by Th3
.= Comput (p,(Comput (p,s,i)),(k + 1)) by A2, Th3 ;
hence  S1[k + 1] ; ::_thesis: verum
end;
A3: S1[ 0 ] ;
thus  for k being Element of NAT holds S1[k] from NAT_1:sch_1(A3, A1); ::_thesis: verum
end;

theorem Th5: :: EXTPRO_1:5
for i, j being Element of NAT st i <= j holds
for N being non empty with_zero set
for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N
for p being NAT -defined the InstructionsF of b4 -valued Function
for s being State of S st CurInstr (p,(Comput (p,s,i))) = halt S holds
Comput (p,s,j) = Comput (p,s,i)
proof
let i, j be Element of NAT ; ::_thesis: ( i <= j implies for N being non empty with_zero set
for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N
for p being NAT -defined the InstructionsF of b2 -valued Function
for s being State of S st CurInstr (p,(Comput (p,s,i))) = halt S holds
Comput (p,s,j) = Comput (p,s,i) )
assume  i <= j ; ::_thesis: for N being non empty with_zero set
for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N
for p being NAT -defined the InstructionsF of b2 -valued Function
for s being State of S st CurInstr (p,(Comput (p,s,i))) = halt S holds
Comput (p,s,j) = Comput (p,s,i)
then consider k being Nat such that
A1: j = i + k by NAT_1:10;
reconsider k = k as Element of NAT by ORDINAL1:def_12;
A2: j = i + k by A1;
let N be non empty with_zero set ; ::_thesis: for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N
for p being NAT -defined the InstructionsF of b1 -valued Function
for s being State of S st CurInstr (p,(Comput (p,s,i))) = halt S holds
Comput (p,s,j) = Comput (p,s,i)
let S be non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N; ::_thesis: for p being NAT -defined the InstructionsF of S -valued Function
for s being State of S st CurInstr (p,(Comput (p,s,i))) = halt S holds
Comput (p,s,j) = Comput (p,s,i)
let p be NAT -defined the InstructionsF of S -valued Function; ::_thesis: for s being State of S st CurInstr (p,(Comput (p,s,i))) = halt S holds
Comput (p,s,j) = Comput (p,s,i)
let s be State of S; ::_thesis: ( CurInstr (p,(Comput (p,s,i))) = halt S implies Comput (p,s,j) = Comput (p,s,i) )
assume A3: CurInstr (p,(Comput (p,s,i))) = halt S ; ::_thesis: Comput (p,s,j) = Comput (p,s,i)
defpred S1[ Element of NAT ] means  Comput (p,s,(i + $1)) = Comput (p,s,i);
A4: now__::_thesis:_for_k_being_Element_of_NAT_st_S1[k]_holds_
S1[k_+_1]
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A5: S1[k] ; ::_thesis: S1[k + 1]
Comput (p,s,(i + (k + 1))) = Comput (p,s,((i + k) + 1))
.= Following (p,(Comput (p,s,(i + k)))) by Th3
.= Comput (p,s,i) by A3, A5, Def3 ;
hence  S1[k + 1] ; ::_thesis: verum
end;
A6: S1[ 0 ] ;
 for k being Element of NAT holds S1[k] from NAT_1:sch_1(A6, A4);
hence  Comput (p,s,j) = Comput (p,s,i) by A2; ::_thesis: verum
end;

definition
let N be non empty with_zero set ;
let S be non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N;
let p be NAT -defined the InstructionsF of S -valued Function;
let s be State of S;
assume A1: p halts_on s ;
func Result (p,s) ->  State of S means :Def9: :: EXTPRO_1:def 9
 ex k being Element of NAT st
( it = Comput (p,s,k) & CurInstr (p,it) = halt S );
uniqueness
 for b1, b2 being State of S st ex k being Element of NAT st
( b1 = Comput (p,s,k) & CurInstr (p,b1) = halt S ) & ex k being Element of NAT st
( b2 = Comput (p,s,k) & CurInstr (p,b2) = halt S ) holds
b1 = b2
proof
let s1, s2 be State of S; ::_thesis: ( ex k being Element of NAT st
( s1 = Comput (p,s,k) & CurInstr (p,s1) = halt S ) & ex k being Element of NAT st
( s2 = Comput (p,s,k) & CurInstr (p,s2) = halt S ) implies s1 = s2 )
given k1 being Element of NAT  such that A1: ( s1 = Comput (p,s,k1) & CurInstr (p,s1) = halt S ) ; ::_thesis: ( for k being Element of NAT holds
( not s2 = Comput (p,s,k) or not CurInstr (p,s2) = halt S ) or s1 = s2 )
given k2 being Element of NAT  such that A2: ( s2 = Comput (p,s,k2) & CurInstr (p,s2) = halt S ) ; ::_thesis: s1 = s2
 ( k1 <= k2 or k2 <= k1 ) ;
hence  s1 = s2 by A1, A2, Th5; ::_thesis: verum
end;
correctness
existence
ex b1 being State of S ex k being Element of NAT st
( b1 = Comput (p,s,k) & CurInstr (p,b1) = halt S );
proof
consider k being Nat such that
 IC (Comput (p,s,k)) in dom p and
A3: CurInstr (p,(Comput (p,s,k))) = halt S by A1, Def8;
 k in NAT by ORDINAL1:def_12;
hence  ex b1 being State of S ex k being Element of NAT st
( b1 = Comput (p,s,k) & CurInstr (p,b1) = halt S ) by A3; ::_thesis: verum
end;
end;

:: deftheorem Def9 defines Result EXTPRO_1:def_9_:_
 for N being non empty with_zero set
for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N
for p being NAT -defined the InstructionsF of b2 -valued Function
for s being State of S st p halts_on s holds
for b5 being State of S holds
( b5 = Result (p,s) iff ex k being Element of NAT st
( b5 = Comput (p,s,k) & CurInstr (p,b5) = halt S ) );

theorem :: EXTPRO_1:6
for k being Element of NAT
for N being non empty with_zero set
for S being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N
for P being Instruction-Sequence of S
for s being State of S holds Comput (P,s,(k + 1)) = Exec ((P . (IC (Comput (P,s,k)))),(Comput (P,s,k)))
proof
let k be Element of NAT ; ::_thesis: for N being non empty with_zero set
for S being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N
for P being Instruction-Sequence of S
for s being State of S holds Comput (P,s,(k + 1)) = Exec ((P . (IC (Comput (P,s,k)))),(Comput (P,s,k)))
let N be non empty with_zero set ; ::_thesis: for S being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N
for P being Instruction-Sequence of S
for s being State of S holds Comput (P,s,(k + 1)) = Exec ((P . (IC (Comput (P,s,k)))),(Comput (P,s,k)))
let S be non empty with_non-empty_values IC-Ins-separated AMI-Struct over N; ::_thesis: for P being Instruction-Sequence of S
for s being State of S holds Comput (P,s,(k + 1)) = Exec ((P . (IC (Comput (P,s,k)))),(Comput (P,s,k)))
let P be Instruction-Sequence of S; ::_thesis: for s being State of S holds Comput (P,s,(k + 1)) = Exec ((P . (IC (Comput (P,s,k)))),(Comput (P,s,k)))
let s be State of S; ::_thesis: Comput (P,s,(k + 1)) = Exec ((P . (IC (Comput (P,s,k)))),(Comput (P,s,k)))
A1: dom P = NAT by PARTFUN1:def_2;
thus  Comput (P,s,(k + 1)) = Following (P,(Comput (P,s,k))) by Th3
.= Exec ((P . (IC (Comput (P,s,k)))),(Comput (P,s,k))) by A1, PARTFUN1:def_6 ; ::_thesis: verum
end;

theorem Th7: :: EXTPRO_1:7
for N being non empty with_zero set
for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N
for P being Instruction-Sequence of S
for s being State of S
for k being Element of NAT st P . (IC (Comput (P,s,k))) = halt S holds
Result (P,s) = Comput (P,s,k)
proof
let N be non empty with_zero set ; ::_thesis: for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N
for P being Instruction-Sequence of S
for s being State of S
for k being Element of NAT st P . (IC (Comput (P,s,k))) = halt S holds
Result (P,s) = Comput (P,s,k)
let S be non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N; ::_thesis: for P being Instruction-Sequence of S
for s being State of S
for k being Element of NAT st P . (IC (Comput (P,s,k))) = halt S holds
Result (P,s) = Comput (P,s,k)
let P be Instruction-Sequence of S; ::_thesis: for s being State of S
for k being Element of NAT st P . (IC (Comput (P,s,k))) = halt S holds
Result (P,s) = Comput (P,s,k)
let s be State of S; ::_thesis: for k being Element of NAT st P . (IC (Comput (P,s,k))) = halt S holds
Result (P,s) = Comput (P,s,k)
let k be Element of NAT ; ::_thesis: ( P . (IC (Comput (P,s,k))) = halt S implies Result (P,s) = Comput (P,s,k) )
A1: dom P = NAT by PARTFUN1:def_2;
assume  P . (IC (Comput (P,s,k))) = halt S ; ::_thesis: Result (P,s) = Comput (P,s,k)
then A2: CurInstr (P,(Comput (P,s,k))) = halt S by A1, PARTFUN1:def_6;
then  P halts_on s by Def8, A1;
hence  Result (P,s) = Comput (P,s,k) by A2, Def9; ::_thesis: verum
end;

theorem Th8: :: EXTPRO_1:8
for N being non empty with_zero set
for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N
for P being Instruction-Sequence of S
for s being State of S st ex k being Element of NAT st P . (IC (Comput (P,s,k))) = halt S holds
for i being Element of NAT holds Result (P,s) = Result (P,(Comput (P,s,i)))
proof
let N be non empty with_zero set ; ::_thesis: for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N
for P being Instruction-Sequence of S
for s being State of S st ex k being Element of NAT st P . (IC (Comput (P,s,k))) = halt S holds
for i being Element of NAT holds Result (P,s) = Result (P,(Comput (P,s,i)))
let S be non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N; ::_thesis: for P being Instruction-Sequence of S
for s being State of S st ex k being Element of NAT st P . (IC (Comput (P,s,k))) = halt S holds
for i being Element of NAT holds Result (P,s) = Result (P,(Comput (P,s,i)))
let P be Instruction-Sequence of S; ::_thesis: for s being State of S st ex k being Element of NAT st P . (IC (Comput (P,s,k))) = halt S holds
for i being Element of NAT holds Result (P,s) = Result (P,(Comput (P,s,i)))
let s be State of S; ::_thesis: ( ex k being Element of NAT st P . (IC (Comput (P,s,k))) = halt S implies for i being Element of NAT holds Result (P,s) = Result (P,(Comput (P,s,i))) )
given k being Element of NAT  such that A1: P . (IC (Comput (P,s,k))) = halt S ; ::_thesis: for i being Element of NAT holds Result (P,s) = Result (P,(Comput (P,s,i)))
let i be Element of NAT ; ::_thesis: Result (P,s) = Result (P,(Comput (P,s,i)))
A2: dom P = NAT by PARTFUN1:def_2;
set s9 = Comput (P,s,k);
A3: CurInstr (P,(Comput (P,s,k))) = halt S by A1, A2, PARTFUN1:def_6;
now__::_thesis:_Result_(P,s)_=_Result_(P,(Comput_(P,s,i)))
percases ( i <= k or i >= k ) ;
suppose i <= k ; ::_thesis: Result (P,s) = Result (P,(Comput (P,s,i)))
then consider j being Nat such that
A4: k = i + j by NAT_1:10;
reconsider j = j as Element of NAT by ORDINAL1:def_12;
A5: Comput (P,s,k) = Comput (P,(Comput (P,s,i)),j) by A4, Th4;
A6: P halts_on Comput (P,s,i) by A3, A5, Def8, A2;
thus  Result (P,s) = Comput (P,s,k) by A1, Th7
.= Result (P,(Comput (P,s,i))) by A3, A5, A6, Def9 ; ::_thesis: verum
end;
supposeA7: i >= k ; ::_thesis: Result (P,s) = Result (P,(Comput (P,s,i)))
A8: Comput (P,(Comput (P,s,k)),0) = Comput (P,s,k) ;
A9: Comput (P,s,i) = Comput (P,s,k) by A3, A7, Th5;
A10: P halts_on Comput (P,s,i) by Def8, A2, A9, A3, A8;
thus  Result (P,s) = Comput (P,s,k) by A1, Th7
.= Result (P,(Comput (P,s,i))) by A3, A9, A8, A10, Def9 ; ::_thesis: verum
end;
end;
end;
hence  Result (P,s) = Result (P,(Comput (P,s,i))) ; ::_thesis: verum
end;

definition
let N be non empty with_zero set ;
let S be non empty with_non-empty_values IC-Ins-separated AMI-Struct over N;
let p be NAT -defined the InstructionsF of S -valued Function;
let IT be PartState of S;
attrIT is p -autonomic  means :Def10: :: EXTPRO_1:def 10
 for P, Q being Instruction-Sequence of S st p c= P & p c= Q holds
for s1, s2 being State of S st IT c= s1 & IT c= s2 holds
for i being Element of NAT holds (Comput (P,s1,i)) | (dom IT) = (Comput (Q,s2,i)) | (dom IT);
end;

:: deftheorem Def10 defines -autonomic EXTPRO_1:def_10_:_
 for N being non empty with_zero set
for S being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N
for p being NAT -defined the InstructionsF of b2 -valued Function
for IT being PartState of S holds
( IT is p -autonomic iff for P, Q being Instruction-Sequence of S st p c= P & p c= Q holds
for s1, s2 being State of S st IT c= s1 & IT c= s2 holds
for i being Element of NAT holds (Comput (P,s1,i)) | (dom IT) = (Comput (Q,s2,i)) | (dom IT) );

definition
let N be non empty with_zero set ;
let S be non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N;
let p be NAT -defined the InstructionsF of S -valued Function;
let IT be PartState of S;
attrIT is p -halted  means :Def11: :: EXTPRO_1:def 11
 for s being State of S st IT c= s holds
for P being Instruction-Sequence of S st p c= P holds
P halts_on s;
end;

:: deftheorem Def11 defines -halted EXTPRO_1:def_11_:_
 for N being non empty with_zero set
for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N
for p being NAT -defined the InstructionsF of b2 -valued Function
for IT being PartState of S holds
( IT is p -halted iff for s being State of S st IT c= s holds
for P being Instruction-Sequence of S st p c= P holds
P halts_on s );

registration
let N be non empty with_zero set ;
cluster non empty with_non-empty_values IC-Ins-separated strict halting for AMI-Struct over N;
existence
 ex b1 being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N st
( b1 is halting & b1 is strict )
proof
take  Trivial-AMI N ; ::_thesis: ( Trivial-AMI N is halting & Trivial-AMI N is strict )
thus  ( Trivial-AMI N is halting & Trivial-AMI N is strict ) ; ::_thesis: verum
end;
end;

begin

theorem Th9: :: EXTPRO_1:9
for N being non empty with_zero set
for S being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N
for l being Element of NAT
for I being Instruction of S
for P being NAT -defined the InstructionsF of b2 -valued Function st l .--> I c= P holds
for s being State of S st (IC ) .--> l c= s holds
CurInstr (P,s) = I
proof
let N be non empty with_zero set ; ::_thesis: for S being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N
for l being Element of NAT
for I being Instruction of S
for P being NAT -defined the InstructionsF of b1 -valued Function st l .--> I c= P holds
for s being State of S st (IC ) .--> l c= s holds
CurInstr (P,s) = I
let S be non empty with_non-empty_values IC-Ins-separated AMI-Struct over N; ::_thesis: for l being Element of NAT
for I being Instruction of S
for P being NAT -defined the InstructionsF of S -valued Function st l .--> I c= P holds
for s being State of S st (IC ) .--> l c= s holds
CurInstr (P,s) = I
let l be Element of NAT ; ::_thesis: for I being Instruction of S
for P being NAT -defined the InstructionsF of S -valued Function st l .--> I c= P holds
for s being State of S st (IC ) .--> l c= s holds
CurInstr (P,s) = I
let I be Instruction of S; ::_thesis: for P being NAT -defined the InstructionsF of S -valued Function st l .--> I c= P holds
for s being State of S st (IC ) .--> l c= s holds
CurInstr (P,s) = I
let P be NAT -defined the InstructionsF of S -valued Function; ::_thesis: ( l .--> I c= P implies for s being State of S st (IC ) .--> l c= s holds
CurInstr (P,s) = I )
assume A1: l .--> I c= P ; ::_thesis: for s being State of S st (IC ) .--> l c= s holds
CurInstr (P,s) = I
let s be State of S; ::_thesis: ( (IC ) .--> l c= s implies CurInstr (P,s) = I )
assume A2: (IC ) .--> l c= s ; ::_thesis: CurInstr (P,s) = I
 dom ((IC ) .--> l) = {(IC )} by FUNCOP_1:13;
then  IC in dom ((IC ) .--> l) by TARSKI:def_1;
then A3: IC s = ((IC ) .--> l) . (IC ) by A2, GRFUNC_1:2
.= l by FUNCOP_1:72 ;
 dom (l .--> I) = {l} by FUNCOP_1:13;
then A4: IC s in dom (l .--> I) by A3, TARSKI:def_1;
 dom (l .--> I) c= dom P by A1, RELAT_1:11;
hence  CurInstr (P,s) = P . (IC s) by A4, PARTFUN1:def_6
.= (l .--> I) . (IC s) by A4, A1, GRFUNC_1:2
.= I by A3, FUNCOP_1:72 ;
::_thesis: verum
end;

theorem Th10: :: EXTPRO_1:10
for N being non empty with_zero set
for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N
for l being Element of NAT
for P being NAT -defined the InstructionsF of b2 -valued Function st l .--> (halt S) c= P holds
for p being b3 -started PartState of S holds p is P -halted
proof
let N be non empty with_zero set ; ::_thesis: for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N
for l being Element of NAT
for P being NAT -defined the InstructionsF of b1 -valued Function st l .--> (halt S) c= P holds
for p being b2 -started PartState of S holds p is P -halted
let S be non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N; ::_thesis: for l being Element of NAT
for P being NAT -defined the InstructionsF of S -valued Function st l .--> (halt S) c= P holds
for p being b1 -started PartState of S holds p is P -halted
let l be Element of NAT ; ::_thesis: for P being NAT -defined the InstructionsF of S -valued Function st l .--> (halt S) c= P holds
for p being l -started PartState of S holds p is P -halted
let P be NAT -defined the InstructionsF of S -valued Function; ::_thesis: ( l .--> (halt S) c= P implies for p being l -started PartState of S holds p is P -halted )
assume A1: l .--> (halt S) c= P ; ::_thesis: for p being l -started PartState of S holds p is P -halted
let p be l -started PartState of S; ::_thesis: p is P -halted
set h = halt S;
set I = p +* P;
let s be State of S; :: according to EXTPRO_1:def_11 ::_thesis: ( p c= s implies for P being Instruction-Sequence of S st P c= P holds
P halts_on s )
assume A2: p c= s ; ::_thesis: for P being Instruction-Sequence of S st P c= P holds
P halts_on s
let Q be Instruction-Sequence of S; ::_thesis: ( P c= Q implies Q halts_on s )
assume A3: P c= Q ; ::_thesis: Q halts_on s
take  0 ; :: according to EXTPRO_1:def_8 ::_thesis: ( IC (Comput (Q,s,0)) in dom Q & CurInstr (Q,(Comput (Q,s,0))) = halt S )
 dom Q = NAT by PARTFUN1:def_2;
hence  IC (Comput (Q,s,0)) in dom Q ; ::_thesis: CurInstr (Q,(Comput (Q,s,0))) = halt S
 Start-At (l,S) c= p by MEMSTR_0:29;
then A4: Start-At (l,S) c= s by A2, XBOOLE_1:1;
A5: l .--> (halt S) c= Q by A1, A3, XBOOLE_1:1;
A6: dom (l .--> (halt S)) = {l} by FUNCOP_1:13;
 IC in dom (Start-At (l,S)) by MEMSTR_0:15;
then A7: IC s = IC (Start-At (l,S)) by A4, GRFUNC_1:2
.= l by FUNCOP_1:72 ;
A8: IC s in dom (l .--> (halt S)) by A6, A7, TARSKI:def_1;
A9: dom (l .--> (halt S)) c= dom Q by A5, RELAT_1:11;
thus  CurInstr (Q,(Comput (Q,s,0))) = CurInstr (Q,s)
.= Q . (IC s) by A9, A8, PARTFUN1:def_6
.= (l .--> (halt S)) . (IC s) by A8, A5, GRFUNC_1:2
.= CurInstr ((l .--> (halt S)),s) by A8, PARTFUN1:def_6
.= halt S by A4, Th9 ; ::_thesis: verum
end;

theorem Th11: :: EXTPRO_1:11
for N being non empty with_zero set
for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N
for l being Element of NAT
for P being NAT -defined the InstructionsF of b2 -valued Function st l .--> (halt S) c= P holds
for p being b3 -started PartState of S
for s being State of S st p c= s holds
for i being Element of NAT holds Comput (P,s,i) = s
proof
let N be non empty with_zero set ; ::_thesis: for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N
for l being Element of NAT
for P being NAT -defined the InstructionsF of b1 -valued Function st l .--> (halt S) c= P holds
for p being b2 -started PartState of S
for s being State of S st p c= s holds
for i being Element of NAT holds Comput (P,s,i) = s
let S be non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N; ::_thesis: for l being Element of NAT
for P being NAT -defined the InstructionsF of S -valued Function st l .--> (halt S) c= P holds
for p being b1 -started PartState of S
for s being State of S st p c= s holds
for i being Element of NAT holds Comput (P,s,i) = s
let l be Element of NAT ; ::_thesis: for P being NAT -defined the InstructionsF of S -valued Function st l .--> (halt S) c= P holds
for p being l -started PartState of S
for s being State of S st p c= s holds
for i being Element of NAT holds Comput (P,s,i) = s
let P be NAT -defined the InstructionsF of S -valued Function; ::_thesis: ( l .--> (halt S) c= P implies for p being l -started PartState of S
for s being State of S st p c= s holds
for i being Element of NAT holds Comput (P,s,i) = s )
assume A1: l .--> (halt S) c= P ; ::_thesis: for p being l -started PartState of S
for s being State of S st p c= s holds
for i being Element of NAT holds Comput (P,s,i) = s
let p be l -started PartState of S; ::_thesis: for s being State of S st p c= s holds
for i being Element of NAT holds Comput (P,s,i) = s
set h = halt S;
let s be State of S; ::_thesis: ( p c= s implies for i being Element of NAT holds Comput (P,s,i) = s )
assume A2: p c= s ; ::_thesis: for i being Element of NAT holds Comput (P,s,i) = s
A3: Start-At (l,S) c= p by MEMSTR_0:29;
defpred S1[ Element of NAT ] means  Comput (P,s,$1) = s;
A4: Start-At (l,S) c= s by A3, A2, XBOOLE_1:1;
A5: now__::_thesis:_for_i_being_Element_of_NAT_st_S1[i]_holds_
S1[i_+_1]
let i be Element of NAT ; ::_thesis: ( S1[i] implies S1[i + 1] )
assume A6: S1[i] ; ::_thesis: S1[i + 1]
Comput (P,s,(i + 1)) = Following (P,s) by A6, Th3
.= Exec ((halt S),s) by A4, A1, Th9
.= s by Def3 ;
hence  S1[i + 1] ; ::_thesis: verum
end;
A7: S1[ 0 ] ;
thus  for i being Element of NAT holds S1[i] from NAT_1:sch_1(A7, A5); ::_thesis: verum
end;

theorem Th12: :: EXTPRO_1:12
for N being non empty with_zero set
for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N
for l being Element of NAT
for P being NAT -defined the InstructionsF of b2 -valued Function st l .--> (halt S) c= P holds
for p being b3 -started PartState of S holds p is P -autonomic
proof
let N be non empty with_zero set ; ::_thesis: for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N
for l being Element of NAT
for P being NAT -defined the InstructionsF of b1 -valued Function st l .--> (halt S) c= P holds
for p being b2 -started PartState of S holds p is P -autonomic
let S be non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N; ::_thesis: for l being Element of NAT
for P being NAT -defined the InstructionsF of S -valued Function st l .--> (halt S) c= P holds
for p being b1 -started PartState of S holds p is P -autonomic
let l be Element of NAT ; ::_thesis: for P being NAT -defined the InstructionsF of S -valued Function st l .--> (halt S) c= P holds
for p being l -started PartState of S holds p is P -autonomic
set h = halt S;
set p = Start-At (l,S);
let P be NAT -defined the InstructionsF of S -valued Function; ::_thesis: ( l .--> (halt S) c= P implies for p being l -started PartState of S holds p is P -autonomic )
assume A1: l .--> (halt S) c= P ; ::_thesis: for p being l -started PartState of S holds p is P -autonomic
let p be l -started PartState of S; ::_thesis: p is P -autonomic
set I = p +* P;
let Q1, Q2 be Instruction-Sequence of S; :: according to EXTPRO_1:def_10 ::_thesis: ( P c= Q1 & P c= Q2 implies for s1, s2 being State of S st p c= s1 & p c= s2 holds
for i being Element of NAT holds (Comput (Q1,s1,i)) | (dom p) = (Comput (Q2,s2,i)) | (dom p) )
assume A2: ( P c= Q1 & P c= Q2 ) ; ::_thesis: for s1, s2 being State of S st p c= s1 & p c= s2 holds
for i being Element of NAT holds (Comput (Q1,s1,i)) | (dom p) = (Comput (Q2,s2,i)) | (dom p)
let s1, s2 be State of S; ::_thesis: ( p c= s1 & p c= s2 implies for i being Element of NAT holds (Comput (Q1,s1,i)) | (dom p) = (Comput (Q2,s2,i)) | (dom p) )
assume that
A3: p c= s1 and
A4: p c= s2 ; ::_thesis: for i being Element of NAT holds (Comput (Q1,s1,i)) | (dom p) = (Comput (Q2,s2,i)) | (dom p)
let i be Element of NAT ; ::_thesis: (Comput (Q1,s1,i)) | (dom p) = (Comput (Q2,s2,i)) | (dom p)
A5: ( l .--> (halt S) c= Q1 & l .--> (halt S) c= Q2 ) by A1, A2, XBOOLE_1:1;
hence (Comput (Q1,s1,i)) | (dom p) = s1 | (dom p) by A3, Th11
.= p by A3, GRFUNC_1:23
.= s2 | (dom p) by A4, GRFUNC_1:23
.= (Comput (Q2,s2,i)) | (dom p) by A4, Th11, A5 ;
::_thesis: verum
end;

registration
let N be non empty with_zero set ;
let S be non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N;
let P be NAT -defined the InstructionsF of S -valued non halt-free Function;
cluster non empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible finite countable V120() P -autonomic P -halted for set ;
existence
 ex b1 being FinPartState of S st
( b1 is P -autonomic & b1 is P -halted & not b1 is empty )
proof
 halt S in rng P by COMPOS_1:def_11;
then consider i being set  such that
A1: i in dom P and
A2: P . i = halt S by FUNCT_1:def_3;
 dom P c= NAT by RELAT_1:def_18;
then reconsider i = i as Element of NAT by A1;
take p = Start-At (i,S); ::_thesis: ( p is P -autonomic & p is P -halted & not p is empty )
 i .--> (halt S) c= P by A1, A2, FUNCT_4:85;
hence  ( p is P -autonomic & p is P -halted & not p is empty ) by Th10, Th12; ::_thesis: verum
end;
end;

definition
let N be non empty with_zero set ;
let S be non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N;
let P be NAT -defined the InstructionsF of S -valued non halt-free Function;
mode Autonomy of P ->  FinPartState of S means :Def12: :: EXTPRO_1:def 12
( it is P -autonomic & it is P -halted );
existence
 ex b1 being FinPartState of S st
( b1 is P -autonomic & b1 is P -halted )
proof
 halt S in rng P by COMPOS_1:def_11;
then consider x being set  such that
A1: x in dom P and
A2: P . x = halt S by FUNCT_1:def_3;
 dom P c= NAT by RELAT_1:def_18;
then reconsider m = x as Element of NAT by A1;
 [m,(halt S)] in P by A1, A2, FUNCT_1:def_2;
then  {[m,(halt S)]} c= P by ZFMISC_1:31;
then A3: m .--> (halt S) c= P by FUNCT_4:82;
take d = Start-At (m,S); ::_thesis: ( d is P -autonomic & d is P -halted )
thus  d is P -autonomic by A3, Th12; ::_thesis: d is P -halted
thus  d is P -halted by A3, Th10; ::_thesis: verum
end;
end;

:: deftheorem Def12 defines Autonomy EXTPRO_1:def_12_:_
 for N being non empty with_zero set
for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N
for P being NAT -defined the InstructionsF of b2 -valued non halt-free Function
for b4 being FinPartState of S holds
( b4 is Autonomy of P iff ( b4 is P -autonomic & b4 is P -halted ) );

definition
let N be non empty with_zero set ;
let S be non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N;
let p be NAT -defined the InstructionsF of S -valued non halt-free Function;
let d be FinPartState of S;
assume A1: d is Autonomy of p ;
func Result (p,d) ->  FinPartState of S means :: EXTPRO_1:def 13
 for P being Instruction-Sequence of S st p c= P holds
for s being State of S st d c= s holds
it = (Result (P,s)) | (dom d);
existence
 ex b1 being FinPartState of S st
for P being Instruction-Sequence of S st p c= P holds
for s being State of S st d c= s holds
b1 = (Result (P,s)) | (dom d)
proof
consider h being State of S such that
A2: d c= h by PBOOLE:141;
consider H being Instruction-Sequence of S such that
A3: p c= H by PBOOLE:145;
A4: ( d is p -halted & d is p -autonomic ) by A1, Def12;
then  H halts_on h by Def11, A3, A2;
then consider k1 being Element of NAT  such that
A5: Result (H,h) = Comput (H,h,k1) and
A6: CurInstr (H,(Result (H,h))) = halt S by Def9;
reconsider R = (Result (H,h)) | (dom d) as FinPartState of S ;
take  R ; ::_thesis: for P being Instruction-Sequence of S st p c= P holds
for s being State of S st d c= s holds
R = (Result (P,s)) | (dom d)
let P be Instruction-Sequence of S; ::_thesis: ( p c= P implies for s being State of S st d c= s holds
R = (Result (P,s)) | (dom d) )
assume A7: p c= P ; ::_thesis: for s being State of S st d c= s holds
R = (Result (P,s)) | (dom d)
let s be State of S; ::_thesis: ( d c= s implies R = (Result (P,s)) | (dom d) )
assume A8: d c= s ; ::_thesis: R = (Result (P,s)) | (dom d)
then  P halts_on s by Def11, A4, A7;
then consider k2 being Element of NAT  such that
A9: Result (P,s) = Comput (P,s,k2) and
A10: CurInstr (P,(Result (P,s))) = halt S by Def9;
percases ( k1 <= k2 or k1 >= k2 ) ;
suppose k1 <= k2 ; ::_thesis: R = (Result (P,s)) | (dom d)
then  Result (H,h) = Comput (H,h,k2) by A5, A6, Th5;
hence  R = (Result (P,s)) | (dom d) by A9, Def10, A4, A3, A7, A8, A2; ::_thesis: verum
end;
suppose k1 >= k2 ; ::_thesis: R = (Result (P,s)) | (dom d)
then  Result (P,s) = Comput (P,s,k1) by A9, A10, Th5;
hence  R = (Result (P,s)) | (dom d) by A5, Def10, A4, A3, A7, A8, A2; ::_thesis: verum
end;
end;
end;
correctness
uniqueness
for b1, b2 being FinPartState of S st ( for P being Instruction-Sequence of S st p c= P holds
for s being State of S st d c= s holds
b1 = (Result (P,s)) | (dom d) ) & ( for P being Instruction-Sequence of S st p c= P holds
for s being State of S st d c= s holds
b2 = (Result (P,s)) | (dom d) ) holds
b1 = b2;
proof
consider h being State of S such that
A11: d c= h by PBOOLE:141;
consider H being Instruction-Sequence of S such that
A12: p c= H by PBOOLE:145;
let p1, p2 be FinPartState of S; ::_thesis: ( ( for P being Instruction-Sequence of S st p c= P holds
for s being State of S st d c= s holds
p1 = (Result (P,s)) | (dom d) ) & ( for P being Instruction-Sequence of S st p c= P holds
for s being State of S st d c= s holds
p2 = (Result (P,s)) | (dom d) ) implies p1 = p2 )
assume that
A13: for P being Instruction-Sequence of S st p c= P holds
for s being State of S st d c= s holds
p1 = (Result (P,s)) | (dom d) and
A14: for P being Instruction-Sequence of S st p c= P holds
for s being State of S st d c= s holds
p2 = (Result (P,s)) | (dom d) ; ::_thesis: p1 = p2
thus p1 = (Result (H,h)) | (dom d) by A13, A11, A12
.= p2 by A14, A11, A12 ; ::_thesis: verum
end;
end;

:: deftheorem  defines Result EXTPRO_1:def_13_:_
 for N being non empty with_zero set
for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N
for p being NAT -defined the InstructionsF of b2 -valued non halt-free Function
for d being FinPartState of S st d is Autonomy of p holds
for b5 being FinPartState of S holds
( b5 = Result (p,d) iff for P being Instruction-Sequence of S st p c= P holds
for s being State of S st d c= s holds
b5 = (Result (P,s)) | (dom d) );

begin

definition
let N be non empty with_zero set ;
let S be non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N;
let p be NAT -defined the InstructionsF of S -valued non halt-free Function;
let d be FinPartState of S;
let F be Function;
predp,d computes F means :Def14: :: EXTPRO_1:def 14
 for x being set st x in dom F holds
ex s being FinPartState of S st
( x = s & d +* s is Autonomy of p & F . s c= Result (p,(d +* s)) );
end;

:: deftheorem Def14 defines computes EXTPRO_1:def_14_:_
 for N being non empty with_zero set
for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N
for p being NAT -defined the InstructionsF of b2 -valued non halt-free Function
for d being FinPartState of S
for F being Function holds
( p,d computes F iff for x being set st x in dom F holds
ex s being FinPartState of S st
( x = s & d +* s is Autonomy of p & F . s c= Result (p,(d +* s)) ) );

theorem :: EXTPRO_1:13
for N being non empty with_zero set
for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N
for p being NAT -defined the InstructionsF of b2 -valued non halt-free Function
for d being FinPartState of S holds p,d computes {}
proof
let N be non empty with_zero set ; ::_thesis: for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N
for p being NAT -defined the InstructionsF of b1 -valued non halt-free Function
for d being FinPartState of S holds p,d computes {}
let S be non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N; ::_thesis: for p being NAT -defined the InstructionsF of S -valued non halt-free Function
for d being FinPartState of S holds p,d computes {}
let p be NAT -defined the InstructionsF of S -valued non halt-free Function; ::_thesis: for d being FinPartState of S holds p,d computes {}
let d be FinPartState of S; ::_thesis: p,d computes {}
let x be set ; :: according to EXTPRO_1:def_14 ::_thesis: ( x in dom {} implies ex s being FinPartState of S st
( x = s & d +* s is Autonomy of p & {} . s c= Result (p,(d +* s)) ) )
assume A1: x in dom {} ; ::_thesis: ex s being FinPartState of S st
( x = s & d +* s is Autonomy of p & {} . s c= Result (p,(d +* s)) )
then reconsider x = x as FinPartState of S ;
take  x ; ::_thesis: ( x = x & d +* x is Autonomy of p & {} . x c= Result (p,(d +* x)) )
thus  ( x = x & d +* x is Autonomy of p & {} . x c= Result (p,(d +* x)) ) by A1; ::_thesis: verum
end;

theorem :: EXTPRO_1:14
for N being non empty with_zero set
for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N
for p being NAT -defined the InstructionsF of b2 -valued non halt-free Function
for d being FinPartState of S holds
( d is Autonomy of p iff p,d computes {} .--> (Result (p,d)) )
proof
let N be non empty with_zero set ; ::_thesis: for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N
for p being NAT -defined the InstructionsF of b1 -valued non halt-free Function
for d being FinPartState of S holds
( d is Autonomy of p iff p,d computes {} .--> (Result (p,d)) )
let S be non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N; ::_thesis: for p being NAT -defined the InstructionsF of S -valued non halt-free Function
for d being FinPartState of S holds
( d is Autonomy of p iff p,d computes {} .--> (Result (p,d)) )
let p be NAT -defined the InstructionsF of S -valued non halt-free Function; ::_thesis: for d being FinPartState of S holds
( d is Autonomy of p iff p,d computes {} .--> (Result (p,d)) )
let d be FinPartState of S; ::_thesis: ( d is Autonomy of p iff p,d computes {} .--> (Result (p,d)) )
thus  ( d is Autonomy of p implies p,d computes {} .--> (Result (p,d)) ) ::_thesis: ( p,d computes {} .--> (Result (p,d)) implies d is Autonomy of p )
proof
A1: dom ({} .--> (Result (p,d))) = {{}} by FUNCOP_1:13;
assume A2: d is Autonomy of p ; ::_thesis: p,d computes {} .--> (Result (p,d))
let x be set ; :: according to EXTPRO_1:def_14 ::_thesis: ( x in dom ({} .--> (Result (p,d))) implies ex s being FinPartState of S st
( x = s & d +* s is Autonomy of p & ({} .--> (Result (p,d))) . s c= Result (p,(d +* s)) ) )
assume A3: x in dom ({} .--> (Result (p,d))) ; ::_thesis: ex s being FinPartState of S st
( x = s & d +* s is Autonomy of p & ({} .--> (Result (p,d))) . s c= Result (p,(d +* s)) )
then A4: x = {} by A1, TARSKI:def_1;
then reconsider s = x as FinPartState of S by FUNCT_1:104, RELAT_1:171;
take  s ; ::_thesis: ( x = s & d +* s is Autonomy of p & ({} .--> (Result (p,d))) . s c= Result (p,(d +* s)) )
thus  x = s ; ::_thesis: ( d +* s is Autonomy of p & ({} .--> (Result (p,d))) . s c= Result (p,(d +* s)) )
A5: d +* {} = d ;
hence  d +* s is Autonomy of p by A2, A3, A1, TARSKI:def_1; ::_thesis: ({} .--> (Result (p,d))) . s c= Result (p,(d +* s))
 d +* s = d by A3, A1, TARSKI:def_1, A5;
hence  ({} .--> (Result (p,d))) . s c= Result (p,(d +* s)) by FUNCOP_1:72, A4; ::_thesis: verum
end;
 dom ({} .--> (Result (p,d))) = {{}} by FUNCOP_1:13;
then A6: {} in dom ({} .--> (Result (p,d))) by TARSKI:def_1;
A7: d +* {} = d ;
assume  p,d computes {} .--> (Result (p,d)) ; ::_thesis: d is Autonomy of p
then  ex s being FinPartState of S st
( {} = s & d +* s is Autonomy of p & ({} .--> (Result (p,d))) . s c= Result (p,(d +* s)) ) by A6, Def14;
hence  d is Autonomy of p by A7; ::_thesis: verum
end;

theorem :: EXTPRO_1:15
for N being non empty with_zero set
for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N
for p being NAT -defined the InstructionsF of b2 -valued non halt-free Function
for d being FinPartState of S holds
( d is Autonomy of p iff p,d computes {} .--> {} )
proof
let N be non empty with_zero set ; ::_thesis: for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N
for p being NAT -defined the InstructionsF of b1 -valued non halt-free Function
for d being FinPartState of S holds
( d is Autonomy of p iff p,d computes {} .--> {} )
let S be non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N; ::_thesis: for p being NAT -defined the InstructionsF of S -valued non halt-free Function
for d being FinPartState of S holds
( d is Autonomy of p iff p,d computes {} .--> {} )
let p be NAT -defined the InstructionsF of S -valued non halt-free Function; ::_thesis: for d being FinPartState of S holds
( d is Autonomy of p iff p,d computes {} .--> {} )
let d be FinPartState of S; ::_thesis: ( d is Autonomy of p iff p,d computes {} .--> {} )
thus  ( d is Autonomy of p implies p,d computes {} .--> {} ) ::_thesis: ( p,d computes {} .--> {} implies d is Autonomy of p )
proof
A1: dom ({} .--> {}) = {{}} by FUNCOP_1:13;
assume A2: d is Autonomy of p ; ::_thesis: p,d computes {} .--> {}
let x be set ; :: according to EXTPRO_1:def_14 ::_thesis: ( x in dom ({} .--> {}) implies ex s being FinPartState of S st
( x = s & d +* s is Autonomy of p & ({} .--> {}) . s c= Result (p,(d +* s)) ) )
assume A3: x in dom ({} .--> {}) ; ::_thesis: ex s being FinPartState of S st
( x = s & d +* s is Autonomy of p & ({} .--> {}) . s c= Result (p,(d +* s)) )
then A4: x = {} by A1, TARSKI:def_1;
then reconsider s = x as FinPartState of S by FUNCT_1:104, RELAT_1:171;
take  s ; ::_thesis: ( x = s & d +* s is Autonomy of p & ({} .--> {}) . s c= Result (p,(d +* s)) )
A5: d +* {} = d ;
thus  x = s ; ::_thesis: ( d +* s is Autonomy of p & ({} .--> {}) . s c= Result (p,(d +* s)) )
thus  d +* s is Autonomy of p by A2, A3, A5, A1, TARSKI:def_1; ::_thesis: ({} .--> {}) . s c= Result (p,(d +* s))
 ({} .--> {}) . s = {} by A4, FUNCOP_1:72;
hence  ({} .--> {}) . s c= Result (p,(d +* s)) by XBOOLE_1:2; ::_thesis: verum
end;
 dom ({} .--> {}) = {{}} by FUNCOP_1:13;
then A6: {} in dom ({} .--> {}) by TARSKI:def_1;
A7: d +* {} = d ;
assume  p,d computes {} .--> {} ; ::_thesis: d is Autonomy of p
then  ex s being FinPartState of S st
( {} = s & d +* s is Autonomy of p & ({} .--> {}) . s c= Result (p,(d +* s)) ) by A6, Def14;
hence  d is Autonomy of p by A7; ::_thesis: verum
end;

begin

registration
let N be non empty with_zero set ;
cluster non empty IC-Ins-separated for AMI-Struct over N;
existence
 ex b1 being non empty AMI-Struct over N st b1 is IC-Ins-separated
proof
take  Trivial-AMI N ; ::_thesis: Trivial-AMI N is IC-Ins-separated
thus  Trivial-AMI N is IC-Ins-separated ; ::_thesis: verum
end;
end;

begin

theorem Th16: :: EXTPRO_1:16
for N being non empty with_zero set
for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N
for p being NAT -defined the InstructionsF of b2 -valued Function
for s being State of S holds
( p halts_on s iff ex i being Element of NAT st p halts_at IC (Comput (p,s,i)) )
proof
let N be non empty with_zero set ; ::_thesis: for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N
for p being NAT -defined the InstructionsF of b1 -valued Function
for s being State of S holds
( p halts_on s iff ex i being Element of NAT st p halts_at IC (Comput (p,s,i)) )
let S be non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N; ::_thesis: for p being NAT -defined the InstructionsF of S -valued Function
for s being State of S holds
( p halts_on s iff ex i being Element of NAT st p halts_at IC (Comput (p,s,i)) )
let p be NAT -defined the InstructionsF of S -valued Function; ::_thesis: for s being State of S holds
( p halts_on s iff ex i being Element of NAT st p halts_at IC (Comput (p,s,i)) )
let s be State of S; ::_thesis: ( p halts_on s iff ex i being Element of NAT st p halts_at IC (Comput (p,s,i)) )
hereby  ::_thesis: ( ex i being Element of NAT st p halts_at IC (Comput (p,s,i)) implies p halts_on s )
assume  p halts_on s ; ::_thesis: ex i being Element of NAT st p halts_at IC (Comput (p,s,i))
then consider i being Nat such that
A1: IC (Comput (p,s,i)) in dom p and
A2: CurInstr (p,(Comput (p,s,i))) = halt S by Def8;
reconsider i = i as Element of NAT by ORDINAL1:def_12;
take i = i; ::_thesis: p halts_at IC (Comput (p,s,i))
 p . (IC (Comput (p,s,i))) = halt S by A1, A2, PARTFUN1:def_6;
hence  p halts_at IC (Comput (p,s,i)) by A1, COMPOS_1:def_12; ::_thesis: verum
end;
given i being Element of NAT  such that A3: p halts_at IC (Comput (p,s,i)) ; ::_thesis: p halts_on s
A4: IC (Comput (p,s,i)) in dom p by A3, COMPOS_1:def_12;
A5: p . (IC (Comput (p,s,i))) = halt S by A3, COMPOS_1:def_12;
take  i ; :: according to EXTPRO_1:def_8 ::_thesis: ( IC (Comput (p,s,i)) in dom p & CurInstr (p,(Comput (p,s,i))) = halt S )
thus  IC (Comput (p,s,i)) in dom p by A3, COMPOS_1:def_12; ::_thesis: CurInstr (p,(Comput (p,s,i))) = halt S
thus  CurInstr (p,(Comput (p,s,i))) = halt S by A4, A5, PARTFUN1:def_6; ::_thesis: verum
end;

theorem Th17: :: EXTPRO_1:17
for N being non empty with_zero set
for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N
for p being NAT -defined the InstructionsF of b2 -valued Function
for s being State of S
for k being Nat st p halts_on s holds
( Result (p,s) = Comput (p,s,k) iff p halts_at IC (Comput (p,s,k)) )
proof
let N be non empty with_zero set ; ::_thesis: for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N
for p being NAT -defined the InstructionsF of b1 -valued Function
for s being State of S
for k being Nat st p halts_on s holds
( Result (p,s) = Comput (p,s,k) iff p halts_at IC (Comput (p,s,k)) )
let S be non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N; ::_thesis: for p being NAT -defined the InstructionsF of S -valued Function
for s being State of S
for k being Nat st p halts_on s holds
( Result (p,s) = Comput (p,s,k) iff p halts_at IC (Comput (p,s,k)) )
let p be NAT -defined the InstructionsF of S -valued Function; ::_thesis: for s being State of S
for k being Nat st p halts_on s holds
( Result (p,s) = Comput (p,s,k) iff p halts_at IC (Comput (p,s,k)) )
let s be State of S; ::_thesis: for k being Nat st p halts_on s holds
( Result (p,s) = Comput (p,s,k) iff p halts_at IC (Comput (p,s,k)) )
let k be Nat; ::_thesis: ( p halts_on s implies ( Result (p,s) = Comput (p,s,k) iff p halts_at IC (Comput (p,s,k)) ) )
assume A1: p halts_on s ; ::_thesis: ( Result (p,s) = Comput (p,s,k) iff p halts_at IC (Comput (p,s,k)) )
then consider n being Nat such that
A2: IC (Comput (p,s,n)) in dom p and
A3: CurInstr (p,(Comput (p,s,n))) = halt S by Def8;
hereby  ::_thesis: ( p halts_at IC (Comput (p,s,k)) implies Result (p,s) = Comput (p,s,k) )
assume A4: Result (p,s) = Comput (p,s,k) ; ::_thesis: p halts_at IC (Comput (p,s,k))
consider i being Element of NAT  such that
A5: Result (p,s) = Comput (p,s,i) and
A6: CurInstr (p,(Result (p,s))) = halt S by A1, Def9;
reconsider i = i, n = n as Element of NAT by ORDINAL1:def_12;
A7: now__::_thesis:_Comput_(p,s,i)_=_Comput_(p,s,n)
percases ( i <= n or n <= i ) ;
suppose i <= n ; ::_thesis: Comput (p,s,i) = Comput (p,s,n)
hence  Comput (p,s,i) = Comput (p,s,n) by A5, A6, Th5; ::_thesis: verum
end;
suppose n <= i ; ::_thesis: Comput (p,s,i) = Comput (p,s,n)
hence  Comput (p,s,i) = Comput (p,s,n) by A3, Th5; ::_thesis: verum
end;
end;
end;
 p . (IC (Comput (p,s,k))) = halt S by A7, A6, A4, A2, A5, PARTFUN1:def_6;
hence  p halts_at IC (Comput (p,s,k)) by A7, A2, A5, A4, COMPOS_1:def_12; ::_thesis: verum
end;
assume that
A8: IC (Comput (p,s,k)) in dom p and
A9: p . (IC (Comput (p,s,k))) = halt S ; :: according to COMPOS_1:def_12 ::_thesis: Result (p,s) = Comput (p,s,k)
A10: CurInstr (p,(Comput (p,s,k))) = halt S by A8, A9, PARTFUN1:def_6;
reconsider k = k, n = n as Element of NAT by ORDINAL1:def_12;
now__::_thesis:_Comput_(p,s,k)_=_Comput_(p,s,n)
percases ( n <= k or k <= n ) ;
suppose n <= k ; ::_thesis: Comput (p,s,k) = Comput (p,s,n)
hence  Comput (p,s,k) = Comput (p,s,n) by A3, Th5; ::_thesis: verum
end;
suppose k <= n ; ::_thesis: Comput (p,s,k) = Comput (p,s,n)
hence  Comput (p,s,k) = Comput (p,s,n) by A10, Th5; ::_thesis: verum
end;
end;
end;
hence  Result (p,s) = Comput (p,s,k) by A3, Def9, A1; ::_thesis: verum
end;

theorem Th18: :: EXTPRO_1:18
for N being non empty with_zero set
for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N
for P being NAT -defined the InstructionsF of b2 -valued Function
for s being State of S
for k being Element of NAT st P halts_at IC (Comput (P,s,k)) holds
Result (P,s) = Comput (P,s,k)
proof
let N be non empty with_zero set ; ::_thesis: for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N
for P being NAT -defined the InstructionsF of b1 -valued Function
for s being State of S
for k being Element of NAT st P halts_at IC (Comput (P,s,k)) holds
Result (P,s) = Comput (P,s,k)
let S be non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N; ::_thesis: for P being NAT -defined the InstructionsF of S -valued Function
for s being State of S
for k being Element of NAT st P halts_at IC (Comput (P,s,k)) holds
Result (P,s) = Comput (P,s,k)
let P be NAT -defined the InstructionsF of S -valued Function; ::_thesis: for s being State of S
for k being Element of NAT st P halts_at IC (Comput (P,s,k)) holds
Result (P,s) = Comput (P,s,k)
let s be State of S; ::_thesis: for k being Element of NAT st P halts_at IC (Comput (P,s,k)) holds
Result (P,s) = Comput (P,s,k)
let k be Element of NAT ; ::_thesis: ( P halts_at IC (Comput (P,s,k)) implies Result (P,s) = Comput (P,s,k) )
assume A1: P halts_at IC (Comput (P,s,k)) ; ::_thesis: Result (P,s) = Comput (P,s,k)
then  P halts_on s by Th16;
hence  Result (P,s) = Comput (P,s,k) by A1, Th17; ::_thesis: verum
end;

theorem Th19: :: EXTPRO_1:19
for i, j being Element of NAT
for N being non empty with_zero set st i <= j holds
for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N
for P being NAT -defined the InstructionsF of b4 -valued Function
for s being State of S st P halts_at IC (Comput (P,s,i)) holds
P halts_at IC (Comput (P,s,j))
proof
let i, j be Element of NAT ; ::_thesis: for N being non empty with_zero set st i <= j holds
for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N
for P being NAT -defined the InstructionsF of b2 -valued Function
for s being State of S st P halts_at IC (Comput (P,s,i)) holds
P halts_at IC (Comput (P,s,j))
let N be non empty with_zero set ; ::_thesis: ( i <= j implies for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N
for P being NAT -defined the InstructionsF of b1 -valued Function
for s being State of S st P halts_at IC (Comput (P,s,i)) holds
P halts_at IC (Comput (P,s,j)) )
assume A1: i <= j ; ::_thesis: for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N
for P being NAT -defined the InstructionsF of b1 -valued Function
for s being State of S st P halts_at IC (Comput (P,s,i)) holds
P halts_at IC (Comput (P,s,j))
let S be non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N; ::_thesis: for P being NAT -defined the InstructionsF of S -valued Function
for s being State of S st P halts_at IC (Comput (P,s,i)) holds
P halts_at IC (Comput (P,s,j))
let p be NAT -defined the InstructionsF of S -valued Function; ::_thesis: for s being State of S st p halts_at IC (Comput (p,s,i)) holds
p halts_at IC (Comput (p,s,j))
let s be State of S; ::_thesis: ( p halts_at IC (Comput (p,s,i)) implies p halts_at IC (Comput (p,s,j)) )
assume that
A2: IC (Comput (p,s,i)) in dom p and
A3: p . (IC (Comput (p,s,i))) = halt S ; :: according to COMPOS_1:def_12 ::_thesis: p halts_at IC (Comput (p,s,j))
A4: CurInstr (p,(Comput (p,s,i))) = halt S by A2, A3, PARTFUN1:def_6;
hence  IC (Comput (p,s,j)) in dom p by A2, A1, Th5; :: according to COMPOS_1:def_12 ::_thesis: p . (IC (Comput (p,s,j))) = halt S
thus  p . (IC (Comput (p,s,j))) = halt S by A1, A3, A4, Th5; ::_thesis: verum
end;

theorem :: EXTPRO_1:20
for i, j being Element of NAT
for N being non empty with_zero set st i <= j holds
for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N
for P being NAT -defined the InstructionsF of b4 -valued Function
for s being State of S st P halts_at IC (Comput (P,s,i)) holds
Comput (P,s,j) = Comput (P,s,i)
proof
let i, j be Element of NAT ; ::_thesis: for N being non empty with_zero set st i <= j holds
for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N
for P being NAT -defined the InstructionsF of b2 -valued Function
for s being State of S st P halts_at IC (Comput (P,s,i)) holds
Comput (P,s,j) = Comput (P,s,i)
let N be non empty with_zero set ; ::_thesis: ( i <= j implies for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N
for P being NAT -defined the InstructionsF of b1 -valued Function
for s being State of S st P halts_at IC (Comput (P,s,i)) holds
Comput (P,s,j) = Comput (P,s,i) )
assume A1: i <= j ; ::_thesis: for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N
for P being NAT -defined the InstructionsF of b1 -valued Function
for s being State of S st P halts_at IC (Comput (P,s,i)) holds
Comput (P,s,j) = Comput (P,s,i)
let S be non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N; ::_thesis: for P being NAT -defined the InstructionsF of S -valued Function
for s being State of S st P halts_at IC (Comput (P,s,i)) holds
Comput (P,s,j) = Comput (P,s,i)
let P be NAT -defined the InstructionsF of S -valued Function; ::_thesis: for s being State of S st P halts_at IC (Comput (P,s,i)) holds
Comput (P,s,j) = Comput (P,s,i)
let s be State of S; ::_thesis: ( P halts_at IC (Comput (P,s,i)) implies Comput (P,s,j) = Comput (P,s,i) )
assume A2: P halts_at IC (Comput (P,s,i)) ; ::_thesis: Comput (P,s,j) = Comput (P,s,i)
then  P halts_at IC (Comput (P,s,j)) by A1, Th19;
hence  Comput (P,s,j) = Result (P,s) by Th18
.= Comput (P,s,i) by A2, Th18 ;
::_thesis: verum
end;

theorem :: EXTPRO_1:21
for N being non empty with_zero set
for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N
for P being Instruction-Sequence of S
for s being State of S st ex k being Element of NAT st P halts_at IC (Comput (P,s,k)) holds
for i being Element of NAT holds Result (P,s) = Result (P,(Comput (P,s,i)))
proof
let N be non empty with_zero set ; ::_thesis: for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N
for P being Instruction-Sequence of S
for s being State of S st ex k being Element of NAT st P halts_at IC (Comput (P,s,k)) holds
for i being Element of NAT holds Result (P,s) = Result (P,(Comput (P,s,i)))
let S be non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N; ::_thesis: for P being Instruction-Sequence of S
for s being State of S st ex k being Element of NAT st P halts_at IC (Comput (P,s,k)) holds
for i being Element of NAT holds Result (P,s) = Result (P,(Comput (P,s,i)))
let P be Instruction-Sequence of S; ::_thesis: for s being State of S st ex k being Element of NAT st P halts_at IC (Comput (P,s,k)) holds
for i being Element of NAT holds Result (P,s) = Result (P,(Comput (P,s,i)))
let s be State of S; ::_thesis: ( ex k being Element of NAT st P halts_at IC (Comput (P,s,k)) implies for i being Element of NAT holds Result (P,s) = Result (P,(Comput (P,s,i))) )
given k being Element of NAT  such that A1: P halts_at IC (Comput (P,s,k)) ; ::_thesis: for i being Element of NAT holds Result (P,s) = Result (P,(Comput (P,s,i)))
let i be Element of NAT ; ::_thesis: Result (P,s) = Result (P,(Comput (P,s,i)))
 P . (IC (Comput (P,s,k))) = halt S by A1, COMPOS_1:def_12;
hence  Result (P,s) = Result (P,(Comput (P,s,i))) by Th8; ::_thesis: verum
end;

definition
let N be non empty with_zero set ;
let S be non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N;
let p be NAT -defined the InstructionsF of S -valued Function;
let s be State of S;
assume X1: p halts_on s ;
func LifeSpan (p,s) ->  Element of NAT  means :Def15: :: EXTPRO_1:def 15
( CurInstr (p,(Comput (p,s,it))) = halt S & ( for k being Element of NAT st CurInstr (p,(Comput (p,s,k))) = halt S holds
it <= k ) );
existence
 ex b1 being Element of NAT st
( CurInstr (p,(Comput (p,s,b1))) = halt S & ( for k being Element of NAT st CurInstr (p,(Comput (p,s,k))) = halt S holds
b1 <= k ) )
proof
defpred S1[ Nat] means  CurInstr (p,(Comput (p,s,$1))) = halt S;
consider k being Nat such that
 IC (Comput (p,s,k)) in dom p and
A1: CurInstr (p,(Comput (p,s,k))) = halt S by X1, Def8;
A2: ex k being Nat st S1[k] by A1;
consider k being Nat such that
A3: ( S1[k] & ( for n being Nat st S1[n] holds
k <= n ) ) from NAT_1:sch_5(A2);
reconsider k = k as Element of NAT by ORDINAL1:def_12;
take  k ; ::_thesis: ( CurInstr (p,(Comput (p,s,k))) = halt S & ( for k being Element of NAT st CurInstr (p,(Comput (p,s,k))) = halt S holds
k <= k ) )
thus  ( CurInstr (p,(Comput (p,s,k))) = halt S & ( for k being Element of NAT st CurInstr (p,(Comput (p,s,k))) = halt S holds
k <= k ) ) by A3; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Element of NAT st CurInstr (p,(Comput (p,s,b1))) = halt S & ( for k being Element of NAT st CurInstr (p,(Comput (p,s,k))) = halt S holds
b1 <= k ) & CurInstr (p,(Comput (p,s,b2))) = halt S & ( for k being Element of NAT st CurInstr (p,(Comput (p,s,k))) = halt S holds
b2 <= k ) holds
b1 = b2
proof
let it1, it2 be Element of NAT ; ::_thesis: ( CurInstr (p,(Comput (p,s,it1))) = halt S & ( for k being Element of NAT st CurInstr (p,(Comput (p,s,k))) = halt S holds
it1 <= k ) & CurInstr (p,(Comput (p,s,it2))) = halt S & ( for k being Element of NAT st CurInstr (p,(Comput (p,s,k))) = halt S holds
it2 <= k ) implies it1 = it2 )
assume A4: ( CurInstr (p,(Comput (p,s,it1))) = halt S & ( for k being Element of NAT st CurInstr (p,(Comput (p,s,k))) = halt S holds
it1 <= k ) & CurInstr (p,(Comput (p,s,it2))) = halt S & ( for k being Element of NAT st CurInstr (p,(Comput (p,s,k))) = halt S holds
it2 <= k ) & not it1 = it2 ) ; ::_thesis: contradiction
then  ( it1 <= it2 & it2 <= it1 ) ;
hence  contradiction by A4, XXREAL_0:1; ::_thesis: verum
end;
end;

:: deftheorem Def15 defines LifeSpan EXTPRO_1:def_15_:_
 for N being non empty with_zero set
for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N
for p being NAT -defined the InstructionsF of b2 -valued Function
for s being State of S st p halts_on s holds
for b5 being Element of NAT holds
( b5 = LifeSpan (p,s) iff ( CurInstr (p,(Comput (p,s,b5))) = halt S & ( for k being Element of NAT st CurInstr (p,(Comput (p,s,k))) = halt S holds
b5 <= k ) ) );

theorem Th22: :: EXTPRO_1:22
for N being non empty with_zero set
for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N
for p being NAT -defined the InstructionsF of b2 -valued Function
for s being State of S
for m being Element of NAT holds
( p halts_on s iff p halts_on Comput (p,s,m) )
proof
let N be non empty with_zero set ; ::_thesis: for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N
for p being NAT -defined the InstructionsF of b1 -valued Function
for s being State of S
for m being Element of NAT holds
( p halts_on s iff p halts_on Comput (p,s,m) )
let S be non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N; ::_thesis: for p being NAT -defined the InstructionsF of S -valued Function
for s being State of S
for m being Element of NAT holds
( p halts_on s iff p halts_on Comput (p,s,m) )
let p be NAT -defined the InstructionsF of S -valued Function; ::_thesis: for s being State of S
for m being Element of NAT holds
( p halts_on s iff p halts_on Comput (p,s,m) )
let s be State of S; ::_thesis: for m being Element of NAT holds
( p halts_on s iff p halts_on Comput (p,s,m) )
let m be Element of NAT ; ::_thesis: ( p halts_on s iff p halts_on Comput (p,s,m) )
hereby  ::_thesis: ( p halts_on Comput (p,s,m) implies p halts_on s )
assume  p halts_on s ; ::_thesis: p halts_on Comput (p,s,m)
then consider n being Nat such that
A1: IC (Comput (p,s,n)) in dom p and
A2: CurInstr (p,(Comput (p,s,n))) = halt S by Def8;
reconsider n = n as Element of NAT by ORDINAL1:def_12;
percases ( n <= m or n >= m ) ;
suppose n <= m ; ::_thesis: p halts_on Comput (p,s,m)
then  Comput (p,s,n) = Comput (p,s,(m + 0)) by A2, Th5
.= Comput (p,(Comput (p,s,m)),0) ;
hence  p halts_on Comput (p,s,m) by Def8, A2, A1; ::_thesis: verum
end;
suppose n >= m ; ::_thesis: p halts_on Comput (p,s,m)
then reconsider k = n - m as Element of NAT by INT_1:5;
Comput (p,(Comput (p,s,m)),k) = Comput (p,s,(m + k)) by Th4
.= Comput (p,s,n) ;
hence  p halts_on Comput (p,s,m) by Def8, A1, A2; ::_thesis: verum
end;
end;
end;
given n being Nat such that A3: IC (Comput (p,(Comput (p,s,m)),n)) in dom p and
A4: CurInstr (p,(Comput (p,(Comput (p,s,m)),n))) = halt S ; :: according to EXTPRO_1:def_8 ::_thesis: p halts_on s
reconsider nn = n as Element of NAT by ORDINAL1:def_12;
take  m + nn ; :: according to EXTPRO_1:def_8 ::_thesis: ( IC (Comput (p,s,(m + nn))) in dom p & CurInstr (p,(Comput (p,s,(m + nn)))) = halt S )
thus  ( IC (Comput (p,s,(m + nn))) in dom p & CurInstr (p,(Comput (p,s,(m + nn)))) = halt S ) by A3, A4, Th4; ::_thesis: verum
end;


theorem :: EXTPRO_1:23
for N being non empty with_zero set
for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N
for p being NAT -defined the InstructionsF of b2 -valued Function
for s being State of S st p halts_on s holds
Result (p,s) = Comput (p,s,(LifeSpan (p,s)))
proof
let N be non empty with_zero set ; ::_thesis: for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N
for p being NAT -defined the InstructionsF of b1 -valued Function
for s being State of S st p halts_on s holds
Result (p,s) = Comput (p,s,(LifeSpan (p,s)))
let S be non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N; ::_thesis: for p being NAT -defined the InstructionsF of S -valued Function
for s being State of S st p halts_on s holds
Result (p,s) = Comput (p,s,(LifeSpan (p,s)))
let p be NAT -defined the InstructionsF of S -valued Function; ::_thesis: for s being State of S st p halts_on s holds
Result (p,s) = Comput (p,s,(LifeSpan (p,s)))
let s be State of S; ::_thesis: ( p halts_on s implies Result (p,s) = Comput (p,s,(LifeSpan (p,s))) )
assume A1: p halts_on s ; ::_thesis: Result (p,s) = Comput (p,s,(LifeSpan (p,s)))
then A2: CurInstr (p,(Comput (p,s,(LifeSpan (p,s))))) = halt S by Def15;
consider m being Element of NAT  such that
A3: Result (p,s) = Comput (p,s,m) and
A4: CurInstr (p,(Result (p,s))) = halt S by A1, Def9;
 LifeSpan (p,s) <= m by A1, A3, A4, Def15;
hence  Result (p,s) = Comput (p,s,(LifeSpan (p,s))) by A2, A3, Th5; ::_thesis: verum
end;

theorem :: EXTPRO_1:24
for N being non empty with_zero set
for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N
for P being Instruction-Sequence of S
for s being State of S
for k being Element of NAT st CurInstr (P,(Comput (P,s,k))) = halt S holds
Comput (P,s,(LifeSpan (P,s))) = Comput (P,s,k)
proof
let N be non empty with_zero set ; ::_thesis: for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N
for P being Instruction-Sequence of S
for s being State of S
for k being Element of NAT st CurInstr (P,(Comput (P,s,k))) = halt S holds
Comput (P,s,(LifeSpan (P,s))) = Comput (P,s,k)
let S be non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N; ::_thesis: for P being Instruction-Sequence of S
for s being State of S
for k being Element of NAT st CurInstr (P,(Comput (P,s,k))) = halt S holds
Comput (P,s,(LifeSpan (P,s))) = Comput (P,s,k)
let P be Instruction-Sequence of S; ::_thesis: for s being State of S
for k being Element of NAT st CurInstr (P,(Comput (P,s,k))) = halt S holds
Comput (P,s,(LifeSpan (P,s))) = Comput (P,s,k)
let s be State of S; ::_thesis: for k being Element of NAT st CurInstr (P,(Comput (P,s,k))) = halt S holds
Comput (P,s,(LifeSpan (P,s))) = Comput (P,s,k)
let k be Element of NAT ; ::_thesis: ( CurInstr (P,(Comput (P,s,k))) = halt S implies Comput (P,s,(LifeSpan (P,s))) = Comput (P,s,k) )
assume A1: CurInstr (P,(Comput (P,s,k))) = halt S ; ::_thesis: Comput (P,s,(LifeSpan (P,s))) = Comput (P,s,k)
A2: dom P = NAT by PARTFUN1:def_2;
A3: P halts_on s by Def8, A2, A1;
set Ls = LifeSpan (P,s);
A4: CurInstr (P,(Comput (P,s,(LifeSpan (P,s))))) = halt S by A3, Def15;
 LifeSpan (P,s) <= k by A1, A3, Def15;
hence  Comput (P,s,(LifeSpan (P,s))) = Comput (P,s,k) by A4, Th5; ::_thesis: verum
end;

theorem :: EXTPRO_1:25
for j being Element of NAT
for N being non empty with_zero set
for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N
for p being NAT -defined the InstructionsF of b3 -valued Function
for s being State of S st LifeSpan (p,s) <= j & p halts_on s holds
Comput (p,s,j) = Comput (p,s,(LifeSpan (p,s)))
proof
let j be Element of NAT ; ::_thesis: for N being non empty with_zero set
for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N
for p being NAT -defined the InstructionsF of b2 -valued Function
for s being State of S st LifeSpan (p,s) <= j & p halts_on s holds
Comput (p,s,j) = Comput (p,s,(LifeSpan (p,s)))
let N be non empty with_zero set ; ::_thesis: for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N
for p being NAT -defined the InstructionsF of b1 -valued Function
for s being State of S st LifeSpan (p,s) <= j & p halts_on s holds
Comput (p,s,j) = Comput (p,s,(LifeSpan (p,s)))
let S be non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N; ::_thesis: for p being NAT -defined the InstructionsF of S -valued Function
for s being State of S st LifeSpan (p,s) <= j & p halts_on s holds
Comput (p,s,j) = Comput (p,s,(LifeSpan (p,s)))
let p be NAT -defined the InstructionsF of S -valued Function; ::_thesis: for s being State of S st LifeSpan (p,s) <= j & p halts_on s holds
Comput (p,s,j) = Comput (p,s,(LifeSpan (p,s)))
let s be State of S; ::_thesis: ( LifeSpan (p,s) <= j & p halts_on s implies Comput (p,s,j) = Comput (p,s,(LifeSpan (p,s))) )
assume that
A1: LifeSpan (p,s) <= j and
A2: p halts_on s ; ::_thesis: Comput (p,s,j) = Comput (p,s,(LifeSpan (p,s)))
 CurInstr (p,(Comput (p,s,(LifeSpan (p,s))))) = halt S by A2, Def15;
hence  Comput (p,s,j) = Comput (p,s,(LifeSpan (p,s))) by A1, Th5; ::_thesis: verum
end;

theorem :: EXTPRO_1:26
for N being non empty with_zero set
for S being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N
for e being Nat
for I being Instruction of S
for t being b3 -started State of S
for u being Instruction-Sequence of S st e .--> I c= u holds
Following (u,t) = Exec (I,t)
proof
let N be non empty with_zero set ; ::_thesis: for S being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N
for e being Nat
for I being Instruction of S
for t being b2 -started State of S
for u being Instruction-Sequence of S st e .--> I c= u holds
Following (u,t) = Exec (I,t)
let S be non empty with_non-empty_values IC-Ins-separated AMI-Struct over N; ::_thesis: for e being Nat
for I being Instruction of S
for t being b1 -started State of S
for u being Instruction-Sequence of S st e .--> I c= u holds
Following (u,t) = Exec (I,t)
let e be Nat; ::_thesis: for I being Instruction of S
for t being e -started State of S
for u being Instruction-Sequence of S st e .--> I c= u holds
Following (u,t) = Exec (I,t)
let I be Instruction of S; ::_thesis: for t being e -started State of S
for u being Instruction-Sequence of S st e .--> I c= u holds
Following (u,t) = Exec (I,t)
let t be e -started State of S; ::_thesis: for u being Instruction-Sequence of S st e .--> I c= u holds
Following (u,t) = Exec (I,t)
let u be Instruction-Sequence of S; ::_thesis: ( e .--> I c= u implies Following (u,t) = Exec (I,t) )
assume A1: e .--> I c= u ; ::_thesis: Following (u,t) = Exec (I,t)
 dom (e .--> I) = {e} by FUNCOP_1:13;
then A2: e in dom (e .--> I) by TARSKI:def_1;
 IC t = e by MEMSTR_0:def_11;
then  CurInstr (u,t) = u . e by PBOOLE:143
.= (e .--> I) . e by A1, A2, GRFUNC_1:2
.= I by FUNCOP_1:72 ;
hence  Following (u,t) = Exec (I,t) ; ::_thesis: verum
end;

theorem :: EXTPRO_1:27
for N being non empty with_zero set
for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N
for P being Instruction-Sequence of S
for s being State of S st s = Following (P,s) holds
for n being Element of NAT holds Comput (P,s,n) = s
proof
let N be non empty with_zero set ; ::_thesis: for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N
for P being Instruction-Sequence of S
for s being State of S st s = Following (P,s) holds
for n being Element of NAT holds Comput (P,s,n) = s
let S be non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N; ::_thesis: for P being Instruction-Sequence of S
for s being State of S st s = Following (P,s) holds
for n being Element of NAT holds Comput (P,s,n) = s
let P be Instruction-Sequence of S; ::_thesis: for s being State of S st s = Following (P,s) holds
for n being Element of NAT holds Comput (P,s,n) = s
let s be State of S; ::_thesis: ( s = Following (P,s) implies for n being Element of NAT holds Comput (P,s,n) = s )
defpred S1[ Element of NAT ] means  Comput (P,s,$1) = s;
assume  s = Following (P,s) ; ::_thesis: for n being Element of NAT holds Comput (P,s,n) = s
then A1: for n being Element of NAT st S1[n] holds
S1[n + 1] by Th3;
A2: S1[ 0 ] ;
thus  for n being Element of NAT holds S1[n] from NAT_1:sch_1(A2, A1); ::_thesis: verum
end;

theorem :: EXTPRO_1:28
for N being non empty with_zero set
for S being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N
for P being Instruction-Sequence of S
for s being State of S
for i being Instruction of S holds (Exec ((P . (IC s)),s)) . (IC ) = IC (Following (P,s))
proof
let N be non empty with_zero set ; ::_thesis: for S being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N
for P being Instruction-Sequence of S
for s being State of S
for i being Instruction of S holds (Exec ((P . (IC s)),s)) . (IC ) = IC (Following (P,s))
let S be non empty with_non-empty_values IC-Ins-separated AMI-Struct over N; ::_thesis: for P being Instruction-Sequence of S
for s being State of S
for i being Instruction of S holds (Exec ((P . (IC s)),s)) . (IC ) = IC (Following (P,s))
let P be Instruction-Sequence of S; ::_thesis: for s being State of S
for i being Instruction of S holds (Exec ((P . (IC s)),s)) . (IC ) = IC (Following (P,s))
let s be State of S; ::_thesis: for i being Instruction of S holds (Exec ((P . (IC s)),s)) . (IC ) = IC (Following (P,s))
let i be Instruction of S; ::_thesis: (Exec ((P . (IC s)),s)) . (IC ) = IC (Following (P,s))
 NAT = dom P by PARTFUN1:def_2;
hence  (Exec ((P . (IC s)),s)) . (IC ) = IC (Following (P,s)) by PARTFUN1:def_6; ::_thesis: verum
end;

theorem :: EXTPRO_1:29
for N being non empty with_zero set
for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N
for P being Instruction-Sequence of S
for s being State of S holds
( P halts_on s iff ex k being Element of NAT st CurInstr (P,(Comput (P,s,k))) = halt S )
proof
let N be non empty with_zero set ; ::_thesis: for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N
for P being Instruction-Sequence of S
for s being State of S holds
( P halts_on s iff ex k being Element of NAT st CurInstr (P,(Comput (P,s,k))) = halt S )
let S be non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N; ::_thesis: for P being Instruction-Sequence of S
for s being State of S holds
( P halts_on s iff ex k being Element of NAT st CurInstr (P,(Comput (P,s,k))) = halt S )
let P be Instruction-Sequence of S; ::_thesis: for s being State of S holds
( P halts_on s iff ex k being Element of NAT st CurInstr (P,(Comput (P,s,k))) = halt S )
let s be State of S; ::_thesis: ( P halts_on s iff ex k being Element of NAT st CurInstr (P,(Comput (P,s,k))) = halt S )
thus  ( P halts_on s implies ex k being Element of NAT st CurInstr (P,(Comput (P,s,k))) = halt S ) ::_thesis: ( ex k being Element of NAT st CurInstr (P,(Comput (P,s,k))) = halt S implies P halts_on s )
proof
given k being Nat such that  IC (Comput (P,s,k)) in dom P and
A1: CurInstr (P,(Comput (P,s,k))) = halt S ; :: according to EXTPRO_1:def_8 ::_thesis: ex k being Element of NAT st CurInstr (P,(Comput (P,s,k))) = halt S
reconsider k = k as Element of NAT by ORDINAL1:def_12;
take  k ; ::_thesis: CurInstr (P,(Comput (P,s,k))) = halt S
thus  CurInstr (P,(Comput (P,s,k))) = halt S by A1; ::_thesis: verum
end;
given k being Element of NAT  such that A2: CurInstr (P,(Comput (P,s,k))) = halt S ; ::_thesis: P halts_on s
take  k ; :: according to EXTPRO_1:def_8 ::_thesis: ( IC (Comput (P,s,k)) in dom P & CurInstr (P,(Comput (P,s,k))) = halt S )
 IC (Comput (P,s,k)) in NAT ;
hence  IC (Comput (P,s,k)) in dom P by PARTFUN1:def_2; ::_thesis: CurInstr (P,(Comput (P,s,k))) = halt S
thus  CurInstr (P,(Comput (P,s,k))) = halt S by A2; ::_thesis: verum
end;

theorem Th30: :: EXTPRO_1:30
for N being non empty with_zero set
for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N
for F being Instruction-Sequence of S
for s being State of S st ex k being Element of NAT st F . (IC (Comput (F,s,k))) = halt S holds
F halts_on s
proof
let N be non empty with_zero set ; ::_thesis: for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N
for F being Instruction-Sequence of S
for s being State of S st ex k being Element of NAT st F . (IC (Comput (F,s,k))) = halt S holds
F halts_on s
let S be non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N; ::_thesis: for F being Instruction-Sequence of S
for s being State of S st ex k being Element of NAT st F . (IC (Comput (F,s,k))) = halt S holds
F halts_on s
let F be Instruction-Sequence of S; ::_thesis: for s being State of S st ex k being Element of NAT st F . (IC (Comput (F,s,k))) = halt S holds
F halts_on s
let s be State of S; ::_thesis: ( ex k being Element of NAT st F . (IC (Comput (F,s,k))) = halt S implies F halts_on s )
given k being Element of NAT  such that A1: F . (IC (Comput (F,s,k))) = halt S ; ::_thesis: F halts_on s
take  k ; :: according to EXTPRO_1:def_8 ::_thesis: ( IC (Comput (F,s,k)) in dom F & CurInstr (F,(Comput (F,s,k))) = halt S )
A2: dom F = NAT by PARTFUN1:def_2;
hence  IC (Comput (F,s,k)) in dom F ; ::_thesis: CurInstr (F,(Comput (F,s,k))) = halt S
thus  CurInstr (F,(Comput (F,s,k))) = halt S by A1, A2, PARTFUN1:def_6; ::_thesis: verum
end;

theorem :: EXTPRO_1:31
for N being non empty with_zero set
for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N
for F being Instruction-Sequence of S
for s being State of S
for k being Element of NAT st F . (IC (Comput (F,s,k))) = halt S holds
Result (F,s) = Comput (F,s,k)
proof
let N be non empty with_zero set ; ::_thesis: for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N
for F being Instruction-Sequence of S
for s being State of S
for k being Element of NAT st F . (IC (Comput (F,s,k))) = halt S holds
Result (F,s) = Comput (F,s,k)
let S be non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N; ::_thesis: for F being Instruction-Sequence of S
for s being State of S
for k being Element of NAT st F . (IC (Comput (F,s,k))) = halt S holds
Result (F,s) = Comput (F,s,k)
let F be Instruction-Sequence of S; ::_thesis: for s being State of S
for k being Element of NAT st F . (IC (Comput (F,s,k))) = halt S holds
Result (F,s) = Comput (F,s,k)
let s be State of S; ::_thesis: for k being Element of NAT st F . (IC (Comput (F,s,k))) = halt S holds
Result (F,s) = Comput (F,s,k)
let k be Element of NAT ; ::_thesis: ( F . (IC (Comput (F,s,k))) = halt S implies Result (F,s) = Comput (F,s,k) )
assume A1: F . (IC (Comput (F,s,k))) = halt S ; ::_thesis: Result (F,s) = Comput (F,s,k)
then A2: F halts_on s by Th30;
 dom F = NAT by PARTFUN1:def_2;
then  CurInstr (F,(Comput (F,s,k))) = halt S by A1, PARTFUN1:def_6;
hence  Result (F,s) = Comput (F,s,k) by A2, Def9; ::_thesis: verum
end;

theorem Th32: :: EXTPRO_1:32
for N being non empty with_zero set
for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N
for F being Instruction-Sequence of S
for s being State of S
for k being Element of NAT holds
( F . (IC (Comput (F,s,k))) <> halt S & F . (IC (Comput (F,s,(k + 1)))) = halt S iff ( LifeSpan (F,s) = k + 1 & F halts_on s ) )
proof
let N be non empty with_zero set ; ::_thesis: for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N
for F being Instruction-Sequence of S
for s being State of S
for k being Element of NAT holds
( F . (IC (Comput (F,s,k))) <> halt S & F . (IC (Comput (F,s,(k + 1)))) = halt S iff ( LifeSpan (F,s) = k + 1 & F halts_on s ) )
let S be non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N; ::_thesis: for F being Instruction-Sequence of S
for s being State of S
for k being Element of NAT holds
( F . (IC (Comput (F,s,k))) <> halt S & F . (IC (Comput (F,s,(k + 1)))) = halt S iff ( LifeSpan (F,s) = k + 1 & F halts_on s ) )
let F be Instruction-Sequence of S; ::_thesis: for s being State of S
for k being Element of NAT holds
( F . (IC (Comput (F,s,k))) <> halt S & F . (IC (Comput (F,s,(k + 1)))) = halt S iff ( LifeSpan (F,s) = k + 1 & F halts_on s ) )
let s be State of S; ::_thesis: for k being Element of NAT holds
( F . (IC (Comput (F,s,k))) <> halt S & F . (IC (Comput (F,s,(k + 1)))) = halt S iff ( LifeSpan (F,s) = k + 1 & F halts_on s ) )
let k be Element of NAT ; ::_thesis: ( F . (IC (Comput (F,s,k))) <> halt S & F . (IC (Comput (F,s,(k + 1)))) = halt S iff ( LifeSpan (F,s) = k + 1 & F halts_on s ) )
A1: dom F = NAT by PARTFUN1:def_2;
hereby  ::_thesis: ( LifeSpan (F,s) = k + 1 & F halts_on s implies ( F . (IC (Comput (F,s,k))) <> halt S & F . (IC (Comput (F,s,(k + 1)))) = halt S ) )
assume that
A2: F . (IC (Comput (F,s,k))) <> halt S and
A3: F . (IC (Comput (F,s,(k + 1)))) = halt S ; ::_thesis: ( LifeSpan (F,s) = k + 1 & F halts_on s )
A4: CurInstr (F,(Comput (F,s,k))) <> halt S by A2, A1, PARTFUN1:def_6;
A5: now__::_thesis:_for_i_being_Element_of_NAT_st_CurInstr_(F,(Comput_(F,s,i)))_=_halt_S_holds_
not_k_+_1_>_i
let i be Element of NAT ; ::_thesis: ( CurInstr (F,(Comput (F,s,i))) = halt S implies not k + 1 > i )
assume that
A6: CurInstr (F,(Comput (F,s,i))) = halt S and
A7: k + 1 > i ; ::_thesis: contradiction
 i <= k by A7, NAT_1:13;
hence  contradiction by A4, A6, Th5; ::_thesis: verum
end;
A8: F halts_on s by A3, Th30;
 CurInstr (F,(Comput (F,s,(k + 1)))) = halt S by A3, A1, PARTFUN1:def_6;
hence  ( LifeSpan (F,s) = k + 1 & F halts_on s ) by A5, Def15, A8; ::_thesis: verum
end;
assume A9: ( LifeSpan (F,s) = k + 1 & F halts_on s ) ; ::_thesis: ( F . (IC (Comput (F,s,k))) <> halt S & F . (IC (Comput (F,s,(k + 1)))) = halt S )
A10: now__::_thesis:_not_CurInstr_(F,(Comput_(F,s,k)))_=_halt_S
assume  CurInstr (F,(Comput (F,s,k))) = halt S ; ::_thesis: contradiction
then  k + 1 <= k by A9, Def15;
hence  contradiction by NAT_1:13; ::_thesis: verum
end;
 CurInstr (F,(Comput (F,s,(k + 1)))) = halt S by A9, Def15;
hence  ( F . (IC (Comput (F,s,k))) <> halt S & F . (IC (Comput (F,s,(k + 1)))) = halt S ) by A10, A1, PARTFUN1:def_6; ::_thesis: verum
end;

theorem :: EXTPRO_1:33
for N being non empty with_zero set
for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N
for F being Instruction-Sequence of S
for s being State of S
for k being Element of NAT st IC (Comput (F,s,k)) <> IC (Comput (F,s,(k + 1))) & F . (IC (Comput (F,s,(k + 1)))) = halt S holds
LifeSpan (F,s) = k + 1
proof
let N be non empty with_zero set ; ::_thesis: for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N
for F being Instruction-Sequence of S
for s being State of S
for k being Element of NAT st IC (Comput (F,s,k)) <> IC (Comput (F,s,(k + 1))) & F . (IC (Comput (F,s,(k + 1)))) = halt S holds
LifeSpan (F,s) = k + 1
let S be non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N; ::_thesis: for F being Instruction-Sequence of S
for s being State of S
for k being Element of NAT st IC (Comput (F,s,k)) <> IC (Comput (F,s,(k + 1))) & F . (IC (Comput (F,s,(k + 1)))) = halt S holds
LifeSpan (F,s) = k + 1
let F be Instruction-Sequence of S; ::_thesis: for s being State of S
for k being Element of NAT st IC (Comput (F,s,k)) <> IC (Comput (F,s,(k + 1))) & F . (IC (Comput (F,s,(k + 1)))) = halt S holds
LifeSpan (F,s) = k + 1
let s be State of S; ::_thesis: for k being Element of NAT st IC (Comput (F,s,k)) <> IC (Comput (F,s,(k + 1))) & F . (IC (Comput (F,s,(k + 1)))) = halt S holds
LifeSpan (F,s) = k + 1
let k be Element of NAT ; ::_thesis: ( IC (Comput (F,s,k)) <> IC (Comput (F,s,(k + 1))) & F . (IC (Comput (F,s,(k + 1)))) = halt S implies LifeSpan (F,s) = k + 1 )
assume that
A1: IC (Comput (F,s,k)) <> IC (Comput (F,s,(k + 1))) and
A2: F . (IC (Comput (F,s,(k + 1)))) = halt S ; ::_thesis: LifeSpan (F,s) = k + 1
A3: dom F = NAT by PARTFUN1:def_2;
now__::_thesis:_not_F_._(IC_(Comput_(F,s,k)))_=_halt_S
assume  F . (IC (Comput (F,s,k))) = halt S ; ::_thesis: contradiction
then  CurInstr (F,(Comput (F,s,k))) = halt S by A3, PARTFUN1:def_6;
hence  contradiction by A1, Th5, NAT_1:11; ::_thesis: verum
end;
hence  LifeSpan (F,s) = k + 1 by A2, Th32; ::_thesis: verum
end;

theorem :: EXTPRO_1:34
for N being non empty with_zero set
for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N
for F being Instruction-Sequence of S
for s being State of S
for k being Element of NAT st F halts_on Comput (F,s,k) & 0 < LifeSpan (F,(Comput (F,s,k))) holds
LifeSpan (F,s) = k + (LifeSpan (F,(Comput (F,s,k))))
proof
let N be non empty with_zero set ; ::_thesis: for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N
for F being Instruction-Sequence of S
for s being State of S
for k being Element of NAT st F halts_on Comput (F,s,k) & 0 < LifeSpan (F,(Comput (F,s,k))) holds
LifeSpan (F,s) = k + (LifeSpan (F,(Comput (F,s,k))))
let S be non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N; ::_thesis: for F being Instruction-Sequence of S
for s being State of S
for k being Element of NAT st F halts_on Comput (F,s,k) & 0 < LifeSpan (F,(Comput (F,s,k))) holds
LifeSpan (F,s) = k + (LifeSpan (F,(Comput (F,s,k))))
let F be Instruction-Sequence of S; ::_thesis: for s being State of S
for k being Element of NAT st F halts_on Comput (F,s,k) & 0 < LifeSpan (F,(Comput (F,s,k))) holds
LifeSpan (F,s) = k + (LifeSpan (F,(Comput (F,s,k))))
let s be State of S; ::_thesis: for k being Element of NAT st F halts_on Comput (F,s,k) & 0 < LifeSpan (F,(Comput (F,s,k))) holds
LifeSpan (F,s) = k + (LifeSpan (F,(Comput (F,s,k))))
let k be Element of NAT ; ::_thesis: ( F halts_on Comput (F,s,k) & 0 < LifeSpan (F,(Comput (F,s,k))) implies LifeSpan (F,s) = k + (LifeSpan (F,(Comput (F,s,k)))) )
set s2 = Comput (F,s,k);
set c = LifeSpan (F,(Comput (F,s,k)));
assume that
A1: F halts_on Comput (F,s,k) and
A2: 0 < LifeSpan (F,(Comput (F,s,k))) ; ::_thesis: LifeSpan (F,s) = k + (LifeSpan (F,(Comput (F,s,k))))
consider l being Nat such that
A3: LifeSpan (F,(Comput (F,s,k))) = l + 1 by A2, NAT_1:6;
reconsider l = l as Element of NAT by ORDINAL1:def_12;
 F . (IC (Comput (F,(Comput (F,s,k)),(l + 1)))) = halt S by A1, A3, Th32;
then A4: F . (IC (Comput (F,s,(k + (l + 1))))) = halt S by Th4;
 F . (IC (Comput (F,(Comput (F,s,k)),l))) <> halt S by A1, A3, Th32;
then  F . (IC (Comput (F,s,(k + l)))) <> halt S by Th4;
hence  LifeSpan (F,s) = (k + l) + 1 by A4, Th32
.= k + (LifeSpan (F,(Comput (F,s,k)))) by A3 ;
::_thesis: verum
end;

theorem :: EXTPRO_1:35
for N being non empty with_zero set
for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N
for F being Instruction-Sequence of S
for s being State of S
for k being Element of NAT st F halts_on Comput (F,s,k) holds
Result (F,(Comput (F,s,k))) = Result (F,s)
proof
let N be non empty with_zero set ; ::_thesis: for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N
for F being Instruction-Sequence of S
for s being State of S
for k being Element of NAT st F halts_on Comput (F,s,k) holds
Result (F,(Comput (F,s,k))) = Result (F,s)
let S be non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N; ::_thesis: for F being Instruction-Sequence of S
for s being State of S
for k being Element of NAT st F halts_on Comput (F,s,k) holds
Result (F,(Comput (F,s,k))) = Result (F,s)
let F be Instruction-Sequence of S; ::_thesis: for s being State of S
for k being Element of NAT st F halts_on Comput (F,s,k) holds
Result (F,(Comput (F,s,k))) = Result (F,s)
let s be State of S; ::_thesis: for k being Element of NAT st F halts_on Comput (F,s,k) holds
Result (F,(Comput (F,s,k))) = Result (F,s)
let k be Element of NAT ; ::_thesis: ( F halts_on Comput (F,s,k) implies Result (F,(Comput (F,s,k))) = Result (F,s) )
set s2 = Comput (F,s,k);
assume A1: F halts_on Comput (F,s,k) ; ::_thesis: Result (F,(Comput (F,s,k))) = Result (F,s)
then consider l being Element of NAT  such that
A2: ( Result (F,(Comput (F,s,k))) = Comput (F,(Comput (F,s,k)),l) & CurInstr (F,(Result (F,(Comput (F,s,k))))) = halt S ) by Def9;
A3: F halts_on s by A1, Th22;
 Comput (F,(Comput (F,s,k)),l) = Comput (F,s,(k + l)) by Th4;
hence  Result (F,(Comput (F,s,k))) = Result (F,s) by A3, A2, Def9; ::_thesis: verum
end;


theorem :: EXTPRO_1:36
for N being non empty with_zero set
for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N
for P being Instruction-Sequence of S
for s being State of S st P halts_on s holds
for k being Element of NAT st LifeSpan (P,s) <= k holds
CurInstr (P,(Comput (P,s,k))) = halt S
proof
let N be non empty with_zero set ; ::_thesis: for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N
for P being Instruction-Sequence of S
for s being State of S st P halts_on s holds
for k being Element of NAT st LifeSpan (P,s) <= k holds
CurInstr (P,(Comput (P,s,k))) = halt S
let S be non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N; ::_thesis: for P being Instruction-Sequence of S
for s being State of S st P halts_on s holds
for k being Element of NAT st LifeSpan (P,s) <= k holds
CurInstr (P,(Comput (P,s,k))) = halt S
let P be Instruction-Sequence of S; ::_thesis: for s being State of S st P halts_on s holds
for k being Element of NAT st LifeSpan (P,s) <= k holds
CurInstr (P,(Comput (P,s,k))) = halt S
let s be State of S; ::_thesis: ( P halts_on s implies for k being Element of NAT st LifeSpan (P,s) <= k holds
CurInstr (P,(Comput (P,s,k))) = halt S )
assume  P halts_on s ; ::_thesis: for k being Element of NAT st LifeSpan (P,s) <= k holds
CurInstr (P,(Comput (P,s,k))) = halt S
then A1: CurInstr (P,(Comput (P,s,(LifeSpan (P,s))))) = halt S by Def15;
let k be Element of NAT ; ::_thesis: ( LifeSpan (P,s) <= k implies CurInstr (P,(Comput (P,s,k))) = halt S )
assume  LifeSpan (P,s) <= k ; ::_thesis: CurInstr (P,(Comput (P,s,k))) = halt S
hence  CurInstr (P,(Comput (P,s,k))) = halt S by A1, Th5; ::_thesis: verum
end;