:: Introduction to Circuits, I
:: by Yatsuka Nakamura, Piotr Rudnicki, Andrzej Trybulec and Pauline N. Kawamoto
::
:: Received December 15, 1994
:: Copyright (c) 1994-2026 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;
definitions TARSKI, MEMBERED;
equalities TARSKI, MSAFREE2;
expansions MSAFREE2;
theorems TARSKI, ZFMISC_1, NAT_1, FINSEQ_1, FINSEQ_2, FINSEQ_3, FUNCT_1,
FUNCT_2, TREES_1, TREES_2, TREES_3, TREES_4, CARD_1, CARD_2, CARD_3,
FUNCOP_1, PBOOLE, PRALG_2, MSUALG_1, MSUALG_2, RELAT_1, MSAFREE1,
MSAFREE, PRE_CIRC, DTCONSTR, LANG1, MSAFREE2, FUNCT_4, FUNCT_6, XBOOLE_0,
XBOOLE_1, MEMBERED, FINSET_1, XREAL_1, XXREAL_0, ORDINAL1, PARTFUN1,
XXREAL_2, XTUPLE_0;
schemes NAT_1, FINSEQ_1, PRE_CIRC, PBOOLE, FRAENKEL, DOMAIN_1;
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
:
Def1: for
x being Vertex of IIG st x in dom it holds it.x in Constants (SCS, x);
existence
proof
defpred P[object, object] means
ex v being Vertex of IIG st v = $1 & $2 in Constants (SCS, v);
set SW = SortsWithConstants IIG;
A1: now
let i be object;
A2: SW = {v where v is SortSymbol of IIG : v is with_const_op } by
MSAFREE2:def 1;
assume
A3: i in SW;
then reconsider x = i as Vertex of IIG;
consider v being Vertex of IIG such that
A4: v = x and
A5: v is with_const_op by A3,A2;
consider o be OperSymbol of IIG such that
A6: (the Arity of IIG).o = {} and
A7: (the ResultSort of IIG).o = v by A5,MSUALG_2:def 1;
A8: dom the ResultSort of IIG = the carrier' of IIG by FUNCT_2:def 1;
set y = the Element of rng Den(o,SCS);
Result (o, SCS)=((the Sorts of SCS) * the ResultSort of IIG).o by
MSUALG_1:def 5
.= (the Sorts of SCS).((the ResultSort of IIG).o) by A8,FUNCT_1:13;
then reconsider y9 = y as Element of (the Sorts of SCS).v by A7;
reconsider y as object;
take y;
ex A being non empty set st A =(the Sorts of SCS).v & Constants (SCS,
v) = { a where a is Element of A : ex o be OperSymbol of IIG st (the Arity of
IIG).o = {} & (the ResultSort of IIG).o = v & a in rng Den(o,SCS) } by
MSUALG_2:def 3;
then y9 in Constants (SCS, x) by A4,A6,A7;
hence P[i, y];
end;
consider f being ManySortedSet of SW such that
A9: for i being object st i in SW holds P[i,f.i] from PBOOLE:sch 3 (A1);
take f;
let x be Vertex of IIG;
assume x in dom f;
then x in SW;
then P[x, f.x] by A9;
hence thesis;
end;
correctness
proof
let it1, it2 be ManySortedSet of SortsWithConstants IIG;
assume
A10: for x being Vertex of IIG st x in dom it1 holds it1.x in
Constants (SCS, x);
assume
A11: for x being Vertex of IIG st x in dom it2 holds it2.x in
Constants (SCS, x);
now
let i be object;
A12: dom the Arity of IIG = the carrier' of IIG by FUNCT_2:def 1;
assume
A13: i in SortsWithConstants IIG;
then reconsider v = i as Vertex of IIG;
A14: ex A being non empty set st A =(the Sorts of SCS).v & Constants (SCS
, v) = { a where a is Element of A : ex o be OperSymbol of IIG st (the Arity of
IIG).o = {} & (the ResultSort of IIG).o = v & a in rng Den(o,SCS) } by
MSUALG_2:def 3;
dom it2 = SortsWithConstants IIG by PARTFUN1:def 2;
then it2.v in Constants (SCS, v) by A11,A13;
then consider a2 being Element of (the Sorts of SCS).v such that
A15: it2.v = a2 and
A16: ex o being OperSymbol of IIG st (the Arity of IIG).o = {} & (
the ResultSort of IIG).o = v & a2 in rng Den(o,SCS) by A14;
consider o2 being OperSymbol of IIG such that
(the Arity of IIG).o2 = {} and
A17: (the ResultSort of IIG).o2 = v and
A18: a2 in rng Den(o2,SCS) by A16;
A19: the_result_sort_of o2 = v by A17,MSUALG_1:def 2;
dom it1 = SortsWithConstants IIG by PARTFUN1:def 2;
then it1.v in Constants (SCS, v) by A10,A13;
then consider a1 being Element of (the Sorts of SCS).v such that
A20: it1.v = a1 and
A21: ex o being OperSymbol of IIG st (the Arity of IIG).o = {} & (
the ResultSort of IIG).o = v & a1 in rng Den(o,SCS) by A14;
consider o1 be OperSymbol of IIG such that
A22: (the Arity of IIG).o1 = {} and
A23: (the ResultSort of IIG).o1 = v and
A24: a1 in rng Den(o1,SCS) by A21;
A25: {} = <*>the carrier of IIG;
A26: ex x2 being object st x2 in dom Den(o2, SCS) & a2 = Den(o2, SCS).x2
by A18,
FUNCT_1:def 3;
the_result_sort_of o1 = v by A23,MSUALG_1:def 2;
then
A27: o1 = o2 by A19,MSAFREE2:def 6;
consider x1 being object such that
A28: x1 in dom Den(o1, SCS) and
A29: a1 = Den(o1,SCS).x1 by A24,FUNCT_1:def 3;
A30: dom Den (o1, SCS) = Args (o1, SCS) by FUNCT_2:def 1
.= ((the Sorts of SCS)# * the Arity of IIG).o1 by MSUALG_1:def 4
.= (the Sorts of SCS)#.((the Arity of IIG).o1) by A12,FUNCT_1:13
.= {{}} by A22,A25,PRE_CIRC:2;
then x1 = {} by A28,TARSKI:def 1;
hence it1.i = it2.i by A20,A15,A27,A30,A29,A26,TARSKI:def 1;
end;
hence it1 = it2 by PBOOLE:3;
end;
end;
theorem
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
proof
let IIG;
let SCS be non-empty Circuit of IIG, v be Vertex of IIG, e be Element of (
the Sorts of SCS).v;
assume that
A1: v in SortsWithConstants IIG and
A2: e in Constants (SCS, v);
A3: ex A being non empty set st A =(the Sorts of SCS).v & Constants (SCS, v)
= { a where a is Element of A : ex o be OperSymbol of IIG st (the Arity of IIG)
.o = {} & (the ResultSort of IIG).o = v & a in rng Den(o,SCS) } by
MSUALG_2:def 3;
then ex a being Element of (the Sorts of SCS).v st a = e & ex o being
OperSymbol of IIG st (the Arity of IIG).o = {} & (the ResultSort of IIG ).o = v
& a in rng Den(o,SCS) by A2;
then consider o being OperSymbol of IIG such that
A4: (the Arity of IIG).o = {} and
A5: (the ResultSort of IIG).o = v and
A6: e in rng Den(o,SCS);
A7: {} = <*>the carrier of IIG;
v in dom Set-Constants SCS by A1,PARTFUN1:def 2;
then (Set-Constants SCS).v in Constants (SCS, v) by Def1;
then
ex a being Element of (the Sorts of SCS).v st a = ( Set-Constants SCS).v
& ex o being OperSymbol of IIG st (the Arity of IIG).o = {} & (the ResultSort
of IIG).o = v & a in rng Den(o,SCS) by A3;
then consider o1 being OperSymbol of IIG such that
(the Arity of IIG).o1 = {} and
A8: (the ResultSort of IIG).o1 = v and
A9: (Set-Constants SCS).v in rng Den(o1,SCS);
A10: ex d1 being object
st d1 in dom Den(o1, SCS) & ( Set-Constants SCS).v = Den
(o1, SCS).d1 by A9,FUNCT_1:def 3;
the_result_sort_of o = (the ResultSort of IIG).o & the_result_sort_of
o1 = ( the ResultSort of IIG).o1 by MSUALG_1:def 2;
then
A11: o = o1 by A5,A8,MSAFREE2:def 6;
consider d being object such that
A12: d in dom Den(o, SCS) and
A13: e = Den(o, SCS).d by A6,FUNCT_1:def 3;
A14: dom the Arity of IIG = the carrier' of IIG by FUNCT_2:def 1;
A15: dom Den (o, SCS) = Args (o, SCS) by FUNCT_2:def 1
.= ((the Sorts of SCS)# * the Arity of IIG).o by MSUALG_1:def 4
.= (the Sorts of SCS)#.((the Arity of IIG).o) by A14,FUNCT_1:13
.= {{}} by A4,A7,PRE_CIRC:2;
then d = {} by A12,TARSKI:def 1;
hence thesis by A11,A15,A13,A10,TARSKI:def 1;
end;
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 Th2:
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
proof
let IIG;
let SCS be non-empty Circuit of IIG, InpFs be InputFuncs of SCS, n be Nat;
reconsider A = InputVertices IIG as Subset of IIG;
reconsider SS = the Sorts of SCS as non-empty ManySortedSet of the carrier
of IIG;
assume IIG is with_input_V;
then reconsider A as non empty Subset of IIG;
reconsider SI = SS | A as ManySortedSet of A;
reconsider SI as non-empty ManySortedSet of A;
reconsider n as Element of NAT by ORDINAL1:def 12;
consider ivm being ManySortedSet of A such that
A1: ivm = (commute InpFs).n and
A2: ivm in SI by PRE_CIRC:7;
now
let v be Vertex of IIG;
assume
A3: v in InputVertices IIG;
then SI.v = (the Sorts of SCS).v by FUNCT_1:49;
hence ivm.v in (the Sorts of SCS).v by A2,A3,PBOOLE:def 1;
end;
hence thesis by A1,MSAFREE2:def 5;
end;
definition
let IIG such that
A1: 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
(commute InpFs).n;
coherence by A1,Th2;
correctness;
end;
definition
let IIG;
let SCS be Circuit of IIG;
mode State of SCS is Element of product (the Sorts of SCS);
end;
theorem
for IIG for SCS being non-empty Circuit of IIG, s being State of SCS
holds dom s = the carrier of IIG by PARTFUN1:def 2;
theorem
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
proof
let IIG;
let SCS be non-empty Circuit of IIG, s be State of SCS, v be Vertex of IIG;
dom the Sorts of SCS = the carrier of IIG & ex g being Function st s = g
& dom g = dom the Sorts of SCS &
for x being object st x in dom the Sorts of SCS
holds g.x in (the Sorts of SCS).x by CARD_3:def 5,PARTFUN1:def 2;
hence thesis;
end;
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
s * (the_arity_of
o);
coherence
proof
Args(o,SCS) = product ((the Sorts of SCS)*(the_arity_of o)) by PRALG_2:3;
hence thesis by CARD_3:83;
end;
correctness;
end;
reserve IIG for monotonic Circuit-like non void non empty ManySortedSign;
theorem Th5:
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
proof
let IIG;
let SCS be finite-yielding non-empty MSAlgebra over IIG, v, w be Vertex of
IIG, e1 be Element of (the Sorts of FreeEnv SCS).v, q1 be DTree-yielding
FinSequence;
assume that
A1: v in InnerVertices IIG and
A2: e1 = [action_at v,the carrier of IIG]-tree q1;
thus 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
proof
reconsider av = action_at v as OperSymbol of IIG;
let k be Element of NAT;
assume that
A3: k in dom q1 and
A4: q1.k in (the Sorts of FreeEnv SCS).w;
A5: FreeEnv SCS = MSAlgebra (# FreeSort the Sorts of SCS, FreeOper the
Sorts of SCS #) by MSAFREE:def 14;
e1 in (the Sorts of FreeEnv SCS).v;
then
A6: e1 in (the Sorts of FreeEnv SCS) .(the_result_sort_of av) by A1,
MSAFREE2:def 7;
then len q1 = len (the_arity_of av) by A2,MSAFREE2:10;
then
A7: k in dom the_arity_of av by A3,FINSEQ_3:29;
then q1.k in (the Sorts of FreeEnv SCS) .((the_arity_of av).k) by A2,A6,
MSAFREE2:11;
then
A8: q1.k in (FreeSort the Sorts of SCS).((the_arity_of av)/.k) by A7,A5,
PARTFUN1:def 6;
now
assume (the_arity_of av)/.k <> w;
then ((FreeSort the Sorts of SCS).((the_arity_of av)/.k)) misses ((
FreeSort the Sorts of SCS).w) by MSAFREE:12;
then ((FreeSort the Sorts of SCS).((the_arity_of av)/.k)) /\ ((FreeSort
the Sorts of SCS).w) = {} by XBOOLE_0:def 7;
hence contradiction by A4,A5,A8,XBOOLE_0:def 4;
end;
hence thesis;
end;
end;
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;
coherence;
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;
coherence;
end;
theorem Th6:
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
proof
set q99 = <*>NAT;
let IIG;
let SCS be finite-yielding non-empty MSAlgebra over IIG, v, w be Vertex of
IIG, e1 be Element of (the Sorts of FreeEnv SCS).v, e2 be Element of (the Sorts
of FreeEnv SCS).w, q1 be DTree-yielding FinSequence, k1 be Element of NAT;
set k = k1 + 1, eke = e1 with-replacement (<*k1*>,e2);
assume that
A1: v in InnerVertices IIG \ SortsWithConstants IIG and
A2: e1 = [action_at v,the carrier of IIG]-tree q1 and
A3: k in dom q1 and
A4: q1.k in (the Sorts of FreeEnv SCS).w;
reconsider O = [:the carrier' of IIG,{the carrier of IIG}:] \/ Union(coprod
the Sorts of SCS) as non empty set;
reconsider R = REL(the Sorts of SCS) as Relation of O, O*;
A5: DTConMSA(the Sorts of SCS) = DTConstrStr (# O, R #) by MSAFREE:def 8;
then reconsider
TSDT = TS(DTConMSA(the Sorts of SCS)) as Subset of FinTrees(O);
for x being object st x in TSDT holds x is DecoratedTree of O;
then reconsider TSDT as DTree-set of O by TREES_3:def 6;
reconsider av = action_at v as OperSymbol of IIG;
reconsider e19 = e1 as DecoratedTree;
ex p9 being DTree-yielding FinSequence st p9 = q1 & dom e19 = tree(doms
p9) by A2,TREES_4:def 4;
then reconsider m = <*k1*> as Element of dom e1 by A3,PRE_CIRC:13;
reconsider m9 = m as FinSequence of NAT;
consider qq being DTree-yielding FinSequence such that
A6: e1 with-replacement (m9,e2) = [av,the carrier of IIG]-tree qq and
A7: len qq = len q1 and
A8: qq.(k1+1) = e2 and
A9: for i being Nat st i in dom q1 holds (i <> (k1+1)
implies qq.i = q1.i) by A2,PRE_CIRC:15;
NonTerminals(DTConMSA(the Sorts of SCS)) = [:the carrier' of IIG,{the
carrier of IIG}:] & the carrier of IIG in {the carrier of IIG} by MSAFREE:6
,TARSKI:def 1;
then reconsider
nt = [av,the carrier of IIG] as NonTerminal of DTConMSA(the Sorts
of SCS) by ZFMISC_1:87;
A10: FreeEnv SCS = MSAlgebra (# FreeSort the Sorts of SCS, FreeOper the Sorts
of SCS #) by MSAFREE:def 14;
then
A11: (the Sorts of FreeEnv SCS).v = FreeSort(the Sorts of SCS, v) by
MSAFREE:def 11;
then
A12: e1 in TS(DTConMSA(the Sorts of SCS)) by TARSKI:def 3;
e1.{} = nt by A2,TREES_4:def 4;
then ex p9 being FinSequence of TS(DTConMSA(the Sorts of SCS)) st e1 = nt
-tree p9 & nt ==> roots p9 by A12,DTCONSTR:10;
then reconsider
q19 = q1 as FinSequence of TS(DTConMSA(the Sorts of SCS)) by A2,TREES_4:15;
(the Sorts of FreeEnv SCS).w = FreeSort(the Sorts of SCS, w) by A10,
MSAFREE:def 11;
then
A13: e2 in FreeSort(the Sorts of SCS, w);
then e2 in {a9 where a9 is Element of TS(DTConMSA(the Sorts of SCS)): (ex x
being set st x in (the Sorts of SCS).w & a9 = root-tree[x,w]) or ex o being
OperSymbol of IIG st [o,the carrier of IIG] = a9.{} & the_result_sort_of o = w}
by MSAFREE:def 10;
then consider aa being Element of TS(DTConMSA(the Sorts of SCS)) such that
A14: aa = e2 and
A15: (ex x being set st x in (the Sorts of SCS).w & aa = root-tree[x,w])
or ex o being OperSymbol of IIG st [o,the carrier of IIG] = aa.{} &
the_result_sort_of o = w;
A16: dom qq = dom q1 by A7,FINSEQ_3:29;
rng qq c= TS(DTConMSA(the Sorts of SCS))
proof
let y be object;
assume y in rng qq;
then consider x being object such that
A17: x in dom qq and
A18: y = qq.x by FUNCT_1:def 3;
reconsider x as Element of NAT by A17;
per cases;
suppose
x = k1+1;
hence thesis by A8,A14,A18;
end;
suppose
x <> k1+1;
then qq.x = q19.x by A9,A16,A17;
hence thesis by A16,A17,A18,FINSEQ_2:11;
end;
end;
then reconsider q9 = qq as FinSequence of TSDT by FINSEQ_1:def 4;
reconsider rq = roots q9 as FinSequence of O;
reconsider rq as Element of O* by FINSEQ_1:def 11;
A19: dom rq = dom qq by TREES_3:def 18;
A20: v in InnerVertices IIG by A1,XBOOLE_0:def 5;
then
A21: (the Sorts of FreeEnv SCS).(the_result_sort_of av) = (the Sorts of
FreeEnv SCS).v by MSAFREE2:def 7;
then
A22: len q1 = len (the_arity_of av) by A2,MSAFREE2:10;
then
A23: dom rq = dom (the_arity_of av) by A7,A19,FINSEQ_3:29;
A24: for x being set st x in dom rq holds (rq.x in [:the carrier' of IIG,{
the carrier of IIG}:] implies for o1 being OperSymbol of IIG st [o1,the carrier
of IIG] = rq.x holds the_result_sort_of o1 = (the_arity_of av).x) & (rq.x in
Union(coprod the Sorts of SCS) implies rq.x in coprod((the_arity_of av).x, the
Sorts of SCS))
proof
the carrier of IIG in {the carrier of IIG} by TARSKI:def 1;
then
[av,the carrier of IIG] in [:the carrier' of IIG,{the carrier of IIG}
:] by ZFMISC_1:87;
then reconsider
av9 = [av,the carrier of IIG] as Symbol of DTConMSA(the Sorts
of SCS) by A5,XBOOLE_0:def 3;
reconsider q19 as FinSequence of TSDT;
let x be set;
reconsider b = roots q19 as Element of ([:the carrier' of IIG,{the carrier
of IIG}:] \/ Union(coprod the Sorts of SCS))* by FINSEQ_1:def 11;
reconsider b as FinSequence;
assume
A25: x in dom rq;
then reconsider x9 = x as Element of NAT;
A26: (the_arity_of av)/.x9 = (the_arity_of av).x9 by A23,A25,PARTFUN1:def 6;
A27: dom q1 = dom the_arity_of av by A22,FINSEQ_3:29;
for n being Nat st n in dom q1 holds q1.n in FreeSort(the Sorts of
SCS, (the_arity_of av)/.n)
proof
let n be Nat;
assume n in dom q1;
then q1.n in (the Sorts of FreeEnv SCS) .((the_arity_of av).n) & (
the_arity_of av ).n = (the_arity_of av)/.n by A2,A21,A27,MSAFREE2:11
,PARTFUN1:def 6;
hence thesis by A10,MSAFREE:def 11;
end;
then
A28: q19 in ((FreeSort the Sorts of SCS)# * (the Arity of IIG)). av by A27,
MSAFREE:9;
Sym(av, the Sorts of SCS) = [av,the carrier of IIG] by MSAFREE:def 9;
then av9 ==> b by A28,MSAFREE:10;
then
A29: dom roots q1 = dom q1 & [av9,b] in R by A5,LANG1:def 1,TREES_3:def 18;
A30: (the_arity_of av)/.k = w by A2,A3,A4,A20,Th5;
A31: ex T being DecoratedTree st T = qq.x9 & rq.x9 = T.{} by A19,A25,
TREES_3:def 18;
A32: ex T9 being DecoratedTree st T9 = q1.x9 & (roots q1).x9 = T9.{} by A16,A19
,A25,TREES_3:def 18;
thus rq.x in [:the carrier' of IIG,{the carrier of IIG}:] implies for o1
being OperSymbol of IIG st [o1,the carrier of IIG] = rq.x holds
the_result_sort_of o1 = (the_arity_of av).x
proof
assume
A33: rq.x in [:the carrier' of IIG,{the carrier of IIG}:];
let o1 be OperSymbol of IIG;
assume
A34: [o1,the carrier of IIG] = rq.x;
per cases;
suppose
A35: x9 = k1+1;
now
per cases by A15;
case
ex xx being set st xx in (the Sorts of SCS).w & aa =
root-tree[xx,w];
then consider xx being set such that
xx in (the Sorts of SCS).w and
A36: aa = root-tree[xx,w];
[o1,the carrier of IIG] = [xx,w] by A8,A14,A31,A34,A35,A36,
TREES_4:3;
then
A37: the carrier of IIG = w by XTUPLE_0:1;
for X be set holds not X in X;
hence contradiction by A37;
end;
case
ex o being OperSymbol of IIG st [o,the carrier of IIG] =
aa.{} & the_result_sort_of o = w;
hence thesis by A8,A14,A26,A31,A30,A34,A35,XTUPLE_0:1;
end;
end;
hence thesis;
end;
suppose
x9 <> k1+1;
then (roots q1).x9 = [o1,the carrier of IIG] by A9,A16,A19,A25,A31,A32
,A34;
hence thesis by A16,A19,A25,A29,A33,A34,MSAFREE1:3;
end;
end;
thus rq.x in Union(coprod the Sorts of SCS) implies rq.x in coprod((
the_arity_of av).x, the Sorts of SCS)
proof
assume
A38: rq.x in Union(coprod the Sorts of SCS);
then rq.x in Terminals DTConMSA(the Sorts of SCS) by MSAFREE:6;
then consider s1 being SortSymbol of IIG, x99 being set such that
A39: x99 in (the Sorts of SCS).s1 & rq.x = [x99,s1] by MSAFREE:7;
per cases;
suppose
A40: x9 = k1+1;
reconsider rqx = rq.x9 as Terminal of DTConMSA the Sorts of SCS by A38,
MSAFREE:6;
aa = root-tree rqx by A8,A14,A31,A40,DTCONSTR:9;
then
aa in {a99 where a99 is Element of TS(DTConMSA(the Sorts of SCS))
: (ex x999 being set st x999 in (the Sorts of SCS).s1 & a99 = root-tree[x999,s1
]) or ex o being OperSymbol of IIG st [o,the carrier of IIG] = a99.{} &
the_result_sort_of o = s1} by A39;
then
A41: aa in FreeSort(the Sorts of SCS, s1) by MSAFREE:def 10;
A42: e2 in (FreeSort the Sorts of SCS).w by A13,MSAFREE:def 11;
now
assume w <> s1;
then
(FreeSort the Sorts of SCS).w misses (FreeSort the Sorts of SCS
).s1 by MSAFREE:12;
then
A43: (FreeSort the Sorts of SCS).w /\ (FreeSort the Sorts of SCS).s1
= {} by XBOOLE_0:def 7;
e2 in (FreeSort the Sorts of SCS).s1 by A14,A41,MSAFREE:def 11;
hence contradiction by A42,A43,XBOOLE_0:def 4;
end;
hence thesis by A26,A30,A39,A40,MSAFREE:def 2;
end;
suppose
x9 <> k1+1;
then rq.x9 = (roots q1).x9 by A9,A16,A19,A25,A31,A32;
hence thesis by A16,A19,A25,A29,A38,MSAFREE1:3;
end;
end;
end;
len rq = len qq by A19,FINSEQ_3:29;
then [nt,roots qq] in REL(the Sorts of SCS) by A7,A22,A24,MSAFREE:5;
then nt ==> roots qq by A5,LANG1:def 1;
then reconsider q9 as SubtreeSeq of nt by DTCONSTR:def 6;
eke = nt-tree q9 by A6;
then reconsider eke9 = eke as Element of TS(DTConMSA(the Sorts of SCS));
q99 in dom e1 with-replacement (m9,dom e2) by TREES_1:22;
then not m9 is_a_prefix_of q99 & eke.q99 = e1.q99 or ex r being FinSequence
of NAT st r in dom e2 & q99 = m9^r & eke.q99 = e2.r by TREES_2:def 11;
then
A44: eke.{} = [av,the carrier of IIG] by A2,TREES_4:def 4;
now
take av;
the_result_sort_of av = v by A20,MSAFREE2:def 7;
hence ex o being OperSymbol of IIG st [o,the carrier of IIG] = eke.{} &
the_result_sort_of o = v by A44;
end;
then eke9 in {a99 where a99 is Element of TS(DTConMSA(the Sorts of SCS)): (
ex x being set st x in (the Sorts of SCS).v & a99 = root-tree[x,v]) or ex o
being OperSymbol of IIG st [o,the carrier of IIG] = a99.{} & the_result_sort_of
o = v};
then reconsider eke9 as Element of (the Sorts of FreeEnv SCS).v by A11,
MSAFREE:def 10;
eke9 in (the Sorts of FreeEnv SCS).v;
hence thesis;
end;
theorem Th7:
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]
proof
let IIG;
let A be finite-yielding non-empty MSAlgebra over IIG, v be Element of IIG,
e be Element of (the Sorts of FreeEnv A).v;
set X = the Sorts of A;
assume
A1: 1 < card e;
A2: (FreeSort X).v = FreeSort(X, v) & FreeSort (X, v) = {a where a is
Element of TS(DTConMSA(X)): (ex x being set st x in X.v & a = root-tree[x,v])
or ex o being OperSymbol of IIG st [o,the carrier of IIG] = a.{} &
the_result_sort_of o = v} by MSAFREE:def 10,def 11;
e in (the Sorts of FreeMSA X).v & FreeMSA X = MSAlgebra (# FreeSort(X),
FreeOper(X) #) by MSAFREE:def 14;
then
ex a being Element of TS(DTConMSA(X)) st a = e &( (ex x being set st x in
X.v & a = root-tree[x,v]) or ex o being OperSymbol of IIG st [o,the carrier of
IIG] = a.{} & the_result_sort_of o = v) by A2;
hence thesis by A1,PRE_CIRC:19;
end;
theorem
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)
proof
let IIG be non void Circuit-like non empty ManySortedSign;
let SCS be non-empty Circuit of IIG, s be State of SCS, o be OperSymbol of
IIG;
A1: dom the ResultSort of IIG = the carrier' of IIG by FUNCT_2:def 1;
Result(o,SCS) = ((the Sorts of SCS) * the ResultSort of IIG).o by
MSUALG_1:def 5
.= (the Sorts of SCS).((the ResultSort of IIG).o) by A1,FUNCT_1:13
.= (the Sorts of SCS).(the_result_sort_of o) by MSUALG_1:def 2;
hence thesis by FUNCT_2:5;
end;
theorem Th9:
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
proof
let IIG;
let A be non-empty Circuit of IIG, v be Vertex of IIG, e be Element of (the
Sorts of FreeEnv A).v such that
A1: e.{} = [action_at v,the carrier of IIG];
set X = the Sorts of A;
NonTerminals(DTConMSA(X)) = [:the carrier' of IIG,{the carrier of IIG}:]
& the carrier of IIG in {the carrier of IIG} by MSAFREE:6,TARSKI:def 1;
then reconsider
nt = [action_at v,the carrier of IIG] as NonTerminal of DTConMSA(
X) by ZFMISC_1:87;
FreeMSA(X) = MSAlgebra (# FreeSort(X), FreeOper(X) #) & e in (the Sorts
of FreeEnv A).v by MSAFREE:def 14;
then e in FreeSort(X,v) by MSAFREE:def 11;
then reconsider tsg = e as Element of TS DTConMSA(X);
consider ts being FinSequence of TS DTConMSA(X) such that
A2: tsg = nt-tree ts and
nt ==> roots ts by A1,DTCONSTR:10;
take ts;
thus thesis by A2;
end;
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;
coherence
proof
the Sorts of A is finite-yielding by MSAFREE2:def 11;
then FreeEnv A is finitely-generated by MSAFREE2:8;
then FreeEnv A is finite-yielding by MSAFREE2:def 13;
then the Sorts of FreeEnv A is finite-yielding;
hence thesis;
end;
end;
defpred P[set] means not contradiction;
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
:Def4:
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;
existence
proof
deffunc F(Element of (the Sorts of FreeEnv A).v) = card $1;
set s = { F(t) where t is Element of (the Sorts of FreeEnv A).v : P[t] };
set t = the Element of (the Sorts of FreeEnv A).v;
A1: card t in s;
A2: s is Subset of NAT from DOMAIN_1:sch 8;
s is finite from PRE_CIRC:sch 1;
then reconsider s as finite non empty Subset of NAT by A1,A2;
reconsider m = max s as Nat by TARSKI:1;
take m,s;
thus thesis;
end;
correctness;
end;
theorem Th10:
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
proof
let IIG;
let A be finite-yielding non-empty MSAlgebra over IIG, v be Element of IIG;
consider s being finite non empty Subset of NAT such that
A1: s = the set of all
card t where t is Element of (the Sorts of FreeEnv A).v and
A2: size(v,A) = max s by Def4;
reconsider Y = s as finite non empty real-membered set;
max Y in the set of all
card t where t is Element of (the Sorts of FreeEnv A).v by A1,XXREAL_2:def 8;
then consider e being Element of (the Sorts of FreeEnv A).v such that
A3: card e = max Y;
A4: FreeEnv A = MSAlgebra (# FreeSort the Sorts of A, FreeOper the Sorts of
A #) by MSAFREE:def 14;
then
e in (the Sorts of FreeEnv A).v & (the Sorts of FreeEnv A).v = FreeSort(
the Sorts of A, v) by MSAFREE:def 11;
then
A5: e in {a where a is Element of TS(DTConMSA(the Sorts of A)): (ex x being
set st x in (the Sorts of A).v & a = root-tree[x,v]) or ex o being OperSymbol
of IIG st [o,the carrier of IIG] = a.{} & the_result_sort_of o = v} by
MSAFREE:def 10;
thus size(v,A) = 1 implies v in InputVertices IIG \/ SortsWithConstants IIG
proof
assume
A6: size(v,A) = 1;
now
assume
A7: not v in InputVertices IIG \/ SortsWithConstants IIG;
then not v in SortsWithConstants IIG by XBOOLE_0:def 3;
then
not v in { v9 where v9 is SortSymbol of IIG : v9 is with_const_op }
by MSAFREE2:def 1;
then
A8: not v is with_const_op;
A9: the carrier of IIG = InputVertices IIG \/ InnerVertices IIG by
XBOOLE_1:45;
not v in InputVertices IIG by A7,XBOOLE_0:def 3;
then v in InnerVertices IIG by A9,XBOOLE_0:def 3;
then consider x being object such that
A10: x in dom the ResultSort of IIG and
A11: v = (the ResultSort of IIG).x by FUNCT_1:def 3;
reconsider o = x as OperSymbol of IIG by A10;
per cases by A8,MSUALG_2:def 1;
suppose
not (the Arity of IIG).o = {};
then
A12: the_arity_of o <> {} by MSUALG_1:def 1;
reconsider O = [:the carrier' of IIG,{the carrier of IIG}:] \/ Union(
coprod(the Sorts of A)) as non empty set;
reconsider R = REL(the Sorts of A) as Relation of O, O*;
the carrier of IIG in {the carrier of IIG} by TARSKI:def 1;
then
A13: [o,the carrier of IIG] in [:the carrier' of IIG,{the carrier of
IIG}:] by ZFMISC_1:87;
DTConMSA(the Sorts of A) = DTConstrStr (# O, R #) by MSAFREE:def 8;
then reconsider
o9 = [o,the carrier of IIG] as Symbol of DTConMSA(the Sorts
of A) by A13,XBOOLE_0:def 3;
o9 in NonTerminals DTConMSA(the Sorts of A) by A13,MSAFREE:6;
then consider
p being FinSequence of TS(DTConMSA(the Sorts of A)) such that
A14: o9 ==> roots p by DTCONSTR:def 5;
reconsider op = o9-tree p as Element of TS(DTConMSA(the Sorts of A))
by A14,DTCONSTR:def 1;
reconsider e1 = op as finite DecoratedTree;
reconsider co = card e1 as Real;
A15: op.{} = o9 by TREES_4:def 4;
now
take o;
the_result_sort_of o = v by A11,MSUALG_1:def 2;
hence ex o being OperSymbol of IIG st [o,the carrier of IIG] = op.{}
& the_result_sort_of o = v by A15;
end;
then
op in {a9 where a9 is Element of TS(DTConMSA(the Sorts of A)) : (
ex x9 being set st x9 in (the Sorts of A).v & a9 = root-tree[x9,v]) or ex o
being OperSymbol of IIG st [o,the carrier of IIG] = a9.{} & the_result_sort_of
o = v};
then
A16: op in FreeSort(the Sorts of A, v) by MSAFREE:def 10;
A17: (the Sorts of FreeEnv A).(the_result_sort_of o) = (FreeSort(the
Sorts of A)).v by A4,A11,MSUALG_1:def 2
.= FreeSort(the Sorts of A, v) by MSAFREE:def 11;
then reconsider
e1 as Element of (the Sorts of FreeEnv A).v by A11,A16,MSUALG_1:def 2;
len p = len the_arity_of o by A16,A17,MSAFREE2:10;
then p <> {} by A12;
then rng p <> {};
then
A18: 1 in dom p by FINSEQ_3:32;
(ex q being DTree-yielding FinSequence st p = q & dom op = tree(
doms q) )& 0 + 1 = 1 by TREES_4:def 4;
then
A19: <*0*> in dom op by A18,PRE_CIRC:13;
then consider
i being Nat, T being DecoratedTree, q being Node
of T such that
A20: i < len p & T = p.(i+1) & <*0*> = <*i*>^q by TREES_4:11;
op.<*0*> = T.q by A20,TREES_4:12;
then
A21: [<*0*>,T.q] in op by A19,FUNCT_1:1;
{} in dom op by TREES_1:22;
then [{},o9] in op by A15,FUNCT_1:1;
then
A22: { [{},o9], [<*0*>,T.q] } c= op by A21,ZFMISC_1:32;
e1 in (the Sorts of FreeEnv A).v;
then
A23: co in Y by A1;
[{},o9] <> [<*0*>,T.q] by XTUPLE_0:1;
then card { [{},o9], [<*0*>,T.q] } = 2 by CARD_2:57;
then 2 <= co by A22,NAT_1:43;
then co > size(v,A) by A6,XXREAL_0:2;
hence contradiction by A2,A23,XXREAL_2:def 8;
end;
suppose
not (the ResultSort of IIG).o = v;
hence contradiction by A11;
end;
end;
hence thesis;
end;
consider a being Element of TS(DTConMSA(the Sorts of A)) such that
A24: a = e and
A25: (ex x being set st x in (the Sorts of A).v & a = root-tree[x,v]) or
ex o being OperSymbol of IIG st [o,the carrier of IIG] = a.{} &
the_result_sort_of o = v by A5;
assume
A26: v in InputVertices IIG \/ SortsWithConstants IIG;
per cases by A26,XBOOLE_0:def 3;
suppose
v in InputVertices IIG;
then consider x being set such that
x in (the Sorts of A).v and
A27: a = root-tree[x,v] by A25,MSAFREE2:2;
root-tree[x,v] = {{}} --> [x,v] by TREES_1:29,TREES_4:def 2
.= [: {{}}, {[x,v]} :] by FUNCOP_1:def 2
.= { [{},[x,v]] } by ZFMISC_1:29;
hence thesis by A2,A3,A24,A27,CARD_1:30;
end;
suppose
v in SortsWithConstants IIG;
then v in { v9 where v9 is SortSymbol of IIG : v9 is with_const_op } by
MSAFREE2:def 1;
then consider v9 being SortSymbol of IIG such that
A28: v9 = v and
A29: v9 is with_const_op;
consider o being OperSymbol of IIG such that
A30: (the Arity of IIG).o = {} and
A31: (the ResultSort of IIG).o = v9 by A29,MSUALG_2:def 1;
now
per cases by A25;
suppose
ex x being set st x in (the Sorts of A).v & a = root-tree[x,v ];
then consider x being set such that
x in (the Sorts of A).v and
A32: a = root-tree[x,v];
root-tree[x,v] = { [{},[x,v]] } by TREES_4:6;
hence thesis by A2,A3,A24,A32,CARD_1:30;
end;
suppose
ex o9 being OperSymbol of IIG st [o9,the carrier of IIG] = a.
{} & the_result_sort_of o9 = v;
then consider o9 being OperSymbol of IIG such that
A33: [o9,the carrier of IIG] = a.{} and
A34: the_result_sort_of o9 = v;
the_result_sort_of o9 = the_result_sort_of o by A28,A31,A34,
MSUALG_1:def 2;
then
A35: o9 = o by MSAFREE2:def 6;
NonTerminals(DTConMSA(the Sorts of A)) = [:the carrier' of IIG,{
the carrier of IIG}:] & the carrier of IIG in {the carrier of IIG} by MSAFREE:6
,TARSKI:def 1;
then reconsider
nt = [o9,the carrier of IIG] as NonTerminal of DTConMSA(the
Sorts of A) by ZFMISC_1:87;
consider ts being FinSequence of TS(DTConMSA(the Sorts of A)) such
that
A36: a = nt-tree ts and
nt ==> roots ts by A33,DTCONSTR:10;
reconsider ts as DTree-yielding FinSequence;
len ts = len the_arity_of o9 by A24,A34,A36,MSAFREE2:10
.= len {} by A30,A35,MSUALG_1:def 1
.= 0;
then ts = {};
then a = root-tree nt by A36,TREES_4:20
.= { [{},nt] } by TREES_4:6;
hence thesis by A2,A3,A24,CARD_1:30;
end;
end;
hence thesis;
end;
end;
theorem
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)
proof
let IIG;
let SCS be finite-yielding non-empty MSAlgebra over IIG, v, w be Vertex of
IIG, e1 be Element of (the Sorts of FreeEnv SCS).v, e2 be Element of (the Sorts
of FreeEnv SCS).w, q1 be DTree-yielding FinSequence;
assume that
A1: v in InnerVertices IIG \ SortsWithConstants IIG and
A2: card e1 = size(v,SCS) and
A3: e1 = [action_at v,the carrier of IIG]-tree q1 and
A4: e2 in rng q1;
consider sw being finite non empty Subset of NAT such that
A5: sw = the set of all
card t where t is Element of (the Sorts of FreeEnv SCS).w and
A6: size(w,SCS) = max sw by Def4;
reconsider Y = sw as finite non empty real-membered set;
reconsider m = max Y as Real;
m in the set of all
card t where t is Element of (the Sorts of FreeEnv SCS).w
by A5,XXREAL_2:def 8;
then consider e3 being Element of (the Sorts of FreeEnv SCS).w such that
A7: card e3 = m;
card e2 in Y by A5;
then
A8: card e2 <= max Y by XXREAL_2:def 8;
reconsider e39 = e3 as DecoratedTree;
reconsider e19 = e1 as DecoratedTree;
reconsider q19 = q1 as Function;
consider k being object such that
A9: k in dom q19 and
A10: e2 = q19.k by A4,FUNCT_1:def 3;
k in dom q1 by A9;
then reconsider kN = k as Element of NAT;
reconsider k1 = kN - 1 as Element of NAT by A9,FINSEQ_3:26;
A11: k1 + 1 = kN;
ex p being DTree-yielding FinSequence st p = q1 & dom e19 = tree(doms p)
by A3,TREES_4:def 4;
then reconsider k9 = <*k1*> as Element of dom e1 by A9,A11,PRE_CIRC:13;
A12: kN <= len q1 by A9,FINSEQ_3:25;
k1 < kN by A11,XREAL_1:29;
then k1 < len q1 by A12,XXREAL_0:2;
then
A13: e1|k9 = e2 by A3,A10,A11,TREES_4:def 4;
assume card e2 <> size(w,SCS);
then card e2 < max Y by A6,A8,XXREAL_0:1;
then card(e1 with-replacement (k9,e3)) + card (e1|k9) = card e1 + card e3 &
card e1 + card (e1|k9) < card e1 + card e3 by A7,A13,PRE_CIRC:18,XREAL_1:6;
then
A14: card e1 < card (e1 with-replacement (k9,e3)) by XREAL_1:6;
reconsider k99 = k9 as FinSequence of NAT;
reconsider eke = e19 with-replacement (k99, e39) as DecoratedTree;
reconsider eke as Element of (the Sorts of FreeEnv SCS).v by A1,A3,A9,A10,A11
,Th6;
consider sv being finite non empty Subset of NAT such that
A15: sv = the set of all
card t where t is Element of (the Sorts of FreeEnv SCS).v and
A16: size(v,SCS) = max sv by Def4;
reconsider Z = sv as finite non empty real-membered set;
card eke in Z by A15;
hence contradiction by A2,A16,A14,XXREAL_2:def 8;
end;
theorem Th12:
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
proof
let IIG;
let A be finite-yielding non-empty MSAlgebra over IIG, v be Vertex of IIG, e
be Element of (the Sorts of FreeEnv A).v;
assume that
A1: v in (InnerVertices IIG \ SortsWithConstants IIG) and
A2: card e = size(v,A);
A3: not v in SortsWithConstants IIG by A1,XBOOLE_0:def 5;
InputVertices IIG misses InnerVertices IIG by XBOOLE_1:79;
then
A4: InputVertices IIG /\ InnerVertices IIG = {} by XBOOLE_0:def 7;
v in InnerVertices IIG by A1,XBOOLE_0:def 5;
then not v in InputVertices IIG by A4,XBOOLE_0:def 4;
then not v in InputVertices IIG \/ SortsWithConstants IIG by A3,
XBOOLE_0:def 3;
then
A5: card e <> 1 by A2,Th10;
reconsider e9 = e as finite non empty set;
FreeEnv A = MSAlgebra (# FreeSort the Sorts of A, FreeOper the Sorts of
A #) by MSAFREE:def 14;
then (the Sorts of FreeEnv A).v = FreeSort(the Sorts of A, v) by
MSAFREE:def 11;
then e in FreeSort(the Sorts of A, v);
then
A6: e in {a where a is Element of TS(DTConMSA(the Sorts of A)): (ex x being
set st x in (the Sorts of A).v & a = root-tree[x,v]) or ex o being OperSymbol
of IIG st [o,the carrier of IIG] = a.{} & the_result_sort_of o = v} by
MSAFREE:def 10;
1 <= card e9 by NAT_1:14;
then 1 < card e9 by A5,XXREAL_0:1;
then consider o being OperSymbol of IIG such that
A7: e.{} = [o,the carrier of IIG] by Th7;
NonTerminals(DTConMSA(the Sorts of A)) = [:the carrier' of IIG,{the
carrier of IIG}:] & the carrier of IIG in {the carrier of IIG} by MSAFREE:6
,TARSKI:def 1;
then reconsider
nt = [o,the carrier of IIG] as NonTerminal of DTConMSA(the Sorts
of A) by ZFMISC_1:87;
consider a being Element of TS(DTConMSA(the Sorts of A)) such that
A8: a = e and
A9: (ex x being set st x in (the Sorts of A).v & a = root-tree[x,v]) or
ex o being OperSymbol of IIG st [o,the carrier of IIG] = a.{} &
the_result_sort_of o = v by A6;
consider x being set such that
A10: x in (the Sorts of A).v & a = root-tree[x,v] or ex o9 being
OperSymbol of IIG st [o9,the carrier of IIG] = a.{} & the_result_sort_of o9 = v
by A9;
consider ts being FinSequence of TS(DTConMSA(the Sorts of A)) such that
A11: a = nt-tree ts and
nt ==> roots ts by A8,A7,DTCONSTR:10;
reconsider q = ts as DTree-yielding FinSequence;
take q;
A12: v in InnerVertices IIG by A1,XBOOLE_0:def 5;
now
assume a = root-tree[x,v];
then [o,the carrier of IIG] = [x,v] by A8,A7,TREES_4:3;
then
A13: the carrier of IIG = v by XTUPLE_0:1;
for X be set holds not X in X;
hence contradiction by A13;
end;
then consider o9 being OperSymbol of IIG such that
A14: [o9,the carrier of IIG] = a.{} and
A15: the_result_sort_of o9 = v by A10;
o = o9 by A8,A7,A14,XTUPLE_0:1
.= action_at v by A15,A12,MSAFREE2:def 7;
hence thesis by A8,A11;
end;
theorem
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]
proof
let IIG;
let A be finite-yielding non-empty MSAlgebra over IIG, v be Vertex of IIG, e
be Element of (the Sorts of FreeEnv A).v;
assume
v in (InnerVertices IIG \ SortsWithConstants IIG) & card e = size(v, A);
then
A1: ex q being DTree-yielding FinSequence st e = [action_at v,the carrier of
IIG]-tree q by Th12;
take action_at v;
thus thesis by A1,TREES_4:def 4;
end;
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
:Def5:
ex e9 being Element of (the
Sorts of FreeMSA the Sorts of A).v st e = e9 & it = depth e9;
existence
proof
reconsider e9 = e as Element of (the Sorts of FreeMSA the Sorts of A).v;
reconsider d = depth e9 as Element of NAT by ORDINAL1:def 12;
take d,e9;
thus thesis;
end;
correctness;
end;
theorem Th14:
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)
proof
let IIG;
let A be finite-yielding non-empty MSAlgebra over IIG, v, w be Element of
IIG;
assume that
A1: v in InnerVertices IIG and
A2: w in rng the_arity_of action_at v;
reconsider av = action_at v as OperSymbol of IIG;
consider x being object such that
A3: x in dom (the_arity_of av) and
A4: w = (the_arity_of av).x by A2,FUNCT_1:def 3;
reconsider k = x as Element of NAT by A3;
reconsider k1 = k - 1 as Element of NAT by A3,FINSEQ_3:26;
A5: k1 + 1 = k;
reconsider o = <*k1*> as FinSequence of NAT;
consider sv being finite non empty Subset of NAT such that
A6: sv = the set of all
card tv where tv is Element of (the Sorts of FreeEnv A).v and
A7: size(v,A) = max sv by Def4;
reconsider Yv = sv as finite non empty real-membered set;
max Yv in Yv by XXREAL_2:def 8;
then consider tv being Element of (the Sorts of FreeEnv A).v such that
A8: card tv = max Yv by A6;
now
assume v in SortsWithConstants IIG;
then v in { v9 where v9 is SortSymbol of IIG : v9 is with_const_op } by
MSAFREE2:def 1;
then consider v9 being SortSymbol of IIG such that
A9: v9 = v and
A10: v9 is with_const_op;
consider oo being OperSymbol of IIG such that
A11: (the Arity of IIG).oo = {} and
A12: (the ResultSort of IIG).oo = v9 by A10,MSUALG_2:def 1;
the_result_sort_of oo = v by A9,A12,MSUALG_1:def 2
.= the_result_sort_of av by A1,MSAFREE2:def 7;
then
A13: av = oo by MSAFREE2:def 6;
reconsider aoo = (the Arity of IIG).oo as FinSequence;
dom aoo = {} by A11;
hence contradiction by A3,A13,MSUALG_1:def 1;
end;
then
A14: v in (InnerVertices IIG \ SortsWithConstants IIG) by A1,XBOOLE_0:def 5;
then consider p being DTree-yielding FinSequence such that
A15: tv = [av,the carrier of IIG]-tree p by A7,A8,Th12;
A16: (the Sorts of FreeEnv A).v = (the Sorts of FreeEnv A).(
the_result_sort_of av) by A1,MSAFREE2:def 7;
then len p = len the_arity_of av by A15,MSAFREE2:10;
then
A17: k in dom p by A3,FINSEQ_3:29;
reconsider e1 = tv as finite DecoratedTree;
reconsider de1 = dom e1 as finite Tree;
consider sw being finite non empty Subset of NAT such that
A18: sw = the set of all
card tw where tw is Element of (the Sorts of FreeEnv A).w and
A19: size(w,A) = max sw by Def4;
reconsider Yw = sw as finite non empty real-membered set;
max Yw in Yw by XXREAL_2:def 8;
then consider tw being Element of (the Sorts of FreeEnv A).w such that
A20: card tw = max Yw by A18;
reconsider e2 = tw as finite DecoratedTree;
reconsider de2 = dom e2 as finite Tree;
ex p9 being DTree-yielding FinSequence st p9 = p & dom e1 = tree(doms p9
) by A15,TREES_4:def 4;
then reconsider o as Element of dom e1 by A17,A5,PRE_CIRC:13;
reconsider eoe = e1 with-replacement (o,e2) as finite Function;
reconsider o as Element of de1;
reconsider deoe = dom eoe as finite Tree;
A21: card (de1|o) < card de1 by PRE_CIRC:16;
dom eoe = de1 with-replacement (o,de2) by TREES_2:def 11;
then card deoe + card (de1|o) = card de1 + card de2 by PRE_CIRC:17;
then card (de1|o) + card de2 < card deoe + card (de1|o) by A21,XREAL_1:6;
then card de2 < card deoe by XREAL_1:6;
then
A22: card e2 < card deoe by CARD_1:62;
p.k in (the Sorts of FreeEnv A).((the_arity_of av).k) by A3,A15,A16,
MSAFREE2:11;
then reconsider
eoe as Element of (the Sorts of FreeEnv A).v by A4,A14,A15,A17,A5,Th6;
card eoe in Yv by A6;
then card eoe <= size(v,A) by A7,XXREAL_2:def 8;
then card deoe <= size(v,A) by CARD_1:62;
hence thesis by A19,A20,A22,XXREAL_0:2;
end;
theorem Th15:
for IIG for A being finite-yielding non-empty MSAlgebra over IIG
, v being SortSymbol of IIG holds size(v,A) > 0
proof
let IIG;
let A be finite-yielding non-empty MSAlgebra over IIG, v be SortSymbol of
IIG;
consider s being finite non empty Subset of NAT such that
A1: s = the set of all
card t where t is Element of (the Sorts of FreeEnv A).v and
A2: size(v,A) = max s by Def4;
reconsider Y = s as finite non empty real-membered set;
max Y in the set of all
card t where t is Element of (the Sorts of FreeEnv A).v by A1,XXREAL_2:def 8;
then ex t being Element of (the Sorts of FreeEnv A).v st card t = max Y;
hence thesis by A2;
end;
theorem
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)
proof
let IIG;
let A be non-empty Circuit of IIG, v be Vertex of IIG, e be Element of (the
Sorts of FreeEnv A).v, p be DTree-yielding FinSequence such that
A1: v in InnerVertices IIG and
A2: e = [action_at v,the carrier of IIG]-tree p and
A3: 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);
consider s being finite non empty Subset of NAT such that
A4: s = the set of all
card t where t is Element of (the Sorts of FreeEnv A).v and
A5: size(v,A) = max s by Def4;
reconsider S = s as finite non empty real-membered set;
A6: now
reconsider e9 = e as finite set;
let r be ExtReal;
A7: 1 <= card e9 by NAT_1:14;
assume r in S;
then consider t being Element of (the Sorts of FreeEnv A).v such that
A8: r = card t by A4;
FreeEnv A = MSAlgebra (# FreeSort the Sorts of A, FreeOper the Sorts
of A #) by MSAFREE:def 14;
then (the Sorts of FreeEnv A).v = FreeSort(the Sorts of A,v) by
MSAFREE:def 11;
then t in FreeSort(the Sorts of A, v);
then t in {a9 where a9 is Element of TS(DTConMSA(the Sorts of A)): (ex x
being set st x in (the Sorts of A).v & a9 = root-tree[x,v]) or ex o being
OperSymbol of IIG st [o,the carrier of IIG] = a9.{} & the_result_sort_of o = v}
by MSAFREE:def 10;
then consider a9 being Element of TS(DTConMSA(the Sorts of A)) such that
A9: a9 = t and
A10: (ex x being set st x in (the Sorts of A).v & a9 = root-tree[x,v])
or ex o being OperSymbol of IIG st [o,the carrier of IIG] = a9.{} &
the_result_sort_of o = v;
per cases by A10;
suppose
ex x being set st x in (the Sorts of A).v & a9 = root-tree[x,v];
then consider x being set such that
x in (the Sorts of A).v and
A11: a9 = root-tree[x,v];
root-tree[x,v] = { [{},[x,v]] } by TREES_4:6;
hence r <= card e by A7,A8,A9,A11,CARD_1:30;
end;
suppose
ex o being OperSymbol of IIG st [o,the carrier of IIG] = a9.{}
& the_result_sort_of o = v;
then a9.{} = [action_at v,the carrier of IIG] by A1,MSAFREE2:def 7;
then consider q being DTree-yielding FinSequence such that
A12: t = [action_at v,the carrier of IIG]-tree q by A9,Th9;
deffunc F(Nat) = p +* (q|Seg $1);
consider T being FinSequence such that
A13: len T = len p and
A14: for k being Nat st k in dom T holds T.k = F(k) from FINSEQ_1:
sch 2;
A15: dom T = dom p by A13,FINSEQ_3:29;
A16: the_result_sort_of action_at v = v by A1,MSAFREE2:def 7;
A17: dom p = Seg len p by FINSEQ_1:def 3;
now
per cases;
suppose
len q = 0;
then q = {};
then t = root-tree [action_at v,the carrier of IIG] by A12,TREES_4:20
;
hence r <= card e by A7,A8,PRE_CIRC:19;
end;
suppose
A18: len q <> 0;
defpred P[Nat] means $1 in dom p implies for qk be
DTree-yielding FinSequence st qk = T.$1 for tk be finite set st tk = [action_at
v,the carrier of IIG]-tree qk holds card tk <= card e;
A19: len p = len the_arity_of action_at v by A2,A16,MSAFREE2:10;
then
A20: len p = len q by A12,A16,MSAFREE2:10;
then
A21: 1+0 <= len p by A18,NAT_1:14;
A22: dom p = dom q by A20,FINSEQ_3:29;
A23: dom p = dom the_arity_of action_at v by A19,FINSEQ_3:29;
A24: now
let k be Nat;
assume
A25: P[k];
thus P[k+1]
proof
reconsider tree0 = [action_at v,the carrier of IIG]-tree p as
finite DecoratedTree by A2;
assume
A26: k+1 in dom p;
let qk1 be DTree-yielding FinSequence such that
A27: qk1 = T.(k+1);
let tk1 be finite set;
assume
A28: tk1 = [action_at v,the carrier of IIG]-tree qk1;
then reconsider treek1 = tk1 as finite DecoratedTree;
per cases;
suppose
A29: k = 0;
set v1 = (the_arity_of action_at v)/.1;
A30: 1 in dom p by A21,FINSEQ_3:25;
then consider
e1 being Element of (the Sorts of FreeEnv A).v1 such
that
A31: e1 = p.1 and
A32: card e1 = size (v1, A) by A3;
1 in Seg 1 by FINSEQ_1:3;
then
A33: 1 in dom(q|Seg 1) by A22,A30,RELAT_1:57;
A34: 1 in dom the_arity_of action_at v by A19,A21,FINSEQ_3:25;
then q.1 in (the Sorts of FreeEnv A).((the_arity_of action_at
v).1) by A12,A16,MSAFREE2:11;
then reconsider
T1 = q.1 as Element of (the Sorts of FreeEnv A).v1
by A34,PARTFUN1:def 6;
reconsider Tx = p.1 as finite DecoratedTree by A31;
{} is Element of dom Tx & <*0*> = <*0*>^{} by FINSEQ_1:34
,TREES_1:22;
then reconsider w0 = <*0*> as Element of dom tree0 by A21,
TREES_4:11;
consider q0 being DTree-yielding FinSequence such that
A35: e with-replacement (w0,T1) = [action_at v,the carrier
of IIG]-tree q0 and
A36: len q0 = len p and
A37: q0.(0+1) = T1 and
A38: for i being Nat st i in dom p & i <> 0+1
holds q0.i = p.i by A2,PRE_CIRC:15;
A39: 1 in dom p by A21,FINSEQ_3:25;
then
A40: qk1.1 = (p +* (q|Seg 1)).1 by A14,A15,A27,A29
.= (q|Seg 1).1 by A33,FUNCT_4:13
.= q.1 by FINSEQ_1:3,FUNCT_1:49;
A41: now
let k be Nat;
assume 1 <= k & k <= len q0;
then
A42: k in dom p by A36,FINSEQ_3:25;
per cases;
suppose
k = 1;
hence q0.k = qk1.k by A40,A37;
end;
suppose
A43: k <> 1;
A44: dom(q|Seg 1) = dom q /\ Seg 1 by RELAT_1:61;
not k in Seg 1 by A43,FINSEQ_1:2,TARSKI:def 1;
then
A45: not k in dom(q|Seg 1) by A44,XBOOLE_0:def 4;
thus qk1.k = (p +* (q|Seg 1)).k by A14,A15,A27,A29,A39
.= p.k by A45,FUNCT_4:11
.=q0.k by A38,A42,A43;
end;
end;
dom qk1 = dom(p +* (q|Seg 1)) by A14,A15,A27,A29,A39
.= dom p \/ dom(q|Seg 1) by FUNCT_4:def 1
.= dom p \/ dom q /\ Seg 1 by RELAT_1:61
.= dom p by A22,XBOOLE_1:22;
then len qk1 = len p by FINSEQ_3:29;
then treek1 = tree0 with-replacement (w0,T1) by A2,A28,A35,A36
,A41,FINSEQ_1:14;
then
A46: card treek1 + card (tree0|w0) = card tree0 + card T1 by
PRE_CIRC:18;
consider s1 being finite non empty Subset of NAT such that
A47: s1 = the set of all
card t1 where t1 is Element of (the Sorts of
FreeEnv A).v1 and
A48: card e1 = max s1 by A32,Def4;
reconsider S1 = s1 as finite non empty real-membered set;
card T1 in S1 by A47;
then
A49: card T1 <= card e1 by A48,XXREAL_2:def 8;
tree0|w0 = e1 by A21,A31,TREES_4:def 4;
hence thesis by A2,A49,A46,XREAL_1:8;
end;
suppose
A50: k <> 0;
A51: k+1 <= len p by A26,FINSEQ_3:25;
then
A52: k < len p by NAT_1:13;
set v1 = (the_arity_of action_at v)/.(k+1);
( not k+1 in Seg k)& dom(q|Seg k) = dom q /\ Seg k by
FINSEQ_3:8,RELAT_1:61;
then
A53: not k+1 in dom(q|Seg k) by XBOOLE_0:def 4;
k+1 >= 1 by NAT_1:11;
then
A54: k+1 in dom the_arity_of action_at v by A19,A51,FINSEQ_3:25;
then p.(k+1) in (the Sorts of FreeEnv A). ((the_arity_of
action_at v).(k+1)) by A2,A16,MSAFREE2:11;
then reconsider
T1 = p.(k+1) as Element of (the Sorts of FreeEnv A)
.v1 by A54,PARTFUN1:def 6;
k+1 in Seg(k+1) by FINSEQ_1:3;
then
A55: k+1 in dom(q|Seg(k+1)) by A22,A26,RELAT_1:57;
A56: k >= 1 by A50,NAT_1:14;
then
A57: k in dom p by A52,FINSEQ_3:25;
then T.k = p +* (q|Seg k) by A14,A15;
then reconsider qk = T.k as Function;
A58: dom qk = dom(p +* (q|Seg k)) by A14,A15,A57
.= dom p \/ dom(q|Seg k) by FUNCT_4:def 1
.= dom p \/ dom q /\ Seg k by RELAT_1:61
.= dom p by A22,XBOOLE_1:22;
then dom qk = Seg len p by FINSEQ_1:def 3;
then reconsider qk as FinSequence by FINSEQ_1:def 2;
A59: for x being set st x in dom qk holds qk.x is finite
DecoratedTree
proof
let x be set;
assume
A60: x in dom qk;
then reconsider n = x as Element of NAT;
set v1 = (the_arity_of action_at v)/.n;
qk.n = q.n or qk.n = p.n
proof
per cases;
suppose
A61: n <= k;
n>=1 by A60,FINSEQ_3:25;
then
A62: n in Seg k by A61,FINSEQ_1:1;
dom(q|Seg k) = dom q /\ Seg k by RELAT_1:61;
then
A63: n in dom(q|Seg k) by A22,A58,A60,A62,XBOOLE_0:def 4;
qk.n = (p +* (q|Seg k)).n by A14,A15,A57
.= (q|Seg k).n by A63,FUNCT_4:13
.= q.n by A63,FUNCT_1:47;
hence thesis;
end;
suppose
A64: n > k;
A65: dom(q|Seg k) = dom q /\ Seg k by RELAT_1:61;
not n in Seg k by A64,FINSEQ_1:1;
then
A66: not n in dom(q|Seg k) by A65,XBOOLE_0:def 4;
qk.n = (p +* (q|Seg k)).n by A14,A15,A57
.= p.n by A66,FUNCT_4:11;
hence thesis;
end;
end;
then qk.n in (the Sorts of FreeEnv A). ((the_arity_of
action_at v).n) by A2,A12,A16,A23,A58,A60,MSAFREE2:11;
then reconsider
T1 = qk.n as Element of (the Sorts of FreeEnv A).
v1 by A23,A58,A60,PARTFUN1:def 6;
T1 in (the Sorts of FreeEnv A).v1;
hence thesis;
end;
then for x being object st x in dom qk holds qk.x is
DecoratedTree;
then reconsider qk as DTree-yielding FinSequence by TREES_3:24;
A67: len qk = len p by A58,FINSEQ_3:29;
A68: qk.(k+1) = (p +* (q|Seg k)).(k+1) by A14,A15,A57
.= p.(k+1) by A53,FUNCT_4:11;
now
let x be object;
assume x in dom doms qk;
then
A69: x in dom qk by TREES_3:37;
then reconsider T1 = qk.x as finite DecoratedTree by A59;
dom T1 is finite Tree;
hence (doms qk).x is finite Tree by A69,FUNCT_6:22;
end;
then reconsider
qkf = doms qk as FinTree-yielding FinSequence by TREES_3:23;
tree(qkf) is finite & ex q being DTree-yielding
FinSequence st qk = q & dom( [action_at v,the carrier of IIG]-tree qk) = tree(
doms q) by TREES_4:def 4;
then reconsider
tk = [action_at v,the carrier of IIG]-tree qk as
finite DecoratedTree by FINSET_1:10;
consider e1 being Element of (the Sorts of FreeEnv A).v1 such
that
A70: e1 = p.(k+1) and
A71: card e1 = size (v1, A) by A3,A26;
T1 in (the Sorts of FreeEnv A).v1;
then reconsider Tx = qk.(k+1) as finite DecoratedTree by A68;
v1 = (the_arity_of action_at v).(k+1) by A54,PARTFUN1:def 6;
then reconsider
T1 = q.(k+1) as Element of (the Sorts of FreeEnv A)
.v1 by A12,A16,A54,MSAFREE2:11;
A72: k in NAT by ORDINAL1:def 12;
A73: {} is Element of dom Tx & <*k*> = <*k*>^{} by FINSEQ_1:34
,TREES_1:22;
then <*k*> in dom tk by A52,A67,TREES_4:11;
then consider q0 being DTree-yielding FinSequence such that
A74: tk with-replacement (<*k*>,T1) = [action_at v,the
carrier of IIG]-tree q0 and
A75: len q0 = len qk and
A76: q0.(k+1) = T1 and
A77: for i being Nat st i in dom qk & i <> k+1
holds q0.i = qk.i by PRE_CIRC:15,A72;
A78: qk1.(k+1) = (p +* (q|Seg(k+1))).(k+1) by A14,A15,A26,A27
.= (q|Seg(k+1)).(k+1) by A55,FUNCT_4:13
.= q.(k+1) by FINSEQ_1:3,FUNCT_1:49;
A79: now
let n be Nat;
assume that
A80: 1 <= n and
A81: n <= len q0;
A82: n in dom qk by A75,A80,A81,FINSEQ_3:25;
per cases by XXREAL_0:1;
suppose
n = k+1;
hence q0.n = qk1.n by A78,A76;
end;
suppose
A83: n > k+1;
k+1 >= k by NAT_1:11;
then n > k by A83,XXREAL_0:2;
then
A84: not n in Seg k by FINSEQ_1:1;
dom(q|Seg k) = dom q /\ Seg k by RELAT_1:61;
then
A85: not n in dom(q|Seg k) by A84,XBOOLE_0:def 4;
A86: dom(q|Seg(k+1)) = dom q /\ Seg(k+1) by RELAT_1:61;
not n in Seg(k+1) by A83,FINSEQ_1:1;
then
A87: not n in dom(q|Seg(k+1)) by A86,XBOOLE_0:def 4;
thus qk1.n = (p +* (q|Seg(k+1))).n by A14,A15,A26,A27
.= p.n by A87,FUNCT_4:11
.= (p +* (q|Seg k)).n by A85,FUNCT_4:11
.= qk.n by A14,A15,A57
.= q0.n by A77,A82,A83;
end;
suppose
A88: n < k+1;
A89: n in dom q by A20,A67,A75,A80,A81,FINSEQ_3:25;
n <= k by A88,NAT_1:13;
then
A90: n in Seg k by A80,FINSEQ_1:1;
dom(q|Seg k) = dom q /\ Seg k by RELAT_1:61;
then
A91: n in dom(q|Seg k) by A89,A90,XBOOLE_0:def 4;
A92: dom(q|Seg(k+1)) = dom q /\ Seg(k+1) by RELAT_1:61;
n in Seg(k+1) by A80,A88,FINSEQ_1:1;
then
A93: n in dom(q|Seg(k+1)) by A89,A92,XBOOLE_0:def 4;
thus qk1.n = (p +* (q|Seg(k+1))).n by A14,A15,A26,A27
.= (q|Seg(k+1)).n by A93,FUNCT_4:13
.= q.n by A93,FUNCT_1:47
.= (q|Seg k).n by A91,FUNCT_1:47
.= (p +* (q|Seg k)).n by A91,FUNCT_4:13
.= qk.n by A14,A15,A57
.= q0.n by A77,A82,A88;
end;
end;
k < len qk by A52,A58,FINSEQ_3:29;
then reconsider w0 = <*k*> as Element of dom tk by A73,
TREES_4:11;
dom qk1 = dom(p +* (q|Seg(k+1))) by A14,A15,A26,A27
.= dom p \/ dom(q|Seg(k+1)) by FUNCT_4:def 1
.= dom p \/ dom q /\ Seg(k+1) by RELAT_1:61
.= dom p by A22,XBOOLE_1:22;
then len qk1 = len p by FINSEQ_3:29;
then treek1 = tk with-replacement (w0,T1) by A28,A67,A74,A75
,A79,FINSEQ_1:14;
then
A94: card treek1 + card (tk|w0) = card tk + card T1 by PRE_CIRC:18;
consider s1 being finite non empty Subset of NAT such that
A95: s1 = the set of all
card t1 where t1 is Element of (the Sorts of
FreeEnv A).v1 and
A96: card e1 = max s1 by A71,Def4;
reconsider S1 = s1 as finite non empty real-membered set;
card T1 in S1 by A95;
then
A97: card T1 <= card e1 by A96,XXREAL_2:def 8;
tk|w0 = e1 by A52,A70,A68,A67,TREES_4:def 4;
then
A98: card tk1 <= card tk by A97,A94,XREAL_1:8;
card tk <= card e by A25,A56,A52,FINSEQ_3:25;
hence thesis by A98,XXREAL_0:2;
end;
end;
end;
A99: P[ 0 ] by FINSEQ_3:25;
A100: for k be Nat holds P[k] from NAT_1:sch 2(A99,A24);
dom p = Seg len p by FINSEQ_1:def 3;
then
A101: dom p = dom q by A20,FINSEQ_1:def 3;
A102: len p in dom p by A21,FINSEQ_3:25;
then T.len p = p +* (q|dom p) by A14,A15,A17
.= p +* q by A101
.= q by A22,FUNCT_4:19;
hence r <= card e by A8,A12,A100,A102;
end;
end;
hence r <= card e;
end;
end;
card e in S by A4;
hence thesis by A5,A6,XXREAL_2:def 8;
end;
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
:Def6:
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;
existence
proof
deffunc F(Element of (the Sorts of FreeEnv A).v) = depth $1;
set s = { F(t) where t is Element of (the Sorts of FreeEnv A).v : P[t]};
set t = the Element of (the Sorts of FreeEnv A).v;
A1: depth t in s;
A2: s is Subset of NAT from DOMAIN_1:sch 8;
s is finite from PRE_CIRC:sch 1;
then reconsider s as finite non empty Subset of NAT by A1,A2;
reconsider m = max s as Nat by TARSKI:1;
take m,s;
thus thesis;
end;
correctness;
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
:Def7:
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;
existence
proof
deffunc F(Element of IIG) = depth($1,A);
set Ds = { F(v) where v is Element of IIG : v in the carrier of IIG };
A1: Ds is natural-membered
proof
let e be object;
assume e in Ds;
then ex v being Element of IIG st e = depth(v,A) & v in the carrier of
IIG;
hence thesis;
end;
set v = the Element of IIG;
A2: depth(v,A) in Ds;
A3: the carrier of IIG is finite;
Ds is finite from FRAENKEL:sch 21 (A3);
then reconsider Ds as finite non empty Subset of NAT by A1,A2,MEMBERED:6;
reconsider m = max Ds as Nat by TARSKI:1;
take m,Ds;
thus thesis;
end;
uniqueness;
end;
theorem
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
proof
let IIG be finite monotonic Circuit-like non void non empty ManySortedSign
, A be non-empty Circuit of IIG, v be Vertex of IIG;
consider Ds being finite non empty Subset of NAT such that
A1: Ds = { depth(v9,A) where v9 is Element of IIG : v9 in the carrier of
IIG } and
A2: depth A = max Ds by Def7;
reconsider Y = Ds as finite non empty real-membered set;
depth(v,A) in Y by A1;
hence thesis by A2,XXREAL_2:def 8;
end;
theorem Th18:
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
proof
let IIG;
let A be non-empty Circuit of IIG, v be Vertex of IIG;
consider s being finite non empty Subset of NAT such that
A1: s = the set of all
depth t where t is Element of (the Sorts of FreeEnv A).v and
A2: depth(v,A) = max s by Def6;
reconsider Y = s as finite non empty real-membered set;
A3: max Y in the set of all
depth t where t is Element of (the Sorts of FreeEnv A).v
by A1,XXREAL_2:def 8;
consider ss being finite non empty Subset of NAT such that
A4: ss = the set of all
card tt where tt is Element of (the Sorts of FreeEnv A).v and
A5: size(v,A) = max ss by Def4;
reconsider YY = ss as finite non empty real-membered set;
consider t being Element of (the Sorts of FreeEnv A).v such that
A6: depth t = max Y by A3;
reconsider t99 = t as Function;
consider t2 being Element of (the Sorts of FreeMSA the Sorts of A).v such
that
A7: t = t2 and
A8: depth t = depth t2 by Def5;
consider dt being finite DecoratedTree, t9 being finite Tree such that
A9: dt = t2 & t9 = dom dt and
A10: depth t2 = height t9 by MSAFREE2:def 14;
consider p being FinSequence of NAT such that
A11: p in t9 and
A12: len p = height t9 by TREES_1:def 12;
consider y99 being object such that
A13: [p,y99] in t99 by A7,A9,A11,XTUPLE_0:def 12;
thus depth(v,A) = 0 implies v in InputVertices IIG or v in
SortsWithConstants IIG
proof
assume
A14: depth(v,A) = 0;
A15: for kk being ExtReal st kk in YY holds kk <= 1
proof
let kk be ExtReal;
assume kk in YY;
then consider tt being Element of (the Sorts of FreeEnv A).v such that
A16: card tt = kk by A4;
consider tiv being Element of (the Sorts of FreeMSA the Sorts of A).v
such that
A17: tt = tiv & depth tt = depth tiv by Def5;
depth tt in Y by A1;
then
A18: depth tt = 0 by A2,A14,XXREAL_2:def 8;
A19: ex dt9 being finite DecoratedTree, t999 being finite Tree st dt9 =
tiv & t999 = dom dt9 & depth tiv = height t999 by MSAFREE2:def 14;
then rng tt = { tt.{} } by A18,A17,FUNCT_1:4,TREES_1:29,43;
then tt = { [{},tt.{}] }
by A18,A17,A19,RELAT_1:189,TREES_1:29,43;
hence thesis by A16,CARD_1:30;
end;
rng t99 = { t.{} } by A2,A6,A7,A8,A9,A10,A14,FUNCT_1:4,TREES_1:29,43;
then t99 = { [{},t.{}] }
by A2,A6,A7,A8,A9,A10,A14,RELAT_1:189,TREES_1:29,43;
then card t = 1 by CARD_1:30;
then 1 in YY by A4;
then size(v,A) = 1 by A5,A15,XXREAL_2:def 8;
then v in InputVertices IIG \/ SortsWithConstants IIG by Th10;
hence thesis by XBOOLE_0:def 3;
end;
reconsider ct = card t as Real;
{} in dom t by TREES_1:22;
then consider y being object such that
A20: [{},y] in t99 by XTUPLE_0:def 12;
A21: card t in ss by A4;
assume v in InputVertices IIG or v in SortsWithConstants IIG;
then v in InputVertices IIG \/ SortsWithConstants IIG by XBOOLE_0:def 3;
then size(v,A) = 1 by Th10;
then ct <= 1 by A5,A21,XXREAL_2:def 8;
then card t <= 0 or card t = 0 + 1 by NAT_1:8;
then consider x being object such that
A22: t = {x} by CARD_2:42;
x = [{},y] by A22,A20,TARSKI:def 1;
then [p,y99] = [{},y] by A22,A13,TARSKI:def 1;
then p = {} by XTUPLE_0:1;
hence thesis by A2,A6,A8,A10,A12;
end;
theorem
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)
proof
let IIG;
let A be finite-yielding non-empty MSAlgebra over IIG, v, v1 be SortSymbol
of IIG;
assume that
A1: v in InnerVertices IIG and
A2: v1 in rng the_arity_of action_at v;
size(v1,A) > 0 by Th15;
then
A3: 0 + 1 <= size(v1,A) by NAT_1:13;
size(v1,A) < size(v,A) by A1,A2,Th14;
then
A4: not v in InputVertices IIG \/ SortsWithConstants IIG by A3,Th10;
then
A5: not v in SortsWithConstants IIG by XBOOLE_0:def 3;
then
A6: v in (InnerVertices IIG \ SortsWithConstants IIG) by A1,XBOOLE_0:def 5;
consider s1 being finite non empty Subset of NAT such that
A7: s1 = the set of all
depth t1 where t1 is Element of (the Sorts of FreeEnv A).v1 and
A8: depth(v1,A) = max s1 by Def6;
reconsider Y1 = s1 as finite non empty real-membered set;
max Y1 in the set of all
depth t1 where t1 is Element of (the Sorts of FreeEnv A ) .
v1 by A7,XXREAL_2:def 8;
then consider t1 being Element of (the Sorts of FreeEnv A).v1 such that
A9: depth t1 = max Y1;
reconsider av = action_at v as OperSymbol of IIG;
consider s being finite non empty Subset of NAT such that
A10: s = the set of all
depth t where t is Element of (the Sorts of FreeEnv A).v and
A11: depth(v,A) = max s by Def6;
consider x being object such that
A12: x in dom the_arity_of av and
A13: v1 = (the_arity_of av).x by A2,FUNCT_1:def 3;
reconsider Y = s as finite non empty real-membered set;
max Y in the set of all
depth t where t is Element of (the Sorts of FreeEnv A).v
by A10,XXREAL_2:def 8;
then consider t being Element of (the Sorts of FreeEnv A).v such that
A14: depth t = max Y;
FreeEnv A = MSAlgebra (# FreeSort the Sorts of A, FreeOper the Sorts of
A #) by MSAFREE:def 14;
then (the Sorts of FreeEnv A).v = FreeSort(the Sorts of A,v) by
MSAFREE:def 11;
then t in FreeSort(the Sorts of A,v);
then
A15: t in {a where a is Element of TS(DTConMSA(the Sorts of A)): (ex x being
set st x in (the Sorts of A).v & a = root-tree[x,v]) or ex o being OperSymbol
of IIG st [o,the carrier of IIG] = a.{} & the_result_sort_of o = v} by
MSAFREE:def 10;
reconsider k = x as Element of NAT by A12;
reconsider k1 = k - 1 as Element of NAT by A12,FINSEQ_3:26;
reconsider f = <*k1*> as FinSequence of NAT;
A16: k1 + 1 = k;
reconsider tft = t with-replacement (f,t1) as DecoratedTree;
consider e9 being Element of (the Sorts of FreeMSA the Sorts of A).v1 such
that
A17: t1 = e9 and
A18: depth t1 = depth e9 by Def5;
consider dt19 being finite DecoratedTree, t19 being finite Tree such that
A19: dt19 = e9 & t19 = dom dt19 and
A20: depth e9 = height t19 by MSAFREE2:def 14;
consider a being Element of TS(DTConMSA(the Sorts of A)) such that
A21: a = t and
A22: (ex x being set st x in (the Sorts of A).v & a = root-tree[x,v]) or
ex o being OperSymbol of IIG st [o,the carrier of IIG] = a.{} &
the_result_sort_of o = v by A15;
A23: not v in InputVertices IIG by A4,XBOOLE_0:def 3;
now
given x being set such that
x in (the Sorts of A).v and
A24: a = root-tree[x,v];
consider e9 being Element of (the Sorts of FreeMSA the Sorts of A).v such
that
A25: t = e9 & depth t = depth e9 by Def5;
ex dta being finite DecoratedTree, ta being finite Tree st dta = e9 &
ta = dom dta & depth e9 = height ta by MSAFREE2:def 14;
then depth t = 0 by A21,A24,A25,TREES_1:42,TREES_4:3;
hence contradiction by A11,A14,A23,A5,Th18;
end;
then consider o being OperSymbol of IIG such that
A26: [o,the carrier of IIG] = a.{} and
A27: the_result_sort_of o = v by A22;
NonTerminals(DTConMSA(the Sorts of A)) = [:the carrier' of IIG,{the
carrier of IIG}:] & the carrier of IIG in {the carrier of IIG} by MSAFREE:6
,TARSKI:def 1;
then reconsider
o9 = [o,the carrier of IIG] as NonTerminal of DTConMSA(the Sorts
of A) by ZFMISC_1:87;
consider q being FinSequence of TS(DTConMSA(the Sorts of A)) such that
A28: a = o9-tree q and
o9 ==> roots q by A26,DTCONSTR:10;
consider q9 being DTree-yielding FinSequence such that
A29: q = q9 and
A30: dom a = tree(doms q9) by A28,TREES_4:def 4;
A31: t = [av,the carrier of IIG]-tree q9 by A1,A21,A27,A28,A29,MSAFREE2:def 7;
A32: o = av by A1,A27,MSAFREE2:def 7;
then
A33: len q9 = len the_arity_of av by A21,A27,A28,A29,MSAFREE2:10;
then
A34: k in dom q9 by A12,FINSEQ_3:29;
A35: dom q9 = dom the_arity_of av by A33,FINSEQ_3:29;
then consider qq being DTree-yielding FinSequence such that
A36: t with-replacement (f,t1) = o9-tree qq and
A37: len qq = len q9 and
qq.(k1+1) = t1 and
for i being Nat st i in dom q9 & i <> k1+1 holds qq.i = q9.i
by A21,A28,A29,A30,A12,PRE_CIRC:13,15;
A38: k in dom qq by A12,A33,A37,FINSEQ_3:29;
q9.k in (the Sorts of FreeEnv A).v1 by A21,A27,A28,A29,A12,A13,A32,
MSAFREE2:11;
then reconsider tft as Element of (the Sorts of FreeEnv A).v by A6,A34,A16
,A31,Th6;
reconsider dtft = depth tft as Real;
dtft in Y by A10;
then
A39: dtft <= depth t by A14,XXREAL_2:def 8;
consider e9 being Element of (the Sorts of FreeMSA the Sorts of A).v such
that
A40: tft = e9 and
A41: depth tft = depth e9 by Def5;
consider dttft being finite DecoratedTree, ttft being finite Tree such that
A42: dttft = e9 & ttft = dom dttft and
A43: depth e9 = height ttft by MSAFREE2:def 14;
ex qq9 being DTree-yielding FinSequence st qq = qq9 & dom tft = tree(
doms qq9) by A36,TREES_4:def 4;
then reconsider f9 = f as Element of ttft by A16,A40,A42,A38,PRE_CIRC:13;
<*k1*> in tree(doms q9) by A12,A35,A16,PRE_CIRC:13;
then dom tft = dom t with-replacement (f,dom t1) by A21,A30,TREES_2:def 11;
then f9 <> {} & ttft|f = t19 by A17,A19,A21,A30,A34,A16,A40,A42,PRE_CIRC:13
,TREES_1:33;
hence thesis by A11,A14,A8,A9,A18,A20,A39,A41,A43,TREES_1:48,XXREAL_0:2;
end;