The abstract of the Mizar article:

Introduction to Circuits, I

by

Yatsuka Nakamura,

Piotr Rudnicki,

Andrzej Trybulec, and

Pauline N. Kawamoto

Received December 15, 1994

MML identifier: CIRCUIT1

[ Mizar article, MML identifier index ]

environ

 vocabulary AMI_1, MSAFREE2, MSUALG_1, PRE_CIRC, ZF_REFLE, PBOOLE, RELAT_1,
      FUNCT_1, UNIALG_2, BOOLE, FINSEQ_1, TDGROUP, PRALG_1, FUNCOP_1, PRALG_2,
      CARD_3, QC_LANG1, TREES_3, TREES_4, MSAFREE, FINSET_1, TREES_2, TREES_1,
      DTCONSTR, LANG1, FUNCT_6, PROB_1, FREEALG, CARD_1, SQUARE_1, ARYTM_1,
      FUNCT_4, CIRCUIT1, FINSEQ_4, ORDINAL2, ARYTM, MEMBERED;
 notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL2, ORDINAL1, NUMBERS,
      XREAL_0, REAL_1, NAT_1, MEMBERED, RELAT_1, STRUCT_0, FUNCT_1, FINSEQ_1,
      RELSET_1, FINSET_1, GROUP_1, CARD_1, PROB_1, CARD_3, FINSEQ_4, FUNCT_4,
      FUNCT_6, TREES_1, TREES_2, TREES_3, TREES_4, LANG1, DTCONSTR, PBOOLE,
      MSUALG_1, MSUALG_2, PRALG_2, MSAFREE, PRE_CIRC, MSAFREE2;
 constructors NAT_1, REAL_1, PRALG_2, PRE_CIRC, MSAFREE2, GROUP_1, FINSOP_1,
      FINSEQ_4, MEMBERED, XBOOLE_0;
 clusters FUNCT_1, FINSET_1, PRELAMB, TREES_1, TREES_2, TREES_3, MSUALG_1,
      PRALG_1, DTCONSTR, MSAFREE, PRE_CIRC, MSAFREE2, STRUCT_0, FINSEQ_1,
      RELSET_1, NAT_1, MEMBERED, XREAL_0, XBOOLE_0, ORDINAL2;
 requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;


begin

::---------------------------------------------------------------------------
:: Circuits
::---------------------------------------------------------------------------

definition
  let S be non void Circuit-like (non empty ManySortedSign);
  mode Circuit of S is locally-finite MSAlgebra over S;
end;

reserve IIG for Circuit-like non void (non empty ManySortedSign);

definition
  let IIG;
  let SCS be non-empty Circuit of IIG;
  func Set-Constants SCS -> ManySortedSet of SortsWithConstants IIG means
:: CIRCUIT1:def 1

    for x being Vertex of IIG st x in dom it
      holds it.x in Constants (SCS, x);
end;

theorem :: CIRCUIT1:1
    for IIG
  for SCS being non-empty Circuit of IIG,
    v being Vertex of IIG,
    e being Element of (the Sorts of SCS).v
      st v in SortsWithConstants IIG & e in Constants (SCS, v)
    holds (Set-Constants SCS).v = e;

definition
  let IIG;
  let CS be Circuit of IIG;
  mode InputFuncs of CS is ManySortedFunction of
    ((InputVertices IIG) --> NAT),
    ((the Sorts of CS) | InputVertices IIG);
end;

theorem :: CIRCUIT1:2
  for IIG
  for SCS being non-empty Circuit of IIG, InpFs being InputFuncs of SCS,
      n being Nat
    st IIG is with_input_V
    holds (commute InpFs).n is InputValues of SCS;

definition
  let IIG such that
  IIG is with_input_V;
  let SCS be non-empty Circuit of IIG,
    InpFs be InputFuncs of SCS,
    n be Nat;
  func n-th_InputValues InpFs -> InputValues of SCS equals
:: CIRCUIT1:def 2
      (commute InpFs).n;
end;

definition
  let IIG;
  let SCS be Circuit of IIG;
  mode State of SCS is Element of product (the Sorts of SCS);
end;

canceled;

theorem :: CIRCUIT1:4
    for IIG
  for SCS being non-empty Circuit of IIG, s being State of SCS
    holds dom s = the carrier of IIG;

theorem :: CIRCUIT1:5
    for IIG
  for SCS being non-empty Circuit of IIG, s being State of SCS,
    v being Vertex of IIG
    holds s.v in (the Sorts of SCS).v;

definition
  let IIG;
  let SCS be non-empty Circuit of IIG,
    s be State of SCS,
    o be OperSymbol of IIG;
  func o depends_on_in s -> Element of Args (o, SCS) equals
:: CIRCUIT1:def 3
             s * (the_arity_of o);
end;

reserve IIG for monotonic Circuit-like
  (non void non empty ManySortedSign);

theorem :: CIRCUIT1:6
  for IIG
  for SCS being locally-finite non-empty MSAlgebra over IIG,
    v, w being Vertex of IIG,
    e1 being Element of (the Sorts of FreeEnv SCS).v,
    q1 being DTree-yielding FinSequence
      st v in InnerVertices IIG &
         e1 = [action_at v,the carrier of IIG]-tree q1
    holds
      for k being Nat st k in dom q1
        & q1.k in (the Sorts of FreeEnv SCS).w
        holds w = (the_arity_of action_at v)/.k;

definition
  let IIG;
  let SCS be locally-finite non-empty MSAlgebra over IIG,
    v be Vertex of IIG;
  cluster -> finite non empty
   Function-like Relation-like Element of (the Sorts of FreeEnv SCS).v;
end;

definition
  let IIG;
  let SCS be locally-finite non-empty MSAlgebra over IIG,
    v be Vertex of IIG;
  cluster -> DecoratedTree-like Element of (the Sorts of FreeEnv SCS).v;
end;

theorem :: CIRCUIT1:7
  for IIG
  for SCS being locally-finite non-empty MSAlgebra over IIG,
    v, w being Vertex of IIG,
    e1 being Element of (the Sorts of FreeEnv SCS).v,
    e2 being Element of (the Sorts of FreeEnv SCS).w,
    q1 being DTree-yielding FinSequence, k1 being Nat
      st v in InnerVertices IIG \ SortsWithConstants IIG
        & e1 = [action_at v,the carrier of IIG]-tree q1
        & k1+1 in dom q1
        & q1.(k1+1) in (the Sorts of FreeEnv SCS).w
      holds e1 with-replacement (<*k1*>,e2) in (the Sorts of FreeEnv SCS).v;

theorem :: CIRCUIT1:8
  for IIG
  for A being locally-finite non-empty MSAlgebra over IIG,
    v being Element of IIG,
    e being Element of (the Sorts of FreeEnv A).v
      st 1 < card e
    ex o being OperSymbol of IIG st e.{} = [o,the carrier of IIG];

theorem :: CIRCUIT1:9
    for IIG being non void Circuit-like (non empty ManySortedSign)
  for SCS being non-empty Circuit of IIG, s being State of SCS,
    o being OperSymbol of IIG
    holds (Den(o,SCS)).(o depends_on_in s)
      in (the Sorts of SCS).(the_result_sort_of o);

theorem :: CIRCUIT1:10
  for IIG
  for A being non-empty Circuit of IIG, v being Vertex of IIG,
    e being Element of (the Sorts of FreeEnv A).v
      st e.{} = [action_at v,the carrier of IIG]
   ex p being DTree-yielding FinSequence st
        e = [action_at v,the carrier of IIG]-tree p;

begin :: Size

definition
  let IIG be monotonic non void (non empty ManySortedSign);
  let A be locally-finite non-empty MSAlgebra over IIG;
  let v be SortSymbol of IIG;
 cluster (the Sorts of FreeEnv A).v -> finite;
end;

definition
  let IIG;
  let A be locally-finite non-empty MSAlgebra over IIG;
  let v be SortSymbol of IIG;
  func size(v,A) -> natural number means
:: CIRCUIT1:def 4

    ex s being finite non empty Subset of NAT
      st s = { card t where t is Element of (the Sorts of FreeEnv A).v :
                 not contradiction }
        & it = max s;
end;

theorem :: CIRCUIT1:11
  for IIG
  for A being locally-finite non-empty MSAlgebra over IIG,
    v being Element of IIG
    holds size(v,A) = 1
      iff v in InputVertices IIG \/ SortsWithConstants IIG;

theorem :: CIRCUIT1:12
    for IIG
  for SCS being locally-finite non-empty MSAlgebra over IIG,
    v, w being Vertex of IIG,
    e1 being Element of (the Sorts of FreeEnv SCS).v,
    e2 being Element of (the Sorts of FreeEnv SCS).w,
    q1 being DTree-yielding FinSequence
      st v in InnerVertices IIG \ SortsWithConstants IIG
        & card e1 = size(v,SCS)
        & e1 = [action_at v,the carrier of IIG]-tree q1
        & e2 in rng q1
    holds card e2 = size(w,SCS);

theorem :: CIRCUIT1:13
  for IIG
  for A being locally-finite non-empty MSAlgebra over IIG,
    v being Vertex of IIG,
    e being Element of (the Sorts of FreeEnv A).v
      st v in (InnerVertices IIG \ SortsWithConstants IIG)
        & card e = size(v,A)
    ex q being DTree-yielding FinSequence st
       e = [action_at v,the carrier of IIG]-tree q;

theorem :: CIRCUIT1:14
    for IIG
  for A being locally-finite non-empty MSAlgebra over IIG,
    v being Vertex of IIG,
    e being Element of (the Sorts of FreeEnv A).v
      st v in (InnerVertices IIG \ SortsWithConstants IIG)
        & card e = size(v,A)
    ex o being OperSymbol of IIG st e.{} = [o,the carrier of IIG];

definition
  let S be non void (non empty ManySortedSign),
      A be locally-finite non-empty MSAlgebra over S,
    v be SortSymbol of S,
    e be Element of (the Sorts of FreeEnv A).v;
  func depth e -> Nat means
:: CIRCUIT1:def 5
 ex e' being Element of (the Sorts of FreeMSA the Sorts of A).v st
      e = e' & it = depth e';
end;

theorem :: CIRCUIT1:15
  for IIG
  for A being locally-finite non-empty MSAlgebra over IIG,
    v, w being Element of IIG
      st v in InnerVertices IIG & w in rng the_arity_of action_at v
    holds size(w,A) < size(v,A);

theorem :: CIRCUIT1:16
  for IIG
  for A being locally-finite non-empty MSAlgebra over IIG,
    v being SortSymbol of IIG
    holds size(v,A) > 0;

theorem :: CIRCUIT1:17
    for IIG
  for A being non-empty Circuit of IIG, v being Vertex of IIG,
    e being Element of (the Sorts of FreeEnv A).v,
    p being DTree-yielding FinSequence
      st v in InnerVertices IIG
        & e = [action_at v,the carrier of IIG]-tree p
        & for k being Nat st k in dom p
            ex ek being Element of (the Sorts of FreeEnv A)
              .((the_arity_of action_at v)/.k) st ek = p.k
              & card ek = size ((the_arity_of action_at v)/.k, A)
    holds card e = size(v,A);

begin :: Depth

definition
  let S be monotonic non void (non empty ManySortedSign),
    A be locally-finite non-empty MSAlgebra over S,
    v be SortSymbol of S;
  func depth(v,A) -> natural number means
:: CIRCUIT1:def 6

    ex s being finite non empty Subset of NAT st
      s = { depth t where t is Element of (the Sorts of FreeEnv A).v :
               not contradiction }
      & it = max s;
end;

definition
  let IIG be finite monotonic
    Circuit-like non void (non empty ManySortedSign),
    A be non-empty Circuit of IIG;
  func depth A -> natural number means
:: CIRCUIT1:def 7

    ex Ds being finite non empty Subset of NAT st
      Ds = { depth(v,A) where v is Element of IIG :
      v in the carrier of IIG }
      & it = max Ds;
end;

theorem :: CIRCUIT1:18
    for IIG being finite monotonic
    Circuit-like (non void non empty ManySortedSign),
    A being non-empty Circuit of IIG,
    v being Vertex of IIG
    holds depth(v,A) <= depth A;

theorem :: CIRCUIT1:19
  for IIG
  for A being non-empty Circuit of IIG, v being Vertex of IIG
    holds depth(v,A) = 0
      iff v in InputVertices IIG or v in SortsWithConstants IIG;

theorem :: CIRCUIT1:20
    for IIG
  for A being locally-finite non-empty MSAlgebra over IIG,
    v, v1 being SortSymbol of IIG
      st v in InnerVertices IIG & v1 in rng the_arity_of action_at v
    holds depth(v1,A) < depth(v,A);