AMISTD_1: Standard Ordering of Instruction Locations

:: Standard Ordering of Instruction Locations
:: by Andrzej Trybulec , Piotr Rudnicki and Artur Korni{\l}owicz
::
:: Received April 14, 2000
:: Copyright (c) 2000-2012 Association of Mizar Users

begin

registration

let N be with_zero set ;
let S be with_non-empty_values AMI-Struct over N;
let i be Element of the InstructionsF of S;
let s be State of S;

cluster ( the Execution of S . i) . s -> Relation-like Function-like ;

coherence

proof end;

end;

registration

let N be with_zero set ;

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

existence

proof end;

end;

definition

let N be with_zero set ;
let S be non empty with_non-empty_values AMI-Struct over N;
let T be InsType of the InstructionsF of S;

attr T is jump-only means :: AMISTD_1:def 1
for s being State of S
for o being Object of S
for I being Instruction of S st InsCode I = T & o in Data-Locations holds
(Exec (I,s)) . o = s . o;

end;

:: deftheorem defines jump-only AMISTD_1:def 1 :

definition

let N be with_zero set ;
let S be non empty with_non-empty_values AMI-Struct over N;
let I be Instruction of S;

attr I is jump-only means :: AMISTD_1:def 2
InsCode I is jump-only ;

end;

:: deftheorem defines jump-only AMISTD_1:def 2 :

definition

let N be with_zero set ;
let S be non empty with_non-empty_values IC-Ins-separated AMI-Struct over N;
let l be Nat;
let i be Element of the InstructionsF of S;

func NIC (i,l) -> Subset of NAT equals :: AMISTD_1:def 3
{ (IC (Exec (i,ss))) where ss is Element of product (the_Values_of S) : IC ss = l } ;

coherence

proof end;

end;

:: deftheorem defines NIC AMISTD_1:def 3 :

Lm1: now :: thesis:

let N be with_zero set ; :: thesis:
let S be non empty with_non-empty_values IC-Ins-separated AMI-Struct over N; :: thesis:
let i be Element of the InstructionsF of S; :: thesis:
let l be Element of NAT ; :: thesis:
let s be State of S; :: thesis:
let P be Instruction-Sequence of S; :: thesis:
reconsider t = s +* ((IC ),l) as Element of product (the_Values_of S) by CARD_3:107;
l in NAT ;
then A1: l in dom P by PARTFUN1:def 2;
IC in dom s by MEMSTR_0:2;
then A2: IC t = l by FUNCT_7:31;
then CurInstr ((P +* (l,i)),t) = (P +* (l,i)) . l by PBOOLE:143
.= i by A1, FUNCT_7:31 ;
hence IC (Following ((P +* (l,i)),(s +* ((IC ),l)))) in NIC (i,l) by A2; :: thesis:

end;

registration

let N be with_zero set ;
let S be non empty with_non-empty_values IC-Ins-separated AMI-Struct over N;
let i be Element of the InstructionsF of S;
let l be Element of NAT ;

cluster NIC (i,l) -> non empty ;

coherence by Lm1;

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 i be Element of the InstructionsF of S;

func JUMP i -> Subset of NAT equals :: AMISTD_1:def 4
meet { (NIC (i,l)) where l is Element of NAT : verum } ;

coherence

proof end;

end;

:: deftheorem defines JUMP AMISTD_1:def 4 :

definition

let N be with_zero set ;
let S be non empty with_non-empty_values IC-Ins-separated AMI-Struct over N;
let l be Nat;

func SUCC (l,S) -> Subset of NAT equals :: AMISTD_1:def 5
union { ((NIC (i,l)) \ (JUMP i)) where i is Element of the InstructionsF of S : verum } ;

coherence

proof end;

end;

:: deftheorem defines SUCC AMISTD_1:def 5 :

theorem Th1: :: AMISTD_1:1

for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N
for i being Element of the InstructionsF of S st ( for l being Element of NAT holds NIC (i,l) = {l} ) holds
JUMP i is empty

proof end;

theorem Th2: :: AMISTD_1:2

for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N
for il being Element of NAT
for i being Instruction of S st i is halting holds
NIC (i,il) = {il}

proof end;

begin

definition

let N be with_zero set ;
let S be non empty with_non-empty_values IC-Ins-separated AMI-Struct over N;

attr S is standard means :Def6: :: AMISTD_1:def 6
for m, n being Element of NAT holds
( m <= n iff ex f being non empty FinSequence of NAT st
( f /. 1 = m & f /. (len f) = n & ( for n being Element of NAT st 1 <= n & n < len f holds
f /. (n + 1) in SUCC ((f /. n),S) ) ) );

end;

:: deftheorem Def6 defines standard AMISTD_1:def 6 :

Lm2: for k being Element of NAT
for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N ex f being non empty FinSequence of NAT st
( f /. 1 = k & f /. (len f) = k & ( for n being Element of NAT st 1 <= n & n < len f holds
f /. (n + 1) in SUCC ((f /. n),S) ) )

proof end;

theorem Th3: :: AMISTD_1:3

for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N holds
( S is standard iff for k being Element of NAT holds
( k + 1 in SUCC (k,S) & ( for j being Element of NAT st j in SUCC (k,S) holds
k <= j ) ) )

proof end;

set III = {[1,0,0],[0,0,0]};

begin

definition

let N be with_zero set ;

func STC N -> strict AMI-Struct over N means :Def7: :: AMISTD_1:def 7
( the carrier of it = {0} & the ZeroF of it = 0 & the InstructionsF of it = {[0,0,0],[1,0,0]} & the Object-Kind of it = 0 .--> 0 & the ValuesF of it = N --> NAT & ex f being Function of (product (the_Values_of it)),(product (the_Values_of it)) st
( ( for s being Element of product (the_Values_of it) holds f . s = s +* (0 .--> (succ (s . 0))) ) & the Execution of it = ([1,0,0] .--> f) +* ([0,0,0] .--> (id (product (the_Values_of it)))) ) );

existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def7 defines STC AMISTD_1:def 7 :

registration

let N be with_zero set ;

cluster STC N -> non empty finite strict ;

coherence by Def7;

end;

registration

let N be with_zero set ;

cluster STC N -> with_non-empty_values strict ;

coherence

proof end;

end;

registration

let N be with_zero set ;

cluster STC N -> IC-Ins-separated strict ;

coherence

proof end;

end;

Lm3: for N being with_zero set
for i being Instruction of (STC N)
for s being State of (STC N) st InsCode i = 1 holds
(Exec (i,s)) . (IC ) = succ (IC s)

proof end;

theorem Th4: :: AMISTD_1:4

for N being with_zero set
for i being Instruction of (STC N) st InsCode i = 0 holds
i is halting

proof end;

theorem :: AMISTD_1:5

for N being with_zero set
for i being Instruction of (STC N) st InsCode i = 1 holds
not i is halting

proof end;

theorem Th6: :: AMISTD_1:6

for N being with_zero set
for i being Element of the InstructionsF of (STC N) holds
( InsCode i = 1 or InsCode i = 0 )

proof end;

theorem :: AMISTD_1:7

for N being with_zero set
for i being Instruction of (STC N) holds i is jump-only

proof end;

registration

let N be with_zero set ;

cluster -> ins-loc-free for Element of the InstructionsF of (STC N);

coherence

proof end;

end;

Lm4: for z being Nat
for N being with_zero set
for l being Element of NAT
for i being Element of the InstructionsF of (STC N) st l = z & InsCode i = 1 holds
NIC (i,l) = {(z + 1)}

proof end;

Lm5: for N being with_zero set
for i being Element of the InstructionsF of (STC N) holds JUMP i is empty

proof end;

theorem Th8: :: AMISTD_1:8

for z being Nat
for N being with_zero set
for l being Element of NAT st l = z holds
SUCC (l,(STC N)) = {z,(z + 1)}

proof end;

registration

let N be with_zero set ;

cluster STC N -> strict standard ;

coherence

proof end;

end;

registration

let N be with_zero set ;

cluster STC N -> strict halting ;

coherence

proof end;

end;

registration

let N be with_zero set ;

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

existence

proof end;

end;

theorem :: AMISTD_1:9

for N being with_zero set
for i being Instruction of (STC N)
for s being State of (STC N) st InsCode i = 1 holds
(Exec (i,s)) . (IC ) = succ (IC s) by Lm3;

theorem :: AMISTD_1:10

for N being with_zero set
for l being Element of NAT
for i being Element of the InstructionsF of (STC N) st InsCode i = 1 holds
NIC (i,l) = {(succ l)} by Lm4;

theorem :: AMISTD_1:11

for N being with_zero set
for l being Element of NAT holds SUCC (l,(STC N)) = {l,(succ l)} by Th8;

definition

let N be with_zero set ;
let S be non empty with_non-empty_values IC-Ins-separated AMI-Struct over N;
let i be Instruction of S;

attr i is sequential means :: AMISTD_1:def 8
for s being State of S holds (Exec (i,s)) . (IC ) = succ (IC s);

end;

:: deftheorem defines sequential AMISTD_1:def 8 :

theorem Th12: :: AMISTD_1:12

for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N
for il being Element of NAT
for i being Instruction of S st i is sequential holds
NIC (i,il) = {(succ il)}

proof end;

registration

let N be with_zero set ;
let S be non empty with_non-empty_values IC-Ins-separated AMI-Struct over N;

cluster sequential -> non halting for Element of the InstructionsF of S;

coherence

proof end;

cluster halting -> non sequential for Element of the InstructionsF of S;

coherence ;

end;

theorem :: AMISTD_1:13

for N being with_zero set
for T being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N
for i being Instruction of T st not JUMP i is empty holds
not i is sequential

proof end;

begin

definition

let N be with_zero set ;
let S be non empty with_non-empty_values IC-Ins-separated AMI-Struct over N;
let F be preProgram of S;

attr F is really-closed means :Def9: :: AMISTD_1:def 9
for l being Element of NAT st l in dom F holds
NIC ((F /. l),l) c= dom F;

end;

:: deftheorem Def9 defines really-closed AMISTD_1:def 9 :

definition

let N be with_zero set ;
let S be non empty with_non-empty_values IC-Ins-separated AMI-Struct over N;
let F be NAT -defined the InstructionsF of S -valued Function;

attr F is paraclosed means :: AMISTD_1:def 10
for s being 0 -started State of S
for P being Instruction-Sequence of S st F c= P holds
for k being Element of NAT holds IC (Comput (P,s,k)) in dom F;

end;

:: deftheorem defines paraclosed AMISTD_1:def 10 :

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 F be NAT -defined the InstructionsF of S -valued Function;

attr F is parahalting means :: AMISTD_1:def 11
for s being 0 -started State of S
for P being Instruction-Sequence of S st F c= P holds
P halts_on s;

end;

:: deftheorem defines parahalting AMISTD_1:def 11 :

theorem Th14: :: AMISTD_1:14

for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N
for F being preProgram of S holds
( F is really-closed iff for s being State of S st IC s in dom F holds
for k being Element of NAT holds IC (Comput (F,s,k)) in dom F )

proof end;

Lm6: for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N
for F being preProgram of S holds
( F is really-closed iff for s being State of S st IC s in dom F holds
for P being Instruction-Sequence of S st F c= P holds
for k being Element of NAT holds IC (Comput (P,s,k)) in dom F )

proof end;

theorem Th15: :: AMISTD_1:15

for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated standard AMI-Struct over N
for F being NAT -defined the InstructionsF of b₂ -valued finite Function st F is really-closed & 0 in dom F holds
F is paraclosed

proof end;

theorem Th16: :: AMISTD_1:16

for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated halting standard AMI-Struct over N holds 0 .--> (halt S) is really-closed

proof end;

registration

let N be with_zero set ;
let S be non empty with_non-empty_values IC-Ins-separated standard AMI-Struct over N;

cluster Relation-like NAT -defined the InstructionsF of S -valued non empty Function-like finite initial really-closed -> NAT -defined the InstructionsF of S -valued finite paraclosed for set ;

coherence

proof end;

end;

Lm7: now :: thesis:

let N be with_zero set ; :: thesis:
let S be non empty with_non-empty_values IC-Ins-separated halting standard AMI-Struct over N; :: thesis:
set F = <%(halt S)%>;
A1: dom <%(halt S)%> = {0} by FUNCOP_1:13;
then A2: card (dom <%(halt S)%>) = 1 by CARD_1:30;
A3: LastLoc <%(halt S)%> = (card <%(halt S)%>) -' 1 by AFINSQ_1:70
.= 0 by A2, XREAL_1:232 ;
hence <%(halt S)%> . (LastLoc <%(halt S)%>) = halt S by FUNCOP_1:72; :: thesis:
let l be Nat; :: thesis:
assume <%(halt S)%> . l = halt S ; :: thesis:
assume l in dom <%(halt S)%> ; :: thesis:
hence l = LastLoc <%(halt S)%> by A1, A3, TARSKI:def 1; :: thesis:

end;

registration

let N be with_zero set ;
let S be non empty with_non-empty_values IC-Ins-separated halting standard AMI-Struct over N;

cluster Relation-like NAT -defined the InstructionsF of S -valued non empty trivial Function-like finite initial countable V139() really-closed for set ;

existence

proof end;

end;

registration

let N be with_zero set ;
let S be non empty with_non-empty_values IC-Ins-separated halting standard AMI-Struct over N;

cluster Relation-like NAT -defined the InstructionsF of S -valued T-Sequence-like non empty trivial Function-like finite initial halt-ending unique-halt countable V139() really-closed for set ;

existence

proof end;

end;

registration

let N be with_zero set ;
let S be non empty with_non-empty_values IC-Ins-separated halting standard AMI-Struct over N;

cluster Relation-like NAT -defined the InstructionsF of S -valued T-Sequence-like non empty Function-like finite initial halt-ending unique-halt countable V139() really-closed for set ;

existence

proof end;

end;

theorem :: AMISTD_1:17

for N being with_zero set
for i being Instruction of (Trivial-AMI N) holds i is halting

proof end;

theorem :: AMISTD_1:18

for N being with_zero set
for i being Element of the InstructionsF of (Trivial-AMI N) holds InsCode i = 0

proof end;

begin

:: from SCMPDS_9, 2008.03.10, A.T.

theorem :: AMISTD_1:19

for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N
for i being Instruction of S
for l being Element of NAT holds JUMP i c= NIC (i,l)

proof end;

theorem :: AMISTD_1:20

for N being with_zero set
for i being Instruction of (STC N)
for s being State of (STC N) st InsCode i = 1 holds
Exec (i,s) = IncIC (s,1)

proof end;

registration

let N be with_zero set ;
let p be PartState of (STC N);

cluster DataPart p -> empty ;

coherence

proof end;

end;

theorem :: AMISTD_1:21

for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N
for F being preProgram of S holds
( F is really-closed iff for s being State of S st IC s in dom F holds
for P being Instruction-Sequence of S st F c= P holds
for k being Element of NAT holds IC (Comput (P,s,k)) in dom F ) by Lm6;

registration

let N be with_zero set ;
let S be non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N;

cluster Relation-like NAT -defined the InstructionsF of S -valued non empty Function-like finite non halt-free countable V139() parahalting for set ;

existence

proof end;

end;