Copyright (c) 1994 Association of Mizar Users
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;
definitions TARSKI, MEMBERED;
theorems AXIOMS, TARSKI, REAL_1, ZFMISC_1, NAT_1, FINSEQ_1, FINSEQ_2,
FINSEQ_3, FINSEQ_4, FUNCT_1, FUNCT_2, TREES_1, TREES_2, TREES_3, TREES_4,
GROUP_1, CARD_1, CARD_2, CARD_3, FUNCOP_1, PBOOLE, PRALG_2, MSUALG_1,
MSUALG_2, RELAT_1, MSAFREE1, MSAFREE, PRE_CIRC, DTCONSTR, LANG1,
RLVECT_1, MSAFREE2, FUNCT_4, FUNCT_6, AMI_1, XBOOLE_0, XBOOLE_1,
XCMPLX_1, MEMBERED;
schemes NAT_1, FINSEQ_1, PRE_CIRC, MSUALG_1, FRAENKEL, COMPLSP1;
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
:Def1:
for x being Vertex of IIG st x in dom it
holds it.x in Constants (SCS, x);
existence
proof
set SW = SortsWithConstants IIG;
defpred P[set, set] means
ex v being Vertex of IIG st v = $1 & $2 in Constants (SCS, v);
A1: now
let i be set;
assume
A2: i in SW;
then reconsider x = i as Vertex of IIG;
SW = {v where v is SortSymbol of IIG : v is with_const_op }
by MSAFREE2:def 1;
then consider v being Vertex of IIG such that
A3: v = x & v is with_const_op by A2;
consider o be OperSymbol of IIG such that
A4: (the Arity of IIG).o = {} & (the ResultSort of IIG).o = v by A3,
MSUALG_2:def 2;
consider A being non empty set such that
A5: 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 4;
consider y being Element of rng Den(o,SCS);
Den (o, SCS) is non empty by MSUALG_1:6;
then A6: rng Den (o, SCS) <> {} by RELAT_1:64;
then A7: y in rng Den(o, SCS);
A8: dom the ResultSort of IIG = the OperSymbols of IIG by FUNCT_2:def 1;
Result (o, SCS)=((the Sorts of SCS) * the ResultSort of IIG).o
by MSUALG_1:def 10
.= (the Sorts of SCS).((the ResultSort of IIG).o) by A8,FUNCT_1:23;
then reconsider y' = y as Element of (the Sorts of SCS).v by A4,A7;
A9: y' in Constants (SCS, x) by A3,A4,A5,A6;
reconsider y as set;
take y;
thus P[i, y] by A9;
end;
consider f being ManySortedSet of SW such that
A10: for i being set st i in SW
holds P[i,f.i] from MSSEx (A1);
take f;
let x be Vertex of IIG;
assume x in dom f;
then x in SW by PBOOLE:def 3;
then P[x, f.x] by A10;
hence f.x in Constants (SCS, x);
end;
correctness
proof
let it1, it2 be ManySortedSet of SortsWithConstants IIG;
assume
A11: for x being Vertex of IIG st x in dom it1
holds it1.x in Constants (SCS, x);
assume
A12: for x being Vertex of IIG st x in dom it2
holds it2.x in Constants (SCS, x);
now
let i be set;
assume
A13: i in SortsWithConstants IIG;
then reconsider v = i as Vertex of IIG;
dom it1 = SortsWithConstants IIG
& dom it2 = SortsWithConstants IIG by PBOOLE:def 3;
then A14: it1.v in Constants (SCS, v)
& it2.v in Constants (SCS, v) by A11,A12,A13;
consider A being non empty set such that
A15: 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 4;
consider a1 being Element of (the Sorts of SCS).v such that
A16: it1.v = a1 and
A17: 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,A15;
consider a2 being Element of (the Sorts of SCS).v such that
A18: it2.v = a2 and
A19: 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,A15;
consider o1 be OperSymbol of IIG such that
A20: (the Arity of IIG).o1 = {} and
A21: (the ResultSort of IIG).o1 = v and
A22: a1 in rng Den(o1,SCS) by A17;
consider o2 being OperSymbol of IIG such that
(the Arity of IIG).o2 = {} and
A23: (the ResultSort of IIG).o2 = v and
A24: a2 in rng Den(o2,SCS) by A19;
A25: the_result_sort_of o1 = v & the_result_sort_of o2 = v
by A21,A23,MSUALG_1:def 7;
then A26: o1 = o2 by MSAFREE2:def 6;
A27: dom the Arity of IIG = the OperSymbols of IIG by FUNCT_2:def 1;
A28: {} = <*>the carrier of IIG;
A29: 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 9
.= (the Sorts of SCS)#.((the Arity of IIG).o1) by A27,FUNCT_1:23
.= {{}} by A20,A28,PRE_CIRC:5;
consider x1 being set such that
A30: x1 in dom Den(o1, SCS) and
A31: a1 = Den(o1,SCS).x1 by A22,FUNCT_1:def 5;
consider x2 being set such that
A32: x2 in dom Den(o2, SCS) and
A33: a2 = Den(o2,SCS).x2 by A24,FUNCT_1:def 5;
x1 = {} & x2 = {} by A26,A29,A30,A32,TARSKI:def 1;
hence it1.i = it2.i by A16,A18,A25,A31,A33,MSAFREE2:def 6;
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
A1: v in SortsWithConstants IIG & e in Constants (SCS, v);
then v in dom Set-Constants SCS by PBOOLE:def 3;
then A2: (Set-Constants SCS).v in Constants (SCS, v) by Def1;
consider A being non empty set such that
A3: 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 4;
consider a being Element of (the Sorts of SCS).v such that
A4: 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 A1,A3;
consider o being OperSymbol of IIG such that
A5: (the Arity of IIG).o = {}
& (the ResultSort of IIG).o = v & e in rng Den(o,SCS) by A4;
consider a being Element of (the Sorts of SCS).v such that
A6: 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 A2,A3;
consider o1 being OperSymbol of IIG such that
A7: (the Arity of IIG).o1 = {}
& (the ResultSort of IIG).o1 = v
& (Set-Constants SCS).v in rng Den(o1,SCS) by A6;
A8: the_result_sort_of o = (the ResultSort of IIG).o
& the_result_sort_of o1 = (the ResultSort of IIG).o1
by MSUALG_1:def 7;
then A9: o = o1 by A5,A7,MSAFREE2:def 6;
A10: dom the Arity of IIG = the OperSymbols of IIG by FUNCT_2:def 1;
A11: {} = <*>the carrier of IIG;
A12: 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 9
.= (the Sorts of SCS)#.((the Arity of IIG).o) by A10,FUNCT_1:23
.= {{}} by A5,A11,PRE_CIRC:5;
consider d being set such that
A13: d in dom Den(o, SCS) & e = Den(o, SCS).d by A5,FUNCT_1:def 5;
consider d1 being set such that
A14: d1 in dom Den(o1, SCS) & (Set-Constants SCS).v = Den(o1, SCS).d1
by A7,FUNCT_1:def 5;
d = {} & d1 = {} by A9,A12,A13,A14,TARSKI:def 1;
hence (Set-Constants SCS).v = e by A5,A7,A8,A13,A14,MSAFREE2:def 6;
end;
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 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;
assume
A1: IIG is with_input_V;
reconsider A = InputVertices IIG as Subset of IIG;
reconsider A as non empty Subset of IIG by A1,MSAFREE2:def
4;
reconsider SS = the Sorts of SCS as non-empty ManySortedSet of
the carrier of IIG;
reconsider SI = SS | A as ManySortedSet of A;
reconsider SI as non-empty ManySortedSet of A;
consider ivm being ManySortedSet of A such that
A2: ivm = (commute InpFs).n & ivm in SI by PRE_CIRC:10;
now
let v be Vertex of IIG;
assume
A3: v in InputVertices IIG;
then SI.v = (the Sorts of SCS).v by FUNCT_1:72;
hence ivm.v in (the Sorts of SCS).v by A2,A3,PBOOLE:def 4;
end;
hence (commute InpFs).n is InputValues of SCS by A2,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;
canceled;
theorem
for IIG
for SCS being non-empty Circuit of IIG, s being State of SCS
holds dom s = the carrier of IIG
proof
let IIG;
let SCS be non-empty Circuit of IIG, s be State of SCS;
consider g being Function such that
A1: s = g & dom g = dom the Sorts of SCS
& for x being set st x in dom the Sorts of SCS
holds g.x in (the Sorts of SCS).x by CARD_3:def 5;
thus dom s = the carrier of IIG by A1,PBOOLE:def 3;
end;
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;
A1: dom the Sorts of SCS = the carrier of IIG by PBOOLE:def 3;
consider g being Function such that
A2: s = g & dom g = dom the Sorts of SCS
& for x being set st x in dom the Sorts of SCS
holds g.x in (the Sorts of SCS).x by CARD_3:def 5;
thus s.v in (the Sorts of SCS).v by A1,A2;
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:10;
hence s * (the_arity_of o) is Element of Args (o, SCS) by PRE_CIRC:11;
end;
correctness;
end;
reserve IIG for monotonic Circuit-like
(non void non empty ManySortedSign);
theorem Th6:
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
proof
let IIG;
let SCS be locally-finite 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;
A1: FreeEnv SCS = FreeMSA the Sorts of SCS by MSAFREE2:def 8;
assume that
A2: v in InnerVertices IIG and
A3: e1 = [action_at v,the carrier of IIG]-tree q1;
thus 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
proof
let k be Nat;
assume that
A4: k in dom q1 and
A5: q1.k in (the Sorts of FreeEnv SCS).w;
reconsider av = action_at v as OperSymbol of IIG;
e1 in (the Sorts of FreeEnv SCS).v;
then A6: e1 in (the Sorts of FreeEnv SCS)
.(the_result_sort_of av) by A2,MSAFREE2:def 7;
then len q1 = len (the_arity_of av) by A1,A3,MSAFREE2:13;
then A7: k in dom the_arity_of av by A4,FINSEQ_3:31;
then A8: q1.k in (the Sorts of FreeEnv SCS)
.((the_arity_of av).k) by A1,A3,A6,MSAFREE2:14;
A9: FreeEnv SCS = MSAlgebra (# FreeSort the Sorts of SCS,
FreeOper the Sorts of SCS #) by A1,MSAFREE:def 16;
then A10: q1.k in (FreeSort the Sorts of SCS).((the_arity_of av)/.k) by A7,
A8,FINSEQ_4:def 4;
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:13;
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 A5,A9,A10,XBOOLE_0:def 3;
end;
hence w = (the_arity_of action_at v)/.k;
end;
end;
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;
coherence
proof
let a be Element of (the Sorts of FreeEnv SCS).v;
reconsider b = a
as Element of (the Sorts of FreeMSA the Sorts of SCS).v by MSAFREE2:def 8;
b is finite non empty Function-like Relation-like;
hence thesis;
end;
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;
coherence
proof
let a be Element of (the Sorts of FreeEnv SCS).v;
reconsider b = a
as Element of (the Sorts of FreeMSA the Sorts of SCS).v by MSAFREE2:def 8;
b is DecoratedTree-like;
hence thesis;
end;
end;
theorem Th7:
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
proof
let IIG;
let SCS be locally-finite 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 Nat;
A1: FreeEnv SCS = FreeMSA the Sorts of SCS by MSAFREE2:def 8;
set k = k1 + 1, eke = e1 with-replacement (<*k1*>,e2);
assume that
A2: v in InnerVertices IIG \ SortsWithConstants IIG and
A3: e1 = [action_at v,the carrier of IIG]-tree q1 and
A4: k in dom q1 and
A5: q1.k in (the Sorts of FreeEnv SCS).w;
A6: FreeEnv SCS = MSAlgebra (# FreeSort the Sorts of SCS,
FreeOper the Sorts of SCS #) by A1,MSAFREE:def 16;
then A7: (the Sorts of FreeEnv SCS).v
= FreeSort(the Sorts of SCS, v) by MSAFREE:def 13;
then A8: e1 in TS(DTConMSA(the Sorts of SCS)) by TARSKI:def 3;
reconsider av = action_at v as OperSymbol of IIG;
A9: NonTerminals(DTConMSA(the Sorts of SCS))
= [:the OperSymbols of IIG,{the carrier of IIG}:] by MSAFREE:6;
the carrier of IIG in {the carrier of IIG} by TARSKI:def 1;
then reconsider nt = [av,the carrier of IIG]
as NonTerminal of DTConMSA(the Sorts of SCS) by A9,ZFMISC_1:106;
e1.{} = nt by A3,TREES_4:def 4;
then consider p' being FinSequence of TS(DTConMSA(the Sorts of SCS))
such that
A10: e1 = nt-tree p' and
nt ==> roots p' by A8,DTCONSTR:10;
reconsider q1' = q1 as FinSequence of
TS(DTConMSA(the Sorts of SCS)) by A3,A10,TREES_4:15;
reconsider e1' = e1 as DecoratedTree;
consider p' being DTree-yielding FinSequence such that
A11: p' = q1 and
A12: dom e1' = tree(doms p') by A3,TREES_4:def 4;
reconsider m = <*k1*> as Element of dom e1 by A4,A11,A12,PRE_CIRC:17;
reconsider m' = m as FinSequence of NAT;
consider qq being DTree-yielding FinSequence such that
A13: e1 with-replacement (m',e2) = [av,the carrier of IIG]-tree qq and
A14: len qq = len q1 and
A15: qq.(k1+1) = e2 and
A16: for i being Nat st i in dom q1
holds (i <> (k1+1) implies qq.i = q1.i) by A3,PRE_CIRC:19;
A17: dom qq = dom q1 by A14,FINSEQ_3:31;
reconsider O =
[:the OperSymbols 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*;
A18: DTConMSA(the Sorts of SCS) = DTConstrStr (# O, R #) by MSAFREE:def 10;
then reconsider TSDT = TS(DTConMSA(the Sorts of SCS))
as Subset of FinTrees(O);
now
let x be set;
assume x in TSDT;
then x is Element of FinTrees(O);
hence x is DecoratedTree of O;
end;
then reconsider TSDT as DTree-set of O by TREES_3:def 6;
(the Sorts of FreeEnv SCS).w
= FreeSort(the Sorts of SCS, w) by A6,MSAFREE:def 13;
then A19: e2 in FreeSort(the Sorts of SCS, w);
then e2 in {a' where a' is Element of TS(DTConMSA(the Sorts of SCS)):
(ex x being set st x in (the Sorts of SCS).w
& a' = root-tree[x,w]) or
ex o being OperSymbol of IIG st [o,the carrier of IIG] = a'.{}
& the_result_sort_of o = w} by MSAFREE:def 12;
then consider aa being Element of TS(DTConMSA(the Sorts of SCS))
such that
A20: aa = e2 and
A21: (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;
rng qq c= TS(DTConMSA(the Sorts of SCS))
proof
let y be set;
assume y in rng qq;
then consider x being set such that
A22: x in dom qq and
A23: y = qq.x by FUNCT_1:def 5;
reconsider x as Nat by A22;
per cases;
suppose x = k1+1;
hence y in TS(DTConMSA(the Sorts of SCS)) by A15,A20,A23;
suppose x <> k1+1;
then qq.x = q1'.x by A16,A17,A22;
hence y in TS(DTConMSA(the Sorts of SCS)) by A17,A22,A23,FINSEQ_2:13
;
end;
then reconsider q' = qq as FinSequence of TSDT by FINSEQ_1:def 4;
reconsider rq = roots q' as FinSequence of O;
reconsider rq as Element of O* by FINSEQ_1:def 11;
A24: dom rq = dom qq by DTCONSTR:def 1;
then A25: len rq = len qq by FINSEQ_3:31;
A26: v in InnerVertices IIG by A2,XBOOLE_0:def 4;
then A27: (the Sorts of FreeEnv SCS).(the_result_sort_of av)
= (the Sorts of FreeEnv SCS).v by MSAFREE2:def 7;
then A28: len q1 = len (the_arity_of av) by A1,A3,MSAFREE2:13;
then A29: dom rq = dom (the_arity_of av) by A14,A24,FINSEQ_3:31;
for x being set st x in dom rq
holds (rq.x in [:the OperSymbols 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
let x be set;
assume
A30: x in dom rq;
then reconsider x' = x as Nat;
A31: (the_arity_of av)/.x' = (the_arity_of av).x'
by A29,A30,FINSEQ_4:def 4;
consider T being DecoratedTree such that
A32: T = qq.x' and
A33: rq.x' = T.{} by A24,A30,DTCONSTR:def 1;
A34: dom roots q1 = dom q1 by DTCONSTR:def 1;
consider T' being DecoratedTree such that
A35: T' = q1.x' and
A36: (roots q1).x' = T'.{} by A17,A24,A30,DTCONSTR:def 1;
reconsider q1' as FinSequence of TSDT;
reconsider b = roots q1' as
Element of
([:the OperSymbols of IIG,{the carrier of IIG}:] \/
Union(coprod the Sorts of SCS))* by FINSEQ_1:def 11;
A37: dom q1 = dom the_arity_of av by A28,FINSEQ_3:31;
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
A38: n in dom q1;
then A39: q1.n in (the Sorts of FreeEnv SCS)
.((the_arity_of av).n) by A1,A3,A27,A37,MSAFREE2:14;
(the_arity_of av).n = (the_arity_of av)/.n
by A37,A38,FINSEQ_4:def 4;
hence q1.n in FreeSort(the Sorts of SCS, (the_arity_of av)/.n)
by A6,A39,MSAFREE:def 13;
end;
then A40: q1' in ((FreeSort the Sorts of SCS)# * (the Arity of IIG)).
av
by A37,MSAFREE:9;
reconsider b as FinSequence;
the carrier of IIG in {the carrier of IIG} by TARSKI:def 1;
then [av,the carrier of IIG] in
[:the OperSymbols of IIG,{the carrier of IIG}:] by ZFMISC_1:106;
then reconsider av' = [av,the carrier of IIG]
as Symbol of DTConMSA(the Sorts of SCS) by A18,XBOOLE_0:def 2;
Sym(av, the Sorts of SCS) = [av,the carrier of IIG]
by MSAFREE:def 11;
then av' ==> b by A40,MSAFREE:10;
then A41: [av',b] in R by A18,LANG1:def 1;
A42: (the_arity_of av)/.k = w by A3,A4,A5,A26,Th6;
thus rq.x in [:the OperSymbols 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
A43: rq.x in [:the OperSymbols of IIG,{the carrier of IIG}:];
let o1 be OperSymbol of IIG;
assume
A44: [o1,the carrier of IIG] = rq.x;
per cases;
suppose
A45: x' = k1+1;
now
per cases by A21;
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
A46: aa = root-tree[xx,w];
[o1,the carrier of IIG] = [xx,w] by A15,A20,A32,A33,A44,
A45,A46,TREES_4:3;
then A47: the carrier of IIG = w by ZFMISC_1:33;
for X be set holds not X in X;
hence contradiction by A47;
case ex o being OperSymbol of IIG st
[o,the carrier of IIG] = aa.{}
& the_result_sort_of o = w;
then consider o being OperSymbol of IIG such that
A48: [o,the carrier of IIG] = aa.{} and
A49: the_result_sort_of o = w;
thus the_result_sort_of o1 = (the_arity_of av).x
by A15,A20,A31,A32,A33,A42,A44,A45,A48,A49,ZFMISC_1:33;
end;
hence thesis;
suppose
x' <> k1+1;
then (roots q1).x' = [o1,the carrier of IIG]
by A16,A17,A24,A30,A32,A33,A35,A36,A44;
hence the_result_sort_of o1 = (the_arity_of av).x
by A17,A24,A30,A34,A41,A43,A44,MSAFREE1:3;
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
A50: 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,
x'' being set such that
A51: x'' in (the Sorts of SCS).s1 and
A52: rq.x = [x'',s1] by MSAFREE:7;
per cases;
suppose
A53: x' = k1+1;
A54: e2 in (FreeSort the Sorts of SCS).w by A19,MSAFREE:def 13;
reconsider rqx = rq.x' as Terminal of DTConMSA the Sorts of
SCS by A50,MSAFREE:6;
aa = root-tree rqx by A15,A20,A32,A33,A53,DTCONSTR:9;
then aa in {a'' where a'' is Element of TS(DTConMSA(the Sorts
of SCS)): (ex x''' being set st x''' in (the Sorts of SCS).s1
& a'' = root-tree[x''',s1]) or ex o being OperSymbol of IIG
st [o,the carrier of IIG] = a''.{} &
the_result_sort_of o = s1}
by A51,A52;
then A55: aa in FreeSort(the Sorts of SCS, s1) by
MSAFREE:def 12;
now
A56: e2 in (FreeSort the Sorts of SCS).s1 by A20,A55,MSAFREE:def 13
;
assume w <> s1;
then (FreeSort the Sorts of SCS).w misses
(FreeSort the Sorts of SCS).s1 by MSAFREE:13;
then (FreeSort the Sorts of SCS).w /\
(FreeSort the Sorts of SCS).s1 = {} by XBOOLE_0:def 7;
hence contradiction by A54,A56,XBOOLE_0:def 3;
end;
hence rq.x in coprod((the_arity_of av).x, the Sorts of SCS)
by A31,A42,A51,A52,A53,MSAFREE:def 2;
suppose x' <> k1+1;
then rq.x' = (roots q1).x' by A16,A17,A24,A30,A32,A33,A35,A36;
hence rq.x in coprod((the_arity_of av).x, the Sorts of SCS)
by A17,A24,A30,A34,A41,A50,MSAFREE1:3;
end;
end;
then [nt,roots qq] in REL(the Sorts of SCS) by A14,A25,A28,MSAFREE:5;
then nt ==> roots qq by A18,LANG1:def 1;
then reconsider q' as SubtreeSeq of nt by DTCONSTR:def 9;
eke = nt-tree q' by A13;
then reconsider eke' = eke as Element of TS(DTConMSA(the Sorts of SCS));
reconsider q'' = {} as FinSequence of NAT by FINSEQ_1:29;
q'' in dom e1 with-replacement (m',dom e2) by TREES_1:47;
then A57: not m' is_a_prefix_of q'' & eke.q'' = e1.q'' or
ex r being FinSequence of NAT st r in dom e2
& q'' = m'^r & eke.q'' = e2.r by TREES_2:def 12;
now
given r being FinSequence of NAT such that
A58: {} = m'^r;
m' = {} by A58,FINSEQ_1:48;
hence contradiction by TREES_1:4;
end;
then A59: eke.{} = [av,the carrier of IIG] by A3,A57,TREES_4:def 4;
now
take av;
the_result_sort_of av = v by A26,MSAFREE2:def 7;
hence ex o being OperSymbol of IIG st [o,the carrier of IIG] = eke.{}
& the_result_sort_of o = v by A59;
end;
then eke' in {a'' where a'' is Element of TS(DTConMSA(the Sorts
of SCS)): (ex x being set st x in (the Sorts of SCS).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};
then reconsider eke' as Element of (the Sorts of FreeEnv SCS).v
by A7,MSAFREE:def 12;
eke' in (the Sorts of FreeEnv SCS).v;
hence eke in (the Sorts of FreeEnv SCS).v;
end;
theorem Th8:
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]
proof
let IIG;
let A be locally-finite 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;
A1: FreeEnv A = FreeMSA the Sorts of A by MSAFREE2:def 8;
assume
A2: 1 < card e;
A3: e in (the Sorts of FreeMSA X).v by A1;
A4: FreeMSA X = MSAlgebra (# FreeSort(X), FreeOper(X) #) by MSAFREE:def 16;
A5: (FreeSort X).v = FreeSort(X, v) by MSAFREE:def 13;
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 12;
then consider a being Element of TS(DTConMSA(X)) such that
A6: a = e and
A7: (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 A3,A4,A5;
thus ex o being OperSymbol of IIG st e.{} = [o,the carrier of IIG]
by A2,A6,A7,PRE_CIRC:24;
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 OperSymbols of IIG by FUNCT_2:def 1;
Result(o,SCS)
= ((the Sorts of SCS) * the ResultSort of IIG).o by MSUALG_1:def 10
.= (the Sorts of SCS).((the ResultSort of IIG).o) by A1,FUNCT_1:23
.= (the Sorts of SCS).(the_result_sort_of o) by MSUALG_1:def 7;
hence (Den(o,SCS)).(o depends_on_in s) in (the Sorts of SCS)
.(the_result_sort_of o) by FUNCT_2:7;
end;
theorem Th10:
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;
A2: FreeEnv A = FreeMSA X by MSAFREE2:def 8;
A3:FreeMSA(X) = MSAlgebra (# FreeSort(X), FreeOper(X) #) by MSAFREE:def 16;
e in (the Sorts of FreeEnv A).v;
then e in FreeSort(X,v) by A2,A3,MSAFREE:def 13;
then reconsider tsg = e as Element of TS DTConMSA(X);
A4:NonTerminals(DTConMSA(X)) = [:the OperSymbols of IIG,{the carrier of IIG}:]
by MSAFREE:6;
the carrier of IIG in {the carrier of IIG} by TARSKI:def 1;
then reconsider nt = [action_at v,the carrier of IIG]
as NonTerminal of DTConMSA(X) by A4,ZFMISC_1:106;
consider ts being FinSequence of TS DTConMSA(X) such that
A5: tsg = nt-tree ts and nt ==> roots ts by A1,DTCONSTR:10;
take ts;
thus e = [action_at v,the carrier of IIG]-tree ts by A5;
end;
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;
coherence
proof
A1: FreeEnv A = FreeMSA the Sorts of A by MSAFREE2:def 8;
the Sorts of A is locally-finite by MSAFREE2:def 11;
then FreeEnv A is finitely-generated by A1,MSAFREE2:11;
then FreeEnv A is locally-finite by MSAFREE2:def 13;
then the Sorts of FreeEnv A is locally-finite by MSAFREE2:def 11;
hence (the Sorts of FreeEnv A).v is finite by PRE_CIRC:def 3;
end;
end;
defpred P[set] means not contradiction;
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
:Def4:
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;
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] };
consider t being Element of (the Sorts of FreeEnv A).v;
A1: card t in s;
A2: s is Subset of NAT from SubsetFD;
s is finite from FraenkelFinIm;
then reconsider s as finite non empty Subset of NAT by A1,A2;
take max s, s;
thus thesis;
end;
correctness;
end;
theorem Th11:
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
proof
let IIG;
let A be locally-finite non-empty MSAlgebra over IIG,
v be Element of IIG;
A1: FreeEnv A = FreeMSA the Sorts of A by MSAFREE2:def 8;
consider s being finite non empty Subset of NAT such that
A2: s = { card t where t is Element of (the Sorts of FreeEnv A).v
: not contradiction } and
A3: size(v,A) = max s by Def4;
reconsider Y = s as finite non empty real-membered set;
max Y in { card t where t is Element of (the Sorts of FreeEnv A).v
: not contradiction }
by A2,PRE_CIRC:def 1;
then consider e being Element of (the Sorts of FreeEnv A).v such that
A4: card e = max Y;
A5: e in (the Sorts of FreeEnv A).v;
A6: FreeEnv A = MSAlgebra (# FreeSort the Sorts of A,
FreeOper the Sorts of A #) by A1,MSAFREE:def 16;
then (the Sorts of FreeEnv A).v
= FreeSort(the Sorts of A, v) by MSAFREE:def 13;
then 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 A5,MSAFREE:def 12;
then consider a being Element of TS(DTConMSA(the Sorts of A)) such that
A7: a = e and
A8: (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;
thus size(v,A) = 1 implies
v in InputVertices IIG \/ SortsWithConstants IIG
proof
assume
A9: size(v,A) = 1;
now
assume not v in InputVertices IIG \/ SortsWithConstants IIG;
then A10: not v in InputVertices IIG & not v in
SortsWithConstants IIG
by XBOOLE_0:def 2;
the carrier of IIG = InputVertices IIG \/ InnerVertices IIG
by MSAFREE2:3;
then v in InnerVertices IIG by A10,XBOOLE_0:def 2;
then v in rng the ResultSort of IIG by MSAFREE2:def 3;
then consider x being set such that
A11: x in dom the ResultSort of IIG and
A12: v = (the ResultSort of IIG).x by FUNCT_1:def 5;
reconsider o = x as OperSymbol of IIG by A11;
not v in { v' where v' is SortSymbol of IIG : v' is
with_const_op } by A10,MSAFREE2:def 1;
then A13: not v is with_const_op;
per cases by A13,MSUALG_2:def 2;
suppose
A14: not ((the Arity of IIG).o = {});
the carrier of IIG in {the carrier of IIG} by TARSKI:def 1;
then A15: [o,the carrier of IIG] in
[:the OperSymbols of IIG,{the carrier of IIG}:]
by ZFMISC_1:106;
reconsider O =
[:the OperSymbols 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*;
DTConMSA(the Sorts of A) = DTConstrStr (# O, R #)
by MSAFREE:def 10;
then reconsider o' = [o,the carrier of IIG]
as Symbol of DTConMSA(the Sorts of A) by A15,XBOOLE_0:def 2;
o' in NonTerminals DTConMSA(the Sorts of A) by A15,MSAFREE:6;
then consider p being FinSequence of TS(DTConMSA(the Sorts of A))
such that
A16: o' ==> roots p by DTCONSTR:def 8;
reconsider op = o'-tree p as Element of TS(DTConMSA(the Sorts
of A)) by A16,DTCONSTR:def 4;
A17: op.{} = o' by TREES_4:def 4;
now
take o;
the_result_sort_of o = v by A12,MSUALG_1:def 7;
hence ex o being OperSymbol of IIG st
[o,the carrier of IIG] = op.{}
& the_result_sort_of o = v by A17;
end;
then op 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};
then A18: op in FreeSort(the Sorts of A, v) by MSAFREE:def
12;
A19: (the Sorts of FreeEnv A).(the_result_sort_of o)
= (FreeSort(the Sorts of A)).v by A6,A12,MSUALG_1:def 7
.= FreeSort(the Sorts of A, v) by MSAFREE:def 13;
then len p = len the_arity_of o by A1,A18,MSAFREE2:13;
then A20: dom p = dom the_arity_of o by FINSEQ_3:31;
reconsider e1 = op as finite DecoratedTree;
reconsider co = card e1 as real number;
reconsider e1 as Element of (the Sorts of FreeEnv A).v
by A12,A18,A19,MSUALG_1:def 7;
e1 in (the Sorts of FreeEnv A).v;
then A21: co in Y by A2;
{} in dom op by TREES_1:47;
then A22: [{},o'] in op by A17,FUNCT_1:8;
the_arity_of o <> {} by A14,MSUALG_1:def 6;
then A23: dom p <> {} by A20,FINSEQ_1:26;
consider q being DTree-yielding FinSequence such that
A24: p = q and
A25: dom op = tree(doms q) by TREES_4:def 4;
p <> {} by A23,FINSEQ_1:26;
then rng p <> {} by FINSEQ_1:27;
then A26: 1 in dom p by FINSEQ_3:34;
0 + 1 = 1;
then A27: <*0*> in dom op by A24,A25,A26,PRE_CIRC:17;
A28: <*0*> <> {} by TREES_1:4;
then consider i being Nat, T being DecoratedTree,
q being Node of T such that
A29: i < len p and
A30: T = p.(i+1) and
A31: <*0*> = <*i*>^q by A27,TREES_4:11;
op.<*0*> = T.q by A29,A30,A31,TREES_4:12;
then [<*0*>,T.q] in op by A27,FUNCT_1:8;
then A32: { [{},o'], [<*0*>,T.q] } c= op by A22,ZFMISC_1:38
;
[{},o'] <> [<*0*>,T.q] by A28,ZFMISC_1:33;
then card { [{},o'], [<*0*>,T.q] } = 2 by CARD_2:76;
then 2 <= co by A32,CARD_1:80;
then co > size(v,A) by A9,AXIOMS:22;
hence contradiction by A3,A21,PRE_CIRC:def 1;
suppose not ((the ResultSort of IIG).o = v);
hence contradiction by A12;
end;
hence v in InputVertices IIG \/ SortsWithConstants IIG;
end;
assume
A33: v in InputVertices IIG \/ SortsWithConstants IIG;
per cases by A33,XBOOLE_0:def 2;
suppose v in InputVertices IIG;
then consider x being set such that
x in (the Sorts of A).v and
A34: a = root-tree[x,v] by A8,MSAFREE2:2;
root-tree[x,v] = {{}} --> [x,v] by TREES_1:56,TREES_4:def 2
.= [: {{}}, {[x,v]} :] by FUNCOP_1:def 2
.= { [{},[x,v]] } by ZFMISC_1:35;
hence size(v,A) = 1 by A3,A4,A7,A34,CARD_1:79;
suppose v in SortsWithConstants IIG;
then v in { v' where v' is SortSymbol of IIG : v' is with_const_op }
by MSAFREE2:def 1;
then consider v' being SortSymbol of IIG such that
A35: v' = v and
A36: v' is with_const_op;
consider o being OperSymbol of IIG such that
A37: (the Arity of IIG).o = {} and
A38: (the ResultSort of IIG).o = v' by A36,MSUALG_2:def 2;
now
per cases by A8;
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
A39: a = root-tree[x,v];
root-tree[x,v] = { [{},[x,v]] } by TREES_4:6;
hence size(v,A) = 1 by A3,A4,A7,A39,CARD_1:79;
suppose ex o' being OperSymbol of IIG st
[o',the carrier of IIG] = a.{} & the_result_sort_of o' = v;
then consider o' being OperSymbol of IIG such that
A40: [o',the carrier of IIG] = a.{} and
A41: the_result_sort_of o' = v;
the_result_sort_of o' = the_result_sort_of o
by A35,A38,A41,MSUALG_1:def 7;
then A42: o' = o by MSAFREE2:def 6;
A43: NonTerminals(DTConMSA(the Sorts of A))
= [:the OperSymbols of IIG,{the carrier of IIG}:] by MSAFREE:6;
the carrier of IIG in {the carrier of IIG} by TARSKI:def 1;
then reconsider nt = [o',the carrier of IIG]
as NonTerminal of DTConMSA(the Sorts of A) by A43,ZFMISC_1:106;
consider ts being FinSequence of TS(DTConMSA(the Sorts of A))
such that
A44: a = nt-tree ts and
nt ==> roots ts by A40,DTCONSTR:10;
reconsider ts as DTree-yielding FinSequence;
len ts = len the_arity_of o' by A1,A7,A41,A44,MSAFREE2:13
.= len {} by A37,A42,MSUALG_1:def 6
.= 0 by FINSEQ_1:25;
then ts = {} by FINSEQ_1:25;
then a = root-tree nt by A44,TREES_4:20
.= { [{},nt] } by TREES_4:6;
hence size(v,A) = 1 by A3,A4,A7,CARD_1:79;
end;
hence thesis;
end;
theorem
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)
proof
let IIG;
let SCS be locally-finite 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;
assume
A5: card e2 <> size(w,SCS);
consider sw being finite non empty Subset of NAT such that
A6: sw = { card t where t is Element of (the Sorts of FreeEnv SCS).w
: not contradiction } and
A7: size(w,SCS) = max sw by Def4;
reconsider Y = sw as finite non empty real-membered set;
card e2 in Y by A6;
then card e2 <= max Y by PRE_CIRC:def 1;
then A8: card e2 < max Y by A5,A7,REAL_1:def 5;
reconsider m = max Y as real number;
m in { card t where t is Element of (the Sorts of FreeEnv SCS).w
: not contradiction }
by A6,PRE_CIRC:def 1;
then consider e3 being Element of (the Sorts of FreeEnv SCS).w
such that
A9: card e3 = m;
consider sv being finite non empty Subset of NAT such that
A10: sv = { card t where t is Element of (the Sorts of FreeEnv SCS).v
: not contradiction } and
A11: size(v,SCS) = max sv by Def4;
reconsider Z = sv as finite non empty real-membered set;
reconsider q1' = q1 as Function;
consider k being set such that
A12: k in dom q1' and
A13: e2 = q1'.k by A4,FUNCT_1:def 5;
k in dom q1 by A12;
then reconsider kN = k as Nat;
reconsider k1 = kN - 1 as Nat by A12,FINSEQ_3:28;
A14: k1 + 1 = kN - (1-1) by XCMPLX_1:37
.= kN;
A15: kN <= len q1 by A12,FINSEQ_3:27;
k1 < kN by A14,REAL_1:69;
then A16: k1 < len q1 by A15,AXIOMS:22;
reconsider e1' = e1 as DecoratedTree;
consider p being DTree-yielding FinSequence such that
A17: p = q1 and
A18: dom e1' = tree(doms p) by A3,TREES_4:def 4;
reconsider k' = <*k1*> as Element of dom e1
by A12,A14,A17,A18,PRE_CIRC:17;
reconsider e3' = e3 as DecoratedTree;
reconsider k'' = k' as FinSequence of NAT;
reconsider eke = e1' with-replacement (k'', e3') as DecoratedTree;
reconsider eke as Element of (the Sorts of FreeEnv SCS).v by A1,A3,A12,A13,
A14,Th7;
A19: card eke in Z by A10;
A20: card(e1 with-replacement (k',e3)) + card (e1|k') = card e1 + card e3
by PRE_CIRC:23;
e1|k' = e2 by A3,A13,A14,A16,TREES_4:def 4;
then card e1 + card (e1|k') < card e1 + card e3 by A8,A9,REAL_1:53;
then card e1 < card (e1 with-replacement (k',e3)) by A20,AXIOMS:24;
hence contradiction by A2,A11,A19,PRE_CIRC:def 1;
end;
theorem Th13:
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
proof
let IIG;
let A be locally-finite non-empty MSAlgebra over IIG,
v be Vertex of IIG,
e be Element of (the Sorts of FreeEnv A).v;
A1: FreeEnv A = FreeMSA the Sorts of A by MSAFREE2:def 8;
assume that
A2: v in (InnerVertices IIG \ SortsWithConstants IIG) and
A3: card e = size(v,A);
FreeEnv A = MSAlgebra (# FreeSort the Sorts of A,
FreeOper the Sorts of A #) by A1,MSAFREE:def 16;
then (the Sorts of FreeEnv A).v
= FreeSort(the Sorts of A, v) by MSAFREE:def 13;
then e in FreeSort(the Sorts of A, v);
then 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 12;
then consider a being Element of TS(DTConMSA(the Sorts of A))
such that
A4: a = e and
A5: (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;
A6: v in InnerVertices IIG & not v in SortsWithConstants IIG
by A2,XBOOLE_0:def 4;
InputVertices IIG misses InnerVertices IIG by MSAFREE2:4;
then InputVertices IIG /\ InnerVertices IIG = {} by XBOOLE_0:def 7;
then not v in InputVertices IIG by A6,XBOOLE_0:def 3;
then not v in InputVertices IIG \/ SortsWithConstants IIG
by A6,XBOOLE_0:def 2;
then A7: card e <> 1 by A3,Th11;
reconsider e' = e as finite non empty set;
card e' <> 0 by CARD_2:59;
then 1 <= card e' by RLVECT_1:99;
then 1 < card e' by A7,REAL_1:def 5;
then consider o being OperSymbol of IIG such that
A8: e.{} = [o,the carrier of IIG] by Th8;
A9: NonTerminals(DTConMSA(the Sorts of A))
= [:the OperSymbols of IIG,{the carrier of IIG}:] by MSAFREE:6;
the carrier of IIG in {the carrier of IIG} by TARSKI:def 1;
then reconsider nt = [o,the carrier of IIG]
as NonTerminal of DTConMSA(the Sorts of A) by A9,ZFMISC_1:106;
consider ts being FinSequence of TS(DTConMSA(the Sorts of A))
such that
A10: a = nt-tree ts and
nt ==> roots ts by A4,A8,DTCONSTR:10;
reconsider q = ts as DTree-yielding FinSequence;
take q;
consider x being set such that
A11: 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;
now
assume a = root-tree[x,v];
then [o,the carrier of IIG] = [x,v] by A4,A8,TREES_4:3;
then A12: the carrier of IIG = v by ZFMISC_1:33;
for X be set holds not X in X;
hence contradiction by A12;
end;
then consider o' being OperSymbol of IIG such that
A13: [o',the carrier of IIG] = a.{} and
A14: the_result_sort_of o' = v by A11;
A15: v in InnerVertices IIG & not v in
SortsWithConstants IIG by A2,XBOOLE_0:def 4;
o = o' by A4,A8,A13,ZFMISC_1:33
.= action_at v by A14,A15,MSAFREE2:def 7;
hence thesis by A4,A10;
end;
theorem
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]
proof
let IIG;
let A be locally-finite non-empty MSAlgebra over IIG,
v be Vertex of IIG,
e be Element of (the Sorts of FreeEnv A).v such that
A1: v in (InnerVertices IIG \ SortsWithConstants IIG)
& card e = size(v,A);
consider q being DTree-yielding FinSequence such that
A2: e = [action_at v,the carrier of IIG]-tree q by A1,Th13;
take action_at v;
thus thesis by A2,TREES_4:def 4;
end;
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
:Def5: ex e' being Element of (the Sorts of FreeMSA the Sorts of A).v st
e = e' & it = depth e';
existence
proof
reconsider e' = e as
Element of (the Sorts of FreeMSA the Sorts of A).v by MSAFREE2:
def 8;
take depth e',e';
thus thesis;
end;
correctness;
end;
theorem Th15:
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)
proof
let IIG;
let A be locally-finite non-empty MSAlgebra over IIG,
v, w be Element of IIG;
A1: FreeEnv A = FreeMSA the Sorts of A by MSAFREE2:def 8;
assume that
A2: v in InnerVertices IIG and
A3: w in rng the_arity_of action_at v;
reconsider av = action_at v as OperSymbol of IIG;
consider x being set such that
A4: x in dom (the_arity_of av) and
A5: w = (the_arity_of av).x by A3,FUNCT_1:def 5;
reconsider k = x as Nat by A4;
consider sv being finite non empty Subset of NAT such that
A6: sv = { card tv where tv is Element of (the Sorts of FreeEnv A).v
: not contradiction } and
A7: size(v,A) = max sv by Def4;
reconsider Yv = sv as finite non empty real-membered set;
max Yv in Yv by PRE_CIRC:def 1;
then consider tv being Element of (the Sorts of FreeEnv A).v such that
A8: card tv = max Yv by A6;
reconsider e1 = tv as finite DecoratedTree;
now
assume v in SortsWithConstants IIG;
then v in { v' where v' is SortSymbol of IIG : v' is with_const_op }
by MSAFREE2:def 1;
then consider v' being SortSymbol of IIG such that
A9: v' = v and
A10: v' 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 = v' by A10,MSUALG_2:def 2;
the_result_sort_of oo = v by A9,A12,MSUALG_1:def 7
.= the_result_sort_of av by A2,MSAFREE2:def 7;
then A13: av = oo by MSAFREE2:def 6;
reconsider aoo = (the Arity of IIG).oo as FinSequence by A11;
dom aoo = {} by A11,FINSEQ_1:26;
hence contradiction by A4,A13,MSUALG_1:def 6;
end;
then A14: v in (InnerVertices IIG \ SortsWithConstants IIG)
by A2,XBOOLE_0:def 4;
then consider p being DTree-yielding FinSequence such that
A15: tv = [av,the carrier of IIG]-tree p by A7,A8,Th13;
consider sw being finite non empty Subset of NAT such that
A16: sw = { card tw where tw is Element of (the Sorts of FreeEnv A).w
: not contradiction } and
A17: size(w,A) = max sw by Def4;
reconsider Yw = sw as finite non empty real-membered set;
max Yw in Yw by PRE_CIRC:def 1;
then consider tw being Element of (the Sorts of FreeEnv A).w such that
A18: card tw = max Yw by A16;
reconsider e2 = tw as finite DecoratedTree;
consider p' being DTree-yielding FinSequence such that
A19: p' = p and
A20: dom e1 = tree(doms p') by A15,TREES_4:def 4;
A21: (the Sorts of FreeEnv A).v
= (the Sorts of FreeEnv A).(the_result_sort_of av)
by A2,MSAFREE2:def 7;
then len p = len the_arity_of av by A1,A15,MSAFREE2:13;
then A22: k in dom p by A4,FINSEQ_3:31;
reconsider k1 = k - 1 as Nat by A4,FINSEQ_3:28;
A23: k1 + 1 = k - (1-1) by XCMPLX_1:37
.= k;
reconsider o = <*k1*> as FinSequence of NAT;
reconsider o as Element of dom e1 by A19,A20,A22,A23,PRE_CIRC:17;
reconsider eoe = e1 with-replacement (o,e2) as finite Function;
reconsider de1 = dom e1 as finite Tree;
reconsider de2 = dom e2 as finite Tree;
reconsider o as Element of de1;
A24: dom eoe = de1 with-replacement (o,de2) by TREES_2:def 12;
then reconsider deoe = dom eoe as finite Tree;
p.k in (the Sorts of FreeEnv A).((the_arity_of av).k)
by A1,A4,A15,A21,MSAFREE2:14;
then reconsider eoe as Element of (the Sorts of FreeEnv A).v by A5,A14,
A15,A22,A23,Th7;
card eoe in Yv by A6;
then A25: card eoe <= size(v,A) by A7,PRE_CIRC:def 1;
A26: card deoe + card (de1|o) = card de1 + card de2 by A24,PRE_CIRC:22;
o <> {} by TREES_1:4;
then card (de1|o) < card de1 by PRE_CIRC:20;
then card (de1|o) + card de2 < card deoe + card (de1|o) by A26,REAL_1:53
;
then card de2 < card deoe by AXIOMS:24;
then A27: card e2 < card deoe by PRE_CIRC:21;
card deoe <= size(v,A) by A25,PRE_CIRC:21;
hence size(w,A) < size(v,A) by A17,A18,A27,AXIOMS:22;
end;
theorem Th16:
for IIG
for A being locally-finite non-empty MSAlgebra over IIG,
v being SortSymbol of IIG
holds size(v,A) > 0
proof
let IIG;
let A be locally-finite non-empty MSAlgebra over IIG,
v be SortSymbol of IIG;
consider s being finite non empty Subset of NAT such that
A1: s = { card t where t is Element of (the Sorts of FreeEnv A).v
: not contradiction } and
A2: size(v,A) = max s by Def4;
reconsider Y = s as finite non empty real-membered set;
max Y in { card t where t is Element of (the Sorts of FreeEnv A).v
: not contradiction } by A1,PRE_CIRC:def 1;
then consider t being Element of (the Sorts of FreeEnv A).v such that
A3: card t = max Y;
size(v,A) <> 0 by A2,A3,CARD_2:59;
hence size(v,A) > 0 by NAT_1:19;
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 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 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);
A4: FreeEnv A = FreeMSA the Sorts of A by MSAFREE2:def 8;
consider s being finite non empty Subset of NAT such that
A5: s = { card t where t is Element of (the Sorts of FreeEnv A).v
: not contradiction } and
A6: size(v,A) = max s by Def4;
reconsider S = s as finite non empty real-membered set;
A7: card e in S by A5;
now let r be real number;
FreeEnv A = MSAlgebra (# FreeSort the Sorts of A,
FreeOper the Sorts of A #) by A4,MSAFREE:def 16;
then A8: (the Sorts of FreeEnv A).v
= FreeSort(the Sorts of A,v) by MSAFREE:def 13;
reconsider e' = e as finite set;
card e' <> 0 by CARD_2:59;
then A9: 1 <= card e' by RLVECT_1:99;
assume r in S;
then consider t being Element of (the Sorts of FreeEnv A).v
such that
A10: r = card t by A5;
t in FreeSort(the Sorts of A, v) by A8;
then 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 12;
then consider a' being Element of TS(DTConMSA(the Sorts of A))
such that
A11: a' = t and
A12: (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;
per cases by A12;
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
A13: x in (the Sorts of A).v & a' = root-tree[x,v];
root-tree[x,v] = { [{},[x,v]] } by TREES_4:6;
hence r <= card e by A9,A10,A11,A13,CARD_1:79;
suppose ex o being OperSymbol of IIG st [o,the carrier of IIG] = a'.{}
& the_result_sort_of o = v;
then consider o being OperSymbol of IIG such that
A14: [o,the carrier of IIG] = a'.{} & the_result_sort_of o = v;
a'.{} = [action_at v,the carrier of IIG] by A1,A14,MSAFREE2:def 7;
then consider q being DTree-yielding FinSequence such that
A15: t = [action_at v,the carrier of IIG]-tree q
by A11,Th10;
deffunc F(Nat) = p +* (q|Seg $1);
consider T being FinSequence such that
len T = len p and
A16: for k being Nat st k in Seg len p holds T.k = F(k) from SeqLambda;
A17: dom p = Seg len p by FINSEQ_1:def 3;
A18: the_result_sort_of action_at v = v by A1,MSAFREE2:def 7;
now per cases;
suppose len q = 0;
then q = {} by FINSEQ_1:25;
then t = root-tree [action_at v,the carrier of IIG] by A15,TREES_4:20;
hence r <= card e by A9,A10,PRE_CIRC:24;
suppose
A19: len q <> 0;
A20: len p = len the_arity_of action_at v by A2,A4,A18,MSAFREE2:13;
then A21: len p = len q by A4,A15,A18,MSAFREE2:13;
then A22: dom p = dom q by FINSEQ_3:31;
A23: dom p = dom the_arity_of action_at v by A20,FINSEQ_3:31;
A24: 1+0 <= len p by A19,A21,RLVECT_1:99;
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;
A25: P[0] by FINSEQ_3:27;
A26: now let k be Nat;
assume
A27: P[k];
thus P[k+1]
proof
assume
A28: k+1 in dom p;
let qk1 be DTree-yielding FinSequence such that
A29: qk1 = T.(k+1);
let tk1 be finite set; assume
A30: tk1 = [action_at v,the carrier of IIG]-tree qk1;
then reconsider treek1 = tk1 as finite DecoratedTree;
reconsider tree0 = [action_at v,the carrier of IIG]-tree p
as finite DecoratedTree by A2;
per cases;
suppose
A31: k = 0;
set v1 = (the_arity_of action_at v)/.1;
A32: 1 in dom p by A24,FINSEQ_3:27;
then consider e1 being Element of (the Sorts of FreeEnv A).v1
such that
A33: e1 = p.1 and
A34: card e1 = size (v1, A) by A3;
consider s1 being finite non empty Subset of NAT such that
A35: s1 = { card t1 where t1 is
Element of (the Sorts of FreeEnv A).v1 :
not contradiction } and
A36: card e1 = max s1 by A34,Def4;
reconsider S1 = s1 as finite non empty real-membered set;
A37: 1 in dom the_arity_of action_at v by A20,A24,FINSEQ_3:27;
A38: 1 in dom p by A24,FINSEQ_3:27;
A39: 1 in Seg 1 by FINSEQ_1:5;
then A40: 1 in dom(q|Seg 1) by A22,A32,RELAT_1:86;
A41: qk1.1 = (p +* (q|Seg 1)).1 by A16,A17,A29,A31,A38
.= (q|Seg 1).1 by A40,FUNCT_4:14
.= q.1 by A39,FUNCT_1:72;
dom qk1 = dom(p +* (q|Seg 1)) by A16,A17,A29,A31,A38
.= dom p \/ dom(q|Seg 1) by FUNCT_4:def 1
.= dom p \/ dom q /\ Seg 1 by RELAT_1:90
.= dom p by A22,XBOOLE_1:22;
then A42: len qk1 = len p by FINSEQ_3:31;
q.1 in
(the Sorts of FreeEnv A).((the_arity_of action_at v).1)
by A4,A15,A18,A37,MSAFREE2:14;
then reconsider T1 = q.1 as
Element of (the Sorts of FreeEnv A).v1 by A37,FINSEQ_4:def 4;
card T1 in S1 by A35;
then A43: card T1 <= card e1 by A36,PRE_CIRC:def 1;
reconsider Tx = p.1 as finite DecoratedTree by A33;
A44: {} is Element of dom Tx by TREES_1:47;
A45: 0 < len p by A24,NAT_1:38;
A46: Tx =p.(0+1);
<*0*> = <*0*>^{} by FINSEQ_1:47;
then reconsider w0 = <*0*> as Element of dom tree0 by A44,A45,A46,
TREES_4:11;
A47: tree0|w0 = e1 by A33,A45,A46,TREES_4:def 4;
consider q0 being DTree-yielding FinSequence such that
A48: e with-replacement (w0,T1) =
[action_at v,the carrier of IIG]-tree q0 and
A49: len q0 = len p and
A50: q0.(0+1) = T1 and
A51: for i being Nat st i in dom p & i <> 0+1 holds q0.i = p.i
by A2,PRE_CIRC:19;
now let k be Nat;
assume 1 <= k & k <= len q0;
then A52: k in dom p by A49,FINSEQ_3:27;
per cases;
suppose
k = 1;
hence q0.k = qk1.k by A41,A50;
suppose
A53: k <> 1;
then A54: not k in Seg 1 by FINSEQ_1:4,TARSKI:def 1;
dom(q|Seg 1) = dom q /\ Seg 1 by RELAT_1:90;
then A55: not k in dom(q|Seg 1) by A54,XBOOLE_0:def 3;
thus qk1.k = (p +* (q|Seg 1)).k by A16,A17,A29,A31,A38
.= p.k by A55,FUNCT_4:12
.=q0.k by A51,A52,A53;
end;
then treek1 = tree0 with-replacement (w0,T1)
by A2,A30,A42,A48,A49,FINSEQ_1:18;
then card treek1 + card (tree0|w0) = card tree0 + card T1
by PRE_CIRC:23;
hence card tk1 <= card e by A2,A43,A47,REAL_1:67;
suppose k <> 0;
then A56: k >= 1 by RLVECT_1:99;
A57: k+1 <= len p by A28,FINSEQ_3:27;
then A58: k < len p by NAT_1:38;
then A59: k in dom p by A56,FINSEQ_3:27;
A60: k+1 >= 1 by NAT_1:29;
T.k = p +* (q|Seg k) by A16,A17,A59;
then reconsider qk = T.k as Function;
A61: dom qk1 = dom(p +* (q|Seg(k+1))) by A16,A17,A28,A29
.= dom p \/ dom(q|Seg(k+1)) by FUNCT_4:def 1
.= dom p \/ dom q /\ Seg(k+1) by RELAT_1:90
.= dom p by A22,XBOOLE_1:22;
A62: dom qk = dom(p +* (q|Seg k)) by A16,A17,A59
.= dom p \/ dom(q|Seg k) by FUNCT_4:def 1
.= dom p \/ dom q /\ Seg k by RELAT_1:90
.= 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;
A63: for x being set st x in dom qk holds qk.x is finite DecoratedTree
proof
let x be set;
assume
A64: x in dom qk;
then reconsider n = x as Nat;
set v1 = (the_arity_of action_at v)/.n;
qk.n = q.n or qk.n = p.n
proof per cases;
suppose
A65: n <= k;
n>=1 by A64,FINSEQ_3:27;
then A66: n in Seg k by A65,FINSEQ_1:3;
dom(q|Seg k) = dom q /\ Seg k by RELAT_1:90;
then A67: n in dom(q|Seg k) by A22,A62,A64,A66,
XBOOLE_0:def 3;
qk.n = (p +* (q|Seg k)).n by A16,A17,A59
.= (q|Seg k).n by A67,FUNCT_4:14
.= q.n by A67,FUNCT_1:70;
hence thesis;
suppose n > k;
then A68: not n in Seg k by FINSEQ_1:3;
dom(q|Seg k) = dom q /\ Seg k by RELAT_1:90;
then A69: not n in dom(q|Seg k) by A68,XBOOLE_0:def
3;
qk.n = (p +* (q|Seg k)).n by A16,A17,A59
.= p.n by A69,FUNCT_4:12;
hence thesis;
end;
then qk.n in
(the Sorts of FreeEnv A).
((the_arity_of action_at v).n) by A2,A4,A15,A18,A23,A62,A64,
MSAFREE2:14;
then reconsider T1 = qk.n as
Element of (the Sorts of FreeEnv A).v1 by A23,A62,A64,FINSEQ_4:def
4;
T1 in (the Sorts of FreeEnv A).v1;
hence qk.x is finite DecoratedTree;
end;
then for x being set st x in dom qk holds qk.x is DecoratedTree;
then reconsider qk as DTree-yielding FinSequence by TREES_3:26;
set v1 = (the_arity_of action_at v)/.(k+1);
now let x be set;
assume x in dom doms qk;
then A70: x in dom qk by TREES_3:39;
then reconsider T1 = qk.x as finite DecoratedTree by A63;
dom T1 is finite Tree;
hence (doms qk).x is finite Tree by A70,FUNCT_6:31;
end;
then reconsider qkf = doms qk as FinTree-yielding FinSequence by
TREES_3:25;
A71: 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 A71,AMI_1:21;
A72: card tk <= card e by A27,A56,A58,FINSEQ_3:27;
consider e1 being Element of (the Sorts of FreeEnv A).v1
such that
A73: e1 = p.(k+1) and
A74: card e1 = size (v1, A) by A3,A28;
A75: not k+1 in Seg k by FINSEQ_3:9;
dom(q|Seg k) = dom q /\ Seg k by RELAT_1:90;
then A76: not k+1 in dom(q|Seg k) by A75,XBOOLE_0:def 3;
A77: qk.(k+1) = (p +* (q|Seg k)).(k+1) by A16,A17,A59
.= p.(k+1) by A76,FUNCT_4:12;
A78: k+1 in dom the_arity_of action_at v by A20,A57,A60,FINSEQ_3:27;
then A79: p.(k+1) in
(the Sorts of FreeEnv A).
((the_arity_of action_at v).(k+1)) by A2,A4,A18,MSAFREE2:14;
A80: v1 = (the_arity_of action_at v).(k+1) by A78,FINSEQ_4:def 4;
reconsider T1 = p.(k+1) as
Element of (the Sorts of FreeEnv A).v1 by A78,A79,FINSEQ_4:def 4;
T1 in (the Sorts of FreeEnv A).v1;
then reconsider Tx = qk.(k+1) as finite DecoratedTree
by A77;
consider s1 being finite non empty Subset of NAT such that
A81: s1 = { card t1 where t1 is
Element of (the Sorts of FreeEnv A).v1 :
not contradiction } and
A82: card e1 = max s1 by A74,Def4;
reconsider S1 = s1 as finite non empty real-membered set;
A83: k+1 in Seg(k+1) by FINSEQ_1:5;
then A84: k+1 in dom(q|Seg(k+1)) by A22,A28,RELAT_1:86;
A85: qk1.(k+1) = (p +* (q|Seg(k+1))).(k+1) by A16,A17,A28,A29
.= (q|Seg(k+1)).(k+1) by A84,FUNCT_4:14
.= q.(k+1) by A83,FUNCT_1:72;
A86: len qk1 = len p by A61,FINSEQ_3:31;
reconsider T1 = q.(k+1) as
Element of (the Sorts of FreeEnv A).v1 by A4,A15,A18,A78,A80,
MSAFREE2:14;
card T1 in S1 by A81;
then A87: card T1 <= card e1 by A82,PRE_CIRC:def 1;
A88: {} is Element of dom Tx by TREES_1:47;
A89: len qk = len p by A62,FINSEQ_3:31;
A90: k < len qk by A58,A62,FINSEQ_3:31;
A91: <*k*> = <*k*>^{} by FINSEQ_1:47;
then A92: <*k*> in dom tk by A58,A88,A89,TREES_4:11;
reconsider w0 = <*k*> as Element of dom tk by A88,A90,A91,TREES_4:11;
A93: tk|w0 = e1 by A58,A73,A77,A89,TREES_4:def 4;
consider q0 being DTree-yielding FinSequence such that
A94: tk with-replacement (<*k*>,T1) =
[action_at v,the carrier of IIG]-tree q0 and
A95: len q0 = len qk and
A96: q0.(k+1) = T1 and
A97: for i being Nat st i in dom qk & i <> k+1 holds q0.i = qk.i
by A92,PRE_CIRC:19;
now let n be Nat;
assume
A98: 1 <= n & n <= len q0;
then A99: n in dom qk by A95,FINSEQ_3:27;
per cases by REAL_1:def 5;
suppose
n = k+1;
hence q0.n = qk1.n by A85,A96;
suppose
A100: n > k+1;
then A101: not n in Seg(k+1) by FINSEQ_1:3;
dom(q|Seg(k+1)) = dom q /\ Seg(k+1) by RELAT_1:90;
then A102: not n in dom(q|Seg(k+1)) by A101,XBOOLE_0:def 3;
k+1 >= k by NAT_1:29;
then n > k by A100,AXIOMS:22;
then A103: not n in Seg k by FINSEQ_1:3;
dom(q|Seg k) = dom q /\ Seg k by RELAT_1:90;
then A104: not n in dom(q|Seg k) by A103,XBOOLE_0:def 3;
thus qk1.n = (p +* (q|Seg(k+1))).n by A16,A17,A28,A29
.= p.n by A102,FUNCT_4:12
.= (p +* (q|Seg k)).n by A104,FUNCT_4:12
.= qk.n by A16,A17,A59
.= q0.n by A97,A99,A100;
suppose
A105: n < k+1;
then A106: n in Seg(k+1) by A98,FINSEQ_1:3;
A107: n in dom q by A21,A89,A95,A98,FINSEQ_3:27;
dom(q|Seg(k+1)) = dom q /\ Seg(k+1) by RELAT_1:90;
then A108: n in dom(q|Seg(k+1)) by A106,A107,XBOOLE_0:def
3;
n <= k by A105,NAT_1:38;
then A109: n in Seg k by A98,FINSEQ_1:3;
dom(q|Seg k) = dom q /\ Seg k by RELAT_1:90;
then A110: n in dom(q|Seg k) by A107,A109,XBOOLE_0:def 3;
thus qk1.n = (p +* (q|Seg(k+1))).n by A16,A17,A28,A29
.= (q|Seg(k+1)).n by A108,FUNCT_4:14
.= q.n by A108,FUNCT_1:70
.= (q|Seg k).n by A110,FUNCT_1:70
.= (p +* (q|Seg k)).n by A110,FUNCT_4:14
.= qk.n by A16,A17,A59
.= q0.n by A97,A99,A105;
end;
then treek1 = tk with-replacement (w0,T1)
by A30,A86,A89,A94,A95,FINSEQ_1:18;
then card treek1 + card (tk|w0) = card tk + card T1
by PRE_CIRC:23;
then card tk1 <= card tk by A87,A93,REAL_1:67;
hence card tk1 <= card e by A72,AXIOMS:22;
end;
end;
A111: for k be Nat holds P[k] from Ind(A25,A26);
dom p = Seg len p by FINSEQ_1:def 3;
then A112: dom p = dom q by A21,FINSEQ_1:def 3;
A113: len p in dom p by A24,FINSEQ_3:27;
then T.len p = p +* (q|dom p) by A16,A17
.= p +* q by A112,RELAT_1:98
.= q by A22,FUNCT_4:20;
hence r <= card e by A10,A15,A111,A113;
end;
hence r <= card e;
end;
then card e = max S by A7,PRE_CIRC:def 1;
hence thesis by A6;
end;
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
:Def6:
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;
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]};
consider t being Element of (the Sorts of FreeEnv A).v;
A1: depth t in s;
A2: s is Subset of NAT from SubsetFD;
s is finite from FraenkelFinIm;
then reconsider s as finite non empty Subset of NAT by A1,A2;
take max s, 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 -> natural number 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 number;
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;
consider v being Element of IIG;
A2: depth(v,A) in Ds;
A3: the carrier of IIG is finite by GROUP_1:def 13;
Ds is finite from FraenkelFin (A3);
then reconsider Ds as finite non empty Subset of NAT
by A1,A2,MEMBERED:5;
take max Ds, 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(v',A) where v' is Element of IIG :
v' 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 depth(v,A) <= depth A by A2,PRE_CIRC:def 1;
end;
theorem Th19:
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 = { depth t where t is Element of (the Sorts of FreeEnv A).v
: not contradiction } and
A2: depth(v,A) = max s by Def6;
reconsider Y = s as finite non empty real-membered set;
max Y in { depth t where t is Element of (the Sorts of FreeEnv A).v
: not contradiction } by A1,PRE_CIRC:def 1;
then consider t being Element of (the Sorts of FreeEnv A).v such that
A3: depth t = max Y;
consider t2 being Element of (the Sorts of FreeMSA the Sorts of A).v
such that
A4: t = t2 and
A5: depth t = depth t2 by Def5;
consider dt being finite DecoratedTree, t' being finite Tree such that
A6: dt = t2 and
A7: t' = dom dt and
A8: depth t2 = height t' by MSAFREE2:def 14;
consider p being FinSequence of NAT such that
A9: p in t' and
A10: len p = height t' by TREES_1:def 15;
consider ss being finite non empty Subset of NAT such that
A11: ss = { card tt where tt is Element of (the Sorts of FreeEnv A).v
: not contradiction } and
A12: size(v,A) = max ss by Def4;
reconsider YY = ss as finite non empty real-membered set;
reconsider t'' = t as Function;
thus depth(v,A) = 0 implies
v in InputVertices IIG or v in SortsWithConstants IIG
proof
assume
A13: depth(v,A) = 0;
then A14: t' = { {} } by A2,A3,A5,A8,TREES_1:56,80;
then rng t'' = { t.{} } by A4,A6,A7,FUNCT_1:14;
then t'' = { [{},t.{}] } by A4,A6,A7,A14,PRE_CIRC:2;
then card t = 1 by CARD_1:79;
then A15: 1 in YY by A11;
for kk being real number st kk in YY holds kk <= 1
proof
let kk be real number;
assume kk in YY;
then consider tt being Element of (the Sorts of FreeEnv A).v
such that
A16: card tt = kk by A11;
depth tt in Y by A1;
then depth tt <= 0 by A2,A13,PRE_CIRC:def 1;
then depth tt < 0 + 1 by NAT_1:38;
then A17: depth tt = 0 by RLVECT_1:98;
consider tiv being Element of (the Sorts of FreeMSA the Sorts of A).v
such that
A18: tt = tiv and
A19: depth tt = depth tiv by Def5;
consider dt' being finite DecoratedTree,
t''' being finite Tree such that
A20: dt' = tiv and
A21: t''' = dom dt' and
A22: depth tiv = height t''' by MSAFREE2:def 14;
A23: t''' = { {} } by A17,A19,A22,TREES_1:56,80;
then rng tt = { tt.{} } by A18,A20,A21,FUNCT_1:14;
then tt = { [{},tt.{}] } by A18,A20,A21,A23,PRE_CIRC:2;
hence kk <= 1 by A16,CARD_1:79;
end;
then size(v,A) = 1 by A12,A15,PRE_CIRC:def 1;
then v in InputVertices IIG \/ SortsWithConstants IIG
by Th11;
hence v in InputVertices IIG or v in SortsWithConstants IIG
by XBOOLE_0:def 2;
end;
assume v in InputVertices IIG or v in SortsWithConstants IIG;
then v in InputVertices IIG \/ SortsWithConstants IIG by XBOOLE_0:def
2;
then A24: size(v,A) = 1 by Th11;
A25: card t in ss by A11;
reconsider ct = card t as Real;
ct <= 1 by A12,A24,A25,PRE_CIRC:def 1;
then A26: card t <= 0 or card t = 0 + 1 by NAT_1:26;
now
assume card t <= 0;
then card t < 0 + 1 by NAT_1:38;
then card t = 0 by RLVECT_1:98;
hence contradiction by CARD_2:59;
end;
then consider x being set such that
A27: t = {x} by A26,CARD_2:60;
{} in dom t by TREES_1:47;
then consider y being set such that
A28: [{},y] in t'' by RELAT_1:def 4;
A29: x = [{},y] by A27,A28,TARSKI:def 1;
consider y'' being set such that
A30: [p,y''] in t'' by A4,A6,A7,A9,RELAT_1:def 4;
[p,y''] = [{},y] by A27,A29,A30,TARSKI:def 1;
then p = {} by ZFMISC_1:33;
hence depth(v,A) = 0 by A2,A3,A5,A8,A10,FINSEQ_1:25;
end;
theorem
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)
proof
let IIG;
let A be locally-finite non-empty MSAlgebra over IIG,
v, v1 be SortSymbol of IIG;
A1: FreeEnv A = FreeMSA the Sorts of A by MSAFREE2:def 8;
assume that
A2: v in InnerVertices IIG and
A3: v1 in rng the_arity_of action_at v;
consider s being finite non empty Subset of NAT such that
A4: s = { depth t where t is Element of (the Sorts of FreeEnv A).v
: not contradiction } and
A5: depth(v,A) = max s by Def6;
reconsider Y = s as finite non empty real-membered set;
max Y in { depth t where t is Element of (the Sorts of FreeEnv A).v
: not contradiction } by A4,PRE_CIRC:def 1;
then consider t being Element of (the Sorts of FreeEnv A).v such that
A6: depth t = max Y;
consider s1 being finite non empty Subset of NAT such that
A7: s1 = { depth t1 where t1 is Element of (the Sorts of FreeEnv A).v1
: not contradiction } and
A8: depth(v1,A) = max s1 by Def6;
reconsider Y1 = s1 as finite non empty real-membered set;
max Y1 in { depth t1 where t1 is Element of (the Sorts of FreeEnv A).v1
: not contradiction } by A7,PRE_CIRC:def 1;
then consider t1 being Element of (the Sorts of FreeEnv A).v1 such that
A9: depth t1 = max Y1;
consider e' being Element of (the Sorts of FreeMSA the Sorts of A).v1
such that
A10: t1 = e' and
A11: depth t1 = depth e' by Def5;
consider dt1' being finite DecoratedTree, t1' being finite Tree
such that
A12: dt1' = e' and
A13: t1' = dom dt1' and
A14: depth e' = height t1' by MSAFREE2:def 14;
A15: size(v1,A) < size(v,A) by A2,A3,Th15;
size(v1,A) > 0 by Th16;
then 0 + 1 <= size(v1,A) by NAT_1:38;
then not v in InputVertices IIG \/ SortsWithConstants IIG by A15,Th11;
then A16: not v in InputVertices IIG & not v in SortsWithConstants
IIG
by XBOOLE_0:def 2;
then A17: v in (InnerVertices IIG \ SortsWithConstants IIG) by A2,
XBOOLE_0:def 4
;
FreeEnv A = MSAlgebra (# FreeSort the Sorts of A,
FreeOper the Sorts of A #) by A1,MSAFREE:def 16;
then (the Sorts of FreeEnv A).v
= FreeSort(the Sorts of A,v) by MSAFREE:def 13;
then t in FreeSort(the Sorts of A,v);
then 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 12;
then consider a being Element of TS(DTConMSA(the Sorts of A))
such that
A18: a = t and
A19: (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;
now
given x being set such that
x in (the Sorts of A).v and
A20: a = root-tree[x,v];
consider e' being Element of (the Sorts of FreeMSA the Sorts of A).v
such that
A21: t = e' and
A22: depth t = depth e' by Def5;
consider dta being finite DecoratedTree, ta being finite Tree
such that
A23: dta = e' and
A24: ta = dom dta and
A25: depth e' = height ta by MSAFREE2:def 14;
depth t = 0 by A18,A20,A21,A22,A23,A24,A25,TREES_1:79,TREES_4:3;
hence contradiction by A5,A6,A16,Th19;
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 A19;
A28: NonTerminals(DTConMSA(the Sorts of A))
= [:the OperSymbols of IIG,{the carrier of IIG}:] by MSAFREE:6;
the carrier of IIG in {the carrier of IIG} by TARSKI:def 1;
then reconsider o' = [o,the carrier of IIG]
as NonTerminal of DTConMSA(the Sorts of A) by A28,ZFMISC_1:106;
consider q being FinSequence of TS(DTConMSA(the Sorts of A)) such that
A29: a = o'-tree q and
o' ==> roots q by A26,DTCONSTR:10;
consider q' being DTree-yielding FinSequence such that
A30: q = q' and
A31: dom a = tree(doms q') by A29,TREES_4:def 4;
reconsider av = action_at v as OperSymbol of IIG;
consider x being set such that
A32: x in dom the_arity_of av and
A33: v1 = (the_arity_of av).x by A3,FUNCT_1:def 5;
reconsider k = x as Nat by A32;
A34: o = av by A2,A27,MSAFREE2:def 7;
then A35: len q' = len the_arity_of av by A1,A18,A27,A29,A30,MSAFREE2:13;
then A36: dom q' = dom the_arity_of av by FINSEQ_3:31;
A37: k in dom q' by A32,A35,FINSEQ_3:31;
reconsider k1 = k - 1 as Nat by A32,FINSEQ_3:28;
A38: k1 + 1 = k - (1-1) by XCMPLX_1:37
.= k;
then A39: <*k1*> in tree(doms q') by A32,A36,PRE_CIRC:17;
reconsider f = <*k1*> as FinSequence of NAT;
consider qq being DTree-yielding FinSequence such that
A40: t with-replacement (f,t1) = o'-tree qq and
A41: len qq = len q' and
qq.(k1+1) = t1 and
for i being Nat st i in dom q' & i <> k1+1 holds qq.i = q'.i
by A18,A29,A30,A31,A39,PRE_CIRC:19;
A42: q'.k in (the Sorts of FreeEnv A).v1
by A1,A18,A27,A29,A30,A32,A33,A34,MSAFREE2:14;
reconsider tft = t with-replacement (f,t1) as DecoratedTree;
t = [av,the carrier of IIG]-tree q' by A2,A18,A27,A29,A30,MSAFREE2:def 7;
then reconsider tft as Element of (the Sorts of FreeEnv A).v by A17,A37,
A38,A42,Th7;
reconsider dtft = depth tft as Real;
dtft in Y by A4;
then A43: dtft <= depth t by A6,PRE_CIRC:def 1;
consider e' being Element of (the Sorts of FreeMSA the Sorts of A).v
such that
A44: tft = e' and
A45: depth tft = depth e' by Def5;
consider dttft being finite DecoratedTree, ttft being finite Tree
such that
A46: dttft = e' and
A47: ttft = dom dttft and
A48: depth e' = height ttft by MSAFREE2:def 14;
A49: k in dom qq by A32,A35,A41,FINSEQ_3:31;
consider qq' being DTree-yielding FinSequence such that
A50: qq = qq' and
A51: dom tft = tree(doms qq') by A40,TREES_4:def 4;
reconsider f' = f as Element of ttft by A38,A44,A46,A47,A49,A50,A51,
PRE_CIRC:17;
A52: f' <> {} by TREES_1:4;
A53: f' in dom t by A18,A31,A37,A38,PRE_CIRC:17;
dom tft = dom t with-replacement (f,dom t1) by A18,A31,A39,TREES_2:def
12;
then ttft|f = t1' by A10,A12,A13,A44,A46,A47,A53,TREES_1:66;
then depth t1 < depth tft by A11,A14,A45,A48,A52,TREES_1:85;
hence depth(v1,A) < depth(v,A) by A5,A6,A8,A9,A43,AXIOMS:22
;
end;