:: MSSCYC_1 semantic presentation
begin
definition
let G be Graph;
redefine mode Chain of G means :Def1: :: MSSCYC_1:def 1
( 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
for b1 being set holds
( b1 is Chain of G iff ( b1 is FinSequence of the carrier' of G & ex p being FinSequence of the carrier of G st p is_vertex_seq_of b1 ) )
proof
let c be FinSequence; ::_thesis: ( c is Chain of G iff ( c is FinSequence of the carrier' of G & ex p being FinSequence of the carrier of G st p is_vertex_seq_of c ) )
hereby ::_thesis: ( c is FinSequence of the carrier' of G & ex p being FinSequence of the carrier of G st p is_vertex_seq_of c implies c is Chain of G )
assume A1: c is Chain of G ; ::_thesis: ( c is FinSequence of the carrier' of G & ex p being FinSequence of the carrier of G st p is_vertex_seq_of c )
then consider p being FinSequence such that
A2: len p = (len c) + 1 and
A3: for n being Element of NAT st 1 <= n & n <= len p holds
p . n in the carrier of G and
A4: for n being Element of NAT st 1 <= n & n <= len c holds
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; ::_thesis: ex p being FinSequence of the carrier of G st p is_vertex_seq_of c
now__::_thesis:_for_i_being_Nat_st_i_in_dom_p_holds_
p_._i_in_the_carrier_of_G
let i be Nat; ::_thesis: ( i in dom p implies p . i in the carrier of G )
assume i in dom p ; ::_thesis: p . i in the carrier of G
then A5: ( 1 <= i & i <= len p ) by FINSEQ_3:25;
i in NAT by ORDINAL1:def_12;
hence p . i in the carrier of G by A3, A5; ::_thesis: verum
end;
then reconsider p = p as FinSequence of the carrier of G by FINSEQ_2:12;
take p = p; ::_thesis: p is_vertex_seq_of c
thus p is_vertex_seq_of c ::_thesis: verum
proof
thus len p = (len c) + 1 by A2; :: according to GRAPH_2:def_6 ::_thesis: for b1 being Element of NAT holds
( not 1 <= b1 or not b1 <= len c or c . b1 joins p /. b1,p /. (b1 + 1) )
let n be Element of NAT ; ::_thesis: ( not 1 <= n or not n <= len c or c . n joins p /. n,p /. (n + 1) )
assume that
A6: 1 <= n and
A7: n <= len c ; ::_thesis: c . n joins p /. n,p /. (n + 1)
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 c . n joins p /. n,p /. (n + 1) by A6, A8, FINSEQ_4:15; ::_thesis: verum
end;
end;
assume A9: c is FinSequence of the carrier' of G ; ::_thesis: ( for p being FinSequence of the carrier of G holds not p is_vertex_seq_of c or c is Chain of G )
given p being FinSequence of the carrier of G such that A10: p is_vertex_seq_of c ; ::_thesis: c is Chain of G
hereby :: according to GRAPH_1:def_14 ::_thesis: ex b1 being set st
( len b1 = (len c) + 1 & ( for b2 being Element of NAT holds
( not 1 <= b2 or not b2 <= len b1 or b1 . b2 in the carrier of G ) ) & ( for b2 being Element of NAT holds
( not 1 <= b2 or not b2 <= len c or ex b3, b4 being Element of the carrier of G st
( b3 = b1 . b2 & b4 = b1 . (b2 + 1) & c . b2 joins b3,b4 ) ) ) )
let n be Element of NAT ; ::_thesis: ( 1 <= n & n <= len c implies c . n in the carrier' of G )
assume ( 1 <= n & n <= len c ) ; ::_thesis: c . n in the carrier' of G
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; ::_thesis: verum
end;
take p ; ::_thesis: ( len p = (len c) + 1 & ( for b1 being Element of NAT holds
( not 1 <= b1 or not b1 <= len p or p . b1 in the carrier of G ) ) & ( for b1 being Element of NAT holds
( not 1 <= b1 or not b1 <= len c or ex b2, b3 being Element of the carrier of G st
( b2 = p . b1 & b3 = p . (b1 + 1) & c . b1 joins b2,b3 ) ) ) )
thus A12: len p = (len c) + 1 by A10, GRAPH_2:def_6; ::_thesis: ( ( for b1 being Element of NAT holds
( not 1 <= b1 or not b1 <= len p or p . b1 in the carrier of G ) ) & ( for b1 being Element of NAT holds
( not 1 <= b1 or not b1 <= len c or ex b2, b3 being Element of the carrier of G st
( b2 = p . b1 & b3 = p . (b1 + 1) & c . b1 joins b2,b3 ) ) ) )
hereby ::_thesis: for b1 being Element of NAT holds
( not 1 <= b1 or not b1 <= len c or ex b2, b3 being Element of the carrier of G st
( b2 = p . b1 & b3 = p . (b1 + 1) & c . b1 joins b2,b3 ) )
let n be Element of NAT ; ::_thesis: ( 1 <= n & n <= len p implies p . n in the carrier of G )
assume ( 1 <= n & n <= len p ) ; ::_thesis: p . n in the carrier of G
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; ::_thesis: verum
end;
let n be Element of NAT ; ::_thesis: ( not 1 <= n or not n <= len c or ex b1, b2 being Element of the carrier of G st
( b1 = p . n & b2 = p . (n + 1) & c . n joins b1,b2 ) )
assume that
A14: 1 <= n and
A15: n <= len c ; ::_thesis: ex b1, b2 being Element of the carrier of G st
( b1 = p . n & b2 = p . (n + 1) & c . n joins b1,b2 )
take x9 = p /. n; ::_thesis: ex b1 being Element of the carrier of G st
( x9 = p . n & b1 = p . (n + 1) & c . n joins x9,b1 )
take y9 = p /. (n + 1); ::_thesis: ( x9 = p . n & y9 = p . (n + 1) & c . n joins x9,y9 )
( 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; ::_thesis: c . n joins x9,y9
thus c . n joins x9,y9 by A10, A14, A15, GRAPH_2:def_6; ::_thesis: verum
end;
end;
:: deftheorem Def1 defines Chain MSSCYC_1:def_1_:_
for G being Graph
for b2 being set holds
( b2 is Chain of G iff ( b2 is FinSequence of the carrier' of G & ex p being FinSequence of the carrier of G st p is_vertex_seq_of b2 ) );
theorem :: MSSCYC_1:1
canceled;
theorem :: MSSCYC_1:2
for n being Element of NAT
for p, q being FinSequence st n <= len p holds
(1,n) -cut p = (1,n) -cut (p ^ q)
proof
let n be Element of NAT ; ::_thesis: for p, q being FinSequence st n <= len p holds
(1,n) -cut p = (1,n) -cut (p ^ q)
let p, q be FinSequence; ::_thesis: ( n <= len p implies (1,n) -cut p = (1,n) -cut (p ^ q) )
assume A1: n <= len p ; ::_thesis: (1,n) -cut p = (1,n) -cut (p ^ q)
percases ( n < 1 or 1 <= n ) ;
supposeA2: n < 1 ; ::_thesis: (1,n) -cut p = (1,n) -cut (p ^ q)
then (1,n) -cut p = {} by GRAPH_2:def_1;
hence (1,n) -cut p = (1,n) -cut (p ^ q) by A2, GRAPH_2:def_1; ::_thesis: verum
end;
supposeA3: 1 <= n ; ::_thesis: (1,n) -cut p = (1,n) -cut (p ^ q)
set cp = (1,n) -cut p;
set cpq = (1,n) -cut (p ^ q);
now__::_thesis:_(_len_((1,n)_-cut_p)_=_len_((1,n)_-cut_(p_^_q))_&_(_for_k_being_Nat_st_1_<=_k_&_k_<=_len_((1,n)_-cut_p)_holds_
((1,n)_-cut_p)_._k_=_((1,n)_-cut_(p_^_q))_._k_)_)
A4: (len ((1,n) -cut p)) + 1 = n + 1 by A1, A3, GRAPH_2:def_1;
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 ((1,n) -cut (p ^ q))) + 1 = n + 1 by A3, GRAPH_2:def_1;
hence len ((1,n) -cut p) = len ((1,n) -cut (p ^ q)) by A4; ::_thesis: for k being Nat st 1 <= k & k <= len ((1,n) -cut p) holds
((1,n) -cut p) . k = ((1,n) -cut (p ^ q)) . k
let k be Nat; ::_thesis: ( 1 <= k & k <= len ((1,n) -cut p) implies ((1,n) -cut p) . k = ((1,n) -cut (p ^ q)) . k )
assume that
A7: 1 <= k and
A8: k <= len ((1,n) -cut p) ; ::_thesis: ((1,n) -cut p) . k = ((1,n) -cut (p ^ q)) . k
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 Element of NAT st
( 0 <= i & i < len ((1,n) -cut p) & k = i + 1 ) by A7, A8, GRAPH_2:1;
hence ((1,n) -cut p) . k = p . k by A1, A3, GRAPH_2:def_1
.= (p ^ q) . k by A9, FINSEQ_1:def_7
.= ((1,n) -cut (p ^ q)) . k by A3, A5, A4, A6, A10, GRAPH_2:def_1 ;
::_thesis: verum
end;
hence (1,n) -cut p = (1,n) -cut (p ^ q) by FINSEQ_1:14; ::_thesis: verum
end;
end;
end;
notation
let G be Graph;
let IT be Chain of G;
synonym directed IT for oriented ;
end;
definition
let G be Graph;
let IT be Chain of G;
attrIT is cyclic means :Def2: :: MSSCYC_1:def 2
ex p being FinSequence of the carrier of G st
( p is_vertex_seq_of IT & p . 1 = p . (len p) );
end;
:: deftheorem Def2 defines cyclic MSSCYC_1:def_2_:_
for G being Graph
for IT being Chain of G holds
( IT is cyclic iff ex p being FinSequence of the carrier of G st
( p is_vertex_seq_of IT & p . 1 = p . (len p) ) );
registration
cluster non empty void V54() for MultiGraphStruct ;
existence
ex b1 being Graph st b1 is void
proof
set V = {1};
set E = {} ;
set S = the Function of {},{1};
reconsider G = MultiGraphStruct(# {1},{}, the Function of {},{1}, the Function of {},{1} #) as Graph ;
take G ; ::_thesis: G is void
thus the carrier' of G is empty ; :: according to STRUCT_0:def_13 ::_thesis: verum
end;
end;
theorem Th3: :: MSSCYC_1:3
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; ::_thesis: (rng the Source of G) \/ (rng the Target of G) c= the carrier of G
( 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 (rng the Source of G) \/ (rng the Target of G) c= the carrier of G by XBOOLE_1:8; ::_thesis: verum
end;
registration
cluster non empty non void V54() strict simple connected finite for MultiGraphStruct ;
existence
ex b1 being Graph st
( b1 is finite & b1 is simple & b1 is connected & not b1 is void & b1 is strict )
proof
set V = {1,2};
set E = {1};
( 1 in {1,2} & 2 in {1,2} ) by TARSKI:def_2;
then reconsider S = {1} --> 1, T = {1} --> 2 as Function of {1},{1,2} by FUNCOP_1:45;
reconsider G = MultiGraphStruct(# {1,2},{1},S,T #) as Graph ;
take G ; ::_thesis: ( G is finite & G is simple & G is connected & not G is void & G is strict )
thus G is finite by GRAPH_1:def_11; ::_thesis: ( G is simple & G is connected & not G is void & G is strict )
A1: 1 in {1} by TARSKI:def_1;
then A2: S . 1 = 1 by FUNCOP_1:7;
thus G is simple ::_thesis: ( G is connected & not G is void & G is strict )
proof
given x being set such that A3: x in the carrier' of G and
A4: the Source of G . x = the Target of G . x ; :: according to GRAPH_1:def_9 ::_thesis: contradiction
x = 1 by A3, TARSKI:def_1;
hence contradiction by A1, A2, A4, FUNCOP_1:7; ::_thesis: verum
end;
A5: T . 1 = 2 by A1, FUNCOP_1:7;
thus G is connected ::_thesis: ( not G is void & G is strict )
proof
set MSG = MultiGraphStruct(# the carrier of G, the carrier' of G, the Source of G, the Target 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 ; :: according to GRAPH_1:def_10 ::_thesis: contradiction
A8: MultiGraphStruct(# the carrier of G, the carrier' of G, the Source of G, the Target of G #) = G1 \/ G2 by A7, GRAPH_1:def_6;
set V1 = the carrier of G1;
set V2 = the carrier of G2;
set T1 = the Target of G1;
set T2 = the Target of G2;
set S1 = the Source of G1;
set S2 = the Source of G2;
set E1 = the carrier' of G1;
set E2 = the carrier' of G2;
A9: (rng the Source of G1) \/ (rng the Target of G1) c= the carrier of G1 by Th3;
A10: (rng the Source of G2) \/ (rng the Target of G2) c= the carrier of G2 by Th3;
A11: ( the Target of G1 tolerates the Target of G2 & the Source of G1 tolerates the Source of G2 ) by A7, GRAPH_1:def_6;
then A12: the carrier of MultiGraphStruct(# the carrier of G, the carrier' of G, the Source of G, the Target of G #) = the carrier of G1 \/ the carrier of G2 by A8, GRAPH_1:def_5;
A13: the carrier' of MultiGraphStruct(# the carrier of G, the carrier' of G, the Source of G, the Target of G #) = the carrier' of G1 \/ the carrier' of G2 by A11, A8, GRAPH_1:def_5;
percases ( ( the carrier' of G1 = {1} & the carrier' of G2 = {1} ) or ( the carrier' of G1 = {1} & the carrier' of G2 = {} ) or ( the carrier' of G1 = {} & the carrier' of G2 = {1} ) ) by A13, ZFMISC_1:37;
supposeA14: ( the carrier' of G1 = {1} & the carrier' of G2 = {1} ) ; ::_thesis: contradiction
then the Source of G2 . 1 = S . 1 by A1, A11, A8, GRAPH_1:def_5;
then 1 in rng the Source of G2 by A1, A2, A14, FUNCT_2:4;
then A15: 1 in (rng the Source of G2) \/ (rng the Target of G2) by XBOOLE_0:def_3;
the Source of G1 . 1 = S . 1 by A1, A11, A8, A14, GRAPH_1:def_5;
then 1 in rng the Source of G1 by A1, A2, A14, FUNCT_2:4;
then 1 in (rng the Source of G1) \/ (rng the Target of G1) by XBOOLE_0:def_3;
hence contradiction by A6, A9, A10, A15, XBOOLE_0:3; ::_thesis: verum
end;
supposeA16: ( the carrier' of G1 = {1} & the carrier' of G2 = {} ) ; ::_thesis: contradiction
then the Target of G1 . 1 = T . 1 by A1, A11, A8, GRAPH_1:def_5;
then 2 in rng the Target of G1 by A1, A5, A16, FUNCT_2:4;
then A17: 2 in (rng the Source of G1) \/ (rng the Target of G1) by XBOOLE_0:def_3;
A18: the carrier of G1 c= {1,2} by A12, XBOOLE_1:7;
the Source of G1 . 1 = S . 1 by A1, A11, A8, A16, GRAPH_1:def_5;
then 1 in rng the Source of G1 by A1, A2, A16, FUNCT_2:4;
then 1 in (rng the Source of G1) \/ (rng the Target of G1) by XBOOLE_0:def_3;
then {1,2} c= the carrier of G1 by A9, A17, ZFMISC_1:32;
then {1,2} = the carrier of G1 by A18, XBOOLE_0:def_10;
then the carrier of G2 c= the carrier of G1 by A12, XBOOLE_1:7;
hence contradiction by A6, XBOOLE_1:67; ::_thesis: verum
end;
supposeA19: ( the carrier' of G1 = {} & the carrier' of G2 = {1} ) ; ::_thesis: contradiction
then the Target of G2 . 1 = T . 1 by A1, A11, A8, GRAPH_1:def_5;
then 2 in rng the Target of G2 by A1, A5, A19, FUNCT_2:4;
then A20: 2 in (rng the Source of G2) \/ (rng the Target of G2) by XBOOLE_0:def_3;
A21: the carrier of G2 c= {1,2} by A12, XBOOLE_1:7;
the Source of G2 . 1 = S . 1 by A1, A11, A8, A19, GRAPH_1:def_5;
then 1 in rng the Source of G2 by A1, A2, A19, FUNCT_2:4;
then 1 in (rng the Source of G2) \/ (rng the Target of G2) by XBOOLE_0:def_3;
then {1,2} c= the carrier of G2 by A10, A20, ZFMISC_1:32;
then {1,2} = the carrier of G2 by A21, XBOOLE_0:def_10;
then the carrier of G1 c= the carrier of G2 by A12, XBOOLE_1:7;
hence contradiction by A6, XBOOLE_1:67; ::_thesis: verum
end;
end;
end;
thus not G is void ; ::_thesis: G is strict
thus G is strict ; ::_thesis: verum
end;
end;
theorem Th4: :: MSSCYC_1:4
for G being Graph
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 G be Graph; ::_thesis: 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*>
let e be set ; ::_thesis: 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*>
let s, t be Element of the carrier of G; ::_thesis: ( s = the Source of G . e & t = the Target of G . e implies <*s,t*> is_vertex_seq_of <*e*> )
assume A1: ( s = the Source of G . e & t = the Target of G . e ) ; ::_thesis: <*s,t*> is_vertex_seq_of <*e*>
set c = <*e*>;
set vs = <*s,t*>;
A2: <*s,t*> /. (1 + 1) = t by FINSEQ_4:17;
A3: len <*e*> = 1 by FINSEQ_1:39;
hence len <*s,t*> = (len <*e*>) + 1 by FINSEQ_1:44; :: according to GRAPH_2:def_6 ::_thesis: for b1 being Element of NAT holds
( not 1 <= b1 or not b1 <= len <*e*> or <*e*> . b1 joins <*s,t*> /. b1,<*s,t*> /. (b1 + 1) )
let n be Element of NAT ; ::_thesis: ( not 1 <= n or not n <= len <*e*> or <*e*> . n joins <*s,t*> /. n,<*s,t*> /. (n + 1) )
assume ( 1 <= n & n <= len <*e*> ) ; ::_thesis: <*e*> . n joins <*s,t*> /. n,<*s,t*> /. (n + 1)
then A4: n = 1 by A3, XXREAL_0:1;
( <*e*> . 1 = e & <*s,t*> /. 1 = s ) by FINSEQ_1:40, FINSEQ_4:17;
hence <*e*> . n joins <*s,t*> /. n,<*s,t*> /. (n + 1) by A1, A4, A2, GRAPH_1:def_12; ::_thesis: verum
end;
theorem Th5: :: MSSCYC_1:5
for G being Graph
for e being set st e in the carrier' of G holds
<*e*> is directed Chain of G
proof
let G be Graph; ::_thesis: for e being set st e in the carrier' of G holds
<*e*> is directed Chain of G
let e be set ; ::_thesis: ( e in the carrier' of G implies <*e*> is directed Chain of G )
assume A1: e in the carrier' of G ; ::_thesis: <*e*> is directed Chain 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 = e as Element of E by A1;
<*s,t*> is_vertex_seq_of <*e*> by Th4;
then reconsider c = <*e*> as Chain of G by Def1;
c is directed
proof
let n be Element of NAT ; :: according to GRAPH_1:def_15 ::_thesis: ( not 1 <= n or len c <= n or the Source of G . (c . (n + 1)) = the Target of G . (c . n) )
assume ( 1 <= n & n < len c ) ; ::_thesis: the Source of G . (c . (n + 1)) = the Target of G . (c . n)
hence the Source of G . (c . (n + 1)) = the Target of G . (c . n) by FINSEQ_1:39; ::_thesis: verum
end;
hence <*e*> is directed Chain of G ; ::_thesis: verum
end;
registration
let G be non void Graph;
cluster Relation-like NAT -defined Function-like V14() non empty finite FinSequence-like FinSubsequence-like directed for Chain of G;
existence
ex b1 being Chain of G st
( b1 is directed & not b1 is empty & b1 is V14() )
proof
set e = the Element of the carrier' of G;
reconsider c = <* the Element of the carrier' of G*> as directed Chain of G by Th5;
take c ; ::_thesis: ( c is directed & not c is empty & c is V14() )
thus c is directed ; ::_thesis: ( not c is empty & c is V14() )
thus not c is empty ; ::_thesis: c is V14()
let n, m be Element of NAT ; :: according to GRAPH_1:def_16 ::_thesis: ( not 1 <= n or m <= n or not m <= len c or not c . n = c . m )
assume that
A1: ( 1 <= n & n < m ) and
A2: m <= len c ; ::_thesis: not c . n = c . m
1 < m by A1, XXREAL_0:2;
hence not c . n = c . m by A2, FINSEQ_1:39; ::_thesis: verum
end;
end;
Lm1: for G being Graph
for c being Chain of G
for 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 Graph; ::_thesis: for c being Chain of G
for p being FinSequence of the carrier of G st c is cyclic & p is_vertex_seq_of c holds
p . 1 = p . (len p)
let c be Chain of G; ::_thesis: for p being FinSequence of the carrier of G st c is cyclic & p is_vertex_seq_of c holds
p . 1 = p . (len p)
let p be FinSequence of the carrier of G; ::_thesis: ( c is cyclic & p is_vertex_seq_of c implies p . 1 = p . (len p) )
assume that
A1: c is cyclic and
A2: p is_vertex_seq_of c ; ::_thesis: p . 1 = p . (len p)
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, Def2;
percases ( card the carrier of G = 1 or ( c <> {} & not c alternates_vertices_in G ) or ( not card the carrier of G = 1 & not ( c <> {} & not c alternates_vertices_in G ) ) ) ;
suppose ( card the carrier of G = 1 or ( c <> {} & not c alternates_vertices_in G ) ) ; ::_thesis: p . 1 = p . (len p)
then ( P = vertex-seq c & p = vertex-seq c ) by A2, A3, GRAPH_2:def_8;
hence p . 1 = p . (len p) by A4; ::_thesis: verum
end;
supposeA5: ( not card the carrier of G = 1 & not ( c <> {} & not c alternates_vertices_in G ) ) ; ::_thesis: p . 1 = p . (len p)
A6: len p = (len c) + 1 by A2, GRAPH_2:def_6;
A7: len P = (len c) + 1 by A3, GRAPH_2:def_6;
now__::_thesis:_p_._1_=_p_._(len_p)
percases ( ( card the carrier of G <> 1 & c = {} ) or ( card the carrier of G <> 1 & c alternates_vertices_in G ) ) by A5;
suppose ( card the carrier of G <> 1 & c = {} ) ; ::_thesis: p . 1 = p . (len p)
then len c = 0 ;
hence p . 1 = p . (len p) by A6; ::_thesis: verum
end;
supposeA8: ( card the carrier of G <> 1 & c alternates_vertices_in G ) ; ::_thesis: p . 1 = p . (len p)
then A9: ( p is TwoValued & p is Alternating & P is TwoValued & P is Alternating ) by A2, A3, GRAPH_2:37;
now__::_thesis:_(_p_<>_P_implies_p_._1_=_p_._(len_p)_)
set S = the Source of G;
set T = the Target of G;
assume p <> P ; ::_thesis: p . 1 = p . (len p)
A10: rng p = {( the Source of G . (c . 1)),( the Target of G . (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) = the Source of G . (c . 1) or p . (len p) = the Target of G . (c . 1) ) by A10, TARSKI:def_2;
A13: rng P = {( the Source of G . (c . 1)),( the Target of G . (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 = the Source of G . (c . 1) or P . 1 = the Target of G . (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 = the Source of G . (c . 1) or p . 1 = the Target of G . (c . 1) ) by A10, TARSKI:def_2;
hence p . 1 = p . (len p) by A4, A6, A7, A9, A10, A13, A11, A12, A14, GRAPH_2:21; ::_thesis: verum
end;
hence p . 1 = p . (len p) by A4; ::_thesis: verum
end;
end;
end;
hence p . 1 = p . (len p) ; ::_thesis: verum
end;
end;
end;
theorem Th6: :: MSSCYC_1:6
for G being Graph
for c being Chain of G
for 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 Th7: :: MSSCYC_1:7
for G being Graph
for e being set st e in the carrier' of G holds
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; ::_thesis: for e being set st e in the carrier' of G holds
for fe being directed Chain of G st fe = <*e*> holds
vertex-seq fe = <*( the Source of G . e),( the Target of G . e)*>
let e be set ; ::_thesis: ( e in the carrier' of G implies for fe being directed Chain of G st fe = <*e*> holds
vertex-seq fe = <*( the Source of G . e),( the Target of G . e)*> )
assume e in the carrier' of G ; ::_thesis: for fe being directed Chain of G st fe = <*e*> holds
vertex-seq fe = <*( the Source of G . e),( the Target of G . e)*>
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; ::_thesis: ( fe = <*e*> implies vertex-seq fe = <*( the Source of G . e),( the Target of G . e)*> )
assume A1: fe = <*e*> ; ::_thesis: vertex-seq fe = <*( the Source of G . e),( the Target of G . 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; :: according to GRAPH_2:def_6 ::_thesis: for b1 being Element of NAT holds
( not 1 <= b1 or not b1 <= len fe or fe . b1 joins sota /. b1,sota /. (b1 + 1) )
let n be Element of NAT ; ::_thesis: ( not 1 <= n or not n <= len fe or fe . n joins sota /. n,sota /. (n + 1) )
A4: sota /. 2 = ta by FINSEQ_4:17;
assume ( 1 <= n & n <= len fe ) ; ::_thesis: fe . n joins sota /. n,sota /. (n + 1)
then A5: n = 1 by A2, XXREAL_0:1;
( e joins so,ta & sota /. 1 = so ) by FINSEQ_4:17, GRAPH_1:def_12;
hence fe . n joins sota /. n,sota /. (n + 1) by A1, A5, A4, FINSEQ_1:40; ::_thesis: verum
end;
e = fe . 1 by A1, FINSEQ_1:40;
then sota . 1 = the Source of G . (fe . 1) by FINSEQ_1:44;
hence vertex-seq fe = <*( the Source of G . e),( the Target of G . e)*> by A1, A3, GRAPH_2:def_10; ::_thesis: verum
end;
theorem :: MSSCYC_1:8
for m, n being Element of NAT
for f being FinSequence holds len ((m,n) -cut f) <= len f
proof
let m, n be Element of NAT ; ::_thesis: for f being FinSequence holds len ((m,n) -cut f) <= len f
let f be FinSequence; ::_thesis: len ((m,n) -cut f) <= len f
set lmnf = len ((m,n) -cut f);
set lf = len f;
percases ( ( 1 <= m & m <= n & n <= len f ) or not 1 <= m or not m <= n or not n <= len f ) ;
supposeA1: ( 1 <= m & m <= n & n <= len f ) ; ::_thesis: len ((m,n) -cut f) <= len f
then (len ((m,n) -cut f)) + m = n + 1 by GRAPH_2:def_1;
then n + ((len ((m,n) -cut f)) + m) <= (n + 1) + (len f) by A1, XREAL_1:6;
then n + ((len ((m,n) -cut f)) + m) <= n + (1 + (len f)) ;
then (len ((m,n) -cut f)) + m <= 1 + (len f) by XREAL_1:6;
then ((len ((m,n) -cut f)) + m) + 1 <= m + (1 + (len f)) by A1, XREAL_1:7;
then (len ((m,n) -cut f)) + (m + 1) <= (m + 1) + (len f) ;
hence len ((m,n) -cut f) <= len f by XREAL_1:6; ::_thesis: verum
end;
suppose ( not 1 <= m or not m <= n or not n <= len f ) ; ::_thesis: len ((m,n) -cut f) <= len f
then (m,n) -cut f is empty by GRAPH_2:def_1;
hence len ((m,n) -cut f) <= len f ; ::_thesis: verum
end;
end;
end;
theorem :: MSSCYC_1:9
for m, n being Element of NAT
for G being non void Graph
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 m, n be Element of NAT ; ::_thesis: for G being non void Graph
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
let G be non void Graph; ::_thesis: 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
let c be directed Chain of G; ::_thesis: ( 1 <= m & m <= n & n <= len c implies (m,n) -cut c is directed Chain of G )
assume that
A1: 1 <= m and
A2: m <= n and
A3: n <= len c ; ::_thesis: (m,n) -cut c is directed Chain of G
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, GRAPH_2:def_1;
now__::_thesis:_for_k_being_Element_of_NAT_st_1_<=_k_&_k_<_len_mnc_holds_
the_Source_of_G_._(mnc_._(k_+_1))_=_the_Target_of_G_._(mnc_._k)
A5: (len mnc) + m <= (len c) + 1 by A3, A4, XREAL_1:6;
let k be Element of NAT ; ::_thesis: ( 1 <= k & k < len mnc implies the Source of G . (mnc . (k + 1)) = the Target of G . (mnc . k) )
assume that
A6: 1 <= k and
A7: k < len mnc ; ::_thesis: the Source of G . (mnc . (k + 1)) = the Target of G . (mnc . k)
0 + 1 <= k by A6;
then consider i being Element of NAT such that
0 <= i and
A8: i < len mnc and
A9: k = i + 1 by A7, GRAPH_2:1;
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, GRAPH_2:def_1;
( mnc . (i + 1) = c . (m + i) & m + k = (m + i) + 1 ) by A1, A2, A3, A8, A9, GRAPH_2:def_1;
hence the Source of G . (mnc . (k + 1)) = the Target of G . (mnc . k) by A12, A10, A11, GRAPH_1:def_15; ::_thesis: verum
end;
hence (m,n) -cut c is directed Chain of G by GRAPH_1:def_15; ::_thesis: verum
end;
theorem Th10: :: MSSCYC_1:10
for G being non void Graph
for oc being non empty directed Chain of G holds len (vertex-seq oc) = (len oc) + 1
proof
let G be non void Graph; ::_thesis: for oc being non empty directed Chain of G holds len (vertex-seq oc) = (len oc) + 1
let oc be non empty directed Chain of G; ::_thesis: len (vertex-seq oc) = (len oc) + 1
vertex-seq oc is_vertex_seq_of oc by GRAPH_2:def_10;
hence len (vertex-seq oc) = (len oc) + 1 by GRAPH_2:def_6; ::_thesis: verum
end;
registration
let G be non void Graph;
let oc be non empty directed Chain of G;
cluster vertex-seq oc -> non empty ;
coherence
not vertex-seq oc is empty
proof
len (vertex-seq oc) = (len oc) + 1 by Th10;
hence not vertex-seq oc is empty ; ::_thesis: verum
end;
end;
theorem Th11: :: MSSCYC_1:11
for G being non void Graph
for oc being non empty directed Chain of G
for n being Element of NAT 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 G be non void Graph; ::_thesis: for oc being non empty directed Chain of G
for n being Element of NAT 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) )
let oc be non empty directed Chain of G; ::_thesis: for n being Element of NAT 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) )
set vsoc = vertex-seq oc;
set S = the Source of G;
set T = the Target of G;
defpred S1[ Element of NAT ] means ( 1 <= $1 & $1 <= len oc implies ( (vertex-seq oc) . $1 = the Source of G . (oc . $1) & (vertex-seq oc) . ($1 + 1) = the Target of G . (oc . $1) ) );
A1: for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] )
assume A2: ( 1 <= n & n <= len oc implies ( (vertex-seq oc) . n = the Source of G . (oc . n) & (vertex-seq oc) . (n + 1) = the Target of G . (oc . n) ) ) ; ::_thesis: S1[n + 1]
A3: vertex-seq oc is_vertex_seq_of oc by GRAPH_2:def_10;
assume that
A4: 1 <= n + 1 and
A5: n + 1 <= len oc ; ::_thesis: ( (vertex-seq oc) . (n + 1) = the Source of G . (oc . (n + 1)) & (vertex-seq oc) . ((n + 1) + 1) = the Target of G . (oc . (n + 1)) )
percases ( n = 0 or n <> 0 ) ;
supposeA6: n = 0 ; ::_thesis: ( (vertex-seq oc) . (n + 1) = the Source of G . (oc . (n + 1)) & (vertex-seq oc) . ((n + 1) + 1) = the Target of G . (oc . (n + 1)) )
hence A7: (vertex-seq oc) . (n + 1) = the Source of G . (oc . (n + 1)) by GRAPH_2:def_10; ::_thesis: (vertex-seq oc) . ((n + 1) + 1) = the Target of G . (oc . (n + 1))
A8: ( (vertex-seq oc) /. 1 = (vertex-seq oc) /. (1 + 1) or (vertex-seq oc) /. 1 <> (vertex-seq oc) /. (1 + 1) ) ;
1 in dom (vertex-seq oc) by FINSEQ_5:6;
then A9: (vertex-seq oc) /. 1 = (vertex-seq oc) . 1 by PARTFUN1:def_6;
A10: 1 <= len oc by A4, A5, XXREAL_0:2;
len (vertex-seq oc) = (len oc) + 1 by Th10;
then 1 + 1 <= len (vertex-seq oc) by A10, XREAL_1:6;
then 1 + 1 in dom (vertex-seq oc) by FINSEQ_3:25;
then A11: (vertex-seq oc) /. (1 + 1) = (vertex-seq oc) . (1 + 1) by PARTFUN1:def_6;
oc . 1 joins (vertex-seq oc) /. 1,(vertex-seq oc) /. (1 + 1) by A3, A10, GRAPH_2:def_6;
hence (vertex-seq oc) . ((n + 1) + 1) = the Target of G . (oc . (n + 1)) by A6, A7, A8, A9, A11, GRAPH_1:def_12; ::_thesis: verum
end;
supposeA12: n <> 0 ; ::_thesis: ( (vertex-seq oc) . (n + 1) = the Source of G . (oc . (n + 1)) & (vertex-seq oc) . ((n + 1) + 1) = the Target of G . (oc . (n + 1)) )
A13: n < len oc by A5, NAT_1:13;
1 <= n by A12, NAT_1:14;
hence A14: (vertex-seq oc) . (n + 1) = the Source of G . (oc . (n + 1)) by A2, A13, GRAPH_1:def_15; ::_thesis: (vertex-seq oc) . ((n + 1) + 1) = the Target of G . (oc . (n + 1))
A15: ( (vertex-seq oc) /. (n + 1) = (vertex-seq oc) /. ((n + 1) + 1) or (vertex-seq oc) /. (n + 1) <> (vertex-seq oc) /. ((n + 1) + 1) ) ;
A16: len (vertex-seq oc) = (len oc) + 1 by Th10;
then ( 1 <= (n + 1) + 1 & (n + 1) + 1 <= len (vertex-seq oc) ) by A5, NAT_1:11, XREAL_1:6;
then (n + 1) + 1 in dom (vertex-seq oc) by FINSEQ_3:25;
then A17: (vertex-seq oc) /. ((n + 1) + 1) = (vertex-seq oc) . ((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 (vertex-seq oc) by A16, XREAL_1:6;
then n + 1 in dom (vertex-seq oc) by A4, FINSEQ_3:25;
then A18: (vertex-seq oc) /. (n + 1) = (vertex-seq oc) . (n + 1) by PARTFUN1:def_6;
oc . (n + 1) joins (vertex-seq oc) /. (n + 1),(vertex-seq oc) /. ((n + 1) + 1) by A4, A5, A3, GRAPH_2:def_6;
hence (vertex-seq oc) . ((n + 1) + 1) = the Target of G . (oc . (n + 1)) by A14, A15, A18, A17, GRAPH_1:def_12; ::_thesis: verum
end;
end;
end;
A19: S1[ 0 ] ;
thus for n being Element of NAT holds S1[n] from NAT_1:sch_1(A19, A1); ::_thesis: verum
end;
theorem Th12: :: MSSCYC_1:12
for m, n being Element of NAT
for f being non empty FinSequence st 1 <= m & m <= n & n <= len f holds
not (m,n) -cut f is empty
proof
let m, n be Element of NAT ; ::_thesis: for f being non empty FinSequence st 1 <= m & m <= n & n <= len f holds
not (m,n) -cut f is empty
let f be non empty FinSequence; ::_thesis: ( 1 <= m & m <= n & n <= len f implies not (m,n) -cut f is empty )
set lmn = len ((m,n) -cut f);
assume ( 1 <= m & m <= n & n <= len f ) ; ::_thesis: not (m,n) -cut f is empty
then ( m < n + 1 & (len ((m,n) -cut f)) + m = n + 1 ) by GRAPH_2:def_1, NAT_1:13;
then m - ((len ((m,n) -cut f)) + m) < (n + 1) - (n + 1) by XREAL_1:9;
then - (- (len ((m,n) -cut f))) > 0 ;
hence not (m,n) -cut f is empty ; ::_thesis: verum
end;
theorem :: MSSCYC_1:13
for m, n being Element of NAT
for G being non void Graph
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 m, n be Element of NAT ; ::_thesis: for G being non void Graph
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)
let G be non void Graph; ::_thesis: 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)
let c, c1 be directed Chain of G; ::_thesis: ( 1 <= m & m <= n & n <= len c & c1 = (m,n) -cut c implies vertex-seq c1 = (m,(n + 1)) -cut (vertex-seq c) )
assume that
A1: 1 <= m and
A2: m <= n and
A3: n <= len c and
A4: c1 = (m,n) -cut c ; ::_thesis: vertex-seq c1 = (m,(n + 1)) -cut (vertex-seq c)
set mn1c = (m,(n + 1)) -cut (vertex-seq c);
A5: not c is empty by A1, A2, A3;
then A6: vertex-seq c is_vertex_seq_of c by GRAPH_2:def_10;
then A7: (m,(n + 1)) -cut (vertex-seq c) 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 (vertex-seq c) = (len c) + 1 by A6, GRAPH_2:def_6;
then A10: n + 1 <= len (vertex-seq c) by A3, XREAL_1:6;
A11: not c1 is empty by A1, A2, A3, A4, A5, Th12;
then 0 < len c1 ;
then A12: c1 . (0 + 1) = c . (m + 0) by A1, A2, A3, A4, GRAPH_2:def_1;
A13: m <= n + 1 by A2, NAT_1:12;
not vertex-seq c is empty by A9;
then not (m,(n + 1)) -cut (vertex-seq c) is empty by A1, A8, A10, Th12;
then 0 < len ((m,(n + 1)) -cut (vertex-seq c)) ;
then A14: (vertex-seq c) . (m + 0) = ((m,(n + 1)) -cut (vertex-seq c)) . (0 + 1) by A1, A10, A13, GRAPH_2:def_1;
m <= len c by A2, A3, XXREAL_0:2;
then ((m,(n + 1)) -cut (vertex-seq c)) . 1 = the Source of G . (c1 . 1) by A1, A5, A12, A14, Th11;
hence vertex-seq c1 = (m,(n + 1)) -cut (vertex-seq c) by A7, A11, GRAPH_2:def_10; ::_thesis: verum
end;
theorem Th14: :: MSSCYC_1:14
for G being non void Graph
for oc being non empty directed Chain of G holds (vertex-seq oc) . ((len oc) + 1) = the Target of G . (oc . (len oc))
proof
let G be non void Graph; ::_thesis: for oc being non empty directed Chain of G holds (vertex-seq oc) . ((len oc) + 1) = the Target of G . (oc . (len oc))
let oc be non empty directed Chain of G; ::_thesis: (vertex-seq oc) . ((len oc) + 1) = the Target of G . (oc . (len oc))
1 in dom oc by FINSEQ_5:6;
then 1 <= len oc by FINSEQ_3:25;
hence (vertex-seq oc) . ((len oc) + 1) = the Target of G . (oc . (len oc)) by Th11; ::_thesis: verum
end;
theorem Th15: :: MSSCYC_1:15
for G being non void Graph
for c1, c2 being non empty directed Chain of G holds
( (vertex-seq c1) . ((len c1) + 1) = (vertex-seq c2) . 1 iff c1 ^ c2 is non empty directed Chain of G )
proof
let G be non void Graph; ::_thesis: for c1, c2 being non empty directed Chain of G holds
( (vertex-seq c1) . ((len c1) + 1) = (vertex-seq c2) . 1 iff c1 ^ c2 is non empty directed Chain of G )
let c1, c2 be non empty directed Chain of G; ::_thesis: ( (vertex-seq c1) . ((len c1) + 1) = (vertex-seq c2) . 1 iff c1 ^ c2 is non empty directed Chain of G )
set vsc1 = vertex-seq c1;
set vsc2 = vertex-seq c2;
A1: len (c1 ^ c2) = (len c1) + (len c2) by FINSEQ_1:22;
A2: vertex-seq c1 is_vertex_seq_of c1 by GRAPH_2:def_10;
then A3: ( vertex-seq c2 is_vertex_seq_of c2 & len (vertex-seq c1) = (len c1) + 1 ) by GRAPH_2:def_6, GRAPH_2:def_10;
hereby ::_thesis: ( c1 ^ c2 is non empty directed Chain of G implies (vertex-seq c1) . ((len c1) + 1) = (vertex-seq c2) . 1 )
assume A4: (vertex-seq c1) . ((len c1) + 1) = (vertex-seq c2) . 1 ; ::_thesis: c1 ^ c2 is non empty directed Chain of G
then reconsider c1c2 = c1 ^ c2 as Chain of G by A2, A3, GRAPH_2:43;
c1c2 is directed
proof
let n be Element of NAT ; :: according to GRAPH_1:def_15 ::_thesis: ( not 1 <= n or len c1c2 <= n or the Source of G . (c1c2 . (n + 1)) = the Target of G . (c1c2 . n) )
assume that
A5: 1 <= n and
A6: n < len c1c2 ; ::_thesis: the Source of G . (c1c2 . (n + 1)) = the Target of G . (c1c2 . n)
percases ( n < len c1 or n = len c1 or n > len c1 ) by XXREAL_0:1;
supposeA7: n < len c1 ; ::_thesis: the Source of G . (c1c2 . (n + 1)) = the Target of G . (c1c2 . n)
then ( 1 <= n + 1 & n + 1 <= len c1 ) by NAT_1:11, NAT_1: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 the Source of G . (c1c2 . (n + 1)) = the Target of G . (c1c2 . n) by A5, A7, A8, GRAPH_1:def_15; ::_thesis: verum
end;
supposeA9: n = len c1 ; ::_thesis: the Source of G . (c1c2 . (n + 1)) = the Target of G . (c1c2 . n)
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;
(vertex-seq c1) . ((len c1) + 1) = the Target of G . (c1 . (len c1)) by Th14;
hence the Source of G . (c1c2 . (n + 1)) = the Target of G . (c1c2 . n) by A4, A9, A11, A10, GRAPH_2:def_10; ::_thesis: verum
end;
supposeA12: n > len c1 ; ::_thesis: the Source of G . (c1c2 . (n + 1)) = the Target of G . (c1c2 . n)
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, NAT_1: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 the Source of G . (c1c2 . (n + 1)) = the Target of G . (c1c2 . n) by A17, A15, A16, GRAPH_1:def_15; ::_thesis: verum
end;
end;
end;
hence c1 ^ c2 is non empty directed Chain of G ; ::_thesis: verum
end;
set n = len c1;
assume c1 ^ c2 is non empty directed Chain of G ; ::_thesis: (vertex-seq c1) . ((len c1) + 1) = (vertex-seq c2) . 1
then reconsider c1c2 = c1 ^ c2 as non empty directed Chain of G ;
A18: len c1 < len c1c2 by A1, XREAL_1:29;
A19: len c1 in dom c1 by FINSEQ_5:6;
then A20: c1c2 . (len c1) = c1 . (len c1) by FINSEQ_1:def_7;
1 <= len c1 by A19, FINSEQ_3:25;
then A21: the Source of G . (c1c2 . ((len c1) + 1)) = the Target of G . (c1c2 . (len c1)) by A18, GRAPH_1:def_15;
1 in dom c2 by FINSEQ_5:6;
then A22: c1c2 . ((len c1) + 1) = c2 . 1 by FINSEQ_1:def_7;
(vertex-seq c1) . ((len c1) + 1) = the Target of G . (c1 . (len c1)) by Th14;
hence (vertex-seq c1) . ((len c1) + 1) = (vertex-seq c2) . 1 by A21, A22, A20, GRAPH_2:def_10; ::_thesis: verum
end;
theorem Th16: :: MSSCYC_1:16
for G being non void Graph
for c, c1, c2 being non empty directed 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 G be non void Graph; ::_thesis: for c, c1, c2 being non empty directed 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) )
let c, c1, c2 be non empty directed Chain of G; ::_thesis: ( c = c1 ^ c2 implies ( (vertex-seq c) . 1 = (vertex-seq c1) . 1 & (vertex-seq c) . ((len c) + 1) = (vertex-seq c2) . ((len c2) + 1) ) )
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 Th11;
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 Th11;
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 Th11;
assume A5: c = c1 ^ c2 ; ::_thesis: ( (vertex-seq c) . 1 = (vertex-seq c1) . 1 & (vertex-seq c) . ((len c) + 1) = (vertex-seq c2) . ((len c2) + 1) )
then ( len c2 in dom c2 & len c = (len c1) + (len c2) ) by FINSEQ_1:22, FINSEQ_5:6;
hence ( (vertex-seq c) . 1 = (vertex-seq c1) . 1 & (vertex-seq c) . ((len c) + 1) = (vertex-seq c2) . ((len c2) + 1) ) by A5, A2, A3, A1, A4, FINSEQ_1:def_7; ::_thesis: verum
end;
theorem Th17: :: MSSCYC_1:17
for G being non void Graph
for oc being non empty directed Chain of G st oc is cyclic holds
(vertex-seq oc) . 1 = (vertex-seq oc) . ((len oc) + 1)
proof
let G be non void Graph; ::_thesis: for oc being non empty directed Chain of G st oc is cyclic holds
(vertex-seq oc) . 1 = (vertex-seq oc) . ((len oc) + 1)
let oc be non empty directed Chain of G; ::_thesis: ( oc is cyclic implies (vertex-seq oc) . 1 = (vertex-seq oc) . ((len oc) + 1) )
assume A1: oc is cyclic ; ::_thesis: (vertex-seq oc) . 1 = (vertex-seq oc) . ((len oc) + 1)
set vsoc = vertex-seq oc;
A2: vertex-seq oc is_vertex_seq_of oc by GRAPH_2:def_10;
then len (vertex-seq oc) = (len oc) + 1 by GRAPH_2:def_6;
hence (vertex-seq oc) . 1 = (vertex-seq oc) . ((len oc) + 1) by A1, A2, Th6; ::_thesis: verum
end;
theorem Th18: :: MSSCYC_1:18
for G being non void Graph
for c being non empty directed Chain of G st c is cyclic holds
for n being Element of NAT ex ch being directed Chain of G st
( len ch = n & ch ^ c is non empty directed Chain of G )
proof
let G be non void Graph; ::_thesis: for c being non empty directed Chain of G st c is cyclic holds
for n being Element of NAT ex ch being directed Chain of G st
( len ch = n & ch ^ c is non empty directed Chain of G )
let c be non empty directed Chain of G; ::_thesis: ( c is cyclic implies for n being Element of NAT ex ch being directed Chain of G st
( len ch = n & ch ^ c is non empty directed Chain of G ) )
defpred S1[ Element of NAT ] means ex ch being directed Chain of G st
( rng ch c= rng c & len ch = $1 & ch ^ c is non empty directed 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 ; ::_thesis: for n being Element of NAT ex ch being directed Chain of G st
( len ch = n & ch ^ c is non empty directed Chain of G )
A3: for i being Element of NAT st S1[i] holds
S1[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 Th5;
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 Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] )
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 non empty directed Chain of G ; ::_thesis: S1[n + 1]
percases ( n = 0 or n <> 0 ) ;
supposeA11: n = 0 ; ::_thesis: S1[n + 1]
take ch9 ; ::_thesis: ( rng ch9 c= rng c & len ch9 = n + 1 & ch9 ^ c is non empty directed Chain of G )
thus rng ch9 c= rng c by A4, A5, ZFMISC_1:31; ::_thesis: ( len ch9 = n + 1 & ch9 ^ c is non empty directed Chain of G )
thus len ch9 = n + 1 by A11, FINSEQ_1:39; ::_thesis: ch9 ^ c is non empty directed Chain of G
set vsch9 = vertex-seq ch9;
vertex-seq ch9 = <*( the Source of G . clc),( the Target of G . clc)*> by Th7;
then (vertex-seq ch9) . ((len ch9) + 1) = the Target of G . clc by A7, FINSEQ_1:44
.= (vertex-seq c) . ((len c) + 1) by Th14
.= (vertex-seq c) . 1 by A2, Th17 ;
hence ch9 ^ c is non empty directed Chain of G by Th15; ::_thesis: verum
end;
suppose n <> 0 ; ::_thesis: S1[n + 1]
then A12: not ch is 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__::_thesis:_ex_ch1_being_directed_Chain_of_G_st_
(_rng_ch1_c=_rng_c_&_len_ch1_=_n_+_1_&_ch1_^_c_is_non_empty_directed_Chain_of_G_)
percases ( i = 1 or i <> 1 ) ;
supposeA17: i = 1 ; ::_thesis: ex ch1 being directed Chain of G st
( rng ch1 c= rng c & len ch1 = n + 1 & ch1 ^ c is non empty directed Chain of G )
set vsch9 = vertex-seq ch9;
vertex-seq ch9 = <*( the Source of G . clc),( the Target of G . clc)*> by Th7;
then (vertex-seq ch9) . ((len ch9) + 1) = the Target of G . clc by A7, FINSEQ_1:44
.= (vertex-seq c) . ((len c) + 1) by Th14
.= (vertex-seq c) . 1 by A2, Th17
.= 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, Th15;
take ch1 = ch1; ::_thesis: ( rng ch1 c= rng c & len ch1 = n + 1 & ch1 ^ c is non empty directed Chain of G )
rng ch1 = (rng ch9) \/ (rng ch) by FINSEQ_1:31;
hence rng ch1 c= rng c by A8, A6, XBOOLE_1:8; ::_thesis: ( len ch1 = n + 1 & ch1 ^ c is non empty directed Chain of G )
thus len ch1 = n + 1 by A9, A7, FINSEQ_1:22; ::_thesis: ch1 ^ c is non empty directed Chain of G
(vertex-seq ch1) . ((len ch1) + 1) = (vertex-seq ch) . ((len ch) + 1) by A12, Th16
.= (vertex-seq c) . 1 by A10, A12, Th15 ;
hence ch1 ^ c is non empty directed Chain of G by Th15; ::_thesis: verum
end;
suppose i <> 1 ; ::_thesis: ex ch1 being directed Chain of G st
( rng ch1 c= rng c & len ch1 = n + 1 & ch1 ^ c is non empty directed Chain of G )
then 1 < i by A16, XXREAL_0:1;
then 1 + 1 <= i by NAT_1:13;
then consider k being Element of NAT such that
A18: ( 1 <= k & k < len c ) and
A19: i = k + 1 by A15, GRAPH_2:1;
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 Th5;
set vsch9 = vertex-seq ch9;
A21: len ch9 = 1 by FINSEQ_1:39;
vertex-seq ch9 = <*( the Source of G . ck),( the Target of G . ck)*> by Th7;
then (vertex-seq ch9) . ((len ch9) + 1) = the Target of G . ck by A21, FINSEQ_1:44
.= 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, Th15;
take ch1 = ch1; ::_thesis: ( rng ch1 c= rng c & len ch1 = n + 1 & ch1 ^ c is non empty directed Chain of G )
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; ::_thesis: ( len ch1 = n + 1 & ch1 ^ c is non empty directed Chain of G )
thus len ch1 = n + 1 by A9, A21, FINSEQ_1:22; ::_thesis: ch1 ^ c is non empty directed Chain of G
(vertex-seq ch1) . ((len ch1) + 1) = (vertex-seq ch) . ((len ch) + 1) by A12, Th16
.= (vertex-seq c) . 1 by A10, A12, Th15 ;
hence ch1 ^ c is non empty directed Chain of G by Th15; ::_thesis: verum
end;
end;
end;
hence S1[n + 1] ; ::_thesis: verum
end;
end;
end;
let n be Element of NAT ; ::_thesis: ex ch being directed Chain of G st
( len ch = n & ch ^ c is non empty directed Chain of G )
A23: S1[ 0 ]
proof
reconsider ch = {} as empty Chain of G by GRAPH_1:14;
reconsider ch = ch as directed Chain of G ;
take ch ; ::_thesis: ( rng ch c= rng c & len ch = 0 & ch ^ c is non empty directed Chain of G )
rng ch = {} ;
hence rng ch c= rng c by XBOOLE_1:2; ::_thesis: ( len ch = 0 & ch ^ c is non empty directed Chain of G )
thus len ch = 0 ; ::_thesis: ch ^ c is non empty directed Chain of G
thus ch ^ c is non empty directed Chain of G by FINSEQ_1:34; ::_thesis: verum
end;
for n being Element of NAT holds S1[n] from NAT_1:sch_1(A23, A3);
then ex ch being directed Chain of G st
( rng ch c= rng c & len ch = n & ch ^ c is non empty directed Chain of G ) ;
hence ex ch being directed Chain of G st
( len ch = n & ch ^ c is non empty directed Chain of G ) ; ::_thesis: verum
end;
definition
let IT be Graph;
attrIT is directed_cycle-less means :Def3: :: MSSCYC_1:def 3
for dc being directed Chain of IT st not dc is empty holds
not dc is cyclic ;
end;
:: deftheorem Def3 defines directed_cycle-less MSSCYC_1:def_3_:_
for IT being Graph holds
( IT is directed_cycle-less iff for dc being directed Chain of IT st not dc is empty holds
not dc is cyclic );
notation
let IT be Graph;
antonym with_directed_cycle IT for directed_cycle-less ;
end;
registration
cluster non empty void -> directed_cycle-less for MultiGraphStruct ;
coherence
for b1 being Graph st b1 is void holds
b1 is directed_cycle-less
proof
let G be Graph; ::_thesis: ( G is void implies G is directed_cycle-less )
assume A1: G is void ; ::_thesis: G is directed_cycle-less
let c be directed Chain of G; :: according to MSSCYC_1:def_3 ::_thesis: ( not c is empty implies not c is cyclic )
assume A2: not c is empty ; ::_thesis: not c is cyclic
c is FinSequence of the carrier' of G by Def1;
hence not c is cyclic by A1, A2; ::_thesis: verum
end;
end;
definition
let IT be Graph;
attrIT is well-founded means :Def4: :: MSSCYC_1:def 4
for v being Element of the carrier of IT ex n being Element of NAT st
for c being directed Chain of IT st not c is empty & (vertex-seq c) . ((len c) + 1) = v holds
len c <= n;
end;
:: deftheorem Def4 defines well-founded MSSCYC_1:def_4_:_
for IT being Graph holds
( IT is well-founded iff for v being Element of the carrier of IT ex n being Element of NAT st
for c being directed Chain of IT st not c is empty & (vertex-seq c) . ((len c) + 1) = v holds
len c <= n );
registration
let G be void Graph;
cluster -> empty for Chain of G;
coherence
for b1 being Chain of G holds b1 is empty
proof
let c be Chain of G; ::_thesis: c is empty
assume A1: not c is empty ; ::_thesis: contradiction
c is FinSequence of the carrier' of G by Def1;
hence contradiction by A1; ::_thesis: verum
end;
end;
registration
cluster non empty void -> well-founded for MultiGraphStruct ;
coherence
for b1 being Graph st b1 is void holds
b1 is well-founded
proof
let G be Graph; ::_thesis: ( G is void implies G is well-founded )
assume G is void ; ::_thesis: G is well-founded
then reconsider G9 = G as void Graph ;
let v be Element of the carrier of G; :: according to MSSCYC_1:def_4 ::_thesis: ex n being Element of NAT st
for c being directed Chain of G st not c is empty & (vertex-seq c) . ((len c) + 1) = v holds
len c <= n
take 0 ; ::_thesis: for c being directed Chain of G st not c is empty & (vertex-seq c) . ((len c) + 1) = v holds
len c <= 0
let c be directed Chain of G; ::_thesis: ( not c is empty & (vertex-seq c) . ((len c) + 1) = v implies len c <= 0 )
reconsider c = c as Chain of G9 ;
c is empty ;
hence ( not c is empty & (vertex-seq c) . ((len c) + 1) = v implies len c <= 0 ) ; ::_thesis: verum
end;
end;
registration
cluster non empty non well-founded -> non void for MultiGraphStruct ;
coherence
for b1 being Graph st not b1 is well-founded holds
not b1 is void ;
end;
registration
cluster non empty V54() well-founded for MultiGraphStruct ;
existence
ex b1 being Graph st b1 is well-founded
proof
set G = the void Graph;
the void Graph is well-founded ;
hence ex b1 being Graph st b1 is well-founded ; ::_thesis: verum
end;
end;
registration
cluster non empty well-founded -> directed_cycle-less for MultiGraphStruct ;
coherence
for b1 being Graph st b1 is well-founded holds
b1 is directed_cycle-less
proof
let G be Graph; ::_thesis: ( G is well-founded implies G is directed_cycle-less )
percases ( G is void or not G is void ) ;
suppose G is void ; ::_thesis: ( G is well-founded implies G is directed_cycle-less )
then reconsider G = G as void Graph ;
G is directed_cycle-less ;
hence ( G is well-founded implies G is directed_cycle-less ) ; ::_thesis: verum
end;
suppose not G is void ; ::_thesis: ( G is well-founded implies G is directed_cycle-less )
then reconsider G9 = G as non void Graph ;
assume that
A1: G is well-founded and
A2: not G is directed_cycle-less ; ::_thesis: contradiction
consider dc being directed Chain of G9 such that
A3: not dc is empty and
A4: dc is cyclic by A2, Def3;
set p = vertex-seq dc;
len (vertex-seq dc) = (len dc) + 1 by A3, Th10;
then 1 <= len (vertex-seq dc) by NAT_1:11;
then 1 in dom (vertex-seq dc) by FINSEQ_3:25;
then reconsider v = (vertex-seq dc) . 1 as Element of the carrier of G by FINSEQ_2:11;
consider n being Element of NAT such that
A5: for c being directed Chain of G9 st not c is empty & (vertex-seq c) . ((len c) + 1) = v holds
len c <= n by A1, Def4;
consider ch being directed Chain of G9 such that
A6: len ch = n + 1 and
A7: ch ^ dc is non empty directed Chain of G9 by A3, A4, Th18;
reconsider ch = ch as non empty directed Chain of G9 by A6;
reconsider cc = ch ^ dc as non empty directed Chain of G9 by A7;
(vertex-seq dc) . 1 = (vertex-seq dc) . ((len dc) + 1) by A3, A4, Th17;
then (vertex-seq cc) . ((len cc) + 1) = v by A3, Th16;
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; ::_thesis: verum
end;
end;
end;
end;
registration
cluster non empty V54() non well-founded for MultiGraphStruct ;
existence
not for b1 being Graph holds b1 is well-founded
proof
set V = {1};
set E = {1};
reconsider j = 1 as Element of {1} by TARSKI:def_1;
reconsider S = {1} --> j, T = {1} --> j as Function of {1},{1} ;
reconsider G = MultiGraphStruct(# {1},{1},S,T #) as Graph ;
reconsider v = 1 as Element of the carrier of G ;
take G ; ::_thesis: not G is well-founded
A1: S . 1 = 1 by FUNCOP_1:7;
A2: G is with_directed_cycle
proof
reconsider dc = <*1*> as directed Chain of G by Th5;
take dc ; :: according to MSSCYC_1:def_3 ::_thesis: ( not dc is empty & dc is cyclic )
thus not dc is empty ; ::_thesis: dc is cyclic
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, Th4, FINSEQ_1:44;
hence dc is cyclic by A3, Def2; ::_thesis: verum
end;
assume G is well-founded ; ::_thesis: contradiction
then reconsider G = G as well-founded Graph ;
G is directed_cycle-less ;
hence contradiction by A2; ::_thesis: verum
end;
end;
registration
cluster non empty V54() directed_cycle-less for MultiGraphStruct ;
existence
ex b1 being Graph st b1 is directed_cycle-less
proof
set G = the well-founded Graph;
the well-founded Graph is directed_cycle-less ;
hence ex b1 being Graph st b1 is directed_cycle-less ; ::_thesis: verum
end;
end;
theorem :: MSSCYC_1:19
for t being DecoratedTree
for p being Node of t
for k being Element of NAT holds p | k is Node of t
proof
let t be DecoratedTree; ::_thesis: for p being Node of t
for k being Element of NAT holds p | k is Node of t
let p be Node of t; ::_thesis: for k being Element of NAT holds p | k is Node of t
let k be Element of NAT ; ::_thesis: p | k is Node of t
p | k = p | (Seg k) by FINSEQ_1:def_15;
then p | k is_a_prefix_of p by TREES_1:def_1;
hence p | k is Node of t by TREES_1:20; ::_thesis: verum
end;
begin
theorem :: MSSCYC_1:20
for S being non empty non void ManySortedSign
for X being V2() ManySortedSet of the carrier of S
for t being Term of S,X st not t is root holds
ex o being OperSymbol of S st t . {} = [o, the carrier of S]
proof
let S be non empty non void ManySortedSign ; ::_thesis: for X being V2() ManySortedSet of the carrier of S
for t being Term of S,X st not t is root holds
ex o being OperSymbol of S st t . {} = [o, the carrier of S]
let X be V2() ManySortedSet of the carrier of S; ::_thesis: for t being Term of S,X st not t is root holds
ex o being OperSymbol of S st t . {} = [o, the carrier of S]
let t be Term of S,X; ::_thesis: ( not t is root implies ex o being OperSymbol of S st t . {} = [o, the carrier of S] )
assume A1: not t is root ; ::_thesis: ex o being OperSymbol of S st t . {} = [o, the carrier of S]
percases ( ex s being SortSymbol of S ex v being Element of X . s st t . {} = [v,s] or t . {} in [: the carrier' of S,{ the carrier of S}:] ) by MSATERM:2;
suppose ex s being SortSymbol of S ex v being Element of X . s st t . {} = [v,s] ; ::_thesis: ex o being OperSymbol of S st t . {} = [o, the carrier of 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 ex o being OperSymbol of S st t . {} = [o, the carrier of S] by A1; ::_thesis: verum
end;
suppose t . {} in [: the carrier' of S,{ the carrier of S}:] ; ::_thesis: ex o being OperSymbol of S st t . {} = [o, the carrier of S]
then consider o, c being set 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 = o as OperSymbol of S by A3;
take o ; ::_thesis: t . {} = [o, the carrier of S]
thus t . {} = [o, the carrier of S] by A4, TARSKI:def_1; ::_thesis: verum
end;
end;
end;
theorem Th21: :: MSSCYC_1:21
for S being non empty non void ManySortedSign
for A being MSAlgebra over S
for G being GeneratorSet of A
for B being MSSubset of A st G c= B holds
B is GeneratorSet of A
proof
let S be non empty non void ManySortedSign ; ::_thesis: for A being MSAlgebra over S
for G being GeneratorSet of A
for B being MSSubset of A st G c= B holds
B is GeneratorSet of A
let A be MSAlgebra over S; ::_thesis: for G being GeneratorSet of A
for B being MSSubset of A st G c= B holds
B is GeneratorSet of A
let G be GeneratorSet of A; ::_thesis: for B being MSSubset of A st G c= B holds
B is GeneratorSet of A
let B be MSSubset of A; ::_thesis: ( G c= B implies B is GeneratorSet 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 ; ::_thesis: B is GeneratorSet of A
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; :: according to MSAFREE:def_4 ::_thesis: verum
end;
registration
let S be non empty non void ManySortedSign ;
let A be non-empty finitely-generated MSAlgebra over S;
cluster Relation-like V2() the carrier of S -defined Function-like non empty V25() total for GeneratorSet of A;
existence
ex b1 being GeneratorSet of A st
( b1 is V2() & b1 is V25() )
proof
consider G being GeneratorSet of A such that
A1: G is V25() 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 H1( set ) -> set = {(B . S)};
consider C being ManySortedSet of the carrier of S such that
A3: for i being set st i in the carrier of S holds
C . i = H1(i) from PBOOLE:sch_4();
set H = G \/ C;
now__::_thesis:_for_i_being_set_st_i_in_the_carrier_of_S_holds_
C_._i_c=_the_Sorts_of_A_._i
let i be set ; ::_thesis: ( i in the carrier of S implies C . i c= the Sorts of A . i )
assume A4: i in the carrier of S ; ::_thesis: C . i c= the Sorts of A . i
then B . i in the Sorts of A . i by A2, PBOOLE:def_1;
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; ::_thesis: verum
end;
then ( G c= the Sorts of A & C c= the Sorts of A ) by PBOOLE:def_2, PBOOLE:def_18;
then A5: ( C c= G \/ C & G \/ C c= the Sorts of A ) by PBOOLE:14, PBOOLE:16;
now__::_thesis:_for_i_being_set_st_i_in_the_carrier_of_S_holds_
not_C_._i_is_empty
let i be set ; ::_thesis: ( i in the carrier of S implies not C . i is empty )
assume i in the carrier of S ; ::_thesis: not C . i is empty
then C . i = {(B . i)} by A3;
hence not C . i is empty ; ::_thesis: verum
end;
then C is V2() by PBOOLE:def_13;
then reconsider H = G \/ C as V2() MSSubset of A by A5, PBOOLE:131, PBOOLE:def_18;
G c= H by PBOOLE:14;
then reconsider H = H as GeneratorSet of A by Th21;
take H ; ::_thesis: ( H is V2() & H is V25() )
thus H is V2() ; ::_thesis: H is V25()
let i be set ; :: according to FINSET_1:def_5 ::_thesis: ( not i in the carrier of S or H . i is finite )
assume A6: i in the carrier of S ; ::_thesis: H . i is finite
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 H . i is finite by A7, A8; ::_thesis: verum
end;
end;
theorem Th22: :: MSSCYC_1:22
for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S
for X being V2() GeneratorSet of A ex F being ManySortedFunction of (FreeMSA X),A st F is_epimorphism FreeMSA X,A
proof
let S be non empty non void ManySortedSign ; ::_thesis: for A being non-empty MSAlgebra over S
for X being V2() GeneratorSet of A ex F being ManySortedFunction of (FreeMSA X),A st F is_epimorphism FreeMSA X,A
let A be non-empty MSAlgebra over S; ::_thesis: for X being V2() GeneratorSet of A ex F being ManySortedFunction of (FreeMSA X),A st F is_epimorphism FreeMSA X,A
let X be V2() GeneratorSet of A; ::_thesis: ex F being ManySortedFunction of (FreeMSA X),A st F is_epimorphism FreeMSA X,A
reconsider X9 = X as MSSubset of A ;
now__::_thesis:_for_i_being_set_st_i_in_the_carrier_of_S_holds_
(Reverse_X)_._i_is_Function_of_((FreeGen_X)_._i),(_the_Sorts_of_A_._i)
let i be set ; ::_thesis: ( i in the carrier of S implies (Reverse X) . i is Function of ((FreeGen X) . i),( the Sorts of A . i) )
assume A1: i in the carrier of S ; ::_thesis: (Reverse X) . i is Function of ((FreeGen X) . i),( the Sorts of A . i)
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, PBOOLE:def_2;
hence (Reverse X) . i is Function of ((FreeGen X) . i),( the Sorts of A . i) by A1, A2, FUNCT_2:7; ::_thesis: verum
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 by MSAFREE:def_5;
take h ; ::_thesis: h is_epimorphism FreeMSA X,A
thus h is_homomorphism FreeMSA X,A by A3; :: according to MSUALG_3:def_8 ::_thesis: h is "onto"
let i be set ; :: according to MSUALG_3:def_3 ::_thesis: ( not i in the carrier of S or proj2 (h . i) = the Sorts of A . i )
assume i in the carrier of S ; ::_thesis: proj2 (h . i) = the Sorts of A . i
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, MSUALG_3:def_8;
then A8: Image g = Image h by A6, MSUALG_3:19;
X is MSSubset of (Image h)
proof
let i be set ; :: according to PBOOLE:def_2,PBOOLE:def_18 ::_thesis: ( not i in the carrier of S or X . i c= the Sorts of (Image h) . i )
assume A9: i in the carrier of S ; ::_thesis: X . i c= the Sorts of (Image h) . i
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 set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X . i or x in the Sorts of (Image h) . i )
FreeGen X c= the Sorts of (FreeMSA X) by PBOOLE:def_18;
then A11: (FreeGen X) . s c= the Sorts of (FreeMSA X) . s by PBOOLE:def_2;
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 ; ::_thesis: x in the Sorts of (Image h) . i
then consider c being set 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 x in the Sorts of (Image h) . i by A12, A11, A16, FUNCT_1:def_6; ::_thesis: verum
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 = (h . s) .: ( 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 proj2 (h . i) = the Sorts of A . i by A18, A8, RELSET_1:22; ::_thesis: verum
end;
theorem :: MSSCYC_1:23
for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S
for X being V2() GeneratorSet of A st not A is finite-yielding holds
not FreeMSA X is finite-yielding
proof
let S be non empty non void ManySortedSign ; ::_thesis: for A being non-empty MSAlgebra over S
for X being V2() GeneratorSet of A st not A is finite-yielding holds
not FreeMSA X is finite-yielding
let A be non-empty MSAlgebra over S; ::_thesis: for X being V2() GeneratorSet of A st not A is finite-yielding holds
not FreeMSA X is finite-yielding
let X be V2() GeneratorSet of A; ::_thesis: ( not A is finite-yielding implies not FreeMSA X is finite-yielding )
assume that
A1: not A is finite-yielding and
A2: FreeMSA X is finite-yielding ; ::_thesis: contradiction
the Sorts of A is V25() by A1, MSAFREE2:def_11;
then consider i being set such that
A3: i in the carrier of S and
A4: the Sorts of A . i is infinite by FINSET_1:def_5;
the Sorts of (FreeMSA X) is V25() 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 Th22;
reconsider i = i as Element of S by A3;
reconsider Fi = F . i as Function of FXi,SAi ;
F is "onto" by A6, MSUALG_3:def_8;
then rng Fi = SAi by MSUALG_3:def_3;
hence contradiction by A4, A5; ::_thesis: verum
end;
registration
let S be non empty non void ManySortedSign ;
let X be V2() V25() ManySortedSet of the carrier of S;
let v be SortSymbol of S;
cluster FreeGen (v,X) -> finite ;
coherence
FreeGen (v,X) is finite
proof
A1: X . v, FreeGen (v,X) are_equipotent
proof
set Z = { [a,(root-tree [a,v])] where a is Element of X . v : verum } ;
take { [a,(root-tree [a,v])] where a is Element of X . v : verum } ; :: according to TARSKI:def_6 ::_thesis: ( ( for b1 being set holds
( not b1 in X . v or ex b2 being set st
( b2 in FreeGen (v,X) & [b1,b2] in { [a,(root-tree [a,v])] where a is Element of X . v : verum } ) ) ) & ( for b1 being set holds
( not b1 in FreeGen (v,X) or ex b2 being set st
( b2 in X . v & [b2,b1] in { [a,(root-tree [a,v])] where a is Element of X . v : verum } ) ) ) & ( for b1, b2, b3, b4 being set holds
( not [b1,b2] in { [a,(root-tree [a,v])] where a is Element of X . v : verum } or not [b3,b4] in { [a,(root-tree [a,v])] where a is Element of X . v : verum } or ( ( not b1 = b3 or b2 = b4 ) & ( not b2 = b4 or b1 = b3 ) ) ) ) )
hereby ::_thesis: ( ( for b1 being set holds
( not b1 in FreeGen (v,X) or ex b2 being set st
( b2 in X . v & [b2,b1] in { [a,(root-tree [a,v])] where a is Element of X . v : verum } ) ) ) & ( for b1, b2, b3, b4 being set holds
( not [b1,b2] in { [a,(root-tree [a,v])] where a is Element of X . v : verum } or not [b3,b4] in { [a,(root-tree [a,v])] where a is Element of X . v : verum } or ( ( not b1 = b3 or b2 = b4 ) & ( not b2 = b4 or b1 = b3 ) ) ) ) )
let x be set ; ::_thesis: ( x in X . v implies ex y being set st
( y in FreeGen (v,X) & [x,y] in { [a,(root-tree [a,v])] where a is Element of X . v : verum } ) )
assume A2: x in X . v ; ::_thesis: ex y being set st
( y in FreeGen (v,X) & [x,y] in { [a,(root-tree [a,v])] where a is Element of X . v : verum } )
reconsider y = root-tree [x,v] as set ;
take y = y; ::_thesis: ( y in FreeGen (v,X) & [x,y] in { [a,(root-tree [a,v])] where a is Element of X . v : verum } )
thus y in FreeGen (v,X) by A2, MSAFREE:def_15; ::_thesis: [x,y] in { [a,(root-tree [a,v])] where a is Element of X . v : verum }
thus [x,y] in { [a,(root-tree [a,v])] where a is Element of X . v : verum } by A2; ::_thesis: verum
end;
hereby ::_thesis: for b1, b2, b3, b4 being set holds
( not [b1,b2] in { [a,(root-tree [a,v])] where a is Element of X . v : verum } or not [b3,b4] in { [a,(root-tree [a,v])] where a is Element of X . v : verum } or ( ( not b1 = b3 or b2 = b4 ) & ( not b2 = b4 or b1 = b3 ) ) )
let y be set ; ::_thesis: ( y in FreeGen (v,X) implies ex x being set st
( x in X . v & [x,y] in { [a,(root-tree [a,v])] where a is Element of X . v : verum } ) )
assume y in FreeGen (v,X) ; ::_thesis: ex x being set st
( x in X . v & [x,y] in { [a,(root-tree [a,v])] where a is Element of X . v : verum } )
then consider x being set such that
A3: x in X . v and
A4: y = root-tree [x,v] by MSAFREE:def_15;
take x = x; ::_thesis: ( x in X . v & [x,y] in { [a,(root-tree [a,v])] where a is Element of X . v : verum } )
thus x in X . v by A3; ::_thesis: [x,y] in { [a,(root-tree [a,v])] where a is Element of X . v : verum }
thus [x,y] in { [a,(root-tree [a,v])] where a is Element of X . v : verum } by A3, A4; ::_thesis: verum
end;
let x, y, z, u be set ; ::_thesis: ( not [x,y] in { [a,(root-tree [a,v])] where a is Element of X . v : verum } or not [z,u] in { [a,(root-tree [a,v])] where a is Element of X . v : verum } or ( ( not x = z or y = u ) & ( not y = u or x = z ) ) )
assume that
A5: [x,y] in { [a,(root-tree [a,v])] where a is Element of X . v : verum } and
A6: [z,u] in { [a,(root-tree [a,v])] where a is Element of X . v : verum } ; ::_thesis: ( ( not x = z or y = u ) & ( not y = u or x = 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; ::_thesis: ( not y = u or x = z )
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 ; ::_thesis: x = z
then [a,v] = [b,v] by A11, A12, TREES_4:4;
hence x = z by A10, A9, XTUPLE_0:1; ::_thesis: verum
end;
thus FreeGen (v,X) is finite by A1, CARD_1:38; ::_thesis: verum
end;
end;
theorem Th24: :: MSSCYC_1:24
for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S
for o being 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 empty non void ManySortedSign ; ::_thesis: for A being non-empty MSAlgebra over S
for o being OperSymbol of S st the Arity of S . o = {} holds
dom (Den (o,A)) = {{}}
let A be non-empty MSAlgebra over S; ::_thesis: for o being OperSymbol of S st the Arity of S . o = {} holds
dom (Den (o,A)) = {{}}
let o be OperSymbol of S; ::_thesis: ( the Arity of S . o = {} implies dom (Den (o,A)) = {{}} )
assume A1: the Arity of S . o = {} ; ::_thesis: dom (Den (o,A)) = {{}}
A2: dom the Arity of S = the carrier' of S by FUNCT_2:def_1;
then ( dom ( the Sorts of A #) = 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)) by FINSEQ_2:def_5
.= product ( the Sorts of A * b) by A1, MSUALG_1:def_1
.= {{}} by CARD_3:10 ; ::_thesis: verum
end;
definition
let IT be non empty non void ManySortedSign ;
attrIT is finitely_operated means :Def5: :: MSSCYC_1:def 5
for s being SortSymbol of IT holds { o where o is OperSymbol of IT : the_result_sort_of o = s } is finite ;
end;
:: deftheorem Def5 defines finitely_operated MSSCYC_1:def_5_:_
for IT being non empty non void ManySortedSign holds
( IT is finitely_operated iff for s being SortSymbol of IT holds { o where o is OperSymbol of IT : the_result_sort_of o = s } is finite );
theorem :: MSSCYC_1:25
for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S
for v being SortSymbol of S st S is finitely_operated holds
Constants (A,v) is finite
proof
let S be non empty non void ManySortedSign ; ::_thesis: for A being non-empty MSAlgebra over S
for v being SortSymbol of S st S is finitely_operated holds
Constants (A,v) is finite
let A be non-empty MSAlgebra over S; ::_thesis: for v being SortSymbol of S st S is finitely_operated holds
Constants (A,v) is finite
let v be SortSymbol of S; ::_thesis: ( S is finitely_operated implies Constants (A,v) is finite )
assume A1: S is finitely_operated ; ::_thesis: Constants (A,v) is finite
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 being 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: { o where o is OperSymbol of S : the_result_sort_of o = v } is finite by A1, Def5;
A4: now__::_thesis:_(_not__{__o_where_o_is_OperSymbol_of_S_:_the_result_sort_of_o_=_v__}__is_empty_implies_Constants_(A,v)_is_finite_)
assume not { o where o is OperSymbol of S : the_result_sort_of o = v } is empty ; ::_thesis: Constants (A,v) is finite
then reconsider Ov = { o where o is OperSymbol of S : the_result_sort_of o = v } as non empty set ;
deffunc H1( Element of the carrier' of S) -> set = (Den ($1,A)) . {};
defpred S1[ Element of Ov] means the Arity of S . $1 = {} ;
set COv = { o where o is Element of Ov : S1[o] } ;
set aCOv = { H1(o) where o is Element of the carrier' of S : o in { o where o is Element of Ov : S1[o] } } ;
A5: Constants (A,v) c= { H1(o) where o is Element of the carrier' of S : o in { o where o is Element of Ov : S1[o] } }
proof
let c be set ; :: according to TARSKI:def_3 ::_thesis: ( not c in Constants (A,v) or c in { H1(o) where o is Element of the carrier' of S : o in { o where o is Element of Ov : S1[o] } } )
assume c in Constants (A,v) ; ::_thesis: c in { H1(o) where o is Element of the carrier' of S : o in { o where o is Element of Ov : S1[o] } }
then consider a being Element of Av such that
A6: a = c and
A7: ex o being 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 { o where o is Element of Ov : S1[o] } by A8;
set f = Den (o,A);
consider x being set such that
A12: x in dom (Den (o,A)) and
A13: a = (Den (o,A)) . x by A10, FUNCT_1:def_3;
dom (Den (o,A)) = {{}} by A8, Th24;
then x = {} by A12, TARSKI:def_1;
hence c in { H1(o) where o is Element of the carrier' of S : o in { o where o is Element of Ov : S1[o] } } by A6, A11, A13; ::_thesis: verum
end;
{ o where o is Element of Ov : S1[o] } is Subset of Ov from DOMAIN_1:sch_7();
then A14: { o where o is Element of Ov : S1[o] } is finite by A3;
{ H1(o) where o is Element of the carrier' of S : o in { o where o is Element of Ov : S1[o] } } is finite from FRAENKEL:sch_21(A14);
hence Constants (A,v) is finite by A5; ::_thesis: verum
end;
now__::_thesis:_(__{__o_where_o_is_OperSymbol_of_S_:_the_result_sort_of_o_=_v__}__is_empty_implies_Constants_(A,v)_is_finite_)
assume A15: { o where o is OperSymbol of S : the_result_sort_of o = v } is empty ; ::_thesis: Constants (A,v) is finite
now__::_thesis:_Constants_(A,v)_is_empty
assume not Constants (A,v) is empty ; ::_thesis: contradiction
then consider c being set 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 being 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 { o where o is OperSymbol of S : the_result_sort_of o = v } by A18;
hence contradiction by A15; ::_thesis: verum
end;
hence Constants (A,v) is finite ; ::_thesis: verum
end;
hence Constants (A,v) is finite by A4; ::_thesis: verum
end;
theorem :: MSSCYC_1:26
for S being non empty non void ManySortedSign
for X being V2() ManySortedSet of the carrier of S
for 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 empty non void ManySortedSign ; ::_thesis: for X being V2() ManySortedSet of the carrier of S
for 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))
let X be V2() ManySortedSet of the carrier of S; ::_thesis: for 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))
let v be SortSymbol of S; ::_thesis: { t where t is Element of the Sorts of (FreeMSA X) . v : depth t = 0 } = (FreeGen (v,X)) \/ (Constants ((FreeMSA X),v))
set SF = the Sorts of (FreeMSA X);
set d0 = { t where t is Element of the Sorts of (FreeMSA X) . v : depth t = 0 } ;
A1: { t where t is Element of the Sorts of (FreeMSA X) . v : depth t = 0 } c= (FreeGen (v,X)) \/ (Constants ((FreeMSA X),v))
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { t where t is Element of the Sorts of (FreeMSA X) . v : depth t = 0 } or x in (FreeGen (v,X)) \/ (Constants ((FreeMSA X),v)) )
assume x in { t where t is Element of the Sorts of (FreeMSA X) . v : depth t = 0 } ; ::_thesis: x in (FreeGen (v,X)) \/ (Constants ((FreeMSA X),v))
then consider t being Element of the Sorts of (FreeMSA X) . v such that
A2: x = t and
A3: depth t = 0 ;
t in the Sorts of (FreeMSA X) . 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 being set st
( x in X . v & a = root-tree [x,v] ) or ex o being 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;
percases ( ex x being set st
( x in X . v & a = root-tree [x,v] ) or ex o being OperSymbol of S st
( [o, the carrier of S] = a . {} & the_result_sort_of o = v ) ) by A5;
suppose ex x being set st
( x in X . v & a = root-tree [x,v] ) ; ::_thesis: x in (FreeGen (v,X)) \/ (Constants ((FreeMSA X),v))
then t in FreeGen (v,X) by A4, MSAFREE:def_15;
hence x in (FreeGen (v,X)) \/ (Constants ((FreeMSA X),v)) by A2, XBOOLE_0:def_3; ::_thesis: verum
end;
suppose ex o being OperSymbol of S st
( [o, the carrier of S] = a . {} & the_result_sort_of o = v ) ; ::_thesis: x in (FreeGen (v,X)) \/ (Constants ((FreeMSA X),v))
then consider o being 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 = the Sorts of (FreeMSA X) . v & Constants ((FreeMSA X),v) = { a1 where a1 is Element of Av : ex o being 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 Th24;
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)) . (<*> (TS (DTConMSA X))) = 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 x in (FreeGen (v,X)) \/ (Constants ((FreeMSA X),v)) by A2, XBOOLE_0:def_3; ::_thesis: verum
end;
end;
end;
A17: Constants ((FreeMSA X),v) c= { t where t is Element of the Sorts of (FreeMSA X) . v : depth t = 0 }
proof
set p = <*> (TS (DTConMSA X));
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Constants ((FreeMSA X),v) or x in { t where t is Element of the Sorts of (FreeMSA X) . v : depth t = 0 } )
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 being 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) ; ::_thesis: x in { t where t is Element of the Sorts of (FreeMSA X) . v : depth t = 0 }
then consider a being Element of Av such that
A20: x = a and
A21: ex o being 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, Th24;
(((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 <*> (TS (DTConMSA X)) in (((FreeSort X) #) * the Arity of S) . o by A24, TARSKI:def_1;
then Sym (o,X) ==> roots (<*> (TS (DTConMSA X))) by MSAFREE:10;
then A25: (DenOp (o,X)) . (<*> (TS (DTConMSA X))) = (Sym (o,X)) -tree (<*> (TS (DTConMSA X))) by MSAFREE:def_12;
reconsider a = a as Element of the Sorts of (FreeMSA X) . v by A18;
consider d being set 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 x in { t where t is Element of the Sorts of (FreeMSA X) . v : depth t = 0 } by A20, A29; ::_thesis: verum
end;
FreeGen (v,X) c= { t where t is Element of the Sorts of (FreeMSA X) . v : depth t = 0 }
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in FreeGen (v,X) or x in { t where t is Element of the Sorts of (FreeMSA X) . v : depth t = 0 } )
assume A31: x in FreeGen (v,X) ; ::_thesis: x in { t where t is Element of the Sorts of (FreeMSA X) . v : depth t = 0 }
then reconsider x9 = x as Element of the Sorts of (FreeMSA X) . 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 x in { t where t is Element of the Sorts of (FreeMSA X) . v : depth t = 0 } by A33; ::_thesis: verum
end;
then (FreeGen (v,X)) \/ (Constants ((FreeMSA X),v)) c= { t where t is Element of the Sorts of (FreeMSA X) . v : depth t = 0 } by A17, XBOOLE_1:8;
hence { t where t is Element of the Sorts of (FreeMSA X) . v : depth t = 0 } = (FreeGen (v,X)) \/ (Constants ((FreeMSA X),v)) by A1, XBOOLE_0:def_10; ::_thesis: verum
end;
theorem :: MSSCYC_1:27
for S being non empty non void ManySortedSign
for X being V2() ManySortedSet of the carrier of S
for v, vk being SortSymbol of S
for o being OperSymbol of S
for t being Element of the Sorts of (FreeMSA X) . v
for a being ArgumentSeq of Sym (o,X)
for k being Element of NAT
for 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 empty non void ManySortedSign ; ::_thesis: for X being V2() ManySortedSet of the carrier of S
for v, vk being SortSymbol of S
for o being OperSymbol of S
for t being Element of the Sorts of (FreeMSA X) . v
for a being ArgumentSeq of Sym (o,X)
for k being Element of NAT
for 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
let X be V2() ManySortedSet of the carrier of S; ::_thesis: for v, vk being SortSymbol of S
for o being OperSymbol of S
for t being Element of the Sorts of (FreeMSA X) . v
for a being ArgumentSeq of Sym (o,X)
for k being Element of NAT
for 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
let v, vk be SortSymbol of S; ::_thesis: for o being OperSymbol of S
for t being Element of the Sorts of (FreeMSA X) . v
for a being ArgumentSeq of Sym (o,X)
for k being Element of NAT
for 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
let o be OperSymbol of S; ::_thesis: for t being Element of the Sorts of (FreeMSA X) . v
for a being ArgumentSeq of Sym (o,X)
for k being Element of NAT
for 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
let t be Element of the Sorts of (FreeMSA X) . v; ::_thesis: for a being ArgumentSeq of Sym (o,X)
for k being Element of NAT
for 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
let a be ArgumentSeq of Sym (o,X); ::_thesis: for k being Element of NAT
for 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
let k be Element of NAT ; ::_thesis: for 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
let ak be Element of the Sorts of (FreeMSA X) . vk; ::_thesis: ( t = [o, the carrier of S] -tree a & k in dom a & ak = a . k implies depth ak < depth t )
assume that
A1: t = [o, the carrier of S] -tree a and
A2: k in dom a and
A3: ak = a . k ; ::_thesis: depth ak < depth t
reconsider a9 = a as DTree-yielding FinSequence ;
A4: ( ex dt being finite DecoratedTree ex 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 depth ak < depth t by A6, A4, TREES_3:78; ::_thesis: verum
end;