:: 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 c₂ 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 c₂ -> Action of the Instructions of c₂,(product the Object-Kind of c₂);

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 b₁ being strict AMI-Struct of N st
( the carrier of b₁ = succ NAT & the ZeroF of b₁ = NAT & the Instructions of b₁ = {[0,{},{}]} & the haltF of b₁ = [0,{},{}] & the Object-Kind of b₁ = (NAT --> {[0,{},{}]}) +* (NAT .--> NAT) & the Execution of b₁ = [0,{},{}] .--> (id (product ((NAT --> {[0,{},{}]}) +* (NAT .--> NAT)))) )

proof end;

uniqueness
for b₁, b₂ being strict AMI-Struct of N st the carrier of b₁ = succ NAT & the ZeroF of b₁ = NAT & the Instructions of b₁ = {[0,{},{}]} & the haltF of b₁ = [0,{},{}] & the Object-Kind of b₁ = (NAT --> {[0,{},{}]}) +* (NAT .--> NAT) & the Execution of b₁ = [0,{},{}] .--> (id (product ((NAT --> {[0,{},{}]}) +* (NAT .--> NAT)))) & the carrier of b₂ = succ NAT & the ZeroF of b₂ = NAT & the Instructions of b₂ = {[0,{},{}]} & the haltF of b₂ = [0,{},{}] & the Object-Kind of b₂ = (NAT --> {[0,{},{}]}) +* (NAT .--> NAT) & the Execution of b₂ = [0,{},{}] .--> (id (product ((NAT --> {[0,{},{}]}) +* (NAT .--> NAT)))) holds
b₁ = b₂ ;

end;

:: deftheorem Def1 defines Trivial-AMI EXTPRO_1:def 1 :
for N being set
for b₂ being strict AMI-Struct of N holds
( b₂ = Trivial-AMI N iff ( the carrier of b₂ = succ NAT & the ZeroF of b₂ = NAT & the Instructions of b₂ = {[0,{},{}]} & the haltF of b₂ = [0,{},{}] & the Object-Kind of b₂ = (NAT --> {[0,{},{}]}) +* (NAT .--> NAT) & the Execution of b₂ = [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 b₁ being AMI-Struct of N st
( not b₁ is empty & b₁ 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 b₁ being AMI-Struct of N st b₁ 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 b₁ being Instruction of S st b₁ 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 b₁ being non empty stored-program AMI-Struct of M st
( b₁ is IC-Ins-separated & b₁ is definite & b₁ 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 b₁ being non empty stored-program AMI-Struct of N st
( b₁ is IC-Ins-separated & b₁ is halting & b₁ is definite & b₁ 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 b₂ -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 H₁( 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 b₁ being State of S ex f being Function of NAT,(product the Object-Kind of S) st
( b₁ = f . k & f . 0 = s & ( for i being Nat holds f . (i + 1) = Following (p,(f . i)) ) )

proof end;

uniqueness
for b₁, b₂ being State of S st ex f being Function of NAT,(product the Object-Kind of S) st
( b₁ = 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
( b₂ = f . k & f . 0 = s & ( for i being Nat holds f . (i + 1) = Following (p,(f . i)) ) ) holds
b₁ = b₂

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 b₂ -valued Function
for s being State of S
for k being Nat
for b₆ being State of S holds
( b₆ = Comput (p,s,k) iff ex f being Function of NAT,(product the Object-Kind of S) st
( b₆ = 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 b₂ -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 b₂ -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 b₂ -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 b₃ -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 b₄ -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 b₁, b₂ being State of S st ex k being Element of NAT st
( b₁ = Comput (p,s,k) & CurInstr (p,b₁) = halt S ) & ex k being Element of NAT st
( b₂ = Comput (p,s,k) & CurInstr (p,b₂) = halt S ) holds
b₁ = b₂

proof end;

correctness
existence
ex b₁ being State of S ex k being Element of NAT st
( b₁ = Comput (p,s,k) & CurInstr (p,b₁) = 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 b₂ -valued Function
for s being State of S st p halts_on s holds
for b₅ being State of S holds
( b₅ = Result (p,s) iff ex k being Element of NAT st
( b₅ = Comput (p,s,k) & CurInstr (p,b₅) = 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 b₃ -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 b₂ -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 b₂ -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 b₂ -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 b₂ -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 b₁ being non empty stored-program IC-Ins-separated definite AMI-Struct of N st
( b₁ is halting & b₁ is realistic & b₁ 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 b₂ -valued Function st l .--> (halt S) c= P holds
for p being b₃ -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 b₂ -valued Function st l .--> (halt S) c= P holds
for p being b₃ -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 b₂ -valued Function st l .--> (halt S) c= P holds
for p being b₃ -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 b₁ being FinPartState of S st
( b₁ is autonomic & b₁ is halting & not b₁ is program-free & b₁ 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 b₁ being FinPartState of S st
( b₁ +* P is autonomic & b₁ +* 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 b₂ -valued non halt-free Function
for b₄ being FinPartState of S holds
( b₄ is Autonomy of P iff ( b₄ +* P is autonomic & b₄ +* 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 b₁ 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
b₁ = (Result (P,s)) | (dom (NPP d))

proof end;

correctness
uniqueness
for b₁, b₂ 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
b₁ = (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
b₂ = (Result (P,s)) | (dom (NPP d)) ) holds
b₁ = b₂;

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 b₂ -valued non halt-free Function
for d being FinPartState of S st d is Autonomy of p & p = ProgramPart d holds
for b₅ being FinPartState of S holds
( b₅ = Result (p,d) iff for P being the Instructions of b₂ -valued ManySortedSet of NAT st p c= P holds
for s being State of S st d c= s holds
b₅ = (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 b₂ -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 b₂ -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 b₂ -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 b₂ -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 b₁ being non empty stored-program AMI-Struct of N st
( b₁ is IC-Ins-separated & b₁ is definite & b₁ 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 b₂ -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 b₂ -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 b₂ -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 b₄ -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 b₄ -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 b₂ -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 b₁ being Element of NAT st
( CurInstr (p,(Comput (p,s,b₁))) = halt S & ( for k being Element of NAT st CurInstr (p,(Comput (p,s,k))) = halt S holds
b₁ <= k ) )

proof end;

uniqueness
for b₁, b₂ being Element of NAT st CurInstr (p,(Comput (p,s,b₁))) = halt S & ( for k being Element of NAT st CurInstr (p,(Comput (p,s,k))) = halt S holds
b₁ <= k ) & CurInstr (p,(Comput (p,s,b₂))) = halt S & ( for k being Element of NAT st CurInstr (p,(Comput (p,s,k))) = halt S holds
b₂ <= k ) holds
b₁ = b₂

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 b₂ -valued Function
for s being State of S st p halts_on s holds
for b₅ being Element of NAT holds
( b₅ = LifeSpan (p,s) iff ( CurInstr (p,(Comput (p,s,b₅))) = halt S & ( for k being Element of NAT st CurInstr (p,(Comput (p,s,k))) = halt S holds
b₅ <= 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 b₂ -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 b₂ -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 b₂ -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 b₃ -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 b₂ -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 b₂ -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 b₂ -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 b₁ being FinPartState of S st
( b₁ is autonomic & not b₁ 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 b₁ being FinPartState of S st b₁ 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 b₁ being PartState of S st b₁ is halting & not b₁ is program-free holds
not b₁ 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 b₂ -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 b₂ -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 b₂ -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 b₂ -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 b₂ -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 b₂ -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;