The abstract of the Mizar article:

Input and Output of Instructions

by

Artur Kornilowicz

Received May 8, 2001

MML identifier: AMI_7

[ Mizar article, MML identifier index ]

environ

 vocabulary 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_2, INT_1, FINSEQ_1, ARYTM_1, SQUARE_1, ARYTM_3, NAT_1, AMI_7;
 notation TARSKI, XBOOLE_0, ENUMSET1, SUBSET_1, RELAT_1, FUNCT_1, REALSET1,
      NUMBERS, XCMPLX_0, XREAL_0, SQUARE_1, FINSEQ_1, FUNCOP_1, CQC_LANG,
      INT_1, NAT_1, FUNCT_4, STRUCT_0, AMI_1, AMI_2, AMI_3, AMI_5, FUNCT_7,
      AMISTD_1, AMISTD_2;
 constructors DOMAIN_1, FUNCT_7, NAT_1, AMI_5, SQUARE_1, AMISTD_2, REALSET1,
      PRE_CIRC;
 clusters AMI_1, XREAL_0, INT_1, AMISTD_1, SCMRING1, AMI_6, AMISTD_2, RELSET_1,
      FUNCOP_1, WAYBEL12, SCMRING3, SQUARE_1, XBOOLE_0, FRAENKEL;
 requirements NUMERALS, SUBSET, BOOLE, REAL, ARITHM;


begin :: Preliminaries

reserve N for with_non-empty_elements set;

theorem :: AMI_7:1
 for x, y, z being set st x <> y & x <> z holds {x, y, z} \ {x} = {y, z};

theorem :: AMI_7:2
  for A being non empty non void AMI-Struct over 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 non void AMI-Struct over 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 N be with_non-empty_elements set,
      A be IC-Ins-separated definite (non empty non void AMI-Struct over 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 non void AMI-Struct over 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;

theorem :: AMI_7:5
 for A being IC-Ins-separated definite (non empty non void AMI-Struct over N),
     s being State of A,
     o being Object of A,
     w being Element of ObjectKind o
    st o <> IC A
  holds IC s = IC (s+*(o,w));

theorem :: AMI_7:6
 for A being standard (IC-Ins-separated definite
       (non empty non void AMI-Struct over 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 non void AMI-Struct over 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 non void AMI-Struct over 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 N be set,
       A be AMI-Struct over N;
 attr A is with_non_trivial_Instructions means
:: AMI_7:def 1

  the Instructions of A is non trivial;
end;

definition
   let N be set,
       A be non empty AMI-Struct over 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;

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

definition
   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 (IC-Ins-separated definite
         (non empty non void AMI-Struct over N)));
end;

definition
   let N be with_non-empty_elements set;
 cluster with_non_trivial_ObjectKinds -> with_non_trivial_Instructions
         (definite (non empty non void AMI-Struct over N));
end;

definition
   let N be with_non-empty_elements set;
 cluster with_non_trivial_ObjectKinds ->
         with-non-trivial-Instruction-Locations
         (IC-Ins-separated (non empty AMI-Struct over N));
end;

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

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

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

definition
  let N be with_non-empty_elements set,
      A be non empty non void AMI-Struct over 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 N be with_non-empty_elements set,
      A be IC-Ins-separated definite (non empty non void AMI-Struct over 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 N be with_non-empty_elements set,
      A be IC-Ins-separated definite (non empty non void AMI-Struct over 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;

theorem :: AMI_7:9
 for A being IC-Ins-separated definite (non empty non void AMI-Struct over N),
     I being Instruction of A holds
  Out_\_Inp I misses Input I;

theorem :: AMI_7:10
 for A being with_non_trivial_ObjectKinds IC-Ins-separated definite
             (non empty non void AMI-Struct over 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 non void AMI-Struct over N),
     I being Instruction of A holds
  Output I c= Out_U_Inp I;

theorem :: AMI_7:12
 for A being IC-Ins-separated definite (non empty non void AMI-Struct over N),
     I being Instruction of A holds
  Input I c= Out_U_Inp I;

theorem :: AMI_7:13
   for A being with_non_trivial_ObjectKinds IC-Ins-separated definite
             (non empty non void AMI-Struct over 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 non void AMI-Struct over 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 non void AMI-Struct over 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 non void AMI-Struct over 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 non void AMI-Struct over 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 non void AMI-Struct over 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 non void AMI-Struct over 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 non void AMI-Struct over 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 non void AMI-Struct over N),
     I being Instruction of A st I is halting
  holds Input I is empty;

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

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

theorem :: AMI_7:22
 for A being with_non_trivial_Instructions steady-programmed IC-Ins-separated
             definite (non empty non void AMI-Struct over 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 non void AMI-Struct over 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 non void AMI-Struct over 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;

theorem :: AMI_7:25
 for A being standard (IC-Ins-separated definite
       (non empty non void AMI-Struct over 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 non void AMI-Struct over 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 non void AMI-Struct over 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 non void AMI-Struct over 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 (non empty non void AMI-Struct over 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;

begin  :: SCM

reserve a, b for Data-Location,
        f for Instruction-Location of SCM,
        I for Instruction of SCM;

theorem :: AMI_7:30
 for s being State of SCM, w being Element of ObjectKind IC SCM
  holds (s+*(IC SCM,w)).a = s.a;

theorem :: AMI_7:31
 f <> Next f;

definition
  let s be State of SCM, dl be Data-Location, k be Integer;
 redefine func s+*(dl,k) -> State of SCM;
end;

definition
 cluster SCM -> with_non_trivial_ObjectKinds;
end;

theorem :: AMI_7:32
 Out_\_Inp (a:=a) = {};

theorem :: AMI_7:33
 a <> b implies Out_\_Inp (a:=b) = { a };

theorem :: AMI_7:34
 Out_\_Inp AddTo(a,b) = {};

theorem :: AMI_7:35
 Out_\_Inp SubFrom(a,a) = { a };

theorem :: AMI_7:36
 a <> b implies Out_\_Inp SubFrom(a,b) = {};

theorem :: AMI_7:37
 Out_\_Inp MultBy(a,b) = {};

theorem :: AMI_7:38
 Out_\_Inp Divide(a,a) = { a };

theorem :: AMI_7:39
 a <> b implies Out_\_Inp Divide(a,b) = {};

theorem :: AMI_7:40
 Out_\_Inp goto f = { IC SCM };

theorem :: AMI_7:41
 Out_\_Inp (a =0_goto f) = {};

theorem :: AMI_7:42
  Out_\_Inp (a >0_goto f) = {};

theorem :: AMI_7:43
   Output (a:=a) = { IC SCM };

theorem :: AMI_7:44
 a <> b implies Output (a:=b) = { a, IC SCM };

theorem :: AMI_7:45
 Output AddTo(a,b) = { a, IC SCM };

theorem :: AMI_7:46
 Output SubFrom(a,b) = { a, IC SCM };

theorem :: AMI_7:47
 Output MultBy(a,b) = { a, IC SCM };

theorem :: AMI_7:48
 Output Divide(a,b) = { a, b, IC SCM };

theorem :: AMI_7:49
 Output goto f = { IC SCM };

theorem :: AMI_7:50
 Output (a =0_goto f) = { IC SCM };

theorem :: AMI_7:51
 Output (a >0_goto f) = { IC SCM };

theorem :: AMI_7:52
 not f in Out_U_Inp I;

theorem :: AMI_7:53
 Out_U_Inp (a:=a) = { IC SCM };

theorem :: AMI_7:54
 a <> b implies Out_U_Inp (a:=b) = { a, b, IC SCM };

theorem :: AMI_7:55
 Out_U_Inp AddTo(a,b) = { a, b, IC SCM };

theorem :: AMI_7:56
 Out_U_Inp SubFrom(a,b) = { a, b, IC SCM };

theorem :: AMI_7:57
 Out_U_Inp MultBy(a,b) = { a, b, IC SCM };

theorem :: AMI_7:58
 Out_U_Inp Divide(a,b) = { a, b, IC SCM };

theorem :: AMI_7:59
 Out_U_Inp (goto f) = { IC SCM };

theorem :: AMI_7:60
 Out_U_Inp (a =0_goto f) = { a, IC SCM };

theorem :: AMI_7:61
 Out_U_Inp (a >0_goto f) = { a, IC SCM };

theorem :: AMI_7:62
   Input (a:=a) = { IC SCM };

theorem :: AMI_7:63
   a <> b implies Input (a:=b) = { b, IC SCM };

theorem :: AMI_7:64
   Input AddTo(a,b) = { a, b, IC SCM };

theorem :: AMI_7:65
   Input SubFrom(a,a) = { IC SCM };

theorem :: AMI_7:66
   a <> b implies Input SubFrom(a,b) = { a, b, IC SCM };

theorem :: AMI_7:67
   Input MultBy(a,b) = { a, b, IC SCM };

theorem :: AMI_7:68
   Input Divide(a,a) = { IC SCM };

theorem :: AMI_7:69
   a <> b implies Input Divide(a,b) = { a, b, IC SCM };

theorem :: AMI_7:70
   Input goto f = {};

theorem :: AMI_7:71
   Input (a =0_goto f) = { a, IC SCM };

theorem :: AMI_7:72
   Input (a >0_goto f) = { a, IC SCM };