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

theorem :: AMISTD_1:1

canceled;

theorem :: AMISTD_1:2

canceled;

theorem :: AMISTD_1:3

canceled;

theorem :: AMISTD_1:4

canceled;

theorem :: AMISTD_1:5

canceled;

theorem :: AMISTD_1:6

canceled;

theorem :: AMISTD_1:7

canceled;

theorem :: AMISTD_1:8

canceled;

theorem :: AMISTD_1:9

canceled;

theorem :: AMISTD_1:10

canceled;

theorem Th11: :: AMISTD_1:11

for N being with_non-empty_elements set
for IL being non empty set
for S being non empty stored-program definite AMI-Struct of IL,N
for I being Element of the Instructions of S
for s being State of S holds s +* (IL --> I) is State of S

proof end;

registration

let IL, N be set ;
let S be AMI-Struct of IL,N;
cluster empty -> IL -defined Element of sproduct the Object-Kind of S;
coherence
for b₁ being FinPartState of S st b₁ is empty holds
b₁ is IL -defined

proof end;

end;

registration

let IL, N be set ;
let S be AMI-Struct of IL,N;
cluster empty Element of sproduct the Object-Kind of S;
existence
ex b₁ being FinPartState of S st b₁ is empty

proof end;

end;

registration

let IL be non empty set ;
let N be with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite AMI-Struct of IL,N;
cluster IL -defined non empty trivial Element of sproduct the Object-Kind of S;
existence
ex b₁ being FinPartState of S st
( not b₁ is empty & b₁ is trivial & b₁ is IL -defined )

proof end;

end;

registration

let IL be non empty set ;
let N be with_non-empty_elements set ;
let S be stored-program AMI-Struct of IL,N;
let i be Element of the Instructions of S;
let s be State of S;
cluster (the Execution of S . i) . s -> Relation-like Function-like ;
coherence
( (the Execution of S . i) . s is Function-like & (the Execution of S . i) . s is Relation-like )

proof end;

end;

Lm1: for N being with_non-empty_elements set
for IL being non empty set
for S being non empty stored-program IC-Ins-separated steady-programmed definite AMI-Struct of IL,N
for il being Instruction-Location of S
for I being Element of the Instructions of S
for f being FinPartState of S st f = il .--> I holds
f is autonomic

proof end;

registration

let IL be non empty set ;
let N be with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated steady-programmed definite AMI-Struct of IL,N;
cluster IL -defined non empty trivial autonomic Element of sproduct the Object-Kind of S;
existence
ex b₁ being FinPartState of S st
( not b₁ is empty & b₁ is trivial & b₁ is autonomic & b₁ is IL -defined )

proof end;

end;

theorem :: AMISTD_1:12

for N being with_non-empty_elements set
for IL being non empty set
for S being non empty stored-program IC-Ins-separated steady-programmed definite AMI-Struct of IL,N
for il being Instruction-Location of S
for I being Element of the Instructions of S holds il .--> I is autonomic by Lm1;

theorem Th13: :: AMISTD_1:13

for N being with_non-empty_elements set
for IL being non empty set
for S being non empty stored-program IC-Ins-separated steady-programmed definite AMI-Struct of IL,N holds S is programmable

proof end;

registration

let IL be non empty set ;
let N be with_non-empty_elements set ;
cluster non empty stored-program IC-Ins-separated steady-programmed definite -> non empty stored-program IC-Ins-separated definite programmable AMI-Struct of IL,N;
coherence
for b₁ being non empty stored-program IC-Ins-separated definite AMI-Struct of IL,N st b₁ is steady-programmed holds
b₁ is programmable by Th13;

end;

definition

let IL, N be set ;
let S be AMI-Struct of IL,N;
mode IL-Subset of S -> Subset of IL means :Def1: :: AMISTD_1:def 1
verum;
existence
ex b₁ being Subset of IL st verum ;

end;

:: deftheorem Def1 defines IL-Subset AMISTD_1:def 1 :

for IL, N being set
for S being AMI-Struct of IL,N
for b₄ being Subset of IL holds
( b₄ is IL-Subset of S iff verum );

registration

let IL, N be set ;
let S be AMI-Struct of IL,N;
cluster empty IL-Subset of S;
existence
ex b₁ being IL-Subset of S st b₁ is empty

proof end;

end;

registration

let IL be non empty set ;
let N be set ;
let S be non empty AMI-Struct of IL,N;
cluster non empty IL-Subset of S;
existence
not for b₁ being IL-Subset of S holds b₁ is empty

proof end;

end;

definition

let IL be non empty set ;
let N be with_non-empty_elements set ;
let S be non empty stored-program standard-ins AMI-Struct of IL,N;
let T be InsType of S;
canceled;
attr T is jump-only means :: AMISTD_1:def 3
for s being State of S
for o being Object of S
for I being Instruction of S st InsCode I = T & o <> IC S holds
(Exec I,s) . o = s . o;

end;

:: deftheorem AMISTD_1:def 2 :

canceled;

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

for IL being non empty set
for N being with_non-empty_elements set
for S being non empty stored-program standard-ins AMI-Struct of IL,N
for T being InsType of S holds
( T is jump-only iff for s being State of S
for o being Object of S
for I being Instruction of S st InsCode I = T & o <> IC S holds
(Exec I,s) . o = s . o );

definition

let IL be non empty set ;
let N be with_non-empty_elements set ;
let S be non empty stored-program standard-ins AMI-Struct of IL,N;
let I be Instruction of S;
attr I is jump-only means :: AMISTD_1:def 4
InsCode I is jump-only ;

end;

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

for IL being non empty set
for N being with_non-empty_elements set
for S being non empty stored-program standard-ins AMI-Struct of IL,N
for I being Instruction of S holds
( I is jump-only iff InsCode I is jump-only );

definition

let IL be non empty set ;
let N be with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite AMI-Struct of IL,N;
let l be Instruction-Location of S;
let i be Element of the Instructions of S;
func NIC i,l -> IL-Subset of S equals :: AMISTD_1:def 5
{ (IC (Following s)) where s is State of S : ( IC s = l & s . l = i ) } ;
coherence
{ (IC (Following s)) where s is State of S : ( IC s = l & s . l = i ) } is IL-Subset of S

proof end;

end;

:: deftheorem defines NIC AMISTD_1:def 5 :

for IL being non empty set
for N being with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite AMI-Struct of IL,N
for l being Instruction-Location of S
for i being Element of the Instructions of S holds NIC i,l = { (IC (Following s)) where s is State of S : ( IC s = l & s . l = i ) } ;

Lm2: now

let IL be non empty set ; :: thesis: for N being with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite realistic AMI-Struct of IL,N
for i being Element of the Instructions of S
for l being Instruction-Location of S
for s being State of S
for f being FinPartState of S st f = (IC S),l --> l,i holds
IC (Following (s +* f)) in NIC i,l
let N be with_non-empty_elements set ; :: thesis: for S being non empty stored-program IC-Ins-separated definite realistic AMI-Struct of IL,N
for i being Element of the Instructions of S
for l being Instruction-Location of S
for s being State of S
for f being FinPartState of S st f = (IC S),l --> l,i holds
IC (Following (s +* f)) in NIC i,l
let S be non empty stored-program IC-Ins-separated definite realistic AMI-Struct of IL,N; :: thesis: for i being Element of the Instructions of S
for l being Instruction-Location of S
for s being State of S
for f being FinPartState of S st f = (IC S),l --> l,i holds
IC (Following (s +* f)) in NIC i,l
let i be Element of the Instructions of S; :: thesis: for l being Instruction-Location of S
for s being State of S
for f being FinPartState of S st f = (IC S),l --> l,i holds
IC (Following (s +* f)) in NIC i,l
let l be Instruction-Location of S; :: thesis: for s being State of S
for f being FinPartState of S st f = (IC S),l --> l,i holds
IC (Following (s +* f)) in NIC i,l
let s be State of S; :: thesis: for f being FinPartState of S st f = (IC S),l --> l,i holds
IC (Following (s +* f)) in NIC i,l
let f be FinPartState of S; :: thesis: ( f = (IC S),l --> l,i implies IC (Following (s +* f)) in NIC i,l )
assume A1: f = (IC S),l --> l,i ; :: thesis: IC (Following (s +* f)) in NIC i,l
set t = s +* f;
A2: dom f = {(IC S),l} by A1, FUNCT_4:65;
then l in dom f by TARSKI:def 2;
then A3: (s +* f) . l = f . l by FUNCT_4:14
.= i by A1, FUNCT_4:66 ;
IC S in dom f by A2, TARSKI:def 2;
then IC (s +* f) = f . (IC S) by FUNCT_4:14
.= l by A1, AMI_1:48, FUNCT_4:66 ;
hence IC (Following (s +* f)) in NIC i,l by A3; :: thesis: verum

end;

registration

let IL be non empty set ;
let N be with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite realistic AMI-Struct of IL,N;
let i be Element of the Instructions of S;
let l be Instruction-Location of S;
cluster NIC i,l -> non empty ;
coherence
not NIC i,l is empty

proof end;

end;

definition

let IL be non empty set ;
let N be with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite AMI-Struct of IL,N;
let i be Element of the Instructions of S;
func JUMP i -> Subset of IL equals :: AMISTD_1:def 6
meet { (NIC i,l) where l is Instruction-Location of S : verum } ;
coherence
meet { (NIC i,l) where l is Instruction-Location of S : verum } is Subset of IL

proof end;

end;

:: deftheorem defines JUMP AMISTD_1:def 6 :

for IL being non empty set
for N being with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite AMI-Struct of IL,N
for i being Element of the Instructions of S holds JUMP i = meet { (NIC i,l) where l is Instruction-Location of S : verum } ;

definition

let IL be non empty set ;
let N be with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite AMI-Struct of IL,N;
let l be Instruction-Location of S;
func SUCC l -> Subset of IL equals :: AMISTD_1:def 7
union { ((NIC i,l) \ (JUMP i)) where i is Element of the Instructions of S : verum } ;
coherence
union { ((NIC i,l) \ (JUMP i)) where i is Element of the Instructions of S : verum } is Subset of IL

proof end;

end;

:: deftheorem defines SUCC AMISTD_1:def 7 :

for IL being non empty set
for N being with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite AMI-Struct of IL,N
for l being Instruction-Location of S holds SUCC l = union { ((NIC i,l) \ (JUMP i)) where i is Element of the Instructions of S : verum } ;

theorem Th14: :: AMISTD_1:14

for N being with_non-empty_elements set
for IL being non empty set
for S being non empty stored-program IC-Ins-separated definite AMI-Struct of IL,N
for i being Element of the Instructions of S st not IL is trivial & ( for l being Instruction-Location of S holds NIC i,l = {l} ) holds
JUMP i is empty

proof end;

theorem Th15: :: AMISTD_1:15

for N being with_non-empty_elements set
for IL being non empty set
for S being non empty stored-program IC-Ins-separated definite realistic AMI-Struct of IL,N
for il being Instruction-Location of S
for i being Instruction of S st i is halting holds
NIC i,il = {il}

proof end;

definition

let IL be non empty set ;
let N be with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite AMI-Struct of IL,N;
let l1, l2 be Instruction-Location of S;
pred l1 <= l2 means :Def8: :: AMISTD_1:def 8
ex f being non empty IL-FinSequence of S st
( f /. 1 = l1 & f /. (len f) = l2 & ( for n being Element of NAT st 1 <= n & n < len f holds
f /. (n + 1) in SUCC (f /. n) ) );
reflexivity
for l1 being Instruction-Location of S ex f being non empty IL-FinSequence of S st
( f /. 1 = l1 & f /. (len f) = l1 & ( for n being Element of NAT st 1 <= n & n < len f holds
f /. (n + 1) in SUCC (f /. n) ) )

proof end;

end;

:: deftheorem Def8 defines <= AMISTD_1:def 8 :

for IL being non empty set
for N being with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite AMI-Struct of IL,N
for l1, l2 being Instruction-Location of S holds
( l1 <= l2 iff ex f being non empty IL-FinSequence of S st
( f /. 1 = l1 & f /. (len f) = l2 & ( for n being Element of NAT st 1 <= n & n < len f holds
f /. (n + 1) in SUCC (f /. n) ) ) );

theorem :: AMISTD_1:16

for N being with_non-empty_elements set
for IL being non empty set
for S being non empty stored-program IC-Ins-separated definite AMI-Struct of IL,N
for l1, l2, l3 being Instruction-Location of S st l1 <= l2 & l2 <= l3 holds
l1 <= l3

proof end;

definition

let IL be non empty set ;
let N be with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite AMI-Struct of IL,N;
attr S is InsLoc-antisymmetric means :: AMISTD_1:def 9
for l1, l2 being Instruction-Location of S st l1 <= l2 & l2 <= l1 holds
l1 = l2;

end;

:: deftheorem defines InsLoc-antisymmetric AMISTD_1:def 9 :

for IL being non empty set
for N being with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite AMI-Struct of IL,N holds
( S is InsLoc-antisymmetric iff for l1, l2 being Instruction-Location of S st l1 <= l2 & l2 <= l1 holds
l1 = l2 );

definition

let IL be non empty set ;
let N be with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite AMI-Struct of IL,N;
attr S is standard means :Def10: :: AMISTD_1:def 10
ex f being IL-Function of NAT ,S st
( f is bijective & ( for m, n being Element of NAT holds
( m <= n iff f . m <= f . n ) ) );

end;

:: deftheorem Def10 defines standard AMISTD_1:def 10 :

for IL being non empty set
for N being with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite AMI-Struct of IL,N holds
( S is standard iff ex f being IL-Function of NAT ,S st
( f is bijective & ( for m, n being Element of NAT holds
( m <= n iff f . m <= f . n ) ) ) );

theorem Th17: :: AMISTD_1:17

for N being with_non-empty_elements set
for IL being non empty set
for S being non empty stored-program IC-Ins-separated definite AMI-Struct of IL,N
for f1, f2 being IL-Function of NAT ,S st f1 is bijective & ( for m, n being Element of NAT holds
( m <= n iff f1 . m <= f1 . n ) ) & f2 is bijective & ( for m, n being Element of NAT holds
( m <= n iff f2 . m <= f2 . n ) ) holds
f1 = f2

proof end;

theorem Th18: :: AMISTD_1:18

for N being with_non-empty_elements set
for IL being non empty set
for S being non empty stored-program IC-Ins-separated definite AMI-Struct of IL,N
for f being IL-Function of NAT ,S st f is bijective holds
( ( for m, n being Element of NAT holds
( m <= n iff f . m <= f . n ) ) iff for k being Element of NAT holds
( f . (k + 1) in SUCC (f . k) & ( for j being Element of NAT st f . j in SUCC (f . k) holds
k <= j ) ) )

proof end;

theorem Th19: :: AMISTD_1:19

for N being with_non-empty_elements set
for IL being non empty set
for S being non empty stored-program IC-Ins-separated definite AMI-Struct of IL,N holds
( S is standard iff ex f being IL-Function of NAT ,S st
( f is bijective & ( for k being Element of NAT holds
( f . (k + 1) in SUCC (f . k) & ( for j being Element of NAT st f . j in SUCC (f . k) holds
k <= j ) ) ) ) )

proof end;

Lm3: for a, b being set holds dom ((NAT --> a) +* (NAT .--> b)) = NAT \/ {NAT }

proof end;

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

definition

let N be with_non-empty_elements set ;
func STC N -> strict AMI-Struct of NAT ,N means :Def11: :: AMISTD_1:def 11
( the carrier of it = NAT \/ {NAT } & the Instruction-Counter of it = NAT & the Instructions of it = {[0 ,0 ],[1,0 ]} & the Object-Kind of it = (NAT --> {[1,0 ],[0 ,0 ]}) +* (NAT .--> NAT ) & ex f being Function of (product the Object-Kind of it),(product the Object-Kind of it) st
( ( for s being Element of product the Object-Kind of it holds f . s = s +* (NAT .--> (succ (s . NAT ))) ) & the Execution of it = ([1,0 ] .--> f) +* ([0 ,0 ] .--> (id (product the Object-Kind of it))) ) );
existence
ex b₁ being strict AMI-Struct of NAT ,N st
( the carrier of b₁ = NAT \/ {NAT } & the Instruction-Counter of b₁ = NAT & the Instructions of b₁ = {[0 ,0 ],[1,0 ]} & the Object-Kind of b₁ = (NAT --> {[1,0 ],[0 ,0 ]}) +* (NAT .--> NAT ) & ex f being Function of (product the Object-Kind of b₁),(product the Object-Kind of b₁) st
( ( for s being Element of product the Object-Kind of b₁ holds f . s = s +* (NAT .--> (succ (s . NAT ))) ) & the Execution of b₁ = ([1,0 ] .--> f) +* ([0 ,0 ] .--> (id (product the Object-Kind of b₁))) ) )

proof end;

uniqueness
for b₁, b₂ being strict AMI-Struct of NAT ,N st the carrier of b₁ = NAT \/ {NAT } & the Instruction-Counter of b₁ = NAT & the Instructions of b₁ = {[0 ,0 ],[1,0 ]} & the Object-Kind of b₁ = (NAT --> {[1,0 ],[0 ,0 ]}) +* (NAT .--> NAT ) & ex f being Function of (product the Object-Kind of b₁),(product the Object-Kind of b₁) st
( ( for s being Element of product the Object-Kind of b₁ holds f . s = s +* (NAT .--> (succ (s . NAT ))) ) & the Execution of b₁ = ([1,0 ] .--> f) +* ([0 ,0 ] .--> (id (product the Object-Kind of b₁))) ) & the carrier of b₂ = NAT \/ {NAT } & the Instruction-Counter of b₂ = NAT & the Instructions of b₂ = {[0 ,0 ],[1,0 ]} & the Object-Kind of b₂ = (NAT --> {[1,0 ],[0 ,0 ]}) +* (NAT .--> NAT ) & ex f being Function of (product the Object-Kind of b₂),(product the Object-Kind of b₂) st
( ( for s being Element of product the Object-Kind of b₂ holds f . s = s +* (NAT .--> (succ (s . NAT ))) ) & the Execution of b₂ = ([1,0 ] .--> f) +* ([0 ,0 ] .--> (id (product the Object-Kind of b₂))) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def11 defines STC AMISTD_1:def 11 :

for N being with_non-empty_elements set
for b₂ being strict AMI-Struct of NAT ,N holds
( b₂ = STC N iff ( the carrier of b₂ = NAT \/ {NAT } & the Instruction-Counter of b₂ = NAT & the Instructions of b₂ = {[0 ,0 ],[1,0 ]} & the Object-Kind of b₂ = (NAT --> {[1,0 ],[0 ,0 ]}) +* (NAT .--> NAT ) & ex f being Function of (product the Object-Kind of b₂),(product the Object-Kind of b₂) st
( ( for s being Element of product the Object-Kind of b₂ holds f . s = s +* (NAT .--> (succ (s . NAT ))) ) & the Execution of b₂ = ([1,0 ] .--> f) +* ([0 ,0 ] .--> (id (product the Object-Kind of b₂))) ) ) );

registration

let N be with_non-empty_elements set ;
cluster STC N -> infinite strict ;
coherence
not STC N is finite

proof end;

end;

registration

let N be with_non-empty_elements set ;
cluster STC N -> non empty strict stored-program standard-ins ;
coherence
( not STC N is empty & STC N is stored-program & STC N is standard-ins )

proof end;

end;

registration

let N be with_non-empty_elements set ;
cluster STC N -> strict IC-Ins-separated steady-programmed definite realistic ;
coherence
( STC N is IC-Ins-separated & STC N is definite & STC N is realistic & STC N is steady-programmed )

proof end;

end;

Lm4: for N being with_non-empty_elements set
for i being Instruction of (STC N)
for s being State of (STC N) st InsCode i = 1 holds
(Exec i,s) . (IC (STC N)) = succ (IC s)

proof end;

theorem Th20: :: AMISTD_1:20

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

proof end;

theorem :: AMISTD_1:21

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

proof end;

theorem Th22: :: AMISTD_1:22

for N being with_non-empty_elements set
for i being Element of the Instructions of (STC N) holds
( InsCode i = 1 or InsCode i = 0 )

proof end;

theorem :: AMISTD_1:23

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

proof end;

Lm5: for z being natural number
for N being with_non-empty_elements set
for l being Instruction-Location of STC N
for i being Element of the Instructions of (STC N) st l = z & InsCode i = 1 holds
NIC i,l = {(z + 1)}

proof end;

Lm6: for N being with_non-empty_elements set
for i being Element of the Instructions of (STC N) holds JUMP i is empty

proof end;

theorem Th24: :: AMISTD_1:24

for z being natural number
for N being with_non-empty_elements set
for l being Instruction-Location of STC N st l = z holds
SUCC l = {z,(z + 1)}

proof end;

registration

let N be with_non-empty_elements set ;
cluster STC N -> strict standard ;
coherence
STC N is standard

proof end;

end;

registration

let N be with_non-empty_elements set ;
cluster STC N -> strict halting ;
coherence
STC N is halting

proof end;

end;

registration

let N be with_non-empty_elements set ;
cluster non empty stored-program halting IC-Ins-separated steady-programmed definite realistic programmable standard-ins standard AMI-Struct of NAT ,N;
existence
ex b₁ being non empty stored-program IC-Ins-separated definite AMI-Struct of NAT ,N st
( b₁ is standard & b₁ is halting & b₁ is realistic & b₁ is steady-programmed & b₁ is programmable & b₁ is standard-ins )

proof end;

end;

definition

let N be with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite standard AMI-Struct of NAT ,N;
let k be natural number ;
func il. S,k -> Instruction-Location of S means :Def12: :: AMISTD_1:def 12
ex f being IL-Function of NAT ,S st
( f is bijective & ( for m, n being Element of NAT holds
( m <= n iff f . m <= f . n ) ) & it = f . k );
existence
ex b₁ being Instruction-Location of S ex f being IL-Function of NAT ,S st
( f is bijective & ( for m, n being Element of NAT holds
( m <= n iff f . m <= f . n ) ) & b₁ = f . k )

proof end;

uniqueness
for b₁, b₂ being Instruction-Location of S st ex f being IL-Function of NAT ,S st
( f is bijective & ( for m, n being Element of NAT holds
( m <= n iff f . m <= f . n ) ) & b₁ = f . k ) & ex f being IL-Function of NAT ,S st
( f is bijective & ( for m, n being Element of NAT holds
( m <= n iff f . m <= f . n ) ) & b₂ = f . k ) holds
b₁ = b₂ by Th17;

end;

:: deftheorem Def12 defines il. AMISTD_1:def 12 :

for N being with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite standard AMI-Struct of NAT ,N
for k being natural number
for b₄ being Instruction-Location of S holds
( b₄ = il. S,k iff ex f being IL-Function of NAT ,S st
( f is bijective & ( for m, n being Element of NAT holds
( m <= n iff f . m <= f . n ) ) & b₄ = f . k ) );

theorem Th25: :: AMISTD_1:25

for N being with_non-empty_elements set
for T being non empty stored-program IC-Ins-separated definite standard AMI-Struct of NAT ,N
for k1, k2 being natural number st il. T,k1 = il. T,k2 holds
k1 = k2

proof end;

theorem Th26: :: AMISTD_1:26

for N being with_non-empty_elements set
for T being non empty stored-program IC-Ins-separated definite standard AMI-Struct of NAT ,N
for l being Instruction-Location of T ex k being natural number st l = il. T,k

proof end;

definition

let N be with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite standard AMI-Struct of NAT ,N;
let l be Instruction-Location of S;
func locnum l -> natural number means :Def13: :: AMISTD_1:def 13
il. S,it = l;
existence
ex b₁ being natural number st il. S,b₁ = l by Th26;
uniqueness
for b₁, b₂ being natural number st il. S,b₁ = l & il. S,b₂ = l holds
b₁ = b₂ by Th25;

end;

:: deftheorem Def13 defines locnum AMISTD_1:def 13 :

for N being with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite standard AMI-Struct of NAT ,N
for l being Instruction-Location of S
for b₄ being natural number holds
( b₄ = locnum l iff il. S,b₄ = l );

definition

let N be with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite standard AMI-Struct of NAT ,N;
let l be Instruction-Location of S;
:: original: locnum
redefine func locnum l -> Element of NAT ;
coherence
locnum l is Element of NAT by ORDINAL1:def 13;

end;

theorem Th27: :: AMISTD_1:27

for N being with_non-empty_elements set
for T being non empty stored-program IC-Ins-separated definite standard AMI-Struct of NAT ,N
for l1, l2 being Instruction-Location of T st locnum l1 = locnum l2 holds
l1 = l2

proof end;

theorem Th28: :: AMISTD_1:28

for N being with_non-empty_elements set
for T being non empty stored-program IC-Ins-separated definite standard AMI-Struct of NAT ,N
for k1, k2 being natural number holds
( il. T,k1 <= il. T,k2 iff k1 <= k2 )

proof end;

theorem Th29: :: AMISTD_1:29

for N being with_non-empty_elements set
for T being non empty stored-program IC-Ins-separated definite standard AMI-Struct of NAT ,N
for l1, l2 being Instruction-Location of T holds
( locnum l1 <= locnum l2 iff l1 <= l2 )

proof end;

theorem Th30: :: AMISTD_1:30

for N being with_non-empty_elements set
for T being non empty stored-program IC-Ins-separated definite standard AMI-Struct of NAT ,N holds T is InsLoc-antisymmetric

proof end;

registration

let N be with_non-empty_elements set ;
cluster non empty stored-program IC-Ins-separated definite standard -> non empty stored-program IC-Ins-separated definite InsLoc-antisymmetric AMI-Struct of NAT ,N;
coherence
for b₁ being non empty stored-program IC-Ins-separated definite AMI-Struct of NAT ,N st b₁ is standard holds
b₁ is InsLoc-antisymmetric by Th30;

end;

definition

let N be with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite standard AMI-Struct of NAT ,N;
let f be Instruction-Location of S;
let k be natural number ;
func f + k -> Instruction-Location of S equals :: AMISTD_1:def 14
il. S,((locnum f) + k);
coherence
il. S,((locnum f) + k) is Instruction-Location of S ;

end;

:: deftheorem defines + AMISTD_1:def 14 :

for N being with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite standard AMI-Struct of NAT ,N
for f being Instruction-Location of S
for k being natural number holds f + k = il. S,((locnum f) + k);

theorem :: AMISTD_1:31

for N being with_non-empty_elements set
for T being non empty stored-program IC-Ins-separated definite standard AMI-Struct of NAT ,N
for f being Instruction-Location of T holds f + 0 = f by Def13;

theorem :: AMISTD_1:32

for z being natural number
for N being with_non-empty_elements set
for T being non empty stored-program IC-Ins-separated definite standard AMI-Struct of NAT ,N
for f, g being Instruction-Location of T st f + z = g + z holds
f = g

proof end;

theorem :: AMISTD_1:33

for z being natural number
for N being with_non-empty_elements set
for T being non empty stored-program IC-Ins-separated definite standard AMI-Struct of NAT ,N
for f being Instruction-Location of T holds (locnum f) + z = locnum (f + z) by Def13;

definition

let N be with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite standard AMI-Struct of NAT ,N;
let f be Instruction-Location of S;
func NextLoc f -> Instruction-Location of S equals :: AMISTD_1:def 15
f + 1;
coherence
f + 1 is Instruction-Location of S ;

end;

:: deftheorem defines NextLoc AMISTD_1:def 15 :

for N being with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite standard AMI-Struct of NAT ,N
for f being Instruction-Location of S holds NextLoc f = f + 1;

theorem :: AMISTD_1:34

for N being with_non-empty_elements set
for T being non empty stored-program IC-Ins-separated definite standard AMI-Struct of NAT ,N
for f being Instruction-Location of T holds NextLoc f = il. T,((locnum f) + 1) ;

theorem Th35: :: AMISTD_1:35

for N being with_non-empty_elements set
for T being non empty stored-program IC-Ins-separated definite standard AMI-Struct of NAT ,N
for f being Instruction-Location of T holds f <> NextLoc f

proof end;

theorem :: AMISTD_1:36

for N being with_non-empty_elements set
for T being non empty stored-program IC-Ins-separated definite standard AMI-Struct of NAT ,N
for f, g being Instruction-Location of T st NextLoc f = NextLoc g holds
f = g

proof end;

theorem Th37: :: AMISTD_1:37

for z being natural number
for N being with_non-empty_elements set holds il. (STC N),z = z

proof end;

theorem :: AMISTD_1:38

for N being with_non-empty_elements set
for i being Instruction of (STC N)
for s being State of (STC N) st InsCode i = 1 holds
(Exec i,s) . (IC (STC N)) = NextLoc (IC s)

proof end;

theorem :: AMISTD_1:39

for N being with_non-empty_elements set
for l being Instruction-Location of STC N
for i being Element of the Instructions of (STC N) st InsCode i = 1 holds
NIC i,l = {(NextLoc l)}

proof end;

theorem :: AMISTD_1:40

for N being with_non-empty_elements set
for l being Instruction-Location of STC N holds SUCC l = {l,(NextLoc l)}

proof end;

definition

let N be with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite standard AMI-Struct of NAT ,N;
let i be Instruction of S;
attr i is sequential means :: AMISTD_1:def 16
for s being State of S holds (Exec i,s) . (IC S) = NextLoc (IC s);

end;

:: deftheorem defines sequential AMISTD_1:def 16 :

for N being with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite standard AMI-Struct of NAT ,N
for i being Instruction of S holds
( i is sequential iff for s being State of S holds (Exec i,s) . (IC S) = NextLoc (IC s) );

theorem Th41: :: AMISTD_1:41

for N being with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite realistic standard AMI-Struct of NAT ,N
for il being Instruction-Location of S
for i being Instruction of S st i is sequential holds
NIC i,il = {(NextLoc il)}

proof end;

theorem Th42: :: AMISTD_1:42

for N being with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite realistic standard AMI-Struct of NAT ,N
for i being Instruction of S st i is sequential holds
not i is halting

proof end;

registration

let N be with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite realistic standard AMI-Struct of NAT ,N;
cluster sequential -> non halting Element of the Instructions of S;
coherence
for b₁ being Instruction of S st b₁ is sequential holds
not b₁ is halting by Th42;
cluster halting -> non sequential Element of the Instructions of S;
coherence
for b₁ being Instruction of S st b₁ is halting holds
not b₁ is sequential ;

end;

theorem :: AMISTD_1:43

for N being with_non-empty_elements set
for T being non empty stored-program IC-Ins-separated definite standard AMI-Struct of NAT ,N
for i being Instruction of T st not JUMP i is empty holds
not i is sequential

proof end;

definition

let IL be non empty set ;
let N be with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite AMI-Struct of IL,N;
let F be IL -defined FinPartState of S;
attr F is closed means :Def17: :: AMISTD_1:def 17
for l being Instruction-Location of S st l in dom F holds
NIC (pi F,l),l c= dom F;
attr F is really-closed means :: AMISTD_1:def 18
for s being State of S st F c= s & IC s in dom F holds
for k being Element of NAT holds IC (Computation s,k) in dom F;

end;

:: deftheorem Def17 defines closed AMISTD_1:def 17 :

for IL being non empty set
for N being with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite AMI-Struct of IL,N
for F being b₁ -defined FinPartState of S holds
( F is closed iff for l being Instruction-Location of S st l in dom F holds
NIC (pi F,l),l c= dom F );

:: deftheorem defines really-closed AMISTD_1:def 18 :

for IL being non empty set
for N being with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite AMI-Struct of IL,N
for F being b₁ -defined FinPartState of S holds
( F is really-closed iff for s being State of S st F c= s & IC s in dom F holds
for k being Element of NAT holds IC (Computation s,k) in dom F );

definition

let N be with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite standard AMI-Struct of NAT ,N;
let F be FinPartState of S;
attr F is para-closed means :: AMISTD_1:def 19
for s being State of S st F c= s & IC s = il. S,0 holds
for k being Element of NAT holds IC (Computation s,k) in dom F;

end;

:: deftheorem defines para-closed AMISTD_1:def 19 :

for N being with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite standard AMI-Struct of NAT ,N
for F being FinPartState of S holds
( F is para-closed iff for s being State of S st F c= s & IC s = il. S,0 holds
for k being Element of NAT holds IC (Computation s,k) in dom F );

theorem Th44: :: AMISTD_1:44

for N being with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated steady-programmed definite standard AMI-Struct of NAT ,N
for F being NAT -defined FinPartState of S st F is really-closed & il. S,0 in dom F holds
F is para-closed

proof end;

theorem Th45: :: AMISTD_1:45

for N being with_non-empty_elements set
for IL being non empty set
for S being non empty stored-program IC-Ins-separated steady-programmed definite AMI-Struct of IL,N
for F being b₂ -defined FinPartState of S st F is closed holds
F is really-closed

proof end;

registration

let IL be non empty set ;
let N be with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated steady-programmed definite AMI-Struct of IL,N;
cluster IL -defined closed -> IL -defined really-closed Element of sproduct the Object-Kind of S;
coherence
for b₁ being IL -defined FinPartState of S st b₁ is closed holds
b₁ is really-closed by Th45;

end;

theorem Th46: :: AMISTD_1:46

for N being with_non-empty_elements set
for S being non empty stored-program halting IC-Ins-separated definite realistic standard AMI-Struct of NAT ,N holds (il. S,0 ) .--> (halt S) is closed

proof end;

definition

let IL be non empty set ;
let N be with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite AMI-Struct of IL,N;
let F be FinPartState of S;
attr F is lower means :Def20: :: AMISTD_1:def 20
for l being Instruction-Location of S st l in dom F holds
for m being Instruction-Location of S st m <= l holds
m in dom F;

end;

:: deftheorem Def20 defines lower AMISTD_1:def 20 :

for IL being non empty set
for N being with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite AMI-Struct of IL,N
for F being FinPartState of S holds
( F is lower iff for l being Instruction-Location of S st l in dom F holds
for m being Instruction-Location of S st m <= l holds
m in dom F );

theorem Th47: :: AMISTD_1:47

for N being with_non-empty_elements set
for IL being non empty set
for S being non empty stored-program IC-Ins-separated definite AMI-Struct of IL,N
for F being empty FinPartState of S holds F is lower

proof end;

registration

let IL be non empty set ;
let N be with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite AMI-Struct of IL,N;
cluster empty -> lower Element of sproduct the Object-Kind of S;
coherence
for b₁ being FinPartState of S st b₁ is empty holds
b₁ is lower by Th47;

end;

theorem Th48: :: AMISTD_1:48

for N being with_non-empty_elements set
for T being non empty stored-program IC-Ins-separated definite standard AMI-Struct of NAT ,N
for i being Element of the Instructions of T holds (il. T,0 ) .--> i is lower

proof end;

registration

let N be with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite standard AMI-Struct of NAT ,N;
cluster NAT -defined non empty trivial lower Element of sproduct the Object-Kind of S;
existence
ex b₁ being FinPartState of S st
( b₁ is lower & not b₁ is empty & b₁ is trivial & b₁ is NAT -defined )

proof end;

end;

theorem Th49: :: AMISTD_1:49

for N being with_non-empty_elements set
for T being non empty stored-program IC-Ins-separated definite standard AMI-Struct of NAT ,N
for F being NAT -defined non empty lower FinPartState of T holds il. T,0 in dom F

proof end;

theorem Th50: :: AMISTD_1:50

for z being natural number
for N being with_non-empty_elements set
for T being non empty stored-program IC-Ins-separated definite standard AMI-Struct of NAT ,N
for P being NAT -defined lower FinPartState of T holds
( z < card P iff il. T,z in dom P )

proof end;

definition

let N be with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite standard AMI-Struct of NAT ,N;
let F be NAT -defined non empty FinPartState of S;
func LastLoc F -> Instruction-Location of S means :Def21: :: AMISTD_1:def 21
ex M being non empty finite natural-membered set st
( M = { (locnum l) where l is Instruction-Location of S : l in dom F } & it = il. S,(max M) );
existence
ex b₁ being Instruction-Location of S ex M being non empty finite natural-membered set st
( M = { (locnum l) where l is Instruction-Location of S : l in dom F } & b₁ = il. S,(max M) )

proof end;

uniqueness
for b₁, b₂ being Instruction-Location of S st ex M being non empty finite natural-membered set st
( M = { (locnum l) where l is Instruction-Location of S : l in dom F } & b₁ = il. S,(max M) ) & ex M being non empty finite natural-membered set st
( M = { (locnum l) where l is Instruction-Location of S : l in dom F } & b₂ = il. S,(max M) ) holds
b₁ = b₂ ;

end;

:: deftheorem Def21 defines LastLoc AMISTD_1:def 21 :

for N being with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite standard AMI-Struct of NAT ,N
for F being NAT -defined non empty FinPartState of S
for b₄ being Instruction-Location of S holds
( b₄ = LastLoc F iff ex M being non empty finite natural-membered set st
( M = { (locnum l) where l is Instruction-Location of S : l in dom F } & b₄ = il. S,(max M) ) );

theorem Th51: :: AMISTD_1:51

for N being with_non-empty_elements set
for T being non empty stored-program IC-Ins-separated definite standard AMI-Struct of NAT ,N
for F being NAT -defined non empty FinPartState of T holds LastLoc F in dom F

proof end;

theorem :: AMISTD_1:52

for N being with_non-empty_elements set
for T being non empty stored-program IC-Ins-separated definite standard AMI-Struct of NAT ,N
for F, G being NAT -defined non empty FinPartState of T st F c= G holds
LastLoc F <= LastLoc G

proof end;

theorem Th53: :: AMISTD_1:53

for N being with_non-empty_elements set
for T being non empty stored-program IC-Ins-separated definite standard AMI-Struct of NAT ,N
for F being NAT -defined non empty FinPartState of T
for l being Instruction-Location of T st l in dom F holds
l <= LastLoc F

proof end;

theorem :: AMISTD_1:54

for N being with_non-empty_elements set
for T being non empty stored-program IC-Ins-separated definite standard AMI-Struct of NAT ,N
for F being NAT -defined non empty lower FinPartState of T
for G being NAT -defined non empty FinPartState of T st F c= G & LastLoc F = LastLoc G holds
F = G

proof end;

theorem Th55: :: AMISTD_1:55

for N being with_non-empty_elements set
for T being non empty stored-program IC-Ins-separated definite standard AMI-Struct of NAT ,N
for F being NAT -defined non empty lower FinPartState of T holds LastLoc F = il. T,((card F) -' 1)

proof end;

registration

let N be with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated steady-programmed definite standard AMI-Struct of NAT ,N;
cluster NAT -defined non empty really-closed lower -> NAT -defined para-closed Element of sproduct the Object-Kind of S;
coherence
for b₁ being NAT -defined FinPartState of S st b₁ is really-closed & b₁ is lower & not b₁ is empty holds
b₁ is para-closed

proof end;

end;

Lm7: now

let IL be non empty set ; :: thesis: for N being with_non-empty_elements set
for S being non empty stored-program halting IC-Ins-separated definite standard AMI-Struct of NAT ,N holds
( ((il. S,0 ) .--> (halt S)) . (LastLoc ((il. S,0 ) .--> (halt S))) = halt S & ( for l being Instruction-Location of S st ((il. S,0 ) .--> (halt S)) . l = halt S & l in dom ((il. S,0 ) .--> (halt S)) holds
l = LastLoc ((il. S,0 ) .--> (halt S)) ) )
let N be with_non-empty_elements set ; :: thesis: for S being non empty stored-program halting IC-Ins-separated definite standard AMI-Struct of NAT ,N holds
( ((il. S,0 ) .--> (halt S)) . (LastLoc ((il. S,0 ) .--> (halt S))) = halt S & ( for l being Instruction-Location of S st ((il. S,0 ) .--> (halt S)) . l = halt S & l in dom ((il. S,0 ) .--> (halt S)) holds
l = LastLoc ((il. S,0 ) .--> (halt S)) ) )
let S be non empty stored-program halting IC-Ins-separated definite standard AMI-Struct of NAT ,N; :: thesis: ( ((il. S,0 ) .--> (halt S)) . (LastLoc ((il. S,0 ) .--> (halt S))) = halt S & ( for l being Instruction-Location of S st ((il. S,0 ) .--> (halt S)) . l = halt S & l in dom ((il. S,0 ) .--> (halt S)) holds
l = LastLoc ((il. S,0 ) .--> (halt S)) ) )
set F = (il. S,0 ) .--> (halt S);
A1: dom ((il. S,0 ) .--> (halt S)) = {(il. S,0 )} by FUNCOP_1:19;
then A2: card (dom ((il. S,0 ) .--> (halt S))) = 1 by CARD_1:50;
(il. S,0 ) .--> (halt S) is lower FinPartState of S by Th48;
then A3: LastLoc ((il. S,0 ) .--> (halt S)) = il. S,((card ((il. S,0 ) .--> (halt S))) -' 1) by Th55
.= il. S,((card (dom ((il. S,0 ) .--> (halt S)))) -' 1) by CARD_1:104
.= il. S,0 by A2, XREAL_1:234 ;
hence ((il. S,0 ) .--> (halt S)) . (LastLoc ((il. S,0 ) .--> (halt S))) = halt S by FUNCOP_1:87; :: thesis: for l being Instruction-Location of S st ((il. S,0 ) .--> (halt S)) . l = halt S & l in dom ((il. S,0 ) .--> (halt S)) holds
l = LastLoc ((il. S,0 ) .--> (halt S))
let l be Instruction-Location of S; :: thesis: ( ((il. S,0 ) .--> (halt S)) . l = halt S & l in dom ((il. S,0 ) .--> (halt S)) implies l = LastLoc ((il. S,0 ) .--> (halt S)) )
assume ((il. S,0 ) .--> (halt S)) . l = halt S ; :: thesis: ( l in dom ((il. S,0 ) .--> (halt S)) implies l = LastLoc ((il. S,0 ) .--> (halt S)) )
assume l in dom ((il. S,0 ) .--> (halt S)) ; :: thesis: l = LastLoc ((il. S,0 ) .--> (halt S))
hence l = LastLoc ((il. S,0 ) .--> (halt S)) by A1, A3, TARSKI:def 1; :: thesis: verum

end;

definition

let N be with_non-empty_elements set ;
let S be non empty stored-program halting IC-Ins-separated definite standard AMI-Struct of NAT ,N;
let F be NAT -defined non empty FinPartState of S;
attr F is halt-ending means :Def22: :: AMISTD_1:def 22
F . (LastLoc F) = halt S;
attr F is unique-halt means :Def23: :: AMISTD_1:def 23
for f being Instruction-Location of S st F . f = halt S & f in dom F holds
f = LastLoc F;

end;

:: deftheorem Def22 defines halt-ending AMISTD_1:def 22 :

for N being with_non-empty_elements set
for S being non empty stored-program halting IC-Ins-separated definite standard AMI-Struct of NAT ,N
for F being NAT -defined non empty FinPartState of S holds
( F is halt-ending iff F . (LastLoc F) = halt S );

:: deftheorem Def23 defines unique-halt AMISTD_1:def 23 :

for N being with_non-empty_elements set
for S being non empty stored-program halting IC-Ins-separated definite standard AMI-Struct of NAT ,N
for F being NAT -defined non empty FinPartState of S holds
( F is unique-halt iff for f being Instruction-Location of S st F . f = halt S & f in dom F holds
f = LastLoc F );

registration

let N be with_non-empty_elements set ;
let S be non empty stored-program halting IC-Ins-separated definite standard AMI-Struct of NAT ,N;
cluster NAT -defined non empty trivial lower halt-ending unique-halt Element of sproduct the Object-Kind of S;
existence
ex b₁ being NAT -defined non empty lower FinPartState of S st
( b₁ is halt-ending & b₁ is unique-halt & b₁ is trivial )

proof end;

end;

registration

let N be with_non-empty_elements set ;
let S be non empty stored-program halting IC-Ins-separated definite realistic standard AMI-Struct of NAT ,N;
cluster NAT -defined non empty trivial closed lower Element of sproduct the Object-Kind of S;
existence
ex b₁ being NAT -defined FinPartState of S st
( b₁ is trivial & b₁ is closed & b₁ is lower & not b₁ is empty )

proof end;

end;

registration

let N be with_non-empty_elements set ;
let S be non empty stored-program halting IC-Ins-separated definite realistic standard AMI-Struct of NAT ,N;
cluster NAT -defined non empty trivial closed lower halt-ending unique-halt Element of sproduct the Object-Kind of S;
existence
ex b₁ being NAT -defined non empty lower FinPartState of S st
( b₁ is halt-ending & b₁ is unique-halt & b₁ is trivial & b₁ is closed )

proof end;

end;

registration

let N be with_non-empty_elements set ;
let S be non empty stored-program halting IC-Ins-separated steady-programmed definite realistic standard AMI-Struct of NAT ,N;
cluster NAT -defined non empty trivial autonomic closed lower halt-ending unique-halt Element of sproduct the Object-Kind of S;
existence
ex b₁ being NAT -defined non empty lower FinPartState of S st
( b₁ is halt-ending & b₁ is unique-halt & b₁ is autonomic & b₁ is trivial & b₁ is closed )

proof end;

end;

definition

let N be with_non-empty_elements set ;
let S be non empty stored-program halting IC-Ins-separated definite standard AMI-Struct of NAT ,N;
mode pre-Macro of S is NAT -defined non empty lower halt-ending unique-halt FinPartState of S;

end;

registration

let N be with_non-empty_elements set ;
let S be non empty stored-program halting IC-Ins-separated definite realistic standard AMI-Struct of NAT ,N;
cluster closed Element of sproduct the Object-Kind of S;
existence
ex b₁ being pre-Macro of S st b₁ is closed

proof end;

end;

theorem :: AMISTD_1:56

for N being with_non-empty_elements set
for IL being non empty set
for i being Instruction of (Trivial-AMI IL,N) holds i is halting

proof end;

theorem :: AMISTD_1:57

for N being with_non-empty_elements set
for IL being non empty set
for i being Element of the Instructions of (Trivial-AMI IL,N) holds InsCode i = 0

proof end;

theorem :: AMISTD_1:58

for IL being non empty set
for N being with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite AMI-Struct of IL,N
for i being Instruction of S
for l being Instruction-Location of S holds JUMP i c= NIC i,l

proof end;

theorem :: AMISTD_1:59

for IL being non empty set
for N being with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite AMI-Struct of IL,N
for l1, l2 being Instruction-Location of S st SUCC l1 = IL holds
l1 <= l2

proof end;

definition

let N be with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite standard AMI-Struct of NAT ,N;
let loc be Instruction-Location of S;
let k be natural number ;
func loc -' k -> Instruction-Location of S equals :: AMISTD_1:def 24
il. S,((locnum loc) -' k);
coherence
il. S,((locnum loc) -' k) is Instruction-Location of S ;

end;

:: deftheorem defines -' AMISTD_1:def 24 :

for N being with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite standard AMI-Struct of NAT ,N
for loc being Instruction-Location of S
for k being natural number holds loc -' k = il. S,((locnum loc) -' k);

theorem :: AMISTD_1:60

for N being with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite standard AMI-Struct of NAT ,N
for l being Instruction-Location of S holds l -' 0 = l

proof end;

theorem Th61: :: AMISTD_1:61

for k being natural number
for N being with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite standard AMI-Struct of NAT ,N
for l being Instruction-Location of S holds (l + k) -' k = l

proof end;

theorem :: AMISTD_1:62

canceled;

theorem :: AMISTD_1:63

for k being natural number
for N being with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite standard AMI-Struct of NAT ,N
for l1, l2 being Instruction-Location of S holds
( Start-At (l1 + k) = Start-At (l2 + k) iff Start-At l1 = Start-At l2 )

proof end;

theorem :: AMISTD_1:64

for k being natural number
for N being with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite standard AMI-Struct of NAT ,N
for l1, l2 being Instruction-Location of S st Start-At l1 = Start-At l2 holds
Start-At (l1 -' k) = Start-At (l2 -' k)

proof end;