:: 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, PARTFUN1, FINSET_1, AMI_1, NEWTON, AMI_5, MCART_1,
      AMISTD_2, FINSEQ_1, FINSEQ_4, GRAPH_2, TREES_2, ORDINAL1, ARYTM, AMI_3,
      SCM_1, FUNCT_7, ARYTM_1;
 notations TARSKI, XBOOLE_0, ZFMISC_1, MCART_1, SUBSET_1, SETFAM_1, ORDINAL1,
      NUMBERS, FUNCT_7, CARD_3, XCMPLX_0, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2,
      FINSET_1, NAT_1, FUNCOP_1, FUNCT_4, FINSEQ_1, FINSEQ_4, GRAPH_2,
      DOMAIN_1, TREES_2, STRUCT_0, XXREAL_0, SEQ_1;
 constructors SETFAM_1, PARTFUN1, DOMAIN_1, FUNCT_4, XXREAL_0, NAT_1, FUNCT_7,
      SEQ_1, INT_1, CARD_3, STRUCT_0, FINSEQ_4, GRAPH_2, TREES_2;
 registrations XBOOLE_0, SETFAM_1, RELAT_1, FUNCT_1, ORDINAL1, FUNCT_2,
      FUNCOP_1, FUNCT_4, FINSET_1, FRAENKEL, XREAL_0, FINSEQ_1, CARD_3,
      STRUCT_0, INT_1;
 requirements NUMERALS, BOOLE, SUBSET, ARITHM;


begin :: General concepts

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

definition
  let IL,N be set;
  canceled;
  func Trivial-AMI(IL,N) -> strict AMI-Struct over IL, N means
:: AMI_1:def 2

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

definition
  let IL,N be set;
  let S be AMI-Struct over IL,N;
  attr S is stored-program means
:: AMI_1:def 3

  IL c= the carrier of S;
end;

registration
  let IL,N be set;
  cluster Trivial-AMI(IL,N)-> non empty stored-program;
end;

registration
  let IL,N be set;
  cluster non empty stored-program AMI-Struct over IL,N;
end;

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

definition
  let IL be non empty set, N be set;
  let S be AMI-Struct over IL,N;
  mode Instruction-Location of S means
:: AMI_1:def 4

    it in IL;
end;

definition
  let IL be non empty set, N be set;
  let S be AMI-Struct over IL,N;
  redefine mode Instruction-Location of S -> Element of IL;
end;

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

definition
  let IL,N be set;
  let S be non empty AMI-Struct over IL,N;
  func IC S -> Object of S equals
:: AMI_1:def 5

  the Instruction-Counter of S;
end;

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

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

definition
  let IL be non empty set;
  let N be with_non-empty_elements set;
  let S be AMI-Struct over IL,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 IL for non empty set;
reserve N for with_non-empty_elements set;

definition
  let IL,N;
  let S be AMI-Struct over IL,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 IL,N;
  let S be AMI-Struct over IL,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(IL,N) is halting;

registration
  let IL,N;
  cluster Trivial-AMI(IL,N) -> halting;
end;

registration
  let IL,N;
  cluster halting AMI-Struct over IL,N;
end;

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

definition
  let IL be non empty set;
  let N be with_non-empty_elements set;
  let S be halting (AMI-Struct over IL,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 IL,N;
  let S be halting (AMI-Struct over IL,N);
  cluster halt S -> halting;
end;

definition
  let IL,N be set;
  let IT be non empty AMI-Struct over IL,N;
  attr IT is IC-Ins-separated means
:: AMI_1:def 11

  ObjectKind IC IT = IL;
end;

definition
  let IL;
  let N be with_non-empty_elements set;
  let IT be non empty AMI-Struct over IL,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 IL be non empty set, N be set;
  let IT be non empty stored-program AMI-Struct over IL,N;
  redefine mode Instruction-Location of IT -> Element of IT;
end;

definition
  let IL be non empty set, N be set;
  let IT be non empty stored-program AMI-Struct over IL,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(IL,E) is IC-Ins-separated;

canceled;

theorem :: AMI_1:9
  for s being State of Trivial-AMI(IL,N),
  i being Instruction of Trivial-AMI(IL,N) holds Exec(i,s) = s;

theorem :: AMI_1:10
  Trivial-AMI(IL,N) is steady-programmed;

theorem :: AMI_1:11
  Trivial-AMI(IL,E) is definite;

registration
  let IL be non empty set, E be set;
  cluster Trivial-AMI(IL,E) -> IC-Ins-separated definite;
end;

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

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

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

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

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

  s.IC S;
end;

theorem :: AMI_1:12
  for s1, s2 being State of Trivial-AMI(IL,N) st IC s1 = IC s2 holds s1=s2;

definition
  let IL;
  let N be with_non-empty_elements set;
  let S be IC-Ins-separated (non empty stored-program AMI-Struct over IL,N);
  let s be State of S;
  redefine func IC s -> Instruction-Location of 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 IL;
  let N be with_non-empty_elements set;
  canceled;
  let S be IC-Ins-separated definite
  (non empty stored-program AMI-Struct over IL,N);
  let s be State of S;
  func CurInstr s -> Instruction of S equals
:: AMI_1:def 17

  s.IC s;
end;

definition
  let IL,N;
  let S be IC-Ins-separated definite
  (non empty stored-program AMI-Struct over IL,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 IL,N;
  let S be IC-Ins-separated definite
  (non empty stored-program AMI-Struct over IL,N);
  let s be State of S, k be Nat;
  func Computation(s,k) -> State of S means
:: AMI_1:def 19
   ex f being Function of NAT, product the Object-Kind of S st
  it = f.k & f.0 = s & for i being Nat holds f.(i+1) = Following(f.i);
end;

definition
  let IL,N;
  let S be AMI-Struct over IL,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 IL,N;
  let S be halting IC-Ins-separated definite
  (non empty stored-program AMI-Struct over IL,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 IL,N be set;
  let IT be AMI-Struct over IL,N;
  attr IT is realistic means
:: AMI_1:def 21

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

theorem :: AMI_1:13
  for IL,N for S be IC-Ins-separated definite
  (non empty stored-program AMI-Struct over IL,N),
   s be State of S holds
 Computation(s,0) = s;

theorem :: AMI_1:14
  for IL,N for S be IC-Ins-separated definite
  (non empty stored-program AMI-Struct over IL,N),
   s be State of S, k be Nat holds
 Computation(s,k+1) = Following Computation(s,k);

canceled 33;

theorem :: AMI_1:48
  for S being IC-Ins-separated definite
  (non empty stored-program AMI-Struct over IL,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 stored-program AMI-Struct over IL,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 IL,N for S being halting IC-Ins-separated definite
  (non empty stored-program AMI-Struct over IL,N)
  for s being State of S st CurInstr Computation(s,i) = halt S
  holds  Computation(s,j) =  Computation(s,i);

definition
  let IL,N;
  let S be halting IC-Ins-separated definite
  (non empty stored-program AMI-Struct over IL,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 stored-program AMI-Struct over IL,N)
  for s being State of S, i be Instruction-Location of S
  holds s.i = (Following s).i;

definition
  let IL,N;
  let S be definite (non empty stored-program AMI-Struct over IL,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 stored-program AMI-Struct over IL,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 stored-program AMI-Struct over IL,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 stored-program AMI-Struct over IL,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 stored-program AMI-Struct over IL,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 IL,N;
  let S be non empty AMI-Struct over IL,N, o be Object of S;
  cluster ObjectKind o -> non empty;
end;

begin :: Finite substates

definition
  let IL,N be set;
  let S be AMI-Struct over IL,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 IL,N be set;
  let S be AMI-Struct over IL,N;
  cluster finite Element of sproduct the Object-Kind of S;
end;

definition
  let IL,N be set;
  let S be AMI-Struct over IL,N;
  mode FinPartState of S is finite Element of sproduct the Object-Kind of S;
end;

definition
  let IL,N;
  canceled;
  let S be IC-Ins-separated definite
  (non empty stored-program AMI-Struct over IL,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 IL,N;
  let S be halting IC-Ins-separated definite
  (non empty stored-program AMI-Struct over IL,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 IL,N;
  let IT be IC-Ins-separated definite
  (non empty stored-program AMI-Struct over IL,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 stored-program AMI-Struct over IL,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 stored-program AMI-Struct over IL,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 IL,N;
  let S be IC-Ins-separated definite
  (non empty stored-program AMI-Struct over IL,N);
  let la be Object of S;
  let a be Element of ObjectKind la;
  redefine func la .--> a -> FinPartState of S;
end;

definition
  let IL,N;
  let S be IC-Ins-separated definite
  (non empty stored-program AMI-Struct over IL,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(IL,E) is realistic;

theorem :: AMI_1:61
  Trivial-AMI(IL,N) is programmable;

registration
  let IL,E;
  cluster Trivial-AMI(IL,E) -> realistic;
end;

registration
  let IL,N;
  cluster Trivial-AMI(IL,N) -> programmable;
end;

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

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

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

theorem :: AMI_1:62
  for S being AMI-Struct over IL,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 IL,N holds {} is FinPartState of S;

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

definition
  let IL,N be set;
  let S be AMI-Struct over IL,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 stored-program AMI-Struct over IL,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 stored-program AMI-Struct over IL,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 stored-program AMI-Struct over IL,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 stored-program AMI-Struct over IL,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 IL,N;
  let S be realistic halting IC-Ins-separated definite
  (non empty stored-program AMI-Struct over IL,N);
  cluster autonomic halting FinPartState of S;
end;

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

definition
  let IL,N;
  let S be realistic halting IC-Ins-separated definite
  (non empty stored-program AMI-Struct over IL,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 IL,N;
  let S be realistic halting IC-Ins-separated definite
  (non empty stored-program AMI-Struct over IL,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 IL,N;
  let S be realistic halting IC-Ins-separated definite
  (non empty stored-program AMI-Struct over IL,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 stored-program AMI-Struct over IL,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 stored-program AMI-Struct over IL,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 stored-program AMI-Struct over IL,N)
  for p being FinPartState of S
  holds p is pre-program of S iff p computes {} .--> {};

definition
  let IL,N;
  let S be realistic halting IC-Ins-separated definite
  (non empty stored-program AMI-Struct over IL,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 stored-program AMI-Struct over IL,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 stored-program AMI-Struct over IL,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 stored-program AMI-Struct over IL,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 IL,N;
  let S be realistic halting IC-Ins-separated definite
  (non empty stored-program AMI-Struct over IL,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 stored-program AMI-Struct over IL,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 stored-program AMI-Struct over IL,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 stored-program AMI-Struct over IL,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 IL,N be set, S be AMI-Struct over IL,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 IL,N be set;
  cluster Trivial-AMI(IL,N) -> standard-ins;
end;

registration
  let IL,N be set;
  cluster standard-ins non empty stored-program AMI-Struct over IL,N;
end;

registration
  let IL,N;
  cluster IC-Ins-separated definite standard-ins
    (non empty stored-program AMI-Struct over IL,N);
end;

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

definition
  let IL,N be set, S be standard-ins AMI-Struct over IL,N;
  func InsCodes S equals
:: AMI_1:def 33

  dom the Instructions of S;
end;

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

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

theorem :: AMI_1:77
  for IL,N being set, S being AMI-Struct over IL,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 IL,N be set, S be AMI-Struct over IL,N;
  mode IL-FinSequence of S -> FinSequence of IL means
:: AMI_1:def 34

    not contradiction;
end;

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

definition
  let IL,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 IL,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 IL,N,S;
  cluster non empty IL-FinSequence of S;
end;

definition
  let IL,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 IL,N, S;
  mode IL-Function of D,S -> Function of D, IL means
:: AMI_1:def 36

    not contradiction;
end;

definition
  let D be non empty set;
  let IL,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 IL,N,S;
  mode IL-DecoratedTree of S -> DecoratedTree of IL means
:: AMI_1:def 37

    not contradiction;
end;

definition
  let IL,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 {IL() -> non empty set, N() -> set,
  S() -> non empty stored-program AMI-Struct over IL(),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
 {IL() -> non empty set, N,D()-> set,
  S()-> non empty stored-program AMI-Struct over IL(),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 IL;
  let N be set;
  let S be AMI-Struct over IL,N;
  cluster FinPartSt S -> non empty;
end;

definition
  let IL be non empty set;
  let N be with_non-empty_elements set;
  let S be IC-Ins-separated definite
  (non empty stored-program AMI-Struct over IL,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 IL,N be set;
  let S be AMI-Struct over IL,N;
  let IT be FinPartState of S;
  attr IT is programmed means
:: AMI_1:def 40

  dom IT c= IL;
end;

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

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

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

theorem :: AMI_1:80
  for S being AMI-Struct over IL,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 stored-program AMI-Struct over IL,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 IL,N;
  let S be IC-Ins-separated (non empty AMI-Struct over IL,N);
  let s be State of S, l be Element of IL;
  pred s starts_at l means
:: AMI_1:def 41

  IC s = l;
end;

definition
  let IL,N;
  let S be IC-Ins-separated halting (non empty AMI-Struct over IL,N);
  let s be State of S, l be set;
  pred s halts_at l means
:: AMI_1:def 42

  s.l = halt S;
end;

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

definition
  let IL,N;
  let S be definite IC-Ins-separated
  (non empty stored-program AMI-Struct over IL,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 IL,N;
  let S be definite IC-Ins-separated
  (non empty stored-program AMI-Struct over IL,N);
  let p be FinPartState of S, l be Element of IL;
  pred p starts_at l means
:: AMI_1:def 44

  IC S in dom p & IC p = l;
end;

definition
  let IL,N;
  let S be definite IC-Ins-separated halting
  (non empty stored-program AMI-Struct over IL,N);
  let p be FinPartState of S, l be set;
  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 stored-program AMI-Struct over IL,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 stored-program AMI-Struct over IL,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 stored-program AMI-Struct over IL,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 stored-program AMI-Struct over IL,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 stored-program AMI-Struct over IL,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 stored-program AMI-Struct over IL,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 stored-program AMI-Struct over IL,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 stored-program AMI-Struct over IL,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 stored-program AMI-Struct over IL,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 stored-program AMI-Struct over IL,N),
  p being FinPartState of S, l being Element of IL
  st p starts_at l for s being State of S st p c= s holds s starts_at l;

definition
  let IL,N;
  let S be definite IC-Ins-separated
  (non empty stored-program AMI-Struct over IL,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 IL;
  let N be with_non-empty_elements set;
  let S be halting IC-Ins-separated definite
  (non empty stored-program AMI-Struct over IL,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 stored-program AMI-Struct over IL,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 stored-program AMI-Struct over IL,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 IL,N,S;
  let p be programmed FinPartState of S, loc be set;
  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 IL,N being set, S being AMI-Struct over IL,N
  for x being set, p being FinPartState of S st x c= p
  holds x is FinPartState of S;

definition
  let IL,N be set;
  let S be AMI-Struct over IL,N;
  let p be FinPartState of S;
  func ProgramPart p -> programmed FinPartState of S equals
:: AMI_1:def 48

  p | IL;
end;

definition
  let IL,N be set;
  let S be non empty stored-program AMI-Struct over IL,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} \/ IL));
end;

definition
  let IL,N be set, S be non empty AMI-Struct over IL,N;
  let IT be FinPartState of S;
  attr IT is data-only means
:: AMI_1:def 50

  dom IT misses {IC S} \/ IL;
end;

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

theorem :: AMI_1:99
  for S being steady-programmed IC-Ins-separated definite
  (non empty stored-program AMI-Struct over IL,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 IL,N being set, S being non empty stored-program AMI-Struct over IL,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 stored-program AMI-Struct over IL,N)
  for p being FinPartState of S holds not IC S in dom (ProgramPart p);

theorem :: AMI_1:102
  for IL,N being set, S being non empty stored-program AMI-Struct over IL,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 stored-program AMI-Struct over IL,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 stored-program AMI-Struct over IL,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 IL,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 stored-program AMI-Struct over IL,N)
  for p being FinPartState of S st IC S in dom p holds p is not programmed;

definition
  let IL,N;
  let S be AMI-Struct over IL,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 stored-program AMI-Struct over IL,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 IL being non empty set, N being with_non-empty_elements set,
  S being stored-program AMI-Struct over IL,N, s being State of S
  holds IL c= dom s;

theorem :: AMI_1:115
  for N being with_non-empty_elements set,
  S being IC-Ins-separated (non empty stored-program AMI-Struct over IL,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 stored-program AMI-Struct over IL,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 stored-program AMI-Struct over IL,N)
  for i being Instruction of S, s being State of S holds Exec (i, s) | IL
  = s | IL;

:: from SCMFSA_4, 2007.07.22, A.T.

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

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

definition
  let IL be non empty set, N be set;
  let S be AMI-Struct over IL,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 stored-program AMI-Struct over IL,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 IL;
  let N be non empty with_non-empty_elements set;
  let S be definite (non empty stored-program AMI-Struct over IL,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 IL,N being set, A being AMI-Struct over IL,N, s being State of A,
  I being programmed FinPartState of A holds s,s+*I equal_outside IL;

theorem :: AMI_1:121
  for N being with_non-empty_elements set,
  S being realistic IC-Ins-separated definite
  (non empty stored-program AMI-Struct over IL,N),
  s1, s2 being State of S holds s1,s2 equal_outside IL 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 stored-program AMI-Struct over IL,N),
  s being State of S st s is halting
  holds Result s =  Computation(s,LifeSpan s);

definition
  let IL,N;
  let S be IC-Ins-separated definite
  (non empty stored-program AMI-Struct over IL,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 stored-program AMI-Struct over IL,N) for s being State of S, n
  holds s|IL = ( Computation(s,n))|IL;

:: 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 stored-program AMI-Struct over IL,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;

:: missing, 2007.11.13, A.T.

theorem :: AMI_1:125
  for S being AMI-Struct over IL,N, p being Element of FinPartSt S
  holds p is FinPartState of S;

:: from SCMFSA8A, 2008.02.12, A.T.

theorem :: AMI_1:126
  for IL being non empty set, N being with_non-empty_elements set,
  S being definite (non empty stored-program AMI-Struct over IL,N),
  I being programmed FinPartState of S, x being set holds
  x in dom I implies I.x is Instruction of S;

:: from SCMFSA9A, 2008.02.12, A.T.

theorem :: AMI_1:127
  for IL being non empty set
  for N being non empty with_non-empty_elements set,
  S being halting IC-Ins-separated definite
  (non empty stored-program AMI-Struct over IL,N),
  s being State of S, k being Element of NAT
  st CurInstr( Computation(s,k)) = halt S
  holds  Computation(s,LifeSpan s) =  Computation(s,k);

:: from SCMISORT, 2008.02.12, A.T.

theorem :: AMI_1:128
  for IL being non empty set for N being non empty with_non-empty_elements set
  for S being halting IC-Ins-separated definite
  (non empty stored-program AMI-Struct over IL,N)
  for s being State of S st (LifeSpan s) <= j & s is halting holds
   Computation(s,j) =  Computation(s,LifeSpan s);

:: from AMI_6, 2008.02.12, A.T.

theorem :: AMI_1:129
  for IL being non empty set for N being with_non-empty_elements set,
  S being realistic IC-Ins-separated definite
  (non empty stored-program AMI-Struct over IL,N), t, u being State of S,
  il being Instruction-Location of S, e being Element of ObjectKind IC S,
  I being Element of ObjectKind il st e = il & u = t+*((IC S, il)-->(e, I))
  holds u.il = I & IC u = il & IC Following u = Exec(u.IC u, u).IC S;

:: from SCMPDS_5, 2008.02.12, A.T.

theorem :: AMI_1:130
  for S being halting IC-Ins-separated definite
  (non empty stored-program AMI-Struct over IL,N),
  s being State of S st s = Following s
  holds for n holds  Computation(s,n) = s;

:: from SCMPDS_9, 2008.02.12, A.T.

theorem :: AMI_1:131
 for IL being non empty set for N being with_non-empty_elements set,
S being IC-Ins-separated definite
(non empty stored-program AMI-Struct over IL,N), s being State of S,
i being Instruction of S holds Exec(s.IC s,s).IC S = IC Following s;