:: Preliminaries to Circuits, I
:: by Yatsuka Nakamura, Piotr Rudnicki, Andrzej Trybulec and Pauline N. Kawamoto
::
:: Received November 17, 1994
:: Copyright (c) 1994-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, FINSET_1, XBOOLE_0, SUBSET_1, TARSKI, FUNCT_1, RELAT_1,
FUNCOP_1, FUNCT_4, PBOOLE, FINSEQ_1, CARD_3, PARTFUN1, FUNCT_5, FUNCT_2,
ZFMISC_1, FUNCT_6, NAT_1, CARD_1, ARYTM_3, MCART_1, FINSEQ_2, TREES_1,
TREES_3, TREES_2, ORDINAL4, TREES_A, XXREAL_0, TREES_4, ARYTM_1, REAL_1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, XCMPLX_0, XREAL_0, XTUPLE_0,
MCART_1, CARD_1, RELAT_1, FUNCT_1, FINSET_1, PARTFUN1, FUNCT_2, ORDINAL1,
NUMBERS, XXREAL_0, XXREAL_2, BINOP_1, FUNCOP_1, FUNCT_4, FUNCT_7, CARD_3,
TREES_2, TREES_1, TREES_3, TREES_4, FUNCT_5, FUNCT_6, PBOOLE, FINSEQ_1,
FINSEQ_2, NAT_1, NAT_D;
constructors WELLORD2, BINOP_1, FUNCT_4, SETWISEO, XXREAL_0, NAT_1, FUNCT_5,
CARD_3, SEQ_4, PBOOLE, TREES_4, BINARITH, INT_1, XXREAL_2, PARTFUN1,
RELSET_1, FUNCT_7, XTUPLE_0, NAT_D;
registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, FUNCOP_1,
FINSET_1, XREAL_0, MEMBERED, FINSEQ_1, CARD_3, PBOOLE, TREES_2, TREES_3,
XXREAL_2, CARD_1, RELSET_1, TREES_1, XTUPLE_0, NAT_1;
requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
definitions TARSKI, FUNCOP_1, WELLORD2, FUNCT_1, RELAT_1, PBOOLE, XBOOLE_0;
equalities FINSEQ_2;
expansions TARSKI, XBOOLE_0, FINSET_1;
theorems TARSKI, ZFMISC_1, FINSEQ_1, FINSEQ_3, FUNCT_1, FUNCT_2, FUNCT_4,
FUNCT_5, TREES_1, TREES_2, TREES_3, TREES_4, NAT_1, RELAT_1, CARD_3,
FUNCOP_1, MCART_1, PBOOLE, CARD_2, CARD_1, FUNCT_6, FINSET_1, XBOOLE_0,
XBOOLE_1, XCMPLX_1, ORDERS_1, XREAL_1, XXREAL_0, XXREAL_2, XREAL_0,
PARTFUN1, FINSEQ_2, ORDINAL1;
schemes DOMAIN_1, PBOOLE, FUNCT_1, FRAENKEL, FINSEQ_1, NAT_1;
begin
scheme
FraenkelFinIm{ A() -> finite non empty set, F(set) -> set, P[set] }:
{ F(x) where x is Element of A() : P[x] } is finite
proof
set B = { F(x) where x is Element of A() : x in A() };
A1: { F(x) where x is Element of A() : P[x] } c= B
proof
let a be object;
assume a in { F(x) where x is Element of A() : P[x] };
then ex b being Element of A() st F(b) = a & P[b];
hence thesis;
end;
A2: A() is finite;
B is finite from FRAENKEL:sch 21(A2);
hence thesis by A1;
end;
begin
::---------------------------------------------------------------------------
:: Many Sorted Sets and Functions
::---------------------------------------------------------------------------
::$CT
theorem
for I being set, MSS being ManySortedSet of I holds MSS#.<*>I = {{}}
proof
let I be set, MSS be ManySortedSet of 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;
end;
reserve i,j,x,y for object,
f,g for Function;
scheme
MSSLambda2Part { I() -> set, P [object], F, G (object) -> object }:
ex f being ManySortedSet of I() st
for i being Element of I() st i in I() holds
(P[i] implies f.i = F(i)) & (not P[i] implies f.i = G(i))
proof
defpred Q[object,object] means
(P[$1] implies $2 = F($1)) & (not P[$1] implies $2 = G($1));
A1: now
let i be object such that
i in I();
thus ex j being object st Q[i,j]
proof
per cases;
suppose
A2: P[i];
take F(i);
thus thesis by A2;
end;
suppose
A3: not P[i];
take G(i);
thus thesis by A3;
end;
end;
end;
consider f being ManySortedSet of I() such that
A4: for i being object st i in I() holds Q[i,f.i] from PBOOLE:sch 3(A1);
take f;
thus thesis by A4;
end;
registration
let I be set;
cluster non-empty finite-yielding for ManySortedSet of I;
existence
proof
reconsider f = I --> {{}} as Function;
reconsider f as ManySortedSet of I;
take f;
thus f is non-empty;
thus f is finite-yielding by FUNCOP_1:7;
end;
end;
registration
let I be set, M be ManySortedSet of I, A be Subset of I;
cluster M | A -> total for A-defined Function;
coherence
proof
set B = M | A;
dom B = dom M /\ A & dom M = I by PARTFUN1:def 2,RELAT_1:61;
then dom B = A by XBOOLE_1:28;
hence thesis by PARTFUN1:def 2;
end;
end;
registration
let I be set, M be ManySortedSet of I, A be Subset of I;
cluster M | A -> total;
coherence;
end;
theorem Th2:
for I being non empty set, B being non-empty ManySortedSet of I
holds union rng B is non empty
proof
let I be non empty set, B be non-empty ManySortedSet of I;
set i = the Element of I;
i in I;
then i in dom B by PARTFUN1:def 2;
then B.i in rng B by FUNCT_1:def 3;
hence thesis by ORDERS_1:6;
end;
theorem Th3:
for I being set holds uncurry (I --> {}) = {}
proof
let I be set;
per cases;
suppose
I = {};
hence thesis by FUNCT_5:43;
end;
suppose
I <> {};
then rng (I --> {}) = {{}} by FUNCOP_1:8
.= Funcs({} qua set, {} qua set) by FUNCT_5:57;
then dom uncurry (I --> {}) = [:dom (I --> {}), {}:] by FUNCT_5:26
.= {} by ZFMISC_1:90;
hence thesis;
end;
end;
theorem
for I being non empty set, A being set,
B being non-empty ManySortedSet of I,
F being ManySortedFunction of (I --> A qua total I-defined
Function), B holds dom commute F = A
proof
let I be non empty set, A be set, B be non-empty ManySortedSet of I,
F be ManySortedFunction of (I --> A), B;
A1: dom B = I by PARTFUN1:def 2;
A2: dom F = I by PARTFUN1:def 2;
per cases;
suppose
A3: A is empty;
rng F c= {{}}
proof
let x be object;
assume x in rng F;
then consider i being object 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 thesis by TARSKI:def 1;
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,Th3,FUNCT_5:42;
hence thesis by A3;
end;
suppose
A6: A is non empty;
rng F c= Funcs(A, union rng B)
proof
let x be object;
assume x in rng F;
then consider i being object 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;
dom x9 = A by A2,A7,FUNCT_2:def 1;
hence thesis by A9,FUNCT_2:def 2;
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;
union rng B is non empty by Th2;
then Funcs (I, union rng B) is non empty by FUNCT_2:8;
hence thesis by A10,FUNCT_2:def 1;
end;
end;
scheme
LambdaRecCorrD {D() -> non empty set, A() -> Element of D(),
F(Nat, Element of D()) -> Element of D() } :
(ex f being sequence of D() st f.0 = A() &
for i being Nat holds f.(i+1) = F(i, f.i)) &
for f1, f2 being sequence of D() st
(f1.0 = A() & for i being Nat holds f1.(i+1) = F(i, f1.i)) &
(f2.0 = A() & for i being Nat holds f2.(i+1) = F(i,f2.i)) holds f1 = f2
proof
thus ex f being sequence of D() st f.0 = A() &
for i being Nat holds f.(i+1) = F(i,f.i) from NAT_1:sch 12;
let f1, f2 be sequence of D() such that
A1: f1.0 = A() and
A2: for i being Nat holds f1.(i+1) = F(i,f1.i) and
A3: f2.0 = A() and
A4: for i being Nat holds f2.(i+1) = F(i,f2.i);
thus f1 = f2 from NAT_1:sch 16(A1,A2,A3,A4);
end;
scheme
LambdaMSFD{J() -> non empty set, I() -> Subset of J(),
A, B() -> ManySortedSet of I(), F(object) -> set } :
ex f being ManySortedFunction of A(), B() st
for i being Element of J() st i in I() holds f.i = F(i)
provided
A1: for i being Element of J() st i in I() holds
F(i) is Function of A().i, B().i
proof
consider f being ManySortedSet of I() such that
A2: for i being object st i in I() holds f.i = F(i) from PBOOLE:sch 4;
f is Function-yielding
proof
let i be object;
assume i in dom f;
then
A3: i in I() by PARTFUN1:def 2;
then F(i) is Function by A1;
hence thesis by A2,A3;
end;
then reconsider f as ManySortedFunction of I();
f is ManySortedFunction of A(), B()
proof
let i;
assume
A4: i in I();
then F(i) is Function of A().i, B().i by A1;
hence thesis by A2,A4;
end;
then reconsider f as ManySortedFunction of A(), B();
take f;
thus thesis by A2;
end;
theorem
for I being set, f being non-empty ManySortedSet of I,
g being Function, 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, f be non-empty ManySortedSet of I, g be Function, s be 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;
A3: now
let x be object;
assume
A4: x in dom f;
per cases;
suppose
A5: x in dom g;
then (s+*g).x = g.x by FUNCT_4:13;
hence (s+*g).x in f.x by A2,A5;
end;
suppose
A6: not x in dom g;
A7: ex g9 being Function st s = g9 & dom g9 = dom f & for x being object
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;
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 thesis by A3,CARD_3:9;
end;
theorem
for A, B being non empty set, C being non-empty ManySortedSet of A,
InpFs being ManySortedFunction of A --> B, C, 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, C be non-empty ManySortedSet of A, InpFs be
ManySortedFunction of A --> B, C, b be Element of B;
A1: dom InpFs = A by PARTFUN1:def 2;
dom uncurry InpFs = [:A,B:]
proof
thus dom uncurry InpFs c= [:A,B:]
proof
let i be object;
assume i in dom(uncurry InpFs);
then consider x,g,y 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 thesis by A1,A2,A3,A5,ZFMISC_1:87;
end;
let i1,i2 be object;
reconsider g = InpFs.[i1,i2]`1 as Function;
assume
A6: [i1,i2] in [:A,B:];
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 thesis by A7,A8,FUNCT_5:38;
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 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;
thus c = (commute InpFs).b;
let i be object;
reconsider h = InpFs.i as Function;
assume
A10: i in A;
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 thesis by A10,A11,FUNCT_2:5;
end;
theorem
for n being Nat, a being set holds
product ( n |-> {a} ) = { n |-> a }
proof
let n be Nat, a be set;
now
let i be object;
hereby
assume i in product ( n |-> {a} );
then consider g being Function such that
A1: i = g and
A2: dom g = dom( n |-> {a} ) and
A3: for x being object 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;
now
let x be object;
assume
A5: x in dom g;
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;
end;
hence i = n |-> a by A1,A4,FUNCOP_1:11;
end;
assume
A6: i = n |-> a;
then reconsider g = i as Function;
A7: now
let x be object;
assume x in dom( n |-> {a} );
then x in Seg n;
then g.x = a & ( n |-> {a} ).x = {a} by A6,FUNCOP_1:7;
hence g.x in ( n |-> {a} ).x by TARSKI:def 1;
end;
dom g = Seg n by A6
.= dom( n |-> {a} );
hence i in product ( n |-> {a} ) by A7,CARD_3:9;
end;
hence thesis by TARSKI:def 1;
end;
begin
::---------------------------------------------------------------------------
:: Trees
::---------------------------------------------------------------------------
reserve T,T1 for finite Tree,
t,p for Element of T,
t1 for Element of T1;
registration
let D be non empty set;
cluster -> finite for Element of FinTrees D;
coherence
proof
let t be Element of FinTrees D;
dom t is finite;
hence thesis by FINSET_1:10;
end;
end;
registration
let T be finite DecoratedTree;
let t be Element of dom T;
cluster T|t -> finite;
coherence
proof
dom(T|t) = (dom T)|t by TREES_2:def 10;
hence thesis by FINSET_1:10;
end;
end;
theorem Th8:
T|p,{ t : p is_a_prefix_of t } are_equipotent
proof
set X = { t : p is_a_prefix_of t };
deffunc F(Element of T|p) = 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 = F(n) from FUNCT_1:sch 4;
take f;
thus f is one-to-one
proof
let x,y be object such that
A3: x in dom f & y in dom f and
A4: f.x = f.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 thesis by FINSEQ_1:33;
end;
thus dom f = T|p by A1;
thus rng f c= X
proof
let i be object;
assume i in rng f;
then consider n being object such that
A5: n in dom f and
A6: i = f.n by FUNCT_1:def 3;
reconsider 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 thesis by A6;
end;
let i be object;
assume i in X;
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 as Element of T|p by A7,A8,TREES_1:def 6;
i = f.n by A2,A8;
hence thesis by A1,FUNCT_1:def 3;
end;
registration
let T be finite DecoratedTree-like Function;
let t be Element of dom T;
let T1 be finite DecoratedTree;
cluster T with-replacement (t,T1) -> finite;
coherence
proof
dom (T with-replacement (t,T1)) = dom T with-replacement (t,dom T1)
by TREES_2:def 11;
hence thesis by FINSET_1:10;
end;
end;
theorem Th9:
T with-replacement (p,T1) =
{ t : not p is_a_prefix_of t } \/ the set of all p^t1
proof
defpred P2[set] means not contradiction;
defpred P1[set] means $1=$1;
deffunc F(FinSequence) = p^$1;
set A = { t : not p is_a_proper_prefix_of t }, B = { F(t1) : P1[t1] }, C = {
t: not p is_a_prefix_of t }, D = { F(t1) : P2[t1] };
now
let x be object;
hereby
assume x in A;
then consider 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;
hence x in C or x in {p} by A1,TARSKI:def 1;
end;
assume x in C or x in {p};
then x = p or ex t st t = x & not p is_a_prefix_of t by TARSKI:def 1;
then consider 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;
hence x in A by A3;
end;
then
A5: A = C \/ {p} by XBOOLE_0:def 3;
{} is Element of T1 & p^{} = p by FINSEQ_1:34,TREES_1:22;
then
A6: p in D;
thus T with-replacement (p,T1) = C \/ {p} \/ D by A5,TREES_1:32
.= C \/ ({p} \/ D) by XBOOLE_1:4
.= C \/ D by A6,ZFMISC_1:40;
end;
theorem Th10:
for f being FinSequence of NAT st f in T with-replacement (p,T1)
& p is_a_prefix_of f ex t1 st f = p^t1
proof
let f be FinSequence of NAT such that
A1: f in T with-replacement (p,T1) and
A2: p is_a_prefix_of f;
A3: not f in { t : not p is_a_prefix_of t }
proof
assume f in { t : not p is_a_prefix_of t };
then ex t st f = t & not p is_a_prefix_of t;
hence contradiction by A2;
end;
T with-replacement (p,T1) = { t : not p is_a_prefix_of t } \/ the set of all
p^t1 by Th9;
then f in the set of all p^t1 by A1,A3,XBOOLE_0:def 3;
hence thesis;
end;
theorem Th11:
for p being Tree-yielding FinSequence, 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, k be Element of NAT;
assume k+1 in dom p;
then k+1 <= len p by FINSEQ_3:25;
then k < len p by NAT_1:13;
hence thesis by TREES_3:49;
end;
theorem
for q being DTree-yielding FinSequence, k being Nat st
k+1 in dom q holds <*k*> in tree doms q
proof
let q be DTree-yielding FinSequence, k be Nat;
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;
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 thesis by A5,A4,TREES_3:def 15;
end;
theorem Th13:
for p,q being Tree-yielding FinSequence, k being Element of NAT st
len p = len q & k+1 in dom p & for i being Nat st i in dom p &
i <> k+1 holds p.i = q.i
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, k be Element of NAT such that
A1: len p = len q and
A2: k+1 in dom p and
A3: for i being Nat st i in dom p & i <> k+1 holds p.i = q.i;
let t be Tree;
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;
A6: now
let s be FinSequence of NAT;
hereby
assume
A7: s in tree(q);
per cases by A7,TREES_3:def 15;
suppose
s = {};
hence s in tree(p) & not o is_a_proper_prefix_of s or ex r being
FinSequence of NAT st r in t & s = o^r by TREES_1:22;
end;
suppose
ex n being Nat, r being FinSequence st n < len q &
r in q.(n+1) & s = <*n*>^r;
then consider n being Nat, r being FinSequence such that
A8: n < len q and
A9: r in q.(n+1) and
A10: s = <*n*>^r;
now
per cases;
case
A11: n = k;
reconsider r as FinSequence of NAT by A10,FINSEQ_1:36;
take r;
thus r in t & s = o^r by A5,A9,A10,A11;
end;
case
A12: n <> k;
1 <= n+1 & n+1 <= len p by A1,A8,NAT_1:11,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;
assume o is_a_proper_prefix_of s;
then o is_a_prefix_of s;
then ex s1 being FinSequence st s = o^s1 by TREES_1:1;
then k = s.1 by FINSEQ_1:41
.= n by A10,FINSEQ_1:41;
hence contradiction by A12;
end;
end;
hence s in tree(p) & not o is_a_proper_prefix_of s or ex r being
FinSequence of NAT st r in t & s = o^r;
end;
end;
assume
A13: s in tree(p) & not o is_a_proper_prefix_of s or ex r being
FinSequence of NAT st r in t & s = o^r;
per cases by A13;
suppose that
A14: s in tree(p) and
A15: not o is_a_proper_prefix_of s;
now
per cases by A14,TREES_3:def 15;
suppose
s = {};
hence s in tree(q) by TREES_1:22;
end;
suppose
ex n being Nat, r being FinSequence st n < len p
& r in p.(n+1) & s = <*n*>^r;
then consider n being Nat, r being FinSequence such that
A16: n < len p and
A17: r in p.(n+1) and
A18: s = <*n*>^r;
now
per cases;
suppose
A19: r = {};
1 <= n+1 & n+1 <= len q by A1,A16,NAT_1:11,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;
end;
suppose r <> {};
then
A20: n <> k by A15,A18,FINSEQ_1:87,TREES_1:1;
1 <= n+1 & n+1 <= len p by A16,NAT_1:11,13;
then n+1 in dom p by FINSEQ_3:25;
then q.(n+1) = p.(n+1) by A3,A20,XCMPLX_1:2;
hence s in tree(q) by A1,A16,A17,A18,TREES_3:def 15;
end;
end;
hence s in tree(q);
end;
end;
hence s in tree(q);
end;
suppose
ex r being FinSequence of NAT st r in t & s = o^r;
hence s in tree(q) by A1,A4,A5,TREES_3:def 15;
end;
end;
p.(k+1) is Tree by A2,TREES_3:22;
then
A21: {} in p.(k+1) by TREES_1:22;
o = o^{} by FINSEQ_1:34;
then o in tree(p) by A4,A21,TREES_3:def 15;
hence thesis by A6,TREES_1:def 9;
end;
theorem
for e1,e2 being finite DecoratedTree, x being set,
k being Element of NAT, p being DTree-yielding FinSequence st
<*k*> in dom e1 & e1 = x-tree p
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 Nat st i in dom p & i <> k+1 holds q.i = p.i
proof
let e1,e2 be finite DecoratedTree, x be set, k be Element of NAT,
p be DTree-yielding FinSequence such that
A1: <*k*> in dom e1 and
A2: e1 = x-tree p;
consider j being 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 F(Nat) = 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 = F(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
let x;
assume
A12: x in dom q;
then reconsider i = x as 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;
end;
then reconsider 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
let i be Nat;
assume that
A19: i in dom doms pp and
A20: i <> k+1;
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;
end;
reconsider dqq = doms qq as Tree-yielding FinSequence;
take q;
<*j*> = <*k*> by A4,FINSEQ_1:88;
then
A22: j = <*k*>.1
.= k;
then 1 <= k+1 & k+1 <= len p by A3,NAT_1:11,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 (o, dom e2) by A2,A23,A15,A6,A16
,A7,A18,Th13;
for f being FinSequence of NAT st f in dom e1 with-replacement (o, dom
e2) holds not o is_a_prefix_of f & (x-tree q).f = e1.f or ex r being
FinSequence of NAT st r in dom e2 & f = o^ r & (x-tree q).f = e2.r
proof
reconsider o9 = o as Element of dom e1 by A1;
let f be FinSequence of NAT;
assume
A26: f in dom e1 with-replacement (o, dom e2);
per cases by A26,Th10;
suppose
A27: not o9 is_a_prefix_of f;
A28: (x-tree q).f = e1.f
proof
per cases by A15,A25,A26,TREES_3:def 15;
suppose
A29: f = {};
hence (x-tree q).f = x by TREES_4:def 4
.= e1.f by A2,A29,TREES_4:def 4;
end;
suppose
ex w being Nat, u being FinSequence st w < len(
dqq) & u in (dqq).(w+1) & f = <*w*>^u;
then consider w be 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 as FinSequence of NAT by A32,FINSEQ_1:36;
reconsider w as Element of NAT by ORDINAL1:def 12;
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,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,Th11
.= 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,Th11;
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;
end;
end;
assume o is_a_prefix_of f or (x-tree q).f <> e1.f;
hence thesis by A27,A28;
end;
suppose
ex t1 being Element of dom e2 st f=o9^t1;
then consider r being Element of dom e2 such that
A40: f = o^r;
assume o is_a_prefix_of f or (x-tree q).f <> e1.f;
A41: (x-tree q)|o = q.(k+1) by A8,A3,A22,TREES_4:def 4;
reconsider r as FinSequence of NAT;
take r;
thus
A42: r in dom e2;
thus f = o^r by A40;
r in (dom(x-tree q))|o by A1,A25,A42,TREES_1:33;
hence thesis by A24,A40,A41,TREES_2:def 10;
end;
end;
hence e1 with-replacement (o,e2) = x-tree q by A1,A25,TREES_2:def 11;
thus len q = len p by A8;
thus q.(k+1) = e2 by A24;
let i be Nat;
assume i in dom p;
then q.i = IFEQ(i,k+1,e2,p.i) by A9,A10,A17;
hence thesis by FUNCOP_1:def 8;
end;
theorem
for T being finite Tree, p being Element of T st p <> {} holds
card (T | p) < card T
proof
let T be finite Tree, p be Element of 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,X are_equipotent
proof
deffunc F(Element of T|p) = 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 = F(n) from FUNCT_1:sch 4;
take f;
thus f is one-to-one
proof
let x,y be object such that
A4: x in dom f & y in dom f and
A5: f.x = f.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 thesis by FINSEQ_1:33;
end;
thus dom f = T|p by A2;
thus rng f c= X
proof
let i be object;
assume i in rng f;
then consider n being object 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 as Element of NAT* by A2,A6;
f.n = p9^n by A2,A3,A6;
hence thesis by A2,A6,A7;
end;
let i be object;
assume i in X;
then consider n being Element of NAT* such that
A8: i = p9^n and
A9: n in T|p;
reconsider n as Element of T|p by A9;
i = f.n by A3,A8;
hence thesis by A2,FUNCT_1:def 3;
end;
then reconsider X as finite set by CARD_1:38;
A10: card X = card(T|p) by A1,CARD_1:5;
assume
A11: p <> {};
A12: X <> T
proof
assume X = T;
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;
end;
X c= T
proof
let i be object;
assume i in X;
then ex n being Element of NAT* st i = p9^n & n in T|p;
hence thesis by TREES_1:def 6;
end;
then X c< T by A12;
hence thesis by A10,CARD_2:48;
end;
theorem Th16:
for T, T1 being finite Tree, p being Element of T holds
card(T with-replacement (p,T1)) + card (T|p) = card T + card T1
proof
let T, T1, p;
defpred P1[Element of T] means not p is_a_prefix_of $1;
defpred P2[Element of T] means p is_a_prefix_of $1;
set A = { t : P1[t] };
set B = { t : P2[t] };
set C = the set of all p^t1 ;
A1: A is Subset of T from DOMAIN_1:sch 7;
A2: B is Subset of T from DOMAIN_1:sch 7;
A3: T1,C are_equipotent
proof
deffunc F(Element of T1) = p^$1;
consider f being Function such that
A4: dom f = T1 and
A5: for n being Element of T1 holds f.n = F(n) from FUNCT_1:sch 4;
take f;
thus f is one-to-one
proof
let x,y be object such that
A6: x in dom f & y in dom f and
A7: f.x = f.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 thesis by FINSEQ_1:33;
end;
thus dom f = T1 by A4;
thus rng f c= C
proof
let i be object;
assume i in rng f;
then consider n being object 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 as Element of NAT* by A4,A8;
f.n = p^n by A4,A5,A8;
hence thesis by A4,A8,A9;
end;
let i be object;
assume i in C;
then consider n being Element of T1 such that
A10: i = p^n;
i = f.n by A5,A10;
hence thesis by A4,FUNCT_1:def 3;
end;
reconsider A,B as finite set by A1,A2;
now
let x be object;
hereby
assume x in T;
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;
end;
assume x in A or x in B;
hence x in T by A1,A2;
end;
then
A11: T = A \/ B by XBOOLE_0:def 3;
A12: A misses C
proof
assume not thesis;
then consider x being object such that
A13: x in A /\ C by XBOOLE_0:4;
x in C by A13,XBOOLE_0:def 4;
then
A14: ex t1 st x = p^t1;
x in A by A13,XBOOLE_0:def 4;
then ex t st x = t & not p is_a_prefix_of t;
hence contradiction by A14,TREES_1:1;
end;
A15: A misses B
proof
assume not thesis;
then consider x being object such that
A16: x in A /\ B by XBOOLE_0:4;
x in B by A16,XBOOLE_0:def 4;
then
A17: ex t st x = t & p is_a_prefix_of t;
x in A by A16,XBOOLE_0:def 4;
then ex t st x = t & not p is_a_prefix_of t;
hence contradiction by A17;
end;
A18: T with-replacement (p,T1) = A \/ C by Th9;
reconsider C as finite set by A3,CARD_1:38;
A19: card T1 = card C by A3,CARD_1:5;
T|p,B are_equipotent by Th8;
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;
end;
theorem
for T, T1 being finite DecoratedTree, 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, p be Element of dom T;
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,def 11;
hence thesis by A1,A2,Th16;
end;
registration
let x be object;
cluster root-tree x -> finite;
coherence
proof
root-tree x = {[{},x]} by TREES_4:6;
hence thesis;
end;
end;
theorem
for x being set holds card root-tree x = 1
proof
let x be set;
root-tree x = {[{},x]} by TREES_4:6;
hence thesis by CARD_1:30;
end;
begin :: Addenda
:: from AMISTD_2
theorem Th19:
for F being non empty finite set holds card F - 1 = card F -' 1
proof
let F be non empty finite set;
card F - 1 >= 0 by NAT_1:14,XREAL_1:48;
hence thesis by XREAL_0:def 2;
end;
:: from AMISTD_2, 2006.03.26, A.T.
theorem
for f, g being Function holds
dom f,dom g are_equipotent iff f,g are_equipotent
proof
let f, g be Function;
A1: card f = card dom f & card g = card dom g by CARD_1:62;
hereby
assume dom f,dom g are_equipotent;
then card dom f = card dom g by CARD_1:5;
hence f,g are_equipotent by A1,CARD_1:5;
end;
assume f,g are_equipotent;
then card f = card g by CARD_1:5;
hence thesis by A1,CARD_1:5;
end;
theorem
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 such that
A1: dom f misses dom 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;
end;
:: from SCMPDS_9. 2008.05.06, A.T.
theorem
for n being Nat holds
{k where k is Nat: k > n} is infinite
proof
let n be Nat;
set X = {k where k is Nat: k > n};
A1: X c= NAT
proof
let x be object;
assume x in X;
then ex k being Nat st x = k & k > n;
hence thesis by ORDINAL1:def 12;
end;
n+1 > n+0 by XREAL_1:8; then
A2: n+1 in X;
assume X is finite;
then reconsider X as non empty finite Subset of NAT by A1,A2;
set m = max X;
m in X by XXREAL_2:def 8;
then consider k being Nat such that
A3: m = k and
A4: k > n;
k+1 > k+0 by XREAL_1:8;
then k+1 > n by A4,XXREAL_0:2;
then m+1 in X by A3;
then m+1 <= m+0 by XXREAL_2:def 8;
hence contradiction by XREAL_1:8;
end;
theorem Th23:
for D being finite set, k being Nat st card D = k+1
ex x being Element of D,C being Subset of D st D = C \/ { x } & card C = k
proof
let D be finite set,k be Nat;
assume
A1: card D = k+1;
then D <> {};
then consider x being object such that
A2: x in D by XBOOLE_0:def 1;
reconsider C=D \ { x } as Subset of D;
reconsider x as Element of D by A2;
take x,C;
x in {x} by TARSKI:def 1;
then
A3: not x in C by XBOOLE_0:def 5;
{x} c= D by A2,ZFMISC_1:31;
hence D=C \/ {x} by XBOOLE_1:45;
then card D = card C + 1 by A3,CARD_2:41;
hence thesis by A1;
end;
theorem Th24:
for D being finite set st card D = 1 holds ex x being Element of D st D={x}
proof
let D be finite set;
assume card D = 1;
then card D = 0+1;
then consider x being Element of D,C being Subset of D such that
A1: D = C \/ { x } and
A2: card C = 0 by Th23;
take x;
C = {} by A2;
hence thesis by A1;
end;
reserve k for Nat;
scheme
MinValue { D() -> non empty finite set, F(Element of D())-> Real}:
ex x being Element of D() st for y being Element of D() holds F(x) <= F(y)
proof
defpred P[Nat] means
for A being Subset of D() st $1+1 = card A
ex x being Element of D() st x in A &
for y being Element of D() st y in A holds F(x) <= F(y);
A1: card D() -' 1 + 1= card D() -1 +1 by Th19
.=card D();
A2: D() c= D();
A3: for k st P[k] holds P[k+1]
proof
let k;
assume
A4: P[k];
now
let A be Subset of D();
assume
A5: k+1+1 = card A;
then
A6: A <> {};
consider x being Element of A,C being Subset of A such that
A7: A = C \/ { x } and
A8: card C = k+1 by A5,Th23;
x in A by A6;
then reconsider x as Element of D();
reconsider C as Subset of D() by XBOOLE_1:1;
consider z being Element of D() such that
A9: z in C and
A10: for y being Element of D() st y in C holds F(z) <= F(y) by A4,A8;
per cases;
suppose
A11: F(x) <= F(z);
take x;
thus x in A by A6;
hereby
let y be Element of D();
assume
A12: y in A;
per cases by A7,A12,XBOOLE_0:def 3;
suppose
y in C;
then F(z) <= F(y) by A10;
hence F(x) <= F(y) by A11,XXREAL_0:2;
end;
suppose
y in {x};
hence F(x) <= F(y) by TARSKI:def 1;
end;
end;
end;
suppose
A13: F(x) > F(z);
take z;
thus z in A by A9;
hereby
let y be Element of D();
assume
A14: y in A;
per cases by A7,A14,XBOOLE_0:def 3;
suppose
y in C;
hence F(z) <= F(y) by A10;
end;
suppose
y in {x};
hence F(z) <= F(y) by A13,TARSKI:def 1;
end;
end;
end;
end;
hence thesis;
end;
A15: P[0]
proof
let A be Subset of D();
assume 0+1 = card A;
then consider x being Element of A such that
A16: A = {x} by Th24;
reconsider x as Element of D() by A16,ZFMISC_1:31;
take x;
thus x in A by A16;
thus thesis by A16,TARSKI:def 1;
end;
for k holds P[k] from NAT_1:sch 2(A15,A3);
then card D() -' 1+1 = card D() implies
ex x being Element of D() st x in D() &
for y being Element of D() st y in D() holds F(x) <= F(y) by A2;
then consider x being Element of D() such that
x in D() and
A17: for y being Element of D() st y in D() holds F(x) <= F(y) by A1;
take x;
let y be Element of D();
thus thesis by A17;
end;