:: Introduction to Circuits, II
:: by Yatsuka Nakamura, Piotr Rudnicki, Andrzej Trybulec and Pauline N. Kawamoto
::
:: Received April 10, 1995
:: Copyright (c) 1995-2021 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 MSAFREE2, STRUCT_0, XBOOLE_0, MSUALG_1, RELAT_1, PBOOLE, MSAFREE,
FUNCOP_1, FUNCT_1, TREES_3, FINSEQ_1, SUBSET_1, TREES_4, MSUALG_3,
MARGREL1, FINSEQ_4, TARSKI, DTCONSTR, NAT_1, NUMBERS, TREES_2, CARD_3,
PARTFUN1, ZFMISC_1, TDGROUP, CIRCUIT1, FSM_1, FUNCT_4, GLIB_000,
UNIALG_2, MSATERM, PRELAMB, REALSET1, CARD_1, XXREAL_0, ARYTM_3, FUNCT_6,
TREES_A, FINSET_1, CIRCUIT2;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, CARD_1, ORDINAL1, NUMBERS,
RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2, FUNCT_4, XXREAL_0, XCMPLX_0, NAT_1,
FINSEQ_1, FINSEQ_2, FINSET_1, TREES_2, TREES_3, TREES_4, CARD_3, FUNCT_6,
LANG1, DTCONSTR, PBOOLE, FUNCOP_1, XXREAL_2, STRUCT_0, PRALG_1, MSUALG_1,
MSUALG_2, MSUALG_3, MSAFREE, MSAFREE2, CIRCUIT1, MSATERM;
constructors PRALG_1, MSUALG_3, MSATERM, CIRCUIT1, SEQ_4, RELSET_1, FUNCT_4;
registrations XBOOLE_0, RELAT_1, FUNCT_1, ORDINAL1, FUNCOP_1, FINSET_1,
XREAL_0, MEMBERED, FINSEQ_1, CARD_3, TREES_3, PRE_CIRC, STRUCT_0,
MSUALG_1, MSUALG_3, MSAFREE, MSAFREE2, CIRCUIT1, XXREAL_2, CARD_1,
RELSET_1, PBOOLE;
requirements NUMERALS, BOOLE, SUBSET;
begin
reserve IIG for monotonic Circuit-like non void non empty ManySortedSign;
theorem :: CIRCUIT2:1
for X being non-empty ManySortedSet of the carrier of IIG,
H being ManySortedFunction of FreeMSA X, FreeMSA X,
HH being Function-yielding Function,
v being SortSymbol of IIG,
p being DTree-yielding FinSequence,
t being Element of (the Sorts of FreeMSA X).v st
v in InnerVertices IIG & t = [action_at v,the carrier of IIG]-tree p &
H is_homomorphism FreeMSA X, FreeMSA X
& HH = H * the_arity_of action_at v ex HHp being DTree-yielding FinSequence st
HHp = HH..p & H.v.t = [action_at v,the carrier of IIG]-tree HHp;
definition
let IIG;
let SCS be non-empty Circuit of IIG, s be State of SCS,
iv be InputValues of SCS;
redefine func s +* iv -> State of SCS;
end;
definition
let IIG;
let A be non-empty Circuit of IIG, iv be InputValues of A;
func Fix_inp iv -> ManySortedFunction of FreeGen the Sorts of A, the Sorts
of FreeEnv A means
:: CIRCUIT2:def 1
for v being Vertex of IIG holds (v in InputVertices
IIG implies it.v = FreeGen(v, the Sorts of A) --> root-tree[iv.v, v]) & (v in
SortsWithConstants IIG implies it.v = FreeGen(v, the Sorts of A) --> root-tree
[action_at v,the carrier of IIG]) & (v in (InnerVertices IIG \
SortsWithConstants IIG) implies it.v = id FreeGen(v, the Sorts of A));
end;
definition
let IIG;
let A be non-empty Circuit of IIG, iv be InputValues of A;
func Fix_inp_ext iv -> ManySortedFunction of FreeEnv A, FreeEnv A means
:: CIRCUIT2:def 2
it is_homomorphism FreeEnv A, FreeEnv A & Fix_inp iv c= it;
end;
theorem :: CIRCUIT2:2
for A being non-empty Circuit of IIG, iv being InputValues of A,
v being Vertex of IIG, e being Element of (the Sorts of FreeEnv A).v, x being
set st v in InnerVertices IIG \ SortsWithConstants IIG & e = root-tree[x,v]
holds (Fix_inp_ext iv).v.e = e;
theorem :: CIRCUIT2:3
for A being non-empty Circuit of IIG, iv being InputValues of A,
v being Vertex of IIG, x being Element of (the Sorts of A).v st v in
InputVertices IIG holds (Fix_inp_ext iv).v.(root-tree[x,v]) = root-tree[iv.v,v]
;
theorem :: CIRCUIT2:4
for A being non-empty Circuit of IIG, iv being InputValues of A,
v being Vertex of IIG, e being Element of (the Sorts of FreeEnv A).v, p, q
being DTree-yielding FinSequence st v in InnerVertices IIG & e = [action_at v,
the carrier of IIG]-tree p & dom p = dom q & for k being Element of NAT st k in
dom p holds q.k = (Fix_inp_ext iv).((the_arity_of action_at v)/.k).(p.k) holds
(Fix_inp_ext iv).v.e = [action_at v,the carrier of IIG]-tree q;
theorem :: CIRCUIT2:5
for A being non-empty Circuit of IIG, iv being InputValues of A,
v being Vertex of IIG, e being Element of (the Sorts of FreeEnv A).v st v in
SortsWithConstants IIG holds (Fix_inp_ext iv).v.e = root-tree[action_at v,the
carrier of IIG];
theorem :: CIRCUIT2:6
for A being non-empty Circuit of IIG, iv being InputValues of A,
v being Vertex of IIG, e, e1 being Element of (the Sorts of FreeEnv A).v, t, t1
being DecoratedTree st t = e & t1 = e1 & e1 = (Fix_inp_ext iv).v.e holds dom t
= dom t1;
theorem :: CIRCUIT2:7
for A being non-empty Circuit of IIG, iv being InputValues of A,
v being Vertex of IIG, e, e1 being Element of (the Sorts of FreeEnv A).v st e1
= (Fix_inp_ext iv).v.e holds card e = card e1;
definition
let IIG;
let SCS be non-empty Circuit of IIG, v be Vertex of IIG, iv be InputValues
of SCS;
func IGTree(v,iv) -> Element of (the Sorts of FreeEnv SCS).v means
:: CIRCUIT2:def 3
ex
e being Element of (the Sorts of FreeEnv SCS).v st card e = size(v,SCS) & it =
(Fix_inp_ext iv).v.e;
end;
theorem :: CIRCUIT2:8
for SCS being non-empty Circuit of IIG, v being Vertex of IIG,
iv being InputValues of SCS holds
IGTree(v,iv) = (Fix_inp_ext iv).v.IGTree(v,iv);
theorem :: CIRCUIT2:9
for SCS being non-empty Circuit of IIG, v being Vertex of IIG, iv
being InputValues of SCS, p being DTree-yielding FinSequence st v in
InnerVertices IIG & dom p = dom the_arity_of action_at v & for k being Element
of NAT st k in dom p holds p.k = IGTree((the_arity_of action_at v)/.k, iv)
holds IGTree(v,iv) = [action_at v,the carrier of IIG]-tree p;
definition
let IIG;
let SCS be non-empty Circuit of IIG, v be Vertex of IIG,
iv be InputValues of SCS;
func IGValue(v,iv) -> Element of (the Sorts of SCS).v equals
:: CIRCUIT2:def 4
(Eval SCS).v.(IGTree(v,iv));
end;
theorem :: CIRCUIT2:10
for SCS being non-empty Circuit of IIG, v being Vertex of IIG,
iv being InputValues of SCS st v in InputVertices IIG holds IGValue(v,iv) = iv.
v;
theorem :: CIRCUIT2:11
for SCS being non-empty Circuit of IIG, v being Vertex of IIG,
iv being InputValues of SCS st v in SortsWithConstants IIG holds IGValue(v,iv)
= (Set-Constants SCS).v;
begin
::---------------------------------------------------------------------------
:: Computations
::---------------------------------------------------------------------------
definition
let IIG be Circuit-like non void non empty ManySortedSign;
let SCS be non-empty Circuit of IIG, s be State of SCS;
func Following s -> State of SCS means
:: CIRCUIT2:def 5
for v being Vertex of IIG
holds (v in InputVertices IIG implies it.v = s.v) & (v in InnerVertices IIG
implies it.v = (Den(action_at v,SCS)).(action_at v depends_on_in s));
end;
theorem :: CIRCUIT2:12
for SCS being non-empty Circuit of IIG, s being State of SCS, iv
being InputValues of SCS st iv c= s holds iv c= Following s;
definition
let IIG be Circuit-like non void non empty ManySortedSign;
let SCS be non-empty Circuit of IIG;
let IT be State of SCS;
attr IT is stable means
:: CIRCUIT2:def 6
IT = Following IT;
end;
definition
let IIG;
let SCS be non-empty Circuit of IIG, s be State of SCS, iv be InputValues of
SCS;
func Following(s,iv) -> State of SCS equals
:: CIRCUIT2:def 7
Following(s+*iv);
end;
definition
let IIG;
let SCS be non-empty Circuit of IIG, InpFs be InputFuncs of SCS, s be State
of SCS;
func InitialComp(s,InpFs) -> State of SCS equals
:: CIRCUIT2:def 8
s +* (0-th_InputValues
InpFs) +* Set-Constants SCS;
end;
definition
let IIG;
let SCS be non-empty Circuit of IIG, InpFs be InputFuncs of SCS, s be State
of SCS;
func Computation(s,InpFs) -> sequence of (product the Sorts of SCS)
means
:: CIRCUIT2:def 9
it.0 = InitialComp(s,InpFs) & for i being Nat holds it.(i+1) =
Following(it.i,(i+1)-th_InputValues InpFs);
end;
reserve SCS for non-empty Circuit of IIG;
reserve s for State of SCS;
reserve iv for InputValues of SCS;
theorem :: CIRCUIT2:13
for k being Nat st for v being Vertex of IIG st depth
(v,SCS) <= k holds s.v = IGValue(v,iv) holds for v1 being Vertex of IIG st
depth(v1,SCS) <= k+1 holds (Following s).v1 = IGValue(v1,iv);
reserve IIG for finite monotonic Circuit-like non void non empty
ManySortedSign;
reserve SCS for non-empty Circuit of IIG;
reserve InpFs for InputFuncs of SCS;
reserve s for State of SCS;
reserve iv for InputValues of SCS;
theorem :: CIRCUIT2:14
commute InpFs is constant & InputVertices IIG is non empty
implies for s, iv st iv = (commute InpFs).0 for k being Nat holds iv
c= (Computation(s,InpFs)).k;
theorem :: CIRCUIT2:15
for n being Element of NAT st commute InpFs is constant &
InputVertices IIG is non empty & (Computation(s,InpFs)).n is stable
for m being Nat st n <= m
holds (Computation(s,InpFs)).n = (Computation(s,InpFs)).m;
theorem :: CIRCUIT2:16
commute InpFs is constant & InputVertices IIG is non empty
implies for s, iv st iv = (commute InpFs).0 for k being Nat, v being
Vertex of IIG st depth(v,SCS) <= k holds ((Computation(s,InpFs)).k qua Element
of product the Sorts of SCS).v = IGValue(v,iv);
theorem :: CIRCUIT2:17
commute InpFs is constant & InputVertices IIG is non empty & iv
= (commute InpFs).0 implies for s being State of SCS, v being Vertex of IIG, n
being Element of NAT st n = depth SCS holds ((Computation(s,InpFs)).n qua State
of SCS).v = IGValue(v,iv);
theorem :: CIRCUIT2:18
commute InpFs is constant & InputVertices IIG is non empty implies for
s being State of SCS, n be Element of NAT st n = depth SCS holds (Computation(s
,InpFs)).n is stable;
theorem :: CIRCUIT2:19
commute InpFs is constant & InputVertices IIG is non empty implies for
s1, s2 being State of SCS holds (Computation(s1,InpFs)).(depth SCS) = (
Computation(s2,InpFs)).(depth SCS);