:: by Artur Korni{\l}owicz

::

:: Received April 14, 2000

:: Copyright (c) 2000-2018 Association of Mizar Users

theorem :: AMISTD_2:1

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;

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

let I be Instruction of S;

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

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;

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

attr S is with_explicit_jumps means :Def2: :: AMISTD_2:def 2

for I being Instruction of S holds I is with_explicit_jumps ;

for I being Instruction of S holds I is with_explicit_jumps ;

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

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 ;

existence

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

end;
existence

ex b

proof 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) = {(f + 1)} ) holds

JUMP I is empty

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) = {(f + 1)} ) holds

JUMP I is empty

proof end;

registration
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}

for T being InsType of the InstructionsF of (STC N) holds JumpParts T = {0}

proof end;

Lm1: for N being with_zero set

for I being Instruction of (Trivial-AMI N) holds JumpPart I = 0

proof end;

Lm2: for N being with_zero set

for T being InsType of the InstructionsF of (Trivial-AMI N) holds JumpParts T = {0}

proof end;

registration

let N be with_zero set ;

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

( b_{1} is standard & b_{1} is halting & b_{1} is with_explicit_jumps )

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

existence ex b

( b

proof end;

registration

let N be with_zero set ;

let I be Instruction of (Trivial-AMI N);

coherence

JUMP I is empty

end;
let I be Instruction of (Trivial-AMI N);

coherence

JUMP I is empty

proof end;

registration
end;

registration

let N be with_zero set ;

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

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

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

existence ex b

( b

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

coherence

for b_{1} being Instruction of S holds b_{1} is with_explicit_jumps
by Def2;

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

coherence

for b

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

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

proof end;

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;

coherence

JUMP I is empty by Th4;

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

let I be halting Instruction of S;

coherence

JUMP I is empty by Th4;

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

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

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

coherence

for b_{1} being Instruction of S st b_{1} is halting holds

b_{1} is ins-loc-free

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

coherence

for b

b

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

coherence

for b_{1} being Instruction of S st b_{1} is sequential holds

b_{1} is ins-loc-free

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

coherence

for b

b

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

let I be halting Instruction of S;

let k be Nat;

coherence

IncAddr (I,k) is halting by COMPOS_0:4;

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

coherence

IncAddr (I,k) is halting by COMPOS_0:4;

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;

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;

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

let I be Instruction of S;

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

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;

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

attr S is IC-relocable means :Def4: :: AMISTD_2:def 4

for I being Instruction of S holds I is IC-relocable ;

for I being Instruction of S holds I is IC-relocable ;

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

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;

coherence

for b_{1} being Instruction of S st b_{1} is sequential holds

b_{1} is IC-relocable

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

coherence

for b

b

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

coherence

for b_{1} being Instruction of S st b_{1} is halting holds

b_{1} is IC-relocable

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

coherence

for b

b

proof end;

registration
end;

registration

let N be with_zero set ;

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

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

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

existence ex b

( b

proof end;

registration

let N be with_zero set ;

ex b_{1} being non empty with_non-empty_values IC-Ins-separated halting standard with_explicit_jumps AMI-Struct over N st b_{1} is IC-relocable

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

existence ex b

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

coherence

for b_{1} being Instruction of S holds b_{1} is IC-relocable
by Def4;

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

coherence

for b

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;

existence

ex b_{1} being Instruction of S st b_{1} is IC-relocable

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

existence

ex b

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

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

proof end;

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 really-closed Program of ;

coherence

F ';' G is really-closed

end;
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 really-closed Program of ;

coherence

F ';' G is really-closed

proof end;

theorem :: AMISTD_2:8

theorem :: AMISTD_2:9

theorem :: AMISTD_2:10

for N being with_zero set

for n being 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 & I c= P2 & ( for m being Nat st m < n holds

IC (Comput (P2,s,m)) in dom I ) holds

for m being Nat st m <= n holds

Comput (P1,s,m) = Comput (P2,s,m)

for n being 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 & I c= P2 & ( for m being Nat st m < n holds

IC (Comput (P2,s,m)) in dom I ) holds

for m being Nat st m <= n holds

Comput (P1,s,m) = Comput (P2,s,m)

proof end;

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