:: Externally Programmed Machines
:: by Yatsuka Nakamura and Andrzej Trybulec
::
:: Received June 30, 2010
:: Copyright (c) 2010-2012 Association of Mizar Users


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)))) )
proofend;
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
proofend;
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
proofend;
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
proofend;
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 )
proofend;
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
proofend;
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
proofend;
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
proofend;
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
proofend;
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
proofend;

registration
let E be with_zero set ;
cluster Trivial-AMI E ->  IC-Ins-separated strict ;
coherence
 Trivial-AMI E is IC-Ins-separated
proofend;
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 )
proofend;
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 )
proofend;
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)) ) )
proofend;
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
proofend;
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
proofend;
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)))
proofend;

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)
proofend;

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)
proofend;

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) &amp; 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) &amp; CurInstr (p,b1) = halt S ) &amp; ex k being Element of NAT st
( b2 = Comput (p,s,k) &amp; CurInstr (p,b2) = halt S ) holds
b1 = b2
proofend;
correctness
existence
ex b1 being State of S ex k being Element of NAT st
( b1 = Comput (p,s,k) &amp; CurInstr (p,b1) = halt S );
proofend;
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) &amp; 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)))
proofend;

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)
proofend;

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)))
proofend;

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 &amp; p c= Q holds
for s1, s2 being State of S st IT c= s1 &amp; 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 &amp; p c= Q holds
for s1, s2 being State of S st IT c= s1 &amp; 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 &amp; b1 is strict )
proofend;
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
proofend;

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
proofend;

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
proofend;

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
proofend;

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 &amp; b1 is P -halted &amp; not b1 is empty )
proofend;
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 &amp; it is P -halted );
existence
 ex b1 being FinPartState of S st
( b1 is P -autonomic &amp; b1 is P -halted )
proofend;
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 &amp; 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)
proofend;
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) ) &amp; ( 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;
proofend;
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 &amp; d +* s is Autonomy of p &amp; 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 &amp; d +* s is Autonomy of p &amp; 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 {}
proofend;

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)) )
proofend;

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 {} .--> {} )
proofend;

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
proofend;
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)) )
proofend;

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)) )
proofend;

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)
proofend;

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))
proofend;

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)
proofend;

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)))
proofend;

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 &amp; ( 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 &amp; ( for k being Element of NAT st CurInstr (p,(Comput (p,s,k))) = halt S holds
b1 <= k ) )
proofend;
uniqueness
 for b1, b2 being Element of NAT st CurInstr (p,(Comput (p,s,b1))) = halt S &amp; ( for k being Element of NAT st CurInstr (p,(Comput (p,s,k))) = halt S holds
b1 <= k ) &amp; CurInstr (p,(Comput (p,s,b2))) = halt S &amp; ( for k being Element of NAT st CurInstr (p,(Comput (p,s,k))) = halt S holds
b2 <= k ) holds
b1 = b2
proofend;
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 &amp; ( 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) )
proofend;

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)))
proofend;

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)
proofend;

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 &amp; p halts_on s holds
Comput (p,s,j) = Comput (p,s,(LifeSpan (p,s)))
proofend;

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)
proofend;

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
proofend;

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))
proofend;

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 )
proofend;

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
proofend;

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)
proofend;

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 &amp; F . (IC (Comput (F,s,(k + 1)))) = halt S iff ( LifeSpan (F,s) = k + 1 &amp; F halts_on s ) )
proofend;

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))) &amp; F . (IC (Comput (F,s,(k + 1)))) = halt S holds
LifeSpan (F,s) = k + 1
proofend;

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) &amp; 0 < LifeSpan (F,(Comput (F,s,k))) holds
LifeSpan (F,s) = k + (LifeSpan (F,(Comput (F,s,k))))
proofend;

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)
proofend;

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
proofend;