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

definition

let N be set ;
attr c₂ 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 c₂ -> Action of the InstructionsF of c₂,(product ( the ValuesF of c₂ * the Object-Kind of c₂));

end;

definition

let N be with_zero set ;

func Trivial-AMI N -> strict AMI-Struct over N means :Def1: :: EXTPRO_1:def 1
( the carrier of it = {0} & the ZeroF of it = 0 & the InstructionsF of it = {[0,{},{}]} & the Object-Kind of it = 0 .--> 0 & the ValuesF of it = N --> NAT & the Execution of it = [0,{},{}] .--> (id (product ((N --> NAT) * (0 .--> 0)))) );

existence
ex b₁ being strict AMI-Struct over N st
( the carrier of b₁ = {0} & the ZeroF of b₁ = 0 & the InstructionsF of b₁ = {[0,{},{}]} & the Object-Kind of b₁ = 0 .--> 0 & the ValuesF of b₁ = N --> NAT & the Execution of b₁ = [0,{},{}] .--> (id (product ((N --> NAT) * (0 .--> 0)))) )

proof end;

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

end;

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

registration

let N be with_zero set ;

cluster Trivial-AMI N -> 1 -element strict ;

coherence
Trivial-AMI N is 1 -element by Def1;

end;

registration

let N be with_zero set ;

cluster non empty for AMI-Struct over N;

existence
not for b₁ being AMI-Struct over N holds b₁ is empty

proof end;

end;

registration

let N be with_zero set ;

cluster Trivial-AMI N -> with_non-empty_values strict ;

coherence
Trivial-AMI N is with_non-empty_values

proof end;

end;

registration

let N be with_zero set ;

cluster 1 -element with_non-empty_values for AMI-Struct over N;

existence
ex b₁ being AMI-Struct over N st
( b₁ is with_non-empty_values & b₁ 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 ;

cluster Trivial-AMI N -> strict halting ;

coherence
Trivial-AMI N is halting

proof end;

end;

registration

let N be with_zero set ;

cluster non empty with_non-empty_values halting for AMI-Struct over N;

existence
ex b₁ being non empty with_non-empty_values AMI-Struct over N st b₁ is halting

proof end;

end;

registration

let N be with_zero set ;
let S be with_non-empty_values halting AMI-Struct over N;

cluster halt S -> halting ;

coherence
halt S is halting by Def4;

end;

registration

let N be with_zero set ;
let S be with_non-empty_values halting AMI-Struct over N;

cluster halting for Element of the InstructionsF of S;

existence
ex b₁ being Instruction of S st b₁ is halting

proof end;

end;

theorem :: EXTPRO_1:1

for N being with_zero set
for s being State of (Trivial-AMI N)
for i being Instruction of (Trivial-AMI N) holds Exec (i,s) = s

proof end;

registration

let E be with_zero set ;

cluster Trivial-AMI E -> IC-Ins-separated strict ;

coherence
Trivial-AMI E is IC-Ins-separated

proof end;

end;

registration

let M be with_zero set ;

cluster non empty trivial with_non-empty_values IC-Ins-separated strict for AMI-Struct over M;

existence
ex b₁ being non empty with_non-empty_values AMI-Struct over M st
( b₁ is IC-Ins-separated & b₁ is strict & b₁ is trivial )

proof end;

end;

registration

let N be with_zero set ;

cluster non empty trivial V58() 1 -element with_non-empty_values IC-Ins-separated strict halting for AMI-Struct over N;

existence
ex b₁ being 1 -element with_non-empty_values AMI-Struct over N st
( b₁ is IC-Ins-separated & b₁ is halting & b₁ 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 b₂ -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 b₂ -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 H₁( set , State of S) -> Element of product (the_Values_of S) = down (Following (p,$2));
let s be State of S;
let k be Nat;

func Comput (p,s,k) -> State of S means :Def7: :: EXTPRO_1:def 7
ex f being sequence of (product (the_Values_of S)) st
( it = f . k & f . 0 = s & ( for i being Nat holds f . (i + 1) = Following (p,(f . i)) ) );

existence
ex b₁ being State of S ex f being sequence of (product (the_Values_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 sequence of (product (the_Values_of S)) st
( b₁ = f . k & f . 0 = s & ( for i being Nat holds f . (i + 1) = Following (p,(f . i)) ) ) & ex f being sequence of (product (the_Values_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 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 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 sequence of (product (the_Values_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 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 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 ) );

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 b₂ -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 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 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 b₃ -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 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_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 b₁, b₂ being State of S st ex k being Nat st
( b₁ = Comput (p,s,k) & CurInstr (p,b₁) = halt S ) & ex k being 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 Nat st
( b₁ = Comput (p,s,k) & CurInstr (p,b₁) = 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 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 Nat st
( b₅ = Comput (p,s,k) & CurInstr (p,b₅) = 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 b₂ -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 b₂ -valued Function
for IT being PartState of S holds
( IT is p -halted iff for s being State of S st IT c= s holds
for P being Instruction-Sequence of S st p c= P holds
P halts_on s );

registration

let N be non empty with_zero set ;

cluster non empty with_non-empty_values IC-Ins-separated strict halting for AMI-Struct over N;

existence
ex b₁ being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N st
( b₁ is halting & b₁ 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 b₂ -valued Function st l .--> I c= P holds
for s being State of S st (IC ) .--> l c= s holds
CurInstr (P,s) = I

proof 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 b₂ -valued Function st l .--> (halt S) c= P holds
for p being b₃ -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 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 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 b₂ -valued Function st l .--> (halt S) c= P holds
for p being b₃ -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;

cluster non empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible V39() countable P -autonomic P -halted for set ;

existence
ex b₁ being FinPartState of S st
( b₁ is P -autonomic & b₁ is P -halted & not b₁ 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 b₁ being FinPartState of S st
( b₁ is P -autonomic & b₁ 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 b₂ -valued non halt-free Function
for b₄ being FinPartState of S holds
( b₄ is Autonomy of P iff ( b₄ is P -autonomic & b₄ 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 b₁ 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
b₁ = (Result (P,s)) | (dom d)

proof end;

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

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 b₂ -valued non halt-free Function
for d being FinPartState of S st d is Autonomy of p holds
for b₅ being FinPartState of S holds
( b₅ = 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
b₅ = (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 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_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 b₂ -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 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_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 b₂ -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 b₁ being non empty AMI-Struct over N st b₁ 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 b₂ -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 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_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 b₂ -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 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 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 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_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 b₁ being Nat st
( CurInstr (p,(Comput (p,s,b₁))) = halt S & ( for k being Nat st CurInstr (p,(Comput (p,s,k))) = halt S holds
b₁ <= k ) )

proof end;

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

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 b₂ -valued Function
for s being State of S st p halts_on s holds
for b₅ being Nat holds
( b₅ = LifeSpan (p,s) iff ( CurInstr (p,(Comput (p,s,b₅))) = halt S & ( for k being Nat st CurInstr (p,(Comput (p,s,k))) = halt S holds
b₅ <= 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 b₂ -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 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_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 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_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 b₃ -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 ) = 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;