:: Externally Programmed Machines
:: by Yatsuka Nakamura and Andrzej Trybulec
::
:: Copyright (c) 2010-2018 Association of Mizar Users

definition
let N be set ;
attr c2 is strict ;
struct AMI-Struct over N -> Mem-Struct over N, COM-Struct ;
aggr AMI-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 = & the ZeroF of it = 0 & the InstructionsF of it = & the Object-Kind of it = 0 .--> 0 & the ValuesF of it = N --> NAT & the Execution of it = [0,{},{}] .--> (id (product (() * ()))) );
existence
ex b1 being strict AMI-Struct over N st
( the carrier of b1 = & the ZeroF of b1 = 0 & the InstructionsF of b1 = & the Object-Kind of b1 = 0 .--> 0 & the ValuesF of b1 = N --> NAT & the Execution of b1 = [0,{},{}] .--> (id (product (() * ()))) )
proof end;
uniqueness
for b1, b2 being strict AMI-Struct over N st the carrier of b1 = & the ZeroF of b1 = 0 & the InstructionsF of b1 = & the Object-Kind of b1 = 0 .--> 0 & the ValuesF of b1 = N --> NAT & the Execution of b1 = [0,{},{}] .--> (id (product (() * ()))) & the carrier of b2 = & the ZeroF of b2 = 0 & the InstructionsF of b2 = & the Object-Kind of b2 = 0 .--> 0 & the ValuesF of b2 = N --> NAT & the Execution of b2 = [0,{},{}] .--> (id (product (() * ()))) 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 = & the ZeroF of b2 = 0 & the InstructionsF of b2 = & the Object-Kind of b2 = 0 .--> 0 & the ValuesF of b2 = N --> NAT & the Execution of b2 = [0,{},{}] .--> (id (product (() * ()))) ) );

registration
let N be with_zero set ;
coherence
Trivial-AMI N is 1 -element
by Def1;
end;

registration
let N be with_zero set ;
cluster non empty for AMI-Struct over N;
existence
not for b1 being AMI-Struct over N holds b1 is empty
proof end;
end;

registration
let N be with_zero set ;
coherence
proof end;
end;

registration
let N be with_zero set ;
existence
ex b1 being AMI-Struct over N st
( b1 is with_non-empty_values & b1 is 1 -element )
proof end;
end;

definition
let N be with_zero set ;
let S be with_non-empty_values AMI-Struct over N;
let I be Instruction of S;
let s be State of S;
func Exec (I,s) -> State of S equals :: EXTPRO_1:def 2
( the Execution of S . I) . s;
coherence
( the Execution of S . I) . s is State of S
proof end;
end;

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

definition
let N be with_zero set ;
let S be with_non-empty_values AMI-Struct over N;
let I be Instruction of S;
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_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;
attr S 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 ;
coherence
proof end;
end;

registration
let N be with_zero set ;
existence
ex b1 being non empty with_non-empty_values AMI-Struct over N st b1 is halting
proof end;
end;

registration
let N be with_zero set ;
let S be with_non-empty_values halting AMI-Struct over N;
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 Instruction of S;
existence
ex b1 being Instruction of S st b1 is halting
proof end;
end;

theorem :: EXTPRO_1:1
for N being with_zero set
for s being State of ()
for i being Instruction of () holds Exec (i,s) = s
proof end;

registration
let E be with_zero set ;
coherence
proof end;
end;

registration
let M be with_zero set ;
existence
ex b1 being non empty with_non-empty_values AMI-Struct over M st
( b1 is IC-Ins-separated & b1 is strict & b1 is trivial )
proof end;
end;

registration
let N be with_zero set ;
existence
ex b1 being 1 -element with_non-empty_values AMI-Struct over N st
( b1 is IC-Ins-separated & b1 is halting & b1 is strict )
proof end;
end;

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 () = 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 sequence of () 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 sequence of () 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 sequence of () st ( b1 = f . k & f . 0 = s & ( for i being Nat holds f . (i + 1) = Following (p,(f . i)) ) ) & ex f being sequence of () 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 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 sequence of () 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; pred p halts_on s means :: 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 defines halts_on EXTPRO_1:def 8 : for N being with_zero set for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N for p being NAT -defined the InstructionsF of b2 -valued Function for s being State of S holds ( p halts_on s iff ex k being Nat st ( IC (Comput (p,s,k)) in dom p & CurInstr (p,(Comput (p,s,k))) = halt S ) ); registration let N be non empty with_zero set ; let S be non empty with_non-empty_values IC-Ins-separated AMI-Struct over N; let p be NAT -defined the InstructionsF of S -valued Function; let s be State of S; reduce Comput (p,s,0) to s; reducibility Comput (p,s,0) = s proof end; end; theorem :: EXTPRO_1:2 for N being non empty with_zero set for S being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N for p being NAT -defined the InstructionsF of b2 -valued Function for s being State of S holds Comput (p,s,0) = s ; theorem Th3: :: EXTPRO_1:3 for N being non empty with_zero set for S being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N for p being NAT -defined the InstructionsF of b2 -valued Function for s being State of S for k being Nat holds Comput (p,s,(k + 1)) = Following (p,(Comput (p,s,k))) proof end; theorem Th4: :: EXTPRO_1:4 for i being 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 Nat holds Comput (p,s,(i + k)) = Comput (p,(Comput (p,s,i)),k) proof end; theorem Th5: :: EXTPRO_1:5 for i, j being Nat st i <= j holds for N being non empty with_zero set for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N for p being NAT -defined the InstructionsF of b4 -valued Function for s being State of S st CurInstr (p,(Comput (p,s,i))) = halt S holds Comput (p,s,j) = Comput (p,s,i) proof end; definition let N be non empty with_zero set ; let S be non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N; let p be NAT -defined the InstructionsF of S -valued Function; let s be State of S; assume A1: p halts_on s ; func Result (p,s) -> State of S means :Def9: :: EXTPRO_1:def 9 ex k being Nat st ( it = Comput (p,s,k) & CurInstr (p,it) = halt S ); uniqueness for b1, b2 being State of S st ex k being Nat st ( b1 = Comput (p,s,k) & CurInstr (p,b1) = halt S ) & ex k being 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 Nat st ( b1 = Comput (p,s,k) & CurInstr (p,b1) = halt S ) ; by A1; 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 Nat st ( b5 = Comput (p,s,k) & CurInstr (p,b5) = halt S ) ); theorem :: EXTPRO_1:6 for k being Nat for N being non empty with_zero set for S being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N for P being Instruction-Sequence of S for s being State of S holds Comput (P,s,(k + 1)) = Exec ((P . (IC (Comput (P,s,k)))),(Comput (P,s,k))) proof end; theorem Th7: :: EXTPRO_1:7 for N being non empty with_zero set for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N for P being Instruction-Sequence of S for s being State of S for k being Nat st P . (IC (Comput (P,s,k))) = halt S holds Result (P,s) = Comput (P,s,k) proof end; theorem Th8: :: EXTPRO_1:8 for N being non empty with_zero set for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N for P being Instruction-Sequence of S for s being State of S st ex k being Nat st P . (IC (Comput (P,s,k))) = halt S holds for i being Nat holds Result (P,s) = Result (P,(Comput (P,s,i))) proof end; definition let N be non empty with_zero set ; let S be non empty with_non-empty_values IC-Ins-separated AMI-Struct over N; let p be NAT -defined the InstructionsF of S -valued Function; let IT be PartState of S; attr IT is p -autonomic means :: EXTPRO_1:def 10 for P, Q being Instruction-Sequence of S st p c= P & p c= Q holds for s1, s2 being State of S st IT c= s1 & IT c= s2 holds for i being Nat holds (Comput (P,s1,i)) | (dom IT) = (Comput (Q,s2,i)) | (dom IT); end; :: deftheorem defines -autonomic EXTPRO_1:def 10 : for N being non empty with_zero set for S being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N for p being NAT -defined the InstructionsF of b2 -valued Function for IT being PartState of S holds ( IT is p -autonomic iff for P, Q being Instruction-Sequence of S st p c= P & p c= Q holds for s1, s2 being State of S st IT c= s1 & IT c= s2 holds for i being 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; attr IT is p -halted means :: 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 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 ; existence ex b1 being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N st ( b1 is halting & b1 is strict ) proof end; end; 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 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 () .--> l c= s holds CurInstr (P,s) = I proof end; theorem Th10: :: EXTPRO_1:10 for N being non empty with_zero set for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N for l being Nat for P being NAT -defined the InstructionsF of b2 -valued Function st l .--> (halt S) c= P holds for p being b3 -started PartState of S holds p is P -halted proof end; theorem Th11: :: EXTPRO_1:11 for N being non empty with_zero set for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N for l being 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 Nat holds Comput (P,s,i) = s proof end; theorem Th12: :: EXTPRO_1:12 for N being non empty with_zero set for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N for l being Nat for P being NAT -defined the InstructionsF of b2 -valued Function st l .--> (halt S) c= P holds for p being b3 -started PartState of S holds p is P -autonomic proof end; registration let N be non empty with_zero set ; let S be non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N; let P be NAT -defined the InstructionsF of S -valued non halt-free Function; existence ex b1 being FinPartState of S st ( b1 is P -autonomic & b1 is P -halted & not b1 is empty ) proof end; end; definition let N be non empty with_zero set ; let S be non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N; let P be NAT -defined the InstructionsF of S -valued non halt-free Function; mode Autonomy of P -> FinPartState of S means :Def12: :: EXTPRO_1:def 12 ( it is P -autonomic & it is P -halted ); existence ex b1 being FinPartState of S st ( b1 is P -autonomic & b1 is P -halted ) proof end; end; :: deftheorem Def12 defines Autonomy EXTPRO_1:def 12 : for N being non empty with_zero set for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N for P being NAT -defined the InstructionsF of b2 -valued non halt-free Function for b4 being FinPartState of S holds ( b4 is Autonomy of P iff ( b4 is P -autonomic & b4 is P -halted ) ); definition let N be non empty with_zero set ; let S be non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N; let p be NAT -defined the InstructionsF of S -valued non halt-free Function; let d be FinPartState of S; assume A1: d is Autonomy of p ; func Result (p,d) -> FinPartState of S means :: EXTPRO_1:def 13 for P being Instruction-Sequence of S st p c= P holds for s being State of S st d c= s holds it = (Result (P,s)) | (dom d); existence ex b1 being FinPartState of S st for P being Instruction-Sequence of S st p c= P holds for s being State of S st d c= s holds b1 = (Result (P,s)) | (dom d) proof end; correctness uniqueness for b1, b2 being FinPartState of S st ( for P being Instruction-Sequence of S st p c= P holds for s being State of S st d c= s holds b1 = (Result (P,s)) | (dom d) ) & ( for P being Instruction-Sequence of S st p c= P holds for s being State of S st d c= s holds b2 = (Result (P,s)) | (dom d) ) holds b1 = b2 ; proof end; end; :: deftheorem defines Result EXTPRO_1:def 13 : for N being non empty with_zero set for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N for p being NAT -defined the InstructionsF of b2 -valued non halt-free Function for d being FinPartState of S st d is Autonomy of p holds for b5 being FinPartState of S holds ( b5 = Result (p,d) iff for P being Instruction-Sequence of S st p c= P holds for s being State of S st d c= s holds b5 = (Result (P,s)) | (dom d) ); 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; pred p,d computes F means :: EXTPRO_1:def 14 for x being set st x in dom F holds ex s being FinPartState of S st ( x = s & d +* s is Autonomy of p & F . s c= Result (p,(d +* s)) ); end; :: deftheorem defines computes EXTPRO_1:def 14 : for N being non empty with_zero set for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N for p being NAT -defined the InstructionsF of b2 -valued non halt-free Function for d being FinPartState of S for F being Function holds ( p,d computes F iff for x being set st x in dom F holds ex s being FinPartState of S st ( x = s & d +* s is Autonomy of p & F . s c= Result (p,(d +* s)) ) ); theorem :: EXTPRO_1:13 for N being non empty with_zero set for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N for p being NAT -defined the InstructionsF of b2 -valued non halt-free Function for d being FinPartState of S holds p,d computes {} ; theorem :: EXTPRO_1:14 for N being non empty with_zero set for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N for p being NAT -defined the InstructionsF of b2 -valued non halt-free Function for d being FinPartState of S holds ( d is Autonomy of p iff p,d computes {} .--> (Result (p,d)) ) proof end; theorem :: EXTPRO_1:15 for N being non empty with_zero set for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N for p being NAT -defined the InstructionsF of b2 -valued non halt-free Function for d being FinPartState of S holds ( d is Autonomy of p iff p,d computes {} .--> {} ) proof end; registration let N be non empty with_zero set ; cluster non empty IC-Ins-separated for AMI-Struct over N; existence ex b1 being non empty AMI-Struct over N st b1 is IC-Ins-separated proof end; end; 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 Nat st p halts_at IC (Comput (p,s,i)) ) proof end; theorem Th17: :: EXTPRO_1:17 for N being non empty with_zero set for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N for p being NAT -defined the InstructionsF of b2 -valued Function for s being State of S for k being Nat st p halts_on s holds ( Result (p,s) = Comput (p,s,k) iff p halts_at IC (Comput (p,s,k)) ) proof end; theorem Th18: :: EXTPRO_1:18 for N being non empty with_zero set for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N for P being NAT -defined the InstructionsF of b2 -valued Function for s being State of S for k being 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 Nat for N being non empty with_zero set st i <= j holds for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N for P being NAT -defined the InstructionsF of b4 -valued Function for s being State of S st P halts_at IC (Comput (P,s,i)) holds P halts_at IC (Comput (P,s,j)) proof end; theorem :: EXTPRO_1:20 for i, j being Nat for N being non empty with_zero set st i <= j holds for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N for P being NAT -defined the InstructionsF of b4 -valued Function for s being State of S st P halts_at IC (Comput (P,s,i)) holds Comput (P,s,j) = Comput (P,s,i) proof end; theorem :: EXTPRO_1:21 for N being non empty with_zero set for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N for P being Instruction-Sequence of S for s being State of S st ex k being Nat st P halts_at IC (Comput (P,s,k)) holds for i being Nat holds Result (P,s) = Result (P,(Comput (P,s,i))) by Th8; 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 LifeSpan (p,s) -> Nat means :Def15: :: EXTPRO_1:def 15 ( CurInstr (p,(Comput (p,s,it))) = halt S & ( for k being Nat st CurInstr (p,(Comput (p,s,k))) = halt S holds it <= k ) ); existence ex b1 being Nat st ( CurInstr (p,(Comput (p,s,b1))) = halt S & ( for k being Nat st CurInstr (p,(Comput (p,s,k))) = halt S holds b1 <= k ) ) proof end; uniqueness for b1, b2 being Nat st CurInstr (p,(Comput (p,s,b1))) = halt S & ( for k being Nat st CurInstr (p,(Comput (p,s,k))) = halt S holds b1 <= k ) & CurInstr (p,(Comput (p,s,b2))) = halt S & ( for k being Nat st CurInstr (p,(Comput (p,s,k))) = halt S holds b2 <= k ) holds b1 = b2 proof end; end; :: deftheorem Def15 defines LifeSpan EXTPRO_1:def 15 : for N being non empty with_zero set for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N for p being NAT -defined the InstructionsF of b2 -valued Function for s being State of S st p halts_on s holds for b5 being Nat holds ( b5 = LifeSpan (p,s) iff ( CurInstr (p,(Comput (p,s,b5))) = halt S & ( for k being 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 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_zero set for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N for p being NAT -defined the InstructionsF of b2 -valued Function for s being State of S st p halts_on s holds Result (p,s) = Comput (p,s,(LifeSpan (p,s))) proof end; theorem :: EXTPRO_1:24 for N being non empty with_zero set for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N for P being Instruction-Sequence of S for s being State of S for k being 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 Nat for N being non empty with_zero set for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N for p being NAT -defined the InstructionsF of b3 -valued Function for s being State of S st LifeSpan (p,s) <= j & p halts_on s holds Comput (p,s,j) = Comput (p,s,(LifeSpan (p,s))) proof end; theorem :: EXTPRO_1:26 for N being non empty with_zero set for S being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N for e being Nat for I being Instruction of S for t being b3 -started State of S for u being Instruction-Sequence of S st e .--> I c= u holds Following (u,t) = Exec (I,t) proof end; theorem :: EXTPRO_1:27 for N being non empty with_zero set for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N for P being Instruction-Sequence of S for s being State of S st s = Following (P,s) holds for n being Nat holds Comput (P,s,n) = s proof end; theorem :: EXTPRO_1:28 for N being non empty with_zero set for S being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N for P being Instruction-Sequence of S for s being State of S for i being Instruction of S holds (Exec ((P . (IC s)),s)) . () = IC (Following (P,s)) proof end; theorem :: EXTPRO_1:29 for N being non empty with_zero set for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N for P being Instruction-Sequence of S for s being State of S holds ( P halts_on s iff ex k being Nat st CurInstr (P,(Comput (P,s,k))) = halt S ) proof end; theorem Th30: :: EXTPRO_1:30 for N being non empty with_zero set for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N for F being Instruction-Sequence of S for s being State of S st ex k being Nat st F . (IC (Comput (F,s,k))) = halt S holds F halts_on s proof end; theorem :: EXTPRO_1:31 canceled; ::$CT
theorem Th31: :: 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 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: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 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: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 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: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 Nat st F halts_on Comput (F,s,k) holds
Result (F,(Comput (F,s,k))) = Result (F,s)
proof end;

theorem :: EXTPRO_1:36
for N being non empty with_zero set
for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N
for P being Instruction-Sequence of S
for s being State of S st P halts_on s holds
for k being Nat st LifeSpan (P,s) <= k holds
CurInstr (P,(Comput (P,s,k))) = halt S
proof end;