:: 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;