EXTPRO_1: Externally Programmed Machines

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

proof end;

end;

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

registration

let N be with_zero set ;

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

coherence by Def1;

end;

registration

let N be with_zero set ;

cluster non empty for AMI-Struct over N;

proof end;

end;

registration

let N be with_zero set ;

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

proof end;

end;

registration

let N be with_zero set ;

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

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;

proof end;

end;

:: deftheorem defines Exec EXTPRO_1:def 2 :

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 :

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 :

registration

let N be with_zero set ;

cluster Trivial-AMI N -> strict halting ;

proof end;

end;

registration

let N be with_zero set ;

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

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

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 ;

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;

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;

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

end;

:: deftheorem defines CurInstr EXTPRO_1:def 5 :

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

end;

:: deftheorem defines Following EXTPRO_1:def 6 :

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

proof end;

proof end;

end;

:: deftheorem Def7 defines Comput EXTPRO_1:def 7 :

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 :

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;

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

proof end;

correctness by A1;

end;

:: deftheorem Def9 defines Result EXTPRO_1:def 9 :

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 :

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 :

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;

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 ;

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

proof end;

end;

:: deftheorem Def12 defines Autonomy EXTPRO_1:def 12 :

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

proof end;

proof end;

end;

:: deftheorem defines Result EXTPRO_1:def 13 :

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 :

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;

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

proof end;

proof end;

end;

:: deftheorem Def15 defines LifeSpan EXTPRO_1:def 15 :

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;