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