:: by Yatsuka Nakamura and Andrzej Trybulec

::

:: Received June 30, 2010

:: Copyright (c) 2010-2019 Association of Mizar Users

definition

let N be set ;

attr c_{2} 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_{2} -> Action of the InstructionsF of c_{2},(product ( the ValuesF of c_{2} * the Object-Kind of c_{2}));

end;
attr c

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

definition

let N be with_zero set ;

ex b_{1} being strict AMI-Struct over N st

( the carrier of b_{1} = {0} & the ZeroF of b_{1} = 0 & the InstructionsF of b_{1} = {[0,{},{}]} & the Object-Kind of b_{1} = 0 .--> 0 & the ValuesF of b_{1} = N --> NAT & the Execution of b_{1} = [0,{},{}] .--> (id (product ((N --> NAT) * (0 .--> 0)))) )

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

b_{1} = b_{2}
;

end;
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 ( 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)))) );

ex b

( the carrier of b

proof end;

uniqueness for b

b

:: deftheorem Def1 defines Trivial-AMI EXTPRO_1:def 1 :

for N being with_zero set

for b_{2} being strict AMI-Struct over N holds

( b_{2} = Trivial-AMI N iff ( the carrier of b_{2} = {0} & the ZeroF of b_{2} = 0 & the InstructionsF of b_{2} = {[0,{},{}]} & the Object-Kind of b_{2} = 0 .--> 0 & the ValuesF of b_{2} = N --> NAT & the Execution of b_{2} = [0,{},{}] .--> (id (product ((N --> NAT) * (0 .--> 0)))) ) );

for N being with_zero set

for b

( b

registration

let N be with_zero set ;

existence

not for b_{1} being AMI-Struct over N holds b_{1} is empty

end;
existence

not for b

proof end;

registration
end;

registration

let N be with_zero set ;

existence

ex b_{1} being AMI-Struct over N st

( b_{1} is with_non-empty_values & b_{1} is 1 -element )

end;
existence

ex b

( b

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

coherence

( the Execution of S . I) . s is State of S

end;
let S be with_non-empty_values AMI-Struct over N;

let I be Instruction of S;

let s be State of S;

coherence

( the Execution of S . I) . s is State of S

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

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

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

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

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 ;

existence

ex b_{1} being non empty with_non-empty_values AMI-Struct over N st b_{1} is halting

end;
existence

ex b

proof 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;
let S be with_non-empty_values halting AMI-Struct over N;

coherence

halt S is halting by Def4;

registration

let N be with_zero set ;

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

existence

ex b_{1} being Instruction of S st b_{1} is halting

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

existence

ex b

proof 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

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 M be with_zero set ;

existence

ex b_{1} being non empty with_non-empty_values AMI-Struct over M st

( b_{1} is IC-Ins-separated & b_{1} is strict & b_{1} is trivial )

end;
existence

ex b

( b

proof end;

registration

let N be with_zero set ;

ex b_{1} being 1 -element with_non-empty_values AMI-Struct over N st

( b_{1} is IC-Ins-separated & b_{1} is halting & b_{1} is strict )

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

existence ex b

( b

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

coherence

p /. (IC s) is Instruction of S ;

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

coherence

p /. (IC s) is Instruction of S ;

:: 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_{2} -valued Function

for s being State of S holds CurInstr (p,s) = p /. (IC s);

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

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;

correctness

coherence

Exec ((CurInstr (p,s)),s) is State of S;

;

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

correctness

coherence

Exec ((CurInstr (p,s)),s) is State of S;

;

:: 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_{2} -valued Function holds Following (p,s) = Exec ((CurInstr (p,s)),s);

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

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_{1}( 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;

ex b_{1} being State of S ex f being sequence of (product (the_Values_of S)) st

( b_{1} = f . k & f . 0 = s & ( for i being Nat holds f . (i + 1) = Following (p,(f . i)) ) )

for b_{1}, b_{2} being State of S st ex f being sequence of (product (the_Values_of S)) st

( b_{1} = 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_{2} = f . k & f . 0 = s & ( for i being Nat holds f . (i + 1) = Following (p,(f . i)) ) ) holds

b_{1} = b_{2}

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

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

ex b

( b

proof end;

uniqueness for b

( b

( b

b

proof 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_{2} -valued Function

for s being State of S

for k being Nat

for b_{6} being State of S holds

( b_{6} = Comput (p,s,k) iff ex f being sequence of (product (the_Values_of S)) st

( b_{6} = f . k & f . 0 = s & ( for i being Nat holds f . (i + 1) = Following (p,(f . i)) ) ) );

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

for s being State of S

for k being Nat

for b

( b

( b

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;

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

:: 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_{2} -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 ) );

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

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;

reducibility

Comput (p,s,0) = s

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

reducibility

Comput (p,s,0) = s

proof 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_{2} -valued Function

for s being State of S holds Comput (p,s,0) = s ;

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

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_{2} -valued Function

for s being State of S

for k being Nat holds Comput (p,s,(k + 1)) = Following (p,(Comput (p,s,k)))

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

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_{3} -valued Function

for k being Nat holds Comput (p,s,(i + k)) = Comput (p,(Comput (p,s,i)),k)

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

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_{4} -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)

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

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 ;

for b_{1}, b_{2} being State of S st ex k being Nat st

( b_{1} = Comput (p,s,k) & CurInstr (p,b_{1}) = halt S ) & ex k being Nat st

( b_{2} = Comput (p,s,k) & CurInstr (p,b_{2}) = halt S ) holds

b_{1} = b_{2}

existence

ex b_{1} being State of S ex k being Nat st

( b_{1} = Comput (p,s,k) & CurInstr (p,b_{1}) = halt S );

by A1;

end;
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 ex k being Nat st

( it = Comput (p,s,k) & CurInstr (p,it) = halt S );

for b

( b

( b

b

proof end;

correctness existence

ex b

( b

by A1;

:: 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_{2} -valued Function

for s being State of S st p halts_on s holds

for b_{5} being State of S holds

( b_{5} = Result (p,s) iff ex k being Nat st

( b_{5} = Comput (p,s,k) & CurInstr (p,b_{5}) = halt S ) );

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

for s being State of S st p halts_on s holds

for b

( b

( b

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

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)

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

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;

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

:: 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_{2} -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) );

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

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;

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

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;

:: 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_{2} -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 );

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

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 b_{1} being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N st

( b_{1} is halting & b_{1} is strict )

end;
existence

ex b

( b

proof 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_{2} -valued Function st l .--> I c= P holds

for s being State of S st (IC ) .--> l c= s holds

CurInstr (P,s) = I

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

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_{2} -valued Function st l .--> (halt S) c= P holds

for p being b_{3} -started PartState of S holds p is P -halted

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

for p being b

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_{2} -valued Function st l .--> (halt S) c= P holds

for p being b_{3} -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

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

for p being b

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_{2} -valued Function st l .--> (halt S) c= P holds

for p being b_{3} -started PartState of S holds p is P -autonomic

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

for p being b

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;

ex b_{1} being FinPartState of S st

( b_{1} is P -autonomic & b_{1} is P -halted & not b_{1} is empty )

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

( b

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 non halt-free Function;

ex b_{1} being FinPartState of S st

( b_{1} is P -autonomic & b_{1} is P -halted )

end;
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 ( it is P -autonomic & it is P -halted );

ex b

( b

proof 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_{2} -valued non halt-free Function

for b_{4} being FinPartState of S holds

( b_{4} is Autonomy of P iff ( b_{4} is P -autonomic & b_{4} is P -halted ) );

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

for b

( b

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 ;

ex b_{1} 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_{1} = (Result (P,s)) | (dom d)

uniqueness

for b_{1}, b_{2} 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_{1} = (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_{2} = (Result (P,s)) | (dom d) ) holds

b_{1} = b_{2};

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

ex b

for P being Instruction-Sequence of S st p c= P holds

for s being State of S st d c= s holds

b

proof end;

correctness uniqueness

for b

for s being State of S st d c= s holds

b

for s being State of S st d c= s holds

b

b

proof 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_{2} -valued non halt-free Function

for d being FinPartState of S st d is Autonomy of p holds

for b_{5} being FinPartState of S holds

( b_{5} = 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_{5} = (Result (P,s)) | (dom d) );

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

for d being FinPartState of S st d is Autonomy of p holds

for b

( b

for s being State of S st d c= s holds

b

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;

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

:: 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_{2} -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)) ) );

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

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_{2} -valued non halt-free Function

for d being FinPartState of S holds p,d computes {} ;

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

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_{2} -valued non halt-free Function

for d being FinPartState of S holds

( d is Autonomy of p iff p,d computes {} .--> (Result (p,d)) )

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

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_{2} -valued non halt-free Function

for d being FinPartState of S holds

( d is Autonomy of p iff p,d computes {} .--> {} )

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

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 ;

existence

ex b_{1} being non empty AMI-Struct over N st b_{1} is IC-Ins-separated

end;
existence

ex b

proof 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_{2} -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)) )

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

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_{2} -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)) )

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

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_{2} -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)

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

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_{4} -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))

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

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_{4} -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)

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

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;

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 ;

ex b_{1} being Nat st

( CurInstr (p,(Comput (p,s,b_{1}))) = halt S & ( for k being Nat st CurInstr (p,(Comput (p,s,k))) = halt S holds

b_{1} <= k ) )

for b_{1}, b_{2} being Nat st CurInstr (p,(Comput (p,s,b_{1}))) = halt S & ( for k being Nat st CurInstr (p,(Comput (p,s,k))) = halt S holds

b_{1} <= k ) & CurInstr (p,(Comput (p,s,b_{2}))) = halt S & ( for k being Nat st CurInstr (p,(Comput (p,s,k))) = halt S holds

b_{2} <= k ) holds

b_{1} = b_{2}

end;
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 ( CurInstr (p,(Comput (p,s,it))) = halt S & ( for k being Nat st CurInstr (p,(Comput (p,s,k))) = halt S holds

it <= k ) );

ex b

( CurInstr (p,(Comput (p,s,b

b

proof end;

uniqueness for b

b

b

b

proof 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_{2} -valued Function

for s being State of S st p halts_on s holds

for b_{5} being Nat holds

( b_{5} = LifeSpan (p,s) iff ( CurInstr (p,(Comput (p,s,b_{5}))) = halt S & ( for k being Nat st CurInstr (p,(Comput (p,s,k))) = halt S holds

b_{5} <= k ) ) );

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

for s being State of S st p halts_on s holds

for b

( b

b

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_{2} -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) )

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

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_{2} -valued Function

for s being State of S st p halts_on s holds

Result (p,s) = Comput (p,s,(LifeSpan (p,s)))

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

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)

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_{3} -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)))

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

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_{3} -started State of S

for u being Instruction-Sequence of S st e .--> I c= u holds

Following (u,t) = Exec (I,t)

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

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

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

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 )

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

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;

::$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 ) )

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

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

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)

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

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;