:: On the Composition of Macro Instructions of Standard Computers
:: by Artur Korni{\l}owicz
::
:: Received April 14, 2000
:: Copyright (c) 2000-2012 Association of Mizar Users


begin

theorem :: AMISTD_2:1
for N being with_zero set
for I being Instruction of (STC N) holds JumpPart I = 0 ;

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;
attrI is with_explicit_jumps  means :Def1: :: AMISTD_2:def 1
 JUMP I = rng (JumpPart I);
end;

:: deftheorem Def1 defines with_explicit_jumps AMISTD_2:def_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 Instruction of S holds
( I is with_explicit_jumps iff JUMP I = rng (JumpPart I) );

definition
let N be with_zero set ;
let S be non empty with_non-empty_values IC-Ins-separated AMI-Struct over N;
attrS is with_explicit_jumps  means :Def2: :: AMISTD_2:def 2
 for I being Instruction of S holds I is with_explicit_jumps ;
end;

:: deftheorem Def2 defines with_explicit_jumps AMISTD_2:def_2_:_
 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 with_explicit_jumps iff for I being Instruction of S holds I is with_explicit_jumps );

registration
let N be with_zero set ;
cluster non empty with_non-empty_values IC-Ins-separated standard for AMI-Struct over N;
existence
 ex b1 being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N st b1 is standard
proofend;
end;

theorem Th2: :: AMISTD_2:2
for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated standard AMI-Struct over N
for I being Instruction of S st ( for f being Element of NAT holds NIC (I,f) = {(succ f)} ) holds
JUMP I is empty
proofend;

registration
let N be with_zero set ;
let I be Instruction of (STC N);
cluster JUMP I ->  empty ;
coherence
 JUMP I is empty
proofend;
end;

theorem :: AMISTD_2:3
for N being with_zero set
for T being InsType of the InstructionsF of (STC N) holds JumpParts T = {0}
proofend;

Lm1:  for N being with_zero set
for I being Instruction of (Trivial-AMI N) holds JumpPart I = 0
proofend;

Lm2:  for N being with_zero set
for T being InsType of the InstructionsF of (Trivial-AMI N) holds JumpParts T = {0}
proofend;

registration
let N be with_zero set ;
cluster STC N ->  with_explicit_jumps ;
coherence
 STC N is with_explicit_jumps
proofend;
end;

registration
let N be with_zero set ;
cluster non empty with_non-empty_values IC-Ins-separated halting standard with_explicit_jumps for AMI-Struct over N;
existence
 ex b1 being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N st
( b1 is standard & b1 is halting & b1 is with_explicit_jumps )
proofend;
end;

registration
let N be with_zero set ;
let I be Instruction of (Trivial-AMI N);
cluster JUMP I ->  empty ;
coherence
 JUMP I is empty
proofend;
end;

registration
let N be with_zero set ;
cluster Trivial-AMI N ->  with_explicit_jumps ;
coherence
 Trivial-AMI N is with_explicit_jumps
proofend;
end;

registration
let N be with_zero set ;
cluster non empty with_non-empty_values IC-Ins-separated halting with_explicit_jumps for AMI-Struct over N;
existence
 ex b1 being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N st
( b1 is with_explicit_jumps & b1 is halting )
proofend;
end;

registration
let N be with_zero set ;
let S be non empty with_non-empty_values IC-Ins-separated with_explicit_jumps AMI-Struct over N;
cluster  ->  with_explicit_jumps for Element of the InstructionsF of S;
coherence
 for b1 being Instruction of S holds b1 is with_explicit_jumps by Def2;
end;

theorem Th4: :: AMISTD_2:4
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 st I is halting holds
JUMP I is empty
proofend;

registration
let N be with_zero set ;
let S be non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N;
let I be halting Instruction of S;
cluster JUMP I ->  empty ;
coherence
 JUMP I is empty by Th4;
end;

theorem :: AMISTD_2:5
for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated halting with_explicit_jumps AMI-Struct over N
for I being Instruction of S st I is ins-loc-free holds
JUMP I is empty
proofend;

registration
let N be with_zero set ;
let S be non empty with_non-empty_values IC-Ins-separated with_explicit_jumps AMI-Struct over N;
cluster halting  ->  ins-loc-free for Element of the InstructionsF of S;
coherence
 for b1 being Instruction of S st b1 is halting holds
b1 is ins-loc-free
proofend;
end;

registration
let N be with_zero set ;
let S be non empty with_non-empty_values IC-Ins-separated with_explicit_jumps AMI-Struct over N;
cluster sequential  ->  ins-loc-free for Element of the InstructionsF of S;
coherence
 for b1 being Instruction of S st b1 is sequential holds
b1 is ins-loc-free
proofend;
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 Stop S ->  really-closed ;
coherence
 Stop S is really-closed by AMISTD_1:16;
end;

begin

registration
let N be with_zero set ;
let S be non empty with_non-empty_values IC-Ins-separated halting with_explicit_jumps AMI-Struct over N;
let I be halting Instruction of S;
let k be Nat;
cluster IncAddr (I,k) ->  halting ;
coherence
 IncAddr (I,k) is halting by COMPOS_0:4;
end;

theorem :: AMISTD_2:6
for k being Nat
for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated halting standard with_explicit_jumps AMI-Struct over N
for I being Instruction of S st I is sequential holds
IncAddr (I,k) is sequential by COMPOS_0:4;

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 I be Instruction of S;
attrI is IC-relocable  means :Def3: :: AMISTD_2:def 3
 for j, k being Nat
for s being State of S holds (IC (Exec ((IncAddr (I,j)),s))) + k = IC (Exec ((IncAddr (I,(j + k))),(IncIC (s,k))));
end;

:: deftheorem Def3 defines IC-relocable AMISTD_2:def_3_:_
 for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N
for I being Instruction of S holds
( I is IC-relocable iff for j, k being Nat
for s being State of S holds (IC (Exec ((IncAddr (I,j)),s))) + k = IC (Exec ((IncAddr (I,(j + k))),(IncIC (s,k)))) );

definition
let N be with_zero set ;
let S be non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N;
attrS is IC-relocable  means :Def4: :: AMISTD_2:def 4
 for I being Instruction of S holds I is IC-relocable ;
end;

:: deftheorem Def4 defines IC-relocable AMISTD_2:def_4_:_
 for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N holds
( S is IC-relocable iff for I being Instruction of S holds I is IC-relocable );

registration
let N be with_zero set ;
let S be non empty with_non-empty_values IC-Ins-separated halting with_explicit_jumps AMI-Struct over N;
cluster sequential  ->  IC-relocable for Element of the InstructionsF of S;
coherence
 for b1 being Instruction of S st b1 is sequential holds
b1 is IC-relocable
proofend;
end;

registration
let N be with_zero set ;
let S be non empty with_non-empty_values IC-Ins-separated halting with_explicit_jumps AMI-Struct over N;
cluster halting  ->  IC-relocable for Element of the InstructionsF of S;
coherence
 for b1 being Instruction of S st b1 is halting holds
b1 is IC-relocable
proofend;
end;

registration
let N be with_zero set ;
cluster STC N ->  IC-relocable ;
coherence
 STC N is IC-relocable
proofend;
end;

registration
let N be with_zero set ;
cluster non empty with_non-empty_values IC-Ins-separated halting standard with_explicit_jumps for AMI-Struct over N;
existence
 ex b1 being non empty with_non-empty_values IC-Ins-separated standard AMI-Struct over N st
( b1 is halting & b1 is with_explicit_jumps )
proofend;
end;

registration
let N be with_zero set ;
cluster non empty with_non-empty_values IC-Ins-separated halting standard with_explicit_jumps IC-relocable for AMI-Struct over N;
existence
 ex b1 being non empty with_non-empty_values IC-Ins-separated halting standard with_explicit_jumps AMI-Struct over N st b1 is IC-relocable
proofend;
end;

registration
let N be with_zero set ;
let S be non empty with_non-empty_values IC-Ins-separated halting IC-relocable AMI-Struct over N;
cluster  ->  IC-relocable for Element of the InstructionsF of S;
coherence
 for b1 being Instruction of S holds b1 is IC-relocable by Def4;
end;

registration
let N be with_zero set ;
let S be non empty with_non-empty_values IC-Ins-separated halting with_explicit_jumps AMI-Struct over N;
cluster with_explicit_jumps IC-relocable for Element of the InstructionsF of S;
existence
 ex b1 being Instruction of S st b1 is IC-relocable
proofend;
end;

theorem Th7: :: AMISTD_2:7
for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated halting with_explicit_jumps AMI-Struct over N
for I being IC-relocable Instruction of S
for k being Nat
for s being State of S holds (IC (Exec (I,s))) + k = IC (Exec ((IncAddr (I,k)),(IncIC (s,k))))
proofend;

registration
let N be with_zero set ;
let S be non empty with_non-empty_values IC-Ins-separated halting standard with_explicit_jumps IC-relocable AMI-Struct over N;
let F, G be NAT -defined the InstructionsF of S -valued non empty finite initial really-closed Function;
clusterF ';' G ->  really-closed ;
coherence
 F ';' G is really-closed
proofend;
end;

theorem :: AMISTD_2:8
for N being with_zero set
for I being Instruction of (Trivial-AMI N) holds JumpPart I = 0 by Lm1;

theorem :: AMISTD_2:9
for N being with_zero set
for T being InsType of the InstructionsF of (Trivial-AMI N) holds JumpParts T = {0} by Lm2;

theorem :: AMISTD_2:10
for N being with_zero set
for n being Element of NAT
for S being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N
for s being State of S
for I being Program of
for P1, P2 being Instruction-Sequence of S st I c= P1 &amp; I c= P2 &amp; ( for m being Element of NAT st m < n holds
IC (Comput (P2,s,m)) in dom I ) holds
for m being Element of NAT st m <= n holds
Comput (P1,s,m) = Comput (P2,s,m)
proofend;

theorem :: AMISTD_2:11
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 Instruction-Sequence of S
for s being State of S st s = Following (P,s) holds
for n being Element of NAT holds Comput (P,s,n) = s
proofend;