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


begin

definition
let N be set ;
attr c2 is strict ;
struct AMI-Struct of N -> COM-Struct of N;
aggr AMI-Struct(# carrier, ZeroF, Instructions, haltF, Object-Kind, Execution #) -> AMI-Struct of N;
sel Execution c2 -> Action of the Instructions of c2,(product the Object-Kind of c2);
end;

definition
let N be set ;
func Trivial-AMI N -> strict AMI-Struct of N means :Def1: :: EXTPRO_1:def 1
( the carrier of it = succ NAT & the ZeroF of it = NAT & the Instructions of it = {[0,{},{}]} & the haltF of it = [0,{},{}] & the Object-Kind of it = (NAT --> {[0,{},{}]}) +* (NAT .--> NAT) & the Execution of it = [0,{},{}] .--> (id (product ((NAT --> {[0,{},{}]}) +* (NAT .--> NAT)))) );
existence
ex b1 being strict AMI-Struct of N st
( the carrier of b1 = succ NAT & the ZeroF of b1 = NAT & the Instructions of b1 = {[0,{},{}]} & the haltF of b1 = [0,{},{}] & the Object-Kind of b1 = (NAT --> {[0,{},{}]}) +* (NAT .--> NAT) & the Execution of b1 = [0,{},{}] .--> (id (product ((NAT --> {[0,{},{}]}) +* (NAT .--> NAT)))) )
proof end;
uniqueness
for b1, b2 being strict AMI-Struct of N st the carrier of b1 = succ NAT & the ZeroF of b1 = NAT & the Instructions of b1 = {[0,{},{}]} & the haltF of b1 = [0,{},{}] & the Object-Kind of b1 = (NAT --> {[0,{},{}]}) +* (NAT .--> NAT) & the Execution of b1 = [0,{},{}] .--> (id (product ((NAT --> {[0,{},{}]}) +* (NAT .--> NAT)))) & the carrier of b2 = succ NAT & the ZeroF of b2 = NAT & the Instructions of b2 = {[0,{},{}]} & the haltF of b2 = [0,{},{}] & the Object-Kind of b2 = (NAT --> {[0,{},{}]}) +* (NAT .--> NAT) & the Execution of b2 = [0,{},{}] .--> (id (product ((NAT --> {[0,{},{}]}) +* (NAT .--> NAT)))) holds
b1 = b2
;
end;

:: deftheorem Def1 defines Trivial-AMI EXTPRO_1:def 1 :
for N being set
for b2 being strict AMI-Struct of N holds
( b2 = Trivial-AMI N iff ( the carrier of b2 = succ NAT & the ZeroF of b2 = NAT & the Instructions of b2 = {[0,{},{}]} & the haltF of b2 = [0,{},{}] & the Object-Kind of b2 = (NAT --> {[0,{},{}]}) +* (NAT .--> NAT) & the Execution of b2 = [0,{},{}] .--> (id (product ((NAT --> {[0,{},{}]}) +* (NAT .--> NAT)))) ) );

registration
let N be set ;
cluster Trivial-AMI N -> non empty stored-program strict ;
coherence
( not Trivial-AMI N is empty & Trivial-AMI N is stored-program )
proof end;
end;

registration
let N be set ;
cluster non empty stored-program AMI-Struct of N;
existence
ex b1 being AMI-Struct of N st
( not b1 is empty & b1 is stored-program )
proof end;
end;

definition
let N be with_non-empty_elements set ;
let S be AMI-Struct of 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 end;
end;

:: deftheorem defines Exec EXTPRO_1:def 2 :
for N being with_non-empty_elements set
for S being AMI-Struct of 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_non-empty_elements set ;
let S be AMI-Struct of N;
let I be Instruction of S;
attr I 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_non-empty_elements set
for S being AMI-Struct of 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_non-empty_elements set ;
let S be AMI-Struct of N;
attr S is halting means :Def4: :: EXTPRO_1:def 4
the haltF of S is halting ;
end;

:: deftheorem Def4 defines halting EXTPRO_1:def 4 :
for N being with_non-empty_elements set
for S being AMI-Struct of N holds
( S is halting iff the haltF of S is halting );

registration
let N be with_non-empty_elements set ;
cluster Trivial-AMI N -> strict halting ;
coherence
Trivial-AMI N is halting
proof end;
end;

registration
let N be with_non-empty_elements set ;
cluster halting AMI-Struct of N;
existence
ex b1 being AMI-Struct of N st b1 is halting
proof end;
end;

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

registration
let N be with_non-empty_elements set ;
let S be halting AMI-Struct of N;
cluster halting Element of the Instructions of S;
existence
ex b1 being Instruction of S st b1 is halting
proof end;
end;

theorem :: EXTPRO_1:1
for N being with_non-empty_elements set
for s being State of (Trivial-AMI N)
for i being Instruction of (Trivial-AMI N) holds Exec (i,s) = s
proof end;

registration
let E be set ;
cluster Trivial-AMI E -> IC-Ins-separated definite strict ;
coherence
( Trivial-AMI E is IC-Ins-separated & Trivial-AMI E is definite )
proof end;
end;

registration
let M be set ;
cluster non empty stored-program IC-Ins-separated definite strict AMI-Struct of M;
existence
ex b1 being non empty stored-program AMI-Struct of M st
( b1 is IC-Ins-separated & b1 is definite & b1 is strict )
proof end;
end;

registration
let N be with_non-empty_elements set ;
cluster non empty stored-program IC-Ins-separated definite strict halting AMI-Struct of N;
existence
ex b1 being non empty stored-program AMI-Struct of N st
( b1 is IC-Ins-separated & b1 is halting & b1 is definite & b1 is strict )
proof end;
end;

theorem :: EXTPRO_1:2
for N being with_non-empty_elements set
for s1, s2 being State of (Trivial-AMI N) st IC s1 = IC s2 holds
s1 = s2
proof end;

begin

definition
let N be non empty with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite AMI-Struct of N;
let s be State of S;
let p be the Instructions of S -valued Function;
func Following (p,s) -> State of S equals :: EXTPRO_1:def 5
Exec ((CurInstr (p,s)),s);
correctness
coherence
Exec ((CurInstr (p,s)),s) is State of S
;
;
end;

:: deftheorem defines Following EXTPRO_1:def 5 :
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite AMI-Struct of N
for s being State of S
for p being the Instructions of b2 -valued Function holds Following (p,s) = Exec ((CurInstr (p,s)),s);

definition
let N be non empty with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite AMI-Struct of N;
let p be NAT -defined the Instructions of S -valued Function;
deffunc H1( set , State of S) -> Element of product the Object-Kind 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 :Def6: :: EXTPRO_1:def 6
ex f being Function of NAT,(product the Object-Kind 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 Object-Kind of S) st
( b1 = f . k & f . 0 = s & ( for i being Nat holds f . (i + 1) = Following (p,(f . i)) ) )
proof end;
uniqueness
for b1, b2 being State of S st ex f being Function of NAT,(product the Object-Kind 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 Object-Kind 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 end;
end;

:: deftheorem Def6 defines Comput EXTPRO_1:def 6 :
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite AMI-Struct of N
for p being NAT -defined the Instructions 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 Object-Kind 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 non empty with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite halting AMI-Struct of N;
let p be NAT -defined the Instructions of S -valued Function;
let s be State of S;
pred p halts_on s means :Def7: :: EXTPRO_1:def 7
ex k being Nat st
( IC (Comput (p,s,k)) in dom p & CurInstr (p,(Comput (p,s,k))) = halt S );
end;

:: deftheorem Def7 defines halts_on EXTPRO_1:def 7 :
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite halting AMI-Struct of N
for p being NAT -defined the Instructions 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 ) );

theorem Th3: :: EXTPRO_1:3
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite AMI-Struct of N
for p being NAT -defined the Instructions of b2 -valued Function
for s being State of S holds Comput (p,s,0) = s
proof end;

theorem Th4: :: EXTPRO_1:4
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite AMI-Struct of N
for p being NAT -defined the Instructions 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 end;

theorem Th5: :: EXTPRO_1:5
for i being Element of NAT
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite AMI-Struct of N
for s being State of S
for p being NAT -defined the Instructions of b3 -valued Function
for k being Element of NAT holds Comput (p,s,(i + k)) = Comput (p,(Comput (p,s,i)),k)
proof end;

theorem Th6: :: EXTPRO_1:6
for i, j being Element of NAT st i <= j holds
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite halting AMI-Struct of N
for p being NAT -defined the Instructions 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 end;

definition
let N be non empty with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite halting AMI-Struct of N;
let p be NAT -defined the Instructions of S -valued Function;
let s be State of S;
assume A1: p halts_on s ;
func Result (p,s) -> State of S means :Def8: :: EXTPRO_1:def 8
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 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 end;
end;

:: deftheorem Def8 defines Result EXTPRO_1:def 8 :
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite halting AMI-Struct of N
for p being NAT -defined the Instructions 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:7
for k being Element of NAT
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite AMI-Struct of N
for P being the Instructions of b3 -valued ManySortedSet of NAT
for s being State of S holds Comput (P,s,(k + 1)) = Exec ((P . (IC (Comput (P,s,k)))),(Comput (P,s,k)))
proof end;

theorem Th8: :: EXTPRO_1:8
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite halting AMI-Struct of N
for P being the Instructions of b2 -valued ManySortedSet of NAT
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 end;

theorem Th9: :: EXTPRO_1:9
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite halting AMI-Struct of N
for P being the Instructions of b2 -valued ManySortedSet of NAT
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 end;

definition
let N be non empty with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite AMI-Struct of N;
let IT be PartState of S;
attr IT is autonomic means :Def9: :: EXTPRO_1:def 9
for P, Q being the Instructions of S -valued ManySortedSet of NAT st ProgramPart IT c= P & ProgramPart IT c= Q holds
for s1, s2 being State of S st NPP IT c= s1 & NPP IT c= s2 holds
for i being Element of NAT holds (Comput (P,s1,i)) | (dom (NPP IT)) = (Comput (Q,s2,i)) | (dom (NPP IT));
end;

:: deftheorem Def9 defines autonomic EXTPRO_1:def 9 :
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite AMI-Struct of N
for IT being PartState of S holds
( IT is autonomic iff for P, Q being the Instructions of b2 -valued ManySortedSet of NAT st ProgramPart IT c= P & ProgramPart IT c= Q holds
for s1, s2 being State of S st NPP IT c= s1 & NPP IT c= s2 holds
for i being Element of NAT holds (Comput (P,s1,i)) | (dom (NPP IT)) = (Comput (Q,s2,i)) | (dom (NPP IT)) );

definition
let N be non empty with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite halting AMI-Struct of N;
let IT be PartState of S;
attr IT is halting means :Def10: :: EXTPRO_1:def 10
for s being State of S st NPP IT c= s holds
for P being the Instructions of S -valued ManySortedSet of NAT st ProgramPart IT c= P holds
P halts_on s;
end;

:: deftheorem Def10 defines halting EXTPRO_1:def 10 :
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite halting AMI-Struct of N
for IT being PartState of S holds
( IT is halting iff for s being State of S st NPP IT c= s holds
for P being the Instructions of b2 -valued ManySortedSet of NAT st ProgramPart IT c= P holds
P halts_on s );

registration
let N be non empty with_non-empty_elements set ;
cluster Trivial-AMI N -> realistic strict ;
coherence
Trivial-AMI N is realistic
proof end;
end;

registration
let N be non empty with_non-empty_elements set ;
cluster non empty stored-program IC-Ins-separated definite realistic strict halting AMI-Struct of N;
existence
ex b1 being non empty stored-program IC-Ins-separated definite AMI-Struct of N st
( b1 is halting & b1 is realistic & b1 is strict )
proof end;
end;

begin

theorem Th10: :: EXTPRO_1:10
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite realistic halting AMI-Struct of N
for l being Element of NAT
for P being NAT -defined the Instructions of b2 -valued Function st l .--> (halt S) c= P holds
for p being b3 -started PartState of S holds p +* P is halting
proof end;

theorem Th11: :: EXTPRO_1:11
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite realistic halting AMI-Struct of N
for l being Element of NAT
for P being NAT -defined the Instructions 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 end;

theorem Th12: :: EXTPRO_1:12
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite realistic halting AMI-Struct of N
for l being Element of NAT
for P being NAT -defined the Instructions of b2 -valued Function st l .--> (halt S) c= P holds
for p being b3 -started PartState of S holds p +* P is autonomic
proof end;

registration
let N be non empty with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite realistic halting AMI-Struct of N;
let l be Element of NAT ;
cluster Relation-like the carrier of S -defined Function-like the Object-Kind of S -compatible finite countable V114() l -started non program-free autonomic halting set ;
existence
ex b1 being FinPartState of S st
( b1 is autonomic & b1 is halting & not b1 is program-free & b1 is l -started )
proof end;
end;

definition
let N be non empty with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite realistic halting AMI-Struct of N;
let P be NAT -defined the Instructions of S -valued non halt-free Function;
mode Autonomy of P -> FinPartState of S means :Def11: :: EXTPRO_1:def 11
( it +* P is autonomic & it +* P is halting );
existence
ex b1 being FinPartState of S st
( b1 +* P is autonomic & b1 +* P is halting )
proof end;
end;

:: deftheorem Def11 defines Autonomy EXTPRO_1:def 11 :
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite realistic halting AMI-Struct of N
for P being NAT -defined the Instructions of b2 -valued non halt-free Function
for b4 being FinPartState of S holds
( b4 is Autonomy of P iff ( b4 +* P is autonomic & b4 +* P is halting ) );

definition
let N be non empty with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite realistic halting AMI-Struct of N;
let p be NAT -defined the Instructions of S -valued non halt-free Function;
let d be FinPartState of S;
assume A1: ( d is Autonomy of p & p = ProgramPart d ) ;
func Result (p,d) -> FinPartState of S means :: EXTPRO_1:def 12
for P being the Instructions of S -valued ManySortedSet of NAT st p c= P holds
for s being State of S st d c= s holds
it = (Result (P,s)) | (dom (NPP d));
existence
ex b1 being FinPartState of S st
for P being the Instructions of S -valued ManySortedSet of NAT st p c= P holds
for s being State of S st d c= s holds
b1 = (Result (P,s)) | (dom (NPP d))
proof end;
correctness
uniqueness
for b1, b2 being FinPartState of S st ( for P being the Instructions of S -valued ManySortedSet of NAT st p c= P holds
for s being State of S st d c= s holds
b1 = (Result (P,s)) | (dom (NPP d)) ) & ( for P being the Instructions of S -valued ManySortedSet of NAT st p c= P holds
for s being State of S st d c= s holds
b2 = (Result (P,s)) | (dom (NPP d)) ) holds
b1 = b2
;
proof end;
end;

:: deftheorem defines Result EXTPRO_1:def 12 :
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite realistic halting AMI-Struct of N
for p being NAT -defined the Instructions of b2 -valued non halt-free Function
for d being FinPartState of S st d is Autonomy of p & p = ProgramPart d holds
for b5 being FinPartState of S holds
( b5 = Result (p,d) iff for P being the Instructions of b2 -valued ManySortedSet of NAT st p c= P holds
for s being State of S st d c= s holds
b5 = (Result (P,s)) | (dom (NPP d)) );

begin

definition
let N be non empty with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite realistic halting AMI-Struct of N;
let p be NAT -defined the Instructions of S -valued non halt-free Function;
let d be FinPartState of S;
let F be Function;
pred p,d computes F means :Def13: :: EXTPRO_1:def 13
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 Def13 defines computes EXTPRO_1:def 13 :
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite realistic halting AMI-Struct of N
for p being NAT -defined the Instructions 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_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite realistic halting AMI-Struct of N
for p being NAT -defined the Instructions of b2 -valued non halt-free Function
for d being FinPartState of S holds p,d computes {}
proof end;

theorem :: EXTPRO_1:14
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite realistic halting AMI-Struct of N
for p being NAT -defined the Instructions 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 end;

theorem :: EXTPRO_1:15
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite realistic halting AMI-Struct of N
for p being NAT -defined the Instructions of b2 -valued non halt-free Function
for d being FinPartState of S holds
( d is Autonomy of p iff p,d computes {} .--> {} )
proof end;

begin

registration
let N be set ;
cluster Trivial-AMI N -> standard-ins strict ;
coherence
Trivial-AMI N is standard-ins
proof end;
end;

registration
let N be non empty with_non-empty_elements set ;
cluster non empty stored-program IC-Ins-separated definite standard-ins AMI-Struct of N;
existence
ex b1 being non empty stored-program AMI-Struct of N st
( b1 is IC-Ins-separated & b1 is definite & b1 is standard-ins )
proof end;
end;

begin

theorem Th16: :: EXTPRO_1:16
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite halting AMI-Struct of N
for p being NAT -defined the Instructions 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 end;

theorem Th17: :: EXTPRO_1:17
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite halting AMI-Struct of N
for p being NAT -defined the Instructions 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 end;

theorem Th18: :: EXTPRO_1:18
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite halting AMI-Struct of N
for P being NAT -defined the Instructions 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 end;

theorem Th19: :: EXTPRO_1:19
for i, j being Element of NAT
for N being non empty with_non-empty_elements set st i <= j holds
for S being non empty stored-program IC-Ins-separated definite halting AMI-Struct of N
for P being NAT -defined the Instructions 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 end;

theorem :: EXTPRO_1:20
for i, j being Element of NAT
for N being non empty with_non-empty_elements set st i <= j holds
for S being non empty stored-program IC-Ins-separated definite halting AMI-Struct of N
for P being NAT -defined the Instructions 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 end;

theorem :: EXTPRO_1:21
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite halting AMI-Struct of N
for P being the Instructions of b2 -valued ManySortedSet of NAT
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 end;

definition
let N be non empty with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite halting AMI-Struct of N;
let p be NAT -defined the Instructions of S -valued Function;
let s be State of S;
assume A1: p halts_on s ;
func LifeSpan (p,s) -> Element of NAT means :Def14: :: EXTPRO_1:def 14
( 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 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 end;
end;

:: deftheorem Def14 defines LifeSpan EXTPRO_1:def 14 :
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite halting AMI-Struct of N
for p being NAT -defined the Instructions 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_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite halting AMI-Struct of N
for p being NAT -defined the Instructions 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 end;

theorem :: EXTPRO_1:23
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite halting AMI-Struct of N
for p being NAT -defined the Instructions 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 end;

theorem :: EXTPRO_1:24
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite halting AMI-Struct of N
for P being the Instructions of b2 -valued ManySortedSet of NAT
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 end;

theorem :: EXTPRO_1:25
for j being Element of NAT
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite halting AMI-Struct of N
for p being NAT -defined the Instructions 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 end;

theorem :: EXTPRO_1:26
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite realistic AMI-Struct of N
for t, u being State of S
for e being Element of NAT
for I being Instruction of S st u = t +* (((IC ),e) --> (e,I)) holds
( u . e = I & IC u = e & IC (Following ((ProgramPart u),u)) = (Exec ((u . (IC u)),u)) . (IC ) )
proof end;

theorem :: EXTPRO_1:27
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite halting AMI-Struct of N
for P being the Instructions of b2 -valued ManySortedSet of NAT
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 end;

theorem :: EXTPRO_1:28
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite AMI-Struct of N
for P being the Instructions of b2 -valued ManySortedSet of NAT
for s being State of S
for i being Instruction of S holds (Exec ((P . (IC s)),s)) . (IC ) = IC (Following (P,s))
proof end;

theorem :: EXTPRO_1:29
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite realistic AMI-Struct of N
for t, u being State of S
for il being Element of NAT
for e being Element of ObjectKind (IC )
for I being Element of the Object-Kind of S . il st e = il & u = t +* (((IC ),il) --> (e,I)) holds
( u . il = I & IC u = il & IC (Following ((ProgramPart u),u)) = (Exec ((u . (IC u)),u)) . (IC ) )
proof end;

theorem :: EXTPRO_1:30
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite halting AMI-Struct of N
for P being the Instructions of b2 -valued ManySortedSet of NAT
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 end;

registration
let N be non empty with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite realistic halting AMI-Struct of N;
cluster Relation-like non NAT -defined the carrier of S -defined Function-like the Object-Kind of S -compatible finite countable V114() autonomic set ;
existence
ex b1 being FinPartState of S st
( b1 is autonomic & not b1 is NAT -defined )
proof end;
end;

registration
let N be non empty with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite realistic halting AMI-Struct of N;
cluster Relation-like the carrier of S -defined Function-like the Object-Kind of S -compatible finite countable V114() halting set ;
existence
ex b1 being FinPartState of S st b1 is halting
proof end;
end;

registration
let N be non empty with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite realistic halting AMI-Struct of N;
let p be non program-free halting PartState of S;
cluster ProgramPart p -> non halt-free ;
coherence
not ProgramPart p is halt-free
proof end;
end;

registration
let N be non empty with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite realistic halting AMI-Struct of N;
cluster Relation-like the carrier of S -defined Function-like the Object-Kind of S -compatible non program-free halting -> non halt-free set ;
coherence
for b1 being PartState of S st b1 is halting & not b1 is program-free holds
not b1 is halt-free
proof end;
end;

theorem Th31: :: EXTPRO_1:31
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite halting AMI-Struct of N
for F being NAT -defined the Instructions of b2 -valued total Function
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 end;

theorem :: EXTPRO_1:32
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite halting AMI-Struct of N
for F being NAT -defined the Instructions of b2 -valued total Function
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 end;

theorem Th33: :: EXTPRO_1:33
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite halting AMI-Struct of N
for F being NAT -defined the Instructions of b2 -valued total Function
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 end;

theorem :: EXTPRO_1:34
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite halting AMI-Struct of N
for F being NAT -defined the Instructions of b2 -valued total Function
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 end;

theorem :: EXTPRO_1:35
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite halting AMI-Struct of N
for F being NAT -defined the Instructions of b2 -valued total Function
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 end;

theorem :: EXTPRO_1:36
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite halting AMI-Struct of N
for F being NAT -defined the Instructions of b2 -valued total Function
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 end;