:: The Correspondence Between Monotonic Many Sorted Signatures
:: and Well-Founded Graphs. {P}art {I}
:: by Czes{\l}aw Byli\'nski and Piotr Rudnicki
::
:: Received February 14, 1996
:: Copyright (c) 1996-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, FINSET_1, FUNCT_1, RELAT_1, CARD_3, GRAPH_1, SUBSET_1,
TREES_2, FINSEQ_1, STRUCT_0, GRAPH_2, ARYTM_3, XXREAL_0, NAT_1, PARTFUN1,
TARSKI, ORDINAL4, XBOOLE_0, CARD_1, WAYBEL_0, GLIB_000, RELAT_2,
FUNCOP_1, ARYTM_1, TREES_4, TREES_1, MSUALG_1, PBOOLE, MSATERM, TREES_9,
ZFMISC_1, MSAFREE, MSUALG_2, MSAFREE2, MSUALG_3, PRELAMB, REALSET1,
GROUP_6, FUNCT_6, MARGREL1, UNIALG_2, DTCONSTR, TDGROUP, TREES_3,
TREES_A, MSSCYC_1, SETLIM_2;
notations TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, SUBSET_1, XCMPLX_0, CARD_1,
ORDINAL1, NUMBERS, NAT_1, FINSEQ_2, STRUCT_0, CARD_3, RELAT_1, FUNCT_1,
PARTFUN1, FUNCT_2, FINSET_1, FUNCOP_1, FINSEQ_1, GRAPH_1, FINSEQ_6,
GRAPH_2, TREES_1, TREES_2, TREES_3, FUNCT_6, TREES_4, LANG1, DTCONSTR,
PBOOLE, MSUALG_1, MSUALG_2, MSUALG_3, MSAFREE, MSAFREE2, TREES_9,
MSATERM, XXREAL_0, PRE_POLY;
constructors WELLORD2, FINSEQ_4, MSUALG_3, MSATERM, MSAFREE2, GRAPH_2,
RELSET_1, PRE_POLY, XTUPLE_0, FINSEQ_6;
registrations XBOOLE_0, RELAT_1, FUNCT_1, FINSET_1, XXREAL_0, XREAL_0, NAT_1,
INT_1, FINSEQ_1, PBOOLE, TREES_2, TREES_3, PRE_CIRC, TREES_9, STRUCT_0,
MSUALG_1, MSAFREE, MSAFREE2, EXTENS_1, ORDINAL1, CARD_1, GRAPH_1,
RELSET_1, TREES_1, MSATERM;
requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
definitions TARSKI, GRAPH_1, GRAPH_2, MSAFREE, PBOOLE, FINSET_1, MSUALG_3,
STRUCT_0;
equalities MSAFREE;
expansions TARSKI, GRAPH_1, GRAPH_2, MSAFREE, PBOOLE, FINSET_1, MSUALG_3;
theorems TARSKI, NAT_1, ZFMISC_1, GRAPH_1, GRAPH_2, FUNCOP_1, FUNCT_1,
FUNCT_2, FUNCT_6, FINSEQ_1, FINSEQ_2, FINSEQ_3, FINSEQ_4, FINSEQ_5,
CARD_1, CARD_3, TREES_1, TREES_3, TREES_4, PBOOLE, MSUALG_1, MSUALG_2,
MSUALG_3, MSAFREE, MSAFREE2, MSATERM, EXTENS_1, INT_1, XBOOLE_0,
XBOOLE_1, XREAL_1, XXREAL_0, PARTFUN1, RELAT_1, RELSET_1, XTUPLE_0,
FINSEQ_6;
schemes NAT_1, FRAENKEL, PBOOLE, DOMAIN_1;
begin :: Some properties of graphs and trees
reserve G for Graph,
k, m, n for Nat;
definition
let G be Graph;
redefine mode Chain of G means :: redefines Chain (GRAPH_1, definition)
:Def1:
it is FinSequence of the carrier' of G
& ex p being FinSequence of the carrier of G st p is_vertex_seq_of it;
compatibility
proof
let c be FinSequence;
hereby
assume
A1: c is Chain of G;
then consider p being FinSequence such that
A2: len p = len c + 1 and
A3: for n st 1 <= n & n <= len p holds p.n in the carrier of G and
A4: for n st 1 <= n & n <= len c ex x9, y9 being Element of the
carrier of G st x9 = p.n & y9 = p.(n+1) & c.n joins x9, y9 by GRAPH_1:def 14;
thus c is FinSequence of the carrier' of G by A1;
now
let i be Nat;
assume i in dom p;
then
A5: 1<=i & i<=len p by FINSEQ_3:25;
thus p.i in the carrier of G by A3,A5;
end;
then reconsider p as FinSequence of the carrier of G by FINSEQ_2:12;
take p;
thus p is_vertex_seq_of c
proof
thus len p = len c + 1 by A2;
let n;
assume that
A6: 1<=n and
A7: n<=len c;
n+1<=len p by A2,A7,XREAL_1:6;
then
A8: p/.(n+1)=p.(n+1) by FINSEQ_4:15,NAT_1:12;
n<=len p & ex x9, y9 being Element of the carrier of G st x9 = p.
n & y9 = p. (n+1) & c.n joins x9, y9 by A2,A4,A6,A7,NAT_1:12;
hence thesis by A6,A8,FINSEQ_4:15;
end;
end;
assume
A9: c is FinSequence of the carrier' of G;
given p being FinSequence of the carrier of G such that
A10: p is_vertex_seq_of c;
hereby
let n;
assume 1 <= n & n <= len c;
then n in dom c by FINSEQ_3:25;
then
A11: c.n in rng c by FUNCT_1:def 3;
rng c c= the carrier' of G by A9,FINSEQ_1:def 4;
hence c.n in the carrier' of G by A11;
end;
take p;
thus
A12: len p = len c + 1 by A10;
hereby
let n;
assume 1 <= n & n <= len p;
then n in dom p by FINSEQ_3:25;
then
A13: p.n in rng p by FUNCT_1:def 3;
rng p c= the carrier of G by FINSEQ_1:def 4;
hence p.n in the carrier of G by A13;
end;
let n;
assume that
A14: 1 <= n and
A15: n <= len c;
take x9=p/.n, y9=p/.(n+1);
n<=len p & n+1<=len p by A12,A15,NAT_1:12,XREAL_1:6;
hence x9 = p.n & y9 = p.(n+1) by A14,FINSEQ_4:15,NAT_1:12;
thus thesis by A10,A14,A15;
end;
end;
::$CT
theorem
for p,q being FinSequence st n<=len p holds (1,n)-cut p = (1,n)-cut (p ^q)
proof
let p,q be FinSequence;
assume
A1: n<=len p;
per cases;
suppose
A2: n < 1;
then (1,n)-cut p = {} by FINSEQ_6:def 4;
hence thesis by A2,FINSEQ_6:def 4;
end;
suppose
A3: 1<=n;
set cp = (1,n)-cut p, cpq = (1,n)-cut (p^q);
now
A4: len cp +1 = n+1 by A1,A3,FINSEQ_6:def 4;
len (p^q) = len p + len q by FINSEQ_1:22;
then
A5: n<=len (p^q) by A1,NAT_1:12;
then
A6: len cpq +1 = n +1 by A3,FINSEQ_6:def 4;
hence len cp = len cpq by A4;
let k be Nat;
assume that
A7: 1 <=k and
A8: k <= len cp;
k<=len p by A1,A4,A8,XXREAL_0:2;
then
A9: k in dom p by A7,FINSEQ_3:25;
0+1 = 1;
then
A10: ex i being Nat st 0<=i & i<len cp & k=i+1 by A7,A8,FINSEQ_6:127;
hence cp.k = p.k by A1,A3,FINSEQ_6:def 4
.= (p^q).k by A9,FINSEQ_1:def 7
.= cpq.k by A3,A5,A4,A6,A10,FINSEQ_6:def 4;
end;
hence thesis by FINSEQ_1:14;
end;
end;
notation
let G be Graph;
let IT be Chain of G;
synonym IT is directed for IT is oriented;
end;
definition
let G be Graph;
let IT be Chain of G;
attr IT is cyclic means
ex p being FinSequence of the carrier of G st
p is_vertex_seq_of IT & p.1 = p.(len p);
end;
registration
cluster void for Graph;
existence
proof
set V = {1}, E = {};
set S = the Function of E, V;
reconsider G = MultiGraphStruct (# V, E, S, S #) as Graph;
take G;
thus the carrier' of G is empty;
end;
end;
theorem Th2:
for G being Graph holds rng (the Source of G) \/ rng (the Target
of G) c= the carrier of G
proof
let G be Graph;
rng (the Source of G) c= the carrier of G & rng (the Target of G) c= the
carrier of G by RELAT_1:def 19;
hence thesis by XBOOLE_1:8;
end;
registration
cluster finite simple connected non void strict for Graph;
existence
proof
set V = {1,2}, E = {1};
1 in V & 2 in V by TARSKI:def 2;
then reconsider S = E --> 1, T = E --> 2 as Function of E, V by FUNCOP_1:45
;
reconsider G = MultiGraphStruct(# V, E, S, T #) as Graph;
take G;
thus G is finite;
A1: 1 in E by TARSKI:def 1;
then
A2: S.1 = 1 by FUNCOP_1:7;
thus G is simple
proof
given x be set such that
A3: x in the carrier' of G and
A4: (the Source of G).x = (the Target of G).x;
x = 1 by A3,TARSKI:def 1;
hence contradiction by A1,A2,A4,FUNCOP_1:7;
end;
A5: T.1 = 2 by A1,FUNCOP_1:7;
thus G is connected
proof
set MSG = the MultiGraphStruct of G;
given G1, G2 being Graph such that
A6: (the carrier of G1) misses (the carrier of G2) and
A7: G is_sum_of G1, G2;
A8: the MultiGraphStruct of G = G1 \/ G2 by A7;
set V1 = the carrier of G1, V2 = the carrier of G2;
set T1 = the Target of G1, T2 = the Target of G2;
set S1 = the Source of G1, S2 = the Source of G2;
set E1 = the carrier' of G1, E2 = the carrier' of G2;
A9: rng S1 \/ rng T1 c= V1 by Th2;
A10: rng S2 \/ rng T2 c= V2 by Th2;
A11: (the Target of G1) tolerates (the Target of G2) & (the Source of G1
) tolerates (the Source of G2) by A7;
then
A12: the carrier of MSG = (the carrier of G1) \/ (the carrier of G2) by A8,
GRAPH_1:def 5;
A13: the carrier' of MSG = (the carrier' of G1) \/ (the carrier' of G2)
by A11,A8,GRAPH_1:def 5;
per cases by A13,ZFMISC_1:37;
suppose
A14: E1 = E & E2 = E;
then S2.1 = S.1 by A1,A11,A8,GRAPH_1:def 5;
then 1 in rng S2 by A1,A2,A14,FUNCT_2:4;
then
A15: 1 in rng S2 \/ rng T2 by XBOOLE_0:def 3;
S1.1 = S.1 by A1,A11,A8,A14,GRAPH_1:def 5;
then 1 in rng S1 by A1,A2,A14,FUNCT_2:4;
then 1 in rng S1 \/ rng T1 by XBOOLE_0:def 3;
hence contradiction by A6,A9,A10,A15,XBOOLE_0:3;
end;
suppose
A16: E1 = E & E2 = {};
then T1.1 = T.1 by A1,A11,A8,GRAPH_1:def 5;
then 2 in rng T1 by A1,A5,A16,FUNCT_2:4;
then
A17: 2 in rng S1 \/ rng T1 by XBOOLE_0:def 3;
A18: V1 c=V by A12,XBOOLE_1:7;
S1.1 = S.1 by A1,A11,A8,A16,GRAPH_1:def 5;
then 1 in rng S1 by A1,A2,A16,FUNCT_2:4;
then 1 in rng S1 \/ rng T1 by XBOOLE_0:def 3;
then V c=V1 by A9,A17,ZFMISC_1:32;
then V = V1 by A18,XBOOLE_0:def 10;
then V2 c=V1 by A12,XBOOLE_1:7;
hence contradiction by A6,XBOOLE_1:67;
end;
suppose
A19: E1 = {} & E2 = E;
then T2.1 = T.1 by A1,A11,A8,GRAPH_1:def 5;
then 2 in rng T2 by A1,A5,A19,FUNCT_2:4;
then
A20: 2 in rng S2 \/ rng T2 by XBOOLE_0:def 3;
A21: V2 c=V by A12,XBOOLE_1:7;
S2.1 = S.1 by A1,A11,A8,A19,GRAPH_1:def 5;
then 1 in rng S2 by A1,A2,A19,FUNCT_2:4;
then 1 in rng S2 \/ rng T2 by XBOOLE_0:def 3;
then V c=V2 by A10,A20,ZFMISC_1:32;
then V = V2 by A21,XBOOLE_0:def 10;
then V1 c=V2 by A12,XBOOLE_1:7;
hence contradiction by A6,XBOOLE_1:67;
end;
end;
thus G is non void;
thus thesis;
end;
end;
theorem Th3:
for e being set for s, t being Element of the carrier of G st s =
(the Source of G).e & t = (the Target of G).e holds <*s, t*> is_vertex_seq_of
<*e*>
proof
let e be set;
let s, t be Element of the carrier of G;
assume
A1: s = (the Source of G).e & t = (the Target of G).e;
set c = <*e*>;
set vs = <*s, t*>;
A2: vs/.(1+1) = t by FINSEQ_4:17;
A3: len c = 1 by FINSEQ_1:39;
hence len vs = len c + 1 by FINSEQ_1:44;
let n be Nat;
assume 1<=n & n<=len c;
then
A4: n = 1 by A3,XXREAL_0:1;
c.1 = e & vs/.1 = s by FINSEQ_4:17;
hence thesis by A1,A4,A2;
end;
theorem Th4:
for e being set st e in the carrier' of G holds <*e*> is directed Chain of G
proof
let e be set;
assume
A1: e in the carrier' of G;
then reconsider
s = (the Source of G).e, t = (the Target of G).e as Element of
the carrier of G by FUNCT_2:5;
reconsider E = the carrier' of G as non empty set by A1;
reconsider e as Element of E by A1;
<*s,t*> is_vertex_seq_of <*e*> by Th3;
then reconsider c = <*e*> as Chain of G by Def1;
c is directed
by FINSEQ_1:39;
hence thesis;
end;
reserve G for non void Graph;
registration
let G;
cluster directed non empty one-to-one for Chain of G;
existence
proof
set e = the Element of the carrier' of G;
reconsider c = <*e*> as directed Chain of G by Th4;
take c;
thus c is directed;
thus c is non empty;
let n, m be Nat;
assume that
A1: 1 <= n & n < m and
A2: m <= len c;
1 < m by A1,XXREAL_0:2;
hence thesis by A2,FINSEQ_1:39;
end;
end;
Lm1: for G being non empty Graph, c being Chain of G, p being FinSequence of
the carrier of G st c is cyclic & p is_vertex_seq_of c holds p.1 = p.(len p)
proof
let G be non empty Graph;
let c be Chain of G, p be FinSequence of the carrier of G;
assume that
A1: c is cyclic and
A2: p is_vertex_seq_of c;
consider P being FinSequence of the carrier of G such that
A3: P is_vertex_seq_of c and
A4: P.1 = P.(len P) by A1;
per cases;
suppose
card the carrier of G = 1 or c <>{} & not c alternates_vertices_in G;
then P = vertex-seq c & p = vertex-seq c by A2,A3,GRAPH_2:def 8;
hence thesis by A4;
end;
suppose
A5: not(card the carrier of G =1 or c <>{}¬ c alternates_vertices_in G);
A6: len p = len c+1 by A2;
A7: len P = len c +1 by A3;
now
per cases by A5;
suppose
card the carrier of G <>1& c ={};
then len c =0;
hence thesis by A6;
end;
suppose
A8: card the carrier of G <>1 & c alternates_vertices_in G;
then
A9: p is TwoValued Alternating & P is TwoValued Alternating by A2,A3,
GRAPH_2:37;
now
set S=the Source of G, T=the Target of G;
assume p<>P;
A10: rng p ={S.(c.1),T.(c.1)} by A2,A8,GRAPH_2:36;
A11: 1<=len p by A6,NAT_1:11;
then len p in dom p by FINSEQ_3:25;
then p.(len p) in rng p by FUNCT_1:def 3;
then
A12: p.(len p) = S.(c.1) or p.(len p) = T.(c.1) by A10,TARSKI:def 2;
A13: rng P ={S.(c.1),T.(c.1)} by A3,A8,GRAPH_2:36;
1 in dom P by A6,A7,A11,FINSEQ_3:25;
then P.1 in rng p by A10,A13,FUNCT_1:def 3;
then
A14: P.1 = S.(c.1) or P.1 = T.(c.1) by A10,TARSKI:def 2;
1 in dom p by A11,FINSEQ_3:25;
then p.1 in rng p by FUNCT_1:def 3;
then p.1 = S.(c.1) or p.1 = T.(c.1) by A10,TARSKI:def 2;
hence thesis by A4,A6,A7,A9,A10,A13,A11,A12,A14,FINSEQ_6:147;
end;
hence thesis by A4;
end;
end;
hence thesis;
end;
end;
theorem Th5:
for G being Graph, c being Chain of G, vs being FinSequence of
the carrier of G st c is cyclic & vs is_vertex_seq_of c
holds vs.1 = vs.(len vs) by Lm1;
theorem Th6:
for G being Graph, e being set st e in the carrier' of G for fe
being directed Chain of G st fe = <*e*> holds vertex-seq fe = <*(the Source of
G).e, (the Target of G).e*>
proof
let G be Graph;
let e be set;
assume e in the carrier' of G;
then reconsider
so = (the Source of G).e, ta = (the Target of G).e as Element of
the carrier of G by FUNCT_2:5;
reconsider sota = <*so, ta*> as FinSequence of the carrier of G;
let fe be directed Chain of G;
assume
A1: fe = <*e*>;
then
A2: len fe = 1 by FINSEQ_1:39;
A3: sota is_vertex_seq_of fe
proof
thus len sota = len fe + 1 by A2,FINSEQ_1:44;
let n;
A4: sota/.2=ta by FINSEQ_4:17;
assume 1<=n & n<=len fe;
then
A5: n=1 by A2,XXREAL_0:1;
e joins so, ta & sota/.1 = so by FINSEQ_4:17;
hence thesis by A1,A5,A4;
end;
e = fe.1 by A1;
then sota.1 = (the Source of G).(fe.1);
hence thesis by A1,A3,GRAPH_2:def 10;
end;
theorem
for f being FinSequence holds len (m,n)-cut f <= len f
proof
let f be FinSequence;
set lmnf = len (m,n)-cut f;
set lf = len f;
per cases;
suppose
A1: 1<=m & m<=n & n<=len f;
then lmnf +m = n+1 by FINSEQ_6:def 4;
then n+(lmnf +m) <= n+1+lf by A1,XREAL_1:6;
then n+(lmnf +m) <= n+(1+lf);
then lmnf +m <= 1+lf by XREAL_1:6;
then (lmnf +m)+1 <= m+(1+lf) by A1,XREAL_1:7;
then lmnf +(m+1) <= m+1+lf;
hence thesis by XREAL_1:6;
end;
suppose
not (1<=m & m<=n & n<=len f);
then (m,n)-cut f is empty by FINSEQ_6:def 4;
hence thesis;
end;
end;
theorem
for c being directed Chain of G st 1<=m & m<=n & n<=len c holds (m,n)
-cut c is directed Chain of G
proof
let c be directed Chain of G;
assume that
A1: 1<=m and
A2: m<=n and
A3: n<=len c;
reconsider mnc = (m,n)-cut c as Chain of G by A1,A2,A3,GRAPH_2:41;
A4: len mnc +m = n+1 by A1,A2,A3,FINSEQ_6:def 4;
now
A5: len mnc +m<=len c +1 by A3,A4,XREAL_1:6;
let k;
assume that
A6: 1 <= k and
A7: k < len mnc;
0+1<=k by A6;
then consider i being Nat such that
0<=i and
A8: i<len mnc and
A9: k=i+1 by A7,FINSEQ_6:127;
A10: 1<=m+i by A1,NAT_1:12;
m+(i+1)<len mnc +m by A7,A9,XREAL_1:6;
then m+i+1 < len c + 1 by A5,XXREAL_0:2;
then
A11: m+i<len c by XREAL_1:6;
A12: mnc.(k+1) = c.(m+k) by A1,A2,A3,A7,FINSEQ_6:def 4;
mnc.(i+1) = c.(m+i) & m+k = (m+i)+1 by A1,A2,A3,A8,A9,FINSEQ_6:def 4;
hence (the Source of G).(mnc.(k+1)) = (the Target of G).(mnc.k) by A12,A10
,A11,GRAPH_1:def 15;
end;
hence thesis by GRAPH_1:def 15;
end;
theorem Th9:
for oc being non empty directed Chain of G holds len vertex-seq
oc = len oc +1
proof
let oc be non empty directed Chain of G;
vertex-seq oc is_vertex_seq_of oc by GRAPH_2:def 10;
hence thesis;
end;
registration
let G;
let oc be directed non empty Chain of G;
cluster vertex-seq oc -> non empty;
coherence
proof
len vertex-seq oc = len oc +1 by Th9;
hence thesis;
end;
end;
theorem Th10:
for oc being directed non empty Chain of G, n st 1<=n & n<=len
oc holds (vertex-seq oc).n = (the Source of G).(oc.n) & (vertex-seq oc).(n+1) =
(the Target of G).(oc.n)
proof
let oc be directed non empty Chain of G;
set vsoc = vertex-seq oc, S = the Source of G, T = the Target of G;
defpred P[Nat] means 1<=$1 & $1<=len oc implies vsoc.$1 = S.(oc.
$1) & vsoc.($1+1) = T.(oc.$1);
A1: for k be Nat st P[k] holds P[k+1]
proof
let n;
assume
A2: 1<=n & n<=len oc implies vsoc.n = S.(oc.n) & vsoc.(n+1) = T.(oc.n);
A3: vsoc is_vertex_seq_of oc by GRAPH_2:def 10;
assume that
A4: 1<=n+1 and
A5: n+1<=len oc;
per cases;
suppose
A6: n=0;
hence
A7: vsoc.(n+1) = S.(oc.(n+1)) by GRAPH_2:def 10;
1 in dom vsoc by FINSEQ_5:6;
then
A8: vsoc/.1=vsoc.1 by PARTFUN1:def 6;
A9: 1<=len oc by A4,A5,XXREAL_0:2;
len vsoc = len oc +1 by Th9;
then 1+1<=len vsoc by A9,XREAL_1:6;
then 1+1 in dom vsoc by FINSEQ_3:25;
then
A10: vsoc/.(1+1)=vsoc.(1+1) by PARTFUN1:def 6;
oc.1 joins vsoc/.1,vsoc/.(1+1) by A3,A9;
hence thesis by A6,A7,A8,A10;
end;
suppose
A11: n<>0;
A12: n<len oc by A5,NAT_1:13;
1<=n by A11,NAT_1:14;
hence
A13: vsoc.(n+1) = S.(oc.(n+1)) by A2,A12,GRAPH_1:def 15;
A14: len vsoc = len oc +1 by Th9;
then 1<=n+1+1 & n+1+1<=len vsoc by A5,NAT_1:11,XREAL_1:6;
then n+1+1 in dom vsoc by FINSEQ_3:25;
then
A15: vsoc/.(n+1+1)=vsoc.(n+1+1) by PARTFUN1:def 6;
n<=n+1 by NAT_1:11;
then n<=len oc by A5,XXREAL_0:2;
then n+1<=len vsoc by A14,XREAL_1:6;
then n+1 in dom vsoc by A4,FINSEQ_3:25;
then
A16: vsoc/.(n+1)=vsoc.(n+1) by PARTFUN1:def 6;
oc.(n+1) joins vsoc/.(n+1),vsoc/.(n+1+1) by A4,A5,A3;
hence thesis by A13,A16,A15;
end;
end;
A17: P[ 0 ];
thus for n holds P[n] from NAT_1:sch 2 (A17, A1);
end;
theorem Th11:
for f being non empty FinSequence st 1<=m & m<=n & n<=len f
holds (m,n)-cut f is non empty
proof
let f be non empty FinSequence;
set lmn = len (m,n)-cut f;
assume 1<=m & m<=n & n<=len f;
then m<n+1 & lmn+m = n+1 by FINSEQ_6:def 4,NAT_1:13;
then m-(lmn+m)<(n+1)-(n+1) by XREAL_1:9;
then --lmn>0;
hence thesis;
end;
theorem
for c, c1 being directed Chain of G st 1<=m & m<=n & n<=len c & c1 = (
m,n)-cut c holds vertex-seq c1 = (m,n+1)-cut vertex-seq c
proof
let c, c1 be directed Chain of G;
assume that
A1: 1<=m and
A2: m<=n and
A3: n<=len c and
A4: c1 = (m,n)-cut c;
set mn1c=(m,n+1)-cut vertex-seq c;
A5: c is non empty by A1,A2,A3;
then
A6: vertex-seq c is_vertex_seq_of c by GRAPH_2:def 10;
then
A7: mn1c is_vertex_seq_of c1 by A1,A2,A3,A4,GRAPH_2:42;
set vsc = vertex-seq c;
A8: m<=n+1 by A2,NAT_1:12;
A9: len vsc = len c +1 by A6;
then
A10: n+1<=len vsc by A3,XREAL_1:6;
A11: c1 is non empty by A1,A2,A3,A4,A5,Th11;
then 0<len c1;
then
A12: c1.(0+1) = c.(m+0) by A1,A2,A3,A4,FINSEQ_6:def 4;
A13: m<=n+1 by A2,NAT_1:12;
vsc is non empty by A9;
then mn1c is non empty by A1,A8,A10,Th11;
then 0<len mn1c;
then
A14: vsc.(m+0) = mn1c.(0+1) by A1,A10,A13,FINSEQ_6:def 4;
m<=len c by A2,A3,XXREAL_0:2;
then mn1c.1 = (the Source of G).(c1.1) by A1,A5,A12,A14,Th10;
hence thesis by A7,A11,GRAPH_2:def 10;
end;
theorem Th13:
for oc being directed non empty Chain of G holds (vertex-seq oc)
.(len oc +1) = (the Target of G).(oc.len oc)
proof
let oc be directed non empty Chain of G;
1 in dom oc by FINSEQ_5:6;
then 1<=len oc by FINSEQ_3:25;
hence thesis by Th10;
end;
theorem Th14:
for c1, c2 being directed non empty Chain of G holds (vertex-seq
c1).(len c1 + 1) = (vertex-seq c2).1 iff c1^c2 is directed non empty Chain of G
proof
let c1, c2 be directed non empty Chain of G;
set vsc1 = vertex-seq c1, vsc2 = vertex-seq c2;
A1: len (c1^c2) = len c1 + len c2 by FINSEQ_1:22;
A2: vsc1 is_vertex_seq_of c1 by GRAPH_2:def 10;
then
A3: vsc2 is_vertex_seq_of c2 & len vsc1 = len c1 +1 by GRAPH_2:def 10;
hereby
assume
A4: (vertex-seq c1).(len c1 + 1) = (vertex-seq c2).1;
then reconsider c1c2 = c1^c2 as Chain of G by A2,A3,GRAPH_2:43;
c1c2 is directed
proof
let n;
assume that
A5: 1 <= n and
A6: n < len c1c2;
per cases by XXREAL_0:1;
suppose
A7: n<len c1;
then 1<=n+1 & n+1<=len c1 by NAT_1:11,13;
then n+1 in dom c1 by FINSEQ_3:25;
then
A8: c1c2.(n+1) = c1.(n+1) by FINSEQ_1:def 7;
n in dom c1 by A5,A7,FINSEQ_3:25;
then c1c2.n = c1.n by FINSEQ_1:def 7;
hence thesis by A5,A7,A8,GRAPH_1:def 15;
end;
suppose
A9: n=len c1;
then n in dom c1 by FINSEQ_5:6;
then
A10: c1c2.n = c1.n by FINSEQ_1:def 7;
1 in dom c2 by FINSEQ_5:6;
then
A11: c1c2.(n+1) = c2.1 by A9,FINSEQ_1:def 7;
vsc1.(len c1 +1) =(the Target of G).(c1.(len c1)) by Th13;
hence thesis by A4,A9,A11,A10,GRAPH_2:def 10;
end;
suppose
A12: n>len c1;
then reconsider k = n-len c1 as Element of NAT by INT_1:5;
A13: n = len c1 + k;
A14: n+1 = len c1 +(k+1);
A15: k<len c2 by A1,A6,XREAL_1:19;
then 1<=k+1 & k+1<=len c2 by NAT_1:11,13;
then k+1 in dom c2 by FINSEQ_3:25;
then
A16: c1c2.(n+1) = c2.(k+1) by A14,FINSEQ_1:def 7;
n>=len c1 +1 by A12,NAT_1:13;
then
A17: 1<=k by XREAL_1:19;
then k in dom c2 by A15,FINSEQ_3:25;
then c1c2.n = c2.k by A13,FINSEQ_1:def 7;
hence thesis by A17,A15,A16,GRAPH_1:def 15;
end;
end;
hence c1^c2 is directed non empty Chain of G;
end;
set n = len c1;
assume c1^c2 is directed non empty Chain of G;
then reconsider c1c2 = c1^c2 as directed non empty Chain of G;
A18: n<len c1c2 by A1,XREAL_1:29;
A19: n in dom c1 by FINSEQ_5:6;
then
A20: c1c2.n = c1.n by FINSEQ_1:def 7;
1<=n by A19,FINSEQ_3:25;
then
A21: (the Source of G).(c1c2.(n+1)) = (the Target of G).(c1c2.n) by A18,
GRAPH_1:def 15;
1 in dom c2 by FINSEQ_5:6;
then
A22: c1c2.(n+1) = c2.1 by FINSEQ_1:def 7;
vsc1.(len c1 +1) =(the Target of G).(c1.(len c1)) by Th13;
hence thesis by A21,A22,A20,GRAPH_2:def 10;
end;
theorem Th15:
for c, c1, c2 being directed non empty Chain of G st c =c1^c2
holds (vertex-seq c).1 = (vertex-seq c1).1 & (vertex-seq c).(len c +1) = (
vertex-seq c2).(len c2 +1)
proof
let c, c1, c2 be directed non empty Chain of G;
1 in dom c by FINSEQ_5:6;
then 1<=len c by FINSEQ_3:25;
then
A1: (vertex-seq c).1 = (the Source of G).(c.1) & (vertex-seq c).(len c +1)
= ( the Target of G).(c.len c) by Th10;
A2: 1 in dom c1 by FINSEQ_5:6;
then 1<=len c1 by FINSEQ_3:25;
then
A3: (vertex-seq c1).1 = (the Source of G).(c1.1) by Th10;
1 in dom c2 by FINSEQ_5:6;
then 1<=len c2 by FINSEQ_3:25;
then
A4: (vertex-seq c2).(len c2 +1) = (the Target of G).(c2.len c2) by Th10;
assume
A5: c =c1^c2;
then len c2 in dom c2 & len c = len c1 + len c2 by FINSEQ_1:22,FINSEQ_5:6;
hence thesis by A5,A2,A3,A1,A4,FINSEQ_1:def 7;
end;
theorem Th16:
for oc being directed non empty Chain of G st oc is cyclic holds
(vertex-seq oc).1 = (vertex-seq oc).(len oc +1)
proof
let oc be directed non empty Chain of G;
assume
A1: oc is cyclic;
set vsoc = vertex-seq oc;
A2: vsoc is_vertex_seq_of oc by GRAPH_2:def 10;
thus thesis by A1,A2,Th5;
end;
theorem Th17:
for c being directed non empty Chain of G st c is cyclic for n
ex ch being directed Chain of G st len ch = n & ch^c is directed non empty
Chain of G
proof
let c be directed non empty Chain of G;
defpred Z[Nat] means ex ch being directed Chain of G st rng ch c=
rng c & len ch = $1 & ch^c is directed non empty Chain of G;
c is FinSequence of the carrier' of G by Def1;
then
A1: rng c c= the carrier' of G by FINSEQ_1:def 4;
assume
A2: c is cyclic;
A3: for i be Nat st Z[i] holds Z[i+1]
proof
len c in dom c by FINSEQ_5:6;
then
A4: c.len c in rng c by FUNCT_1:def 3;
then reconsider clc = c.len c as Element of the carrier' of G by A1;
reconsider ch9= <*clc*> as directed Chain of G by Th4;
A5: rng ch9 = {c.len c} by FINSEQ_1:38;
then
A6: rng ch9 c= rng c by A4,ZFMISC_1:31;
A7: len ch9 = 1 by FINSEQ_1:39;
let n be Nat;
given ch being directed Chain of G such that
A8: rng ch c= rng c and
A9: len ch = n and
A10: ch^c is directed non empty Chain of G;
per cases;
suppose
A11: n = 0;
take ch9;
thus rng ch9 c= rng c by A4,A5,ZFMISC_1:31;
thus len ch9 = n+1 by A11,FINSEQ_1:39;
set vsch9 = vertex-seq ch9;
vsch9 = <*(the Source of G).clc, (the Target of G).clc*> by Th6;
then vsch9.(len ch9 +1) = (the Target of G).clc by A7
.= (vertex-seq c).(len c +1) by Th13
.= (vertex-seq c).1 by A2,Th16;
hence thesis by Th14;
end;
suppose
n<>0;
then
A12: ch is non empty by A9;
then 1 in dom ch by FINSEQ_5:6;
then ch.1 in rng ch by FUNCT_1:def 3;
then consider i being Nat such that
A13: i in dom c and
A14: c.i = ch.1 by A8,FINSEQ_2:10;
A15: i<=len c by A13,FINSEQ_3:25;
A16: 1<=i by A13,FINSEQ_3:25;
now
per cases;
suppose
A17: i = 1;
set vsch9 = vertex-seq ch9;
vsch9 = <*(the Source of G).clc, (the Target of G).clc*> by Th6;
then vsch9.(len ch9 +1) = (the Target of G).clc by A7
.= (vertex-seq c).(len c +1) by Th13
.= (vertex-seq c).1 by A2,Th16
.= (the Source of G).(ch.1) by A14,A17,GRAPH_2:def 10
.= (vertex-seq ch).1 by A12,GRAPH_2:def 10;
then reconsider ch1 = ch9^ch as directed Chain of G by A12,Th14;
take ch1;
rng ch1 = rng ch9 \/ rng ch by FINSEQ_1:31;
hence rng ch1 c= rng c by A8,A6,XBOOLE_1:8;
thus len ch1 = n+1 by A9,A7,FINSEQ_1:22;
(vertex-seq ch1).(len ch1 +1) = (vertex-seq ch).(len ch +1) by A12
,Th15
.= (vertex-seq c).1 by A10,A12,Th14;
hence ch1^c is directed non empty Chain of G by Th14;
end;
suppose
i <> 1;
then 1<i by A16,XXREAL_0:1;
then 1+1<=i by NAT_1:13;
then consider k being Nat such that
A18: 1<=k & k<len c and
A19: i=k+1 by A15,FINSEQ_6:127;
k in dom c by A18,FINSEQ_3:25;
then
A20: c.k in rng c by FUNCT_1:def 3;
then reconsider ck = c.k as Element of the carrier' of G by A1;
reconsider ch9= <*ck*> as directed Chain of G by Th4;
set vsch9 = vertex-seq ch9;
A21: len ch9 = 1 by FINSEQ_1:39;
vsch9 = <*(the Source of G).ck, (the Target of G).ck*> by Th6;
then vsch9.(len ch9 +1) = (the Target of G).ck by A21
.= (the Source of G).(ch.1) by A14,A18,A19,GRAPH_1:def 15
.= (vertex-seq ch).1 by A12,GRAPH_2:def 10;
then reconsider ch1 = ch9^ch as directed Chain of G by A12,Th14;
take ch1;
rng ch9 = {c.k} by FINSEQ_1:38;
then
A22: rng ch9 c= rng c by A20,ZFMISC_1:31;
rng ch1 = rng ch9 \/ rng ch by FINSEQ_1:31;
hence rng ch1 c= rng c by A8,A22,XBOOLE_1:8;
thus len ch1 = n+1 by A9,A21,FINSEQ_1:22;
(vertex-seq ch1).(len ch1 +1) = (vertex-seq ch).(len ch +1) by A12
,Th15
.= (vertex-seq c).1 by A10,A12,Th14;
hence ch1^c is directed non empty Chain of G by Th14;
end;
end;
hence thesis;
end;
end;
let n be Nat;
A23: Z[ 0 ]
proof
reconsider ch = {} as empty Chain of G by GRAPH_1:14;
reconsider ch as directed Chain of G;
take ch;
thus rng ch c= rng c;
thus len ch = 0;
thus thesis by FINSEQ_1:34;
end;
for n being Nat holds Z[n] from NAT_1:sch 2 (A23, A3);
then ex ch being directed Chain of G st rng ch c= rng c & len ch = n & ch^c
is directed non empty Chain of G;
hence thesis;
end;
definition
let IT be Graph;
attr IT is directed_cycle-less means
for dc being directed Chain of IT st dc is non empty holds dc is non cyclic;
end;
notation
let IT be Graph;
antonym IT is with_directed_cycle for IT is directed_cycle-less;
end;
registration
cluster void -> directed_cycle-less for Graph;
coherence
proof
let G be Graph;
assume
A1: G is void;
let c be directed Chain of G;
assume
A2: c is non empty;
c is FinSequence of the carrier' of G by Def1;
hence thesis by A1,A2;
end;
end;
definition
let IT be Graph;
attr IT is well-founded means
for v being Element of the carrier of
IT ex n st for c being directed Chain of IT st c is non empty & (vertex-seq c).
(len c +1) = v holds len c <= n;
end;
registration
let G be void Graph;
cluster -> empty for Chain of G;
coherence
proof
let c be Chain of G;
assume
A1: c is non empty;
c is FinSequence of the carrier' of G by Def1;
hence thesis by A1;
end;
end;
registration
cluster void -> well-founded for Graph;
coherence
proof
let G be Graph;
assume G is void;
then reconsider G9 = G as void Graph;
let v be Element of the carrier of G;
take 0;
let c be directed Chain of G;
reconsider c as Chain of G9;
c is empty;
hence thesis;
end;
end;
registration
cluster non well-founded -> non void for Graph;
coherence;
end;
registration
cluster well-founded for Graph;
existence
proof
set G = the void Graph;
G is well-founded;
hence thesis;
end;
end;
registration
cluster well-founded -> directed_cycle-less for Graph;
coherence
proof
let G be Graph;
per cases;
suppose
G is void;
then reconsider G as void Graph;
G is directed_cycle-less;
hence thesis;
end;
suppose
G is non void;
then reconsider G9=G as non void Graph;
assume that
A1: G is well-founded and
A2: G is non directed_cycle-less;
consider dc being directed Chain of G9 such that
A3: dc is non empty and
A4: dc is cyclic by A2;
set p = vertex-seq dc;
len p = len dc +1 by A3,Th9;
then 1<=len p by NAT_1:11;
then 1 in dom p by FINSEQ_3:25;
then reconsider v = p.1 as Element of the carrier of G by FINSEQ_2:11;
consider n such that
A5: for c being directed Chain of G9 st c is non empty & (
vertex-seq c).(len c +1) = v holds len c <= n by A1;
consider ch being directed Chain of G9 such that
A6: len ch = n+1 and
A7: ch^dc is directed non empty Chain of G9 by A3,A4,Th17;
reconsider ch as directed non empty Chain of G9 by A6;
reconsider cc = ch^dc as directed non empty Chain of G9 by A7;
(vertex-seq dc).1 = (vertex-seq dc).(len dc +1) by A3,A4,Th16;
then (vertex-seq cc).(len cc +1) = v by A3,Th15;
then
A8: len cc <=n by A5;
len cc = n+1 + len dc by A6,FINSEQ_1:22;
then n+1<=len cc by NAT_1:11;
hence contradiction by A8,NAT_1:13;
end;
end;
end;
registration
cluster non well-founded for Graph;
existence
proof
set V = {1}, E = {1};
reconsider j = 1 as Element of V by TARSKI:def 1;
reconsider S = E --> j, T = E --> j as Function of E, V;
reconsider G = MultiGraphStruct(# V, E, S, T #) as Graph;
reconsider v = 1 as Element of the carrier of G;
take G;
A1: S.1 = 1 by FUNCOP_1:7;
A2: G is with_directed_cycle
proof
reconsider dc = <*1*> as directed Chain of G by Th4;
take dc;
thus dc is non empty;
A3: <*v,v*>.2 = v & len <*v,v*> = 2 by FINSEQ_1:44;
<*v,v*> is_vertex_seq_of dc & <*v,v*>.1 = v by A1,Th3;
hence thesis by A3;
end;
assume G is well-founded;
then reconsider G as well-founded Graph;
G is directed_cycle-less;
hence contradiction by A2;
end;
end;
registration
cluster directed_cycle-less for Graph;
existence
proof
set G = the well-founded Graph;
G is directed_cycle-less;
hence thesis;
end;
end;
theorem
for t being DecoratedTree, p being Node of t, k being Element of NAT
holds p|k is Node of t
proof
let t be DecoratedTree, p be Node of t, k be Element of NAT;
p|k = p|Seg k by FINSEQ_1:def 16;
then p|k is_a_prefix_of p by TREES_1:def 1;
hence thesis by TREES_1:20;
end;
begin :: Some properties of many sorted algebras
theorem
for S being non void non empty ManySortedSign, X being non-empty
ManySortedSet of the carrier of S, t being Term of S,X st t is not root
ex o being OperSymbol of S st t.{} = [o,the carrier of S]
proof
let S be non void non empty ManySortedSign, X be non-empty ManySortedSet
of the carrier of S, t be Term of S,X;
assume
A1: t is not root;
per cases by MSATERM:2;
suppose
ex s being SortSymbol of S,v being Element of X.s st t.{} = [v,s];
then consider s being SortSymbol of S, v being Element of X.s such that
A2: t.{} = [v,s];
t = root-tree [v,s] by A2,MSATERM:5;
hence thesis by A1;
end;
suppose
t.{} in [:the carrier' of S,{the carrier of S}:];
then consider o, c being object such that
A3: o in the carrier' of S and
A4: c in {the carrier of S} & t.{} = [o,c] by ZFMISC_1:def 2;
reconsider o as OperSymbol of S by A3;
take o;
thus thesis by A4,TARSKI:def 1;
end;
end;
theorem Th20:
for S being non void non empty ManySortedSign, A being MSAlgebra
over S, G being GeneratorSet of A, B being MSSubset of A st G c= B holds B is
GeneratorSet of A
proof
let S be non void non empty ManySortedSign, A be MSAlgebra over S, G be
GeneratorSet of A, B be MSSubset of A;
B is MSSubset of GenMSAlg B by MSUALG_2:def 17;
then
A1: B c= the Sorts of GenMSAlg B by PBOOLE:def 18;
assume G c= B;
then G c= the Sorts of GenMSAlg B by A1,PBOOLE:13;
then G is MSSubset of GenMSAlg B by PBOOLE:def 18;
then GenMSAlg G is MSSubAlgebra of GenMSAlg B by MSUALG_2:def 17;
then the Sorts of GenMSAlg G is MSSubset of GenMSAlg B by MSUALG_2:def 9;
then
A2: the Sorts of GenMSAlg G c= the Sorts of GenMSAlg B by PBOOLE:def 18;
A3: the Sorts of GenMSAlg(G) = the Sorts of A by MSAFREE:def 4;
then the Sorts of GenMSAlg B is MSSubset of GenMSAlg G by MSUALG_2:def 9;
then the Sorts of GenMSAlg B c= the Sorts of GenMSAlg G by PBOOLE:def 18;
hence the Sorts of GenMSAlg(B) = the Sorts of A by A3,A2,PBOOLE:146;
end;
registration
let S be non void non empty ManySortedSign, A be finitely-generated
non-empty MSAlgebra over S;
cluster non-empty finite-yielding for GeneratorSet of A;
existence
proof
consider G being GeneratorSet of A such that
A1: G is finite-yielding by MSAFREE2:def 10;
consider B being ManySortedSet of the carrier of S such that
A2: B in the Sorts of A by PBOOLE:134;
deffunc F(object) = {B.$1};
consider C being ManySortedSet of the carrier of S such that
A3: for i being object st i in the carrier of S holds C.i = F(i) from
PBOOLE:sch 4;
set H = G (\/) C;
now
let i be object;
assume
A4: i in the carrier of S;
then B.i in (the Sorts of A).i by A2;
then {B.i} c= (the Sorts of A).i by ZFMISC_1:31;
hence C.i c= (the Sorts of A).i by A3,A4;
end;
then G c= the Sorts of A & C c= the Sorts of A by PBOOLE:def 18;
then
A5: C c= H & G (\/) C c= the Sorts of A by PBOOLE:14,16;
now
let i be object;
assume i in the carrier of S;
then C.i = {B.i} by A3;
hence C.i is non empty;
end;
then C is non-empty;
then reconsider H as non-empty MSSubset of A by A5,PBOOLE:131,def 18;
G c= H by PBOOLE:14;
then reconsider H as GeneratorSet of A by Th20;
take H;
thus H is non-empty;
let i be object;
assume
A6: i in the carrier of S;
then
A7: C.i = {B.i} by A3;
A8: H.i = G.i \/ C.i by A6,PBOOLE:def 4;
G.i is finite by A1;
hence thesis by A7,A8;
end;
end;
theorem Th21:
for S being non void non empty ManySortedSign, A being non-empty
MSAlgebra over S, X being non-empty GeneratorSet of A ex F being
ManySortedFunction of FreeMSA X, A st F is_epimorphism FreeMSA X, A
proof
let S be non void non empty ManySortedSign, A be non-empty MSAlgebra over S,
X be non-empty GeneratorSet of A;
reconsider X9 = X as MSSubset of A;
now
let i be object such that
A1: i in the carrier of S;
A2: (Reverse X).i is Function of (FreeGen X).i, X.i by A1,PBOOLE:def 15;
X c= the Sorts of A by PBOOLE:def 18;
then X.i c= (the Sorts of A).i by A1;
hence
(Reverse X).i is Function of (FreeGen X).i, (the Sorts of A).i by A1,A2,
FUNCT_2:7;
end;
then reconsider
ff = Reverse X as ManySortedFunction of FreeGen X,the Sorts of A
by PBOOLE:def 15;
FreeGen X is free by MSAFREE:16;
then consider h being ManySortedFunction of FreeMSA X, A such that
A3: h is_homomorphism FreeMSA X, A and
A4: h || FreeGen X = ff;
take h;
thus h is_homomorphism FreeMSA X, A by A3;
let i be set;
assume i in the carrier of S;
then reconsider s = i as SortSymbol of S;
set f = h.s;
consider g being ManySortedFunction of FreeMSA X, Image h such that
A5: h = g and
A6: g is_epimorphism FreeMSA X, Image h by A3,MSUALG_3:21;
A7: g is_homomorphism FreeMSA X, Image h by A6;
A8: Image g = Image h by A6,MSUALG_3:19;
X is MSSubset of Image h
proof
let i be object;
assume
A9: i in the carrier of S;
then reconsider s = i as SortSymbol of S;
s in dom Reverse X by A9,PARTFUN1:def 2;
then
A10: rngs Reverse X = X & (rngs Reverse X).s = rng ((Reverse X).s) by
EXTENS_1:10,FUNCT_6:22;
reconsider hs = h.s as Function of (the Sorts of FreeMSA X).s, (the Sorts
of A).s;
let x be object;
FreeGen X c= the Sorts of FreeMSA X by PBOOLE:def 18;
then
A11: (FreeGen X).s c= (the Sorts of FreeMSA X).s;
the Sorts of Image h = h.:.:(the Sorts of FreeMSA X) by A3,MSUALG_3:def 12;
then
A12: (the Sorts of Image h).s = hs.:((the Sorts of FreeMSA X).s) by
PBOOLE:def 20;
assume x in X.i;
then consider c being object such that
A13: c in dom (ff.s) and
A14: x = ff.s.c by A10,FUNCT_1:def 3;
A15: ff.s = hs | ((FreeGen X).s) by A4,MSAFREE:def 1;
then dom (ff.s) = dom hs /\ (FreeGen X).s by RELAT_1:61;
then
A16: c in (FreeGen X).s & c in dom hs by A13,XBOOLE_0:def 4;
x = hs.c by A15,A13,A14,FUNCT_1:47;
hence thesis by A12,A11,A16,FUNCT_1:def 6;
end;
then GenMSAlg X9 is MSSubAlgebra of Image h by MSUALG_2:def 17;
then the Sorts of GenMSAlg X9 is MSSubset of Image h by MSUALG_2:def 9;
then
A17: the Sorts of GenMSAlg X9 c= the Sorts of Image h by PBOOLE:def 18;
the Sorts of Image g = h.:.:(the Sorts of FreeMSA X) by A5,A7,MSUALG_3:def 12
;
then
A18: (the Sorts of Image g).i = f.:((the Sorts of FreeMSA X).i) by
PBOOLE:def 20;
the Sorts of Image h is MSSubset of A by MSUALG_2:def 9;
then
the Sorts of GenMSAlg X9 = the Sorts of A & the Sorts of Image h c= the
Sorts of A by MSAFREE:def 4,PBOOLE:def 18;
then the Sorts of Image h = the Sorts of A by A17,PBOOLE:146;
hence thesis by A18,A8,RELSET_1:22;
end;
theorem
for S being non void non empty ManySortedSign, A being non-empty
MSAlgebra over S, X being non-empty GeneratorSet of A st A is non
finite-yielding holds FreeMSA X is non finite-yielding
proof
let S be non void non empty ManySortedSign, A be non-empty MSAlgebra over S,
X be non-empty GeneratorSet of A such that
A1: A is non finite-yielding and
A2: FreeMSA X is finite-yielding;
the Sorts of A is non finite-yielding by A1,MSAFREE2:def 11;
then consider i being object such that
A3: i in the carrier of S and
A4: (the Sorts of A).i is infinite;
the Sorts of FreeMSA X is finite-yielding by A2,MSAFREE2:def 11;
then
A5: (the Sorts of FreeMSA X).i is finite;
reconsider FXi = (the Sorts of FreeMSA X).i as non empty set by A3;
reconsider SAi = (the Sorts of A).i as non empty set by A3;
consider F being ManySortedFunction of FreeMSA X, A such that
A6: F is_epimorphism FreeMSA X, A by Th21;
reconsider i as Element of S by A3;
reconsider Fi = F.i as Function of FXi, SAi;
F is "onto" by A6;
then rng Fi = SAi;
hence contradiction by A4,A5;
end;
registration
let S be non void non empty ManySortedSign, X be non-empty finite-yielding
ManySortedSet of the carrier of S, v be SortSymbol of S;
cluster FreeGen(v, X) -> finite;
coherence
proof
A1: X.v,FreeGen(v, X) are_equipotent
proof
set Z = the set of all [a, root-tree[a,v]] where a is Element of X.v;
take Z;
hereby
let x be object such that
A2: x in X.v;
reconsider y = root-tree [x, v] as object;
take y;
thus y in FreeGen(v,X) by A2,MSAFREE:def 15;
thus [x,y] in Z by A2;
end;
hereby
let y be object;
assume y in FreeGen(v, X);
then consider x being set such that
A3: x in X.v and
A4: y = root-tree [x,v] by MSAFREE:def 15;
reconsider x as object;
take x;
thus x in X.v by A3;
thus [x,y] in Z by A3,A4;
end;
let x,y,z,u be object;
assume that
A5: [x,y] in Z and
A6: [z,u] in Z;
consider a being Element of X.v such that
A7: [x,y] = [a, root-tree[a,v]] by A5;
consider b being Element of X.v such that
A8: [z,u] = [b, root-tree[b,v]] by A6;
A9: z = b by A8,XTUPLE_0:1;
A10: x = a by A7,XTUPLE_0:1;
hence x = z implies y = u by A7,A8,A9,XTUPLE_0:1;
A11: y = root-tree[a,v] by A7,XTUPLE_0:1;
A12: u = root-tree[b,v] by A8,XTUPLE_0:1;
assume y = u;
then [a,v] = [b,v] by A11,A12,TREES_4:4;
hence thesis by A10,A9,XTUPLE_0:1;
end;
thus thesis by A1,CARD_1:38;
end;
end;
theorem Th23:
for S being non void non empty ManySortedSign, A being non-empty
MSAlgebra over S, o be OperSymbol of S st (the Arity of S).o = {} holds dom Den
(o, A) = {{}}
proof
dom {} = {} & rng {} = {};
then reconsider b = {} as Function of {},{} by FUNCT_2:1;
let S be non void non empty ManySortedSign, A be non-empty MSAlgebra over S,
o be OperSymbol of S such that
A1: (the Arity of S).o = {};
A2: dom (the Arity of S) = the carrier' of S by FUNCT_2:def 1;
then dom ((the Sorts of A)# qua ManySortedSet of(the carrier of S)*) = (the
carrier of S)* & (the Arity of S).o in rng (the Arity of S) by FUNCT_1:def 3
,PARTFUN1:def 2;
then
A3: o in dom ((the Sorts of A)# * the Arity of S) by A2,FUNCT_1:11;
thus dom Den(o,A) = Args(o,A) by FUNCT_2:def 1
.= ((the Sorts of A)# * the Arity of S).o by MSUALG_1:def 4
.= (the Sorts of A)# . ((the Arity of S).o) by A3,FUNCT_1:12
.= (the Sorts of A)# . (the_arity_of o) by MSUALG_1:def 1
.= product ((the Sorts of A) * (the_arity_of o) qua Function) by
FINSEQ_2:def 5
.= product ((the Sorts of A) * b) by A1,MSUALG_1:def 1
.= {{}} by CARD_3:10;
end;
definition
let IT be non void non empty ManySortedSign;
attr IT is finitely_operated means
for s being SortSymbol of IT holds
{o where o is OperSymbol of IT: the_result_sort_of o = s} is finite;
end;
theorem
for S being non void non empty ManySortedSign, A being non-empty
MSAlgebra over S, v be SortSymbol of S st S is finitely_operated holds
Constants(A, v) is finite
proof
let S be non void non empty ManySortedSign, A be non-empty MSAlgebra over S,
v be SortSymbol of S such that
A1: S is finitely_operated;
set Ov = {o where o is OperSymbol of S: the_result_sort_of o = v};
consider Av being non empty set such that
Av =(the Sorts of A).v and
A2: Constants(A,v) = { a where a is Element of Av : ex o be OperSymbol
of S st (the Arity of S).o = {} & (the ResultSort of S).o = v & a in rng Den(o,
A)} by MSUALG_2:def 3;
A3: Ov is finite by A1;
A4: now
assume Ov is non empty;
then reconsider Ov as non empty set;
deffunc G(Element of the carrier' of S)=Den($1,A).{};
defpred P[Element of Ov] means (the Arity of S).$1 = {};
set COv = {o where o is Element of Ov: P[o]};
set aCOv = {G(o) where o is Element of the carrier' of S : o in COv };
A5: Constants(A,v) c= aCOv
proof
let c be object;
assume c in Constants(A,v);
then consider a being Element of Av such that
A6: a = c and
A7: ex o be OperSymbol of S st (the Arity of S).o = {} & (the
ResultSort of S).o = v & a in rng Den(o,A) by A2;
consider o being OperSymbol of S such that
A8: (the Arity of S).o = {} and
A9: (the ResultSort of S).o = v and
A10: a in rng Den(o,A) by A7;
the_result_sort_of o = (the ResultSort of S).o by MSUALG_1:def 2;
then o in Ov by A9;
then reconsider o9 = o as Element of Ov;
A11: o9 in COv by A8;
set f = Den(o,A);
consider x being object such that
A12: x in dom f and
A13: a = f.x by A10,FUNCT_1:def 3;
dom f = {{}} by A8,Th23;
then x = {} by A12,TARSKI:def 1;
hence thesis by A6,A11,A13;
end;
COv is Subset of Ov from DOMAIN_1:sch 7;
then
A14: COv is finite by A3;
aCOv is finite from FRAENKEL:sch 21(A14);
hence thesis by A5;
end;
now
assume
A15: Ov is empty;
now
assume Constants(A, v) is non empty;
then consider c being object such that
A16: c in Constants(A,v) by XBOOLE_0:def 1;
consider a being Element of Av such that
a = c and
A17: ex o be OperSymbol of S st (the Arity of S).o = {} & (the
ResultSort of S).o = v & a in rng Den(o,A) by A2,A16;
consider o being OperSymbol of S such that
(the Arity of S).o = {} and
A18: (the ResultSort of S).o = v and
a in rng Den(o,A) by A17;
the_result_sort_of o = (the ResultSort of S).o by MSUALG_1:def 2;
then o in Ov by A18;
hence contradiction by A15;
end;
hence thesis;
end;
hence thesis by A4;
end;
theorem
for S being non void non empty ManySortedSign, X being non-empty
ManySortedSet of the carrier of S, v being SortSymbol of S holds {t where t is
Element of (the Sorts of FreeMSA X).v: depth t = 0} = FreeGen(v, X) \/
Constants(FreeMSA X, v)
proof
let S be non void non empty ManySortedSign, X be non-empty ManySortedSet of
the carrier of S, v be SortSymbol of S;
set SF = the Sorts of FreeMSA X;
set d0 = {t where t is Element of SF.v: depth t = 0};
A1: d0 c= FreeGen(v, X) \/ Constants(FreeMSA X, v)
proof
let x be object;
assume x in d0;
then consider t being Element of SF.v such that
A2: x = t and
A3: depth t = 0;
t in SF.v;
then t in FreeSort(X, v) by MSAFREE:def 11;
then consider a being Element of TS(DTConMSA(X)) such that
A4: t = a and
A5: (ex x be set st x in X.v & a = root-tree [x,v]) or ex o be
OperSymbol of S st [o,the carrier of S] = a.{} & the_result_sort_of o = v;
consider dt being finite DecoratedTree, ft being finite Tree such that
A6: dt = t and
A7: ft = dom dt & depth t = height ft by MSAFREE2:def 14;
per cases by A5;
suppose
ex x be set st x in X.v & a = root-tree [x,v];
then t in FreeGen(v,X) by A4,MSAFREE:def 15;
hence thesis by A2,XBOOLE_0:def 3;
end;
suppose
ex o be OperSymbol of S st [o,the carrier of S] = a.{} &
the_result_sort_of o = v;
then consider o be OperSymbol of S such that
A8: [o,the carrier of S] = a.{} and
A9: the_result_sort_of o = v;
A10: (the ResultSort of S).o = v by A9,MSUALG_1:def 2;
set ars9 = <*>TS DTConMSA X;
reconsider t9= t as Term of S, X by A4,MSATERM:def 1;
A11: ex Av being non empty set st Av = SF.v & Constants( FreeMSA X,v) = {
a1 where a1 is Element of Av : ex o be OperSymbol of S st (the Arity of S).o =
{} & (the ResultSort of S).o = v & a1 in rng Den(o, FreeMSA X)} by
MSUALG_2:def 3;
consider ars being ArgumentSeq of Sym(o,X) such that
A12: t9 = [o,the carrier of S]-tree ars by A4,A8,MSATERM:10;
dt = root-tree (dt.{}) by A3,A7,TREES_1:43,TREES_4:5;
then
A13: ars = {} by A6,A12,TREES_4:17;
then 0 = len ars .= len the_arity_of o by MSATERM:22;
then the_arity_of o = {};
then
A14: (the Arity of S).o = {} by MSUALG_1:def 1;
then dom Den(o, FreeMSA X) = {{}} by Th23;
then
A15: {} in dom Den(o, FreeMSA X) by TARSKI:def 1;
Sym(o, X) ==> roots ars by MSATERM:21;
then
A16: DenOp(o, X).ars9 = t by A12,A13,MSAFREE:def 12;
Den(o, FreeMSA X) = (FreeOper X).o by MSUALG_1:def 6
.= DenOp(o, X) by MSAFREE:def 13;
then t in rng Den(o, FreeMSA X) by A16,A15,FUNCT_1:def 3;
then t in Constants(FreeMSA X, v) by A14,A10,A11;
hence thesis by A2,XBOOLE_0:def 3;
end;
end;
A17: Constants(FreeMSA X, v) c= d0
proof
set p = <*>TS(DTConMSA(X));
let x be object;
consider Av being non empty set such that
A18: Av =(the Sorts of FreeMSA X).v and
A19: Constants(FreeMSA X,v) = { a where a is Element of Av : ex o be
OperSymbol of S st (the Arity of S).o = {} & (the ResultSort of S).o = v & a in
rng Den(o,FreeMSA X)} by MSUALG_2:def 3;
assume x in Constants(FreeMSA X, v);
then consider a being Element of Av such that
A20: x = a and
A21: ex o be OperSymbol of S st (the Arity of S).o = {} & (the
ResultSort of S).o = v & a in rng Den(o,FreeMSA X) by A19;
consider o being OperSymbol of S such that
A22: (the Arity of S).o = {} and
(the ResultSort of S).o = v and
A23: a in rng Den(o,FreeMSA X) by A21;
A24: dom Den(o, FreeMSA X) = {{}} by A22,Th23;
((FreeSort X)# * (the Arity of S)).o = Args(o,FreeMSA X) by MSUALG_1:def 4
.= dom Den(o,FreeMSA X) by FUNCT_2:def 1;
then p in ((FreeSort X)# * (the Arity of S)).o by A24,TARSKI:def 1;
then Sym(o,X) ==> roots p by MSAFREE:10;
then
A25: DenOp(o,X).p = (Sym(o,X))-tree p by MSAFREE:def 12;
reconsider a as Element of (the Sorts of FreeMSA X).v by A18;
consider d being object such that
A26: d in dom Den(o,FreeMSA X) and
A27: a = Den(o,FreeMSA X).d by A23,FUNCT_1:def 3;
consider dt being finite DecoratedTree, t being finite Tree such that
A28: dt = a & t = dom dt and
A29: depth a = height t by MSAFREE2:def 14;
A30: Den(o, FreeMSA X) = (FreeOper X).o by MSUALG_1:def 6
.= DenOp(o, X) by MSAFREE:def 13;
d = {} by A24,A26,TARSKI:def 1;
then a = root-tree (Sym(o,X)) by A27,A30,A25,TREES_4:20;
then height t = 0 by A28,TREES_1:42,TREES_4:3;
hence thesis by A20,A29;
end;
FreeGen(v, X) c= d0
proof
let x be object;
assume
A31: x in FreeGen(v, X);
then reconsider x9 = x as Element of SF.v;
consider dt being finite DecoratedTree, t being finite Tree such that
A32: dt = x9 & t = dom dt and
A33: depth x9 = height t by MSAFREE2:def 14;
ex a being set st a in X.v & x = root-tree [a,v] by A31,MSAFREE:def 15;
then height t = 0 by A32,TREES_1:42,TREES_4:3;
hence thesis by A33;
end;
then FreeGen(v, X) \/ Constants(FreeMSA X, v) c= d0 by A17,XBOOLE_1:8;
hence thesis by A1,XBOOLE_0:def 10;
end;
theorem
for S being non void non empty ManySortedSign, X being non-empty
ManySortedSet of the carrier of S, v, vk being SortSymbol of S, o being
OperSymbol of S, t being Element of (the Sorts of FreeMSA X).v, a being (
ArgumentSeq of Sym(o,X)), k being Element of NAT, ak being Element of (the
Sorts of FreeMSA X).vk st t = [o,the carrier of S]-tree a & k in dom a & ak = a
.k holds depth ak < depth t
proof
let S be non void non empty ManySortedSign, X be non-empty ManySortedSet of
the carrier of S, v, vk be SortSymbol of S, o be OperSymbol of S, t be Element
of (the Sorts of FreeMSA X).v, a be (ArgumentSeq of Sym(o,X)), k be Element of
NAT, ak be Element of (the Sorts of FreeMSA X).vk;
assume that
A1: t = [o,the carrier of S]-tree a and
A2: k in dom a and
A3: ak = a.k;
reconsider a9 = a as DTree-yielding FinSequence;
A4: (ex dt being finite DecoratedTree, tt being finite Tree st dt = t & tt =
dom dt & depth t = height tt )& ex q being DTree-yielding FinSequence st a9 = q
& dom t = tree doms q by A1,MSAFREE2:def 14,TREES_4:def 4;
reconsider da = doms a as FinTree-yielding FinSequence;
consider dtk being finite DecoratedTree, ttk being finite Tree such that
A5: dtk = ak & ttk = dom dtk and
A6: depth ak = height ttk by MSAFREE2:def 14;
dom doms a9 = dom a9 & ttk = da.k by A2,A3,A5,FUNCT_6:22,TREES_3:37;
then ttk in rng da by A2,FUNCT_1:def 3;
hence thesis by A6,A4,TREES_3:78;
end;