:: A Mathematical Model of CPU
::  by Yatsuka Nakamura and Andrzej Trybulec
::
:: Received October 14, 1992
:: Copyright (c) 1992 Association of Mizar Users

environ

 vocabularies BOOLE, FUNCT_2, FUNCT_1, RELAT_1, FUNCOP_1, CAT_1, FUNCT_4,
      CARD_3, TARSKI, FRAENKEL, PARTFUN1, FINSET_1, AMI_1, NAT_1, NEWTON,
      AMI_5, MCART_1, AMISTD_2, FUNCT_3, FINSEQ_1, FINSEQ_4, GRAPH_2, TREES_2,
      ORDINAL1, AMI_3, SCM_1, ARYTM_1, FUNCT_7;
 notations TARSKI, XBOOLE_0, ZFMISC_1, MCART_1, SUBSET_1, SETFAM_1, ORDINAL1,
      NUMBERS, CARD_3, XCMPLX_0, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2, BINOP_1,
      FINSET_1, NAT_1, FRAENKEL, FUNCOP_1, FUNCT_4, FINSEQ_1, FINSEQ_4,
      FUNCT_7, GRAPH_2, DOMAIN_1, TREES_1, TREES_2, STRUCT_0, XXREAL_0;
 constructors BINOP_1, SETFAM_1, PARTFUN1, DOMAIN_1, FUNCT_4, FRAENKEL,
      XXREAL_0, NAT_1, FUNCT_7, INT_1, CARD_3, CQC_LANG, STRUCT_0, FINSEQ_4,
      GRAPH_2, TREES_2;
 registrations XBOOLE_0, SUBSET_1, SETFAM_1, RELAT_1, FUNCT_1, ORDINAL1,
      FUNCT_2, FUNCOP_1, FUNCT_4, ARYTM_3, FINSET_1, FRAENKEL, XREAL_0,
      FINSEQ_1, CARD_3, STRUCT_0, ALTCAT_1, AFINSQ_1, TREES_2, TREES_1, INT_1;
 requirements NUMERALS, BOOLE, SUBSET, ARITHM;


begin :: General concepts

definition let N be set;
 struct (1-sorted) AMI-Struct over N
  (# carrier -> set,
    Instruction-Counter -> Element of the carrier,
    Instruction-Locations -> Subset of the carrier,
    Instructions -> non empty set,
    Object-Kind ->
     Function of the carrier,
                 N \/ { the Instructions, the Instruction-Locations },
    Execution ->
     Function of the Instructions,
       Funcs(product the Object-Kind, product the Object-Kind)
  #);
end;

definition let N be set;
 canceled;

 func Trivial-AMI N -> strict AMI-Struct over N means
:: AMI_1:def 2

  the carrier of it = {0,1} &
  the Instruction-Counter of it = 0 &
  the Instruction-Locations of it = {1} &
  the Instructions of it = {[0,{}]} &
  the Object-Kind of it = (0,1) --> ({1},{[0,{}]}) &
  the Execution of it = [0,{}] .--> id product (0,1) --> ({1},{[0,{}]});
end;

definition let N be set; let S be AMI-Struct over N;
 attr S is void means
:: AMI_1:def 3
 the Instruction-Locations of S is empty;
end;

registration let N be set;
 cluster Trivial-AMI N -> non empty non void;
end;

registration let N be set;
 cluster non empty non void AMI-Struct over N;
end;

registration let N be set; let S be non void AMI-Struct over N;
 cluster the Instruction-Locations of S -> non empty;
end;

definition let N be set; let S be non empty AMI-Struct over N;
 mode Object of S is Element of S;
end;

definition let N be set; let S be non empty non void AMI-Struct over N;
 mode Instruction-Location of S -> Element of the Instruction-Locations of S
      means
:: AMI_1:def 4
  not contradiction;
end;

definition let N be set; let S be AMI-Struct over N;
 mode Instruction of S is Element of the Instructions of S;
end;

definition let N be set; let S be non empty AMI-Struct over N;
 func IC S -> Object of S equals
:: AMI_1:def 5
   the Instruction-Counter of S;
end;

definition let N be set; let S be non empty AMI-Struct over N;
 let o be Object of S;
 func ObjectKind o ->
  Element of N \/ { the Instructions of S, the Instruction-Locations of S }
   equals
:: AMI_1:def 6
   (the Object-Kind of S).o;
end;

definition let N be set; let S be AMI-Struct over N;
  mode State of S is Element of product the Object-Kind of S;
end;

definition let N be with_non-empty_elements set;
 let S be non void AMI-Struct over N;
 let I be Instruction of S, s be State of S;
 func Exec(I,s) -> State of S equals
:: AMI_1:def 7
     ((the Execution of S).I).s;
end;

reserve N for with_non-empty_elements set;

definition let N; let S be non void AMI-Struct over N;
           let I be Instruction of S;
 attr I is halting means
:: AMI_1:def 8
  for s being State of S holds Exec(I,s) = s;
end;

definition let N; let S be non void AMI-Struct over N;
 attr S is halting means
:: AMI_1:def 9
  ex I being Instruction of S st I is halting;
end;

reserve E for set;

canceled 5;

theorem :: AMI_1:6
 Trivial-AMI N is halting;

registration let N;
 cluster Trivial-AMI N -> halting;
end;

registration let N;
 cluster halting (non void AMI-Struct over N);
end;

registration let N; let S be halting (non void AMI-Struct over N);
 cluster halting Instruction of S;
end;

definition let N; let S be halting (non void AMI-Struct over N);
 func halt S -> Instruction of S equals
:: AMI_1:def 10
   choose { I where I is Instruction of S: I is halting };
end;

registration let N; let S be halting (non void AMI-Struct over N);
 cluster halt S -> halting;
end;

definition let N be set; let IT be non empty AMI-Struct over N;
 attr IT is IC-Ins-separated means
:: AMI_1:def 11
  ObjectKind IC IT = the Instruction-Locations of IT;
end;

definition let N be with_non-empty_elements set;
 let IT be non empty non void AMI-Struct over N;
canceled;
 attr IT is steady-programmed means
:: AMI_1:def 13
  for s being State of IT, i being Instruction of IT,
      l being Instruction-Location of IT
   holds Exec(i,s).l = s.l;
end;

definition let N be set; let IT be non empty non void AMI-Struct over N;
 attr IT is definite means
:: AMI_1:def 14
  for l being Instruction-Location of IT holds
   ObjectKind l = the Instructions of IT;
end;

theorem :: AMI_1:7
 Trivial-AMI E is IC-Ins-separated;

canceled;

theorem :: AMI_1:9
 for s1, s2 being State of Trivial-AMI E holds s1=s2;

theorem :: AMI_1:10
 Trivial-AMI N is steady-programmed;

theorem :: AMI_1:11
 Trivial-AMI E is definite;

registration let E be set;
  cluster Trivial-AMI E -> IC-Ins-separated definite;
end;

registration let N be with_non-empty_elements set;
  cluster Trivial-AMI N -> steady-programmed;
end;

registration let E be set;
 cluster strict AMI-Struct over E;
end;

registration let M be set;
 cluster IC-Ins-separated definite strict
              (non empty non void AMI-Struct over M);
end;

registration let N;
 cluster IC-Ins-separated halting steady-programmed definite
         strict (non empty non void AMI-Struct over N);
end;

definition let N be with_non-empty_elements set;
  let S be IC-Ins-separated (non empty non void AMI-Struct over N);
 let s be State of S;
 func IC s -> Instruction-Location of S equals
:: AMI_1:def 15
   s.IC S;
end;

begin :: General theory

reserve x,y,z,A,B for set,
        f,g,h for Function,
        i,j,k for Element of NAT;

definition let N;
 canceled;
 let S be IC-Ins-separated definite (non empty non void AMI-Struct over N);
 let s be State of S;
 func CurInstr s -> Instruction of S equals
:: AMI_1:def 17
  s.IC s;
end;

definition let N;
 let S be IC-Ins-separated definite (non empty non void AMI-Struct over N);
 let s be State of S;
 func Following s -> State of S equals
:: AMI_1:def 18
  Exec(CurInstr s,s);
end;

definition let N;
 let S be IC-Ins-separated definite (non empty non void AMI-Struct over N);
 let s be State of S;
 func Computation s -> Function of NAT, product the Object-Kind of S
  means
:: AMI_1:def 19

  it.0 = s &
  for i holds it.(i+1) = Following(it.i);
end;

definition let N; let S be non void AMI-Struct over N;
 let f be Function of NAT, product the Object-Kind of S;
 let k;
 redefine func f.k -> State of S;
end;

definition let N;
 let S be halting IC-Ins-separated definite
       (non empty non void AMI-Struct over N);
 let IT be State of S;
 attr IT is halting means
:: AMI_1:def 20
 ex k st CurInstr((Computation IT).k) = halt S;
end;

definition let N be set; let IT be AMI-Struct over N;
 attr IT is realistic means
:: AMI_1:def 21

  not the Instruction-Counter of IT in the Instruction-Locations of IT;
end;

canceled 36;

theorem :: AMI_1:48
  for S being IC-Ins-separated definite (non empty non void AMI-Struct over E)
  st S is realistic holds
  not ex l being Instruction-Location of S st IC S = l;

 reserve
   S for IC-Ins-separated definite (non empty non void AMI-Struct over N),
   s for State of S;

canceled 2;

theorem :: AMI_1:51
 for k holds
 (Computation s).(i+k) = (Computation (Computation s).i).k;

theorem :: AMI_1:52
 i <= j implies
  for N for S being
   halting IC-Ins-separated definite (non empty non void AMI-Struct over N)
  for s being State of S st CurInstr((Computation s).i) = halt S
   holds (Computation s).j = (Computation s).i;

definition let N;
 let S be halting IC-Ins-separated definite
     (non empty non void AMI-Struct over N);
 let s be State of S such that
 s is halting;
 func Result s -> State of S means
:: AMI_1:def 22
  ex k st it = (Computation s).k & CurInstr(it) = halt S;
end;

theorem :: AMI_1:53
     for S being steady-programmed
  IC-Ins-separated definite (non empty non void AMI-Struct over N)
 for s being State of S, i be Instruction-Location of S
  holds s.i = (Following s).i;

definition let N; let S be definite (non empty non void AMI-Struct over N);
 let s be State of S, l be Instruction-Location of S;
 redefine func s.l -> Instruction of S;
end;

theorem :: AMI_1:54
 for S being steady-programmed IC-Ins-separated definite
   (non empty non void AMI-Struct over N)
 for s being State of S, i be Instruction-Location of S, k
  holds s.i = (Computation s).k.i;

theorem :: AMI_1:55
     for S being steady-programmed IC-Ins-separated definite
    (non empty non void AMI-Struct over N)
 for s being State of S
  holds (Computation s).(k+1)
    = Exec(s.(IC (Computation s).k),(Computation s).k);

theorem :: AMI_1:56
 for S being steady-programmed IC-Ins-separated
 halting definite (non empty non void AMI-Struct over N)
 for s being State of S, k st s.IC (Computation s).k = halt S
  holds Result s = (Computation s).k;

theorem :: AMI_1:57
     for S being steady-programmed IC-Ins-separated
 halting definite (non empty non void AMI-Struct over N)
 for s being State of S st
   ex k st s.IC (Computation s).k = halt S
 for i holds Result s = Result (Computation s).i;

registration let N;
  let S be non empty non void AMI-Struct over N, o be Object of S;
  cluster ObjectKind o -> non empty;
end;

begin :: Finite substates

definition let N be set; let S be AMI-Struct over N;
 func FinPartSt S -> Subset of sproduct the Object-Kind of S equals
:: AMI_1:def 23
      { p where p is Element of sproduct the Object-Kind of S: p is finite };
end;

registration let N be set; let S be AMI-Struct over N;
 cluster finite Element of sproduct the Object-Kind of S;
end;

registration let N be set; let S be AMI-Struct over N;
 cluster FinPartSt S -> non empty functional;
end;

definition let N be set; let S be AMI-Struct over N;
 mode FinPartState of S is Element of FinPartSt S;
end;

registration let N be set; let S be AMI-Struct over N;
 cluster -> finite FinPartState of S;
end;

definition let N;
 canceled;
 let S be IC-Ins-separated definite (non empty non void AMI-Struct over N);
 let IT be FinPartState of S;
 attr IT is autonomic means
:: AMI_1:def 25
  for s1,s2 being State of S st IT c= s1 & IT c= s2
   for i holds (Computation s1).i|dom IT = (Computation s2).i|dom IT;
end;

definition let N;
 let S be halting IC-Ins-separated definite
     (non empty non void AMI-Struct over N);
 let IT be FinPartState of S;
 attr IT is halting means
:: AMI_1:def 26
  for s being State of S st IT c= s holds s is halting;
end;

definition let N;
 let IT be IC-Ins-separated definite (non empty non void AMI-Struct over N);
 attr IT is programmable means
:: AMI_1:def 27
 ex s being FinPartState of IT st s is non empty autonomic;
end;

theorem :: AMI_1:58
 for S being IC-Ins-separated definite (non empty non void AMI-Struct over N)
 for A,B being set, la,lb being Object of S st
  ObjectKind la = A & ObjectKind lb = B
 for a being Element of A, b being Element of B holds
  (la,lb) --> (a,b) is FinPartState of S;

theorem :: AMI_1:59
 for S being IC-Ins-separated definite (non empty non void AMI-Struct over N)
 for A being set, la being Object of S st ObjectKind la = A
 for a being Element of A holds la .--> a is FinPartState of S;

definition let N;
 let S be IC-Ins-separated definite (non empty non void AMI-Struct over N);
 let la be Object of S;
 let a be Element of ObjectKind la;
 redefine func la .--> a -> FinPartState of S;
end;

definition let N;
 let S be IC-Ins-separated definite (non empty non void AMI-Struct over N);
 let la,lb be Object of S;
 let a be Element of ObjectKind la,
     b be Element of ObjectKind lb;
 redefine func (la,lb) --> (a,b) -> FinPartState of S;
end;

theorem :: AMI_1:60
 Trivial-AMI E is realistic;

theorem :: AMI_1:61
 Trivial-AMI N is programmable;

registration let E;
  cluster Trivial-AMI E -> realistic;
end;

registration let N;
  cluster Trivial-AMI N -> programmable;
end;

registration let E;
 cluster realistic strict AMI-Struct over E;
end;

registration let M be set;
 cluster realistic strict IC-Ins-separated
 definite (non empty non void AMI-Struct over M);
end;

registration let N;
 cluster halting steady-programmed realistic programmable
         strict (IC-Ins-separated definite
         (non empty non void AMI-Struct over N));
end;

theorem :: AMI_1:62
 for S being non void AMI-Struct over N,
     s being State of S, p being FinPartState of S
  holds s|dom p is FinPartState of S;

theorem :: AMI_1:63
 for N being set for S being AMI-Struct over N holds {} is FinPartState of S;

registration let N;
 let S be programmable
  (IC-Ins-separated definite (non empty non void AMI-Struct over N));
 cluster non empty autonomic FinPartState of S;
end;

definition let N be set;
 let S be AMI-Struct over N;
 let f,g be FinPartState of S;
 redefine func f +* g -> FinPartState of S;
end;

begin :: Preprograms

theorem :: AMI_1:64
for S being halting realistic IC-Ins-separated definite
  (non empty non void AMI-Struct over N)
for loc being Instruction-Location of S
for l being Element of ObjectKind IC S st l = loc
for h being Element of ObjectKind loc st h = halt S
for s being State of S st (IC S,loc) --> (l, h) c= s
 holds CurInstr s = halt S;

theorem :: AMI_1:65
for S being halting realistic IC-Ins-separated definite
   (non empty non void AMI-Struct over N)
for loc being Instruction-Location of S
for l being Element of ObjectKind IC S st l = loc
for h being Element of ObjectKind loc st h = halt S
 holds (IC S,loc) --> (l, h) is halting;

theorem :: AMI_1:66
for S being realistic halting IC-Ins-separated definite
 (non empty non void AMI-Struct over N)
for loc being Instruction-Location of S
for l being Element of ObjectKind IC S st l = loc
for h being Element of ObjectKind loc st h = halt S
for s being State of S st (IC S,loc) --> (l, h) c= s
for i holds (Computation s).i = s;

theorem :: AMI_1:67
for S be realistic halting IC-Ins-separated definite
   (non empty non void AMI-Struct over N)
for loc being Instruction-Location of S
for l being Element of ObjectKind IC S st l = loc
for h being Element of ObjectKind loc st h = halt S
 holds (IC S,loc) --> (l, h) is autonomic;

registration let N;
 let S be realistic halting IC-Ins-separated definite
  (non empty non void AMI-Struct over N);
 cluster autonomic halting FinPartState of S;
end;

definition let N;
 let S be realistic halting IC-Ins-separated definite
  (non empty non void AMI-Struct over N);
 mode pre-program of S is autonomic halting FinPartState of S;
end;

definition let N;
 let S be realistic halting IC-Ins-separated definite
  (non empty non void AMI-Struct over N);
 let s be FinPartState of S;
 assume
 s is pre-program of S;
 func Result(s) -> FinPartState of S means
:: AMI_1:def 28
     for s' being State of S st s c= s' holds it = (Result s')|dom s;
end;

begin :: Computability

definition let N;
 let S be realistic halting IC-Ins-separated definite
  (non empty non void AMI-Struct over N);
 let p be FinPartState of S, F be Function;
  pred p computes F means
:: AMI_1:def 29

  for x being set st x in dom F ex s being FinPartState of S st x = s &
   p +* s is pre-program of S & F.s c= Result(p +* s);
 end;

notation let N;
 let S be realistic halting IC-Ins-separated definite
  (non empty non void AMI-Struct over N);
 let p be FinPartState of S, F be Function;
  antonym p does_not_compute F for p computes F;
end;

theorem :: AMI_1:68
 for S being realistic halting IC-Ins-separated definite
    (non empty non void AMI-Struct over N)
 for p being FinPartState of S
  holds p computes {};

theorem :: AMI_1:69
 for S being realistic halting IC-Ins-separated definite
  (non empty non void AMI-Struct over N)
 for p being FinPartState of S
  holds p is pre-program of S iff p computes {} .--> Result(p);

theorem :: AMI_1:70
 for S being realistic halting IC-Ins-separated definite
  (non empty non void AMI-Struct over N)
 for p being FinPartState of S
  holds p is pre-program of S iff p computes {} .--> {};

definition let N;
 let S be realistic halting IC-Ins-separated definite
    (non empty non void AMI-Struct over N);
 let IT be PartFunc of FinPartSt S, FinPartSt S;
 attr IT is computable means
:: AMI_1:def 30
 ex p being FinPartState of S st p computes IT;
end;

theorem :: AMI_1:71
 for S being realistic halting IC-Ins-separated definite
  (non empty non void AMI-Struct over N)
 for F being PartFunc of FinPartSt S, FinPartSt S st F = {}
  holds F is computable;

theorem :: AMI_1:72
 for S being realistic halting IC-Ins-separated definite
  (non empty non void AMI-Struct over N)
 for F being PartFunc of FinPartSt S, FinPartSt S st F = {} .--> {}
  holds F is computable;

theorem :: AMI_1:73
 for S being realistic halting IC-Ins-separated definite
  (non empty non void AMI-Struct over N)
 for p being pre-program of S
 for F being PartFunc of FinPartSt S, FinPartSt S st F = {} .--> Result(p)
  holds F is computable;

definition let N;
 let S be realistic halting IC-Ins-separated definite
  (non empty non void AMI-Struct over N);
 let F be PartFunc of FinPartSt S, FinPartSt S such that
 F is computable;
  mode Program of F -> FinPartState of S means
:: AMI_1:def 31
it computes F;
end;

theorem :: AMI_1:74
     for S being realistic halting IC-Ins-separated definite
  (non empty non void AMI-Struct over N)
 for F being PartFunc of FinPartSt S, FinPartSt S st F = {}
 for p being FinPartState of S
  holds p is Program of F;

theorem :: AMI_1:75
     for S being realistic halting IC-Ins-separated definite
  (non empty non void AMI-Struct over N)
 for F being PartFunc of FinPartSt S, FinPartSt S st F = {} .--> {}
 for p being pre-program of S holds p is Program of F;

theorem :: AMI_1:76
     for S being realistic halting IC-Ins-separated definite
  (non empty non void AMI-Struct over N)
 for p being pre-program of S
 for F being PartFunc of FinPartSt S, FinPartSt S st F = {} .--> Result p
  holds p is Program of F;

begin :: InsType & InsCode

notation let x;
 synonym InsCode x for x`1;
 synonym AddressPart x for x`2;
end;

definition
 let N be set, S be AMI-Struct over N;
 attr S is standard-ins means
:: AMI_1:def 32
 the Instructions of S c= [: NAT, ((union N) \/ the carrier of S)* :];
end;

registration let N be set;
 cluster Trivial-AMI N -> standard-ins;
end;

registration let N be set;
 cluster standard-ins non empty non void AMI-Struct over N;
end;

registration
 let N be set, S be standard-ins AMI-Struct over N;
 cluster the Instructions of S -> Relation-like;
end;

definition
 let N be set, S be standard-ins AMI-Struct over N;
 func InsCodes S equals
:: AMI_1:def 33
   dom the Instructions of S;
end;

definition
 let N be set, S be standard-ins AMI-Struct over N;
 mode InsType of S is Element of InsCodes S;
end;

definition
 let N be set, S be standard-ins AMI-Struct over N;
 let I be Element of the Instructions of S;
 redefine func InsCode I -> InsType of S;
end;

theorem :: AMI_1:77
  for N being set, S being AMI-Struct over N
 for x being finite Element of sproduct the Object-Kind of S
         holds x in FinPartSt S;

begin :: On the instruction locations

definition let N be set, S be AMI-Struct over N;
 mode IL-FinSequence of S -> FinSequence of the Instruction-Locations of S
  means
:: AMI_1:def 34
 not contradiction;
end;

reserve N for set, S for non empty non void AMI-Struct over N;

definition let N,S;
 let f be IL-FinSequence of S; let x be set;
 func f/.x -> Instruction-Location of S equals
:: AMI_1:def 35
    f/.x;
end;

definition let N,S; let l1 be Instruction-Location of S;
 redefine func <*l1*> -> IL-FinSequence of S;
 let l2 be Instruction-Location of S;
 redefine func <*l1,l2*> -> IL-FinSequence of S;
end;

registration let N,S;
 cluster non empty IL-FinSequence of S;
end;

definition let N,S;
 let f1,f2 be IL-FinSequence of S;
 redefine func f1^'f2 -> IL-FinSequence of S;
end;

definition let D be set;
 let N, S;
 mode IL-Function of D,S -> Function of D, the Instruction-Locations of S means
:: AMI_1:def 36
   not contradiction;
end;

definition let D be non empty set;
 let N,S;
 let f be IL-Function of D,S, d be Element of D;
 redefine func f.d -> Instruction-Location of S;
end;

definition let N,S;
 mode IL-DecoratedTree of S -> DecoratedTree of the Instruction-Locations of S
      means
:: AMI_1:def 37
   not contradiction;
end;

definition let N,S; let T be IL-DecoratedTree of S;
 let x be set such that
 x in dom T;
 func T.x -> Instruction-Location of S equals
:: AMI_1:def 38
   T.x;
end;

scheme :: AMI_1:sch 1
 ILFraenkelFin {N() -> set,
      S() -> non empty non void AMI-Struct over N(),
      X() -> set, F(set) -> set }:
 { F(w) where w is Instruction-Location of S(): w in X() } is finite
provided
  X() is finite;

scheme :: AMI_1:sch 2
 {N,D()-> set, S()-> non empty non void AMI-Struct over N(),
        F(set) -> set,
        T() -> Instruction-Location of S(),
        P[set,set]}:
  { F(i) where i is Element of D():
    ex l being Instruction-Location of S() st l = T() & P[i,l] }
    = { F(j) where j is Element of D(): P[j,T()] };

begin :: Addenda

begin :: Some Remarks on AMI-Struct, moved from AMI_3, 2007.07.22

reserve N for set;

registration let N be set; let S be AMI-Struct over N;
 cluster FinPartSt S -> non empty;
end;

definition let N be with_non-empty_elements set;
   let S be IC-Ins-separated definite (non empty non void AMI-Struct over N);
   let l be Instruction-Location of S;
 func Start-At l -> FinPartState of S equals
:: AMI_1:def 39
  IC S .--> l;
end;

reserve N for with_non-empty_elements set;

definition let N be set; let S be AMI-Struct over N;
 let IT be FinPartState of S;
 attr IT is programmed means
:: AMI_1:def 40
 dom IT c= the Instruction-Locations of S;
end;

registration let N be set; let S be AMI-Struct over N;
 cluster programmed FinPartState of S;
end;

theorem :: AMI_1:78
    for N being set for S being AMI-Struct over N
 for p1,p2 being programmed FinPartState of S
  holds p1 +* p2 is programmed;

theorem :: AMI_1:79
 for S being non void AMI-Struct over N, s being State of S holds
  dom s = the carrier of S;

theorem :: AMI_1:80
 for S being AMI-Struct over N, p being FinPartState of S holds
  dom p c= the carrier of S;

theorem :: AMI_1:81
    for S being steady-programmed IC-Ins-separated definite
   (non empty non void AMI-Struct over N)
 for p being programmed FinPartState of S
 for s being State of S st p c= s
 for k holds p c= (Computation s).k;

definition let N;
 let S be IC-Ins-separated (non empty non void AMI-Struct over N);
 let s be State of S, l be Instruction-Location of S;
 pred s starts_at l means
:: AMI_1:def 41
      IC s = l;
end;

definition let N;
 let S be IC-Ins-separated halting (non empty non void AMI-Struct over N);
 let s be State of S, l be Instruction-Location of S;
 pred s halts_at l means
:: AMI_1:def 42
  s.l = halt S;
end;

theorem :: AMI_1:82
 for S being non void AMI-Struct over N, p being FinPartState of S
  ex s being State of S st p c= s;

definition let N;
  let S be definite IC-Ins-separated (non empty non void AMI-Struct over N);
 let p be FinPartState of S such that
 IC S in dom p;
 func IC p -> Instruction-Location of S equals
:: AMI_1:def 43
  p.IC S;
end;

definition let N;
 let S be definite IC-Ins-separated (non empty non void AMI-Struct over N);
 let p be FinPartState of S, l be Instruction-Location of S;
 pred p starts_at l means
:: AMI_1:def 44
      IC S in dom p & IC p = l;
end;

definition let N;
 let S be definite IC-Ins-separated halting
  (non empty non void AMI-Struct over N);
 let p be FinPartState of S, l be Instruction-Location of S;
 pred p halts_at l means
:: AMI_1:def 45
      l in dom p & p.l = halt S;
end;

theorem :: AMI_1:83
 for S being IC-Ins-separated
 definite steady-programmed halting (non empty non void AMI-Struct over N),
  s being State of S holds
  s is halting iff ex k st s halts_at IC (Computation s).k;

theorem :: AMI_1:84
     for S being IC-Ins-separated
 definite steady-programmed halting (non empty non void AMI-Struct over N),
  s being State of S, p being FinPartState of S,
  l being Instruction-Location of S st p c= s & p halts_at l
   holds s halts_at l;

theorem :: AMI_1:85
 for S being halting steady-programmed IC-Ins-separated
 definite (non empty non void AMI-Struct over N),
     s being State of S, k st s is halting
  holds Result s = (Computation s).k iff s halts_at IC (Computation s).k;

theorem :: AMI_1:86
     for S being steady-programmed IC-Ins-separated definite
       (non empty non void AMI-Struct over N),
     s being State of S, p being programmed FinPartState of S, k
  holds p c= s iff p c= (Computation s).k;

theorem :: AMI_1:87
 for S being halting steady-programmed IC-Ins-separated
 definite (non empty non void AMI-Struct over N),
     s being State of S, k st s halts_at IC (Computation s).k
  holds Result s = (Computation s).k;

theorem :: AMI_1:88
 i <= j implies
  for S being halting steady-programmed IC-Ins-separated
 definite (non empty non void AMI-Struct over N)
  for s being State of S st s halts_at IC (Computation s).i
   holds s halts_at IC (Computation s).j;

theorem :: AMI_1:89 :: AMI_1:46
     i <= j implies
  for S being halting steady-programmed IC-Ins-separated
 definite (non empty non void AMI-Struct over N)
  for s being State of S st s halts_at IC (Computation s).i
   holds (Computation s).j = (Computation s).i;

theorem :: AMI_1:90 :: AMI_2:46
     for S being steady-programmed IC-Ins-separated
 halting definite (non empty non void AMI-Struct over N)
 for s being State of S st ex k st s halts_at IC (Computation s).k
 for i holds Result s = Result (Computation s).i;

theorem :: AMI_1:91
     for S being steady-programmed IC-Ins-separated
 definite halting (non empty non void AMI-Struct over N)
 for s being State of S,l being Instruction-Location of S,k holds
  s halts_at l iff (Computation s).k halts_at l;

theorem :: AMI_1:92
     for S being definite IC-Ins-separated (non empty non void AMI-Struct over
N
),
     p being FinPartState of S, l being Instruction-Location of S
  st p starts_at l
 for s being State of S st p c= s holds s starts_at l;

definition let N;
 let S be definite IC-Ins-separated (non empty non void AMI-Struct over N);
 let l be Instruction-Location of S, I be Element of the Instructions of S;
 redefine func l .--> I -> programmed FinPartState of S;
end;

:: from SCM_1, 2007.07.22, A.T.

definition
let N be with_non-empty_elements set;
 let S be halting IC-Ins-separated definite
    (non empty non void AMI-Struct over N);
 let s be State of S such that
 s is halting;
 func LifeSpan s -> Element of NAT means
:: AMI_1:def 46
  CurInstr((Computation s).it) = halt S &
  for k being Element of NAT st CurInstr((Computation s).k) = halt S
  holds it <= k;
 end;

theorem :: AMI_1:93
 for N being non empty with_non-empty_elements set,
     S be IC-Ins-separated definite halting
       (non empty non void AMI-Struct over N),
     s being State of S, m being Element of NAT
 holds s is halting iff (Computation s).m is halting;

:: from AMI_5, 2007.07.22, A.T.

reserve
  N for with_non-empty_elements set,
  S for IC-Ins-separated definite (non empty non void AMI-Struct over N);

theorem :: AMI_1:94
 for s being State of S holds IC S in dom s;

theorem :: AMI_1:95
     for s being State of S
  holds Start-At(IC s) = s | {IC S};

theorem :: AMI_1:96
  for l be Instruction-Location of S
   holds Start-At l = {[IC S,l]};

theorem :: AMI_1:97
 for p being FinPartState of S,
     s being State of S st IC S in dom p & p c= s
   holds
    IC p = IC s;

definition let N,S;
 let p be FinPartState of S, loc be Instruction-Location of S;
 assume  loc in dom p;
 func pi (p , loc) -> Instruction of S equals
:: AMI_1:def 47
      p.loc;
end;

theorem :: AMI_1:98
 for N being set, S being AMI-Struct over N
 for x being set, p being FinPartState of S st x c= p
  holds x is FinPartState of S;

definition let N be set; let S be AMI-Struct over N;
 let p be FinPartState of S;
 func ProgramPart p -> programmed FinPartState of S equals
:: AMI_1:def 48
   p | the Instruction-Locations of S;
end;

definition let N be set; let S be non empty AMI-Struct over N;
 let p be FinPartState of S;
 func DataPart p -> FinPartState of S equals
:: AMI_1:def 49
   p | ((the carrier of S) \ ({IC S} \/ the Instruction-Locations of S));
end;

definition let N be set, S be non empty AMI-Struct over N;
 let IT be FinPartState of S;
 attr IT is data-only means
:: AMI_1:def 50
 dom IT misses {IC S} \/ the Instruction-Locations of S;
end;

registration let N be set, S be non empty AMI-Struct over N;
 cluster data-only FinPartState of S;
end;

theorem :: AMI_1:99
    for S being steady-programmed IC-Ins-separated definite
      (non empty non void AMI-Struct over N)
 for p being FinPartState of S,
     s being State of S st p c= s
 for i being Element of NAT
  holds ProgramPart p c= (Computation (s)).i;

theorem :: AMI_1:100
 for N being set, S being non empty AMI-Struct over N
 for p being FinPartState of S holds not IC S in dom (DataPart p);

theorem :: AMI_1:101
 for S being IC-Ins-separated definite realistic
      (non empty non void AMI-Struct over N)
 for p being FinPartState of S
  holds not IC S in dom (ProgramPart p);

theorem :: AMI_1:102
    for N being set, S being non empty AMI-Struct over N
   for p being FinPartState of S holds
   {IC S} misses dom (DataPart p);

theorem :: AMI_1:103
     for S being IC-Ins-separated definite realistic
   (non empty non void AMI-Struct over N)
 for p being FinPartState of S
  holds
   {IC S} misses dom (ProgramPart p);

theorem :: AMI_1:104
 for p,q being FinPartState of S
  holds
   dom DataPart p misses dom ProgramPart q;

theorem :: AMI_1:105
   for p being programmed FinPartState of S holds ProgramPart p = p;

theorem :: AMI_1:106
     for p being FinPartState of S,
     l being Instruction-Location of S st l in dom p
  holds l in dom ProgramPart p;

theorem :: AMI_1:107
     for p being data-only FinPartState of S,
     q being FinPartState of S holds
     p c= q iff p c= DataPart(q);

theorem :: AMI_1:108
     for S being IC-Ins-separated definite realistic
    (non empty non void AMI-Struct over N)
 for p being FinPartState of S st IC S in dom p
  holds p = Start-At(IC p) +* ProgramPart p +* DataPart p;

definition let N,S;let IT be PartFunc of FinPartSt S,FinPartSt S;
 attr IT is data-only means
:: AMI_1:def 51
     for p being FinPartState of S st p in dom IT
  holds p is data-only &
   for q being FinPartState of S st q = IT.p holds
    q is data-only;
end;

theorem :: AMI_1:109
     for S being IC-Ins-separated definite realistic
     (non empty non void AMI-Struct over N)
 for p being FinPartState of S st IC S in dom p
  holds p is not programmed;

definition let N; let S be non void AMI-Struct over N;
 let s be State of S;
 let p be FinPartState of S;
 redefine func s +* p -> State of S;
end;

theorem :: AMI_1:110
     for p being FinPartState of S st IC S in dom p
  holds Start-At (IC p) c= p;

theorem :: AMI_1:111
     for s being State of S,
     iloc being Instruction-Location of S
  holds IC (s +* Start-At iloc ) = iloc;

theorem :: AMI_1:112
     for S being IC-Ins-separated definite realistic
     (non empty non void AMI-Struct over N)
 for s being State of S,
     iloc being Instruction-Location of S,
     a    being Instruction-Location of S
  holds s.a = (s +* Start-At iloc).a;

theorem :: AMI_1:113
     for s, t being State of S, A be set
  holds s +* t|A is State of S;

:: from SCMFSA_2, 2007.07.22, A.T.

theorem :: AMI_1:114
  for N being with_non-empty_elements set,
     S being non void AMI-Struct over N,
     s being State of S
      holds the Instruction-Locations of S c= dom s;

theorem :: AMI_1:115
      for N being with_non-empty_elements set,
     S being IC-Ins-separated non void (non empty AMI-Struct over N),
     s being State of S
  holds IC s in dom s;

theorem :: AMI_1:116
      for N being with_non-empty_elements set,
     S being non empty non void AMI-Struct over N,
     s being State of S,
     l being Instruction-Location of S
  holds l in dom s;

:: from SCMFSA_3, 2007.07.22, A.T.

theorem :: AMI_1:117
  for N being with_non-empty_elements set
  for S being steady-programmed (non empty non void AMI-Struct over N)
  for i being Instruction of S,
      s being State of S
   holds
      Exec (i, s) | the Instruction-Locations of S
          = s | the Instruction-Locations of S;

:: from SCMFSA_4, 2007.07.22, A.T.

registration
 let N be set,
     S be AMI-Struct over N;
 cluster programmed FinPartState of S;
end;

theorem :: AMI_1:118
 for N being with_non-empty_elements set,
     S being definite (non empty non void AMI-Struct over N),
     p being programmed FinPartState of S
 holds rng p c= the Instructions of S;

definition let N be set;
 let S be AMI-Struct over N;
 let I, J be programmed FinPartState of S;
 redefine func I +* J -> programmed FinPartState of S;
end;

theorem :: AMI_1:119
 for N being with_non-empty_elements set,
     S being definite (non empty non void AMI-Struct over N),
     f being Function of the Instructions of S, the Instructions of S,
     s being programmed FinPartState of S
  holds dom(f*s) = dom s;

definition let N be non empty with_non-empty_elements set;
 let S be definite (non empty non void AMI-Struct over N);
 let s be programmed FinPartState of S;
 let f be Function of the Instructions of S, the Instructions of S;
 redefine func f*s -> programmed FinPartState of S;
end;

:: from SCMFSA6A, 2007.07.23, A.T.

theorem :: AMI_1:120
     for N being set, A being AMI-Struct over N, s being State of A,
     I being programmed FinPartState of A holds
 s,s+*I equal_outside the Instruction-Locations of A;

theorem :: AMI_1:121
 for N being with_non-empty_elements set,
     S being realistic IC-Ins-separated definite
       (non empty non void AMI-Struct over N),
     s1, s2 being State of S holds
 s1,s2 equal_outside the Instruction-Locations of S implies
   IC s1 = IC s2;

:: from SCMFSA6B, 2007.07.25, A.T.

reserve m,n for Element of NAT;

theorem :: AMI_1:122
for S being halting IC-Ins-separated definite
   (non empty non void AMI-Struct over N),
    s being State of S st s is halting
 holds Result s = (Computation s).LifeSpan s;

definition let N;
 let S be IC-Ins-separated definite (non empty non void AMI-Struct over N);
 let s be State of S, l be Instruction-Location of S, i be Instruction of S;
 redefine func s+*(l,i) -> State of S;
end;

theorem :: AMI_1:123
 for S being steady-programmed IC-Ins-separated definite
    (non empty non void AMI-Struct over N)
 for s being State of S, n
  holds s|the Instruction-Locations of S
    = ((Computation s).n)|the Instruction-Locations of S;

:: from SCMBSORT, 2007.07.26, A.T.

theorem :: AMI_1:124
 for N being with_non-empty_elements set,
     S being steady-programmed IC-Ins-separated definite
       (non empty non void AMI-Struct over N),
     p being programmed FinPartState of S,
     s1,s2 being State of S
  st p c= s1 & p c= s2
 holds (Computation s1).i | dom p = (Computation s2).i | dom p;