:: Introduction to Circuits, I
:: by Yatsuka Nakamura, Piotr Rudnicki, Andrzej Trybulec and Pauline N. Kawamoto
::
:: Received December 15, 1994
:: Copyright (c) 1994-2016 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, STRUCT_0, MSAFREE2, XBOOLE_0, MSUALG_1, FINSET_1,
RELAT_1, PBOOLE, GLIB_000, FUNCT_1, UNIALG_2, SUBSET_1, FINSEQ_1,
FUNCOP_1, FUNCT_6, FSM_1, CARD_3, MARGREL1, TREES_3, TREES_4, PARTFUN1,
MSAFREE, TREES_2, ARYTM_3, TREES_1, ZFMISC_1, LANG1, DTCONSTR, TREES_A,
TDGROUP, TARSKI, NAT_1, ORDINAL4, CARD_1, XXREAL_0, MEMBERED, ARYTM_1,
FUNCT_4, REAL_1, CIRCUIT1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, CARD_1, NUMBERS,
XCMPLX_0, XREAL_0, REAL_1, NAT_1, MEMBERED, RELAT_1, FUNCT_1, PBOOLE,
PARTFUN1, FINSEQ_1, FINSEQ_2, RELSET_1, FINSET_1, CARD_3, FUNCT_4,
FUNCT_6, TREES_1, TREES_2, TREES_3, TREES_4, STRUCT_0, LANG1, DTCONSTR,
MSUALG_1, MSUALG_2, MSAFREE, XXREAL_2, FUNCOP_1, MSAFREE2, XXREAL_0;
constructors FUNCT_4, REAL_1, MSUALG_2, MSAFREE2, SEQ_4, RELSET_1, NUMBERS;
registrations XBOOLE_0, RELAT_1, FUNCT_1, ORDINAL1, FINSET_1, XXREAL_0,
XREAL_0, NAT_1, MEMBERED, FINSEQ_1, TREES_1, CARD_3, PBOOLE, TREES_2,
TREES_3, PRE_CIRC, STRUCT_0, DTCONSTR, MSUALG_1, MSAFREE, MSAFREE2,
FUNCT_2, XXREAL_2, CARD_1, RELSET_1;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
begin
::---------------------------------------------------------------------------
:: Circuits
::---------------------------------------------------------------------------
definition
let S be non void Circuit-like non empty ManySortedSign;
mode Circuit of S is finite-yielding 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
qua ManySortedSet of InputVertices IIG), ((the Sorts of CS) | InputVertices IIG
qua ManySortedSet of 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;
theorem :: CIRCUIT1:3
for IIG for SCS being non-empty Circuit of IIG, s being State of SCS
holds dom s = the carrier of IIG;
theorem :: CIRCUIT1:4
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:5
for IIG for SCS being finite-yielding 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 Element of NAT st k
in dom q1 & q1.k in (the Sorts of FreeEnv SCS).w holds w = (the_arity_of
action_at v)/.k;
registration
let IIG;
let SCS be finite-yielding non-empty MSAlgebra over IIG, v be Vertex of IIG;
cluster -> finite non empty Function-like Relation-like for Element of (the
Sorts of FreeEnv SCS).v;
end;
registration
let IIG;
let SCS be finite-yielding non-empty MSAlgebra over IIG, v be Vertex of IIG;
cluster -> DecoratedTree-like for Element of (the Sorts of FreeEnv SCS).v;
end;
theorem :: CIRCUIT1:6
for IIG for SCS being finite-yielding 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 Element of 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:7
for IIG for A being finite-yielding 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:8
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:9
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
registration
let IIG be monotonic non void non empty ManySortedSign;
let A be finite-yielding 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 finite-yielding non-empty MSAlgebra over IIG;
let v be SortSymbol of IIG;
func size(v,A) -> Nat means
:: CIRCUIT1:def 4
ex s being finite non empty
Subset of NAT st s = the set of all
card t where t is Element of (the Sorts of FreeEnv A).v
& it = max s;
end;
theorem :: CIRCUIT1:10
for IIG for A being finite-yielding non-empty MSAlgebra over IIG
, v being Element of IIG holds size(v,A) = 1 iff v in InputVertices IIG \/
SortsWithConstants IIG;
theorem :: CIRCUIT1:11
for IIG for SCS being finite-yielding 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:12
for IIG for A being finite-yielding 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:13
for IIG for A being finite-yielding 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 finite-yielding non-empty
MSAlgebra over S, v be SortSymbol of S, e be Element of (the Sorts of FreeEnv A
).v;
func depth e -> Element of NAT means
:: CIRCUIT1:def 5
ex e9 being Element of (the
Sorts of FreeMSA the Sorts of A).v st e = e9 & it = depth e9;
end;
theorem :: CIRCUIT1:14
for IIG for A being finite-yielding 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:15
for IIG for A being finite-yielding non-empty MSAlgebra over IIG
, v being SortSymbol of IIG holds size(v,A) > 0;
theorem :: CIRCUIT1:16
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 Element of 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 finite-yielding
non-empty MSAlgebra over S, v be SortSymbol of S;
func depth(v,A) -> Nat means
:: CIRCUIT1:def 6
ex s being finite non empty
Subset of NAT st s = the set of all
depth t where t is Element of (the Sorts of FreeEnv A).v
& 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 -> Nat 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:17
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:18
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:19
for IIG for A being finite-yielding 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);