:: Input and Output of Instructions
::  by Artur Korni{\l}owicz
::
:: Received May 8, 2001
:: Copyright (c) 2001 Association of Mizar Users

environ

 vocabularies AMI_3, AMI_1, BOOLE, CAT_1, FUNCT_1, RELAT_1, FUNCT_4, GOBOARD5,
      FRECHET, AMISTD_1, REALSET1, FUNCOP_1, AMISTD_2, CARD_5, NET_1, AMI_5,
      AMI_7, ARYTM;
 notations TARSKI, XBOOLE_0, SUBSET_1, SETFAM_1, RELAT_1, FUNCT_1, REALSET1,
      NUMBERS, FUNCOP_1, FUNCT_4, STRUCT_0, AMI_1, FUNCT_7, AMISTD_1, AMISTD_2;
 constructors PARTFUN1, REALSET1, PRE_CIRC, AMISTD_2;
 registrations XBOOLE_0, SETFAM_1, RELAT_1, FUNCOP_1, FRAENKEL, CARD_3,
      STRUCT_0, AMI_1, AMISTD_1, AMISTD_2, REALSET1, CARD_1;
 requirements SUBSET, BOOLE;


begin :: Preliminaries

reserve N for with_non-empty_elements set,
  IL for non empty set;

canceled;

theorem :: AMI_7:2
  for A being non empty stored-program AMI-Struct over IL,N,
  s being State of A, o being Object of A holds s.o in ObjectKind o;

theorem :: AMI_7:3
  for A being realistic IC-Ins-separated definite
  (non empty stored-program AMI-Struct over IL,N), s being State of A,
  f being Instruction-Location of A, w being Element of ObjectKind IC A
  holds (s+*(IC A,w)).f = s.f;

definition
  let IL;
  let N be with_non-empty_elements set, A be IC-Ins-separated definite
  (non empty stored-program AMI-Struct over IL,N), s be State of A,
  o be Object of A, a be Element of ObjectKind o;
  redefine func s+*(o,a) -> State of A;
end;

theorem :: AMI_7:4
  for A being steady-programmed IC-Ins-separated definite
  (non empty stored-program AMI-Struct over IL,N), s being State of A,
  o being Object of A, f being Instruction-Location of A,
  I being Instruction of A, w being Element of ObjectKind o st f <> o
  holds Exec(I,s).f = Exec(I,s+*(o,w)).f;

canceled;

theorem :: AMI_7:6
  for A being standard (IC-Ins-separated definite
  (non empty stored-program AMI-Struct over NAT,N)), I being Instruction of A,
  s being State of A, o being Object of A, w being Element of ObjectKind o
  st I is sequential & o <> IC A holds IC Exec(I,s) = IC Exec(I,s+*(o,w));

theorem :: AMI_7:7
  for A being standard (IC-Ins-separated definite
  (non empty stored-program AMI-Struct over NAT,N)), I being Instruction of A,
  s being State of A, o being Object of A, w being Element of ObjectKind o
  st I is sequential & o <> IC A
  holds IC Exec(I,s+*(o,w)) = IC (Exec(I,s) +* (o,w));

theorem :: AMI_7:8
  for A being standard steady-programmed (IC-Ins-separated definite
  (non empty stored-program AMI-Struct over NAT,N)), I being Instruction of A,
  s being State of A, o being Object of A, w being Element of ObjectKind o,
  i being Instruction-Location of A
  holds Exec(I,s+*(o,w)).i = (Exec(I,s) +* (o,w)).i;

begin :: Input and Output of Instructions

definition
  let IL,N be set, A be AMI-Struct over IL,N;
  attr A is with_non_trivial_Instructions means
:: AMI_7:def 1

  the Instructions of A is non trivial;
end;

definition
  let IL,N be set, A be non empty AMI-Struct over IL,N;
  attr A is with_non_trivial_ObjectKinds means
:: AMI_7:def 2

  for o being Object of A holds ObjectKind o is non trivial;
end;

registration
  let N be with_non-empty_elements set;
  cluster STC N -> with_non_trivial_ObjectKinds;
end;

registration
  let N be with_non-empty_elements set;
  cluster halting realistic steady-programmed programmable
    with_explicit_jumps without_implicit_jumps IC-good Exec-preserving
    with_non_trivial_ObjectKinds with_non_trivial_Instructions
    (regular standard (standard-ins IC-Ins-separated definite
    (non empty stored-program AMI-Struct over NAT,N)));
end;

registration
  let IL;
  let N be with_non-empty_elements set;
  cluster with_non_trivial_ObjectKinds -> with_non_trivial_Instructions
    (definite (non empty stored-program AMI-Struct over IL,N));
end;

registration
  let N be with_non-empty_elements set;
  cluster with_non_trivial_ObjectKinds with_non_trivial_Instructions
    IC-Ins-separated definite
    (non empty stored-program AMI-Struct over NAT,N);
end;

registration
  let N be with_non-empty_elements set,
  A be with_non_trivial_ObjectKinds (non empty AMI-Struct over NAT,N),
  o be Object of A;
  cluster ObjectKind o -> non trivial;
end;

registration
  let N be with_non-empty_elements set,
  A be with_non_trivial_Instructions AMI-Struct over NAT,N;
  cluster the Instructions of A -> non trivial;
end;

registration
  let IL be non trivial set;
  let N be with_non-empty_elements set,
  A be IC-Ins-separated (non empty AMI-Struct over IL,N);
  cluster ObjectKind IC A -> non trivial;
end;

definition
  let IL;
  let N be with_non-empty_elements set,
  A be non empty stored-program AMI-Struct over IL,N, I be Instruction of A;
  func Output I -> Subset of A means
:: AMI_7:def 3

  for o being Object of A holds o in it iff
  ex s being State of A st s.o <> Exec(I,s).o;
end;

definition
  let IL;
  let N be with_non-empty_elements set, A be IC-Ins-separated definite
  (non empty stored-program AMI-Struct over IL,N), I be Instruction of A;
  func Out_\_Inp I -> Subset of A means
:: AMI_7:def 4

  for o being Object of A holds o in it iff
  for s being State of A, a being Element of ObjectKind o
  holds Exec(I,s) = Exec(I,s+*(o,a));
  func Out_U_Inp I -> Subset of A means
:: AMI_7:def 5

  for o being Object of A holds o in it iff
  ex s being State of A, a being Element of ObjectKind o
  st Exec(I,s+*(o,a)) <> Exec(I,s) +* (o,a);
end;

definition
  let IL;
  let N be with_non-empty_elements set, A be IC-Ins-separated definite
  (non empty stored-program AMI-Struct over IL,N), I be Instruction of A;
  func Input I -> Subset of A equals
:: AMI_7:def 6

  Out_U_Inp I \ Out_\_Inp I;
end;

canceled;

theorem :: AMI_7:10
  for A being with_non_trivial_ObjectKinds IC-Ins-separated definite
  (non empty stored-program AMI-Struct over NAT,N),
  I being Instruction of A holds Out_\_Inp I c= Output I;

theorem :: AMI_7:11
  for A being IC-Ins-separated definite
  (non empty stored-program AMI-Struct over IL,N),
  I being Instruction of A holds Output I c= Out_U_Inp I;

canceled;

theorem :: AMI_7:13
  for A being with_non_trivial_ObjectKinds IC-Ins-separated definite
  (non empty stored-program AMI-Struct over NAT,N),
  I being Instruction of A holds Out_\_Inp I = Output I \ Input I;

theorem :: AMI_7:14
  for A being with_non_trivial_ObjectKinds IC-Ins-separated definite
  (non empty stored-program AMI-Struct over NAT,N),
  I being Instruction of A holds Out_U_Inp I = Output I \/ Input I;

theorem :: AMI_7:15
  for A being IC-Ins-separated definite
  (non empty stored-program AMI-Struct over IL,N), I being Instruction of A,
  o being Object of A st ObjectKind o is trivial holds not o in Out_U_Inp I;

theorem :: AMI_7:16
  for A being IC-Ins-separated definite
  (non empty stored-program AMI-Struct over IL,N) , I being Instruction of A,
  o being Object of A st ObjectKind o is trivial holds not o in Input I;

theorem :: AMI_7:17
  for A being IC-Ins-separated definite
  (non empty stored-program AMI-Struct over IL,N) , I being Instruction of A,
  o being Object of A st ObjectKind o is trivial holds not o in Output I;

theorem :: AMI_7:18
  for A being IC-Ins-separated definite
  (non empty stored-program AMI-Struct over IL,N),
  I being Instruction of A holds I is halting iff Output I is empty;

theorem :: AMI_7:19
  for A being with_non_trivial_ObjectKinds IC-Ins-separated definite
  (non empty stored-program AMI-Struct over NAT,N),
  I being Instruction of A st I is halting holds Out_\_Inp I is empty;

theorem :: AMI_7:20
  for A being IC-Ins-separated definite
  (non empty stored-program AMI-Struct over IL,N),
  I being Instruction of A st I is halting holds Out_U_Inp I is empty;

theorem :: AMI_7:21
  for A being IC-Ins-separated definite
  (non empty stored-program AMI-Struct over IL,N),
  I being Instruction of A st I is halting holds Input I is empty;

registration
  let IL;
  let N be with_non-empty_elements set, A be halting IC-Ins-separated definite
  (non empty stored-program AMI-Struct over IL,N),
  I be halting Instruction of A;
  cluster Input I -> empty;
  cluster Output I -> empty;
  cluster Out_U_Inp I -> empty;
end;

registration
  let N be with_non-empty_elements set;
  cluster halting with_non_trivial_ObjectKinds IC-Ins-separated definite
    (non empty stored-program AMI-Struct over NAT,N);
end;

registration
  let N be with_non-empty_elements set,
  A be halting with_non_trivial_ObjectKinds IC-Ins-separated definite
  (non empty stored-program AMI-Struct over NAT,N),
  I be halting Instruction of A;
  cluster Out_\_Inp I -> empty;
end;

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

theorem :: AMI_7:22
  for A being with_non_trivial_Instructions steady-programmed IC-Ins-separated
  definite (non empty stored-program AMI-Struct over NAT,N),
  f being Instruction-Location of A, I being Instruction of A
  holds not f in Out_\_Inp I;

theorem :: AMI_7:23
  for A being standard (IC-Ins-separated definite
  (non empty stored-program AMI-Struct over NAT,N)),
  I being Instruction of A st I is sequential holds not IC A in Out_\_Inp I;

theorem :: AMI_7:24
  for A being IC-Ins-separated definite
  (non empty stored-program AMI-Struct over IL,N), I being Instruction of A st
  ex s being State of A st Exec(I,s).IC A <> IC s
  holds IC A in Output I;

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

theorem :: AMI_7:25
  for A being standard (IC-Ins-separated definite
  (non empty stored-program AMI-Struct over NAT,N)),
  I being Instruction of A st I is sequential holds IC A in Output I;

theorem :: AMI_7:26
  for A being IC-Ins-separated definite
  (non empty stored-program AMI-Struct over IL,N), I being Instruction of A st
  ex s being State of A st Exec(I,s).IC A <> IC s holds IC A in Out_U_Inp I;

theorem :: AMI_7:27
  for A being standard (IC-Ins-separated definite
  (non empty stored-program AMI-Struct over NAT,N)),
  I being Instruction of A st I is sequential holds IC A in Out_U_Inp I;

theorem :: AMI_7:28
  for A being IC-Ins-separated definite
  (non empty stored-program AMI-Struct over IL,N),
  f being Instruction-Location of A, I being Instruction of A
  st for s being State of A, p being programmed FinPartState of A
  holds Exec (I, s +* p) = Exec (I,s) +* p holds not f in Out_U_Inp I;

theorem :: AMI_7:29
  for A being IC-Ins-separated definite
  (standard-ins non empty stored-program AMI-Struct over IL,N),
  I being Instruction of A, o being Object of A st I is jump-only
  holds o in Output I implies o = IC A;