:: PRE_CIRC semantic presentation begin scheme :: PRE_CIRC:sch 1 FraenkelFinIm{ F1() -> non empty finite set , F2( set ) -> set , P1[ set ] } : { F2(x) where x is Element of F1() : P1[x] } is finite proof set B = { F2(x) where x is Element of F1() : x in F1() } ; A1: { F2(x) where x is Element of F1() : P1[x] } c= { F2(x) where x is Element of F1() : x in F1() } proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { F2(x) where x is Element of F1() : P1[x] } or a in { F2(x) where x is Element of F1() : x in F1() } ) assume a in { F2(x) where x is Element of F1() : P1[x] } ; ::_thesis: a in { F2(x) where x is Element of F1() : x in F1() } then ex b being Element of F1() st ( F2(b) = a & P1[b] ) ; hence a in { F2(x) where x is Element of F1() : x in F1() } ; ::_thesis: verum end; A2: F1() is finite ; { F2(x) where x is Element of F1() : x in F1() } is finite from FRAENKEL:sch_21(A2); hence { F2(x) where x is Element of F1() : P1[x] } is finite by A1; ::_thesis: verum end; theorem :: PRE_CIRC:1 for f being Function for x, y being set st dom f = {x} & rng f = {y} holds f = {[x,y]} proof let f be Function; ::_thesis: for x, y being set st dom f = {x} & rng f = {y} holds f = {[x,y]} let x, y be set ; ::_thesis: ( dom f = {x} & rng f = {y} implies f = {[x,y]} ) assume ( dom f = {x} & rng f = {y} ) ; ::_thesis: f = {[x,y]} then f = {x} --> y by FUNCOP_1:9; hence f = {[x,y]} by ZFMISC_1:29; ::_thesis: verum end; begin theorem :: PRE_CIRC:2 for I being set for MSS being ManySortedSet of I holds (MSS #) . (<*> I) = {{}} proof let I be set ; ::_thesis: for MSS being ManySortedSet of I holds (MSS #) . (<*> I) = {{}} let MSS be ManySortedSet of I; ::_thesis: (MSS #) . (<*> I) = {{}} reconsider eI = <*> I as Element of I * by FINSEQ_1:49; thus (MSS #) . (<*> I) = product (MSS * eI) by FINSEQ_2:def_5 .= {{}} by CARD_3:10 ; ::_thesis: verum end; scheme :: PRE_CIRC:sch 2 MSSLambda2Part{ F1() -> set , P1[ set ], F2( set ) -> set , F3( set ) -> set } : ex f being ManySortedSet of F1() st for i being Element of F1() st i in F1() holds ( ( P1[i] implies f . i = F2(i) ) & ( P1[i] implies f . i = F3(i) ) ) proof defpred S1[ set , set ] means ( ( P1[\$1] implies \$2 = F2(\$1) ) & ( P1[\$1] implies \$2 = F3(\$1) ) ); A1: now__::_thesis:_for_i_being_set_st_i_in_F1()_holds_ ex_j_being_set_st_S1[i,j] let i be set ; ::_thesis: ( i in F1() implies ex j being set st S1[i,j] ) assume i in F1() ; ::_thesis: ex j being set st S1[i,j] thus ex j being set st S1[i,j] ::_thesis: verum proof percases ( P1[i] or not P1[i] ) ; supposeA2: P1[i] ; ::_thesis: ex j being set st S1[i,j] take F2(i) ; ::_thesis: S1[i,F2(i)] thus S1[i,F2(i)] by A2; ::_thesis: verum end; supposeA3: P1[i] ; ::_thesis: ex j being set st S1[i,j] take F3(i) ; ::_thesis: S1[i,F3(i)] thus S1[i,F3(i)] by A3; ::_thesis: verum end; end; end; end; consider f being ManySortedSet of F1() such that A4: for i being set st i in F1() holds S1[i,f . i] from PBOOLE:sch_3(A1); take f ; ::_thesis: for i being Element of F1() st i in F1() holds ( ( P1[i] implies f . i = F2(i) ) & ( P1[i] implies f . i = F3(i) ) ) thus for i being Element of F1() st i in F1() holds ( ( P1[i] implies f . i = F2(i) ) & ( P1[i] implies f . i = F3(i) ) ) by A4; ::_thesis: verum end; registration let I be set ; cluster Relation-like V2() I -defined Function-like total V41() for set ; existence ex b1 being ManySortedSet of I st ( b1 is V2() & b1 is V41() ) proof reconsider f = I --> {{}} as Function ; reconsider f = f as ManySortedSet of I ; take f ; ::_thesis: ( f is V2() & f is V41() ) thus f is V2() ; ::_thesis: f is V41() thus f is V41() ::_thesis: verum proof let i be set ; :: according to FINSET_1:def_5 ::_thesis: ( not i in I or f . i is finite ) assume i in I ; ::_thesis: f . i is finite hence f . i is finite by FUNCOP_1:7; ::_thesis: verum end; end; end; registration let I be set ; let M be ManySortedSet of I; let A be Subset of I; clusterM | A -> A -defined total for A -defined Function; coherence for b1 being A -defined Function st b1 = M | A holds b1 is total proof set B = M | A; ( dom (M | A) = (dom M) /\ A & dom M = I ) by PARTFUN1:def_2, RELAT_1:61; then dom (M | A) = A by XBOOLE_1:28; hence for b1 being A -defined Function st b1 = M | A holds b1 is total by PARTFUN1:def_2; ::_thesis: verum end; end; registration let I be set ; let M be ManySortedSet of I; let A be Subset of I; clusterM | A -> total ; coherence M | A is total ; end; registration let M be non-empty Function; let A be set ; clusterM | A -> non-empty ; coherence M | A is non-empty proof rng (M | A) c= rng M by RELAT_1:70; hence not {} in rng (M | A) by RELAT_1:def_9; :: according to RELAT_1:def_9 ::_thesis: verum end; end; theorem Th3: :: PRE_CIRC:3 for I being non empty set for B being V2() ManySortedSet of I holds not union (rng B) is empty proof let I be non empty set ; ::_thesis: for B being V2() ManySortedSet of I holds not union (rng B) is empty let B be V2() ManySortedSet of I; ::_thesis: not union (rng B) is empty set i = the Element of I; the Element of I in I ; then the Element of I in dom B by PARTFUN1:def_2; then B . the Element of I in rng B by FUNCT_1:def_3; hence not union (rng B) is empty by ORDERS_1:6; ::_thesis: verum end; theorem Th4: :: PRE_CIRC:4 for I being set holds uncurry (I --> {}) = {} proof let I be set ; ::_thesis: uncurry (I --> {}) = {} percases ( I = {} or I <> {} ) ; suppose I = {} ; ::_thesis: uncurry (I --> {}) = {} hence uncurry (I --> {}) = {} by FUNCT_5:43; ::_thesis: verum end; suppose I <> {} ; ::_thesis: uncurry (I --> {}) = {} then rng (I --> {}) = {{}} by FUNCOP_1:8 .= Funcs ({},{}) by FUNCT_5:57 ; then dom (uncurry (I --> {})) = [:(dom (I --> {})),{}:] by FUNCT_5:26 .= {} by ZFMISC_1:90 ; hence uncurry (I --> {}) = {} ; ::_thesis: verum end; end; end; theorem :: PRE_CIRC:5 for I being non empty set for A being set for B being V2() ManySortedSet of I for F being ManySortedFunction of I --> A,B holds dom (commute F) = A proof let I be non empty set ; ::_thesis: for A being set for B being V2() ManySortedSet of I for F being ManySortedFunction of I --> A,B holds dom (commute F) = A let A be set ; ::_thesis: for B being V2() ManySortedSet of I for F being ManySortedFunction of I --> A,B holds dom (commute F) = A let B be V2() ManySortedSet of I; ::_thesis: for F being ManySortedFunction of I --> A,B holds dom (commute F) = A let F be ManySortedFunction of I --> A,B; ::_thesis: dom (commute F) = A A1: dom B = I by PARTFUN1:def_2; A2: dom F = I by PARTFUN1:def_2; percases ( A is empty or not A is empty ) ; supposeA3: A is empty ; ::_thesis: dom (commute F) = A rng F c= {{}} proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng F or x in {{}} ) assume x in rng F ; ::_thesis: x in {{}} then consider i being set such that A4: ( i in I & x = F . i ) by A2, FUNCT_1:def_3; ( (I --> A) . i = A & x is Function of ((I --> A) . i),(B . i) ) by A4, FUNCOP_1:7, PBOOLE:def_15; then x = {} by A3; hence x in {{}} by TARSKI:def_1; ::_thesis: verum end; then rng F = {{}} by ZFMISC_1:33; then A5: F = I --> {} by A2, FUNCOP_1:9; commute F = curry' (uncurry F) by FUNCT_6:def_10 .= {} by A5, Th4, FUNCT_5:42 ; hence dom (commute F) = A by A3; ::_thesis: verum end; supposeA6: not A is empty ; ::_thesis: dom (commute F) = A rng F c= Funcs (A,(union (rng B))) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng F or x in Funcs (A,(union (rng B))) ) assume x in rng F ; ::_thesis: x in Funcs (A,(union (rng B))) then consider i being set such that A7: i in dom F and A8: x = F . i by FUNCT_1:def_3; (I --> A) . i = A by A2, A7, FUNCOP_1:7; then reconsider x9 = x as Function of A,(B . i) by A2, A7, A8, PBOOLE:def_15; B . i in rng B by A1, A2, A7, FUNCT_1:def_3; then ( rng x9 c= B . i & B . i c= union (rng B) ) by RELAT_1:def_19, ZFMISC_1:74; then A9: rng x9 c= union (rng B) by XBOOLE_1:1; dom x9 = A by A2, A7, FUNCT_2:def_1; hence x in Funcs (A,(union (rng B))) by A9, FUNCT_2:def_2; ::_thesis: verum end; then F in Funcs (I,(Funcs (A,(union (rng B))))) by A2, FUNCT_2:def_2; then commute F in Funcs (A,(Funcs (I,(union (rng B))))) by A6, FUNCT_6:55; then A10: commute F is Function of A,(Funcs (I,(union (rng B)))) by FUNCT_2:66; not union (rng B) is empty by Th3; then not Funcs (I,(union (rng B))) is empty by FUNCT_2:8; hence dom (commute F) = A by A10, FUNCT_2:def_1; ::_thesis: verum end; end; end; scheme :: PRE_CIRC:sch 3 LambdaRecCorrD{ F1() -> non empty set , F2() -> Element of F1(), F3( Nat, Element of F1()) -> Element of F1() } : ( ex f being Function of NAT,F1() st ( f . 0 = F2() & ( for i being Nat holds f . (i + 1) = F3(i,(f . i)) ) ) & ( for f1, f2 being Function of NAT,F1() st f1 . 0 = F2() & ( for i being Nat holds f1 . (i + 1) = F3(i,(f1 . i)) ) & f2 . 0 = F2() & ( for i being Nat holds f2 . (i + 1) = F3(i,(f2 . i)) ) holds f1 = f2 ) ) proof thus ex f being Function of NAT,F1() st ( f . 0 = F2() & ( for i being Nat holds f . (i + 1) = F3(i,(f . i)) ) ) from NAT_1:sch_12(); ::_thesis: for f1, f2 being Function of NAT,F1() st f1 . 0 = F2() & ( for i being Nat holds f1 . (i + 1) = F3(i,(f1 . i)) ) & f2 . 0 = F2() & ( for i being Nat holds f2 . (i + 1) = F3(i,(f2 . i)) ) holds f1 = f2 let f1, f2 be Function of NAT,F1(); ::_thesis: ( f1 . 0 = F2() & ( for i being Nat holds f1 . (i + 1) = F3(i,(f1 . i)) ) & f2 . 0 = F2() & ( for i being Nat holds f2 . (i + 1) = F3(i,(f2 . i)) ) implies f1 = f2 ) assume that A1: f1 . 0 = F2() and A2: for i being Nat holds f1 . (i + 1) = F3(i,(f1 . i)) and A3: f2 . 0 = F2() and A4: for i being Nat holds f2 . (i + 1) = F3(i,(f2 . i)) ; ::_thesis: f1 = f2 thus f1 = f2 from NAT_1:sch_16(A1, A2, A3, A4); ::_thesis: verum end; scheme :: PRE_CIRC:sch 4 LambdaMSFD{ F1() -> non empty set , F2() -> Subset of F1(), F3() -> ManySortedSet of F2(), F4() -> ManySortedSet of F2(), F5( set ) -> set } : ex f being ManySortedFunction of F3(),F4() st for i being Element of F1() st i in F2() holds f . i = F5(i) provided A1: for i being Element of F1() st i in F2() holds F5(i) is Function of (F3() . i),(F4() . i) proof consider f being ManySortedSet of F2() such that A2: for i being set st i in F2() holds f . i = F5(i) from PBOOLE:sch_4(); f is Function-yielding proof let i be set ; :: according to FUNCOP_1:def_6 ::_thesis: ( not i in proj1 f or f . i is set ) assume i in dom f ; ::_thesis: f . i is set then A3: i in F2() by PARTFUN1:def_2; then F5(i) is Function by A1; hence f . i is set by A2, A3; ::_thesis: verum end; then reconsider f = f as ManySortedFunction of F2() ; f is ManySortedFunction of F3(),F4() proof let i be set ; :: according to PBOOLE:def_15 ::_thesis: ( not i in F2() or f . i is Element of bool [:(F3() . i),(F4() . i):] ) assume A4: i in F2() ; ::_thesis: f . i is Element of bool [:(F3() . i),(F4() . i):] then F5(i) is Function of (F3() . i),(F4() . i) by A1; hence f . i is Element of bool [:(F3() . i),(F4() . i):] by A2, A4; ::_thesis: verum end; then reconsider f = f as ManySortedFunction of F3(),F4() ; take f ; ::_thesis: for i being Element of F1() st i in F2() holds f . i = F5(i) thus for i being Element of F1() st i in F2() holds f . i = F5(i) by A2; ::_thesis: verum end; theorem :: PRE_CIRC:6 for I being set for f being V2() ManySortedSet of I for g being Function for s being Element of product f st dom g c= dom f & ( for x being set st x in dom g holds g . x in f . x ) holds s +* g is Element of product f proof let I be set ; ::_thesis: for f being V2() ManySortedSet of I for g being Function for s being Element of product f st dom g c= dom f & ( for x being set st x in dom g holds g . x in f . x ) holds s +* g is Element of product f let f be V2() ManySortedSet of I; ::_thesis: for g being Function for s being Element of product f st dom g c= dom f & ( for x being set st x in dom g holds g . x in f . x ) holds s +* g is Element of product f let g be Function; ::_thesis: for s being Element of product f st dom g c= dom f & ( for x being set st x in dom g holds g . x in f . x ) holds s +* g is Element of product f let s be Element of product f; ::_thesis: ( dom g c= dom f & ( for x being set st x in dom g holds g . x in f . x ) implies s +* g is Element of product f ) assume that A1: dom g c= dom f and A2: for x being set st x in dom g holds g . x in f . x ; ::_thesis: s +* g is Element of product f A3: now__::_thesis:_for_x_being_set_st_x_in_dom_f_holds_ (s_+*_g)_._x_in_f_._x let x be set ; ::_thesis: ( x in dom f implies (s +* g) . b1 in f . b1 ) assume A4: x in dom f ; ::_thesis: (s +* g) . b1 in f . b1 percases ( x in dom g or not x in dom g ) ; supposeA5: x in dom g ; ::_thesis: (s +* g) . b1 in f . b1 then (s +* g) . x = g . x by FUNCT_4:13; hence (s +* g) . x in f . x by A2, A5; ::_thesis: verum end; supposeA6: not x in dom g ; ::_thesis: (s +* g) . b1 in f . b1 A7: ex g9 being Function st ( s = g9 & dom g9 = dom f & ( for x being set st x in dom f holds g9 . x in f . x ) ) by CARD_3:def_5; (s +* g) . x = s . x by A6, FUNCT_4:11; hence (s +* g) . x in f . x by A4, A7; ::_thesis: verum end; end; end; ( dom (s +* g) = (dom s) \/ (dom g) & dom s = dom f ) by CARD_3:9, FUNCT_4:def_1; then dom (s +* g) = dom f by A1, XBOOLE_1:12; hence s +* g is Element of product f by A3, CARD_3:9; ::_thesis: verum end; theorem :: PRE_CIRC:7 for A, B being non empty set for C being V2() ManySortedSet of A for InpFs being ManySortedFunction of A --> B,C for b being Element of B ex c being ManySortedSet of A st ( c = (commute InpFs) . b & c in C ) proof let A, B be non empty set ; ::_thesis: for C being V2() ManySortedSet of A for InpFs being ManySortedFunction of A --> B,C for b being Element of B ex c being ManySortedSet of A st ( c = (commute InpFs) . b & c in C ) let C be V2() ManySortedSet of A; ::_thesis: for InpFs being ManySortedFunction of A --> B,C for b being Element of B ex c being ManySortedSet of A st ( c = (commute InpFs) . b & c in C ) let InpFs be ManySortedFunction of A --> B,C; ::_thesis: for b being Element of B ex c being ManySortedSet of A st ( c = (commute InpFs) . b & c in C ) let b be Element of B; ::_thesis: ex c being ManySortedSet of A st ( c = (commute InpFs) . b & c in C ) A1: dom InpFs = A by PARTFUN1:def_2; dom (uncurry InpFs) = [:A,B:] proof thus dom (uncurry InpFs) c= [:A,B:] :: according to XBOOLE_0:def_10 ::_thesis: [:A,B:] c= dom (uncurry InpFs) proof let i be set ; :: according to TARSKI:def_3 ::_thesis: ( not i in dom (uncurry InpFs) or i in [:A,B:] ) assume i in dom (uncurry InpFs) ; ::_thesis: i in [:A,B:] then consider x being set , g being Function, y being set such that A2: i = [x,y] and A3: x in dom InpFs and A4: g = InpFs . x and A5: y in dom g by FUNCT_5:def_2; g is Function of ((A --> B) . x),(C . x) by A1, A3, A4, PBOOLE:def_15; then dom g = (A --> B) . x by A1, A3, FUNCT_2:def_1; then dom g = B by A1, A3, FUNCOP_1:7; hence i in [:A,B:] by A1, A2, A3, A5, ZFMISC_1:87; ::_thesis: verum end; let i1, i2 be set ; :: according to RELAT_1:def_3 ::_thesis: ( not [i1,i2] in [:A,B:] or [i1,i2] in dom (uncurry InpFs) ) reconsider g = InpFs . ([i1,i2] `1) as Function ; assume A6: [i1,i2] in [:A,B:] ; ::_thesis: [i1,i2] in dom (uncurry InpFs) then A7: [i1,i2] `1 in dom InpFs by A1, MCART_1:10; g is Function of ((A --> B) . ([i1,i2] `1)),(C . ([i1,i2] `1)) by A6, MCART_1:10, PBOOLE:def_15; then dom g = (A --> B) . ([i1,i2] `1) by A1, A7, FUNCT_2:def_1; then dom g = B by A6, FUNCOP_1:7, MCART_1:10; then A8: [i1,i2] `2 in dom g by A6, MCART_1:10; thus [i1,i2] in dom (uncurry InpFs) by A7, A8, FUNCT_5:38; ::_thesis: verum end; then A9: ( commute InpFs = curry' (uncurry InpFs) & ex g being Function st ( (curry' (uncurry InpFs)) . b = g & dom g = A & rng g c= rng (uncurry InpFs) & ( for i being set st i in A holds g . i = (uncurry InpFs) . (i,b) ) ) ) by FUNCT_5:32, FUNCT_6:def_10; then reconsider c = (commute InpFs) . b as ManySortedSet of A by PARTFUN1:def_2, RELAT_1:def_18; take c ; ::_thesis: ( c = (commute InpFs) . b & c in C ) thus c = (commute InpFs) . b ; ::_thesis: c in C let i be set ; :: according to PBOOLE:def_1 ::_thesis: ( not i in A or c . i in C . i ) reconsider h = InpFs . i as Function ; assume A10: i in A ; ::_thesis: c . i in C . i then (A --> B) . i = B by FUNCOP_1:7; then A11: h is Function of B,(C . i) by A10, PBOOLE:def_15; then A12: dom h = B by A10, FUNCT_2:def_1; c . i = (uncurry InpFs) . (i,b) by A9, A10 .= h . b by A1, A10, A12, FUNCT_5:38 ; hence c . i in C . i by A10, A11, FUNCT_2:5; ::_thesis: verum end; theorem :: PRE_CIRC:8 for n being Element of NAT for a being set holds product (n |-> {a}) = {(n |-> a)} proof let n be Element of NAT ; ::_thesis: for a being set holds product (n |-> {a}) = {(n |-> a)} let a be set ; ::_thesis: product (n |-> {a}) = {(n |-> a)} now__::_thesis:_for_i_being_set_holds_ (_(_i_in_product_(n_|->_{a})_implies_i_=_n_|->_a_)_&_(_i_=_n_|->_a_implies_i_in_product_(n_|->_{a})_)_) let i be set ; ::_thesis: ( ( i in product (n |-> {a}) implies i = n |-> a ) & ( i = n |-> a implies i in product (n |-> {a}) ) ) hereby ::_thesis: ( i = n |-> a implies i in product (n |-> {a}) ) assume i in product (n |-> {a}) ; ::_thesis: i = n |-> a then consider g being Function such that A1: i = g and A2: dom g = dom (n |-> {a}) and A3: for x being set st x in dom (n |-> {a}) holds g . x in (n |-> {a}) . x by CARD_3:def_5; A4: dom g = Seg n by A2, FUNCOP_1:13; now__::_thesis:_for_x_being_set_st_x_in_dom_g_holds_ g_._x_=_a let x be set ; ::_thesis: ( x in dom g implies g . x = a ) assume A5: x in dom g ; ::_thesis: g . x = a then g . x in (n |-> {a}) . x by A2, A3; then g . x in {a} by A4, A5, FUNCOP_1:7; hence g . x = a by TARSKI:def_1; ::_thesis: verum end; hence i = n |-> a by A1, A4, FUNCOP_1:11; ::_thesis: verum end; assume A6: i = n |-> a ; ::_thesis: i in product (n |-> {a}) then reconsider g = i as Function ; A7: now__::_thesis:_for_x_being_set_st_x_in_dom_(n_|->_{a})_holds_ g_._x_in_(n_|->_{a})_._x let x be set ; ::_thesis: ( x in dom (n |-> {a}) implies g . x in (n |-> {a}) . x ) assume x in dom (n |-> {a}) ; ::_thesis: g . x in (n |-> {a}) . x then x in Seg n by FUNCOP_1:13; then ( g . x = a & (n |-> {a}) . x = {a} ) by A6, FUNCOP_1:7; hence g . x in (n |-> {a}) . x by TARSKI:def_1; ::_thesis: verum end; dom g = Seg n by A6, FUNCOP_1:13 .= dom (n |-> {a}) by FUNCOP_1:13 ; hence i in product (n |-> {a}) by A7, CARD_3:9; ::_thesis: verum end; hence product (n |-> {a}) = {(n |-> a)} by TARSKI:def_1; ::_thesis: verum end; begin registration let D be non empty set ; cluster -> finite for Element of FinTrees D; coherence for b1 being Element of FinTrees D holds b1 is finite proof let t be Element of FinTrees D; ::_thesis: t is finite dom t is finite ; hence t is finite by FINSET_1:10; ::_thesis: verum end; end; registration let T be finite DecoratedTree; let t be Element of dom T; clusterT | t -> finite ; coherence T | t is finite proof dom (T | t) = (dom T) | t by TREES_2:def_10; hence T | t is finite by FINSET_1:10; ::_thesis: verum end; end; theorem Th9: :: PRE_CIRC:9 for T being finite Tree for p being Element of T holds T | p, { t where t is Element of T : p is_a_prefix_of t } are_equipotent proof let T be finite Tree; ::_thesis: for p being Element of T holds T | p, { t where t is Element of T : p is_a_prefix_of t } are_equipotent let p be Element of T; ::_thesis: T | p, { t where t is Element of T : p is_a_prefix_of t } are_equipotent set X = { t where t is Element of T : p is_a_prefix_of t } ; deffunc H1( Element of T | p) -> FinSequence of NAT = p ^ \$1; consider f being Function such that A1: dom f = T | p and A2: for n being Element of T | p holds f . n = H1(n) from FUNCT_1:sch_4(); take f ; :: according to WELLORD2:def_4 ::_thesis: ( f is one-to-one & proj1 f = T | p & proj2 f = { t where t is Element of T : p is_a_prefix_of t } ) thus f is one-to-one ::_thesis: ( proj1 f = T | p & proj2 f = { t where t is Element of T : p is_a_prefix_of t } ) proof let x be set ; :: according to FUNCT_1:def_4 ::_thesis: for b1 being set holds ( not x in proj1 f or not b1 in proj1 f or not f . x = f . b1 or x = b1 ) let y be set ; ::_thesis: ( not x in proj1 f or not y in proj1 f or not f . x = f . y or x = y ) assume that A3: ( x in dom f & y in dom f ) and A4: f . x = f . y ; ::_thesis: x = y reconsider m = x, n = y as Element of T | p by A1, A3; p ^ m = f . n by A2, A4 .= p ^ n by A2 ; hence x = y by FINSEQ_1:33; ::_thesis: verum end; thus dom f = T | p by A1; ::_thesis: proj2 f = { t where t is Element of T : p is_a_prefix_of t } thus rng f c= { t where t is Element of T : p is_a_prefix_of t } :: according to XBOOLE_0:def_10 ::_thesis: { t where t is Element of T : p is_a_prefix_of t } c= proj2 f proof let i be set ; :: according to TARSKI:def_3 ::_thesis: ( not i in rng f or i in { t where t is Element of T : p is_a_prefix_of t } ) assume i in rng f ; ::_thesis: i in { t where t is Element of T : p is_a_prefix_of t } then consider n being set such that A5: n in dom f and A6: i = f . n by FUNCT_1:def_3; reconsider n = n as Element of T | p by A1, A5; reconsider t = p ^ n as Element of T by TREES_1:def_6; ( f . n = p ^ n & p is_a_prefix_of t ) by A2, TREES_1:1; hence i in { t where t is Element of T : p is_a_prefix_of t } by A6; ::_thesis: verum end; let i be set ; :: according to TARSKI:def_3 ::_thesis: ( not i in { t where t is Element of T : p is_a_prefix_of t } or i in proj2 f ) assume i in { t where t is Element of T : p is_a_prefix_of t } ; ::_thesis: i in proj2 f then A7: ex t being Element of T st ( i = t & p is_a_prefix_of t ) ; then consider n being FinSequence such that A8: i = p ^ n by TREES_1:1; n is FinSequence of NAT by A7, A8, FINSEQ_1:36; then reconsider n = n as Element of T | p by A7, A8, TREES_1:def_6; i = f . n by A2, A8; hence i in proj2 f by A1, FUNCT_1:def_3; ::_thesis: verum end; registration let T be finite DecoratedTree-like Function; let t be Element of dom T; let T1 be finite DecoratedTree; clusterT with-replacement (t,T1) -> finite ; coherence T with-replacement (t,T1) is finite proof dom (T with-replacement (t,T1)) = (dom T) with-replacement (t,(dom T1)) by TREES_2:def_11; hence T with-replacement (t,T1) is finite by FINSET_1:10; ::_thesis: verum end; end; theorem Th10: :: PRE_CIRC:10 for T, T1 being finite Tree for p being Element of T holds T with-replacement (p,T1) = { t where t is Element of T : not p is_a_prefix_of t } \/ { (p ^ t1) where t1 is Element of T1 : verum } proof let T, T1 be finite Tree; ::_thesis: for p being Element of T holds T with-replacement (p,T1) = { t where t is Element of T : not p is_a_prefix_of t } \/ { (p ^ t1) where t1 is Element of T1 : verum } let p be Element of T; ::_thesis: T with-replacement (p,T1) = { t where t is Element of T : not p is_a_prefix_of t } \/ { (p ^ t1) where t1 is Element of T1 : verum } defpred S1[ set ] means verum; defpred S2[ set ] means \$1 = \$1; deffunc H1( FinSequence) -> set = p ^ \$1; set A = { t where t is Element of T : not p is_a_proper_prefix_of t } ; set B = { H1(t1) where t1 is Element of T1 : S2[t1] } ; set C = { t where t is Element of T : not p is_a_prefix_of t } ; set D = { H1(t1) where t1 is Element of T1 : S1[t1] } ; now__::_thesis:_for_x_being_set_holds_ (_(_not_x_in__{__t_where_t_is_Element_of_T_:_not_p_is_a_proper_prefix_of_t__}__or_x_in__{__t_where_t_is_Element_of_T_:_not_p_is_a_prefix_of_t__}__or_x_in_{p}_)_&_(_(_x_in__{__t_where_t_is_Element_of_T_:_not_p_is_a_prefix_of_t__}__or_x_in_{p}_)_implies_x_in__{__t_where_t_is_Element_of_T_:_not_p_is_a_proper_prefix_of_t__}__)_) let x be set ; ::_thesis: ( ( not x in { t where t is Element of T : not p is_a_proper_prefix_of t } or x in { t where t is Element of T : not p is_a_prefix_of t } or x in {p} ) & ( ( x in { t where t is Element of T : not p is_a_prefix_of t } or x in {p} ) implies x in { t where t is Element of T : not p is_a_proper_prefix_of t } ) ) hereby ::_thesis: ( ( x in { t where t is Element of T : not p is_a_prefix_of t } or x in {p} ) implies x in { t where t is Element of T : not p is_a_proper_prefix_of t } ) assume x in { t where t is Element of T : not p is_a_proper_prefix_of t } ; ::_thesis: ( x in { t where t is Element of T : not p is_a_prefix_of t } or x in {p} ) then consider t being Element of T such that A1: x = t and A2: not p is_a_proper_prefix_of t ; ( not p is_a_prefix_of t or t = p ) by A2, XBOOLE_0:def_8; hence ( x in { t where t is Element of T : not p is_a_prefix_of t } or x in {p} ) by A1, TARSKI:def_1; ::_thesis: verum end; assume ( x in { t where t is Element of T : not p is_a_prefix_of t } or x in {p} ) ; ::_thesis: x in { t where t is Element of T : not p is_a_proper_prefix_of t } then ( x = p or ex t being Element of T st ( t = x & not p is_a_prefix_of t ) ) by TARSKI:def_1; then consider t being Element of T such that A3: t = x and A4: ( t = p or not p is_a_prefix_of t ) ; not p is_a_proper_prefix_of t by A4, XBOOLE_0:def_8; hence x in { t where t is Element of T : not p is_a_proper_prefix_of t } by A3; ::_thesis: verum end; then A5: { t where t is Element of T : not p is_a_proper_prefix_of t } = { t where t is Element of T : not p is_a_prefix_of t } \/ {p} by XBOOLE_0:def_3; ( {} is Element of T1 & p ^ {} = p ) by FINSEQ_1:34, TREES_1:22; then A6: p in { H1(t1) where t1 is Element of T1 : S1[t1] } ; A7: for t1 being Element of T1 holds ( S2[t1] iff S1[t1] ) ; { H1(t1) where t1 is Element of T1 : S2[t1] } = { H1(t1) where t1 is Element of T1 : S1[t1] } from FRAENKEL:sch_3(A7); hence T with-replacement (p,T1) = ( { t where t is Element of T : not p is_a_prefix_of t } \/ {p}) \/ { H1(t1) where t1 is Element of T1 : S1[t1] } by A5, TREES_1:32 .= { t where t is Element of T : not p is_a_prefix_of t } \/ ({p} \/ { H1(t1) where t1 is Element of T1 : S1[t1] } ) by XBOOLE_1:4 .= { t where t is Element of T : not p is_a_prefix_of t } \/ { H1(t1) where t1 is Element of T1 : S1[t1] } by A6, ZFMISC_1:40 ; ::_thesis: verum end; theorem Th11: :: PRE_CIRC:11 for T, T1 being finite Tree for p being Element of T for f being FinSequence of NAT st f in T with-replacement (p,T1) & p is_a_prefix_of f holds ex t1 being Element of T1 st f = p ^ t1 proof let T, T1 be finite Tree; ::_thesis: for p being Element of T for f being FinSequence of NAT st f in T with-replacement (p,T1) & p is_a_prefix_of f holds ex t1 being Element of T1 st f = p ^ t1 let p be Element of T; ::_thesis: for f being FinSequence of NAT st f in T with-replacement (p,T1) & p is_a_prefix_of f holds ex t1 being Element of T1 st f = p ^ t1 let f be FinSequence of NAT ; ::_thesis: ( f in T with-replacement (p,T1) & p is_a_prefix_of f implies ex t1 being Element of T1 st f = p ^ t1 ) assume that A1: f in T with-replacement (p,T1) and A2: p is_a_prefix_of f ; ::_thesis: ex t1 being Element of T1 st f = p ^ t1 A3: not f in { t where t is Element of T : not p is_a_prefix_of t } proof assume f in { t where t is Element of T : not p is_a_prefix_of t } ; ::_thesis: contradiction then ex t being Element of T st ( f = t & not p is_a_prefix_of t ) ; hence contradiction by A2; ::_thesis: verum end; T with-replacement (p,T1) = { t where t is Element of T : not p is_a_prefix_of t } \/ { (p ^ t1) where t1 is Element of T1 : verum } by Th10; then f in { (p ^ t1) where t1 is Element of T1 : verum } by A1, A3, XBOOLE_0:def_3; hence ex t1 being Element of T1 st f = p ^ t1 ; ::_thesis: verum end; theorem Th12: :: PRE_CIRC:12 for p being Tree-yielding FinSequence for k being Element of NAT st k + 1 in dom p holds (tree p) | <*k*> = p . (k + 1) proof let p be Tree-yielding FinSequence; ::_thesis: for k being Element of NAT st k + 1 in dom p holds (tree p) | <*k*> = p . (k + 1) let k be Element of NAT ; ::_thesis: ( k + 1 in dom p implies (tree p) | <*k*> = p . (k + 1) ) assume k + 1 in dom p ; ::_thesis: (tree p) | <*k*> = p . (k + 1) then k + 1 <= len p by FINSEQ_3:25; then k < len p by NAT_1:13; hence (tree p) | <*k*> = p . (k + 1) by TREES_3:49; ::_thesis: verum end; theorem :: PRE_CIRC:13 for q being DTree-yielding FinSequence for k being Element of NAT st k + 1 in dom q holds <*k*> in tree (doms q) proof let q be DTree-yielding FinSequence; ::_thesis: for k being Element of NAT st k + 1 in dom q holds <*k*> in tree (doms q) let k be Element of NAT ; ::_thesis: ( k + 1 in dom q implies <*k*> in tree (doms q) ) A1: k < k + 1 by XREAL_1:29; A2: ( dom q = Seg (len q) & Seg (len (doms q)) = dom (doms q) ) by FINSEQ_1:def_3; assume A3: k + 1 in dom q ; ::_thesis: <*k*> in tree (doms q) then k + 1 <= len q by FINSEQ_3:25; then k < len q by A1, XXREAL_0:2; then A4: k < len (doms q) by A2, FINSEQ_1:6, TREES_3:37; dom (doms q) = dom q by TREES_3:37; then (doms q) . (k + 1) is Tree by A3, TREES_3:22; then A5: {} in (doms q) . (k + 1) by TREES_1:22; <*k*> = <*k*> ^ {} by FINSEQ_1:34; hence <*k*> in tree (doms q) by A5, A4, TREES_3:def_15; ::_thesis: verum end; theorem Th14: :: PRE_CIRC:14 for p, q being Tree-yielding FinSequence for k being Element of NAT st len p = len q & k + 1 in dom p & ( for i being Element of NAT st i in dom p & i <> k + 1 holds p . i = q . i ) holds for t being Tree st q . (k + 1) = t holds tree q = (tree p) with-replacement (<*k*>,t) proof let p, q be Tree-yielding FinSequence; ::_thesis: for k being Element of NAT st len p = len q & k + 1 in dom p & ( for i being Element of NAT st i in dom p & i <> k + 1 holds p . i = q . i ) holds for t being Tree st q . (k + 1) = t holds tree q = (tree p) with-replacement (<*k*>,t) let k be Element of NAT ; ::_thesis: ( len p = len q & k + 1 in dom p & ( for i being Element of NAT st i in dom p & i <> k + 1 holds p . i = q . i ) implies for t being Tree st q . (k + 1) = t holds tree q = (tree p) with-replacement (<*k*>,t) ) assume that A1: len p = len q and A2: k + 1 in dom p and A3: for i being Element of NAT st i in dom p & i <> k + 1 holds p . i = q . i ; ::_thesis: for t being Tree st q . (k + 1) = t holds tree q = (tree p) with-replacement (<*k*>,t) let t be Tree; ::_thesis: ( q . (k + 1) = t implies tree q = (tree p) with-replacement (<*k*>,t) ) set o = <*k*>; k + 1 <= len p by A2, FINSEQ_3:25; then A4: k < len p by NAT_1:13; assume A5: q . (k + 1) = t ; ::_thesis: tree q = (tree p) with-replacement (<*k*>,t) A6: now__::_thesis:_for_s_being_FinSequence_of_NAT_holds_ (_(_not_s_in_tree_q_or_(_s_in_tree_p_&_not_<*k*>_is_a_proper_prefix_of_s_)_or_ex_r_being_FinSequence_of_NAT_st_ (_r_in_t_&_s_=_<*k*>_^_r_)_)_&_(_(_(_s_in_tree_p_&_not_<*k*>_is_a_proper_prefix_of_s_)_or_ex_r_being_FinSequence_of_NAT_st_ (_r_in_t_&_s_=_<*k*>_^_r_)_)_implies_s_in_tree_q_)_) let s be FinSequence of NAT ; ::_thesis: ( ( not s in tree q or ( s in tree p & not <*k*> is_a_proper_prefix_of s ) or ex r being FinSequence of NAT st ( r in t & s = <*k*> ^ r ) ) & ( ( ( s in tree p & not <*k*> is_a_proper_prefix_of s ) or ex r being FinSequence of NAT st ( r in t & s = <*k*> ^ r ) ) implies b1 in tree q ) ) hereby ::_thesis: ( ( ( s in tree p & not <*k*> is_a_proper_prefix_of s ) or ex r being FinSequence of NAT st ( r in t & s = <*k*> ^ r ) ) implies b1 in tree q ) assume A7: s in tree q ; ::_thesis: ( ( s in tree p & not <*k*> is_a_proper_prefix_of s ) or ex r being FinSequence of NAT st ( r in t & s = <*k*> ^ r ) ) percases ( s = {} or ex n being Element of NAT ex r being FinSequence st ( n < len q & r in q . (n + 1) & s = <*n*> ^ r ) ) by A7, TREES_3:def_15; suppose s = {} ; ::_thesis: ( ( s in tree p & not <*k*> is_a_proper_prefix_of s ) or ex r being FinSequence of NAT st ( r in t & s = <*k*> ^ r ) ) hence ( ( s in tree p & not <*k*> is_a_proper_prefix_of s ) or ex r being FinSequence of NAT st ( r in t & s = <*k*> ^ r ) ) by TREES_1:22, XBOOLE_1:115; ::_thesis: verum end; suppose ex n being Element of NAT ex r being FinSequence st ( n < len q & r in q . (n + 1) & s = <*n*> ^ r ) ; ::_thesis: ( ( s in tree p & not <*k*> is_a_proper_prefix_of s ) or ex r being FinSequence of NAT st ( r in t & s = <*k*> ^ r ) ) then consider n being Element of NAT , r being FinSequence such that A8: n < len q and A9: r in q . (n + 1) and A10: s = <*n*> ^ r ; now__::_thesis:_(_(_n_=_k_&_ex_r_being_FinSequence_of_NAT_st_ (_r_in_t_&_s_=_<*k*>_^_r_)_)_or_(_n_<>_k_&_s_in_tree_p_&_not_<*k*>_is_a_proper_prefix_of_s_)_) percases ( n = k or n <> k ) ; caseA11: n = k ; ::_thesis: ex r being FinSequence of NAT st ( r in t & s = <*k*> ^ r ) reconsider r = r as FinSequence of NAT by A10, FINSEQ_1:36; take r = r; ::_thesis: ( r in t & s = <*k*> ^ r ) thus ( r in t & s = <*k*> ^ r ) by A5, A9, A10, A11; ::_thesis: verum end; caseA12: n <> k ; ::_thesis: ( s in tree p & not <*k*> is_a_proper_prefix_of s ) ( 1 <= n + 1 & n + 1 <= len p ) by A1, A8, NAT_1:11, NAT_1:13; then n + 1 in dom p by FINSEQ_3:25; then q . (n + 1) = p . (n + 1) by A3, A12, XCMPLX_1:2; hence s in tree p by A1, A8, A9, A10, TREES_3:def_15; ::_thesis: not <*k*> is_a_proper_prefix_of s assume <*k*> is_a_proper_prefix_of s ; ::_thesis: contradiction then <*k*> is_a_prefix_of s by XBOOLE_0:def_8; then ex s1 being FinSequence st s = <*k*> ^ s1 by TREES_1:1; then k = s . 1 by FINSEQ_1:41 .= n by A10, FINSEQ_1:41 ; hence contradiction by A12; ::_thesis: verum end; end; end; hence ( ( s in tree p & not <*k*> is_a_proper_prefix_of s ) or ex r being FinSequence of NAT st ( r in t & s = <*k*> ^ r ) ) ; ::_thesis: verum end; end; end; assume A13: ( ( s in tree p & not <*k*> is_a_proper_prefix_of s ) or ex r being FinSequence of NAT st ( r in t & s = <*k*> ^ r ) ) ; ::_thesis: b1 in tree q percases ( ( s in tree p & not <*k*> is_a_proper_prefix_of s ) or ex r being FinSequence of NAT st ( r in t & s = <*k*> ^ r ) ) by A13; supposethat A14: s in tree p and A15: not <*k*> is_a_proper_prefix_of s ; ::_thesis: b1 in tree q now__::_thesis:_s_in_tree_q percases ( s = {} or ex n being Element of NAT ex r being FinSequence st ( n < len p & r in p . (n + 1) & s = <*n*> ^ r ) ) by A14, TREES_3:def_15; suppose s = {} ; ::_thesis: s in tree q hence s in tree q by TREES_1:22; ::_thesis: verum end; suppose ex n being Element of NAT ex r being FinSequence st ( n < len p & r in p . (n + 1) & s = <*n*> ^ r ) ; ::_thesis: s in tree q then consider n being Element of NAT , r being FinSequence such that A16: n < len p and A17: r in p . (n + 1) and A18: s = <*n*> ^ r ; now__::_thesis:_s_in_tree_q percases ( r = {} or r <> {} ) ; supposeA19: r = {} ; ::_thesis: s in tree q ( 1 <= n + 1 & n + 1 <= len q ) by A1, A16, NAT_1:11, NAT_1:13; then n + 1 in dom q by FINSEQ_3:25; then q . (n + 1) is Tree by TREES_3:22; then r in q . (n + 1) by A19, TREES_1:22; hence s in tree q by A1, A16, A18, TREES_3:def_15; ::_thesis: verum end; supposeA20: r <> {} ; ::_thesis: s in tree q A21: now__::_thesis:_not_n_=_k assume n = k ; ::_thesis: contradiction then ( <*k*> is_a_prefix_of s & not s = <*k*> ) by A18, A20, FINSEQ_1:87, TREES_1:1; hence contradiction by A15, XBOOLE_0:def_8; ::_thesis: verum end; ( 1 <= n + 1 & n + 1 <= len p ) by A16, NAT_1:11, NAT_1:13; then n + 1 in dom p by FINSEQ_3:25; then q . (n + 1) = p . (n + 1) by A3, A21, XCMPLX_1:2; hence s in tree q by A1, A16, A17, A18, TREES_3:def_15; ::_thesis: verum end; end; end; hence s in tree q ; ::_thesis: verum end; end; end; hence s in tree q ; ::_thesis: verum end; suppose ex r being FinSequence of NAT st ( r in t & s = <*k*> ^ r ) ; ::_thesis: b1 in tree q hence s in tree q by A1, A4, A5, TREES_3:def_15; ::_thesis: verum end; end; end; p . (k + 1) is Tree by A2, TREES_3:22; then A22: {} in p . (k + 1) by TREES_1:22; <*k*> = <*k*> ^ {} by FINSEQ_1:34; then <*k*> in tree p by A4, A22, TREES_3:def_15; hence tree q = (tree p) with-replacement (<*k*>,t) by A6, TREES_1:def_9; ::_thesis: verum end; theorem :: PRE_CIRC:15 for e1, e2 being finite DecoratedTree for x being set for k being Element of NAT for p being DTree-yielding FinSequence st <*k*> in dom e1 & e1 = x -tree p holds ex q being DTree-yielding FinSequence st ( e1 with-replacement (<*k*>,e2) = x -tree q & len q = len p & q . (k + 1) = e2 & ( for i being Element of NAT st i in dom p & i <> k + 1 holds q . i = p . i ) ) proof let e1, e2 be finite DecoratedTree; ::_thesis: for x being set for k being Element of NAT for p being DTree-yielding FinSequence st <*k*> in dom e1 & e1 = x -tree p holds ex q being DTree-yielding FinSequence st ( e1 with-replacement (<*k*>,e2) = x -tree q & len q = len p & q . (k + 1) = e2 & ( for i being Element of NAT st i in dom p & i <> k + 1 holds q . i = p . i ) ) let x be set ; ::_thesis: for k being Element of NAT for p being DTree-yielding FinSequence st <*k*> in dom e1 & e1 = x -tree p holds ex q being DTree-yielding FinSequence st ( e1 with-replacement (<*k*>,e2) = x -tree q & len q = len p & q . (k + 1) = e2 & ( for i being Element of NAT st i in dom p & i <> k + 1 holds q . i = p . i ) ) let k be Element of NAT ; ::_thesis: for p being DTree-yielding FinSequence st <*k*> in dom e1 & e1 = x -tree p holds ex q being DTree-yielding FinSequence st ( e1 with-replacement (<*k*>,e2) = x -tree q & len q = len p & q . (k + 1) = e2 & ( for i being Element of NAT st i in dom p & i <> k + 1 holds q . i = p . i ) ) let p be DTree-yielding FinSequence; ::_thesis: ( <*k*> in dom e1 & e1 = x -tree p implies ex q being DTree-yielding FinSequence st ( e1 with-replacement (<*k*>,e2) = x -tree q & len q = len p & q . (k + 1) = e2 & ( for i being Element of NAT st i in dom p & i <> k + 1 holds q . i = p . i ) ) ) assume that A1: <*k*> in dom e1 and A2: e1 = x -tree p ; ::_thesis: ex q being DTree-yielding FinSequence st ( e1 with-replacement (<*k*>,e2) = x -tree q & len q = len p & q . (k + 1) = e2 & ( for i being Element of NAT st i in dom p & i <> k + 1 holds q . i = p . i ) ) consider j being Element of NAT , T being DecoratedTree, w being Node of T such that A3: j < len p and T = p . (j + 1) and A4: <*k*> = <*j*> ^ w by A1, A2, TREES_4:11; consider pp being DTree-yielding FinSequence such that A5: p = pp and A6: dom (x -tree p) = tree (doms pp) by TREES_4:def_4; A7: dom (doms pp) = dom p by A5, TREES_3:37; deffunc H1( Nat) -> set = IFEQ (\$1,(k + 1),e2,(p . \$1)); set o = <*k*>; consider q being FinSequence such that A8: len q = len p and A9: for i being Nat st i in dom q holds q . i = H1(i) from FINSEQ_1:sch_2(); A10: dom q = Seg (len p) by A8, FINSEQ_1:def_3; A11: dom q = dom p by A8, FINSEQ_3:29; now__::_thesis:_for_x_being_set_st_x_in_dom_q_holds_ q_._x_is_DecoratedTree let x be set ; ::_thesis: ( x in dom q implies q . x is DecoratedTree ) assume A12: x in dom q ; ::_thesis: q . x is DecoratedTree then reconsider i = x as Element of NAT ; A13: ( i = k + 1 or i <> k + 1 ) ; q . i = IFEQ (i,(k + 1),e2,(p . i)) by A9, A12; then ( q . i = e2 or q . i = p . i ) by A13, FUNCOP_1:def_8; hence q . x is DecoratedTree by A11, A12, TREES_3:24; ::_thesis: verum end; then reconsider q = q as DTree-yielding FinSequence by TREES_3:24; consider qq being DTree-yielding FinSequence such that A14: q = qq and A15: dom (x -tree q) = tree (doms qq) by TREES_4:def_4; A16: len (doms pp) = len p by A5, TREES_3:38 .= len (doms qq) by A8, A14, TREES_3:38 ; A17: dom p = Seg (len p) by FINSEQ_1:def_3; A18: now__::_thesis:_for_i_being_Element_of_NAT_st_i_in_dom_(doms_pp)_&_i_<>_k_+_1_holds_ (doms_pp)_._i_=_(doms_qq)_._i let i be Element of NAT ; ::_thesis: ( i in dom (doms pp) & i <> k + 1 implies (doms pp) . i = (doms qq) . i ) assume that A19: i in dom (doms pp) and A20: i <> k + 1 ; ::_thesis: (doms pp) . i = (doms qq) . i A21: q . i = IFEQ (i,(k + 1),e2,(p . i)) by A9, A10, A17, A7, A19 .= p . i by A20, FUNCOP_1:def_8 ; reconsider pii = p . i as DecoratedTree by A7, A19, TREES_3:24; thus (doms pp) . i = dom pii by A5, A7, A19, FUNCT_6:22 .= (doms qq) . i by A11, A14, A7, A19, A21, FUNCT_6:22 ; ::_thesis: verum end; reconsider dqq = doms qq as Tree-yielding FinSequence ; take q ; ::_thesis: ( e1 with-replacement (<*k*>,e2) = x -tree q & len q = len p & q . (k + 1) = e2 & ( for i being Element of NAT st i in dom p & i <> k + 1 holds q . i = p . i ) ) <*j*> = <*k*> by A4, FINSEQ_1:88; then A22: j = <*k*> . 1 by FINSEQ_1:def_8 .= k by FINSEQ_1:def_8 ; then ( 1 <= k + 1 & k + 1 <= len p ) by A3, NAT_1:11, NAT_1:13; then A23: k + 1 in dom p by FINSEQ_3:25; then k + 1 in Seg (len p) by FINSEQ_1:def_3; then A24: q . (k + 1) = IFEQ ((k + 1),(k + 1),e2,(p . (k + 1))) by A9, A10 .= e2 by FUNCOP_1:def_8 ; then (doms qq) . (k + 1) = dom e2 by A11, A23, A14, FUNCT_6:22; then A25: dom (x -tree q) = (dom e1) with-replacement (<*k*>,(dom e2)) by A2, A23, A15, A6, A16, A7, A18, Th14; for f being FinSequence of NAT holds ( not f in (dom e1) with-replacement (<*k*>,(dom e2)) or ( not <*k*> is_a_prefix_of f & (x -tree q) . f = e1 . f ) or ex r being FinSequence of NAT st ( r in dom e2 & f = <*k*> ^ r & (x -tree q) . f = e2 . r ) ) proof reconsider o9 = <*k*> as Element of dom e1 by A1; let f be FinSequence of NAT ; ::_thesis: ( not f in (dom e1) with-replacement (<*k*>,(dom e2)) or ( not <*k*> is_a_prefix_of f & (x -tree q) . f = e1 . f ) or ex r being FinSequence of NAT st ( r in dom e2 & f = <*k*> ^ r & (x -tree q) . f = e2 . r ) ) assume A26: f in (dom e1) with-replacement (<*k*>,(dom e2)) ; ::_thesis: ( ( not <*k*> is_a_prefix_of f & (x -tree q) . f = e1 . f ) or ex r being FinSequence of NAT st ( r in dom e2 & f = <*k*> ^ r & (x -tree q) . f = e2 . r ) ) percases ( not o9 is_a_prefix_of f or ex t1 being Element of dom e2 st f = o9 ^ t1 ) by A26, Th11; supposeA27: not o9 is_a_prefix_of f ; ::_thesis: ( ( not <*k*> is_a_prefix_of f & (x -tree q) . f = e1 . f ) or ex r being FinSequence of NAT st ( r in dom e2 & f = <*k*> ^ r & (x -tree q) . f = e2 . r ) ) A28: (x -tree q) . f = e1 . f proof percases ( f = {} or ex w being Element of NAT ex u being FinSequence st ( w < len dqq & u in dqq . (w + 1) & f = <*w*> ^ u ) ) by A15, A25, A26, TREES_3:def_15; supposeA29: f = {} ; ::_thesis: (x -tree q) . f = e1 . f hence (x -tree q) . f = x by TREES_4:def_4 .= e1 . f by A2, A29, TREES_4:def_4 ; ::_thesis: verum end; suppose ex w being Element of NAT ex u being FinSequence st ( w < len dqq & u in dqq . (w + 1) & f = <*w*> ^ u ) ; ::_thesis: (x -tree q) . f = e1 . f then consider w being Element of NAT , u being FinSequence such that A30: w < len (doms q) and A31: u in (doms q) . (w + 1) and A32: f = <*w*> ^ u by A14; reconsider u = u as FinSequence of NAT by A32, FINSEQ_1:36; reconsider ww = <*w*> as FinSequence of NAT ; A33: w + 1 <> k + 1 by A27, A32, TREES_1:1; A34: ex pp being DTree-yielding FinSequence st ( p = pp & dom (x -tree p) = tree (doms pp) ) by TREES_4:def_4; A35: w < len q by A30, TREES_3:38; then A36: (x -tree q) | <*w*> = q . (w + 1) by TREES_4:def_4; ( 1 <= w + 1 & w + 1 <= len p ) by A8, A35, NAT_1:11, NAT_1:13; then A37: w + 1 in dom p by FINSEQ_3:25; then reconsider pw1 = p . (w + 1) as DecoratedTree by TREES_3:24; A38: q . (w + 1) = IFEQ ((w + 1),(k + 1),e2,(p . (w + 1))) by A9, A10, A17, A37 .= p . (w + 1) by A33, FUNCOP_1:def_8 ; w + 1 in dom (doms p) by A37, TREES_3:37; then A39: (dom (x -tree p)) | <*w*> = (doms p) . (w + 1) by A34, Th12 .= dom pw1 by A37, FUNCT_6:22 .= (doms q) . (w + 1) by A11, A37, A38, FUNCT_6:22 ; w + 1 in dom (doms q) by A11, A37, TREES_3:37; then (dom (x -tree q)) | <*w*> = (doms q) . (w + 1) by A14, A15, Th12; hence (x -tree q) . f = ((x -tree q) | ww) . u by A31, A32, TREES_2:def_10 .= ((x -tree p) | ww) . u by A8, A35, A36, A38, TREES_4:def_4 .= e1 . f by A2, A31, A32, A39, TREES_2:def_10 ; ::_thesis: verum end; end; end; assume ( <*k*> is_a_prefix_of f or (x -tree q) . f <> e1 . f ) ; ::_thesis: ex r being FinSequence of NAT st ( r in dom e2 & f = <*k*> ^ r & (x -tree q) . f = e2 . r ) hence ex r being FinSequence of NAT st ( r in dom e2 & f = <*k*> ^ r & (x -tree q) . f = e2 . r ) by A27, A28; ::_thesis: verum end; suppose ex t1 being Element of dom e2 st f = o9 ^ t1 ; ::_thesis: ( ( not <*k*> is_a_prefix_of f & (x -tree q) . f = e1 . f ) or ex r being FinSequence of NAT st ( r in dom e2 & f = <*k*> ^ r & (x -tree q) . f = e2 . r ) ) then consider r being Element of dom e2 such that A40: f = <*k*> ^ r ; assume ( <*k*> is_a_prefix_of f or (x -tree q) . f <> e1 . f ) ; ::_thesis: ex r being FinSequence of NAT st ( r in dom e2 & f = <*k*> ^ r & (x -tree q) . f = e2 . r ) A41: (x -tree q) | <*k*> = q . (k + 1) by A8, A3, A22, TREES_4:def_4; reconsider r = r as FinSequence of NAT ; take r ; ::_thesis: ( r in dom e2 & f = <*k*> ^ r & (x -tree q) . f = e2 . r ) thus A42: r in dom e2 ; ::_thesis: ( f = <*k*> ^ r & (x -tree q) . f = e2 . r ) thus f = <*k*> ^ r by A40; ::_thesis: (x -tree q) . f = e2 . r r in (dom (x -tree q)) | <*k*> by A1, A25, A42, TREES_1:33; hence (x -tree q) . f = e2 . r by A24, A40, A41, TREES_2:def_10; ::_thesis: verum end; end; end; hence e1 with-replacement (<*k*>,e2) = x -tree q by A1, A25, TREES_2:def_11; ::_thesis: ( len q = len p & q . (k + 1) = e2 & ( for i being Element of NAT st i in dom p & i <> k + 1 holds q . i = p . i ) ) thus len q = len p by A8; ::_thesis: ( q . (k + 1) = e2 & ( for i being Element of NAT st i in dom p & i <> k + 1 holds q . i = p . i ) ) thus q . (k + 1) = e2 by A24; ::_thesis: for i being Element of NAT st i in dom p & i <> k + 1 holds q . i = p . i let i be Element of NAT ; ::_thesis: ( i in dom p & i <> k + 1 implies q . i = p . i ) assume i in dom p ; ::_thesis: ( not i <> k + 1 or q . i = p . i ) then q . i = IFEQ (i,(k + 1),e2,(p . i)) by A9, A10, A17; hence ( not i <> k + 1 or q . i = p . i ) by FUNCOP_1:def_8; ::_thesis: verum end; theorem :: PRE_CIRC:16 for T being finite Tree for p being Element of T st p <> {} holds card (T | p) < card T proof let T be finite Tree; ::_thesis: for p being Element of T st p <> {} holds card (T | p) < card T let p be Element of T; ::_thesis: ( p <> {} implies card (T | p) < card T ) reconsider p9 = p as Element of NAT * by FINSEQ_1:def_11; set X = { (p9 ^ n) where n is Element of NAT * : n in T | p } ; A1: T | p, { (p9 ^ n) where n is Element of NAT * : n in T | p } are_equipotent proof deffunc H1( Element of T | p) -> FinSequence of NAT = p9 ^ \$1; consider f being Function such that A2: dom f = T | p and A3: for n being Element of T | p holds f . n = H1(n) from FUNCT_1:sch_4(); take f ; :: according to WELLORD2:def_4 ::_thesis: ( f is one-to-one & proj1 f = T | p & proj2 f = { (p9 ^ n) where n is Element of NAT * : n in T | p } ) thus f is one-to-one ::_thesis: ( proj1 f = T | p & proj2 f = { (p9 ^ n) where n is Element of NAT * : n in T | p } ) proof let x be set ; :: according to FUNCT_1:def_4 ::_thesis: for b1 being set holds ( not x in proj1 f or not b1 in proj1 f or not f . x = f . b1 or x = b1 ) let y be set ; ::_thesis: ( not x in proj1 f or not y in proj1 f or not f . x = f . y or x = y ) assume that A4: ( x in dom f & y in dom f ) and A5: f . x = f . y ; ::_thesis: x = y reconsider m = x, n = y as Element of T | p by A2, A4; p9 ^ m = f . n by A3, A5 .= p9 ^ n by A3 ; hence x = y by FINSEQ_1:33; ::_thesis: verum end; thus dom f = T | p by A2; ::_thesis: proj2 f = { (p9 ^ n) where n is Element of NAT * : n in T | p } thus rng f c= { (p9 ^ n) where n is Element of NAT * : n in T | p } :: according to XBOOLE_0:def_10 ::_thesis: { (p9 ^ n) where n is Element of NAT * : n in T | p } c= proj2 f proof let i be set ; :: according to TARSKI:def_3 ::_thesis: ( not i in rng f or i in { (p9 ^ n) where n is Element of NAT * : n in T | p } ) assume i in rng f ; ::_thesis: i in { (p9 ^ n) where n is Element of NAT * : n in T | p } then consider n being set such that A6: n in dom f and A7: i = f . n by FUNCT_1:def_3; T | p c= NAT * by TREES_1:def_3; then reconsider n = n as Element of NAT * by A2, A6; f . n = p9 ^ n by A2, A3, A6; hence i in { (p9 ^ n) where n is Element of NAT * : n in T | p } by A2, A6, A7; ::_thesis: verum end; let i be set ; :: according to TARSKI:def_3 ::_thesis: ( not i in { (p9 ^ n) where n is Element of NAT * : n in T | p } or i in proj2 f ) assume i in { (p9 ^ n) where n is Element of NAT * : n in T | p } ; ::_thesis: i in proj2 f then consider n being Element of NAT * such that A8: i = p9 ^ n and A9: n in T | p ; reconsider n = n as Element of T | p by A9; i = f . n by A3, A8; hence i in proj2 f by A2, FUNCT_1:def_3; ::_thesis: verum end; then reconsider X = { (p9 ^ n) where n is Element of NAT * : n in T | p } as finite set by CARD_1:38; A10: card X = card (T | p) by A1, CARD_1:5; assume A11: p <> {} ; ::_thesis: card (T | p) < card T A12: X <> T proof assume X = T ; ::_thesis: contradiction then {} in X by TREES_1:22; then ex n being Element of NAT * st ( {} = p9 ^ n & n in T | p ) ; hence contradiction by A11; ::_thesis: verum end; X c= T proof let i be set ; :: according to TARSKI:def_3 ::_thesis: ( not i in X or i in T ) assume i in X ; ::_thesis: i in T then ex n being Element of NAT * st ( i = p9 ^ n & n in T | p ) ; hence i in T by TREES_1:def_6; ::_thesis: verum end; then X c< T by A12, XBOOLE_0:def_8; hence card (T | p) < card T by A10, CARD_2:48; ::_thesis: verum end; theorem Th17: :: PRE_CIRC:17 for T, T1 being finite Tree for p being Element of T holds (card (T with-replacement (p,T1))) + (card (T | p)) = (card T) + (card T1) proof let T, T1 be finite Tree; ::_thesis: for p being Element of T holds (card (T with-replacement (p,T1))) + (card (T | p)) = (card T) + (card T1) let p be Element of T; ::_thesis: (card (T with-replacement (p,T1))) + (card (T | p)) = (card T) + (card T1) defpred S1[ Element of T] means not p is_a_prefix_of \$1; defpred S2[ Element of T] means p is_a_prefix_of \$1; set A = { t where t is Element of T : S1[t] } ; set B = { t where t is Element of T : S2[t] } ; set C = { (p ^ t1) where t1 is Element of T1 : verum } ; A1: { t where t is Element of T : S1[t] } is Subset of T from DOMAIN_1:sch_7(); A2: { t where t is Element of T : S2[t] } is Subset of T from DOMAIN_1:sch_7(); A3: T1, { (p ^ t1) where t1 is Element of T1 : verum } are_equipotent proof deffunc H1( Element of T1) -> FinSequence of NAT = p ^ \$1; consider f being Function such that A4: dom f = T1 and A5: for n being Element of T1 holds f . n = H1(n) from FUNCT_1:sch_4(); take f ; :: according to WELLORD2:def_4 ::_thesis: ( f is one-to-one & proj1 f = T1 & proj2 f = { (p ^ t1) where t1 is Element of T1 : verum } ) thus f is one-to-one ::_thesis: ( proj1 f = T1 & proj2 f = { (p ^ t1) where t1 is Element of T1 : verum } ) proof let x be set ; :: according to FUNCT_1:def_4 ::_thesis: for b1 being set holds ( not x in proj1 f or not b1 in proj1 f or not f . x = f . b1 or x = b1 ) let y be set ; ::_thesis: ( not x in proj1 f or not y in proj1 f or not f . x = f . y or x = y ) assume that A6: ( x in dom f & y in dom f ) and A7: f . x = f . y ; ::_thesis: x = y reconsider m = x, n = y as Element of T1 by A4, A6; p ^ m = f . n by A5, A7 .= p ^ n by A5 ; hence x = y by FINSEQ_1:33; ::_thesis: verum end; thus dom f = T1 by A4; ::_thesis: proj2 f = { (p ^ t1) where t1 is Element of T1 : verum } thus rng f c= { (p ^ t1) where t1 is Element of T1 : verum } :: according to XBOOLE_0:def_10 ::_thesis: { (p ^ t1) where t1 is Element of T1 : verum } c= proj2 f proof let i be set ; :: according to TARSKI:def_3 ::_thesis: ( not i in rng f or i in { (p ^ t1) where t1 is Element of T1 : verum } ) assume i in rng f ; ::_thesis: i in { (p ^ t1) where t1 is Element of T1 : verum } then consider n being set such that A8: n in dom f and A9: i = f . n by FUNCT_1:def_3; T1 c= NAT * by TREES_1:def_3; then reconsider n = n as Element of NAT * by A4, A8; f . n = p ^ n by A4, A5, A8; hence i in { (p ^ t1) where t1 is Element of T1 : verum } by A4, A8, A9; ::_thesis: verum end; let i be set ; :: according to TARSKI:def_3 ::_thesis: ( not i in { (p ^ t1) where t1 is Element of T1 : verum } or i in proj2 f ) assume i in { (p ^ t1) where t1 is Element of T1 : verum } ; ::_thesis: i in proj2 f then consider n being Element of T1 such that A10: i = p ^ n ; i = f . n by A5, A10; hence i in proj2 f by A4, FUNCT_1:def_3; ::_thesis: verum end; reconsider A = { t where t is Element of T : S1[t] } , B = { t where t is Element of T : S2[t] } as finite set by A1, A2; now__::_thesis:_for_x_being_set_holds_ (_(_not_x_in_T_or_x_in_A_or_x_in_B_)_&_(_(_x_in_A_or_x_in_B_)_implies_x_in_T_)_) let x be set ; ::_thesis: ( ( not x in T or x in A or x in B ) & ( ( x in A or x in B ) implies x in T ) ) hereby ::_thesis: ( ( x in A or x in B ) implies x in T ) assume x in T ; ::_thesis: ( x in A or x in B ) then reconsider t = x as Element of T ; ( p is_a_prefix_of t or not p is_a_prefix_of t ) ; hence ( x in A or x in B ) ; ::_thesis: verum end; assume ( x in A or x in B ) ; ::_thesis: x in T hence x in T by A1, A2; ::_thesis: verum end; then A11: T = A \/ B by XBOOLE_0:def_3; A12: A misses { (p ^ t1) where t1 is Element of T1 : verum } proof assume not A misses { (p ^ t1) where t1 is Element of T1 : verum } ; ::_thesis: contradiction then consider x being set such that A13: x in A /\ { (p ^ t1) where t1 is Element of T1 : verum } by XBOOLE_0:4; x in { (p ^ t1) where t1 is Element of T1 : verum } by A13, XBOOLE_0:def_4; then A14: ex t1 being Element of T1 st x = p ^ t1 ; x in A by A13, XBOOLE_0:def_4; then ex t being Element of T st ( x = t & not p is_a_prefix_of t ) ; hence contradiction by A14, TREES_1:1; ::_thesis: verum end; A15: A misses B proof assume not A misses B ; ::_thesis: contradiction then consider x being set such that A16: x in A /\ B by XBOOLE_0:4; x in B by A16, XBOOLE_0:def_4; then A17: ex t being Element of T st ( x = t & p is_a_prefix_of t ) ; x in A by A16, XBOOLE_0:def_4; then ex t being Element of T st ( x = t & not p is_a_prefix_of t ) ; hence contradiction by A17; ::_thesis: verum end; A18: T with-replacement (p,T1) = A \/ { (p ^ t1) where t1 is Element of T1 : verum } by Th10; reconsider C = { (p ^ t1) where t1 is Element of T1 : verum } as finite set by A3, CARD_1:38; A19: card T1 = card C by A3, CARD_1:5; T | p,B are_equipotent by Th9; then card (T | p) = card B by CARD_1:5; hence (card (T with-replacement (p,T1))) + (card (T | p)) = ((card A) + (card C)) + (card B) by A18, A12, CARD_2:40 .= ((card A) + (card B)) + (card C) .= (card T) + (card T1) by A11, A15, A19, CARD_2:40 ; ::_thesis: verum end; theorem :: PRE_CIRC:18 for T, T1 being finite DecoratedTree for p being Element of dom T holds (card (T with-replacement (p,T1))) + (card (T | p)) = (card T) + (card T1) proof let T, T1 be finite DecoratedTree; ::_thesis: for p being Element of dom T holds (card (T with-replacement (p,T1))) + (card (T | p)) = (card T) + (card T1) let p be Element of dom T; ::_thesis: (card (T with-replacement (p,T1))) + (card (T | p)) = (card T) + (card T1) A1: ( card (dom T) = card T & card (dom T1) = card T1 ) by CARD_1:62; A2: ( card (dom (T with-replacement (p,T1))) = card (T with-replacement (p,T1)) & card (dom (T | p)) = card (T | p) ) by CARD_1:62; ( dom (T with-replacement (p,T1)) = (dom T) with-replacement (p,(dom T1)) & dom (T | p) = (dom T) | p ) by TREES_2:def_10, TREES_2:def_11; hence (card (T with-replacement (p,T1))) + (card (T | p)) = (card T) + (card T1) by A1, A2, Th17; ::_thesis: verum end; registration let x be set ; cluster root-tree x -> finite ; coherence root-tree x is finite proof root-tree x = {[{},x]} by TREES_4:6; hence root-tree x is finite ; ::_thesis: verum end; end; theorem :: PRE_CIRC:19 for x being set holds card (root-tree x) = 1 proof let x be set ; ::_thesis: card (root-tree x) = 1 root-tree x = {[{},x]} by TREES_4:6; hence card (root-tree x) = 1 by CARD_1:30; ::_thesis: verum end; begin theorem :: PRE_CIRC:20 for F being non empty finite set holds (card F) - 1 = (card F) -' 1 proof let F be non empty finite set ; ::_thesis: (card F) - 1 = (card F) -' 1 (card F) - 1 >= 0 by NAT_1:14, XREAL_1:48; hence (card F) - 1 = (card F) -' 1 by XREAL_0:def_2; ::_thesis: verum end; theorem :: PRE_CIRC:21 for f, g being Function holds ( dom f, dom g are_equipotent iff f,g are_equipotent ) proof let f, g be Function; ::_thesis: ( dom f, dom g are_equipotent iff f,g are_equipotent ) A1: ( card f = card (dom f) & card g = card (dom g) ) by CARD_1:62; hereby ::_thesis: ( f,g are_equipotent implies dom f, dom g are_equipotent ) assume dom f, dom g are_equipotent ; ::_thesis: f,g are_equipotent then card (dom f) = card (dom g) by CARD_1:5; hence f,g are_equipotent by A1, CARD_1:5; ::_thesis: verum end; assume f,g are_equipotent ; ::_thesis: dom f, dom g are_equipotent then card f = card g by CARD_1:5; hence dom f, dom g are_equipotent by A1, CARD_1:5; ::_thesis: verum end; theorem :: PRE_CIRC:22 for f, g being finite Function st dom f misses dom g holds card (f +* g) = (card f) + (card g) proof let f, g be finite Function; ::_thesis: ( dom f misses dom g implies card (f +* g) = (card f) + (card g) ) assume A1: dom f misses dom g ; ::_thesis: card (f +* g) = (card f) + (card g) thus card (f +* g) = card (dom (f +* g)) by CARD_1:62 .= card ((dom f) \/ (dom g)) by FUNCT_4:def_1 .= (card (dom f)) + (card (dom g)) by A1, CARD_2:40 .= (card (dom f)) + (card g) by CARD_1:62 .= (card f) + (card g) by CARD_1:62 ; ::_thesis: verum end; theorem :: PRE_CIRC:23 for n being Nat holds { k where k is Element of NAT : k > n } is infinite proof let n be Nat; ::_thesis: { k where k is Element of NAT : k > n } is infinite set X = { k where k is Element of NAT : k > n } ; A1: { k where k is Element of NAT : k > n } c= NAT proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { k where k is Element of NAT : k > n } or x in NAT ) assume x in { k where k is Element of NAT : k > n } ; ::_thesis: x in NAT then ex k being Element of NAT st ( x = k & k > n ) ; hence x in NAT ; ::_thesis: verum end; n + 1 > n + 0 by XREAL_1:8; then A2: n + 1 in { k where k is Element of NAT : k > n } ; assume { k where k is Element of NAT : k > n } is finite ; ::_thesis: contradiction then reconsider X = { k where k is Element of NAT : k > n } as non empty finite Subset of NAT by A1, A2; set m = max X; max X in X by XXREAL_2:def_8; then consider k being Element of NAT such that A3: max X = k and A4: k > n ; k + 1 > k + 0 by XREAL_1:8; then k + 1 > n by A4, XXREAL_0:2; then (max X) + 1 in X by A3; then (max X) + 1 <= (max X) + 0 by XXREAL_2:def_8; hence contradiction by XREAL_1:8; ::_thesis: verum end;