:: 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
 ( ( the Execution of S . i) . s is Function-like & ( the Execution of S . i) . s is Relation-like )
proofend;
end;

registration
let N be with_zero set ;
cluster non empty with_non-empty_values for AMI-Struct over N;
existence
 ex b1 being AMI-Struct over N st
( not b1 is empty & b1 is with_non-empty_values )
proofend;
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;
attrT 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_:_
 for N being with_zero set
for S being non empty with_non-empty_values AMI-Struct over N
for T being InsType of the InstructionsF 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 in Data-Locations holds
(Exec (I,s)) . o = s . o );

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;
attrI is jump-only  means :: AMISTD_1:def 2
 InsCode I is jump-only ;
end;

:: deftheorem  defines jump-only AMISTD_1:def_2_:_
 for N being with_zero set
for S being non empty with_non-empty_values AMI-Struct over N
for I being Instruction of S holds
( I is jump-only iff InsCode I is jump-only );

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
  {  (IC (Exec (i,ss))) where ss is Element of product (the_Values_of S) : IC ss = l  }  is Subset of NAT
proofend;
end;

:: deftheorem  defines NIC AMISTD_1:def_3_:_
 for N being 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 Element of the InstructionsF of S holds NIC (i,l) =  {  (IC (Exec (i,ss))) where ss is Element of product (the_Values_of S) : IC ss = l  }  ;

Lm1: now__::_thesis:_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
for_l_being_Element_of_NAT_
for_s_being_State_of_S
for_P_being_Instruction-Sequence_of_S_holds_IC_(Following_((P_+*_(l,i)),(s_+*_((IC_),l))))_in_NIC_(i,l)
let N be with_zero set ; ::_thesis: 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
for l being Element of NAT
for s being State of S
for P being Instruction-Sequence of S holds IC (Following ((P +* (l,i)),(s +* ((IC ),l)))) in NIC (i,l)
let S be non empty with_non-empty_values IC-Ins-separated AMI-Struct over N; ::_thesis: for i being Element of the InstructionsF of S
for l being Element of NAT
for s being State of S
for P being Instruction-Sequence of S holds IC (Following ((P +* (l,i)),(s +* ((IC ),l)))) in NIC (i,l)
let i be Element of the InstructionsF of S; ::_thesis: for l being Element of NAT
for s being State of S
for P being Instruction-Sequence of S holds IC (Following ((P +* (l,i)),(s +* ((IC ),l)))) in NIC (i,l)
let l be Element of NAT ; ::_thesis: for s being State of S
for P being Instruction-Sequence of S holds IC (Following ((P +* (l,i)),(s +* ((IC ),l)))) in NIC (i,l)
let s be State of S; ::_thesis: for P being Instruction-Sequence of S holds IC (Following ((P +* (l,i)),(s +* ((IC ),l)))) in NIC (i,l)
let P be Instruction-Sequence of S; ::_thesis: IC (Following ((P +* (l,i)),(s +* ((IC ),l)))) in NIC (i,l)
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: verum
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
 not NIC (i,l) is empty 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
 meet  {  (NIC (i,l)) where l is Element of NAT : verum  }  is Subset of NAT
proofend;
end;

:: deftheorem  defines JUMP AMISTD_1:def_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 Element of the InstructionsF of S holds JUMP i = meet  {  (NIC (i,l)) where l is Element of NAT : verum  }  ;

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
 union  {  ((NIC (i,l)) \ (JUMP i)) where i is Element of the InstructionsF of S : verum  }  is Subset of NAT
proofend;
end;

:: deftheorem  defines SUCC AMISTD_1:def_5_:_
 for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N
for l being Nat holds SUCC (l,S) = union  {  ((NIC (i,l)) \ (JUMP i)) where i is Element of the InstructionsF of S : verum  }  ;

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

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

begin

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 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 &amp; f /. (len f) = n &amp; ( for n being Element of NAT st 1 <= n &amp; n < len f holds
f /. (n + 1) in SUCC ((f /. n),S) ) ) );
end;

:: deftheorem Def6 defines standard AMISTD_1:def_6_:_
 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 m, n being Element of NAT holds
( m <= n iff ex f being non empty FinSequence of NAT st
( f /. 1 = m &amp; f /. (len f) = n &amp; ( for n being Element of NAT st 1 <= n &amp; n < len f holds
f /. (n + 1) in SUCC ((f /. n),S) ) ) ) );

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 &amp; f /. (len f) = k &amp; ( for n being Element of NAT st 1 <= n &amp; n < len f holds
f /. (n + 1) in SUCC ((f /. n),S) ) )
proofend;

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) &amp; ( for j being Element of NAT st j in SUCC (k,S) holds
k <= j ) ) )
proofend;

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} &amp; the ZeroF of it = 0 &amp; the InstructionsF of it = {[0,0,0],[1,0,0]} &amp; the Object-Kind of it = 0 .--> 0 &amp; the ValuesF of it = N --> NAT &amp; 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))) ) &amp; the Execution of it = ([1,0,0] .--> f) +* ([0,0,0] .--> (id (product (the_Values_of it)))) ) );
existence
 ex b1 being strict AMI-Struct over N st
( the carrier of b1 = {0} &amp; the ZeroF of b1 = 0 &amp; the InstructionsF of b1 = {[0,0,0],[1,0,0]} &amp; the Object-Kind of b1 = 0 .--> 0 &amp; the ValuesF of b1 = N --> NAT &amp; ex f being Function of (product (the_Values_of b1)),(product (the_Values_of b1)) st
( ( for s being Element of product (the_Values_of b1) holds f . s = s +* (0 .--> (succ (s . 0))) ) &amp; the Execution of b1 = ([1,0,0] .--> f) +* ([0,0,0] .--> (id (product (the_Values_of b1)))) ) )
proofend;
uniqueness
 for b1, b2 being strict AMI-Struct over N st the carrier of b1 = {0} &amp; the ZeroF of b1 = 0 &amp; the InstructionsF of b1 = {[0,0,0],[1,0,0]} &amp; the Object-Kind of b1 = 0 .--> 0 &amp; the ValuesF of b1 = N --> NAT &amp; ex f being Function of (product (the_Values_of b1)),(product (the_Values_of b1)) st
( ( for s being Element of product (the_Values_of b1) holds f . s = s +* (0 .--> (succ (s . 0))) ) &amp; the Execution of b1 = ([1,0,0] .--> f) +* ([0,0,0] .--> (id (product (the_Values_of b1)))) ) &amp; the carrier of b2 = {0} &amp; the ZeroF of b2 = 0 &amp; the InstructionsF of b2 = {[0,0,0],[1,0,0]} &amp; the Object-Kind of b2 = 0 .--> 0 &amp; the ValuesF of b2 = N --> NAT &amp; ex f being Function of (product (the_Values_of b2)),(product (the_Values_of b2)) st
( ( for s being Element of product (the_Values_of b2) holds f . s = s +* (0 .--> (succ (s . 0))) ) &amp; the Execution of b2 = ([1,0,0] .--> f) +* ([0,0,0] .--> (id (product (the_Values_of b2)))) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def7 defines STC AMISTD_1:def_7_:_
 for N being with_zero set
for b2 being strict AMI-Struct over N holds
( b2 = STC N iff ( the carrier of b2 = {0} &amp; the ZeroF of b2 = 0 &amp; the InstructionsF of b2 = {[0,0,0],[1,0,0]} &amp; the Object-Kind of b2 = 0 .--> 0 &amp; the ValuesF of b2 = N --> NAT &amp; ex f being Function of (product (the_Values_of b2)),(product (the_Values_of b2)) st
( ( for s being Element of product (the_Values_of b2) holds f . s = s +* (0 .--> (succ (s . 0))) ) &amp; the Execution of b2 = ([1,0,0] .--> f) +* ([0,0,0] .--> (id (product (the_Values_of b2)))) ) ) );

registration
let N be with_zero set ;
cluster STC N ->  non empty finite strict ;
coherence
 ( STC N is finite &amp; not STC N is empty ) by Def7;
end;

registration
let N be with_zero set ;
cluster STC N ->  with_non-empty_values strict ;
coherence
 STC N is with_non-empty_values
proofend;
end;

registration
let N be with_zero set ;
cluster STC N ->  IC-Ins-separated strict ;
coherence
 STC N is IC-Ins-separated
proofend;
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)
proofend;

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

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

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

theorem :: AMISTD_1:7
for N being with_zero set
for i being Instruction of (STC N) holds i is jump-only
proofend;

registration
let N be with_zero set ;
cluster  ->  ins-loc-free for Element of the InstructionsF of (STC N);
coherence
 for b1 being Instruction of (STC N) holds b1 is ins-loc-free
proofend;
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 &amp; InsCode i = 1 holds
NIC (i,l) = {(z + 1)}
proofend;

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

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

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

registration
let N be with_zero set ;
cluster STC N ->  strict halting ;
coherence
 STC N is halting
proofend;
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
 ex b1 being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N st
( b1 is standard &amp; b1 is halting )
proofend;
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;
attri 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_:_
 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 sequential iff for s being State of S holds (Exec (i,s)) . (IC ) = succ (IC s) );

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

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
 for b1 being Instruction of S st b1 is sequential holds
not b1 is halting
proofend;
cluster halting  ->  non sequential for Element of the InstructionsF of S;
coherence
 for b1 being Instruction of S st b1 is halting holds
not b1 is sequential ;
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
proofend;

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;
attrF 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_:_
 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 l being Element of NAT st l in dom F holds
NIC ((F /. l),l) c= dom F );

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;
attrF 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_:_
 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 NAT -defined the InstructionsF of b2 -valued Function holds
( F is paraclosed iff 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 );

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;
attrF 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_:_
 for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N
for F being NAT -defined the InstructionsF of b2 -valued Function holds
( F is parahalting iff for s being 0 -started State of S
for P being Instruction-Sequence of S st F c= P holds
P halts_on s );

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

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

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 b2 -valued finite Function st F is really-closed &amp; 0 in dom F holds
F is paraclosed
proofend;

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

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
 for b1 being NAT -defined the InstructionsF of S -valued finite Function st b1 is really-closed &amp; b1 is initial &amp; not b1 is empty holds
b1 is paraclosed
proofend;
end;

Lm7: now__::_thesis:_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_
(_<%(halt_S)%>_._(LastLoc_<%(halt_S)%>)_=_halt_S_&amp;_(_for_l_being_Nat_st_<%(halt_S)%>_._l_=_halt_S_&amp;_l_in_dom_<%(halt_S)%>_holds_
l_=_LastLoc_<%(halt_S)%>_)_)
let N be with_zero set ; ::_thesis: for S being non empty with_non-empty_values IC-Ins-separated halting standard AMI-Struct over N holds
( <%(halt S)%> . (LastLoc <%(halt S)%>) = halt S &amp; ( for l being Nat st <%(halt S)%> . l = halt S &amp; l in dom <%(halt S)%> holds
l = LastLoc <%(halt S)%> ) )
let S be non empty with_non-empty_values IC-Ins-separated halting standard AMI-Struct over N; ::_thesis: ( <%(halt S)%> . (LastLoc <%(halt S)%>) = halt S &amp; ( for l being Nat st <%(halt S)%> . l = halt S &amp; l in dom <%(halt S)%> holds
l = LastLoc <%(halt S)%> ) )
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: for l being Nat st <%(halt S)%> . l = halt S &amp; l in dom <%(halt S)%> holds
l = LastLoc <%(halt S)%>
let l be Nat; ::_thesis: ( <%(halt S)%> . l = halt S &amp; l in dom <%(halt S)%> implies l = LastLoc <%(halt S)%> )
assume  <%(halt S)%> . l = halt S ; ::_thesis: ( l in dom <%(halt S)%> implies l = LastLoc <%(halt S)%> )
assume  l in dom <%(halt S)%> ; ::_thesis: l = LastLoc <%(halt S)%>
hence  l = LastLoc <%(halt S)%> by A1, A3, TARSKI:def_1; ::_thesis: verum
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
 ex b1 being NAT -defined the InstructionsF of S -valued finite Function st
( b1 is trivial &amp; b1 is really-closed &amp; b1 is initial &amp; not b1 is empty )
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 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
 ex b1 being NAT -defined the InstructionsF of S -valued non empty finite initial Function st
( b1 is halt-ending &amp; b1 is unique-halt &amp; b1 is trivial &amp; b1 is really-closed )
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 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
 ex b1 being MacroInstruction of S st b1 is really-closed
proofend;
end;

theorem :: AMISTD_1:17
for N being with_zero set
for i being Instruction of (Trivial-AMI N) holds i is halting
proofend;

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

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

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

registration
let N be with_zero set ;
let p be PartState of (STC N);
cluster DataPart p ->  empty ;
coherence
 DataPart p is empty
proofend;
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
 ex b1 being NAT -defined the InstructionsF of S -valued non empty finite non halt-free Function st b1 is parahalting
proofend;
end;