:: 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;
 definitions AMI_1, AMISTD_1, XBOOLE_0, FUNCOP_1;
 theorems AMI_1, FUNCT_7, TARSKI, AMISTD_1, FUNCT_2, SUBSET_1, FUNCOP_1,
      FUNCT_4, ZFMISC_1, YELLOW_8, CARD_3, FUNCT_1, YELLOW15, XBOOLE_0,
      XBOOLE_1;
 schemes SUBSET_1;

begin :: Preliminaries

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

canceled;

theorem Th2:
  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
proof
  let A be non empty stored-program AMI-Struct over IL,N, s be State of A,
  o be Object of A;
  dom the Object-Kind of A = the carrier of A by FUNCT_2:def 1;
  hence s.o in ObjectKind o by CARD_3:18;
end;

theorem
  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 by AMI_1:48,FUNCT_7:34;

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;
  coherence
  proof
    dom s = the carrier of A by AMI_1:79;
    then s+*(o,a) = s+*(o .--> a) by FUNCT_7:def 3;
    hence thesis;
  end;
end;

theorem
  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
proof
  let A be steady-programmed IC-Ins-separated definite
  (non empty stored-program AMI-Struct over IL,N), s be State of A,
  o be Object of A, f be Instruction-Location of A, I being Instruction of A,
  w be Element of ObjectKind o such that
A1: f <> o;
  thus Exec(I,s).f = s.f by AMI_1:def 13
    .= s+*(o,w).f by A1,FUNCT_7:34
    .= Exec(I,s+*(o,w)).f by AMI_1:def 13;
end;

canceled;

theorem Th6:
  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))
proof
  let A be standard (IC-Ins-separated definite
  (non empty stored-program AMI-Struct over NAT,N)), I be Instruction of A,
  s be State of A, o be Object of A, w be Element of ObjectKind o such that
A1: for s being State of A holds Exec(I,s).IC A = NextLoc IC s and
A2: o <> IC A;
  thus IC Exec(I,s) = NextLoc IC s by A1
    .= NextLoc IC (s+*(o,w)) by A2,FUNCT_7:34
    .= IC Exec(I,s+*(o,w)) by A1;
end;

theorem
  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))
proof
  let A be standard (IC-Ins-separated definite
  (non empty stored-program AMI-Struct over NAT,N)), I be Instruction of A,
  s be State of A, o be Object of A, w be Element of ObjectKind o such that
A1: I is sequential and
A2: o <> IC A;
  thus IC Exec(I,s+*(o,w)) = IC Exec(I,s) by A1,A2,Th6
    .= IC (Exec(I,s) +* (o,w)) by A2,FUNCT_7:34;
end;

theorem
  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
proof
  let A be standard steady-programmed (IC-Ins-separated definite
  (non empty stored-program AMI-Struct over NAT,N)), I be Instruction of A,
  s be State of A, o be Object of A, w be Element of ObjectKind o,
  i be Instruction-Location of A;
A1: Exec(I,s+*(o,w)).i = (s+*(o,w)).i by AMI_1:def 13;
A2: dom s = the carrier of A by AMI_1:79;
A3: dom Exec(I,s) = the carrier of A by AMI_1:79;
  per cases;
  suppose
A4: i = o;
    hence Exec(I,s+*(o,w)).i = w by A1,A2,FUNCT_7:33
      .= (Exec(I,s) +* (o,w)).i by A3,A4,FUNCT_7:33;
  end;
  suppose
A5: i <> o;
    hence Exec(I,s+*(o,w)).i = s.i by A1,FUNCT_7:34
      .= Exec(I,s).i by AMI_1:def 13
      .= (Exec(I,s) +* (o,w)).i by A5,FUNCT_7:34;
  end;
end;

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
  :Def1:
  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
  :Def2:
  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;
  coherence
  proof
    let o be Object of STC N;
A1: the carrier of STC N = NAT \/ {NAT} by AMISTD_1:def 11;
A2: the Object-Kind of STC N =
    (NAT --> {[1,0],[0,0]}) +* (NAT .--> NAT) by AMISTD_1:def 11;
A3: dom (NAT .--> NAT) = {NAT} by FUNCOP_1:19;
    per cases by A1,XBOOLE_0:def 2;
    suppose
A4:   o in NAT;
      then o <> NAT;
      then not o in dom (NAT .--> NAT) by A3,TARSKI:def 1;
      then
A5:   ObjectKind o = (NAT --> {[1,0],[0,0]}).o by A2,FUNCT_4:12
        .= {[1,0],[0,0]} by A4,FUNCOP_1:13;
A6:   [1,0] <> [0,0] by ZFMISC_1:33;
      [1,0] in {[1,0],[0,0]} & [0,0] in {[1,0],[0,0]} by TARSKI:def 2;
      hence ObjectKind o is non trivial by A5,A6,YELLOW_8:def 1;
    end;
    suppose
A7:   o in {NAT};
      then ObjectKind o = (NAT .--> NAT).o by A2,A3,FUNCT_4:14
        .= NAT by A7,FUNCOP_1:13;
      hence ObjectKind o is non trivial;
    end;
  end;
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)));
  existence
  proof
    take STC N;
    STC N is with_non_trivial_Instructions
    proof
A1:   the Instructions of STC N = {[0,0],[1,0]} by AMISTD_1:def 11;
A2:   [1,0] <> [0,0] by ZFMISC_1:33;
      [1,0] in {[1,0],[0,0]} & [0,0] in {[1,0],[0,0]} by TARSKI:def 2;
      hence the Instructions of STC N is non trivial by A1,A2,YELLOW_8:def 1;
    end;
    hence thesis;
  end;
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));
  coherence
  proof
    let A be definite (non empty stored-program AMI-Struct over IL,N);
    assume
A1: for o being Object of A holds ObjectKind o is non trivial;
    consider l being Instruction-Location of A;
    ObjectKind l = the Instructions of A by AMI_1:def 14;
    hence the Instructions of A is non trivial by A1;
  end;
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);
  existence
  proof
    take STC N;
    thus thesis;
  end;
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;
  coherence by Def2;
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;
  coherence by Def1;
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;
  coherence by AMI_1:def 11;
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
  :Def3:
  for o being Object of A holds o in it iff
  ex s being State of A st s.o <> Exec(I,s).o;
  existence
  proof
    defpred P[set] means ex s being State of A st s.$1 <> Exec(I,s).$1;
    consider X being Subset of A such that
A1: for x being set holds x in X iff x in the carrier of A & P[x]
    from SUBSET_1:sch 1;
    take X;
    thus thesis by A1;
  end;
  uniqueness
  proof
    defpred P[set] means ex s being State of A st s.$1 <> Exec(I,s).$1;
    let a, b be Subset of A such that
Z1:  for o being Object of A holds o in a iff P[o] and
Z2:  for o being Object of A holds o in b iff P[o];
   thus a = b from SUBSET_1:sch 2(Z1,Z2);
  end;
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
  :Def4:
  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));
  existence
  proof
    defpred P[set] means ex l being Object of A st l = $1 &
    for s being State of A, a being Element of ObjectKind l
    holds Exec(I,s) = Exec(I,s+*(l,a));
    consider X being Subset of A such that
A1: for x being set holds x in X iff x in the carrier of A & P[x]
    from SUBSET_1:sch 1;
    take X;
    let l be Object of A;
    hereby
      assume l in X;
      then P[l] by A1;
      hence for s being State of A, a being Element of ObjectKind l
      holds Exec(I,s) = Exec(I,s+*(l,a));
    end;
    thus thesis by A1;
  end;
  uniqueness
  proof
    defpred P[Object of A] means
    for s being State of A, a being Element of ObjectKind $1
    holds Exec(I,s) = Exec(I,s+*($1,a));
   let a, b be Subset of A such that
Z1: for o being Object of A holds o in a iff P[o] and
Z2: for o being Object of A holds o in b iff P[o];
   thus a = b from SUBSET_1:sch 2(Z1,Z2);
  end;
  func Out_U_Inp I -> Subset of A means
  :Def5:
  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);
  existence
  proof
    defpred P[set] means ex l being Object of A st l = $1 &
    ex s being State of A, a being Element of ObjectKind l
    st Exec(I,s+*(l,a)) <> Exec(I,s) +* (l,a);
    consider X being Subset of A such that
A2: for x being set holds x in X iff x in the carrier of A & P[x]
    from SUBSET_1:sch 1;
    take X;
    let l be Object of A;
    hereby
      assume l in X;
      then P[l] by A2;
      hence ex s being State of A, a being Element of ObjectKind l
      st Exec(I,s+*(l,a)) <> Exec(I,s) +* (l,a);
    end;
    thus thesis by A2;
  end;
  uniqueness
  proof
    defpred P[Object of A] means
    ex s being State of A, a being Element of ObjectKind $1
    st Exec(I,s+*($1,a)) <> Exec(I,s) +* ($1,a);
    let a, b be Subset of A such that
Z1:  for o being Object of A holds o in a iff P[o] and
Z2:  for o being Object of A holds o in b iff P[o];
   thus a = b from SUBSET_1:sch 2(Z1,Z2);
  end;
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

  Out_U_Inp I \ Out_\_Inp I;
  coherence;
end;

canceled;

theorem Th10:
  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
proof
  let A be with_non_trivial_ObjectKinds IC-Ins-separated definite
  (non empty stored-program AMI-Struct over NAT,N), I be Instruction of A;
  for o being Object of A holds o in Out_\_Inp I implies o in Output I
  proof
    let o be Object of A;
    assume
A1: not thesis;
    consider s being State of A, a being Element of ObjectKind o;
    consider w being set such that
A2: w in ObjectKind o & w <> a by YELLOW15:4;
    reconsider w as Element of ObjectKind o by A2;
    set t = s +* (o,w);
A3: dom s = the carrier of A by AMI_1:79;
A4: dom t = the carrier of A by AMI_1:79;
A5: Exec(I,t).o = t.o by A1,Def3
      .= w by A3,FUNCT_7:33;
    Exec(I,t+*(o,a)).o = (t+*(o,a)).o by A1,Def3
      .= a by A4,FUNCT_7:33;
    hence contradiction by A1,A2,A5,Def4;
  end;
  hence thesis by SUBSET_1:7;
end;

theorem Th11:
  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
proof
  let A be IC-Ins-separated definite
  (non empty stored-program AMI-Struct over IL,N), I be Instruction of A;
  for o being Object of A holds o in Output I implies o in Out_U_Inp I
  proof
    let o be Object of A;
    assume
A1: not thesis;
    for s being State of A holds s.o = Exec(I,s).o
    proof
      let s be State of A;
      reconsider so = s.o as Element of ObjectKind o by Th2;
A2:   Exec(I,s+*(o,so)) = Exec(I,s) +* (o,so) by A1,Def5;
      dom Exec(I,s) = the carrier of A by AMI_1:79;
      hence s.o = (Exec(I,s) +* (o,so)).o by FUNCT_7:33
        .= Exec(I,s).o by A2,FUNCT_7:37;
    end;
    hence contradiction by A1,Def3;
  end;
  hence thesis by SUBSET_1:7;
end;

canceled;

theorem
  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
proof
  let A be with_non_trivial_ObjectKinds IC-Ins-separated definite
  (non empty stored-program AMI-Struct over NAT,N), I be Instruction of A;
  for o being Object of A holds o in Out_\_Inp I iff o in Output I \ Input I
  proof
    let o be Object of A;
    hereby
      assume
A1:   o in Out_\_Inp I;
A2:   Out_\_Inp I c= Output I by Th10;
      Out_\_Inp I misses Input I by XBOOLE_1:85;
      then not o in Input I by A1,XBOOLE_0:3;
      hence o in Output I \ Input I by A1,A2,XBOOLE_0:def 4;
    end;
    assume
A3: o in Output I \ Input I;
    then
A4: not o in Input I by XBOOLE_0:def 4;
    per cases by A4,XBOOLE_0:def 4;
    suppose
A5:   not o in Out_U_Inp I;
      Output I c= Out_U_Inp I by Th11;
      then not o in Output I by A5;
      hence thesis by A3,XBOOLE_0:def 4;
    end;
    suppose o in Out_\_Inp I;
      hence thesis;
    end;
  end;
  hence thesis by SUBSET_1:8;
end;

theorem
  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
proof
  let A be with_non_trivial_ObjectKinds IC-Ins-separated definite
  (non empty stored-program AMI-Struct over NAT,N), I be Instruction of A;
  for o being Object of A st o in Out_U_Inp I holds o in Output I \/ Input I
  proof
    let o be Object of A such that
A1: o in Out_U_Inp I;
    o in Input I or o in Output I
    proof
      assume
A2:   not o in Input I;
      per cases by A2,XBOOLE_0:def 4;
      suppose not o in Out_U_Inp I;
        hence thesis by A1;
      end;
      suppose
A3:     o in Out_\_Inp I;
        Out_\_Inp I c= Output I by Th10;
        hence thesis by A3;
      end;
    end;
    hence o in Output I \/ Input I by XBOOLE_0:def 2;
  end;
  hence Out_U_Inp I c= Output I \/ Input I by SUBSET_1:7;
  Output I c= Out_U_Inp I & Input I c= Out_U_Inp I by Th11,XBOOLE_1:36;
  hence thesis by XBOOLE_1:8;
end;

theorem Th15:
  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
proof
  let A be IC-Ins-separated definite
  (non empty stored-program AMI-Struct over IL,N), I be Instruction of A,
  o be Object of A such that
A1: ObjectKind o is trivial;
  assume o in Out_U_Inp I;
  then consider s being State of A, a being Element of ObjectKind o such that
A2: Exec(I,s+*(o,a)) <> Exec(I,s) +* (o,a) by Def5;
  s.o is Element of ObjectKind o by Th2;
  then s.o = a by A1,YELLOW_8:def 1;
  then
A3: Exec(I,s+*(o,a)) = Exec(I,s) by FUNCT_7:37;
A4: dom (Exec(I,s) +* (o,a)) = the carrier of A by AMI_1:79;
A5: dom Exec(I,s) = the carrier of A by AMI_1:79;
  for x being set st x in the carrier of A holds
  (Exec(I,s) +* (o,a)).x = Exec(I,s).x
  proof
    let x be set such that x in the carrier of A;
    per cases;
    suppose
A6:   x = o;
A7:   Exec(I,s).o is Element of ObjectKind o by Th2;
      thus (Exec(I,s) +* (o,a)).x = a by A5,A6,FUNCT_7:33
        .= Exec(I,s).x by A1,A6,A7,YELLOW_8:def 1;
    end;
    suppose x <> o;
      hence (Exec(I,s) +* (o,a)).x = Exec(I,s).x by FUNCT_7:34;
    end;
  end;
  hence contradiction by A2,A3,A4,A5,FUNCT_1:9;
end;

theorem
  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
proof
  let A be IC-Ins-separated definite
  (non empty stored-program AMI-Struct over IL,N), I be Instruction of A,
  o be Object of A;
  assume
A1: ObjectKind o is trivial;
  Input I c= Out_U_Inp I by XBOOLE_1:36;
  hence thesis by A1,Th15;
end;

theorem
  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
proof
  let A be IC-Ins-separated definite
  (non empty stored-program AMI-Struct over IL,N), I be Instruction of A,
  o be Object of A;
  assume
A1: ObjectKind o is trivial;
  Output I c= Out_U_Inp I by Th11;
  hence thesis by A1,Th15;
end;

theorem Th18:
  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
proof
  let A be IC-Ins-separated definite
  (non empty stored-program AMI-Struct over IL,N), I be Instruction of A;
  thus I is halting implies Output I is empty
  proof
    assume
A1: for s being State of A holds Exec(I,s) = s;
    assume not thesis;
    then consider o being Object of A such that
A2: o in Output I by SUBSET_1:10;
    ex s being State of A st s.o <> Exec(I,s).o by A2,Def3;
    hence thesis by A1;
  end;
  assume
A3: Output I is empty;
  let s be State of A;
A4: dom s = the carrier of A by AMI_1:79;
A5: dom Exec(I,s) = the carrier of A by AMI_1:79;
  assume Exec(I,s) <> s;
  then ex x being set st x in the carrier of A & Exec(I,s).x <> s.x
  by A4,A5,FUNCT_1:9;
  hence contradiction by A3,Def3;
end;

theorem Th19:
  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
proof
  let A be with_non_trivial_ObjectKinds IC-Ins-separated definite
  (non empty stored-program AMI-Struct over NAT,N),
  I be Instruction of A such that
A1: I is halting;
  Out_\_Inp I c= Output I by Th10;
  then Out_\_Inp I c= {} by A1,Th18;
  hence thesis by XBOOLE_1:3;
end;

theorem Th20:
  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
proof
  let A be IC-Ins-separated definite
  (non empty stored-program AMI-Struct over IL,N),
  I be Instruction of A such that
A1: for s being State of A holds Exec(I,s) = s;
  assume not thesis;
  then consider o being Object of A such that
A2: o in Out_U_Inp I by SUBSET_1:10;
  consider s being State of A, a being Element of ObjectKind o such that
A3: Exec(I,s+*(o,a)) <> Exec(I,s) +* (o,a) by A2,Def5;
  Exec(I,s+*(o,a)) = s+*(o,a) by A1
    .= Exec(I,s) +* (o,a) by A1;
  hence thesis by A3;
end;

theorem Th21:
  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
proof
  let A be IC-Ins-separated definite
  (non empty stored-program AMI-Struct over IL,N),
  I be Instruction of A such that
A1: I is halting;
  Input I = {} \ Out_\_Inp I by A1,Th20
    .= {};
  hence thesis;
end;

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;
  coherence by Th21;
  cluster Output I -> empty;
  coherence by Th18;
  cluster Out_U_Inp I -> empty;
  coherence by Th20;
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);
  existence
  proof
    take STC N;
    thus thesis;
  end;
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;
  coherence by Th19;
end;

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

theorem
  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
proof
  let A be with_non_trivial_Instructions steady-programmed IC-Ins-separated
  definite (non empty stored-program AMI-Struct over NAT,N),
  f be Instruction-Location of A, I be Instruction of A;
  consider t being State of A;
  consider J being set such that
A1: J in the Instructions of A & t.f <> J by YELLOW15:4;
  reconsider J as Element of ObjectKind f by A1,AMI_1:def 14;
  set s = t +* (f,J);
A2: dom t = the carrier of A by AMI_1:79;
A3: Exec(I,t).f = t.f by AMI_1:def 13;
  Exec(I,s).f = s.f by AMI_1:def 13
    .= J by A2,FUNCT_7:33;
  hence thesis by A1,A3,Def4;
end;

theorem
  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
proof
  let A be standard (IC-Ins-separated definite
  (non empty stored-program AMI-Struct over NAT,N)), I be Instruction of A;
  consider t being State of A;
  assume
A1: for s being State of A holds Exec(I,s).IC A = NextLoc IC s;
  set l = IC A;
  NextLoc IC t in NAT by AMI_1:def 4;
  then reconsider w = NextLoc IC t as Element of ObjectKind l by AMI_1:def 11;
  set s = t +* (l,w);
A2: Exec(I,t).l = NextLoc IC t & Exec(I,s).l = NextLoc IC s by A1;
  dom t = the carrier of A by AMI_1:79;
  then Exec(I,t) <> Exec(I,s) by A2,AMISTD_1:35,FUNCT_7:33;
  hence thesis by Def4;
end;

theorem
  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 by Def3;

registration
  let N;
  cluster standard (IC-Ins-separated definite
    (non empty stored-program AMI-Struct over NAT,N));
  existence
  proof
    take STC N;
    thus thesis;
  end;
end;

theorem
  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
proof
  let A be standard (IC-Ins-separated definite
  (non empty stored-program AMI-Struct over NAT,N)),
  I be Instruction of A such that
A1: for s being State of A holds Exec(I, s).IC A = NextLoc IC s;
  consider s being State of A;
  Exec(I,s).IC A = NextLoc IC s by A1;
  then Exec(I,s).IC A <> IC s by AMISTD_1:35;
  hence IC A in Output I by Def3;
end;

theorem Th26:
  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
proof
  let A be IC-Ins-separated definite
  (non empty stored-program AMI-Struct over IL,N), I be Instruction of A;
  assume ex s being State of A st Exec(I,s).IC A <> IC s;
  then
A1: IC A in Output I by Def3;
  Output I c= Out_U_Inp I by Th11;
  hence thesis by A1;
end;

theorem
  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
proof
  let A be standard (IC-Ins-separated definite
  (non empty stored-program AMI-Struct over NAT,N)), I be Instruction of A;
  assume
A1: for s being State of A holds Exec(I,s).IC A = NextLoc IC s;
  consider s being State of A;
  Exec(I,s).IC A = NextLoc IC s by A1;
  then Exec(I,s).IC A <> IC s by AMISTD_1:35;
  hence thesis by Th26;
end;

theorem
  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
proof
  let A be IC-Ins-separated definite
  (non empty stored-program AMI-Struct over IL,N),
  f be Instruction-Location of A, I be Instruction of A such that
A1: for s being State of A, p being programmed FinPartState of A
  holds Exec (I, s +* p) = Exec (I,s) +* p;
  assume f in Out_U_Inp I;
  then consider s being State of A, w being Element of ObjectKind f such that
A2: Exec(I,s+*(f,w)) <> Exec(I,s) +* (f,w) by Def5;
A3: dom s = the carrier of A by AMI_1:79;
A4: dom Exec(I,s) = the carrier of A by AMI_1:79;
  set p = f .--> w;
A5: f in IL by AMI_1:def 4;
  dom p = {f} by FUNCOP_1:19;
  then dom p c= IL by A5,ZFMISC_1:37;
  then reconsider p as programmed FinPartState of A by AMI_1:def 40;
A6: s+*(f,w) = s +* p by A3,FUNCT_7:def 3;
  Exec (I, s +* p) = Exec (I,s) +* p by A1;
  hence thesis by A2,A4,A6,FUNCT_7:def 3;
end;

theorem
  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
proof
  let A be IC-Ins-separated definite
  (standard-ins non empty stored-program AMI-Struct over IL,N),
  I be Instruction of A, o be Object of A;
  assume
A1: for s being State of A, o being Object of A, J being Instruction of A
  st InsCode I = InsCode J & o <> IC A holds Exec(J,s).o = s.o;
  assume o in Output I;
  then ex s being State of A st s.o <> Exec(I,s).o by Def3;
  hence o = IC A by A1;
end;