--BEGIN HERE -- -- -- This scenario introduces various notions regarding finite graphs, in particular -- connectivity and its equivalent notion 'HasSpanningTree', -- and regarding finite digraphs, in particular -- extensionality, weak extensionality, and acyclicity. -- Moreover it relates graphs to digraphs via the 'Orientates' predicate. -- -- We will prove that every weakly extensional, acyclic digraph can be decorated -- a` la Mostowski by finite sets so that: -- on the one hand, its arcs mimic membership; -- on the other hand, no collisions arise between its vertices -- (otherwise stated, no two vertices are sent to the same set by the decoration). -- This applies, of course, also to the special case of an extensional digraph. -- We will manage to have one node sent to $0$ in the decoration. -- -- We will also see that a graph whatsoever admits an orientation which is weakly -- extensional and acyclic; consequently, and in view of what precedes, one can regard its -- edges as membership arcs deprived of their natural orientation. -- -- To end, we will endow each connected claw-free graph $G$ -- with an extensional acyclic orientation so that, through such an orientation, -- $G$ will be represented as a transitive set $T$ and -- the membership arcs between elements of $T$ will correspond to the edges of $G$. -- -- -- \section{Preparatory notions} -- -- -- -- \subsection{From pairs to single-valued and singleton maps} -- -- -- Formal definition of the ordered pair and of both of its -- ordered-pair component extractor functions. -- Def pair_1: [Ordered pair] Def([X,Y]) := {{X},{{X},{{Y},Y}}} -- Def pair_2: [First component of ordered pair] car(P) := arb(arb(P)) Def pair_3: [Second component of ordered pair] cdr(P) := arb(arb(arb(P - {arb(P)}) - {arb(P)})) -- -- The formal definitions, just seen, of the pairing function -- and of its projections enforce that $(car(0)=0) & (cdr(0)=0)$. -- We will exploit this fact later, to treat $0$ as the result of -- applying a single-valued map $f$ to an operand which lies outside -- the domain of $f$. -- Theorem pair_1: [Both projections extract $0$ from $0$] (car(0) = 0) & (cdr(0) = 0). Proof: Suppose_not() ==> AUTO TELEM ==> arb(0) = 0 TELEM ==> arb(0 - {arb(0)}) - {0} = 0 Use_def(car(0)) ==> AUTO Use_def(cdr(0)) ==> AUTO EQUAL ==> false Discharge ==> QED -- -- -- The following operations are usually applied to sets of ordered pairs, here called \emph{maps}: -- Def maps_1: [Map domain, i.e. set of first components of pairs in map] domain(F) := {car(x): x in F} Def maps_2: [Map restriction] Def(F ¥ON A) := {p in F | car(p) in A} Def maps_3: [Image, i.e. value, of single-valued function] Def(F~[X]) := cdr(arb(F ¥ON {X})) -- Def maps_4: [Map range, i.e. set of second components of pairs in map] range(F) := {cdr(p): p in F} Def maps_5: [Map predicate] Is_map(F) := (FORALL p in F | p = [car(p),cdr(p)]) Def maps_6: [Single-valued map predicate] Svm(F) := Is_map(F) & (FORALL p in F, q in F | (car(p) = car(q)) ¥imp (p = q)) -- -- The following THEORY indicates a convenient rewriting of the domain of a map: -- it will not be called explicitly, but is involved in some uses of the TELEM -- inference mechanism. -- --PAUSE HERE -- THEORY isSvm(s0,f(X),P(X)) END isSvm -- -- ENTER_THEORY isSvm -- Theorem isSvm_0: Svm({[x,f(x)]: x in s0 | P(x)}). Proof: Suppose_not() ==> AUTO Suppose ==> Stat1: not (FORALL q in {[x,f(x)]: x in s0 | P(x)} | q = [car(q),cdr(q)]) p0-->Stat1(Stat1*) ==> Stat2: (p0 in {[x,f(x)]: x in s0 | P(x)}) & (p0 /= [car(p0),cdr(p0)]) x0-->Stat2(Stat2) ==> false Discharge ==> AUTO Use_def(Is_map) ==> Is_map({[x,f(x)]: x in s0}) Use_def(Svm) ==> Stat3: not (FORALL r in {[x,f(x)]: x in s0 | P(x)}, q in {[x,f(x)]: x in s0 | P(x)} | (car(r) = car(q)) ¥imp (r = q)) (p1,q1)-->Stat3(Stat3*) ==> Stat4: (p1 in {[x,f(x)]: x in s0 | P(x)}) & (q1 in {[x,f(x)]: x in s0 | P(x)}) & (car(p1) = car(q1)) & (p1 /= q1) (x1,x2)-->Stat4(Stat4*) ==> (p1 = [x1,f(x1)]) & (q1 = [x2,f(x2)]) TELEM ==> (car([x1,f(x1)]) = x1) & (car([x2,f(x2)]) = x2) EQUAL(Stat4) ==> false Discharge ==> QED -- Theorem isSvm_1: (domain({[x,f(x)]: x in s0 | P(x)}) = {x in s0 | P(x)}) & ({x in s0 | true} = s0). Proof: Suppose_not() ==> AUTO SIMPLF ==> {x in s0 | true} = s0 Use_def(domain) ==> {car(p): p in {[x,f(x)]: x in s0 | P(x)}} /= {x in s0 | P(x)} SIMPLF ==> Stat1: {car([x,f(x)]): x in s0 | P(x)} /= {x in s0 | P(x)} x0-->Stat1(Stat1*) ==> false Discharge ==> QED -- Theorem isSvm_2: range({[x,f(x)]: x in s0 | P(x)}) = {f(x): x in s0 | P(x)}. Proof: Suppose_not() ==> AUTO Use_def(range) ==> {cdr(p): p in {[x,f(x)]: x in s0 | P(x)}} /= {f(x): x in s0 | P(x)} SIMPLF ==> Stat1: {cdr([x,f(x)]): x in s0 | P(x)} /= {f(x): x in s0 | P(x)} x0-->Stat1(Stat1*) ==> false Discharge ==> QED -- ENTER_THEORY Set_theory -- --BEGIN HERE -- -- Our next THEORY captures certain properties such as additivity -- (and, a fortiori, monotonicity) enjoyed by any global function which, -- much like $domain$ and $range$, is characterized by a pointwise definition. -- THEORY pointwise(g(Y),f(X)) (FORALL x | f(x) = {g(y): y in x}) END pointwise -- ENTER_THEORY pointwise -- Theorem pointwise0: [Pointwise defined functions are monotonic] (S ¥incin T) ¥imp (f(S) ¥incin f(T)). Proof: Suppose_not(s0,t0) ==> AUTO Assump ==> Stat0: (FORALL x | f(x) = {g(y): y in x}) & (FORALL x | f(x) = {g(y): y in x}) (s0,t0)-->Stat0(*) ==> Stat1: {g(x): x in s0} ¥nincin {g(x): x in t0} c0-->Stat1(*) ==> Stat2: (c0 in {g(x): x in s0}) & (c0 notin {g(x): x in t0}) & (s0 ¥incin t0) (x0,x0)-->Stat2(Stat2*) ==> false Discharge ==> QED -- Theorem pointwise1: [Pointwise defined functions are additive] (X = Y+Z) ¥imp (f(X) = f(Y) + f(Z)). Proof: Suppose_not(x0,y0,z0) ==> AUTO (y0,x0)-->Tpointwise0 ==> AUTO (z0,x0)-->Tpointwise0 ==> Stat1: f(x0) ¥nincin (f(y0) + f(z0)) u0-->Stat1(Stat1*) ==> Stat2: (u0 in f(x0)) & (u0 notin (f(y0) + f(z0))) Assump ==> Stat3: (FORALL x | f(x) = {g(y): y in x}) & (FORALL x | f(x) = {g(y): y in x}) & (FORALL x | f(x) = {g(y): y in x}) (x0,y0,z0)-->Stat3(Stat2*) ==> Stat4: (u0 in {g(x): x in x0}) & (u0 notin {g(y): y in y0}) & (u0 notin {g(z): z in z0}) (x1,x1,x1)-->Stat4(*) ==> false Discharge ==> QED -- Theorem pointwise2: [Pointwise defined functions send $0$ to $0$] (X = 0) ¥eq (f(X) = 0). Proof: Suppose_not(x0) ==> AUTO Suppose ==> Stat1: ({g(p): p in x0} /= 0) & (x0 = 0) p0-->Stat1(Stat1*) ==> false; Discharge ==> AUTO Assump ==> Stat2: (FORALL x | f(x) = {g(y): y in x}) x0-->Stat2(*) ==> Stat3: (x0 /= 0) & ({g(p): p in x0} = 0) (p1,p1)-->Stat3(Stat3*) ==> false Discharge ==> QED -- ENTER_THEORY Set_theory -- -- -- DISPLAY pointwise -- -- THEORY pointwise(g(Y),f(X)) -- (FORALL x | f(x) = {g(y): y in x}) -- ==> -- (FORALL s, t | (S ¥incin T) ¥imp (f(S) ¥incin f(T))) -- (FORALL x, y, z | (X = Y+Z) ¥imp (f(X) = f(Y) + f(Z))) -- (FORALL x | (X = 0) ¥eq (f(X) = 0)) -- END pointwise -- -- Having now developed a THEORY referring to any global function -- which has a pointwise definition, we readily -- apply it to the range and domain functions. -- Theorem range_1: [Additivity of range] ((X = Y+Z) ¥imp (range(X) = range(Y) + range(Z))) & ((range(X) = 0) ¥eq (X = 0)). Proof: Suppose_not(x0,y0,z0) ==> AUTO Suppose ==> Stat0: not (FORALL x | range(x) = {cdr(y): y in x}) f0-->Stat0(Stat0*) ==> Stat1: range(f0) /= {cdr(y): y in f0} Use_def(range)(Stat1) ==> false Discharge ==> AUTO APPLY() pointwise(g(Y)->cdr(Y),f(X)->range(X)) ==> Stat2: (FORALL x, y, z | (x = y + z) ¥imp (range(x) = range(y) + range(z))) & (FORALL x | (range(x) = 0) ¥eq (x = 0)) (x0,y0,z0,x0)-->Stat2(*) ==> false Discharge ==> QED -- Theorem domain_1: [Additivity of domain] ((X = Y+Z) ¥imp (domain(X) = domain(Y) + domain(Z))) & ((domain(X) = 0) ¥eq (X = 0)). Proof: Suppose_not(x0,y0,z0) ==> AUTO Suppose ==> Stat0: not (FORALL x | domain(x) = {car(y): y in x}) f0-->Stat0(Stat0*) ==> Stat1: domain(f0) /= {car(y): y in f0} Use_def(domain)(Stat1) ==> false Discharge ==> AUTO APPLY() pointwise(g(Y)->car(Y),f(X)->domain(X)) ==> Stat2: (FORALL x, y, z | (x = y + z) ¥imp (domain(x) = domain(y) + domain(z))) & (FORALL x | (domain(x) = 0) ¥eq (x = 0)) (x0,y0,z0,x0)-->Stat2(*) ==> false Discharge ==> QED -- Theorem domain_2: [Elements of domain, of range] (P in S) ¥imp ((car(P) in domain(S)) & (cdr(P) in range(S))). Proof: Suppose_not(p0,s) ==> AUTO Use_def(domain(s)) ==> AUTO Use_def(range) ==> Stat1: (car(p0) notin {car(p): p in s}) or (cdr(p0) notin {cdr(q): q in s}) (p0,p0)-->Stat1(*) ==> false Discharge ==> QED -- Theorem domain_3: [Typical elements of domain, of range] ([X,Y] in S) ¥imp ((X in domain(S)) & (Y in range(S))). Proof: Suppose_not(x0,y0,s) ==> AUTO ([x0,y0],s)-->Tdomain_2 ==> false Discharge ==> QED -- -- We now review a few basic properties of the restriction operation. -- Theorem restr_0: [The restriction of any (set or) map is included in it] (F ¥ON A) ¥incin F. Proof: Suppose_not(f,a) ==> AUTO Set_monot ==> {p: p in f| car(p) in a} ¥incin {p: p in f} Use_def(¥ON) ==> false Discharge ==> QED -- Theorem restr_1: [The domain of a restriction is included in the restraining set] (P in (F ¥ON A)) ¥imp (car(P) in A). Proof: Suppose_not(p0,f,a) ==> AUTO Use_def(¥ON) ==> Stat1: p0 in {p in f| car(p) in a} ()-->Stat1(*) ==> false Discharge ==> QED -- Theorem restr_2: [Each pair in a map belongs to the shoot of an element of its domain] (P = [X,Y]) ¥imp ((P in (F ¥ON {Z})) ¥eq ((Z = X) & ([Z,Y] in F))). Proof: Suppose_not(p0,x0,y0,f,z0) ==> Stat0: (p0=[x0,y0]) & ((p0 in (f ¥ON {z0})) ¥neq ((z0 = x0) &([z0,y0] in f))) Use_def(¥ON) ==> (f ¥ON {z0}) = {p in f | car(p) in {z0}} Suppose ==> Stat1: p0 in {p in f | car(p) in {z0}} ()-->Stat1(Stat1*) ==> (car(p0) = z0) & (p0 in f) TELEM ==> car([x0,y0]) = x0 EQUAL ==> [x0,y0] in f (Stat0*)Discharge ==> AUTO (Stat0*)ELEM ==> Stat2: (p0 notin {p in f | car(p) in {z0}}) & (z0=x0) & ([z0,y0] in f) ([z0,y0])-->Stat2(Stat2) ==> p0 /= [z0,y0] EQUAL ==> false Discharge ==> QED -- Theorem restr_3: [The elements of a map shoot are pairs of fixed first component] (Is_map(F) & (P in (F ¥ON {Z}))) ¥imp ((P = [Z,cdr(P)]) & (P in F)). Proof: Suppose_not(f,p0,x0) ==> AUTO Use_def(Is_map) ==> Stat1: (FORALL p in f | p = [car(p),cdr(p)]) (f,{x0})-->Trestr_0(*) ==> p0 in f (p0,f,{x0})-->Trestr_1(*) ==> car(p0) = x0 p0-->Stat1(Stat1) ==> p0 = [x0,cdr(p0)] Discharge ==> QED -- -- We then review a few basic properties of the application operation. -- Theorem image_0: [The image, under $0$, of any entity is $0$ by convention] (Z = 0) ¥imp (Svm(Z) & ((Z~[X]) = 0)). Proof: Suppose_not(z0,x0) ==> AUTO Suppose ==> not Svm(z0) Use_def(Is_map(z0)) ==> AUTO Use_def(Svm) ==> Stat1: not ((FORALL p in z0 | p = [car(p),cdr(p)]) & (FORALL p in z0, q in z0 | (car(p) = car(q)) ¥imp (p = q))) (p0,p1,p2)-->Stat1(*) ==> false Discharge ==> (z0 = 0) & ((z0~[x0]) /= 0) EQUAL ==> Stat2: (0~[x0]) /= 0 (0,{x0})-->Trestr_0(Stat2*) ==> AUTO Tpair_1(Stat2) ==> (cdr(0) = 0) & (arb(0 ¥ON {x0}) = 0) Use_def(~)(Stat2) ==> (0~[x0]) = cdr(arb(0 ¥ON {x0})) EQUAL(Stat2) ==> false Discharge ==> QED -- Theorem image_1: [Each pair in a map indicates membership of a operand-image pair in the map] ((X in domain(F)) & Is_map(F)) ¥imp ([X,F~[X]] in (F ¥ON {X}) * F). Proof: Suppose_not(x0,f) ==> Stat0: (x0 in domain(f)) & Is_map(f) & ([x0,f~[x0]] notin ((f ¥ON {x0}) * f)) Use_def(domain(f)) ==> AUTO Use_def(Is_map) ==> Stat1: (FORALL p in f | p = [car(p),cdr(p)]) & (x0 in {car(p): p in f}) (p0,p0)-->Stat1(Stat1) ==> (p0=[car(p0),cdr(p0)]) & (p0 in f) & ([x0,cdr(p0)] in f) & (x0 = car(p0)) Loc_def ==> a = arb(f ¥ON {x0}) (p0,car(p0),cdr(p0),f,x0)-->Trestr_2(Stat1) ==> Stat2: a in (f ¥ON {x0}) (a,f,{x0})-->Trestr_1(Stat2*) ==> car(a) = x0 (f,{x0})-->Trestr_0(Stat2*) ==> a in f a-->Stat1(Stat2*) ==> a = [car(a),cdr(a)] Use_def(~)(Stat3) ==> Stat3: (f~[x0]) = cdr(arb(f ¥ON {x0})) EQUAL(Stat1) ==> Stat4: ([x0,f~[x0]] in (f ¥ON {x0})) & ([x0,f~[x0]] in f) (Stat4,Stat0*)Discharge ==> QED -- Theorem image_2: [Application of set union to an operand is affected only by addend which has operand in its domain] (X notin domain(F)) ¥imp (((F+G)~[X]) = (G~[X])). Proof: Suppose_not(x0,f0,g0) ==> AUTO -- -- For, assuming the contrary, there would exist an $x0$ outside $domain(f0)$ such that -- $((f0+g0) ¥ON {x0}) ¥nincin (g0 ¥ON {x0})$... -- Use_def(~) ==> (((f0+g0)~[x0]) = cdr(arb((f0+g0) ¥ON {x0}))) & ((g0~[x0]) = cdr(arb(g0 ¥ON {x0}))) Suppose ==> ((f0+g0) ¥ON {x0}) = (g0 ¥ON {x0}) EQUAL ==> false; Discharge ==> AUTO Set_monot ==> {p in g0 | car(p) in {x0}} ¥incin {p in f0+g0 | car(p) in {x0}} Use_def(¥ON) ==> Stat1: {p in f0+g0 | car(p) in {x0}} ¥nincin {p in g0 | car(p) in {x0}} -- -- ...which, taking the definition of domain into account leads us to a contradiction. -- Use_def(domain(f0)) ==> AUTO e-->Stat1(*) ==> Stat2: (e in {p: p in f0+g0 | car(p) in {x0}}) & (e notin {p: p in g0 | car(p) in {x0}}) & (x0 notin {car(p): p in f0}) (p0,p0,p0)-->Stat2(Stat2*) ==> false Discharge ==> QED -- -- Theorem image_3: [Application of a map to an entity outside its domain yields $0$ by convention] (X notin domain(F)) ¥imp ((F~[X]) = 0). Proof: Suppose_not(x0,f) ==> AUTO (x0,f,0)-->Timage_2(*) ==> ((f+0)~[x0]) = (0~[x0]) (0,x0)-->Timage_0(*) ==> ((0~[x0]) = 0) & ((f+0) = f) EQUAL ==> false Discharge ==> QED -- Theorem image_4: [Meaning of application of a single-valued map] ( Svm(F) & (P in F) ) ¥imp (P = [car(P),F~[car(P)]]). Proof: Suppose_not(f,p0) ==> AUTO (p0,f)-->Tdomain_2(*) ==> car(p0) in domain(f) Use_def(Svm) ==> Stat1: (FORALL p in f, q in f | (car(p) = car(q)) ¥imp (p = q)) & Is_map(f) (car(p0),f)-->Timage_1(*) ==> [car(p0),f~[car(p0)]] in f TELEM ==> car([car(p0),f~[car(p0)]]) = car(p0) (p0,[car(p0),f~[car(p0)]])-->Stat1(*) ==> false Discharge ==> QED -- -- Single valued maps can always be represented in the following convenient form. -- Theorem image_5: [Form of a single-valued map] Svm(F) ¥eq (F = {[x,F~[x]]: x in domain(F)}). Proof: Suppose_not(f) ==> AUTO Suppose ==> (f = {[x,f~[x]]: x in domain(f)}) & (not Svm(f)) Use_def(Svm) ==> not( Is_map(f) & (FORALL p in f, q in f | (car(p) = car(q)) ¥imp (p = q))) Suppose ==> (not Is_map(f)) Use_def(Is_map(f)) ==> AUTO EQUAL ==> Stat1: not(FORALL p in {[x,f~[x]]: x in domain(f)} | p = [car(p),cdr(p)]) p0-->Stat1(Stat1*) ==> Stat2: (p0 in {[x,f~[x]]: x in domain(f)}) & (p0 /= [car(p0),cdr(p0)]) x0-->Stat2(Stat2) ==> false Discharge ==> Stat3: (not(FORALL p in f, q in f | (car(p) = car(q)) ¥imp (p = q))) (p1,q1)-->Stat3(*) ==> Stat4: (p1 in {[x,f~[x]]: x in domain(f)}) & (q1 in {[x,f~[x]]: x in domain(f)}) & (car(p1) = car(q1)) & (p1 /= q1) (x1,y1)-->Stat4(Stat4*) ==> Stat5: (p1 = [x1,f~[x1]]) & (q1 = [y1,f~[y1]]) & (car(p1) = car(q1)) (Stat5)ELEM ==> x1 = y1 EQUAL(Stat4) ==> false Discharge ==> Stat6: (f /= {[x,f~[x]]: x in domain(f)}) & Svm(f) p2-->Stat6(Stat6*) ==> (p2 in f) ¥neq (p2 in {[x,f~[x]]: x in domain(f)}) Use_def(domain) ==> (p2 in f) ¥neq (p2 in {[x,f~[x]]: x in {car(p): p in f}}) SIMPLF ==> (p2 in f) ¥neq (p2 in {[car(p),f~[car(p)]]: p in f}) Suppose ==> Stat7: p2 in {[car(p),f~[car(p)]]: p in f} p3-->Stat7(Stat6*) ==> (p3 in f) & ([car(p3),f~[car(p3)]] notin f) (f,p3)-->Timage_4(Stat6*) ==> false Discharge ==> Stat13: (p2 notin {[car(p),f~[car(p)]]: p in f}) & (p2 in f) p2-->Stat13(Stat13*) ==> p2 /= [car(p2),f~[car(p2)]] (f,p2)-->Timage_4(Stat6*) ==> false Discharge ==> QED -- -- -- -- Theorem svm_0: [The subsets of single valued maps are single valued maps] (Svm(F) & (G ¥incin F)) ¥imp Svm(G). Proof: Suppose_not(f,g) ==> AUTO Use_def(Svm(f)) ==> AUTO Suppose ==> not(Is_map(g)) Use_def(Is_map) ==> Stat1: (not(FORALL p in g | p = [car(p),cdr(p)])) & (FORALL p in f | p = [car(p),cdr(p)]) (p0,p0)-->Stat1(*) ==> false Discharge ==> AUTO Use_def(Svm) ==> Stat2: (not(FORALL p in g, q in g | (car(p) = car(q)) ¥imp (p = q))) & (FORALL p in f, q in f | (car(p) = car(q)) ¥imp (p = q)) & (g ¥incin f) (p1,q1,p1,q1)-->Stat2(Stat2*) ==> false Discharge ==> QED -- -- The union of domain-disjoint single valued maps is a single valued map. -- Theorem svm_1: [Union of domain-disjoint single-valued maps] (Svm(F) & Svm(G) & (domain(F) * domain(G) = 0)) ¥imp Svm(F + G). Proof: Suppose_not(f,g) ==> AUTO f-->Timage_5 ==> AUTO g-->Timage_5 ==> AUTO (f+g)-->Timage_5(*) ==> Stat1: (f+g /= {[z,(f+g)~[z]]: z in domain(f+g)}) & (f = {[x,f~[x]]: x in domain(f)}) & (g = {[y,g~[y]]: y in domain(g)}) & (domain(f) * domain(g) = 0) c-->Stat1(Stat1*) ==> (c in (f+g)) ¥neq (c in {[z,(f+g)~[z]]: z in domain(f+g)}) (f+g,f,g)-->Tdomain_1(Stat1*) ==> Stat2: domain(f+g) = domain(f)+domain(g) Suppose ==> Stat3: c in {[z,(f+g)~[z]]: z in domain(f+g)} z0-->Stat3(Stat2*) ==> (c = [z0,(f+g)~[z0]]) & (z0 in domain(f)+domain(g)) Suppose ==> z0 notin domain(f) (z0,f,g)-->Timage_2(Stat1*) ==> Stat4: (c notin {[y,g~[y]]: y in domain(g)}) & (z0 in domain(g)) & ((f+g)~[z0] = g~[z0]) EQUAL(Stat3) ==> c = [z0,g~[z0]] z0-->Stat4(Stat4*) ==> false Discharge ==> AUTO (z0,g,f)-->Timage_2(Stat1*) ==> Stat5: (c notin {[x,f~[x]]: x in domain(f)}) & (z0 in domain(f)) & ((g+f)~[z0] = f~[z0]) EQUAL(Stat3) ==> c = [z0,f~[z0]] z0-->Stat5(Stat5*) ==> false Discharge ==> AUTO (Stat1*)ELEM ==> Stat6: (c notin {[z,(f+g)~[z]]: z in domain(f+g)}) & (c in {[x,f~[x]]: x in domain(f)}+{[y,g~[y]]: y in domain(g)}) Suppose ==> Stat7: c in {[x,f~[x]]: x in domain(f)} (f+g,f,f+g)-->Tdomain_1 ==> AUTO x0-->Stat7(*) ==> (c = [x0,f~[x0]]) & (x0 notin domain(g)) & (x0 in domain(f+g)) (x0,g,f)-->Timage_2(Stat7*) ==> (((g+f)~[x0]) = (f~[x0])) & (g+f=f+g) EQUAL(Stat7) ==> c = [x0,(f+g)~[x0]] x0-->Stat6(Stat7*) ==> false Discharge ==> Stat8: c in {[y,g~[y]]: y in domain(g)} (f+g,g,f+g)-->Tdomain_1 ==> AUTO y0-->Stat8(*) ==> (c = [y0,g~[y0]]) & (y0 notin domain(f)) & (y0 in domain(f+g)) (y0,f,g)-->Timage_2(Stat8*) ==> ((f+g)~[y0]) = (g~[y0]) EQUAL(Stat8) ==> c = [y0,(f+g)~[y0]] y0-->Stat6(Stat8*) ==> false Discharge ==> QED -- -- -- Theorem singletonMap_0: [Domain and range of a singleton] (domain({P}) = {car(P)}) & (range({P}) = {cdr(P)}). Proof: Suppose_not(p0) ==> (domain({p0}) /= {car(p0)}) or (range({p0}) /= {cdr(p0)}) Use_def(range({p0})) ==> AUTO Use_def(domain) ==> Stat1: ({car(p): p in {p0}} /= {car(p0)}) or ({cdr(p): p in {p0}} /= {cdr(p0)}) SIMPLF(Stat1*) ==> false Discharge ==> QED -- Theorem singletonMap_1: [Singleton maps are single valued] ((F ¥incin {[X,Y]}) ¥imp Svm(F)) & (domain({[X,Y]}) = {X}) & (range({[X,Y]}) = {Y}). Proof: Suppose_not(f0,x0,y0) ==> AUTO ([x0,y0])-->TsingletonMap_0 ==> AUTO Suppose ==> Stat1: not(FORALL p in f0, q in f0 | (car(p) = car(q)) ¥imp (p = q)) (p0,q0)-->Stat1(Stat1*) ==> (p0 in f0) & (q0 in f0) & (p0 /= q0) Discharge ==> AUTO Use_def(Svm(f0)) ==> AUTO Use_def(Is_map) ==> Stat2: (not(FORALL p in f0 | p = [car(p),cdr(p)])) & (f0 ¥incin {[x0,y0]}) p3-->Stat2(Stat2) ==> false Discharge ==> QED -- Theorem singletonMap_2: [Singleton map application] (F = {[X,Y]}) ¥imp ((F~[X])=Y). Proof: Suppose_not(f0,x0,y0) ==> AUTO Use_def(~) ==> (f0~[x0]) = cdr(arb(f0 ¥ON {x0})) Use_def(¥ON) ==> Stat1: (f0 ¥ON {x0}) = {p in f0 | car(p) in {x0}} Suppose ==> Stat2: [x0,y0] notin {p in f0 | car(p) in {x0}} TELEM ==> car([x0,y0]) in {x0} [x0,y0]-->Stat2(*) ==> false Discharge ==> AUTO (Stat1)ELEM ==> arb({p in f0 | car(p) in {x0}}) in {p in f0 | car(p) in {x0}} EQUAL ==> Stat3: arb(f0 ¥ON {x0}) in {p in f0 | car(p) in {x0}} ()-->Stat3(*) ==> (arb(f0 ¥ON {x0}) = [x0,y0]) & (car([x0,y0]) = x0) TELEM ==> cdr([x0,y0]) = y0 EQUAL ==> false Discharge ==> QED -- Theorem singletonMap_3: [Transplant of singleton sub-map] (Svm(F) & ([X,Y] in F) & (Z notin domain(F)) & (G = F-{[X,Y]}+{[Z,Y]})) ¥imp (Svm(G) & (domain(G)=(domain(F)-{X}+{Z})) & (range(G) = range(F))). Proof: Suppose_not(f0,x0,y0,z0,g0) ==> AUTO ELEM ==> Stat0: (Svm(g0) & (domain(g0)=(domain(f0)-{x0}+{z0}))) ¥imp (range(g0) /= range(f0)) ({[x0,y0]},x0,y0)-->TsingletonMap_1(*) ==> (domain({[x0,y0]}) = {x0}) & (range({[x0,y0]}) = {y0}) & (f0-{[x0,y0]}+{[x0,y0]} = f0) (f0-{[x0,y0]}+{[x0,y0]},f0-{[x0,y0]},{[x0,y0]})-->Tdomain_1(*) ==> domain(f0-{[x0,y0]}+{[x0,y0]}) = (domain(f0-{[x0,y0]}) + {x0}) EQUAL ==> domain(f0) = (domain(f0-{[x0,y0]}) + {x0}) Suppose ==> Stat1: x0 in domain(f0-{[x0,y0]}) Use_def(domain)(Stat1) ==> Stat2: x0 in {car(p): p in f0-{[x0,y0]}} p0-->Stat2(Stat2) ==> (p0 in f0) & (p0 /= [x0,y0]) & (car(p0) = car([x0,y0])) Use_def(Svm) ==> Stat3: (FORALL p in f0, q in f0 | (car(p) = car(q)) ¥imp (p = q)) (p0,[x0,y0])-->Stat3(*) ==> false Discharge ==> AUTO ({[z0,y0]},z0,y0)-->TsingletonMap_1(*) ==> Svm({[z0,y0]}) & (domain({[z0,y0]}) = {z0}) & (range({[z0,y0]}) = {y0}) (f0-{[x0,y0]}+{[z0,y0]},f0-{[x0,y0]},{[z0,y0]})-->Tdomain_1(*) ==> domain(f0-{[x0,y0]}+{[z0,y0]}) = domain(f0) - {x0} + {z0} (f0,f0-{[x0,y0]})-->Tsvm_0(*) ==> Svm(f0-{[x0,y0]}) (f0,f0-{[x0,y0]},f0)-->Tdomain_1(*) ==> z0 notin domain(f0-{[x0,y0]}) (f0-{[x0,y0]},{[z0,y0]})-->Tsvm_1(*) ==> Svm(f0-{[x0,y0]}+{[z0,y0]}) (f0-{[x0,y0]}+{[z0,y0]},f0-{[x0,y0]},{[z0,y0]})-->Trange_1(*) ==> range(f0-{[x0,y0]}+{[z0,y0]}) = range(f0-{[x0,y0]}) + {y0} (f0-{[x0,y0]}+{[x0,y0]},f0-{[x0,y0]},{[x0,y0]})-->Trange_1(*) ==> range(f0-{[x0,y0]}+{[x0,y0]}) = range(f0-{[x0,y0]}) + {y0} EQUAL ==> false Discharge ==> QED -- -- -- -- -- \subsection{Basic laws on the power-set global operation} -- Def pow: [Family of all subsets of a given set] pow(S) := { x : x ¥incin S } -- -- -- Our next theorem characterizes the powerset formation operation in -- more usable terms than the very definition of this construct. It also -- proves that no set can equal is own powerset (else it should belong to itself, -- against the acyclicity of membership). -- Theorem pow_0: [Characterization of powerset; also: no set equals its own powerset] ((X incs Y) ¥eq (Y in pow(X))) & (X /= pow(X)). Proof: Suppose_not(x0,y0) ==> AUTO -- -- We begin by excluding the possibility that $x0 = pow(x0)$: -- Suppose ==> Stat0: x0 notin {y: y ¥incin x0} x0-->Stat0 ==> false; Discharge ==> AUTO Use_def(pow(x0)) ==> AUTO -- -- Arguing by contradiction, if $x0,y0$ constituted a counterexample, -- then either one of the literals $x0 incs y0$ and $y0 in {y: y ¥incin x0}$ -- would be true and the other one would be false. -- EQUAL ==> Stat1: (x0 incs y0) ¥neq (y0 in {y: y ¥incin x0}) -- -- If it is the second that is true then, via a substitution in the setformer, -- we would contradict the falsity of the first. -- Suppose ==> Stat2: y0 in {y: y ¥incin x0} y1-->Stat2(Stat1*) ==> false; Discharge ==> Stat3: y0 notin {y: y ¥incin x0} -- -- But then the literals $x0 incs y0$ and $y0 notin {y: y ¥incin x0}$ should hold together, -- which gives us a contradiction if we replace the bounded variable $y$ of the setformer -- by $y0$. -- y0-->Stat3(Stat1*) ==>false Discharge ==> QED -- Theorem pow_1: [Monotonicity of powerset] (S incs X) ¥imp ((pow(X) + {0,X}) ¥incin pow(S)). Proof: Suppose_not(s0,x0) ==> AUTO Set_monot ==> { x : x ¥incin x0 } ¥incin { x : x ¥incin s0 } Use_def(pow) ==> Stat1: (0 notin { x : x ¥incin s0 }) or (x0 notin { x : x ¥incin s0 }) (0,x0)-->Stat1 ==> false Discharge ==> QED -- Theorem pow_2: [Powerset of null set and of singletons] (pow(0) = {0}) & (pow({X}) = {0,{X}}). Proof: Suppose_not(x0) ==> AUTO Suppose ==> pow(0) /= {0} (0,0)-->Tpow_1 ==> Stat0: pow(0) ¥nincin {0} y0-->Stat0(Stat0*) ==> Stat1: (y0 in pow(0)) & (y0 notin {0}) (0,y0)-->Tpow_0(Stat1*) ==> false Discharge ==> (pow({x0}) /= {0,{x0}}) ({x0},{x0})-->Tpow_1 ==> Stat2: pow({x0}) ¥nincin {0,{x0}} y1-->Stat2 ==> Stat3: (y1 in pow({x0})) & (y1 notin {0,{x0}}) ({x0},y1)-->Tpow_0(Stat3*) ==> false Discharge ==> QED -- -- -- -- \subsection{Basic laws on the finiteness property} -- -- -- Traditionally, finiteness is defined through the notion of cardinality of a set: -- a set is finite if its cardinality precedes the first infinite ordinal. As a shortcut, to begin -- developing an acceptable formal treatment of finiteness without much preparatory work, we adopt -- here the following definition (reminiscent of Tarski's 1924 paper "Sur les ensembles fini"): -- a set $F$ is \emph{finite} if every non-null family of subsets of $F$ owns an inclusion-minimal element. -- This notion can be specified very succinctly in terms of the powerset operator. -- -- Def Fin: [Finiteness property] Finite(F) := (FORALL g in (pow(pow(F)) - {0}) | (EXISTS m | (g * pow(m)) = {m})) -- Theorem fin_0: [Monotonicity of finiteness] ((Y incs X) & Finite(Y)) ¥imp Finite(X). Proof: Suppose_not(y0,x0) ==> AUTO (y0,x0)-->Tpow_1(*) ==> pow(y0) incs pow(x0) Use_def(Finite) ==> Stat1: (not(FORALL g in (pow(pow(x0)) - {0}) | (EXISTS m | (g * pow(m)) = {m}))) & (FORALL gp in (pow(pow(y0)) - {0}) | (EXISTS m | (gp * pow(m)) = {m})) (pow(y0),pow(x0))-->Tpow_1(*) ==> pow(pow(y0)) incs pow(pow(x0)) (g0,g0)-->Stat1(Stat1*) ==> (not(EXISTS m | (g0 * pow(m)) = {m})) & (EXISTS m | (g0 * pow(m)) = {m}) Discharge ==> QED -- THEORY finiteInduction(s0, P(S)) Finite(s0) & P(s0) END finiteInduction -- ENTER_THEORY finiteInduction -- Theorem finiteInduction0: (EXISTS m | ({s ¥incin s0 | P(s)} * pow(m)) = {m}). Proof: Suppose_not() ==> AUTO Assump ==> Finite(s0) & P(s0) Use_def(Finite) ==> Stat1: (FORALL g in (pow(pow(s0)) - {0}) | (EXISTS m | (g * pow(m)) = {m})) ({s ¥incin s0 | P(s)})-->Stat1 ==> {s ¥incin s0 | P(s)} notin (pow(pow(s0)) - {0}) Suppose ==> Stat2: s0 notin {s ¥incin s0 | P(s)} s0-->Stat2 ==> false; Discharge ==> {s ¥incin s0 | P(s)} notin (pow(pow(s0))) Use_def(pow) ==> Stat3: {s ¥incin s0 | P(s)} notin {y: y ¥incin {z: z ¥incin s0}} ({s ¥incin s0 | P(s)})-->Stat3 ==> Stat4: {s ¥incin s0 | P(s)} ¥nincin {z: z ¥incin s0} s1-->Stat4 ==> Stat5: (s1 in {s: s ¥incin s0 | P(s)}) & (s1 notin {z: z ¥incin s0}) (s,s1)-->Stat5(Stat5*) ==> false Discharge ==> QED -- APPLY(v1_thryvar:fin_thryvar) Skolem() ==> Theorem finiteInduction1: ({s ¥incin s0 | P(s)} * pow(fin_thryvar)) = {fin_thryvar} -- Theorem finiteInduction2: [Minimal finite set satisfying $P$] (S ¥incin fin_thryvar) ¥imp( Finite(S) & ( P(S) ¥eq (S = fin_thryvar)) ). Proof: Suppose_not(s1) ==> AUTO ()-->TfiniteInduction1 ==> (({s ¥incin s0 | P(s)} * pow(fin_thryvar)) = {fin_thryvar}) & Stat1: (fin_thryvar in {s ¥incin s0 | P(s)}) ()-->Stat1 ==> (fin_thryvar ¥incin s0) & P(fin_thryvar) Assump ==> Finite(s0) (s0,fin_thryvar)-->Tfin_0 ==> Finite(fin_thryvar) (fin_thryvar,s1)-->Tfin_0 ==> P(s1) ¥neq (s1 = fin_thryvar) Suppose ==> s1 = fin_thryvar EQUAL ==> false; Discharge ==> (s1 notin ({s ¥incin s0 | P(s)} * pow(fin_thryvar))) & P(s1) Suppose ==> s1 notin pow(fin_thryvar) Use_def(pow) ==> Stat2: s1 notin {y: y ¥incin fin_thryvar} s1--> Stat2 ==> false Discharge ==> Stat3: s1 notin {s ¥incin s0 | P(s)} s1-->Stat3 ==> false Discharge ==> QED -- ENTER_THEORY Set_theory -- --DISPLAY finiteInduction -- --THEORY finiteInduction(s0,P(S)) -- Finite(s0) & P(s0) --==>(fin_thryvar) -- (FORALL S | (S ¥incin fin_thryvar) ¥imp ( Finite(S) & ( P(S) ¥eq (S = fin_thryvar)) )) --END finiteInduction -- Theorem fin_1: [Finiteness of the union of a finite set with a singleton] Finite(F) ¥imp Finite(F + {X}). Proof: Suppose_not(f0,x0) ==> AUTO -- -- Arguing by contradiction, suppose that $f0$ and $x0$ are such that $f0$ is finite but $f0 + {x0}$ is not. -- A nonnull familiy $g0$ of subsets of $f0 +{x0}$ must then exist none of whose elements is minimal. -- On the other hand ${y-{x0}: y in g0}$, which is also nonnull but consists entirely of subsets of $f0$, -- must have a minimal element $m0=y0-{x0}$, with $y0 in g0$. -- Use_def(Finite) ==> Stat0: (not(FORALL g in (pow(pow(f0+{x0})) - {0}) | (EXISTS m | (g * pow(m)) = {m}))) & Stat1: (FORALL h in (pow(pow(f0)) - {0}) | (EXISTS m | (h * pow(m)) = {m})) g0-->Stat0(Stat0) ==> Stat2: (not (EXISTS m | (g0 * pow(m)) = {m})) & (g0 in pow(pow(f0+{x0}))) & (g0 /= 0) Loc_def ==> Stat3: h0 = {y-{x0}: y in g0} Suppose ==> h0 notin (pow(pow(f0)) - {0}) Suppose ==> Stat4: {y-{x0}: y in g0} = 0 (arb(g0))-->Stat4(Stat2,Stat2) ==> false; Discharge ==> AUTO Use_def(pow) ==> Stat5: h0 notin {h: h ¥incin {k: k ¥incin f0}} h0-->Stat5(Stat5*) ==> Stat6: h0 ¥nincin {k: k ¥incin f0} k0-->Stat6(Stat3*) ==> Stat7: (k0 in {y-{x0}: y in g0}) & (k0 notin {k: k ¥incin f0}) (y1,k0)-->Stat7(Stat7*) ==> (y1 in g0) & (y1 ¥nincin (f0 + {x0})) Use_def(pow)(Stat2,Stat2) ==> Stat8: g0 in {h: h ¥incin {k: k ¥incin (f0 + {x0})}} h1-->Stat8(Stat7*) ==> Stat9: y1 in {k: k ¥incin (f0 + {x0})} k1-->Stat9(Stat7*) ==> false Discharge ==> AUTO (h0,m0)-->Stat1(Stat3*) ==> Stat10: (m0 in {y-{x0}: y in g0}) & ((h0 * pow(m0)) = {m0}) y0-->Stat10(Stat10*) ==> Stat11: (m0 = (y0-{x0})) & (y0 in g0) -- -- We will reach the desired contradiction by showing that either $m0$ or $y0=m0+{x0}$ is minimal in $g0$. -- We check first that $m0$ itself must be minimal when $m0 in g0$. -- Suppose ==> m0 in g0 m0-->Stat2(Stat10*) ==> Stat12: (g0 * pow(m0)) ¥nincin {m0} Use_def(pow(m0)) ==> AUTO z0-->Stat12(Stat3*) ==> Stat13: (z0 in {h: h ¥incin m0}) & (z0 notin {y-{x0}: y in g0}) & (z0 in g0) (h2,z0)-->Stat13(Stat11*) ==> false Discharge ==> AUTO -- -- Suppose next that $m0 notin g0$; we will reach a contradiction by showing that $y0$ is minimal in $g0$. -- Suppose ==> y0 notin pow(y0) Use_def(pow) ==> Stat13a: y0 notin {s: s ¥incin y0} y0-->Stat13a(Stat13a*) ==> false Discharge ==> AUTO y0-->Stat2(Stat11*) ==> Stat14: (g0 * pow(y0)) ¥nincin {y0} Use_def(pow(y0)) ==> AUTO z1-->Stat14(Stat11*) ==> Stat15: (z1 in {h: h ¥incin y0}) & (z1 in g0) & ((z1-{x0}) /= (y0-{x0})) EQUAL(Stat10) ==> (h0 * pow(y0-{x0})) = {y0-{x0}} Suppose ==> (z1-{x0}) notin pow(y0-{x0}) Use_def(pow)(Stat15) ==> Stat16: (z1-{x0}) notin {h: h ¥incin (y0-{x0})} (z1-{x0})-->Stat16(Stat16*) ==> (z1-{x0}) ¥nincin (y0-{x0}) h3-->Stat15(Stat16*) ==> false Discharge ==> AUTO Suppose ==> Stat17: (z1-{x0}) notin {y-{x0}: y in g0} z1-->Stat17(Stat15*) ==> false; Discharge ==> (z1-{x0}) in h0 (Stat15*)Discharge ==> QED -- -- Theorem fin_2: [Singletons are finite] Finite({X}) & Finite(0). Proof: Suppose_not(x0) ==> AUTO ({x0},0)-->Tfin_0 ==> not Finite({x0}) Use_def(Finite) ==> Stat1: (not(FORALL g in (pow(pow({x0})) - {0}) | (EXISTS m | (g * pow(m)) = {m}))) g0-->Stat1 ==> Stat2: (not (EXISTS m | (g0 * pow(m)) = {m})) & (g0 in (pow(pow({x0})) - {0})) Use_def(pow) ==> Stat3: g0 in {y: y ¥incin pow({x0})} x0-->Tpow_2 ==> AUTO y0-->Stat3(Stat2*) ==> Stat4: (g0 /= 0) & (g0 ¥incin {0,{x0}}) Suppose ==> 0 in g0 0-->Stat2(Stat3*) ==> false Discharge ==> g0 = {{x0}} ({x0})-->Stat2(Stat3*) ==> false Discharge ==> QED -- -- THEORY finiteImage(s0,f(X)) Finite(s0) END finiteImage -- ENTER_THEORY finiteImage -- Theorem finiteImage: Finite({f(x): x in s0}). Proof: Suppose_not() ==> AUTO -- -- We can prove the claim by means of finite induction. Arguing by contradiction, let us -- assume that $s0$ has, via the global function $f(X)$, infinite image; then take an $s1$ -- which is finite and minimal (w.r.t. inclusion) and has, much like $s0$, infinite image -- ${f(x): x in s1}$. As one sees easily, $s1 /= 0$; hence, if we remove an element $a$ -- from $s1$, we find that ${f(x): x in (s1 - {a})}$ is finite in consequence of the -- supposed minimality of $s1$. Since the union of two finite sets is finite, -- we get the finiteness of ${f(x): x in (s1 - {a})} + {f(a)}$, -- which hence must differ from ${f(x): x in s1}$. -- Assump ==> Finite(s0) APPLY(fin_thryvar:s1) finiteInduction(s0->s0,P(S)->(not Finite({f(x): x in S}))) ==> Stat1: (FORALL s | (s ¥incin s1) ¥imp ( Finite(s) & ((not Finite({f(x): x in s})) ¥eq (s = s1)) )) s1-->Stat1 ==> not Finite({f(x): x in s1}) Loc_def ==> Stat0: a = arb(s1) (f(a))-->Tfin_2 ==> Finite({f(a)}) & Finite(0) Suppose ==> s1 = 0 ELEM ==> {f(x): x in 0} = 0 EQUAL ==> false Discharge ==> AUTO (Stat0)ELEM ==> Stat2: ((s1 - {a}) ¥incin s1) & ((s1 - {a}) /= s1) Suppose ==> {f(x): x in s1} = ({f(x): x in (s1 - {a})} + {f(a)}) (s1 - {a})-->Stat1(Stat2*) ==> Finite({f(x): x in (s1 - {a})}) ({f(x): x in (s1 - {a})},f(a))-->Tfin_1(Stat1*) ==> Finite({f(x): x in (s1 - {a})} + {f(a)}) EQUAL(Stat1) ==> false Discharge ==> AUTO -- -- On the other hand, ${f(x): x in (s1 - {a})} + {f(a)}$ and ${f(x): x in s1}$ must be equal: -- in fact $a in s1$, and therefore $f(a) in {f(x): x in s1}$; moreover, by monotonicity, -- ${f(x): x in (s1 - {a})} ¥incin {f(x): x in s1}$ and... -- Set_monot ==> {f(x): x in (s1 - {a})} ¥incin {f(x): x in s1} Suppose ==> Stat3: f(a) notin {f(x): x in s1} a-->Stat3(Stat2,Stat2*) ==> false; Discharge ==> Stat4: {f(x): x in s1} ¥nincin ({f(x): x in (s1 - {a})} + {f(a)}) -- -- ...one easily sees that ${f(x): x in s1} ¥incin ({f(x): x in (s1 - {a})} + {f(a)})$, ... -- b-->Stat4(Stat4*) ==> Stat5: (b in {f(x): x in s1}) & (b notin ({f(x): x in (s1 - {a})} + {f(a)})) x0-->Stat5(Stat5*) ==> (f(x0) notin {f(x): x in (s1 - {a})}) & (x0 in s1) & (f(x0) /= f(a)) Suppose ==> x0 = a EQUAL(Stat5) ==> false; Discharge ==> Stat6: (f(x0) notin {f(x): x in (s1 - {a})}) & (x0 /= a) & (x0 in s1) x0-->Stat6(Stat6*)==> false -- -- which leads us to the sought contradiction. -- Discharge ==> QED -- -- ENTER_THEORY Set_theory -- -- DISPLAY finiteImage -- -- THEORY finiteImage(s0,f(X)) -- Finite(s0) -- ==> -- Finite({f(x): x in s0}) -- END finiteImage -- --PAUSE HERE -- -- -- Theorem fin_0a: Finite(0) & ((Finite(F) & ((G ¥incin F) or (G = F+{X}))) ¥imp Finite(G)). Proof+: Suppose_not(f0,g0,x0) ==> AUTO ELEM ==> Finite(f0) & (g0 = f0+{x0}) & (not Finite(g0)) Loc_def ==> s0 = {x0} EQUAL ==> false Discharge ==> QED Ñ- -- -- Theorem fin_b: Finite({X}). Proof: Suppose_not(x0) ==> AUTO (0,{x0},x0)-->Tfin_0a(*) ==> false Discharge ==> QED -- -- Theorem part_whole_0b: [The domain operation applied to a single-valued map preserves finiteness] Svm(F) ¥imp (Finite(F) ¥eq Finite(domain(F))). Proof+: Suppose_not(g0) ==> AUTO Suppose ==> Finite(domain(g0)) g0-->Timage_5(*) ==> g0 = {[x,g0~[x]]: x in domain(g0)} APPLY() finiteImage(s0->domain(g0),f(X)->[X,g0~[X]]) ==> Finite({[x,g0~[x]]: x in domain(g0)}) Discharge ==> Finite(g0) Loc_def ==> d0 = domain(g0) EQUAL ==> false Discharge ==> QED -- Theorem part_whole_0a: [The domain operation applied to a single-valued map preserves finiteness] (Svm(F) & (D=domain(F))) ¥imp (Finite(F) ¥eq Finite(D)). Proof+: Suppose_not(f0,d0) ==> AUTO Suppose ==> Finite(f0) EQUAL ==> false; Discharge ==> AUTO f0-->Timage_5 ==> f0 = {[x,f0~[x]]: x in domain(f0)} APPLY() finiteImage(s0->domain(f0),f(X)->[X,f0~[X]]) ==> Finite({[x,f0~[x]]: x in domain(f0)}) Discharge ==> QED --BEGIN HERE --PAUSE HERE -- Theorem part_whole_0: [The domain operation applied to a single-valued map preserves finiteness] Svm(F) ¥imp (Finite(F) ¥eq Finite(domain(F))). Proof: Suppose_not(f1) ==> AUTO Suppose ==> Finite(f1) APPLY() finiteImage(s0->f1,f(X)->car(X)) ==> Finite({car(x): x in f1}) Use_def(domain) ==> false Discharge ==> AUTO f1-->Timage_5 ==> f1 = {[x,(f1~[x])]: x in domain(f1)} APPLY() finiteImage(s0->domain(f1),f(X)->([x,(f1~[x])])) ==> Finite({[x,(f1~[x])]: x in domain(f1)}) EQUAL ==> false Discharge ==> QED -- Theorem part_whole_a: [The part is smaller than the whole] (Svm(H) & Finite(H) & (range(H) incs domain(H))) ¥imp (range(H) = domain(H)). Proof: Suppose_not(h2) ==> AUTO -- -- For, assuming that a counterexample $h1$ to the claim exists, a minimal counterexample -- $h0$ would be provided by the finite induction principle. -- APPLY (fin_thryvar:h0) finiteInduction(s0->h2,P(S)->(Svm(S) & (range(S) incs domain(S)) & (range(S) /= domain(S)))) ==> Stat1: (FORALL S | (S ¥incin h0) ¥imp ( Finite(S) & ( (Svm(S) & (range(S) incs domain(S)) & (range(S) /= domain(S))) ¥eq (S = h0)) )) h0-->Stat1(Stat1*) ==> Stat2: (range(h0) /= domain(h0)) & Finite(h0) & Svm(h0) & (range(h0) incs domain(h0)) -- -- Let us pick a $p0$ in $h0$ such that $cdr(p0) notin domain(h0)$ -- and put $h1=h0-{p0}$. Also $h1$ is a function; moreover -- $range(h1)=range(h0)-{cdr(p0)}$, $range(h1) incs domain(h0)$, -- and $domain(h0) incs domain(h1)$ holds, and hence by the -- minimality assumption we have $range(h1)=domain(h1)$. -- By inserting $p0$ back into $h1$, we get -- $range(h1)+{cdr(p0)} = range(h0)$, $range(h0) incs domain(h0)$, -- and $domain(h0) = domain(h1)+{car(p0)}$ and -- therefore either $car(p0) = cdr(p0)$ or $car(p0) in range(h1)$; -- however both cases must be rejected: the former in light of -- the fact $cdr(p0) notin domain(h0)$, -- because $p0 in h0$; the latter in view of the single-valuedness -- of $h0$ since $range(h1)=domain(h1)$ and -- $domain(h1) incin domain(h0)$. -- Use_def(range(h0)) ==> AUTO y0-->Stat2(Stat2*) ==> Stat3: (y0 in {cdr(p): p in h0}) & (y0 notin domain(h0)) p0-->Stat3(Stat3*) ==> (p0 in h0) & (cdr(p0) = y0) Loc_def ==> Stat4: h1 = h0-{p0} (h0,h1,h0)-->Tdomain_1(Stat4*) ==> domain(h1) ¥incin domain(h0) Suppose ==> Stat5: range(h1) ¥nincs domain(h1) y1-->Stat5(Stat2*) ==> (y1 /= y0) & (y1 in range(h0)) & (y1 notin range(h1)) Use_def(range)(Stat5) ==> Stat6: (y1 in {cdr(p): p in h0}) & (y1 notin {cdr(p): p in h1}) (p2,p2)-->Stat6(Stat3) ==> false Discharge ==> AUTO (h0,h1)-->Tsvm_0 ==> AUTO h1-->Stat1(Stat2*) ==> range(h1) = domain(h1) p0-->TsingletonMap_0(Stat3*) ==> (range({p0}) = {y0}) & (domain({p0}) = {car(p0)}) (h0,h1,{p0})-->Trange_1(Stat2*) ==> (range(h1) + {y0}) incs domain(h0) (h0,h1,{p0})-->Tdomain_1(Stat3*) ==> (car(p0) = y0) or (car(p0) in domain(h1)) Use_def(domain)(Stat3,Stat3) ==> Stat9: (y0 notin {car(p): p in h0}) & (domain(h1) = {car(q): q in h1}) p0-->Stat9(Stat3*) ==> Stat10: car(p0) in {car(p): p in h1} p1-->Stat10(Stat3*) ==> (p1 /= p0) & (p1 in h0) & (p0 in h0) & (car(p1) = car(p0)) Use_def(Svm) ==> Stat11: (FORALL p in h0, q in h0 | (car(p) = car(q)) ¥imp (p = q)) (p1,p0)-->Stat11(Stat10*) ==> false Discharge ==> QED -- --BEGIN HERE -- Theorem part_whole_1: [The part is smaller than the whole] (Svm(H) & Finite(H) & (range(H) incs domain(H))) ¥imp (range(H) = domain(H)). Proof+: Suppose_not(h2) ==> AUTO -- -- For, assuming that a counterexample $h1$ to the claim exists, a minimal counterexample -- $h0$ would be provided by the finite induction principle. -- APPLY (fin_thryvar:h0) finiteInduction(s0->h2,P(S)->(Svm(S) & (range(S) incs domain(S)) & (range(S) /= domain(S)))) ==> Stat1: (FORALL S | (S ¥incin h0) ¥imp ( Finite(S) & ( (Svm(S) & (range(S) incs domain(S)) & (range(S) /= domain(S))) ¥eq (S = h0)) )) h0-->Stat1(Stat1*) ==> Stat2: (range(h0) /= domain(h0)) & Finite(h0) & Svm(h0) & (range(h0) incs domain(h0)) -- -- Let us pick a $p0$ in $h0$ such that $cdr(p0) notin domain(h0)$ -- and put $h1=h0-{p0}$. By Theorem svm_0, also $h1$ is a function; moreover -- $range(h1)=range(h0)-{cdr(p0)}$, $range(h1) incs domain(h0)$, -- and $domain(h0) incs domain(h1)$ holds, and hence by the -- minimality assumption we have $range(h1)=domain(h1)$. -- By inserting $p0$ back into $h1$, we get -- $range(h1)+{cdr(p0)} = range(h0)$, $range(h0) incs domain(h0)$, -- and $domain(h0) = domain(h1)+{car(p0)}$ and -- therefore either $car(p0) = cdr(p0)$ or $car(p0) in range(h1)$; -- however both cases must be rejected: the former in light of -- the fact $cdr(p0) notin domain(h0)$, -- because $p0 in h0$; the latter in view of the single-valuedness -- of $h0$ since $range(h1)=domain(h1)$ and -- $domain(h1) incin domain(h0)$. -- Use_def(range(h0)) ==> AUTO y0-->Stat2(Stat2*) ==> Stat3: (y0 in {cdr(p): p in h0}) & (y0 notin domain(h0)) p0-->Stat3(Stat3*) ==> Stat4: (p0 in h0) & (cdr(p0) = y0) Loc_def ==> h1 = h0-{p0} Suppose ==> Stat5: range(h1) ¥nincs domain(h1) (h0,h1,h0)-->Tdomain_1(Stat3*) ==> domain(h1) ¥incin domain(h0) y1-->Stat5(Stat2*) ==> (y1 /= y0) & (y1 in range(h0)) & (y1 notin range(h1)) Use_def(range)(Stat5) ==> Stat6: (y1 in {cdr(p): p in h0}) & (y1 notin {cdr(p): p in h1}) (p2,p2)-->Stat6(Stat4) ==> false Discharge ==> AUTO h1-->Stat1(Stat2*) ==> range(h1) = domain(h1) p0-->TsingletonMap_0(Stat4*) ==> (range({p0}) = {y0}) & (domain({p0}) = {car(p0)}) (h0,h1,{p0})-->Trange_1(Stat2*) ==> (range(h1) + {y0}) incs domain(h0) (h0,h1,{p0})-->Tdomain_1(Stat4*) ==> (car(p0) = y0) or (car(p0) in domain(h1)) Use_def(domain)(Stat3,Stat3) ==> Stat9: (y0 notin {car(p): p in h0}) & (domain(h1) = {car(q): q in h1}) p0-->Stat9(Stat4*) ==> Stat10: car(p0) in {car(p): p in h1} p1-->Stat10(Stat4*) ==> (p1 /= p0) & (p1 in h0) & (p0 in h0) & (car(p1) = car(p0)) Use_def(Svm) ==> Stat11: (FORALL p in h0, q in h0 | (car(p) = car(q)) ¥imp (p = q)) (p1,p0)-->Stat11(Stat10*) ==> false Discharge ==> QED -- -- -- -- -- \section{Rudiments about (finite) graphs} -- -- -- -- \subsection{Cartesian product} -- Def cartesianProduct: [Cartesian product] Def(S ¥PROD T) := {[x,y]: x in S, y in T} -- Theorem cartesian_0: (X in (S ¥PROD T)) ¥eq ((X = [car(X),cdr(X)]) & (car(X) in S) & (cdr(X) in T)). Proof: Suppose_not(p0,s0,t0) ==> AUTO Use_def(¥PROD) ==> (s0 ¥PROD t0) = {[x,y]: x in s0, y in t0} Suppose ==> Stat1: p0 in {[x,y]: x in s0, y in t0} (x0,y0)-->Stat1(Stat1) ==> (p0 = [car(p0),cdr(p0)]) & (car(p0) in s0) & (cdr(p0) in t0) Discharge ==> Stat2: p0 notin {[x,y]: x in s0, y in t0} (car(p0),cdr(p0))-->Stat2(*) ==> false Discharge ==> QED -- Theorem cartesian_1: (S /= 0) ¥imp (range(S ¥PROD T) = T). Proof: Suppose_not(s0,t0) ==> Stat1: (s0 /= 0) & (range(s0 ¥PROD t0) /= t0) Use_def(range(s0 ¥PROD t0)) ==> AUTO (a0,b0)-->Stat1(*) ==> Stat2: (a0 in s0) & ((b0 in {cdr(u): u in (s0 ¥PROD t0)}) ¥neq (b0 in t0)) Use_def(¥PROD) ==> (b0 in {cdr(u): u in {[x,y]: x in s0, y in t0}}) ¥neq (b0 in t0) Suppose ==> Stat3: b0 notin {cdr(u): u in {[x,y]: x in s0, y in t0}} TELEM ==> b0 = cdr([a0,b0]) ([a0,b0])-->Stat3(Stat3*) ==> Stat4: [a0,b0] notin {[x,y]: x in s0, y in t0} (a0,b0)-->Stat4(Stat2*) ==> false Discharge ==> Stat5: b0 in {cdr(u): u in {[x,y]: x in s0, y in t0}} u0-->Stat5(Stat5*) ==> Stat6: (u0 in {[x,y]: x in s0, y in t0}) & (b0 = cdr(u0)) (x0,y0)-->Stat6(Stat6) ==> (b0 in t0) (Stat2*)Discharge ==> QED -- Theorem cartesian_2: (T /= 0) ¥imp (domain(S ¥PROD T) = S). Proof: Suppose_not(t0,s0) ==> Stat1: (t0 /= 0) & (domain(s0 ¥PROD t0) /= s0) Use_def(domain(s0 ¥PROD t0)) ==> AUTO (a0,b0)-->Stat1(*) ==> Stat2: (a0 in t0) & ((b0 in {car(u): u in (s0 ¥PROD t0)}) ¥neq (b0 in s0)) Use_def(¥PROD) ==> (b0 in {car(u): u in {[x,y]: x in s0, y in t0}}) ¥neq (b0 in s0) Suppose ==> Stat3: b0 notin {car(u): u in {[x,y]: x in s0, y in t0}} TELEM ==> b0 = car([b0,a0]) ([b0,a0])-->Stat3(Stat3*) ==> Stat4: [b0,a0] notin {[x,y]: x in s0, y in t0} (b0,a0)-->Stat4(Stat2*) ==> false Discharge ==> Stat5: b0 in {car(u): u in {[x,y]: x in s0, y in t0}} u0-->Stat5(Stat5*) ==> Stat6: (u0 in {[x,y]: x in s0, y in t0}) & (b0 = car(u0)) (x0,y0)-->Stat6(Stat6) ==> (b0 in s0) (Stat2*)Discharge ==> QED -- Theorem cartesian_3: [Annichilator of Cartesian product] ((S ¥PROD 0) = 0) & ((0 ¥PROD S) = 0). Proof: Suppose_not(s0) ==> AUTO Suppose ==> Stat1: ({[x,y]: x in s0, y in 0} /= 0) or ({[x,y]: x in 0, y in s0} /= 0) (x1,y1,x2,y2)-->Stat1(Stat1*) ==> false; Discharge ==> AUTO Use_def(¥PROD) ==> false Discharge ==> QED -- Theorem cartesian_4: [Domain of Cartesian square] domain(S ¥PROD S) = S. Proof: Suppose_not(s0) ==> AUTO (s0,s0)-->Tcartesian_2(*) ==> s0 = 0 s0-->Tcartesian_3(*) ==> (s0 ¥PROD 0) = 0 0-->Tdomain_1(*) ==> domain(0) = 0 EQUAL ==> false Discharge ==> QED -- Theorem cartesian_5: [Monotonicity of Cartesian product] ((S ¥incin Sp) & (T ¥incin Tp)) ¥imp ((S ¥PROD T) ¥incin (Sp ¥PROD Tp)). Proof: Suppose_not(s0,s1,t0,t1) ==> AUTO Use_def(¥PROD) ==> Stat1: {[x,y]: x in s0, y in t0} ¥nincin {[x,y]: x in s1, y in t1} c-->Stat1(Stat1*) ==> Stat2: (c in {[x,y]: x in s0, y in t0}) & (c notin {[x,y]: x in s1, y in t1}) (x,y,x,y)-->Stat2(*) ==> false Discharge ==> QED -- Theorem cartesian_6: [All subsets of a Cartesian product are maps] (F ¥incin (S ¥PROD T)) ¥imp Is_map(F). Proof: Suppose_not(f0,s0,t0) ==> AUTO Use_def(Is_map) ==> Stat1: not(FORALL p in f0 | p = [car(p),cdr(p)]) p0-->Stat1(*) ==> (p0 in (s0 ¥PROD t0)) & (p0 /= [car(p0),cdr(p0)]) (p0,s0,t0)-->Tcartesian_0(*) ==> false Discharge ==> QED -- \subsection{Digraphs as resulting from graphs} -- -- An ancillary statement: -- Theorem vertexInduced_0: [Loop-freeness gets inherited] (E ¥incin {{x,y}: x in V, y in V-{x}}) ¥imp (E*{{x,y}: x in W, y in W} = E*{{x,y}: x in W, y in W-{x}}). Proof: Suppose_not(e0,v0,w0) ==> Stat1:(e0*{{x,y}: x in w0, y in w0} /= e0*{{x,y}: x in w0, y in w0-{x}}) & (e0 ¥incin {{x,y}: x in v0, y in v0-{x}}) Set_monot ==> {{x,y}: x in w0, y in w0} incs {{x,y}: x in w0, y in w0-{x}} p0-->Stat1(*) ==> Stat2: (p0 in {{x,y}: x in w0, y in w0}) & (p0 in {{x,y}: x in v0, y in v0-{x}}) & (p0 notin {{x,y}: x in w0, y in w0-{x}}) (x0,y0,x1,y1,x0,y0)-->Stat2(Stat2*) ==> false; Discharge ==> QED -- Def orientation: [Orientation of a graph] Orientates(D,V,E) := (E * {{x,y}: x in V, y in (V-{x})}) = {{car(p),cdr(p)}: p in D | p = [car(p), cdr(p)]} -- Theorem orientation0: [Orientation does not take pseudo-edges into account] (W incs V) ¥imp (Orientates(D,V,E) ¥eq Orientates(D,V,E*{{x,y}: x in W, y in W})). Proof: Suppose_not(v1,v0,d0,e0) ==> AUTO Suppose ==> Stat1: (e0 * {{x,y}: x in v0, y in (v0-{x})}) ¥nincin (e0 * {{x,y}: x in v1, y in v1} * {{x,y}: x in v0, y in (v0-{x})}) c-->Stat1(Stat1*) ==> Stat2: (c in {{x,y}: x in v0, y in (v0-{x})}) & (c notin {{x,y}: x in v1, y in v1}) (x0,y0,x0,y0)-->Stat2(*) ==> false Discharge ==> AUTO Use_def(Orientates) ==> ((e0 * {{x,y}: x in v0, y in (v0-{x})}) = {{car(p),cdr(p)}: p in d0 | p = [car(p), cdr(p)]}) ¥neq ((e0 * {{x,y}: x in v1, y in v1} * {{x,y}: x in v0, y in (v0-{x})}) = {{car(p),cdr(p)}: p in d0 | p = [car(p), cdr(p)]}) Discharge ==> QED -- Theorem orientation1: [The void graph is trivially orientable] (V ¥incin {S}) ¥imp Orientates(0,V,E). Proof: Suppose_not(v0,s0,e0) ==> AUTO Use_def(Orientates) ==> Stat1: (e0 * {{x,y}: x in v0, y in (v0-{x})}) /= {{car(p),cdr(p)}: p in 0 | p = [car(p), cdr(p)]} c-->Stat1 ==> Stat2: (c in {{car(p),cdr(p)}: p in 0 | p = [car(p), cdr(p)]}) or (c in {{x,y}: x in v0, y in (v0-{x})}) (p0,x0,y0)-->Stat2 ==> false Discharge ==> QED -- Theorem orientation2: [Oriented arcs are vertex pairs] Orientates(D,V,E) ¥imp Orientates(D*(V ¥PROD V), V, E). Proof: Suppose_not(d0,v0,e0) ==> AUTO Set_monot ==> {{car(p),cdr(p)}: p in d0 | p = [car(p), cdr(p)]} incs {{car(p),cdr(p)}: p in d0 * (v0 ¥PROD v0) | p = [car(p), cdr(p)]} Use_def(Orientates) ==> Stat1: ({{car(p),cdr(p)}: p in d0 | p = [car(p), cdr(p)]} ¥nincin {{car(p),cdr(p)}: p in d0 * (v0 ¥PROD v0) | p = [car(p), cdr(p)]}) & ({{x,y}: x in v0, y in (v0-{x})} incs {{car(p),cdr(p)}: p in d0 | p = [car(p), cdr(p)]}) q0-->Stat1(Stat1*) ==> Stat2: (q0 in {{car(p),cdr(p)}: p in d0 | p = [car(p), cdr(p)]}) & (q0 notin {{car(p),cdr(p)}: p in d0 * (v0 ¥PROD v0) | p = [car(p), cdr(p)]}) Use_def(¥PROD) ==> (v0 ¥PROD v0) = {[x,y]: x in v0, y in v0} (p0,p0)-->Stat2(Stat1*) ==> Stat3: ({car(p0), cdr(p0)} in {{x,y}: x in v0, y in (v0-{x})}) & (p0 notin {[x,y]: x in v0, y in v0}) & (p0 = [car(p0),cdr(p0)]) (x0,y0,car(p0),cdr(p0))-->Stat3(Stat3*) ==> false Discharge ==> QED -- -- -- Theorem orientation3: [Inward orientability of the neighbors af a new vertex] (Orientates(D,V,E) & (W = V+{S}) & (S notin V) & (Dp = D+({S} ¥PROD {x in V | {S,x} in E})) & (D=D*(V ¥PROD V))) ¥imp Orientates(Dp, W, E). Proof: Suppose_not(d0,v0,e2,v1,x0,d1) ==> Stat0: (d1 = d0 + ({x0} ¥PROD {t in v0 | {x0,t} in e2})) & (not Orientates(d1,v1,e2)) & (x0 in v1) & (v0 = v1-{x0}) & Orientates(d0,v0,e2) & (d0 = d0*(v0 ¥PROD v0)) (Stat0*)ELEM ==> Stat2: v1 = v0 + {x0} EQUAL ==> not Orientates(d0+({x0} ¥PROD {t in v0 | {x0,t} in e2}),v1,e2) Use_def(Orientates) ==> Stat3: ((e2 * {{x,y}: x in v1, y in (v1-{x})}) /= {{car(p),cdr(p)}: p in (d0+({x0} ¥PROD {t in v0 | {x0,t} in e2})) | p = [car(p), cdr(p)]}) & ((e2 * {{x,y}: x in v0, y in (v0-{x})}) = {{car(p),cdr(p)}: p in d0 | p = [car(p), cdr(p)]}) Set_monot(Stat3) ==> ({{car(p),cdr(p)}: p in d0 | p = [car(p), cdr(p)]} ¥incin {{car(p),cdr(p)}: p in (d0+({x0} ¥PROD {t in v0 | {x0,t} in e2})) | p = [car(p), cdr(p)]}) Suppose ==> ({{x,y}: x in v1, y in (v1-{x})} ¥nincs {{x,y}: x in v0, y in (v0-{x})}) EQUAL ==> Stat4: ({{x,y}: x in v1, y in (v1-{x})} ¥nincs {{x,y}: x in v1-{x0}, y in (v1-{x0}-{x})}) q2-->Stat4(Stat4*) ==> Stat5: (q2 in {{x,y}: x in v1-{x0}, y in (v1-{x0}-{x})}) & (q2 notin {{x,y}: x in v1, y in (v1-{x})}) (x3,y3,x3,y3)-->Stat5(Stat5*) ==> false (Stat5*)Discharge ==> AUTO q1-->Stat3(Stat3*) ==> Stat6: (q1 notin {{car(p),cdr(p)}: p in d0 | p = [car(p), cdr(p)]}) & (q1 notin (e2 * {{x,y}: x in v0, y in (v0-{x})})) & ((q1 in (e2 * {{x,y}: x in v1, y in (v1-{x})})) ¥neq (q1 in {{car(p),cdr(p)}: p in (d0+({x0} ¥PROD {t in v0 | {x0,t} in e2})) | p = [car(p), cdr(p)]})) Suppose ==> Stat7: q1 in {{car(p),cdr(p)}: p in (d0+({x0} ¥PROD {t in v0 | {x0,t} in e2})) | p = [car(p),cdr(p)]} p1-->Stat7(Stat6*) ==> Stat8: ({car(p1),cdr(p1)} notin {{car(p),cdr(p)}: p in d0 | p = [car(p), cdr(p)]}) & (p1 in (d0+({x0} ¥PROD {t in v0 | {x0,t} in e2}))) & (p1 = [car(p1), cdr(p1)]) & (q1 = {car(p1),cdr(p1)}) p1-->Stat8(Stat8*) ==> p1 in ({x0} ¥PROD {t in v0 | {x0,t} in e2}) (p1,{x0},{t in v0 | {x0,t} in e2})-->Tcartesian_0(Stat8*) ==> Stat9: (cdr(p1) in {t in v0 | {x0,t} in e2}) & (car(p1) = x0) ()-->Stat9(Stat6*) ==> Stat10: ({x0,cdr(p1)} notin {{x,y}: x in v1, y in (v1-{x})}) & (cdr(p1) in v0) & ({x0,cdr(p1)} in e2) (x0,cdr(p1))-->Stat10(Stat10,Stat0*) ==> false (Stat10*)Discharge ==> Stat11: (q1 in {{x,y}: x in v1, y in (v1-{x})}) & (q1 notin {{x,y}: x in v0, y in (v0-{x})}) & Stat11a: (q1 notin {{car(p),cdr(p)}: p in (d0+({x0} ¥PROD {t in v0 | {x0,t} in e2})) | p = [car(p), cdr(p)]}) & (q1 in e2) (x4,y4,x4,y4,[x4,y4])-->Stat11(Stat11,Stat2*) ==> Stat12: ([x4,y4] notin ({x0} ¥PROD {t in v0 | {x0,t} in e2})) & (q1 = {x4,y4}) & (x4 /= y4) & (x0 in q1) & (x4 in v1) & (y4 in v1) & (v1 = v0 + {x0}) & (q1 in e2) Suppose ==> x4 = x0 ([x4,y4],{x0},{t in v0 | {x0,t} in e2})-->Tcartesian_0(Stat12*) ==> Stat13: y4 notin {t in v0 | {x0,t} in e2} y4-->Stat13(Stat12*) ==> false (Stat13*)Discharge ==> AUTO [y4,x4]-->Stat11a(Stat12*) ==> [y4,x4] notin ({x0} ¥PROD {t in v0 | {x0,t} in e2}) ([y4,x4],{x0},{t in v0 | {x0,t} in e2})-->Tcartesian_0(Stat12*) ==> Stat14: x4 notin {t in v0 | {x0,t} in e2} x4-->Stat14(Stat12*) ==> false (Stat14*)Discharge ==> QED -- -- -- Theorem orientation4: [Addition of an isolated node to an orientation] (Orientates(D,V,E) & (W = V+{S}) & ({x in V | {S,x} in E} = 0) & (D=D*(V ¥PROD V))) ¥imp Orientates(D, W, E). Proof: Suppose_not(d0,v0,e0,w0,s0) ==> AUTO Suppose ==> w0 = v0 EQUAL ==> false; Discharge ==> AUTO ({s0})-->Tcartesian_3 ==> (({s0} ¥PROD 0) = 0) & ({x in v0 | {s0,x} in e0} = 0) EQUAL ==> ({s0} ¥PROD {x in v0 | {x,s0} in e0}) = 0 (d0,v0,e0,w0,s0,d0)-->Torientation3(*) ==> false Discharge ==> QED -- -- Theorem orientation5: [Addition of an isolated node to an orientation, 2] (Orientates(D,W,E) & ({x in V | {S,x} in E} = 0) & (W = V+{S}) & (D=D*(V ¥PROD V))) ¥imp (S notin domain(D)). Proof: Suppose_not(d0,w0,e0,v0,s0) ==> AUTO Use_def(domain) ==> Stat1: s0 in {car(p): p in d0} p0-->Stat1(*) ==> Stat2: (cdr(p0) notin {x in v0 | {s0,x} in e0}) & (p0 in d0) & (car(p0) = s0) & (p0 in (v0 ¥PROD v0)) (p0,v0,v0)-->Tcartesian_0(Stat2*) ==> (p0=[car(p0),cdr(p0)]) & (cdr(p0) in v0) (cdr(p0))-->Stat2(Stat2*) ==> {car(p0), cdr(p0)} notin e0 Use_def(Orientates) ==> Stat3: {car(p0), cdr(p0)} notin {{car(p),cdr(p)}: p in d0 | p = [car(p), cdr(p)]} p0-->Stat3(Stat2*) ==> false Discharge ==> QED -- -- Theorem orientation6: [Undirected edges result from oriented arcs, each arc consisting of edges] (Orientates(D,V,E) & ([X,Y] in D)) ¥imp (({X,Y} in E) & ({X,Y} ¥incin V)). Proof: Suppose_not(d0,v0,e0,x0,y0) ==> AUTO Suppose ==> Stat1: {x0,y0} notin {{car(p),cdr(p)}: p in d0 | p = [car(p), cdr(p)]} ([x0,y0])-->Stat1(*) ==> false; Discharge ==> AUTO Use_def(Orientates) ==> Stat2: ({x0,y0} in {{x,y}: x in v0, y in (v0-{x})}) & ({x0,y0} in e0) (x1,y1)-->Stat2(*) ==> false Discharge ==> QED -- -- Theorem orientation7: [An undirected edge calls for an oriented arc] (Orientates(D,V,E) & (X in V) & (Y in V-{X}) & ([X,Y] notin D) & ([Y,X] notin D)) ¥imp ({X,Y} notin E). Proof: Suppose_not(d0,v0,e0,x0,y0) ==> AUTO Suppose ==> Stat1: {x0,y0} notin {{x,y}: x in v0, y in (v0-{x})} (x0,y0)-->Stat1(*) ==> false; Discharge ==> AUTO Use_def(Orientates) ==> Stat2: ({x0,y0} in {{car(p),cdr(p)}: p in d0 | p = [car(p), cdr(p)]}) p0-->Stat2(Stat2*) ==> Stat3: ({car(p0),cdr(p0)} = {x0,y0}) & ([car(p0),cdr(p0)] in d0) Suppose ==> (x0 = car(p0)) & (y0 = cdr(p0)) EQUAL ==> false Discharge ==> AUTO (Stat3*)ELEM ==> (y0 = car(p0)) & (x0 = cdr(p0)) EQUAL ==> false Discharge ==> QED -- -- Theorem orientation8: [No self-loops in a digraph resulting from orientating a graph] Orientates(D,V,E) ¥imp ([U,U] notin D). Proof: Suppose_not(d0,v0,e0,x0) ==> AUTO Use_def(Orientates) ==> Stat0: ({{x,y}: x in v0, y in (v0-{x})} incs {{car(p),cdr(p)}: p in d0 | p = [car(p), cdr(p)]}) & ([x0,x0] in d0) Suppose ==> Stat1: {x0,x0} notin {{car(p),cdr(p)}: p in d0 | p = [car(p), cdr(p)]} [x0,x0]-->Stat1(Stat0*) ==> false; Discharge ==> Stat2: {x0,x0} in {{x,y}: x in v0, y in (v0-{x})} (x1,y1)-->Stat2(Stat2*) ==> false Discharge ==> QED -- -- -- -- \subsection{Weak extensionality, extensionality, and acyclicity} -- Def extensionality_0: [Extensionality] Extensional(V,D) := (FORALL x in V, y in V | (EXISTS z | (([x,z] in D) ¥eq ([y,z] in D)) ¥imp (x = y))) -- Def extensionality_1: [Weak extensionality] WExtensional(V,D) := Extensional(V*domain(D*(V ¥PROD V)),D*(V ¥PROD V)) -- -- Theorem weaXtensionality0: [Weak extensionality has only to do with vertices] WExtensional(V,D) ¥eq WExtensional(V,D*(V ¥PROD V)). Proof: Suppose_not(v0,d0) ==> AUTO Use_def(WExtensional) ==> Extensional(v0*domain(d0*(v0 ¥PROD v0)*(v0 ¥PROD v0)),d0*(v0 ¥PROD v0)*(v0 ¥PROD v0)) ¥neq Extensional(v0*domain(d0*(v0 ¥PROD v0)),d0*(v0 ¥PROD v0)) TELEM ==> d0*(v0 ¥PROD v0)*(v0 ¥PROD v0) = d0*(v0 ¥PROD v0) EQUAL ==> false Discharge ==> QED -- Theorem weaXtensionality1: [Addition of an isolated vertex preserves weak extensionality] (WExtensional(V,D) & (S notin domain(D)) & (W = V+{S}) & (D=D*(V ¥PROD V))) ¥imp WExtensional(W,D). Proof: Suppose_not(v0,d0,s0,w0) ==> Stat0: WExtensional(v0,d0) & (s0 notin domain(d0)) & (w0 = v0+{s0}) & (d0=d0*(v0 ¥PROD v0)) & (not WExtensional(w0,d0)) Use_def(WExtensional) ==> Extensional(v0*domain(d0*(v0 ¥PROD v0)),d0*(v0 ¥PROD v0)) & (not Extensional(w0*domain(d0*(w0 ¥PROD w0)),d0*(w0 ¥PROD w0))) Use_def(Extensional) ==> Stat1: (not(FORALL x in w0*domain(d0*(w0 ¥PROD w0)), y in w0*domain(d0*(w0 ¥PROD w0)) | (EXISTS z | (([x,z] in d0*(w0 ¥PROD w0)) ¥eq ([y,z] in d0*(w0 ¥PROD w0))) ¥imp (x = y)))) & (FORALL x in v0*domain(d0*(v0 ¥PROD v0)), y in v0*domain(d0*(v0 ¥PROD v0)) | (EXISTS z | (([x,z] in d0*(v0 ¥PROD v0)) ¥eq ([y,z] in d0*(v0 ¥PROD v0))) ¥imp (x = y))) (x0,y0,x0,y0)-->Stat1(Stat1*) ==> Stat2: (not(EXISTS z | (([x0,z] in d0*(w0 ¥PROD w0)) ¥eq ([y0,z] in d0*(w0 ¥PROD w0))) ¥imp (x0 = y0))) & (x0 in w0*domain(d0*(w0 ¥PROD w0))) & (y0 in w0*domain(d0*(w0 ¥PROD w0))) & (not((x0 in v0*domain(d0*(v0 ¥PROD v0))) & (y0 in v0*domain(d0*(v0 ¥PROD v0))) & (not(EXISTS z | (([x0,z] in d0*(v0 ¥PROD v0)) ¥eq ([y0,z] in d0*(v0 ¥PROD v0))) ¥imp (x0 = y0))))) Suppose ==> Stat3: d0*(v0 ¥PROD v0) /= d0*(w0 ¥PROD w0) c-->Stat3(Stat3,Stat0*) ==> (c in d0) & (c in (v0 ¥PROD v0)) & (c notin (w0 ¥PROD w0)) Set_monot ==> {[x,y]: x in v0, y in v0} ¥incin {[x,y]: x in w0, y in w0} Use_def(¥PROD)(Stat3) ==> false Discharge ==> d0*(v0 ¥PROD v0) = d0*(w0 ¥PROD w0) EQUAL ==> domain(d0*(v0 ¥PROD v0)) = domain(d0*(w0 ¥PROD w0)) Suppose ==> w0*domain(d0*(w0 ¥PROD w0)) /= v0*domain(d0*(v0 ¥PROD v0)) EQUAL ==> Stat4: w0*domain(d0) /= v0*domain(d0) (v0 ¥PROD v0, d0, v0 ¥PROD v0)-->Tdomain_1(Stat0*) ==> domain(d0) ¥incin domain(v0 ¥PROD v0) Use_def(domain(v0 ¥PROD v0)) ==> AUTO d-->Stat4(Stat0*) ==> Stat5: (d in {car(p): p in (v0 ¥PROD v0)}) & (d notin v0) p0-->Stat5(Stat5*) ==> (d = car(p0)) & (p0 in (v0 ¥PROD v0)) (p0,v0,v0)-->Tcartesian_0(Stat5*) ==> false Discharge ==> AUTO (Stat0*)ELEM ==> Stat8: (EXISTS z | (([x0,z] in d0*(v0 ¥PROD v0)) ¥eq ([y0,z] in d0*(v0 ¥PROD v0))) ¥imp (x0 = y0)) z0-->Stat8(Stat8*) ==> (([x0,z0] in d0*(v0 ¥PROD v0)) ¥eq ([y0,z0] in d0*(v0 ¥PROD v0))) ¥imp (x0 = y0) z0-->Stat2(Stat2*) ==> false Discharge ==> QED -- -- Theorem weaXtensionality2: [A new vertex whose out-neighborhood comprises what was, previously, a source does not disrupt weak extensionality] (WExtensional(V,D) & (Dp=D+({S} ¥PROD Vp)) & (Vp ¥nincin range(D)) & (D=D*(V ¥PROD V)) & (W incs V+Vp)) ¥imp WExtensional(W,Dp). Proof: Suppose_not(v0,d0,d1,s0,v1,w0) ==> AUTO -- -- Suppose $v0,d0,d1,s0,v1,w0$ form a counterexample to the claim so that, among others, -- $v0*domain(d0),d0$ is extensional whereas $w0*domain(d1*(w0 ¥PROD w0)),d1*(w0 ¥PROD w0)$ -- is not. -- Use_def(WExtensional) ==> Extensional(v0*domain(d0*(v0 ¥PROD v0)),d0*(v0 ¥PROD v0)) & (not Extensional(w0*domain(d1*(w0 ¥PROD w0)),d1*(w0 ¥PROD w0))) EQUAL ==> Extensional(v0*domain(d0),d0) Use_def(Extensional) ==> Stat1: (not(FORALL x in w0*domain(d1*(w0 ¥PROD w0)), y in w0*domain(d1*(w0 ¥PROD w0)) | (EXISTS z | (([x,z] in (d1*(w0 ¥PROD w0))) ¥eq ([y,z] in (d1*(w0 ¥PROD w0)))) ¥imp (x = y)))) & (FORALL x in v0*domain(d0), y in v0*domain(d0) | (EXISTS z | (([x,z] in d0) ¥eq ([y,z] in d0)) ¥imp (x = y))) -- -- Consequently, there must exist $x0,y0$ in $w0*domain(d1*(w0 ¥PROD w0))$ which $d1*(w0 ¥PROD w0)$ does -- not differentiate; but which $d0$ differentiates if they belong to $domain(d0)$. -- (v0 ¥PROD v0,d0,v0 ¥PROD v0)-->Tdomain_1(*) ==> domain(d0) ¥incin domain(v0 ¥PROD v0) v0-->Tcartesian_4(Stat1*) ==> v0 = domain(v0 ¥PROD v0) (x0,y0,x0,y0)-->Stat1(Stat1*) ==> Stat2: (not(EXISTS z | (([x0,z] in (d1*(w0 ¥PROD w0))) ¥eq ([y0,z] in (d1*(w0 ¥PROD w0)))) ¥imp (x0 = y0))) & (((x0 in domain(d0)) & (y0 in domain(d0))) ¥imp (EXISTS z | (([x0,z] in d0) ¥eq ([y0,z] in d0)) ¥imp (x0 = y0))) & (x0 in w0*domain(d1*(w0 ¥PROD w0))) & (y0 in w0*domain(d1*(w0 ¥PROD w0))) -- -- Plainly, $x0 /= y0$ must hold. -- (v0,w0,v0,w0)-->Tcartesian_5(*) ==> Stat2a: ((v0 ¥PROD v0) ¥incin (w0 ¥PROD w0)) & (d0 ¥incin d1) Suppose ==> x0 = y0 0-->Stat2(Stat2*) ==> false; Discharge ==> Stat3: ((v1-range(d0)) /= 0) & (x0 /= y0) -- -- Let $z0$ be a source of $d0$ which does not belong to $v1$. -- Use_def(range(d0)) ==> AUTO z0-->Stat3(Stat3*) ==> Stat4: (z0 notin {cdr(p): p in d0}) & (z0 in v1) -- -- Observe that $domain(d0) ¥incin domain(d1*(w0 ¥PROD w0))$ and -- $domain(d1*(w0 ¥PROD w0)) ¥incin (domain(d0) + {s0})$, -- where $s0$ is the new vertex. -- (d1*(w0 ¥PROD w0),d0,d1*(w0 ¥PROD w0))-->Tdomain_1(*) ==> Stat4a: domain(d0) ¥incin domain(d1*(w0 ¥PROD w0)) Suppose ==> domain(d1*(w0 ¥PROD w0)) ¥nincin (domain(d0) + {s0}) (v1,{s0})-->Tcartesian_2(*) ==> domain({s0} ¥PROD v1) = {s0} (d1,d0,{s0} ¥PROD v1)-->Tdomain_1(*) ==> domain(d1) = domain(d0) + {s0} (d1,d1*(w0 ¥PROD w0),d1)-->Tdomain_1(Stat2*) ==> false Discharge ==> AUTO -- -- Also notice that ${[x0,z0],[y0,z0]} ¥incin (w0 ¥PROD w0)$. -- Suppose ==> ([x0,z0] notin (w0 ¥PROD w0)) or ([y0,z0] notin (w0 ¥PROD w0)) Use_def(¥PROD) ==> Stat5: ([x0,z0] notin {[x,y]: x in w0, y in w0}) or ([y0,z0] notin {[x,y]: x in w0, y in w0}) (x0,z0,y0,z0)-->Stat5(Stat4,Stat4*) ==> not((x0 in w0) & (y0 in w0) & (z0 in w0)) Discharge ==> AUTO -- -- We can exclude that $s0 in {x0,y0}$, through the following argument: -- Suppose ==> Stat6: (x0 = s0) or (y0 = s0) -- -- Let $t0$ be the one, of $x0,y0$ which differs from $s0$, -- so that $[t0,z0] notin d0$ (because $z0$ is a source of $d0$). -- Loc_def ==> Stat7: t0 = arb({x0,y0}-{s0}) [t0,z0]-->Stat4(Stat4,Stat4*) ==> Stat9: [t0,z0] notin d0 -- -- On the contrary, $[s0,z0] in d0$ because we have drawn $z0$ from $v1$. -- It hence follows easily that $[t0,z0] notin d1$ and $[s0,z0] in d1$. -- Suppose ==> [s0,z0] notin d1 EQUAL ==> Stat10: [s0,z0] notin d0+({s0} ¥PROD v1) ([s0,z0],{s0},v1)-->Tcartesian_0(Stat10,Stat4) ==> false Discharge ==> AUTO (Stat3,Stat6,Stat7)ELEM ==> Stat11: {x0,y0} = {s0,t0} Suppose ==> [t0,z0] in d1 EQUAL ==> Stat12: [t0,z0] in d0+({s0} ¥PROD v1) ([t0,z0],{s0},v1)-->Tcartesian_0(Stat9,Stat12) ==> t0 = s0 (Stat3*)Discharge ==> AUTO -- -- If $x0 = s0$, we have $[y0,z0] notin d1$ and $[x0,z0] in d1$, -- contradicting the fact that they $x0,y0$ are not differentiated by $d1$ -- Suppose ==> (x0 = s0) & (y0 = t0) EQUAL(Stat6) ==> ([x0,z0] in d1) & ([y0,z0] notin d1) z0-->Stat2(Stat4a*) ==> false Discharge ==> AUTO -- -- It is likewise untenable that $y0 = s0$. -- (Stat11*)ELEM ==> (y0 = s0) & (x0 = t0) EQUAL(Stat6) ==> ([y0,z0] in d1) & ([x0,z0] notin d1) z0-->Stat2(Stat4a*) ==> false Discharge ==> AUTO -- -- But then both $x0$ and $y0$ belong to $domain(v0)$ and hence $d0$ -- differentiates them; i.e., there is a $z1$ such that either one of the -- conditions $[x0,z1] in d0$, $[y0,z1] in d0$, but not both, are met. -- (Stat2*)ELEM ==> Stat16: (EXISTS z | (([x0,z] in d0) ¥eq ([y0,z] in d0)) ¥imp (x0 = y0)) z1-->Stat16(Stat16,Stat3*) ==> ([x0,z1] in d0) ¥neq ([y0,z1] in d0) -- -- Our proof by contradiction is then completed by excluding either possibility -- through the following argument. -- EQUAL ==> Stat17: (d0 = d0*(v0 ¥PROD v0)) & (d1 = d0+({s0} ¥PROD v1)) Suppose ==> Stat18: ([x0,z1] in d0*(v0 ¥PROD v0)) & ([y0,z1] notin d0) z1-->Stat2(Stat18,Stat2a*) ==> Stat19: ([y0,z1] in d1) & ([y0,z1] notin d0) EQUAL(Stat17) ==> Stat20: [y0,z1] in d0+({s0} ¥PROD v1) ([y0,z1],{s0},v1)-->Tcartesian_0(Stat19,Stat20*) ==> y0 = s0 (Stat4*)Discharge ==> AUTO (Stat16*)ELEM ==> Stat21: ([y0,z1] in d0*(v0 ¥PROD v0)) & ([x0,z1] notin d0) z1-->Stat2(Stat21,Stat2a*) ==> [x0,z1] in d1 EQUAL(Stat17) ==> Stat22: [x0,z1] in d0+({s0} ¥PROD v1) ([x0,z1],{s0},v1)-->Tcartesian_0(Stat21,Stat22*) ==> x0 = s0 (Stat4*)Discharge ==> QED -- Theorem extensionality0: [Extensional digraphs are weakly extensional] (Extensional(V,D) & ((V ¥PROD V) incs D)) ¥imp WExtensional(V,D). Proof: Suppose_not(v0,d0) ==> AUTO Use_def(WExtensional) ==> not Extensional(v0*domain(d0*(v0 ¥PROD v0)),d0*(v0 ¥PROD v0)) ELEM ==> d0*(v0 ¥PROD v0) = d0 EQUAL ==> Stat1: Extensional(v0,d0) & (not Extensional(v0*domain(d0),d0)) Use_def(Extensional)(Stat1) ==> Stat2: (not(FORALL x in v0*domain(d0), y in v0*domain(d0) | (EXISTS z | (([x,z] in d0) ¥eq ([y,z] in d0)) ¥imp (x = y)))) & (FORALL x in v0, y in v0 | (EXISTS z | (([x,z] in d0) ¥eq ([y,z] in d0)) ¥imp (x = y))) (x0,y0,x0,y0)-->Stat2(Stat2*) ==> false Discharge ==> QED -- Theorem extensionality1: [Making a new vertex the son of a set of vertices comprising a sink cannot disrupt extensionality] (((V ¥PROD V) incs D) & (X notin V) & (V incs S) & (EXISTS t in S | (D ¥ON {t}) = 0) & Extensional(V,D)) ¥imp Extensional(V+{X},D+(S ¥PROD {X})). Proof: Suppose_not(v0,d0,x0,s0) ==> AUTO Use_def(Extensional) ==> Stat1: (not(FORALL x in (v0+{x0}), y in (v0+{x0}) | (EXISTS z | (([x,z] in (d0+(s0 ¥PROD {x0}))) ¥eq ([y,z] in (d0+(s0 ¥PROD {x0})))) ¥imp (x = y)))) & Stat1a: (FORALL x in v0, y in v0 | (EXISTS z | (([x,z] in d0) ¥eq ([y,z] in d0)) ¥imp (x = y))) (u0,w0,u0,w0)-->Stat1(Stat1*) ==> Stat2: (not (EXISTS z | (([u0,z] in (d0+(s0 ¥PROD {x0}))) ¥eq ([w0,z] in (d0+(s0 ¥PROD {x0})))) ¥imp (u0 = w0))) & (u0 in (v0+{x0})) & (w0 in (v0+{x0})) & (((u0 in v0) & (w0 in v0)) ¥imp (EXISTS z | (([u0,z] in d0) ¥eq ([w0,z] in d0)) ¥imp (u0 = w0))) ELEM ==> Stat3: (EXISTS t in s0 | (d0 ¥ON {t}) = 0) & ((v0 ¥PROD v0) incs d0) & (x0 notin v0) & (v0 incs s0) Suppose ==> (u0 in v0) & (w0 in v0) (Stat2*)ELEM ==> Stat4: (EXISTS z | (([u0,z] in d0) ¥eq ([w0,z] in d0)) ¥imp (u0 = w0)) z0-->Stat4 ==> AUTO z0-->Stat2(Stat4*) ==> Stat5: (([u0,z0] in d0) ¥neq ([w0,z0] in d0)) & (([u0,z0] in (d0+(s0 ¥PROD {x0}))) ¥eq ([w0,z0] in (d0+(s0 ¥PROD {x0})))) Suppose ==> z0 notin v0 ([u0,z0],v0,v0)-->Tcartesian_0(Stat3*) ==> [u0,z0] notin d0 ([w0,z0],v0,v0)-->Tcartesian_0(Stat3*) ==> [w0,z0] notin d0 (Stat4*)Discharge ==> AUTO Suppose ==> [u0,z0] in d0 ([w0,z0],s0,{x0})-->Tcartesian_0(Stat5*) ==> z0 = x0 (Stat3*)Discharge ==> AUTO ([u0,z0],s0,{x0})-->Tcartesian_0(Stat5*) ==> z0 = x0 (Stat3*)Discharge ==> AUTO Suppose ==> Stat6: (EXISTS z | [x0,z] in (d0+(s0 ¥PROD {x0}))) z1-->Stat6(Stat6*) ==> ([x0,z1] in (d0+(s0 ¥PROD {x0}))) ([x0,z1],v0,v0)-->Tcartesian_0(Stat3*) ==> [x0,z1] in (s0 ¥PROD {x0}) ([x0,z1],s0,{x0})-->Tcartesian_0(Stat3*) ==> false Discharge ==> Stat7: not (EXISTS z | [x0,z] in (d0+(s0 ¥PROD {x0}))) t0-->Stat3(Stat3,Stat3*) ==> (t0 in s0) & ((d0 ¥ON {t0}) = 0) Suppose ==> Stat8: (EXISTS z | [t0,z] in d0) z2-->Stat8(Stat8*) ==> [t0,z2] in d0 ([t0,z2],t0,z2,d0,t0)-->Trestr_2(Stat7*) ==> false Discharge ==> Stat9: not (EXISTS z | [t0,z] in d0) ([t0,x0],s0,{x0})-->Tcartesian_0(Stat7*) ==> [t0,x0] in (s0 ¥PROD {x0}) 0-->Stat2(Stat2,Stat2*) ==> Stat10: u0 /= w0 Suppose ==> (u0 in v0) & (w0 = x0) Suppose ==> Stat11: (EXISTS z | [u0,z] in d0) z3-->Stat11(Stat11*) ==> [u0,z3] in (d0+(s0 ¥PROD {x0})) z3-->Stat2(Stat10*) ==> [w0,z3] in (d0+(s0 ¥PROD {x0})) z3-->Stat7(Stat10) ==> false Discharge ==> Stat12: not(EXISTS z | [u0,z] in d0) Suppose ==> t0 /= u0 (t0,u0)-->Stat1a(Stat3*) ==> Stat13: (EXISTS z | (([t0,z] in d0) ¥eq ([u0,z] in d0)) ¥imp (t0 = u0)) z4-->Stat13 ==> AUTO z4-->Stat9 ==> AUTO z4-->Stat12(Stat12*) ==> false Discharge ==> AUTO x0-->Stat2(Stat10,Stat10*) ==> ([u0,x0] in (d0+(s0 ¥PROD {x0}))) ¥eq ([w0,x0] in (d0+(s0 ¥PROD {x0}))) EQUAL(Stat10) ==> Stat14: ([t0,x0] in (d0+(s0 ¥PROD {x0}))) ¥eq ([x0,x0] in (d0+(s0 ¥PROD {x0}))) ([x0,x0],v0,v0)-->Tcartesian_0(Stat3*) ==> [x0,x0] in (s0 ¥PROD {x0}) ([x0,x0],s0,{x0})-->Tcartesian_0(Stat3*) ==> false Discharge ==> AUTO (Stat2*)ELEM ==> (w0 in v0) & (u0 = x0) Suppose ==> Stat15: (EXISTS z | [w0,z] in d0) z5-->Stat15(Stat15*) ==> [w0,z5] in (d0+(s0 ¥PROD {x0})) z5-->Stat2(Stat10*) ==> [u0,z5] in (d0+(s0 ¥PROD {x0})) z5-->Stat7(Stat10) ==> false Discharge ==> Stat16: not(EXISTS z | [w0,z] in d0) Suppose ==> t0 /= w0 (t0,w0)-->Stat1a(Stat3*) ==> Stat17: (EXISTS z | (([t0,z] in d0) ¥eq ([w0,z] in d0)) ¥imp (t0 = w0)) z6-->Stat17 ==> AUTO z6-->Stat9 ==> AUTO z6-->Stat16(Stat16*) ==> false Discharge ==> AUTO x0-->Stat2(Stat10,Stat10*) ==> ([u0,x0] in (d0+(s0 ¥PROD {x0}))) ¥eq ([w0,x0] in (d0+(s0 ¥PROD {x0}))) EQUAL(Stat10) ==> Stat18: ([x0,x0] in (d0+(s0 ¥PROD {x0}))) ¥eq ([w0,x0] in (d0+(s0 ¥PROD {x0}))) (Stat3)ELEM ==> [x0,x0] in (d0+(s0 ¥PROD {x0})) ([x0,x0],v0,v0)-->Tcartesian_0(Stat3*) ==> [x0,x0] in (s0 ¥PROD {x0}) ([x0,x0],s0,{x0})-->Tcartesian_0(Stat3*) ==> false Discharge ==> QED -- Theorem extensionality2: [An extensional digraph has at most one sink] (Extensional(V,D) & (X in V) & (Y in V) & (FORALL z | [X,z] notin D) & (FORALL z | [Y,z] notin D)) ¥imp (X = Y). Proof: Suppose_not(v0,d0,x0,y0) ==> AUTO Use_def(Extensional) ==> Stat1: (FORALL x in v0, y in v0 | (EXISTS z | (([x,z] in d0) ¥eq ([y,z] in d0)) ¥imp (x = y))) (x0,y0)-->Stat1(*) ==> Stat2: (EXISTS z | (([x0,z] in d0) ¥eq ([y0,z] in d0)) ¥imp (x0 = y0)) z0-->Stat2(*) ==> ([x0,z0] in d0) or ([y0,z0] in d0) ELEM ==> Stat3: (FORALL z | [x0,z] notin d0) & (FORALL z | [y0,z] notin d0) (z0,z0)-->Stat3(*) ==> false Discharge ==> QED -- -- -- -- We can characterize acyclicity as well-foundedness, in view of the finiteness of the graphs on which we are focusing: -- a set of nodes which has no sinks, in fact, is not necessarily a cycle, but it contains one. -- Def acyclicity: [Acyclicity] Acyclic(V,D) := (FORALL w ¥incin V | (w /= 0) ¥imp (EXISTS t in w | 0 = {y in w | [t,y] in D})) -- Theorem acyclicity0: [Adjunction of an outer vertex to a digraph cannot disrupt acyclicity] (((V ¥PROD V) incs D) & (X notin V) & (V incs S) & Acyclic(V,D)) ¥imp Acyclic(V+{X},D+({X} ¥PROD S)). Proof: Suppose_not(v0,d0,x0,s0) ==> AUTO Use_def(Acyclic) ==> Stat1: not(FORALL w ¥incin (v0+{x0}) | (w /= 0) ¥imp (EXISTS t in w | 0 = {y in w | [t,y] in (d0+({x0} ¥PROD s0))})) & Stat2: (FORALL w ¥incin v0 | (w /= 0) ¥imp (EXISTS t in w | 0 = {y in w | [t,y] in d0})) w0-->Stat1(*) ==> Stat3: (not(EXISTS t in w0 | 0 = {y in w0 | [t,y] in (d0+({x0} ¥PROD s0))})) & (w0 ¥incin (v0+{x0})) & (w0 /= 0) & (x0 notin v0) & ((v0 ¥PROD v0) incs d0) w0-->Stat2 ==> ((w0 ¥incin v0) ¥imp (EXISTS t in w0 | 0 = {y in w0 | [t,y] in d0})) Suppose ==> Stat4: (EXISTS t in w0 | 0 = {y in w0 | [t,y] in d0}) & (w0 ¥incin v0) t0-->Stat4 ==> Stat5: ({y in w0 | [t0,y] in d0} = 0) & (t0 in w0) t0-->Stat3 ==> Stat6: {y in w0 | [t0,y] in (d0+({x0} ¥PROD s0))} /= 0 y0-->Stat6 ==> (y0 in w0) & ([t0,y0] in (d0+({x0} ¥PROD s0))) y0-->Stat5 ==> Stat7: [t0,y0] in ({x0} ¥PROD s0) ([t0,y0],{x0},s0)-->Tcartesian_0(Stat7) ==> t0 = x0 Discharge ==> x0 in w0 x0-->Stat3(Stat3*) ==> Stat9: {y in w0 | [x0,y] in (d0+({x0} ¥PROD s0))} /= 0 y2-->Stat9 ==> Stat10: (y2 in w0) & ([x0,y2] in (d0+({x0} ¥PROD s0))) ([x0,y2],v0,v0)-->Tcartesian_0(Stat11,Stat3) ==> Stat11: [x0,y2] notin (v0 ¥PROD v0) ([x0,y2],{x0},s0)-->Tcartesian_0(Stat3,Stat10,Stat11) ==> y2 in s0 ELEM ==> y2 in w0-{x0} (w0-{x0})-->Stat2 ==> Stat13: (EXISTS t in (w0-{x0}) | 0 = {y in (w0-{x0}) | [t,y] in d0}) t1-->Stat13 ==> Stat14: ({y in (w0-{x0}) | [t1,y] in d0} = 0) & (t1 in (w0-{x0})) t1-->Stat3 ==> Stat15: {y in w0 | [t1,y] in (d0+({x0} ¥PROD s0))} /= 0 y5-->Stat15 ==> (y5 in w0) & ([t1,y5] in (d0+({x0} ¥PROD s0))) Suppose ==> y5 /= x0 y5-->Stat14 ==> Stat16: [t1,y5] in ({x0} ¥PROD s0) ([t1,y5],{x0},s0)-->Tcartesian_0(Stat16) ==> t1 = x0 (Stat14*)Discharge ==> AUTO EQUAL(Stat15) ==> Stat18: [t1,x0] in (d0+({x0} ¥PROD s0)) Suppose ==> Stat19: [t1,x0] in d0 ([t1,x0],v0,v0)-->Tcartesian_0(Stat19,Stat3) ==> false Discharge ==> AUTO ([t1,x0],{x0},s0)-->Tcartesian_0(Stat18) ==> t1 = x0 (Stat14*)Discharge ==> QED -- -- Theorem acyclicity1: [Reduction of the set of edges of a digraph preserves its acyclicity] (Acyclic(V,D) & (Vp ¥incin V) & (Dp ¥incin D)) ¥imp Acyclic(Vp,Dp). Proof: Suppose_not(v0,d0,v1,d1) ==> AUTO Use_def(Acyclic) ==> Stat1: (not (FORALL w ¥incin v1 | (w /= 0) ¥imp (EXISTS t in w | 0 = {y in w | [t,y] in d1}))) & Stat2: (FORALL w ¥incin v0 | (w /= 0) ¥imp (EXISTS t in w | 0 = {y in w | [t,y] in d0})) w0-->Stat1 ==> AUTO w0-->Stat2(*) ==> Stat3: (EXISTS t in w0 | 0 = {y in w0 | [t,y] in d0}) & (not (EXISTS t in w0 | 0 = {y in w0 | [t,y] in d1})) (t0,t0)-->Stat3(*) ==> Stat4: (0 /= {y in w0 | [t0,y] in d1}) & (0 = {y in w0 | [t0,y] in d0}) (y0,y0)-->Stat4(*) ==> false Discharge ==> QED -- -- Theorem acyclicity2: [Acyclic digraphs are devoid of self-loops and of symmetrical arcs] (Acyclic(V,D) & ({Y,X} ¥incin V) & ([X,Y] in D)) ¥imp (([Y,X] notin D) & (X /= Y)). Proof: Suppose_not(v0,d0,y0,x0) ==> AUTO Use_def(Acyclic) ==> Stat1: (FORALL w ¥incin v0 | (w /= 0) ¥imp (EXISTS t in w | 0 = {y in w | [t,y] in d0})) ({y0,x0})-->Stat1 ==> Stat2: (EXISTS t in {y0,x0} | 0 = {y in {y0,x0} | [t,y] in d0}) & ([x0,y0] in d0) t0-->Stat2(Stat2*) ==> Stat3: (0 = {y in {y0,x0} | [t0,y] in d0}) & (t0 in {y0,x0}) y0-->Stat3(Stat2) ==> t0 /= x0 x0-->Stat3(Stat2) ==> [y0,x0] notin d0 Discharge ==> QED -- --PAUSE HERE -- -- Although they deserve some interest of their own, our next two theorems will not be exploited -- in the present scenario: we are including them only as in preparation -- for the subsequent Theorem $acyclicity4$, of which Theorem $acyclicity3$ is -- a down-sized, easier-to-read version. Theorem $acyclicity3a$ is slightly more -- cumbersome than the other two, but it conveys the basic insight, namely: -- the converse of an acyclic graph is acyclic. -- Theorem acyclicity3a: [The converse of any acyclic graph is acyclic] (Acyclic(V,D) & Finite(V)) ¥imp Acyclic(V,{[cdr(p),car(p)]: p in D | p = [car(p),cdr(p)]}). Proof: Suppose_not(v0,d0) ==> AUTO -- -- Arguing by contradiction, suppose that there is a counterexample $w2,v0,d0$ to the claim. -- Then, using finite induction, we can pick a counterexample $w1,v0,d0$ whose $w1$ is minimal. -- Use_def(Acyclic) ==> Stat1: (FORALL w ¥incin v0 | (w /= 0) ¥imp (EXISTS t in w | 0 = {y in w | [t,y] in d0})) & Stat2: (not(FORALL w ¥incin v0 | (w /= 0) ¥imp (EXISTS t in w | 0 = {y in w | [t,y] in {[cdr(p),car(p)]: p in d0 | p = [car(p),cdr(p)]}}))) w2-->Stat2 ==> Stat3: (not(EXISTS t in w2 | 0 = {y in w2 | [t,y] in {[cdr(p),car(p)]: p in d0 | p = [car(p),cdr(p)]}})) & (w2 ¥incin v0) & (w2 /= 0) & Finite(w2) APPLY (fin_thryvar:w1) finiteInduction(s0->w2, P(W)->((W ¥incin v0) & (W/=0) & (not(EXISTS t in W | 0 = {y in W | [t,y] in {[cdr(p),car(p)]: p in d0 | p = [car(p),cdr(p)]}})))) ==> Stat7: (FORALL v | (v ¥incin w1) ¥imp (Finite(v) & (((v ¥incin v0) & (v/=0) & (not(EXISTS t in v | 0 = {y in v | [t,y] in {[cdr(p),car(p)]: p in d0 | p = [car(p),cdr(p)]}}))) ¥eq (v=w1)))) w1-->Stat7(*) ==> Stat8: (not (EXISTS t in w1 | 0 = {y in w1 | [t,y] in {[cdr(p),car(p)]: p in d0 | p = [car(p),cdr(p)]}})) & (w1/=0) & (w1 ¥incin v0) -- -- Now consider a sink $a$ of $w1$. It is easily seen that $w1/={a}$. -- w1-->Stat1 ==> Stat9: (EXISTS t in w1 | 0 = {y in w1 | [t,y] in d0}) a-->Stat9 ==> Stat10: ({y in w1 | [a,y] in d0} = 0) & (a in w1) Suppose ==> w1 = {a} a-->Stat8 ==> Stat11: {y in w1 | [a,y] in {[cdr(p),car(p)]: p in d0 | p = [car(p),cdr(p)]}} /= 0 c-->Stat11 ==> Stat12: [a,a] in {[cdr(p),car(p)]: p in d0 | p = [car(p),cdr(p)]} p0-->Stat12(Stat12) ==> [a,a] in d0 a-->Stat10 ==> AUTO (Stat12*)Discharge ==> AUTO (w1-{a})-->Stat7(*) ==> Stat15: (EXISTS t in (w1-{a}) | 0 = {y in (w1-{a}) | [t,y] in {[cdr(p),car(p)]: p in d0 | p = [car(p),cdr(p)]}}) t0-->Stat15 ==> ({y in (w1-{a}) | [t0,y] in {[cdr(p),car(p)]: p in d0 | p = [car(p),cdr(p)]}} = 0) & (t0 in (w1-{a})) -- -- If $t0$, which is a source of $w1-{a}$, is not a source of $w1$, then $[a,t0]$ must be an edge; -- but this conflicts with the way $a$ has been chosen. -- t0-->Stat8 ==> Stat16: {y in w1 | [t0,y] in {[cdr(p),car(p)]: p in d0 | p = [car(p),cdr(p)]}} /= 0 b-->Stat16 ==> Stat17: (b notin {y in (w1-{a}) | [t0,y] in {[cdr(p),car(p)]: p in d0 | p = [car(p),cdr(p)]}}) & ([t0,b] in {[cdr(p),car(p)]: p in d0 | p = [car(p),cdr(p)]}) & (b in w1) b-->Stat17 ==> Stat18: [t0,a] in {[cdr(p),car(p)]: p in d0 | p = [car(p),cdr(p)]} p1-->Stat18(Stat18) ==> [a,t0] in d0 t0-->Stat10(Stat10*) ==> false Discharge ==> QED -- -- The following theorem states that every non-null set $W$ of vertices in an acyclic digraph -- $V, D$ has at least one source; that is, it has a vertex s whose in-neighborhood does not -- intersect $W$. Although it deserves some interest of its own, this theorem will not be -- exploited in the present scenario: we are including it only as a down-sized, easier-to-read -- version of the subsequent Theorem $acyclicity4$. -- Theorem acyclicity3: [Local sources exist in any acyclic graph] ((W /= 0) & Acyclic(V,D) & Finite(V) & (V incs W)) ¥imp (EXISTS t in W | 0 = {y in W | [y,t] in D}). Proof: Suppose_not(w2,v0,d0) ==> AUTO -- -- Arguing by contradiction, suppose that there is a counterexample $w2,v0,d0$ to the claim. -- Then, using finite induction, we can pick a counterexample $w1,v0,d0$ whose $w1$ is minimal. -- Use_def(Acyclic) ==> Stat1: (FORALL w ¥incin v0 | (w /= 0) ¥imp (EXISTS t in w | 0 = {y in w | [t,y] in d0})) & Finite(w2) -- -- APPLY (fin_thryvar:w1) finiteInduction(s0->w2, P(W)->((W ¥incin v0) & (W/=0) & (not (EXISTS t in W | 0 = {y in W | [y,t] in d0})))) ==> Stat7: (FORALL v | (v ¥incin w1) ¥imp (Finite(v) & (((v ¥incin v0) & (v/=0) & (not (EXISTS t in v | 0 = {y in v | [y,t] in d0}))) ¥eq (v=w1)))) w1-->Stat7(Stat7*) ==> Stat8: (not (EXISTS t in w1 | 0 = {y in w1 | [y,t] in d0})) & (w1/=0) & (w1 ¥incin v0) -- -- Now consider a sink $a$ of $w1$. It is easily seen that $w1/={a}$. -- w1-->Stat1(Stat8*) ==> Stat9: (EXISTS t in w1 | 0 = {y in w1 | [t,y] in d0}) a-->Stat9(Stat9*) ==> Stat10: ({y in w1 | [a,y] in d0} = 0) & (a in w1) Suppose ==> w1 = {a} a-->Stat8(Stat10*) ==> Stat11: {y in w1 | [y,a] in d0} /= 0 c-->Stat11(Stat10) ==> [a,a] in d0 a-->Stat10 ==> AUTO (Stat11*)Discharge ==> AUTO (w1-{a})-->Stat7(Stat8*) ==> Stat14: (EXISTS t in (w1-{a}) | 0 = {y in (w1-{a}) | [y,t] in d0}) t0-->Stat14(Stat14*) ==> Stat15: ({y in (w1-{a}) | [y,t0] in d0} = 0) & (t0 in (w1-{a})) -- -- If $t0$, which is a source of $w1-{a}$, is not a source of $w1$, then $[a,t0]$ must be an edge; -- but this conflicts with the way $a$ has been chosen. -- t0-->Stat8(Stat15*) ==> Stat16: {y in w1 | [y,t0] in d0} /= 0 b-->Stat16(Stat15*) ==> Stat17: (b notin {y in (w1-{a}) | [y,t0] in d0}) & ([b,t0] in d0) & (b in w1) b-->Stat17(Stat17) ==> Stat18: [a,t0] in d0 t0-->Stat10(Stat15,Stat18*) ==> false Discharge ==> QED -- -- --BEGIN HERE -- -- The following theorem states that every acyclic digraph $V,D$ (with $V /= 0$) has at least -- one source and one sink, namely it has vertices $s,t$ whose in-neighborhood and out-neighborhood, -- respectively, are empty. -- Theorem acyclicity4: [Every acyclic graph has sinks and sources] (Acyclic(V,D) & Finite(V) & (V /= 0)) ¥imp (EXISTS s in V, t in V | 0 = {y in V | ([s,y] in D) or ([y,t] in D)}). Proof: Suppose_not(w2,d0) ==> AUTO -- -- Arguing by contradiction, suppose that there is a counterexample $w2,d0$ to the claim. -- It readily follows from the definition of acyclicity that $w2,d0$ has sinks; -- therefore $w2,d0$ has no sources. -- Use_def(Acyclic) ==> Stat1: (FORALL w ¥incin w2 | (w /= 0) ¥imp (EXISTS t in w | 0 = {y in w | [t,y] in d0})) Suppose ==> Stat2: (EXISTS t in w2 | 0 = {y in w2 | [y,t] in d0}) t1-->Stat2(*) ==> Stat3: (not(EXISTS s in w2, t in w2 | 0 = {y in w2 | ([s,y] in d0) or ([y,t] in d0)})) & (0 = {y in w2 | [y,t1] in d0}) & (t1 in w2) w2-->Stat1(*) ==> Stat4: (EXISTS s in w2 | 0 = {y in w2 | [s,y] in d0}) s0-->Stat4 ==> AUTO (s0,t1)-->Stat3(Stat3*) ==> Stat5: (0 /= {y in w2 | ([s0,y] in d0) or ([y,t1] in d0)}) & (0 = {y in w2 | [s0,y] in d0}) & (0 = {y in w2 | [y,t1] in d0}) & (s0 in w2) & (t1 in w2) (y0,y0,y0)-->Stat5(Stat5*) ==> false Discharge ==> AUTO -- -- Then, using finite induction, we can pick a counterexample $w1,d0$ whose $w1$ is minimal. -- APPLY (fin_thryvar:w1) finiteInduction(s0->w2, P(W)->((W ¥incin w2) & (W/=0) & (not (EXISTS t in W | 0 = {y in W | [y,t] in d0})))) ==> Stat7: (FORALL v | (v ¥incin w1) ¥imp (Finite(v) & (((v ¥incin w2) & (v/=0) & (not (EXISTS t in v | 0 = {y in v | [y,t] in d0}))) ¥eq (v=w1)))) w1-->Stat7(Stat7*) ==> Stat8: (not (EXISTS t in w1 | 0 = {y in w1 | [y,t] in d0})) & (w1/=0) & (w1 ¥incin w2) -- -- Now consider a sink $a$ of $w1$. It is easily seen that $w1/={a}$. -- w1-->Stat1(Stat8*) ==> Stat9: (EXISTS t in w1 | 0 = {y in w1 | [t,y] in d0}) a-->Stat9(Stat9*) ==> Stat10: ({y in w1 | [a,y] in d0} = 0) & (a in w1) Suppose ==> w1 = {a} a-->Stat8(Stat10*) ==> Stat11: {y in w1 | [y,a] in d0} /= 0 c-->Stat11(Stat10) ==> [a,a] in d0 a-->Stat10 ==> AUTO (Stat11)Discharge ==> AUTO (w1-{a})-->Stat7(Stat8*) ==> Stat14: (EXISTS t in (w1-{a}) | 0 = {y in (w1-{a}) | [y,t] in d0}) t0-->Stat14(Stat14*) ==> Stat15: ({y in (w1-{a}) | [y,t0] in d0} = 0) & (t0 in (w1-{a})) -- -- If $t0$, which is a source of $w1-{a}$, is not a source of $w1$, then $[a,t0]$ must be an edge; -- but this conflicts with the way $a$ has been chosen. -- t0-->Stat8(Stat15*) ==> Stat16: {y in w1 | [y,t0] in d0} /= 0 b-->Stat16(Stat15*) ==> Stat17: (b notin {y in (w1-{a}) | [y,t0] in d0}) & ([b,t0] in d0) & (b in w1) b-->Stat17(Stat17) ==> Stat18: [a,t0] in d0 t0-->Stat10(Stat15,Stat18*) ==> false Discharge ==> QED -- Theorem acyclicity5: [No triangle inside an acyclic digraph] (Acyclic(V,D) & ({X,Y,Z} ¥incin V) & ({[X,Y],[Y,Z]} ¥incin D)) ¥imp ([Z,X] notin D). Proof: Suppose_not(v0,d0,x0,y0,z0) ==> AUTO Use_def(Acyclic) ==> Stat1: (FORALL w ¥incin v0 | (w /= 0) ¥imp (EXISTS t in w | 0 = {y in w | [t,y] in d0})) {x0,y0,z0}-->Stat1(*) ==> Stat2: (EXISTS t in {x0,y0,z0} | 0 = {y in {x0,y0,z0} | [t,y] in d0}) t0-->Stat2(Stat2*) ==> Stat3: (t0 in {x0,y0,z0}) & ({y in {x0,y0,z0} | [t0,y] in d0} = 0) Suppose ==> t0 = x0 EQUAL(Stat3) ==> Stat4: y0 notin {y in {x0,y0,z0} | [x0,y] in d0} y0-->Stat4(*) ==> false Discharge ==> AUTO Suppose ==> t0 = y0 EQUAL(Stat3) ==> Stat5: z0 notin {y in {x0,y0,z0} | [y0,y] in d0} z0-->Stat5(*) ==> false Discharge ==> t0 = z0 EQUAL(Stat3) ==> Stat6: x0 notin {y in {x0,y0,z0} | [z0,y] in d0} x0-->Stat6(*) ==> false Discharge ==> QED -- Theorem acyclicity6: [Adjunction of an inner vertex to a digraph cannot disrupt acyclicity] (((V ¥PROD V) incs D) & (X notin V) & (V incs S) & Acyclic(V,D)) ¥imp Acyclic(V+{X},D+(S ¥PROD {X})). Proof: Suppose_not(v0,d0,x0,s0) ==> AUTO Use_def(Acyclic) ==> Stat1: (not(FORALL w ¥incin (v0+{x0}) | (w /= 0) ¥imp (EXISTS t in w | 0 = {y in w | [t,y] in d0+(s0 ¥PROD {x0})}))) & (FORALL w ¥incin v0 | (w /= 0) ¥imp (EXISTS t in w | 0 = {y in w | [t,y] in d0})) (w0,w0)-->Stat1(Stat1*) ==> Stat2: (not(EXISTS t in w0 | 0 = {y in w0 | [t,y] in d0+(s0 ¥PROD {x0})})) & (w0 ¥incin (v0+{x0})) & (w0 /= 0) & ((x0 notin w0) ¥imp (EXISTS t in w0 | 0 = {y in w0 | [t,y] in d0})) ELEM ==> Stat3: ((v0 ¥PROD v0) incs d0) & (x0 notin v0) & (v0 incs s0) Suppose ==> Stat4: (EXISTS t in w0 | 0 = {y in w0 | [t,y] in d0}) t0-->Stat4(Stat4*) ==> Stat5: ({y in w0 | [t0,y] in d0} = 0) & (t0 in w0) t0-->Stat2(Stat5*) ==> Stat6: {y in w0 | [t0,y] in d0+(s0 ¥PROD {x0})} /= 0 y0-->Stat6(Stat6*) ==> (y0 in w0) & ([t0,y0] in d0+(s0 ¥PROD {x0})) y0-->Stat5(Stat6*) ==> Stat7: [t0,y0] in (s0 ¥PROD {x0}) ([t0,y0],s0,{x0})-->Tcartesian_0(Stat7) ==> (t0 in s0) & (y0 = x0) EQUAL(Stat6) ==> Stat8: x0 in w0 x0-->Stat2(Stat8*) ==> Stat9: {y in w0 | [x0,y] in d0+(s0 ¥PROD {x0})} /= 0 y2-->Stat9(Stat9*) ==> [x0,y2] in d0+(s0 ¥PROD {x0}) Suppose ==> [x0,y2] in (v0 ¥PROD v0) ([x0,y2],v0,v0)-->Tcartesian_0(Stat3) ==> false; Discharge ==> AUTO (Stat3*)ELEM ==> Stat10: [x0,y2] in (s0 ¥PROD {x0}) ([x0,y2],s0,{x0})-->Tcartesian_0(Stat10) ==> x0 in s0 (Stat3*)Discharge ==> x0 in w0 x0-->Stat2(Stat3*) ==> Stat11: {y in w0 | [x0,y] in d0+(s0 ¥PROD {x0})} /= 0 y3-->Stat11(Stat11*) ==> [x0,y3] in d0+(s0 ¥PROD {x0}) Suppose ==> [x0,y3] in (v0 ¥PROD v0) ([x0,y3],v0,v0)-->Tcartesian_0(Stat3) ==> false; Discharge ==> AUTO (Stat3*)ELEM ==> Stat12: [x0,y3] in (s0 ¥PROD {x0}) ([x0,y3],s0,{x0})-->Tcartesian_0(Stat12) ==> x0 in s0 (Stat3*)Discharge ==> QED -- -- Theorem voidgraph1: [The void has all virtues] (V ¥incin {X}) ¥imp (Extensional(V,0) & Orientates(0,V,E)). Proof: Suppose_not(v0,x0,e0) ==> AUTO Suppose ==> not Extensional(v0,0) Use_def(Extensional) ==> Stat1: not(FORALL x in v0, y in v0 | (EXISTS z | (([x,z] in 0) ¥eq ([y,z] in 0)) ¥imp (x = y))) (x1,y1)-->Stat1(*) ==> Stat2: not (EXISTS z | (([x1,z] in 0) ¥eq ([y1,z] in 0)) ¥imp (x1 = y1)) & (x1 = x0) & (y1 = x0) 0-->Stat2(Stat2*) ==> false Discharge ==> AUTO Use_def(Orientates) ==> Stat3: ({{x,y}: x in v0, y in (v0-{x})} /= 0) or ({{car(p),cdr(p)}: p in 0 | p = [car(p), cdr(p)]} /= 0) (x2,y2,p)-->Stat3(*) ==> false Discharge ==> QED -- Theorem voidgraph2: [The void has all virtues, 2] Acyclic(V,0). Proof: Suppose_not(v0) ==> AUTO Use_def(Acyclic) ==> Stat1: not(FORALL w ¥incin v0 | (w /= 0) ¥imp (EXISTS t in w | 0 = {y in w | [t,y] in 0})) w0-->Stat1(*) ==> Stat2: (w0 /= 0) & (not(EXISTS t in w0 | 0 = {y in w0 | [t,y] in 0})) (t0,t0)-->Stat2(Stat2*) ==> Stat3: 0 /= {y in w0 | [t0,y] in 0} y0-->Stat3(Stat3*) ==> false Discharge ==> QED -- -- THEORY finAcycLabeling(v0,d0,h(S,X)) Is_map(d0) Acyclic(v0,d0) Finite(v0) END finAcycLabeling -- ENTER_THEORY finAcycLabeling -- Theorem finAcycLabeling_0: [Recursive labeling of an acyclic graph] (EXISTS f | Svm(f) & (domain(f) = v0) & (FORALL x in v0 | (f~[x]) = h({(f~[cdr(p)]): p in (d0 ¥ON {x}) | cdr(p) in v0},x))). Proof: Suppose_not() ==> AUTO Assump ==> Stat0: Finite(v0) & Acyclic(v0,d0) & Is_map(d0) -- -- Suppose that the contrary holds, so that $v0$ has a subset $v1$ which cannot be labeled in the way specified for $v0$ in the claim. -- Suppose ==> Stat1: not(EXISTS v ¥incin v0 | Finite(v) & (not(EXISTS f | Svm(f) & (domain(f) = v) & (FORALL x in v | (f~[x]) = h({(f~[cdr(p)]): p in (d0 ¥ON {x}) | cdr(p) in v},x))))) v0-->Stat1(*) ==> false; Discharge ==> Stat2: (EXISTS v ¥incin v0 | Finite(v) & (not(EXISTS f | Svm(f) & (domain(f) = v) & (FORALL x in v | (f~[x]) = h({(f~[cdr(p)]): p in (d0 ¥ON {x}) | cdr(p) in v},x))))) v1-->Stat2(Stat2*) ==> Finite(v1) & (v1 ¥incin v0) & (not (EXISTS f | Svm(f) & (domain(f) = v1) & (FORALL x in v1 | (f~[x]) = h({(f~[cdr(p)]): p in (d0 ¥ON {x}) | cdr(p) in v1},x)))) -- -- In view of the finiteness of $v0$, we can consider an inclusion-minimal such subset, $v2$. -- Plainly, $v2 /= 0$ must hold. -- APPLY(fin_thryvar:v2) finiteInduction(s0->v1,P(V)->((V ¥incin v0) & (not(EXISTS f | Svm(f) & (domain(f) = V) & (FORALL x in V | (f~[x]) = h({(f~[cdr(p)]): p in (d0 ¥ON {x}) | cdr(p) in V},x)))))) ==> Stat3: (FORALL V | (V ¥incin v2) ¥imp ( Finite(V) & (((V ¥incin v0) & (not(EXISTS f | Svm(f) & (domain(f) = V) & (FORALL x in V | (f~[x]) = h({(f~[cdr(p)]): p in (d0 ¥ON {x}) | cdr(p) in V},x))))) ¥eq (V = v2) ) )) v2-->Stat3(Stat3*) ==> Stat4: (not(EXISTS f | Svm(f) & (domain(f) = v2) & (FORALL x in v2 | (f~[x]) = h({(f~[cdr(p)]): p in (d0 ¥ON {x}) | cdr(p) in v2},x)))) & (v2 ¥incin v0) & Finite(v2) Suppose ==> v2 = 0 0-->Tdomain_1(Stat4*) ==> domain(0) = v2 0-->Timage_0(Stat4*) ==> Svm(0) 0-->Stat4(Stat4*) ==> Stat5: not (FORALL x in v2 | (0~[x]) = h({(0~[cdr(p)]): p in (d0 ¥ON {x}) | cdr(p) in v2},x)) x0-->Stat5(Stat4*) ==> false Discharge ==> AUTO -- -- The digraph $v2,d0$ inherits from $v0,d0$ the acyclicity property; therefore it has a source, $s0$. -- The minimality of $v2$ implies that $v2-{s0}$ can be labeled in the way specified for $v0$ in the claim. -- Let $f1$ be such a labeling for $v2-{s0}$. -- (v0,d0,v2,d0)-->Tacyclicity1(*) ==> Acyclic(v2,d0) (v2,d0)-->Tacyclicity4(Stat4*) ==> Stat6: (EXISTS t in v2, s in v2 | 0 = {y in v2 | ([t,y] in d0) or ([y,s] in d0)}) (t0,s0)-->Stat6(Stat6*) ==> Stat7: (0 = {y in v2 | ([t0,y] in d0) or ([y,s0] in d0)}) & (s0 in v2) (v2-{s0})-->Stat3(Stat4*) ==> Stat8: (EXISTS f | Svm(f) & (domain(f) = (v2-{s0})) & (FORALL x in (v2-{s0}) | (f~[x]) = h({(f~[cdr(p)]): p in (d0 ¥ON {x}) | cdr(p) in (v2-{s0})},x))) f1-->Stat8(Stat8*) ==> Stat9: (FORALL x in (v2-{s0}) | (f1~[x]) = h({(f1~[cdr(p)]): p in (d0 ¥ON {x}) | cdr(p) in (v2-{s0})},x)) & Svm(f1) & (domain(f1) = (v2-{s0})) -- -- We will define a single-valued map $f2$ of domain $v2$ such that -- $(f2~[x]) = h({(f2~[cdr(p)]): p in (d0 ¥ON {x}) | cdr(p) in v2},x)$ -- holds for all $x in v2$, contrary to what Stat4 claims. This contradiction will lead us to the desired conclusion. -- Loc_def ==> Stat10: f2 = f1 + {[s0,h({(f1~[cdr(p)]): p in (d0 ¥ON {s0}) | cdr(p) in (v2-{s0})},s0)]} -- -- After defining $f2$ in the way just shown, we readily check that $f2$ is a single-valued map -- and that its domain is $v2$. According to Stat4, $f2$ fails to meet the labeling condition. -- ({[s0,h({(f1~[cdr(p)]): p in (d0 ¥ON {s0}) | cdr(p) in (v2-{s0})},s0)]},s0,h({(f1~[cdr(p)]): p in (d0 ¥ON {s0}) | cdr(p) in (v2-{s0})},s0))-->TsingletonMap_1(Stat10*) ==> Svm({[s0,h({(f1~[cdr(p)]): p in (d0 ¥ON {s0}) | cdr(p) in (v2-{s0})},s0)]}) & (domain({[s0,h({(f1~[cdr(p)]): p in (d0 ¥ON {s0}) | cdr(p) in (v2-{s0})},s0)]}) = {s0}) (f1,{[s0,h({(f1~[cdr(p)]): p in (d0 ¥ON {s0}) | cdr(p) in (v2-{s0})},s0)]})-->Tsvm_1(Stat8*) ==> Svm(f1 + {[s0,h({(f1~[cdr(p)]): p in (d0 ¥ON {s0}) | cdr(p) in (v2-{s0})},s0)]}) (f1+{[s0,h({(f1~[cdr(p)]): p in (d0 ¥ON {s0}) | cdr(p) in (v2-{s0})},s0)]},f1,{[s0,h({(f1~[cdr(p)]): p in (d0 ¥ON {s0}) | cdr(p) in (v2-{s0})},s0)]})-->Tdomain_1(Stat6*) ==> domain(f1+{[s0,h({(f1~[cdr(p)]): p in (d0 ¥ON {s0}) | cdr(p) in (v2-{s0})},s0)]}) = v2 EQUAL(Stat10) ==> Svm(f2) & (domain(f2) = v2) -- -- Where is the map $f2$ defective? Let $x2$ be a vertex in $v2$ where the labeling condition is violated. -- f2-->Stat4(Stat10*) ==> Stat11: not(FORALL x in v2 | (f2~[x]) = h({(f2~[cdr(p)]): p in (d0 ¥ON {x}) | cdr(p) in v2},x)) x2-->Stat11(Stat11*) ==> (x2 in v2) & ((f2~[x2]) /= h({(f2~[cdr(p)]): p in (d0 ¥ON {x2}) | cdr(p) in v2},x2)) TELEM ==> {[s0,h({(f1~[cdr(p)]): p in (d0 ¥ON {s0}) | cdr(p) in (v2-{s0})},s0)]}+f1 = f1+{[s0,h({(f1~[cdr(p)]): p in (d0 ¥ON {s0}) | cdr(p) in (v2-{s0})},s0)]} -- -- Notice that -- ${(f1~[cdr(p)]): p in (d0 ¥ON {x2}) | cdr(p) in (v2-{s0})} /= {(f2~[cdr(p)]): p in (d0 ¥ON {x2}) | cdr(p) in v2}$. -- This is proved in two slightly different ways depending on whether $x2$ is the selected source of $v2$. -- Suppose ==> {(f1~[cdr(p)]): p in (d0 ¥ON {x2}) | cdr(p) in (v2-{s0})} = {(f2~[cdr(p)]): p in (d0 ¥ON {x2}) | cdr(p) in v2} -- -- Discard first the case when $x2 = s0$: -- Suppose ==> x2 = s0 (x2,f1,{[s0,h({(f1~[cdr(p)]): p in (d0 ¥ON {s0}) | cdr(p) in (v2-{s0})},s0)]})-->Timage_2(Stat8*) ==> (f1 + {[s0,h({(f1~[cdr(p)]): p in (d0 ¥ON {s0}) | cdr(p) in (v2-{s0})},s0)]})~[x2] = {[s0,h({(f1~[cdr(p)]): p in (d0 ¥ON {s0}) | cdr(p) in (v2-{s0})},s0)]}~[x2] ({[s0,h({(f1~[cdr(p)]): p in (d0 ¥ON {s0}) | cdr(p) in (v2-{s0})},s0)]},s0,h({(f1~[cdr(p)]): p in (d0 ¥ON {s0}) | cdr(p) in (v2-{s0})},s0))-->TsingletonMap_2(Stat11*) ==> {[s0,h({(f1~[cdr(p)]): p in (d0 ¥ON {s0}) | cdr(p) in (v2-{s0})},s0)]}~[s0] = h({(f1~[cdr(p)]): p in (d0 ¥ON {s0}) | cdr(p) in (v2-{s0})},s0) EQUAL(Stat10) ==> false; Discharge ==> AUTO -- -- But then $x2$ must be an element of $v2-{s0}$, where $f2$ behaves exactly like $f1$ -- and hence meets the labeling condition. By reaching a contradiction also in this case, -- we obtain the sought intermediate conclusion. -- x2-->Stat9(Stat11*) ==> (x2 in v2-{s0}) & ((f1~[x2]) = h({(f1~[cdr(p)]): p in (d0 ¥ON {x2}) | cdr(p) in (v2-{s0})},x2)) (x2,{[s0,h({(f1~[cdr(p)]): p in (d0 ¥ON {s0}) | cdr(p) in (v2-{s0})},s0)]},f1)-->Timage_2(Stat8*) ==> (({[s0,h({(f1~[cdr(p)]): p in (d0 ¥ON {s0}) | cdr(p) in (v2-{s0})},s0)]}+f1)~[x2]) = (f1~[x2]) EQUAL(Stat10) ==> false; Discharge ==> Stat15: {(f1~[cdr(p)]): p in (d0 ¥ON {x2}) | cdr(p) in (v2-{s0})} /= {(f2~[cdr(p)]): p in (d0 ¥ON {x2}) | cdr(p) in v2} p3-->Stat15(Stat15*) ==> Stat16: (p3 in (d0 ¥ON {x2})) & (((cdr(p3) in (v2-{s0})) ¥neq (cdr(p3) in v2)) or ((f1~[cdr(p3)]) /= (f2~[cdr(p3)]))) (d0,p3,x2)-->Trestr_3(Stat0,Stat16*) ==> (p3 = [x2,cdr(p3)]) & (p3 in d0) Suppose ==> cdr(p3) = s0 EQUAL(Stat16) ==> [x2,s0] in d0 x2-->Stat7(Stat11*) ==> false Discharge ==> AUTO (cdr(p3),{[s0,h({(f1~[cdr(p)]): p in (d0 ¥ON {s0}) | cdr(p) in (v2-{s0})},s0)]},f1)-->Timage_2(Stat9*) ==> ({[s0,h({(f1~[cdr(p)]): p in (d0 ¥ON {s0}) | cdr(p) in (v2-{s0})},s0)]}+f1)~[cdr(p3)] = f1~[cdr(p3)] EQUAL(Stat10) ==> f1~[cdr(p3)] = f2~[cdr(p3)] (Stat16*)Discharge ==> QED -- -- APPLY(v1_thryvar:lab_thryvar) Skolem() ==> Theorem finAcycLabeling_1: Svm(lab_thryvar) & (domain(lab_thryvar) = v0) & (FORALL x in v0 | (lab_thryvar~[x]) = h({(lab_thryvar~[cdr(p)]): p in (d0 ¥ON {x}) | cdr(p) in v0},x)) -- ENTER_THEORY Set_theory -- -- DISPLAY finAcycLabeling -- -- THEORY finAcycLabeling(v0,d0,h(s,x)) -- Acyclic(v0,d0) -- Finite(v0) -- ==>(lab_thryvar) -- Svm(lab_thryvar) -- (domain(lab_thryvar) = v0) -- (FORALL x in v0 | (lab_thryvar~[x]) = h({(lab_thryvar~[cdr(p)]): p in (d0 ¥ON {x}) | cdr(p) in v0},x)) -- END finAcycLabeling -- -- \subsection{Connectivity} -- -- A handy introduction to connectivity is achieved along the path developed below. -- We will say that a (finite) graph is connected if and only if it has a spanning tree. -- A spanning tree must have the same vertices as the graph $V,E$ which it spans, -- and, for edges, a subset of $E$. In the special case when $V$ is singleton, we choose -- to represent the tree as a self-loop; in all other cases, a tree shall be devoid of hanks -- (i.e., it must be cycle-free) and will admit no non-trivial partition -- of its set of edges into vertex-disjoint blocks. -- -- \subsubsection{The unionset operation} -- Def unionset: [Family of all members of members of a set] Un(S) := {u: v in S, u in v} -- Theorem un_0: [Unionset operation yielding null result] (Un(X) = 0) ¥eq (X ¥incin {0}). Proof: Suppose_not(x0) ==> AUTO Use_def(Un(x0)) ==> AUTO Suppose ==> Stat1: (x0 ¥nincin {0}) & ({y: x in x0, y in x} = 0) (x1,x1,arb(x1))-->Stat1(Stat1) ==> false; Discharge ==> Stat2: ({y: x in x0, y in x} /= 0) & (x0 ¥incin {0}) (x2,y2)-->Stat2(Stat2*) ==> false Discharge ==> QED -- Theorem un_1: [Unionset operation yielding sigleton result] (Un(X) = {Y}) ¥eq ((X ¥incin {0,{Y}}) & ({Y} in X)). Proof: Suppose_not(x0,y0) ==> AUTO Use_def(Un) ==> Stat0: Un(x0) = {y: x in x0, y in x} Suppose ==> Stat1: (x0 ¥nincin {0,{y0}}) & (Un(x0) = {y0}) x1-->Stat1(Stat1) ==> Stat2: (arb(x1 - {y0}) in (x1 - {y0})) & (x1 in x0) Loc_def ==> a = arb(x1 - {y0}) EQUAL(Stat0) ==> Stat3: a notin {y: x in x0, y in x} (x1,a)-->Stat3(Stat2*) ==> false Discharge ==> AUTO Suppose ==> ({y0} notin x0) & (Un(x0) = {y0}) x0-->Tun_0(Stat0*) ==> false Discharge ==> AUTO Suppose ==> Stat4: (y0 notin {y: x in x0, y in x}) & ({y0} in x0) ({y0},y0)-->Stat4(Stat4*) ==> false; Discharge ==> Stat5: (Un(x0) ¥nincin {y0}) & (x0 ¥incin {0,{y0}}) e-->Stat5(Stat0*) ==> Stat6: (e in {y: x in x0, y in x}) & (e /= y0) (x2,y2)-->Stat6(Stat5) ==> (x2 = {y0}) & (e in x2) (Stat6*)Discharge ==> QED -- Theorem un_2: [Unionset operation combined with set adjunction] (X + {Y} = Z) ¥imp (Un(Z) = Un(X) + Y). Proof: Suppose_not(x0,y0,z0) ==> AUTO EQUAL ==> Stat0: Un(x0 + {y0}) /= Un(x0) + y0 Use_def(Un)(Stat0) ==> Stat1: {y: x in x0+{y0}, y in x} /= ({yp: xp in x0, yp in xp} + y0) c-->Stat1(Stat1*) ==> (c in {y: x in x0+{y0}, y in x}) ¥neq (c in ({yp: xp in x0, yp in xp} + y0)) Suppose ==> Stat2: (c in {y: x in x0+{y0}, y in x}) & (c notin {yp: xp in x0, yp in xp}) & (c notin y0) (x1,y1,x1,y1)-->Stat2(Stat2*) ==> false; Discharge ==> AUTO Suppose ==> Stat3: (c notin {y: x in x0+{y0}, y in x}) & (c in y0) (y0,c)-->Stat3(Stat3*) ==> false; Discharge ==> Stat4: (c in {yp: xp in x0, yp in xp}) & (c notin {y: x in x0+{y0}, y in x}) (x2,y2,x2,y2)-->Stat4(Stat4*) ==> false Discharge ==> QED -- Theorem un_3: [Unionset operation combined with single removal and adjunction] (B in S) ¥imp (Un(S-{B}+{B+{A}}) = Un(S)+{A}). Proof: Suppose_not(b0,s0,a0) ==> AUTO (s0-{b0},b0,s0)-->Tun_2(*) ==> Un(s0) = Un(s0-{b0}) + b0 (s0-{b0},b0+{a0},s0-{b0}+{b0+{a0}})-->Tun_2(*) ==> Un(s0-{b0}+{b0+{a0}}) = Un(s0-{b0}) + b0 + {a0} EQUAL ==> false Discharge ==> QED -- Theorem un_4: [Unionset operation applied to a singleton] ({Y} = Z) ¥imp (Un(Z) = Y). Proof: Suppose_not(y0,z0) ==> AUTO 0-->Tun_0(*) ==> Un(0) = 0 (0,y0,z0)-->Tun_2(*) ==> false Discharge ==> QED -- Theorem un_5: [Unionset operation applied to a singleton, 2] ((U /= 0) & (Un(S) = U) & (S ¥incin {X})) ¥imp (S = {U}). Proof: Suppose_not(u0,s0,x0) ==> AUTO s0-->Tun_0(*) ==> {x0} = s0 (x0,s0)-->Tun_4(*) ==> u0 = x0 Discharge ==> QED -- -- \subsubsection{Trees} -- -- -- A first characterization of connectivity, which plays a limited role in the ongoing -- formal development but which we need in order to define trees, is that a set of edges -- is connected if it can nohow be partitioned into multiple vertex-disjoint blocks. -- We do not need to adopt officially the definition shown in this comment, because we -- will build it directly into the definition of tree: -- -- Def connectivity0: [A set of edges that cannot be partitioned into multiple vertex-disjoint blocks] $PreTree(E) := {b ¥incin E | Un(b) * Un(E-b) = 0} ¥incin {0,E}$ -- Def hank_free: [A hank-free graph is one whose edges do not include a hank] HankFree(T) := (FORALL e ¥incin T | (e = 0) or (EXISTS a in e | a ¥nincin Un( e - {a} ))) -- Def tree1: [A tree is a hank-free graph whose edges cannot be partitioned into multiple vertex-disjoint blocks] Is_tree(T) := (T /= 0) & ({b ¥incin T | Un(b) * Un(T-b) = 0} ¥incin {0,T}) & HankFree(T) -- Theorem tree_0: [A tree cannot be null or have a null edge] Is_tree(T) ¥imp (0 notin (T+{T})). Proof: Suppose_not(t0) ==> AUTO Use_def(HankFree(t0)) ==> AUTO Use_def(Is_tree) ==> Stat0: (0 in t0) & Stat1: (FORALL e ¥incin t0 | (e = 0) or (EXISTS a in e | a ¥nincin Un( e - {a}))) {0}-->Stat1(Stat0*) ==> Stat2: (EXISTS a in {0} | a ¥nincin Un( {0} - {a})) x0-->Stat2(Stat0*) ==> false Discharge ==> QED -- -- Theorem tree_1: [Non-singleton trees can be pruned] (Is_tree(T) & (T /= {arb(T)}) & (T ¥incin {{x,y}: p in T, x in p, y in p})) ¥imp (EXISTS e in T, u in e | ({a in T | u notin a} = T-{e}) & Is_tree(T-{e})). Proof: Suppose_not(t0) ==> AUTO -- -- Supposing that the contrary holds for $t0$, consider an edge $a0$ of $t0$ -- one of whose endpoints, $u0$, is not a vertex of $t0-{a0}$. Consequently, -- either $t0-{a0}$ differs from the set of edges not incident to $u0$ or -- $t0-{a0}$ is not a tree. -- Loc_def ==> ap = arb(t0) Use_def(HankFree(t0)) ==> AUTO Use_def(Is_tree) ==> Stat0: (FORALL e ¥incin t0 | (e = 0) or (EXISTS a in e | a ¥nincin Un( e - {a}))) & Stat0a: ({b ¥incin t0 | Un(b) * Un(t0-b) = 0} ¥incin {0,t0}) t0-->Ttree_0 ==> Stat1: (t0 incs {ap}) & (t0 /= {ap}) t0-->Stat0(Stat0*) ==> Stat2: (EXISTS a in t0 | a ¥nincin Un( t0 - {a})) a0-->Stat2(*) ==> Stat3: (a0 ¥nincin Un( t0 - {a0})) & (not(EXISTS e in t0, u in e | ({a in t0 | u notin a} = t0-{e}) & Is_tree(t0-{e}))) & (a0 in t0) & (t0 ¥incin {{x,y}: p in t0, x in p, y in p}) (u0,a0,u0)-->Stat3(Stat3*) ==> Stat4: (u0 notin Un(t0 - {a0})) & (not (({a in t0 | u0 notin a} = t0-{a0}) & Is_tree(t0-{a0}))) & (u0 in a0) -- -- The first condition of the alternative is readily discharged; -- hence $t0-{a0}$ is not a tree and it must violate at least one of the -- two conditions for being a tree. -- Suppose ==> Stat7: {a in t0 | u0 notin a} /= t0-{a0} a1-->Stat7 ==> AUTO Suppose ==> Stat8: a1 notin {a in t0 | u0 notin a} (t0-{a0},a1,t0-{a0})-->Tun_2(Stat4*) ==> (a1 in t0) & (u0 notin a1) a1-->Stat8(Stat8*) ==> false Discharge ==> Stat9: (a1 in {a in t0 | u0 notin a}) & (a1 notin t0-{a0}) ()-->Stat9(Stat9,Stat4*) ==> false Discharge ==> {a in t0 | u0 notin a} = t0-{a0} -- -- One easily sees that the violated condition cannot be cycle-freeness; hence -- it must be the other condition. Consider, accordingly, a partition $p0$ of $t0-{a0}$ -- into two equivalence classes, $b0$ and $t0-{a0}-b0$, devoid of common vertices. -- Plainly, ${a0}$ does not belong to $p0$. -- Set_monot ==> (FORALL e ¥incin t0 | (e = 0) or (EXISTS a in e | a ¥nincin Un( e - {a}))) ¥imp (FORALL e ¥incin (t0-{a0}) | (e = 0) or (EXISTS a in e | a ¥nincin Un( e - {a}))) Use_def(HankFree(t0-{a0})) ==> AUTO Use_def(Is_tree) ==> Stat10: ({b ¥incin (t0-{a0}) | Un(b) * Un(t0-{a0}-b) = 0} ¥nincin {0, t0-{a0}}) b0-->Stat10(Stat10,Stat1*) ==> Stat12: (b0 in {b ¥incin (t0-{a0}) | Un(b) * Un(t0-{a0}-b) = 0}) & (b0 /= 0) & (b0 /= (t0-{a0})) ()-->Stat12(Stat12*) ==> Stat13: (b0 ¥incin (t0-{a0})) & (Un(b0) * Un(t0-{a0}-b0) = 0) Use_def(Is_tree) ==> {b ¥incin t0 | Un(b) * Un(t0-b) = 0} ¥incin {0,t0} -- -- We discard first the possibility that the block $t0-{a0}-b0$ of the partition -- $p0$ has $Un(t0-{a0}-b0)$ intersecting $a0$, by showing that if this were the case, -- then $p0$ could be extended into a multiple partition $p1$ of $t0$ -- in which no two blocks share vertices. Such a $p1$ is simply obtained -- by adjoining $a0$ to the block $b0$ of $p0$. -- Suppose ==> a0 * Un(t0-{a0}-b0) = 0 Loc_def ==> b1 = b0 + {a0} (b0,a0,b1)-->Tun_2(Stat12*) ==> Stat14: (b1 notin {b ¥incin t0 | Un(b) * Un(t0-b) = 0}) & (Un(b1) = Un(b0) + a0) b1-->Stat14(Stat3*) ==> ((Un(b0) + a0) * Un(t0-b1) /= 0) & (t0-{a0}-b0 = t0-b1) EQUAL ==> (Un(b0) * Un(t0-b1) = 0) & (a0 * Un(t0-b1) = 0) (Stat14*)Discharge ==> AUTO -- -- In sight of showing that $a0 * Un(b0) = 0$, we observe that $a0$ can neither consist -- of $u0$ alone nor have more than two elements; hence let $w0$ be its endpoint -- distinct from $u0$. This must be the only member of $a0 * Un(t0-{a0}-b0)$. -- Set_monot ==> {v: u in t0-{a0}-b0, v in u} ¥incin {v: u in t0-{a0}, v in u} Use_def(Un) ==> u0 notin Un(t0-{a0}-b0) (Stat3*)ELEM ==> Stat15: (a0 in {{x,y}: q in t0, x in q, y in q}) & (a0 ¥nincin {u0}) (q0,x0,y0,w0)-->Stat15(Stat15,Stat4*) ==> ({u0,w0} = a0) & (u0 /= w0) (Stat12*)ELEM ==> a0 * Un(t0-{a0}-b0) = {w0} -- -- Now suppose that $Un(b0)$ also intersects $a0$. -- If this were the case then $Un(b0)$ and $Un(t0-{a0}-b0)$ would intersect; indeed, -- neither $Un(b0)$ nor $Un(t0-{a0}-b0)$ can have $u0$ for element, hence these two unions -- must share $w0$. However, we know that in $p0$ no two blocks share vertices. -- Suppose ==> a0 * Un(b0) /= 0 Set_monot ==> {v: u in b0, v in u} ¥incin {v: u in t0-{a0}, v in u} Use_def(Un) ==> u0 notin Un(b0) (Stat12*)ELEM ==> false Discharge ==> Stat16: a0 * Un(b0) = 0 -- -- Now extend $p0$ by adjoining the edge $a0$ to its block $t0-{a0}-b0$. -- This extension will result into a multiple partition $p2$ of -- $t0$ in which no two blocks share vertices. -- Loc_def ==> b2 = t0-{a0}-b0 + {a0} (t0-{a0}-b0,a0,b2)-->Tun_2(Stat12*) ==> Un(b2) = a0 + Un(t0-{a0}-b0) (Stat12*)ELEM ==> Stat17: b2 notin {b ¥incin t0 | Un(b) * Un(t0-b) = 0} b2-->Stat17(Stat3*) ==> ((a0 + Un(t0-{a0}-b0)) * Un(t0-b2) /= 0) & (b0 = t0-b2) EQUAL(Stat17) ==> Stat18: (a0 * Un(b0)) + (Un(t0-{a0}-b0) * Un(b0)) /= 0 (Stat13,Stat16,Stat18*)Discharge ==> QED -- -- Theorem tree_2: [Every singleton other than ${0}$ is a tree] (A /= 0) ¥eq Is_tree({A}). Proof: Suppose_not(a0) ==> AUTO -- -- Recall that ${0}$ is not a tree and observe that no singleton $a0$ -- cannot be partitioned into more than one equivalence class. -- {a0}-->Ttree_0 ==> AUTO Suppose ==> Stat1: {b ¥incin {a0} | Un(b) * Un({a0}-b) = 0} ¥nincin {0,{a0}} b0-->Stat1(Stat1*) ==> Stat2: (b0 in {b ¥incin {a0} | Un(b) * Un({a0}-b) = 0}) & (b0 /= 0) & (b0 /= {a0}) b1-->Stat2(Stat2*) ==> false Discharge ==> AUTO -- -- Consequently, the only reason why a singleton $a0/={0}$ might fail to be a tree -- could be its lack of cycle-freeness. But this is also untenable. -- Use_def(HankFree({a0})) ==> AUTO Use_def(Is_tree) ==> Stat3: not (FORALL e ¥incin {a0} | (e = 0) or (EXISTS a in e | a ¥nincin Un( e - {a}))) & (a0 /= 0) e1-->Stat3(Stat3*) ==> Stat4: (not(EXISTS a in e1 | a ¥nincin Un( e1 - {a}))) & (e1 = {a0}) a0-->Stat4(Stat4*) ==> a0 ¥incin Un(e1 - {a0}) (e1 - {a0})-->Tun_0(Stat3*) ==> a0 = 0 (Stat3*)Discharge ==> QED -- -- Theorem tree_3: [Irreducible singleton edges in trees] (Is_tree(T) & ({X} in T) & ({e in T | X notin e} = T-{{X}})) ¥imp (not Is_tree(T-{{X}})). Proof: Suppose_not(t0,x0) ==> Stat0: ({e in t0 | x0 notin e} = t0-{{x0}}) & Is_tree(t0) & ({x0} in t0) & Is_tree(t0-{{x0}}) Use_def(Is_tree) ==> {b ¥incin t0 | Un(b) * Un(t0-b) = 0} ¥incin {0,t0} (t0-{{x0}})-->Ttree_0(*) ==> Stat1: ((t0-{{x0}}) notin {b ¥incin t0 | Un(b) * Un(t0-b) = 0}) & (t0-(t0-{{x0}}) = {{x0}}) (t0-{{x0}})-->Stat1(Stat1*) ==> Un(t0-{{x0}}) * Un(t0-(t0-{{x0}})) /= 0 ({x0},{{x0}})-->Tun_4(Stat2*) ==> Stat2: Un({{x0}}) = {x0} Use_def(Un(t0-{{x0}})) ==> AUTO EQUAL(Stat1) ==> Stat3: x0 in {v: u in t0-{{x0}}, v in u} (u0,v0)-->Stat3(Stat3,Stat0*) ==> Stat4: (u0 in {e in t0 | x0 notin e}) & (x0 in u0) ()-->Stat4(Stat4*) ==> false Discharge ==> QED -- -- Theorem tree_4: [In a tree resulting from removal of an edge from a tree, only one vertex gets lost] (Is_tree(T) & ({X,Y} = A) & (A in T) & Is_tree(T-{A}) & ({e in T | X notin e} = T-{A})) ¥imp (Un(T-{A}) = Un(T)-{X}). Proof: Suppose_not(t0,u0,w0,a0) ==> AUTO -- -- Contrary to the claim, suppose that -- $(Un(t0-{a0}) /= Un(t0)-{u0}) & Is_tree(t0) & ({u0,w0} = a0) & (a0 in t0) & Is_tree(t0-{a0}) & ({e in t0 | u0 notin e} = t0-{a0})$ -- holds for $t0,u0,w0,a0$. Then we must have $u0 /= w0$ as the only -- element differentiating $Un(t0-{a0})$ from $Un(t0)-{u0}$. -- Suppose ==> Stat0: not( Un(t0) - {u0} = Un(t0-{a0}) + {w0} ) Suppose ==> Un(t0-{a0}) ¥nincin (Un(t0) - {u0}) Use_def(Un)(Stat0) ==> Stat1: {x: y in t0-{a0}, x in y} ¥nincin ({x: y in t0, x in y} - {u0}) Set_monot(Stat1) ==> {x: y in t0-{a0}, x in y} ¥incin {x: y in t0, x in y} (Stat1*)ELEM ==> Stat2: u0 in {x: y in t0-{a0}, x in y} (y1,x1)-->Stat2(*) ==> Stat3: (y1 in {e in t0 | u0 notin e}) & (u0 in y1) ()-->Stat3(Stat3*) ==> false Discharge ==> AUTO (t0,a0,t0)-->Tun_2 ==> AUTO Suppose ==> a0 = {u0} EQUAL ==> Stat4: Is_tree(t0) & ({u0} in t0) & ({e in t0 | u0 notin e} = t0-{{u0}}) & Is_tree(t0-{{u0}}) (t0,u0)-->Ttree_3(Stat4*) ==> false Discharge ==> u0 /= w0 u1-->Stat0(*) ==> (u1 in Un(t0) - {u0}) & (u1 notin Un(t0-{a0}) + {w0}) Use_def(Un) ==> Stat5: (u1 in {x: y in t0, x in y}) & (u1 notin {x: y in t0-{a0}, x in y}) & (u1 /= u0) & (u1 /= w0) (y2,x2,y2,x2)-->Stat5(Stat5*) ==> (u1 in a0) & (u1 /= u0) & (u1 /= w0) Discharge ==> AUTO -- -- Consider now the partition ${t0-{a0},{a0}}$ of $Un(t0)$. -- The two blocks of the said partition must share a vertex, because $t0$ is a tree. -- The shared vertex must be either $u0$ or $w0$, because $u0,w0$ are the only vertices in $a0$; -- however, as we already know, neither of $u0,w0$ belongs to $Un(t0-{a0})$ -- (see the statement Stat0 discharged above and bear in mind that $Un(t0-{a0})/=Un(t0)-{u0}$). -- This contradiction completes our argument and proves the claim. -- Use_def(Is_tree) ==> {b ¥incin t0 | Un(b) * Un(t0-b) = 0} ¥incin {0,t0} (t0-{a0})-->Ttree_0(*) ==> Stat7: ((t0-{a0}) notin {b ¥incin t0 | Un(b) * Un(t0-b) = 0}) & (t0-(t0-{a0}) = {a0}) (t0-{a0})-->Stat7(Stat7*) ==> Un(t0-{a0}) * Un(t0-(t0-{a0})) /= 0 (a0,{a0})-->Tun_4(Stat8*) ==> Stat8: Un({a0}) = a0 EQUAL ==> Stat9: Un(t0-{a0}) * Un({a0}) /= 0 Discharge ==> QED -- -- -- \subsubsection{Spanning trees and cut vertices} -- -- Next we bring into play an alternative notion -- of connectivity, based on a spanning tree, more directly -- exploitable than the connectivity notion which helped -- us in characterizing trees in what precedes. -- Def connectivity1: [A graph endowed with a spanning tree] HasSpanningTree(V,E) := (EXISTS t | Is_tree(t) & (Un(t) = V) & ((V = {arb(V)}) or (t ¥incin E))) -- Theorem connectivity_0: [Non-triviality of connectivity] HasSpanningTree(V,E) ¥imp (V /= 0). Proof: Suppose_not(v0,e0) ==> AUTO Use_def(HasSpanningTree) ==> Stat1: (EXISTS t | Is_tree(t) & (Un(t) = v0) & ((v0 = {arb(v0)}) or (t ¥incin e0))) t0-->Stat1(*) ==> Is_tree(t0) & (Un(t0) = 0) t0-->Tun_0(Stat1*) ==> t0 ¥incin {0} t0-->Ttree_0(Stat1*) ==> false Discharge ==> QED -- Theorem connectivity_1: [No vertex is isolated in a graph endowed with a spanning tree] (HasSpanningTree(V,E) & (E ¥incin {{x,y}: x in Z, y in Z-{x}}) & (U in V) & (V-{U} /= 0)) ¥imp (EXISTS w in V-{U} | {U,w} in E). Proof: Suppose_not(v0,e0,v1,u0) ==> AUTO -- -- Suppose that $v0,e0$ is a graph endowed with at least two vertices $u0,w0$ and -- also endowed with a spanning tree $t0$. -- Use_def(HasSpanningTree) ==> Stat1: (EXISTS t | Is_tree(t) & (Un(t) = v0) & ((v0 = {arb(v0)}) or (t ¥incin e0))) Use_def(Un(t0)) ==> AUTO t0-->Stat1(*) ==> Stat2: (u0 in {y: x in t0, y in x}) & (v0 = {y: x in t0, y in x}) & (t0 ¥incin e0) & Stat2a: (not(EXISTS w in v0-{u0} | {u0,w} in e0)) (a0,y1)-->Stat2(*) ==> Stat3: (a0 in {{x,y}: x in v1, y in v1-{x}}) & (a0 in t0) & (u0 in a0) (x2,y2)-->Stat3(Stat3*) ==> (a0 = {x2,y2}) & (x2 /= y2) Suppose ==> Stat4: (x2 notin {y: x in t0, y in x}) or (y2 notin {y: x in t0, y in x}) (a0,x2,a0,y2)-->Stat4(Stat3*) ==> false Discharge ==> AUTO Suppose ==> u0 = x2 y2-->Stat2a(Stat2*) ==> false Discharge ==> u0 = y2 x2-->Stat2a(Stat2*) ==> false Discharge ==> QED -- -- Any vertex whose degree is less than $2$ in the spanning tree of a graph will be a non-cut vertex: -- namely, removing such a vertex along with the edges incident to it does not disrupt connectivity. -- Such a vertex must exist, as proved above, in view of the cycle-freeness of trees. -- Theorem connectivity_2: [Every graph endowed with a spanning tree has a non-cut vertex] (HasSpanningTree(V,E) & (E ¥incin {{x,y}: x in V, y in V-{x}}) & (V /= {arb(V)})) ¥imp (EXISTS u in V | HasSpanningTree( V-{u}, {a in E | u notin a} )). Proof: Suppose_not(v0,e0) ==> AUTO -- -- Suppose that $v0,e0$ is a graph endowed with more than one vertex, -- also endowed with a spanning tree $t0$, and -- such that no vertex can be removed from it without disrupting its connectivity. -- Use_def(HasSpanningTree) ==> Stat1: (EXISTS t | Is_tree(t) & (Un(t) = v0) & ((v0 = {arb(v0)}) or (t ¥incin e0))) & Stat1a: (not (EXISTS u in v0 | HasSpanningTree( v0-{u}, {a in e0 | u notin a} ))) & (v0 /= {arb(arb(t0))}) t0-->Stat1(*) ==> Is_tree(t0) & (Un(t0) = v0) & (t0 ¥incin e0) & (t0 ¥incin {{x,y}: x in v0, y in v0-{x}}) Suppose ==> Stat2: t0 ¥nincin {{x,y}: p in t0, x in p, y in p} p0-->Stat2(Stat1*) ==> Stat3: (p0 in {{x,y}: x in v0, y in v0-{x}}) & (p0 notin {{x,y}: p in t0, x in p, y in p}) & (p0 in t0) (x0,y0,p0,x0,y0)-->Stat3(Stat3*) ==> false Discharge ==> AUTO -- -- Suppose first that $t0$ consists of a sole edge. After observing that this edge must have -- two endpoints $x1,y1$, we see that removal of one endpoint---say $y1$ for specificity--- -- would lead to a spanning tree for the original graph deprived of the vertex in question. -- Since the reduced graph would retain connectivity, we must discard this case. -- Suppose ==> Stat4: t0 = {arb(t0)} (Stat4)ELEM ==> arb(t0) in t0 (arb(t0),t0)-->Tun_4(*) ==> Stat5: (v0 in {{x,y}: x in v0, y in v0-{x}}) & (v0 /= {arb(v0)}) (x1,y1)-->Stat5(Stat5) ==> Stat6: (v0 = {x1,y1}) & (x1 /= y1) y1-->Stat1a(Stat5*) ==> (not HasSpanningTree( v0-{y1}, {a in e0 | y1 notin a} )) & (v0-{y1} = {x1}) Suppose ==> Stat7: {a in e0 | y1 notin a} /= 0 a1-->Stat7(*) ==> Stat8: (a1 in {{x,y}: x in v0, y in v0 -{x}}) & (y1 notin a1) (x2,y2)-->Stat8(Stat8*) ==> Stat9: (x2 in v0) & (y2 in v0) & (x2 /= y2) & (y1 notin {x2,y2}) (Stat6,Stat9*)Discharge ==> {a in e0 | y1 notin a} = 0 Use_def(HasSpanningTree({x1},0)) ==> AUTO EQUAL(Stat5) ==> Stat10: not (EXISTS t | Is_tree(t) & (Un(t) = {x1}) & (({x1} = {arb({x1})}) or (t ¥incin 0))) {{x1}}-->Stat10(Stat10) ==> not (Is_tree({{x1}}) & (Un({{x1}}) = {x1})) {x1}-->Ttree_2(Stat10*) ==> Un({{x1}}) /= {x1} ({x1},{{x1}})-->Tun_4(Stat10*) ==> false Discharge ==> AUTO -- -- Knowing, now, that $t0$ consists of more than one edge, we are ensured by Theorem tree_1 -- that $t0$ has a vertex $u0$ whose removal from $t0$ leads to a sub-tree $t1$. We will -- show that $t1$ is a spanning tree for the original graph deprived of the vertex in question. -- t0-->Ttree_1(*) ==> Stat11: (EXISTS e in t0, u in e | ({a in t0 | u notin a} = t0-{e}) & Is_tree(t0-{e})) (a0,u0)-->Stat11(Stat11*) ==> (a0 in t0) & (u0 in a0) & ({a in t0 | u0 notin a} = t0-{a0}) & Is_tree(t0-{a0}) (t0,a0,t0)-->Tun_2(Stat11*) ==> u0 in Un(t0) u0-->Stat1a(Stat1*) ==> not HasSpanningTree( v0-{u0}, {a in e0 | u0 notin a} ) Use_def(HasSpanningTree)(Stat11) ==> Stat12: not (EXISTS t | Is_tree(t) & (Un(t) = v0-{u0}) & ((v0-{u0} = {arb(v0-{u0})}) or (t ¥incin {a in e0 | u0 notin a}))) Set_monot(Stat1) ==> {a in t0 | u0 notin a} ¥incin {a in e0 | u0 notin a} (t0-{a0})-->Stat12(Stat1*) ==> Stat13: (a0 in {{x,y}: x in v0, y in v0-{x}}) & (Un(t0-{a0}) /= v0-{u0}) (x3,y3)-->Stat13(Stat13*) ==> Stat14: (a0 ¥nincin {u0}) & (a0 = {x3,y3}) w0-->Stat14(Stat11*) ==> a0 = {u0,w0} (t0,u0,w0,a0)-->Ttree_4 ==> AUTO EQUAL(Stat1) ==> Un(t0-{a0}) = v0-{u0} (Stat12*)Discharge ==> QED -- -- -- \section{Representation of a graph by way of a membership digraph} -- -- -- Our initial plan was to develop with Referee the following representation THEORYs, -- in order to explain why one can work with membership as a convenient surrogate -- for the edge relationship of general graphs. Initially, we meant to insist on a -- weak form of extensionality. -- -- DISPLAY weaklyExtGraphRepr -- -- THEORY weaklyExtGraphRepr(v1,e0) -- (e0 ¥incin {{x,y}: x in v1, y in v1 | x /= y}) & Finite(v1) -- ==>(we_thryvar) -- ((v1 ¥PROD v1) incs we_thryvar) & Orientates(we_thryvar,v1,e0) -- Acyclic(v1,we_thryvar) -- WExtensional(v1,we_thryvar) -- END weaklyExtGraphRepr -- -- DISPLAY finMostowskiDecoration -- -- THEORY finMostowskiDecoration(v0,d0) -- ((v0 ¥PROD v0) incs d0) & (v0 /= 0) & Finite(v0) -- Acyclic(v0,d0) -- WExtensional(v0,d0) -- ==>(mski_thryvar) -- One_1_map(mski_thryvar) & ( domain(mski_thryvar) = v0 ) -- ( 0 in range(mski_thryvar) ) & (FORALL m in range(mski_thryvar) | Finite(m)) -- (FORALL w in domain(d0) | (mski_thryvar~[w]) = { (mski_thryvar~[cdr(p)]) : p in (d0 ¥ON {w}) }) -- (FORALL y, x | (y in v0) ¥imp (((mski_thryvar~[y]) in (mski_thryvar~[x])) ¥eq ([x,y] in d0))) -- END finMostowskiDecoration -- -- -- DISPLAY finiteGraphRepr -- -- THEORY finiteGraphRepr(v0,e0) -- (e0 ¥incin {{x,y}: x in v0, y in v0 | x /= y}) & Finite(v0) -- ==>(rho_thryvar,nu_thryvar) -- One_1_map(rho_thryvar) & ( domain(rho_thryvar) = v0 ) & ( range(rho_thryvar) = nu_thryvar ) -- (FORALL x in v0, y in v0 | ({x,y} in e0) ¥eq (((rho_thryvar~[x]) in (rho_thryvar~[y])) or ((rho_thryvar~[y]) in (rho_thryvar~[x])))) -- { x in nu_thryvar | x * nu_thryvar /= 0 } ¥incin pow( nu_thryvar ) -- END finiteGraphRepr -- -- \subsection{Weakly extensional, acyclic orientation of a graph whatsoever} -- -- It turned out to be doable, instead of (or preliminary to) developing the first -- of the three THEORYs just outlined, to prove via an inductive proof a single theorem -- of equipollent content, namely: -- Theorem xtensionalization_0: [Weakly extensional acyclic orientability of a finite nonvoid graph] (Finite(V) & (S in V)) ¥imp (EXISTS d | Orientates(d,V,E) & Acyclic(V,d) & WExtensional(V,d) & (S notin range(d))). Proof: Suppose_not(v2,s2,e0) ==> AUTO -- -- Arguing by contradiction, assume that there is a counterexample $v2,s2,e0$ to the claim. -- Then, thanks to the finiteness hypothesis, we can take a minimal counterexample $v1,s1,e0$. -- Suppose ==> Stat0: not(EXISTS s in v2 | not(EXISTS d | Orientates(d,v2,e0) & Acyclic(v2,d) & WExtensional(v2,d) & (s notin range(d)))) s2-->Stat0(*)==> false; Discharge ==> AUTO APPLY(fin_thryvar:v1) finiteInduction(s0->v2,P(V)->(EXISTS t in V | (not(EXISTS d | Orientates(d,V,e0) & Acyclic(V,d) & WExtensional(V,d) & (t notin range(d)))))) ==> Stat1: (FORALL V | (V ¥incin v1) ¥imp ( Finite(V) & ( (EXISTS t in V | (not(EXISTS d | Orientates(d,V,e0) & Acyclic(V,d) & WExtensional(V,d) & (t notin range(d))))) ¥eq (V = v1)) )) v1-->Stat1(Stat1*) ==> Stat2: (EXISTS t in v1 | (not(EXISTS d | Orientates(d,v1,e0) & Acyclic(v1,d) & WExtensional(v1,d) & (t notin range(d))))) s1-->Stat2(Stat2*) ==> Stat3: (not(EXISTS d | Orientates(d,v1,e0) & Acyclic(v1,d) & WExtensional(v1,d) & (s1 notin range(d)))) & (s1 in v1) -- -- Now consider the strict subset $v0=v1-{s1}$ of $v1$. -- Due to the minimality assumption, $v0,e0$ can be oriented in an acyclic and -- weakly extensional way, for any vertex $t in v0$, so that $t$ plays the role of a source. -- Loc_def ==> Stat4: v0 = v1-{s1} v0-->Stat1(Stat3*) ==> Stat5: not(EXISTS t in v0 | (not(EXISTS d | Orientates(d,v0,e0) & Acyclic(v0,d) & WExtensional(v0,d) & (t notin range(d))))) & (v1=v0+{s1}) -- -- Unless $s1$ is an isolated vertex, an acyclic and weakly extensional orientation of $v1-{s1}$ -- having as source a neighbor $t1$ of $s1$ exists, by the assumed minimality of $v1$. -- However, that orientation (conveniently restricted to the Cartesian square of the set of vertices) -- could trivially be extended to the overall graph $v1,e0$ so that $s1$ becomes the new source. -- This contradiction shows that $s1$ must be devoid of neighbors. -- Suppose ==> Stat6: {x in v0 | {s1,x} in e0} /= 0 t1-->Stat6(Stat6*) ==> Stat7: (t1 in v0) & ({t1,s1} in e0) t1-->Stat5(Stat5*) ==> Stat8: (EXISTS d | Orientates(d,(v0),e0) & Acyclic(v0,d) & WExtensional(v0,d) & (t1 notin range(d))) d2-->Stat8(Stat8*) ==> Orientates(d2,v0,e0) & Acyclic(v0,d2) & WExtensional(v0,d2) & (t1 notin range(d2)) Loc_def ==> (d0 = d2 * (v0 ¥PROD v0)) & (d1 = d0 + ({s1} ¥PROD {x in v0 | {s1,x} in e0})) Suppose ==> not(Orientates(d0,v0,e0) & Acyclic(v0,d0) & WExtensional(v0,d0) & (t1 notin range(d0))) (d2,v0,e0)-->Torientation2(Stat8*) ==> Orientates(d2*(v0 ¥PROD v0), v0, e0) (v0,d2)-->TweaXtensionality0(Stat8*) ==> WExtensional(v0,d2*(v0 ¥PROD v0)) EQUAL(Stat8) ==> Orientates(d0, v0, e0) & WExtensional(v0,d0) (v0,d2,v0,d0)-->Tacyclicity1 ==> AUTO (d2,d0,d2)-->Trange_1(Stat8*) ==> range(d0) ¥incin range(d2) (Stat8*)Discharge ==> AUTO (d0,v0,e0,v1,s1,d1)-->Torientation3(Stat3*) ==> Stat9: Orientates(d1,v1,e0) d1-->Stat3(Stat9*) ==> not(Acyclic(v1,d1) & WExtensional(v1,d1) & (s1 notin range(d1))) Suppose ==> (not Acyclic(v1,d1)) Suppose ==> Stat10: {x in v0 | {s1,x} in e0} ¥nincin v0 x1-->Stat10(Stat10*) ==> Stat11: (x1 in {x in v0 | {s1,x} in e0}) & (x1 notin v0) ()-->Stat11(Stat11*) ==> false Discharge ==> AUTO (v0,d0,s1,{x in v0 | {s1,x} in e0})-->Tacyclicity0(Stat4*) ==> Acyclic(v0+{s1},d0+({s1} ¥PROD {x in v0 | {s1,x} in e0})) EQUAL(Stat5) ==> false Discharge ==> AUTO Suppose ==> (not WExtensional(v1,d1)) Suppose ==> Stat12: t1 notin {x in v0 | {s1,x} in e0} t1-->Stat12(Stat7,Stat7*) ==> false; Discharge ==> AUTO Set_monot ==> {x in v0 | {s1,x} in e0} ¥incin {x in v0 | true} (v0,d0,d1,s1,{x in v0 | {s1,x} in e0},v1)-->TweaXtensionality2(Stat4*) ==> false Discharge ==> AUTO ({s1},{x in v0 | {s1,x} in e0})-->Tcartesian_1 ==> AUTO (d1,d0,{s1} ¥PROD {x in v0 | {s1,x} in e0})-->Trange_1(Stat4*) ==> (s1 in range(d0)) or (s1 in {x in v0 | {s1,x} in e0}) Suppose ==> Stat13: s1 in {x in v0 | {s1,x} in e0} ()-->Stat13(Stat4,Stat4*) ==> false; Discharge ==> s1 in range(d0) (v0,v0)-->Tcartesian_1 ==> AUTO (v0 ¥PROD v0,d0,v0 ¥PROD v0)-->Trange_1(Stat4*) ==> false Discharge ==> AUTO -- -- At this point we know that $s1$ is an isolated vertex. -- However, we will find a contradiction also in this case: -- any orientation for $v0$, in fact, works also as an orientation -- for $v1$ and, as such, has each isolated vertex of $v1$---in particular -- $s1$---as a source. Hence we will conclude that the claim of this -- theorem is true. -- Suppose ==> Stat14: v0 /= 0 -- -- The argument is split into two subcases depending on whether -- $v1$ has vertices different from $s1$ or $s1$ is the sole vertex. -- t2-->Stat14(Stat3*) ==> t2 in v0 t2-->Stat5(Stat5*) ==> Stat15: (EXISTS d | Orientates(d,v0,e0) & Acyclic(v0,d) & WExtensional(v0,d) & (t2 notin range(d))) d3-->Stat15(Stat15*) ==> Orientates(d3,v0,e0) & Acyclic(v0,d3) & WExtensional(v0,d3) (v0 ¥PROD v0,d3*(v0 ¥PROD v0),v0 ¥PROD v0)-->Trange_1 ==> AUTO (v0,v0)-->Tcartesian_1 ==> AUTO (d3,v0,e0)-->Torientation2(Stat5*) ==> Orientates(d3*(v0 ¥PROD v0), v0, e0) (d3*(v0 ¥PROD v0),v0,e0,v1,s1)-->Torientation4(Stat3*) ==> Orientates(d3*(v0 ¥PROD v0), v1, e0) (d3*(v0 ¥PROD v0))-->Stat3(Stat4*) ==> Stat16: not(Acyclic(v1,d3*(v0 ¥PROD v0)) & WExtensional(v1,d3*(v0 ¥PROD v0))) Suppose ==> not Acyclic(v1,d3*(v0 ¥PROD v0)) (v0,d3,v0,d3*(v0 ¥PROD v0))-->Tacyclicity1(Stat15*) ==> Acyclic(v0,d3*(v0 ¥PROD v0)) (v0,d3*(v0 ¥PROD v0),s1,0)-->Tacyclicity0(Stat4*) ==> Acyclic(v0+{s1},d3*(v0 ¥PROD v0)+({s1} ¥PROD 0)) {s1}-->Tcartesian_3(Stat16*) ==> d3*(v0 ¥PROD v0)+({s1} ¥PROD 0) = d3*(v0 ¥PROD v0) EQUAL(Stat5) ==> false Discharge ==> AUTO (v0,d3)-->TweaXtensionality0(Stat15*) ==> (not WExtensional(v1,d3*(v0 ¥PROD v0))) & WExtensional(v0,d3*(v0 ¥PROD v0)) (d3*(v0 ¥PROD v0),v1,e0,v0,s1)-->Torientation5(Stat3*) ==> s1 notin domain(d3*(v0 ¥PROD v0)) (v0,d3*(v0 ¥PROD v0),s1,v1)-->TweaXtensionality1(Stat3*) ==> false Discharge ==> AUTO 0-->Stat3(Stat3*) ==> Stat17: (v1={s1}) & (not(Orientates(0,v1,e0) & Acyclic(v1,0) & WExtensional(v1,0) & (s1 notin range(0)))) (v1,0)-->Textensionality0 ==> AUTO (v1,s1)-->Tvoidgraph1 ==> AUTO ({s1})-->Tvoidgraph2 ==> AUTO 0-->Trange_1(Stat17*) ==> s1 notin range(0) EQUAL(Stat17) ==> not(Orientates(0,{s1},e0) & (s1 notin range(0))) ({s1},s1,e0)-->Torientation1(Stat17*) ==> false Discharge ==> QED -- -- Theorem xtensionalization_1: ((W = V+{U}) & (U notin V) & Extensional(V,D) & (E ¥incin {{x,y}: x in Z, y in Z-{x}}) & (D ¥incin (V ¥PROD V)) & (Dp = D + ({U} ¥PROD {t in V | {U,t} in E}))) ¥imp ((Dp ¥incin (W ¥PROD W)) & ((not Extensional(W,Dp)) ¥imp (EXISTS x in V | (FORALL z | ([U,z] in Dp) ¥eq ([x,z] in D))))). Proof: Suppose_not(v1,v0,x0,d0,e2,v2,d1) ==> Stat0: (d1 = d0 + ({x0} ¥PROD {t in v0 | {x0,t} in e2})) & (not((d1 ¥incin (v1 ¥PROD v1)) & ((not Extensional(v1,d1)) ¥imp (EXISTS x in v0 | (FORALL z | ([x0,z] in d1) ¥eq ([x,z] in d0)))))) & (x0 in v1) & (v0 = v1-{x0}) & (e2 ¥incin {{x,y}: x in v2, y in v2-{x}}) & Extensional(v0,d0) & (d0 ¥incin (v0 ¥PROD v0)) Set_monot ==> {t in v0 | true} incs {t in v0 | {x0,t} in e2} (Stat0*)ELEM ==> Stat2: (v1 = v0 + {x0}) & (v0 incs {t in v0 | {x0,t} in e2}) Suppose ==> d1 ¥nincin (v1 ¥PROD v1) (v0,v1,v0,v1)-->Tcartesian_5(Stat0*) ==> ({x0} ¥PROD {t in v0 | {x0,t} in e2}) ¥nincin (v1 ¥PROD v1) ({x0},v1,{t in v0 | {x0,t} in e2},v1)-->Tcartesian_5(Stat0*) ==> false Discharge ==> AUTO (Stat0*)ELEM ==> Stat99: (not(EXISTS x in v0 | (FORALL z | ([x0,z] in d1) ¥eq ([x,z] in d0)))) & (not Extensional(v1,d1)) Use_def(Extensional) ==> Stat15: (not(FORALL x in v1, y in v1 | (EXISTS z | (([x,z] in d1) ¥eq ([y,z] in d1)) ¥imp (x = y)))) & Stat15a: (FORALL x in v0, y in v0 | (EXISTS z | (([x,z] in d0) ¥eq ([y,z] in d0)) ¥imp (x = y))) (x2,y2,x2,y2)-->Stat15(Stat15*) ==> Stat16: (not(EXISTS z | (([x2,z] in d1) ¥eq ([y2,z] in d1)) ¥imp (x2 = y2))) & (x2 in v1) & (y2 in v1) Suppose ==> Stat17: x0 notin {x2,y2} (x2,y2)-->Stat15a(Stat16,Stat17,Stat2*) ==> Stat18: (EXISTS z | (([x2,z] in d0) ¥eq ([y2,z] in d0)) ¥imp (x2 = y2)) & (not(EXISTS z | (([x2,z] in d1) ¥eq ([y2,z] in d1)) ¥imp (x2 = y2))) (z2,z2)-->Stat18(Stat18*) ==> (x2 /= y2) & (([x2,z2] in d0) ¥neq ([y2,z2] in d0)) & (([x2,z2] in d1) ¥eq ([y2,z2] in d1)) Suppose ==> (([x2,z2] in d0) ¥eq ([x2,z2] in d1)) & (([y2,z2] in d0) ¥eq ([y2,z2] in d1)) EQUAL(Stat18) ==> false; Discharge ==> AUTO ([x2,z2],{x0},{t in v0 | {x0,t} in e2})-->Tcartesian_0(Stat17*) ==> [x2,z2] notin ({x0} ¥PROD {t in v0 | {x0,t} in e2}) ([y2,z2],{x0},{t in v0 | {x0,t} in e2})-->Tcartesian_0(Stat17*) ==> [y2,z2] notin ({x0} ¥PROD {t in v0 | {x0,t} in e2}) (Stat0*)Discharge ==> AUTO Loc_def ==> x1 = if (x0 = x2) then y2 else x2 end if 0-->Stat16(Stat16*) ==> Stat19: x1 in (v1-{x0}) Suppose ==> Stat20: not(FORALL z | ([x0,z] in d1) ¥eq ([x1,z] in d0)) z1-->Stat20(Stat20*) ==> ([x0,z1] in d1) ¥neq ([x1,z1] in d0) (Stat16*)ELEM ==> (x0 /= x1) & ({x0,x1} = {x2,y2}) z1-->Stat16(Stat20*) ==> ([x2,z1] in d1) ¥eq ([y2,z1] in d1) Suppose ==> Stat21: not(([x1,z1] in d1) ¥eq ([x1,z1] in d0)) (Stat0,Stat21*)ELEM ==> [x1,z1] in ({x0} ¥PROD {t in v0 | {x0,t} in e2}) ([x1,z1],{x0},{t in v0 | {x0,t} in e2})-->Tcartesian_0(Stat20*) ==> false Discharge ==> AUTO Suppose ==> (x0 = x2) & (x1 = y2) EQUAL(Stat20) ==> false Discharge ==> AUTO (Stat20*)ELEM ==> (x0 = y2) & (x1 = x2) EQUAL(Stat20) ==> false Discharge ==> AUTO x1-->Stat99(Stat19,Stat2*) ==> not (FORALL z | ([x0,z] in d1) ¥eq ([x1,z] in d0)) (Stat19*)Discharge ==> QED -- -- Theorem xtensionalization_2: [Preservation of acyclicity and extensionality under adjunction of an inner vertex] ((W = V+{U}) & (U notin V) & (S in V) & ({y in V | [S,y] in D} = 0) & (S in {t in W | {U,t} in E}) & (E ¥incin {{x,y}: x in Z, y in Z-{x}}) & Orientates(D,V,E) & Acyclic(V,D) & Extensional(V,D) & (D ¥incin (V ¥PROD V))) ¥imp (EXISTS d ¥incin (W ¥PROD W) | Orientates(d,W,E) & Acyclic(W,d) & Extensional(W,d)). Proof: Suppose_not(v1,v0,u0,s0,d0,e2,v2) ==> Stat0: (not(EXISTS d ¥incin (v1 ¥PROD v1) | Orientates(d,v1,e2) & Acyclic(v1,d) & Extensional(v1,d))) & (u0 in v1) & (v0 = v1-{u0}) & (s0 in v0) & ({y in v0 | [s0,y] in d0} = 0) & (s0 in {t in v1 | {u0,t} in e2}) & (e2 ¥incin {{x,y}: x in v2, y in v2-{x}}) & Orientates(d0,v0,e2) & Acyclic(v0,d0) & Extensional(v0,d0) & (d0 ¥incin (v0 ¥PROD v0)) Suppose ==> {u0,u0} in e2 (Stat0*)ELEM ==> Stat1: {u0,u0} in {{x,y}: x in v2, y in v2-{x}} (x1,y1)-->Stat1(Stat1*) ==> false Discharge ==> Stat2: {u0,u0} notin e2 -- -- Orient the edges incident to $u0$ as in-coming to $u0$. -- The neighbors of $u0$ through $e2$ are ${t in v1 | {u0,t} in e2}$. -- Suppose ==> Stat3: v0 ¥nincs {t in v1 | {u0,t} in e2} x2-->Stat3(Stat3*) ==> Stat4: (x2 in {t in v1 | {u0,t} in e2}) & (x2 notin v0) ()-->Stat4(Stat4,Stat0,Stat2*) ==> false Discharge ==> AUTO Suppose ==> Stat5: not(EXISTS t in {t in v1 | {u0,t} in e2} | (d0 ¥ON {t}) = 0) s0-->Stat5(Stat0*) ==> Stat6: ((d0 ¥ON {s0}) /= 0) & ({y in v0 | [s0,y] in d0} = 0) & (d0 ¥incin (v0 ¥PROD v0)) Use_def(¥ON)(Stat6) ==> (d0 ¥ON {s0}) = {p in d0 | car(p) in {s0}} p0-->Stat6(Stat6*) ==> Stat7: p0 in {p in d0 | car(p) in {s0}} (p0,v0,v0)-->Tcartesian_0 ==> AUTO ()-->Stat7(Stat6*) ==> Stat8: (cdr(p0) notin {y in v0 | [s0,y] in d0}) & (p0 in d0) & (p0 = [car(p0),cdr(p0)]) & (car(p0) = s0) & (cdr(p0) in v0) (cdr(p0))-->Stat8(Stat8) ==> false Discharge ==> AUTO (v0,d0,u0,{t in v1 | {u0,t} in e2})-->Tacyclicity6(Stat0*) ==> Stat9: Acyclic(v0+{u0}, d0+({t in v1 | {u0,t} in e2} ¥PROD {u0})) & (v1 = v0+{u0}) (v0,d0,u0,{t in v1 | {u0,t} in e2})-->Textensionality1(Stat0*) ==> Extensional(v0+{u0}, d0+({t in v1 | {u0,t} in e2} ¥PROD {u0})) Suppose ==> not Orientates(d0+({t in v1 | {u0,t} in e2} ¥PROD {u0}),v1,e2) Use_def(Orientates) ==> Stat10: ((e2 * {{x,y}: x in v1, y in (v1-{x})}) /= {{car(p),cdr(p)}: p in (d0+({t in v1 | {u0,t} in e2} ¥PROD {u0})) | p = [car(p), cdr(p)]}) & ((e2 * {{x,y}: x in v0, y in (v0-{x})}) = {{car(p),cdr(p)}: p in d0 | p = [car(p), cdr(p)]}) Set_monot(Stat10) ==> ({{car(p),cdr(p)}: p in d0 | p = [car(p), cdr(p)]} ¥incin {{car(p),cdr(p)}: p in (d0+({t in v1 | {u0,t} in e2} ¥PROD {u0})) | p = [car(p), cdr(p)]}) Suppose ==> ({{x,y}: x in v1, y in (v1-{x})} ¥nincs {{x,y}: x in v0, y in (v0-{x})}) EQUAL ==> Stat11: ({{x,y}: x in v1, y in (v1-{x})} ¥nincs {{x,y}: x in v1-{u0}, y in (v1-{u0}-{x})}) q2-->Stat11(Stat11*) ==> Stat12: (q2 in {{x,y}: x in v1-{u0}, y in (v1-{u0}-{x})}) & (q2 notin {{x,y}: x in v1, y in (v1-{x})}) (x3,y3,x3,y3)-->Stat12(Stat12*) ==> false Discharge ==> AUTO q1-->Stat10(Stat10*) ==> Stat13: (q1 notin {{car(p),cdr(p)}: p in d0 | p = [car(p), cdr(p)]}) & (q1 notin (e2 * {{x,y}: x in v0, y in (v0-{x})})) & ((q1 in (e2 * {{x,y}: x in v1, y in (v1-{x})})) ¥neq (q1 in {{car(p),cdr(p)}: p in (d0+({t in v1 | {u0,t} in e2} ¥PROD {u0})) | p = [car(p), cdr(p)]})) Suppose ==> Stat14: q1 in {{car(p),cdr(p)}: p in (d0+({t in v1 | {u0,t} in e2} ¥PROD {u0})) | p = [car(p),cdr(p)]} p1-->Stat14(Stat13*) ==> Stat15: ({car(p1),cdr(p1)} notin {{car(p),cdr(p)}: p in d0 | p = [car(p), cdr(p)]}) & (p1 in (d0+({t in v1 | {u0,t} in e2} ¥PROD {u0}))) & (p1 = [car(p1), cdr(p1)]) & (q1 = {car(p1),cdr(p1)}) p1-->Stat15(Stat15*) ==> p1 in ({t in v1 | {u0,t} in e2} ¥PROD {u0}) (p1,{t in v1 | {u0,t} in e2},{u0})-->Tcartesian_0(Stat15*) ==> Stat16: (car(p1) in {t in v1 | {u0,t} in e2}) & (cdr(p1) = u0) ()-->Stat16(Stat13*) ==> Stat17: ({car(p1),u0} notin {{x,y}: x in v1, y in (v1-{x})}) & (car(p1) in v1) & ({car(p1),u0} in e2) (car(p1),u0)-->Stat17(Stat17,Stat9,Stat2*) ==> false (Stat17*)Discharge ==> Stat18: (q1 in {{x,y}: x in v1, y in (v1-{x})}) & (q1 notin {{x,y}: x in v0, y in (v0-{x})}) & Stat18a: (q1 notin {{car(p),cdr(p)}: p in (d0+({t in v1 | {u0,t} in e2} ¥PROD {u0})) | p = [car(p), cdr(p)]}) & (q1 in e2) (x4,y4,x4,y4,[x4,y4])-->Stat18(Stat18,Stat9*) ==> Stat19: ([x4,y4] notin ({t in v1 | {u0,t} in e2} ¥PROD {u0})) & (q1 = {x4,y4}) & (x4 /= y4) & (u0 in q1) & (x4 in v1) & (y4 in v1) Suppose ==> y4 = u0 ([x4,y4],{t in v1 | {u0,t} in e2},{u0})-->Tcartesian_0(Stat19*) ==> Stat20: x4 notin {t in v1 | {u0,t} in e2} x4-->Stat20(Stat18*) ==> false (Stat20*)Discharge ==> AUTO [y4,x4]-->Stat18a(Stat18*) ==> [y4,x4] notin ({t in v1 | {u0,t} in e2} ¥PROD {u0}) ([y4,x4],{t in v1 | {u0,t} in e2},{u0})-->Tcartesian_0(Stat19*) ==> Stat21: y4 notin {t in v1 | {u0,t} in e2} y4-->Stat21(Stat18*) ==> false Discharge ==> AUTO Loc_def ==> Stat22: d1 = d0 + ({t in v1 | {u0,t} in e2} ¥PROD {u0}) EQUAL(Stat9) ==> Orientates(d1,v1,e2) & Acyclic(v1, d1) & Extensional(v1, d1) d1-->Stat0(Stat22*) ==> (d0 + ({t in v1 | {u0,t} in e2} ¥PROD {u0})) ¥nincin (v1 ¥PROD v1) (v0,v1,v0,v1)-->Tcartesian_5(Stat0*) ==> ({t in v1 | {u0,t} in e2} ¥PROD {u0}) ¥nincin (v1 ¥PROD v1) Set_monot(Stat22) ==> Stat23: {t in v1 | {u0,t} in e2} ¥incin {t in v1 | true} ({t in v1 | {u0,t} in e2},v1,{u0},v1)-->Tcartesian_5(Stat0*) ==> {t in v1 | {u0,t} in e2} ¥nincin v1 (Stat23*)Discharge ==> QED -- -- \subsection{Injective decoration of a weakly extensional and acyclic digraph} -- -- -- An outline of the construction needed for a decoration a` la Mostowski is as follows: -- \begin{itemize} -- \item Send every sink $w$ but one (because we must send one sink to $0$) to the set, ${{v0}+(v0-{w})}$, -- whose rank is $2$ bigger than the rank of $v0$ and whose cardinality equals the cardinality of $v0$. -- \item Extend $mski_thryvar$ consistently with the desideratum. -- \item Injectivity will follow from the fact that no two vertices have the same immediate successors, -- save for the sinks, which can neither collide with one another -- (because their images are, plainly, pairwise distinct) nor with internal nodes -- (because they differ from them for rank---as well as for cardinality). -- \end{itemize} -- THEORY finMostowskiDecoration(v0,d0) ((v0 ¥PROD v0) incs d0) & (v0 /= 0) & Finite(v0) Acyclic(v0,d0) WExtensional(v0,d0) END finMostowskiDecoration -- ENTER_THEORY finMostowskiDecoration -- Theorem finMostowskiDecoration0: [Trivial inclusions between edge endpoints and vertices] Is_map(d0) & (domain(d0) ¥incin v0) & (range(d0) ¥incin v0) & (FORALL x in domain(d0), y in domain(d0) | (EXISTS z | (([x,z] in d0) ¥eq ([y,z] in d0)) ¥imp (x = y))). Proof: Suppose_not() ==> AUTO Assump ==> (d0*(v0 ¥PROD v0) = d0) & (v0 /= 0) & WExtensional(v0,d0) (v0 ¥PROD v0,d0,v0 ¥PROD v0)-->Trange_1 ==> AUTO (v0,v0)-->Tcartesian_1 ==> AUTO (v0 ¥PROD v0,d0,v0 ¥PROD v0)-->Tdomain_1 ==> AUTO (v0,v0)-->Tcartesian_2 ==> AUTO Use_def(WExtensional(v0,d0)) ==> AUTO Use_def(Extensional(domain(d0),d0)) ==> AUTO ELEM ==> v0*domain(d0) = domain(d0) EQUAL ==> (FORALL x in domain(d0), y in domain(d0) | (EXISTS z | (([x,z] in d0) ¥eq ([y,z] in d0)) ¥imp (x = y))) (d0,v0,v0)-->Tcartesian_6 ==> AUTO Discharge ==> QED -- Theorem finMostowskiDecoration1: [No self-loops in an acyclic digraph] W notin range(d0 ¥ON {W}). Proof: Suppose_not(w0) ==> AUTO Use_def(range(d0 ¥ON {w0})) ==> AUTO Use_def(¥ON) ==> w0 in {cdr(q): q in {p in d0 | car(p) in {w0}}} SIMPLF ==> Stat2: w0 in {cdr(p): p in d0 | car(p) in {w0}} p0-->Stat2(Stat2*) ==> (p0 in d0) & (car(p0) = cdr(p0)) Assump ==> Acyclic(v0,d0) & ((v0 ¥PROD v0) incs d0) (v0,d0,cdr(p0),car(p0))-->Tacyclicity2(Stat2*) ==> Stat3: not((car(p0) in v0) & ([car(p0),cdr(p0)] in d0)) Suppose ==> car(p0) notin v0 Use_def(domain(d0)) ==> AUTO ()-->TfinMostowskiDecoration0(Stat3*) ==> Stat4: car(p0) notin {car(p): p in d0} p0-->Stat4(Stat2*) ==> false Discharge ==> AUTO (p0,v0,v0)-->Tcartesian_0(Stat2*) ==> false Discharge ==> QED -- -- The following function assigns $0$ to every set which is not a sink of the current graph; also a designated sink -- is assigned the image $0$. Special non-zero sets are assigned to the sinks other than the designated one. -- Def finMostowskiDecoration1: [Non-recursive part of labeling, used to enforce one-oneness] lbl(W) := if (W in domain(d0)+{arb(v0-domain(d0))}) then 0 else {{v0}+(v0-{W})} end if -- APPLY(lab_thryvar:mski_thryvar) finAcycLabeling(v0->v0,d0->d0,h(s,x)->(s+lbl(x))) ==> Theorem finMostowskiDecoration2a: (Svm(mski_thryvar) & (domain(mski_thryvar) = v0) & (FORALL x in v0 | (mski_thryvar~[x]) = ({(mski_thryvar~[cdr(p)]): p in (d0 ¥ON {x}) | cdr(p) in v0}+lbl(x)))) -- Theorem finMostowskiDecoration2: Svm(mski_thryvar) & (domain(mski_thryvar) = v0). Proof: Suppose_not() ==> AUTO ()-->TfinMostowskiDecoration2a ==> false Discharge ==> QED -- -- -- Theorem finMostowskiDecoration3: [Images of internal vertices under Mostowski's decoration] (W in domain(d0)) ¥imp (((mski_thryvar~[W]) = { mski_thryvar~[cdr(p)] : p in (d0 ¥ON {W}) }) & ((mski_thryvar~[W]) /= 0)). Proof: Suppose_not(w0) ==> AUTO Suppose ==> (mski_thryvar~[w0]) /= ({mski_thryvar~[cdr(p)]: p in (d0 ¥ON {w0})}+lbl(w0)) ()-->TfinMostowskiDecoration2a(*) ==> Stat1: (FORALL x in v0 | (mski_thryvar~[x]) = ({(mski_thryvar~[cdr(p)]): p in (d0 ¥ON {x}) | cdr(p) in v0}+lbl(x))) ()-->TfinMostowskiDecoration0(*) ==> domain(d0) ¥incin v0 w0-->Stat1(*) ==> Stat2: {(mski_thryvar~[cdr(p)]): p in (d0 ¥ON {w0}) | cdr(p) in v0} /= { mski_thryvar~[cdr(p)] : p in (d0 ¥ON {w0}) } p0-->Stat2(Stat2*) ==> (p0 in (d0 ¥ON {w0})) & (cdr(p0) notin v0) Use_def(¥ON) ==> Stat3: p0 in {p in d0 | car(p) in {w0}} Assump ==> (v0 ¥PROD v0) incs d0 ()-->Stat3(Stat3*) ==> Stat4: p0 in (v0 ¥PROD v0) (p0,v0,v0)-->Tcartesian_0(Stat4*) ==> cdr(p0) in v0 (Stat2*)Discharge ==> AUTO Use_def(lbl) ==> (mski_thryvar~[w0]) = { mski_thryvar~[cdr(p)] : p in (d0 ¥ON {w0}) } Use_def(domain) ==> Stat6: (w0 in {car(p): p in d0}) & ({ mski_thryvar~[cdr(p)] : p in (d0 ¥ON {w0}) } = 0) Use_def(¥ON) ==> (d0 ¥ON {w0}) = {p in d0 | car(p) in {w0}} (p1,p1)-->Stat6(Stat6*) ==> Stat7: (p1 notin {p in d0 | car(p) in {w0}}) & (w0 = car(p1)) & (p1 in d0) p1-->Stat7(Stat7*) ==> false Discharge ==> QED -- Theorem finMostowskiDecoration4: [Images of sinks under Mostowski's decoration] (W in v0-domain(d0)) ¥imp (((mski_thryvar~[W]) = lbl(W)) & ((mski_thryvar~[W]) notin ({{v0} + (v0-{0})}))). Proof: Suppose_not(w0) ==> AUTO Suppose ==> (mski_thryvar~[w0]) /= lbl(w0) ()-->TfinMostowskiDecoration2a ==> Stat0: (FORALL x in v0 | (mski_thryvar~[x]) = ({(mski_thryvar~[cdr(p)]): p in (d0 ¥ON {x}) | cdr(p) in v0}+lbl(x))) w0-->Stat0(*) ==> Stat1: {mski_thryvar~[cdr(p)]: p in (d0 ¥ON {w0})| cdr(p) in v0} /= 0 Use_def(¥ON) ==> (d0 ¥ON {w0}) = {p in d0 | car(p) in {w0}} Use_def(domain(d0)) ==> AUTO p0-->Stat1(*) ==> Stat2: (p0 in {p: p in d0 | car(p) in {w0}}) & (w0 notin {car(q): q in d0}) (p1,p1)-->Stat2(Stat2*) ==> false Discharge ==> AUTO -- -- Recall: -- $lbl(W) = if (W in domain(d0)+{arb(v0-domain(d0))}) then 0 else {{v0}+(v0-{W})} end if$ -- Assump ==> v0 /= 0 Use_def(lbl) ==> false Discharge ==> QED -- -- Theorem finMostowskiDecoration5: [One image under Mostowski's decoration is null] 0 in range(mski_thryvar). Proof: -- In fact from $v0/=0$, after putting $a0=arb(v0-domain(d0))$, we will get $a0 in v0$, $lbl(a0)=0$, $(mski_thryvar~[a0]) = 0$. Suppose_not() ==> AUTO Use_def(lbl) ==> lbl(arb(v0-domain(d0))) = 0 Loc_def ==> a0 = arb(v0-domain(d0)) EQUAL ==> lbl(a0) = 0 Use_def(domain(d0)) ==> AUTO Suppose ==> v0 ¥incin domain(d0) Assump ==> Acyclic(v0,d0) & Finite(v0) & (v0 /= 0) & ((v0 ¥PROD v0) incs d0) (v0,d0)-->Tacyclicity4(*) ==> Stat1: (EXISTS w in v0, s in v0 | 0 = {y in v0 | ([w,y] in d0) or ([y,s] in d0)}) (w0,s0)-->Stat1(*) ==> Stat2: (w0 in {car(p): p in d0}) & ({y in v0 | ([w0,y] in d0) or ([y,s0] in d0)} = 0) (p0,cdr(p0))-->Stat2(Stat2*) ==> (w0 = car(p0)) & (p0 in d0) & ((cdr(p0) notin v0) or ([w0,cdr(p0)] notin d0)) EQUAL(Stat2) ==> (p0 in d0) & ((cdr(p0) notin v0) or ([car(p0),cdr(p0)] notin d0)) ()-->TfinMostowskiDecoration0(*) ==> range(d0) ¥incin v0 Use_def(range(d0)) ==> AUTO (p0,v0,v0)-->Tcartesian_0(*) ==> Stat3: cdr(p0) notin {cdr(p): p in d0} p0-->Stat3(Stat2*) ==> false Discharge ==> Stat4: (a0 in v0) & (a0 notin domain(d0)) a0-->TfinMostowskiDecoration4(*) ==> mski_thryvar~[a0] = 0 Use_def(range) ==> Stat7: mski_thryvar~[a0] notin {cdr(p): p in mski_thryvar} ([a0,mski_thryvar~[a0]])-->Stat7(Stat7) ==> [a0,mski_thryvar~[a0]] notin mski_thryvar (mski_thryvar)-->Timage_5 ==> AUTO ()-->TfinMostowskiDecoration2(Stat4*) ==> Stat8: ([a0,mski_thryvar~[a0]] notin {[x,mski_thryvar~[x]]: x in domain(mski_thryvar)}) & (a0 in domain(mski_thryvar)) a0-->Stat8(Stat8*) ==> false Discharge ==> QED -- Theorem finMostowskiDecoration6: [Finiteness of each image of Mostowski's decoration] (Y in range(mski_thryvar)) ¥imp Finite(Y). Proof: Suppose_not(y0) ==> AUTO -- -- In fact, each $lbl(w)$ is either $0$ or has as many elements as $v0$, which we have supposed to be finite; -- moreover, each ${(mski_thryvar~[cdr(p)]): p in (d0 ¥ON {x}) | cdr(p) in v0}$ with $x in v0$ has fewer elements than $v0$; -- consequently each $mski_thryvar~[x]$ with $x in v0$ must be finite, because it results from the union of two finite sets. -- Use_def(range(mski_thryvar)) ==> AUTO EQUAL ==> Stat1: (y0 in {cdr(p): p in mski_thryvar}) & (not Finite(y0)) p0-->Stat1(Stat1*) ==> (p0 in mski_thryvar) & (y0 = cdr(p0)) ()-->TfinMostowskiDecoration2a(*) ==> Stat2: (FORALL x in v0 | (mski_thryvar~[x]) = ({(mski_thryvar~[cdr(p)]): p in (d0 ¥ON {x}) | cdr(p) in v0}+lbl(x))) & Svm(mski_thryvar) & (domain(mski_thryvar) = v0) mski_thryvar-->Timage_5(*) ==> Stat3: p0 in {[x,mski_thryvar~[x]]: x in domain(mski_thryvar)} x0-->Stat3(Stat2*) ==> (x0 in v0) & (p0=[x0,mski_thryvar~[x0]]) x0-->Stat2(Stat3*) ==> mski_thryvar~[x0] = {(mski_thryvar~[cdr(p)]): p in (d0 ¥ON {x0}) | cdr(p) in v0}+lbl(x0) TELEM ==> (car([x0,mski_thryvar~[x0]]) = x0) & (cdr([x0,mski_thryvar~[x0]]) = mski_thryvar~[x0]) EQUAL(Stat1) ==> Stat4: not Finite( {(mski_thryvar~[cdr(p)]): p in (d0 ¥ON {x0}) | cdr(p) in v0}+lbl(x0) ) Suppose ==> Finite({(mski_thryvar~[cdr(p)]): p in (d0 ¥ON {x0}) | cdr(p) in v0}) Use_def(lbl) ==> Stat5: lbl(x0) = if (x0 in domain(d0)+{arb(v0-domain(d0))}) then 0 else {{v0}+(v0-{x0})} end if Suppose ==> x0 in domain(d0)+{arb(v0-domain(d0))} (Stat5*)ELEM ==> {(mski_thryvar~[cdr(p)]): p in (d0 ¥ON {x0}) | cdr(p) in v0}+lbl(x0) = {(mski_thryvar~[cdr(p)]): p in (d0 ¥ON {x0}) | cdr(p) in v0} EQUAL(Stat4) ==> false Discharge ==> AUTO (Stat5*)ELEM ==> lbl(x0) = {{v0}+(v0-{x0})} ({(mski_thryvar~[cdr(p)]): p in (d0 ¥ON {x0}) | cdr(p) in v0},{v0}+(v0-{x0}))-->Tfin_1(Stat4*) ==> Finite({(mski_thryvar~[cdr(p)]): p in (d0 ¥ON {x0}) | cdr(p) in v0}+{{v0}+(v0-{x0})}) EQUAL(Stat4) ==> false Discharge ==> AUTO Assump ==> ((v0 ¥PROD v0) incs d0) & Finite(v0) Suppose ==> (d0 ¥ON {x0}) ¥nincin {[x0,y]: y in v0} Use_def(¥ON) ==> Stat6: {p in d0 | car(p) in {x0}} ¥nincin {[x0,y]: y in v0} p1-->Stat6(Stat6*) ==> Stat7: (p1 in {p in d0 | car(p) in {x0}}) & Stat7a: (p1 notin {[x0,y]: y in v0}) ()-->Stat7(Stat4*) ==> Stat8: (p1 in (v0 ¥PROD v0)) & (car(p1) = x0) (p1,v0,v0)-->Tcartesian_0(Stat8) ==> (p1 = [x0,cdr(p1)]) & (cdr(p1) in v0) (cdr(p1))-->Stat7a(Stat8*) ==> false Discharge ==> AUTO APPLY() finiteImage(s0->v0,f(X)->([x0,X])) ==> Finite({[x0,y]: y in v0}) ({[x0,y]: y in v0},d0 ¥ON {x0})-->Tfin_0(Stat4*) ==> Finite(d0 ¥ON {x0}) APPLY() finiteImage(s0->(d0 ¥ON {x0}),f(X)->(mski_thryvar~[cdr(X)])) ==> Finite({(mski_thryvar~[cdr(p)]): p in (d0 ¥ON {x0})}) Set_monot ==> {(mski_thryvar~[cdr(p)]): p in (d0 ¥ON {x0}) | cdr(p) in v0} ¥incin {(mski_thryvar~[cdr(p)]): p in (d0 ¥ON {x0})} ({(mski_thryvar~[cdr(p)]): p in (d0 ¥ON {x0})},{(mski_thryvar~[cdr(p)]): p in (d0 ¥ON {x0}) | cdr(p) in v0})-->Tfin_0(Stat4*) ==> false Discharge ==> QED -- -- -- Theorem finMostowskiDecoration7: [Under Mostowski's decoration, no image belongs to the image of a sink] (({X,Y} ¥incin v0) & ((mski_thryvar~[Y]) in (mski_thryvar~[X]))) ¥imp (X in domain(d0)). Proof+: Suppose_not(w0,w1) ==> AUTO -- -- Arguing by contradiction, assume that $w0,w1$ is a counterexample; -- then $w0$ must be a sink, but $w1$ must not, else we would readily get a contradiction. -- Use_def(lbl(w0)) ==> AUTO w0-->TfinMostowskiDecoration4(*) ==> Stat0: (w1 in v0) & ((mski_thryvar~[w1]) = ({v0}+(v0-{w0}))) Suppose ==> w1 notin domain(d0) w1-->TfinMostowskiDecoration4(Stat0*) ==> lbl(w1) = ({v0}+(v0-{w0})) Use_def(lbl(w1)) ==> AUTO (Stat0*)Discharge ==> AUTO -- -- Hence suppose that $w1$, unlike $w0$, is not a sink. Can then $lbl(w0) = (mski_thryvar~[w1])$ hold? -- If this were the case, then -- ${ (mski_thryvar~[cdr(p)]) : p in (d0 ¥ON {w1}) } = {{v0}+(v0-{w0})}$. -- w1-->TfinMostowskiDecoration3(*) ==> Stat1: ({ mski_thryvar~[cdr(p)] : p in (d0 ¥ON {w1}) } = {v0}+(v0-{w0})) & (w1 in domain(d0)) Loc_def ==> h0 = {[y,mski_thryvar~[y]]: y in range(d0 ¥ON {w1})} -- -- The following TELEM step makes implicit use of the THEORY $isSvm$ seen at the beginning of this scenario. -- TELEM ==> Svm({[y,mski_thryvar~[y]]: y in range(d0 ¥ON {w1})}) & (range({[y,mski_thryvar~[y]]: y in range(d0 ¥ON {w1})}) = {(mski_thryvar~[y]): y in range(d0 ¥ON {w1})}) & (domain({[y,mski_thryvar~[y]]: y in range(d0 ¥ON {w1})}) = range(d0 ¥ON {w1})) -- -- The intuitive idea is that since $range(d0 ¥ON {w1})$ is a proper subset of $v0$ -- (in fact $w1 notin range(d0 ¥ON {w1})$) and ${v0}+(v0-{w0})$ has the same cardinality as $v0$, -- the surjectivity of $h0$ is untenable in view of the finiteness of $v0$. -- Use_def(range(d0 ¥ON {w1})) ==> AUTO SIMPLF ==> {(mski_thryvar~[y]): y in {cdr(p): p in (d0 ¥ON {w1})}} = {(mski_thryvar~[cdr(p)]): p in (d0 ¥ON {w1})} Assump ==> Finite(v0) & Acyclic(v0,d0) & (v0 /= 0) & ((v0 ¥PROD v0) incs d0) Suppose ==> range(d0 ¥ON {w1}) ¥nincin v0 Use_def(¥ON) ==> {cdr(p): p in {q in d0 | car(q) in {w1} }} ¥nincin v0 Set_monot ==> {cdr(q): q in d0 | car(q) in {w1}} ¥incin {cdr(q): q in (v0 ¥PROD v0)} Use_def(¥PROD) ==> {cdr(q): q in d0 | car(q) in {w1}} ¥incin {cdr(q): q in {[x,y]: x in v0, y in v0}} SIMPLF ==> Stat2: {cdr([x,y]): x in v0, y in v0} ¥nincin v0 y1-->Stat2(Stat2*) ==> Stat2a: (y1 in {cdr([x,y]): x in v0, y in v0}) & (y1 notin v0) (xp,yp)-->Stat2a(Stat2a*) ==> false Discharge ==> Stat3: range(d0 ¥ON {w1}) ¥incin v0 EQUAL(Stat1) ==> Stat5: Svm(h0) & (range(h0) = {v0}+(v0-{w0})) & (domain(h0) ¥incin v0) & Finite(h0) -- -- However, since we have not developed a rich enough theory of cardinals within this scenario, -- we prefer to formalize the argument-by-contradiction outlined above in more direct, -- albeit slightly less intuitive, terms. -- We easily discard the case when $w0 notin domain(h0)$: in this case -- $domain(h0) ¥incin range(h0)$ and we can resort to Theorem $part_whole_1$ -- to get $range(h0)=domain(h0)$; but this conflicts with $v0 in range(h0)$ and -- $domain(h0) ¥incin v0$. -- -- h0-->Tpart_whole_0(Stat1) ==> Stat5: Finite(h0) Use_def(domain(h0)) ==> AUTO -- h0-->Tpart_whole_1(Stat3) ==> Stat6: w0 in {car(p): p in h0} h0-->Tpart_whole_1(Stat3*) ==> Stat6: w0 in {car(p): p in h0} -- -- On the other hand, if $w0 in domain(h0)$ then we can retouch $h0$ by replacing -- its pair $[w0,h0~[w0]]$ by $[w1,h0~[w0]]$. Since $w1 notin range(d0 ¥ON {w1})$, -- the resulting single-valued map $h1$ will have the same range as the original $h0$ and will -- be finite, much like $h0$. It will satisfy $domain(h1) ¥incin range(h1)$, making us -- able to derive $domain(h1) ¥incin v0$ via Theorem $part_whole_1$, and leading us -- to a contradiction again. -- p0-->Stat6(Stat6*) ==> (p0 in h0) & (w0 = car(p0)) (h0,p0)-->Timage_4(Stat3*) ==> p0 = [car(p0),h0~[car(p0)]] Loc_def ==> Stat7: (y0=h0~[car(p0)]) & (h1 = h0-{[w0,y0]}+{[w1,y0]}) -- (h0-{[w0,y0]},[w1,y0])-->Tfin_1(Stat5,Stat5) ==> Finite(h0-{[w0,y0]}+{[w1,y0]}) EQUAL(Stat1) ==> ([w0,y0] in h0) & Finite(h1) & (domain(h0) = range(d0 ¥ON {w1})) w1-->TfinMostowskiDecoration1(Stat0*) ==> w1 in v0-{w0}-domain(h0) (h0,w0,y0,w1,h1)-->TsingletonMap_3(Stat3*) ==> Svm(h1) & (domain(h1) ¥incin (v0-{w0})) & (range(h1)={v0}+(v0-{w0})) h1-->Tpart_whole_1(Stat7*) ==> false Discharge ==> QED -- Theorem finMostowskiDecoration8: [Injectivity of Mostowski's decoration over the sinks] (({X,Y} ¥incin v0) & (X notin domain(d0)) & ((mski_thryvar~[X]) = (mski_thryvar~[Y]))) ¥imp (X=Y). Proof: Suppose_not(x0,x1) ==> AUTO -- -- Recalling that -- $lbl(W) = if (W in domain(d0)+{arb(v0-domain(d0))}) then 0 else {{v0}+(v0-{W})} end if$, -- we readily get that distinct sinks $x0,x1$ cannot be sent to the same value by $lbl$ . -- Suppose ==> x1 notin domain(d0) x0-->TfinMostowskiDecoration4(*) ==> (mski_thryvar~[x1]) = lbl(x0) x1-->TfinMostowskiDecoration4(*) ==> Stat1: (lbl(x0) = lbl(x1)) & (x0 in v0) & (({x0,x1} * domain(d0)) = 0) & (x0 /= x1) Use_def(lbl)(Stat1) ==> false Discharge ==> AUTO Use_def(lbl(x0)) ==> AUTO x1-->TfinMostowskiDecoration3(*) ==> Stat2: ({ mski_thryvar~[cdr(p)] : p in (d0 ¥ON {x1}) } /= 0) & ((mski_thryvar~[x0]) = { mski_thryvar~[cdr(p)] : p in (d0 ¥ON {x1}) }) p0-->Stat2(Stat2*) ==> p0 in (d0 ¥ON {x1}) Suppose ==> Stat3: (mski_thryvar~[cdr(p0)]) notin { mski_thryvar~[cdr(p)] : p in (d0 ¥ON {x1}) } p0-->Stat3(Stat2*) ==> false; Discharge ==> AUTO (x0,cdr(p0))-->TfinMostowskiDecoration7(*) ==> Stat4: cdr(p0) notin v0 Assump ==> d0 ¥incin (v0 ¥PROD v0) (d0,{x1})-->Trestr_0(Stat2*) ==> p0 in (v0 ¥PROD v0) (p0,v0,v0)-->Tcartesian_0(Stat4*) ==> cdr(p0) in v0 Discharge ==> QED -- Theorem finMostowskiDecoration9: [Injectivity of Mostowski's decoration] (({X,Y} ¥incin v0) & ((mski_thryvar~[X]) = (mski_thryvar~[Y]))) ¥imp (X=Y). Proof: Suppose_not(x1,x2) ==> AUTO -- -- Arguing by contradiction, suppose that -- $(x1 in v0) & (x2 in v0) & ((mski_thryvar~[x1]) = (mski_thryvar~[x2])) & (x1 /= x2)$. -- Loc_def ==> Stat0: a = arb({mski_thryvar~[x]: x in v0 | (EXISTS xp in v0-{x} | (mski_thryvar~[x]) = (mski_thryvar~[xp]))}) -- -- The $a$ just defined (since the argument of $arb$ in its definition is a nonnull set) will satisfy -- $a = (mski_thryvar~[x0])$ and $a = (mski_thryvar~[x3])$ for some $x0 in v0$ and some $x3 in v0$ such that $x0 /= x3$. -- Suppose ==> Stat1: {mski_thryvar~[x]: x in v0 | (EXISTS xp in v0-{x} | (mski_thryvar~[x]) = (mski_thryvar~[xp]))} = 0 x1-->Stat1(*) ==> Stat2: not(EXISTS xp in v0-{x1} | (mski_thryvar~[x1]) = (mski_thryvar~[xp])) x2-->Stat2(*) ==> false Discharge ==> AUTO (Stat0)ELEM ==> Stat3: (0 = a * {mski_thryvar~[x]: x in v0 | (EXISTS xp in v0-{x} | (mski_thryvar~[x]) = (mski_thryvar~[xp]))}) & Stat4: (a in {mski_thryvar~[x]: x in v0 | (EXISTS xp in v0-{x} | (mski_thryvar~[x]) = (mski_thryvar~[xp]))}) x0-->Stat4(Stat3*) ==> Stat5: (EXISTS xp in v0-{x0} | (mski_thryvar~[x0]) = (mski_thryvar~[xp])) & (a = mski_thryvar~[x0]) & (x0 in v0) x3-->Stat5(Stat5*) ==> Stat6: (x3 /= x0) & (x3 in v0) & ((mski_thryvar~[x0]) = (mski_thryvar~[x3])) -- -- On the basis of Theorem $finMostowskiDecoration8$, ${x0,x3} ¥incin domain(d0)$ and therefore, -- by Theorem $finMostowskiDecoration3$, $a /= 0$ and $a = { mski_thryvar~[cdr(p)] : p in (d0 ¥ON {x0}) }$ -- and $a = { mski_thryvar~[cdr(p)] : p in (d0 ¥ON {x3}) }$. -- (x0,x3)-->TfinMostowskiDecoration8(Stat5*) ==> x0 in domain(d0) (x3,x0)-->TfinMostowskiDecoration8(Stat5*) ==> x3 in domain(d0) ()-->TfinMostowskiDecoration0(Stat6*) ==> Stat7: (FORALL x in domain(d0), y in domain(d0) | (EXISTS z | (([x,z] in d0) ¥eq ([y,z] in d0)) ¥imp (x = y))) x0-->TfinMostowskiDecoration3(Stat5*) ==> a = { mski_thryvar~[cdr(p)] : p in (d0 ¥ON {x0}) } x3-->TfinMostowskiDecoration3(Stat5*) ==> (a = { mski_thryvar~[cdr(p)] : p in (d0 ¥ON {x3}) }) & (a /= 0) -- -- Consequently, by the weak extensionality of the digraph under consideration, we can find a $z0$ such that -- $([x0,z0] in d0) ¥neq ([x3,z0] in d0)$. Hence ${x0,x3,z0} ¥incin v0$. -- (x0,x3)-->Stat7(Stat6*) ==> Stat8: (EXISTS z | (([x0,z] in d0) ¥eq ([x3,z] in d0)) ¥imp (x0 = x3)) z0-->Stat8(Stat6*) ==> ([x0,z0] in d0) ¥neq ([x3,z0] in d0) Assump ==> (v0 ¥PROD v0) incs d0 Suppose ==> z0 notin v0 TELEM ==> (cdr([x0,z0]) = z0) & (cdr([x3,z0]) = z0) ([x0,z0],v0,v0)-->Tcartesian_0 ==> AUTO ([x3,z0],v0,v0)-->Tcartesian_0 ==> AUTO (Stat8*)Discharge ==> AUTO Suppose ==> [x0,z0] in d0 -- -- Suppose first that $[x0,z0] in d0$, so that $[x3,z0] notin d0$. Then $(mski_thryvar~[z0]) in a$ -- and therefore there is a $p1 in (d0 ¥ON {x3})$ such that $(mski_thryvar~[cdr(p1)]) = (mski_thryvar~[z0])$ -- and $(mski_thryvar~[z0]) in a$. -- ([x0,z0],x0,z0,d0,x0)-->Trestr_2(Stat8*) ==> [x0,z0] in (d0 ¥ON {x0}) Suppose ==> Stat9: (mski_thryvar~[cdr([x0,z0])]) notin { mski_thryvar~[cdr(p)] : p in (d0 ¥ON {x0}) } ([x0,z0])-->Stat9(Stat8*) ==> false; Discharge ==> AUTO (Stat3*)ELEM ==> Stat10: ((mski_thryvar~[z0]) in { mski_thryvar~[cdr(p)] : p in (d0 ¥ON {x3}) }) & Stat11: ((mski_thryvar~[z0]) notin {mski_thryvar~[x]: x in v0 | (EXISTS xp in v0-{x} | (mski_thryvar~[x]) = (mski_thryvar~[xp]))}) p1-->Stat10(Stat10*) ==> (p1 in (d0 ¥ON {x3})) & ((mski_thryvar~[cdr(p1)]) = (mski_thryvar~[z0])) -- -- Since no $(mski_thryvar~[z0]) in a$ can coincide with $(mski_thryvar~[z1])$ for any -- $z1 in v0$ distinct from $z0$, and since $cdr(p1) in v0$, we have $z0 = cdr(p1)$. -- (d0,{x3})-->Trestr_0(Stat8*) ==> p1 in (v0 ¥PROD v0) (p1,v0,v0)-->Tcartesian_0(Stat10*) ==> (p1 = [car(p1),cdr(p1)]) & (cdr(p1) in v0) (p1,car(p1),cdr(p1),d0,x3)-->Trestr_2(Stat10*) ==> (x3 = car(p1)) & ([x3,cdr(p1)] in d0) (cdr(p1))-->Stat11(Stat10*) ==> Stat12: (not (EXISTS xp in v0-{cdr(p1)} | (mski_thryvar~[cdr(p1)]) = (mski_thryvar~[xp]))) z0-->Stat12(Stat8*) ==> z0 = cdr(p1) -- -- However, the left component of the pair $p1$ is $x3$, which contradicts the supposition -- that $[x3,z0] notin 0$. -- EQUAL(Stat10) ==> [x3,z0] in d0 (Stat8*)Discharge ==> Stat13: ([x3,z0] in d0) & ([x0,z0] notin d0) -- -- Likewise we derive a contradiction, leading to the desired conclusion, -- from the other possibile case, namely from $[x3,z0] in d0$. -- ([x3,z0],x3,z0,d0,x3)-->Trestr_2(Stat13*) ==> [x3,z0] in (d0 ¥ON {x3}) Suppose ==> Stat14: (mski_thryvar~[cdr([x3,z0])]) notin { mski_thryvar~[cdr(p)] : p in (d0 ¥ON {x3}) } ([x3,z0])-->Stat14(Stat8*) ==> false; Discharge ==> AUTO (Stat3*)ELEM ==> Stat15: ((mski_thryvar~[z0]) in { mski_thryvar~[cdr(p)] : p in (d0 ¥ON {x0}) }) & Stat16: ((mski_thryvar~[z0]) notin {mski_thryvar~[x]: x in v0 | (EXISTS xp in v0-{x} | (mski_thryvar~[x]) = (mski_thryvar~[xp]))}) p2-->Stat15(Stat15*) ==> (p2 in (d0 ¥ON {x0})) & ((mski_thryvar~[cdr(p2)]) = (mski_thryvar~[z0])) (d0,{x0})-->Trestr_0(Stat8*) ==> p2 in (v0 ¥PROD v0) (p2,v0,v0)-->Tcartesian_0(Stat15*) ==> (p2 = [car(p2),cdr(p2)]) & (cdr(p2) in v0) (p2,car(p2),cdr(p2),d0,x0)-->Trestr_2(Stat15*) ==> (x0 = car(p2)) & ([x0,cdr(p2)] in d0) (cdr(p2))-->Stat16(Stat15*) ==> Stat17: (not (EXISTS xp in v0-{cdr(p2)} | (mski_thryvar~[cdr(p2)]) = (mski_thryvar~[xp]))) z0-->Stat17(Stat8*) ==> z0 = cdr(p2) EQUAL(Stat8) ==> false Discharge ==> QED -- -- The premiss in the claim of the following theorem is needed because of our convention -- that the application of a map to an element outside its domain yields the value $0$. -- Theorem finMostowskiDecoration10: [Under Mostowski's decoration, arcs are modeled by membership] (Y in v0) ¥imp (((mski_thryvar~[Y]) in (mski_thryvar~[X])) ¥eq ([X,Y] in d0)). Proof: Suppose_not(y0,x0) ==> AUTO Assump ==> Stat1: (v0 ¥PROD v0) incs d0 Suppose ==> x0 in domain(d0) x0-->TfinMostowskiDecoration3(*) ==> Stat2: ((mski_thryvar~[y0]) in { mski_thryvar~[cdr(p)] : p in (d0 ¥ON {x0}) }) ¥neq ([x0,y0] in d0) Suppose ==> Stat3: (mski_thryvar~[y0]) in { mski_thryvar~[cdr(p)] : p in (d0 ¥ON {x0}) } p0-->Stat3(Stat3*) ==> ((mski_thryvar~[y0]) = (mski_thryvar~[cdr(p0)])) & (p0 in (d0 ¥ON {x0})) (d0,{x0})-->Trestr_0(Stat1*) ==> p0 in (v0 ¥PROD v0) (p0,v0,v0)-->Tcartesian_0(Stat3*) ==> (p0 = [car(p0),cdr(p0)]) & (cdr(p0) in v0) (p0,car(p0),cdr(p0),d0,x0)-->Trestr_2(Stat3*) ==> (x0 = car(p0)) & ([x0,cdr(p0)] in d0) (y0,cdr(p0))-->TfinMostowskiDecoration9(*) ==> y0=cdr(p0) EQUAL(Stat3) ==> [x0,y0] in d0 (Stat2*)Discharge ==> AUTO (Stat2*)ELEM ==> Stat4: ((mski_thryvar~[y0]) notin { mski_thryvar~[cdr(p)] : p in (d0 ¥ON {x0}) }) & ([x0,y0] in d0) [x0,y0]-->Stat4(Stat4*) ==> not(((mski_thryvar~[y0]) = (mski_thryvar~[cdr([x0,y0])])) & ([x0,y0] in (d0 ¥ON {x0}))) ([x0,y0],x0,y0,d0,x0)-->Trestr_2(Stat4*) ==> (mski_thryvar~[y0]) /= (mski_thryvar~[cdr([x0,y0])]) TELEM ==> y0 = cdr([x0,y0]) EQUAL(Stat4) ==> false Discharge ==> AUTO Suppose ==> x0 in v0 (x0,y0)-->TfinMostowskiDecoration7(*) ==> Stat5: [x0,y0] in d0 (x0,y0,d0)-->Tdomain_3(Stat1*) ==> false Discharge ==> AUTO ()-->TfinMostowskiDecoration2(Stat1*) ==> x0 notin domain(mski_thryvar) Use_def(domain(mski_thryvar)) ==> AUTO (x0,mski_thryvar)-->Timage_3(*) ==> Stat12: [x0,y0] in (v0 ¥PROD v0) ([x0,y0],v0,v0)-->Tcartesian_0(Stat12) ==> x0 in v0 (Stat1*)Discharge ==> QED -- ENTER_THEORY Set_theory -- --DISPLAY finMostowskiDecoration -- --THEORY finMostowskiDecoration(v0,d0) -- ((v0 ¥PROD v0) incs d0) & (v0 /= 0) & Finite(v0) -- Acyclic(v0,d0) -- WExtensional(v0,d0) --==>(mski_thryvar) -- Is_map(d0) & (domain(d0) ¥incin v0) & (range(d0) ¥incin v0) & (FORALL x in domain(d0), y in domain(d0) | (EXISTS z | (([x,z] in d0) ¥eq ([y,z] in d0)) ¥imp (x = y))) -- Svm(mski_thryvar) & (domain(mski_thryvar) = v0) -- (FORALL w | (W in domain(d0)) ¥imp (((mski_thryvar~[W]) = { mski_thryvar~[cdr(p)] : p in (d0 ¥ON {W}) }) & ((mski_thryvar~[W]) /= 0))) -- 0 in range(mski_thryvar) -- (FORALL y | (Y in range(mski_thryvar)) ¥imp Finite(Y)) -- (FORALL x, y | (({X,Y} ¥incin v0) & (X notin domain(d0))) ¥imp ((mski_thryvar~[Y]) notin (mski_thryvar~[X]))) -- (FORALL x, y | (({X,Y} ¥incin v0) & (X notin domain(d0)) & ((mski_thryvar~[X]) = (mski_thryvar~[Y]))) ¥imp (X=Y)) -- (FORALL x, y | (({X,Y} ¥incin v0) & ((mski_thryvar~[X]) = (mski_thryvar~[Y]))) ¥imp (X=Y)) -- (FORALL y | (Y in v0) ¥imp (((mski_thryvar~[Y]) in (mski_thryvar~[X])) ¥eq ([X,Y] in d0))) --END finMostowskiDecoration -- -- -- \subsection{Weak result about representing graphs as membership digraphs} -- -- Our next THEORY will combine the one just seen, namely $finMostowskiDecoration$, with -- Theorem $xtensionalization_0$, in order to represent an undirected graph by way -- of a membership digraph. -- -- Specifically, we will label the vertices of a graph devoid of self-loops so that: -- * the labeling be injective; -- * each label be finite; -- * the null set be the label of a vertex; -- * each doubleton ${V, W}$ of vertices be and edge if and only if the label of one of the two vertices belongs to the label of the other vertex; -- * the label of a vertex be a subset of the set of all labels whenever it intersects it. -- THEORY finGraphRepr(v0,e0) (e0 ¥incin {{x,y}: x in v0, y in v0-{x}}) & (v0 /= 0) & Finite(v0) END finGraphRepr -- ENTER_THEORY finGraphRepr -- Theorem finGraphRepr0: [Acyclic weakly extensional orientation of current graph] (EXISTS d | (d ¥incin (v0 ¥PROD v0)) & Orientates(d,v0,e0) & Acyclic(v0,d) & WExtensional(v0,d) & (v0 /= 0) & Finite(v0)). Proof: Suppose_not() ==> Stat0: not(EXISTS d | (d ¥incin (v0 ¥PROD v0)) & Orientates(d,v0,e0) & Acyclic(v0,d) & WExtensional(v0,d) & (v0 /= 0) & Finite(v0)) Assump ==> Finite(v0) & (arb(v0) in v0) Loc_def ==> s0 = arb(v0) (v0,s0,e0)-->Txtensionalization_0(*) ==> Stat1: (EXISTS d | Orientates(d,v0,e0) & Acyclic(v0,d) & WExtensional(v0,d) & (s0 notin range(d))) d0-->Stat1(Stat1*) ==> Orientates(d0,v0,e0) & Acyclic(v0,d0) & WExtensional(v0,d0) & (s0 notin range(d0)) (d0 * (v0 ¥PROD v0))-->Stat0(*) ==> not(Orientates(d0*(v0 ¥PROD v0),v0,e0) & Acyclic(v0,d0*(v0 ¥PROD v0)) & WExtensional(v0,d0*(v0 ¥PROD v0))) (d0,v0,e0)-->Torientation2 ==> AUTO (v0,d0,v0,d0*(v0 ¥PROD v0))-->Tacyclicity1 ==> AUTO (v0,d0)-->TweaXtensionality0 ==> AUTO (Stat1*)Discharge ==> QED -- APPLY(v1_thryvar:wskiArcs) Skolem() ==> Theorem finGraphRepr0a: (wskiArcs ¥incin (v0 ¥PROD v0)) & Orientates(wskiArcs,v0,e0) & Acyclic(v0,wskiArcs) & WExtensional(v0,wskiArcs) & (v0 /= 0) & Finite(v0) -- APPLY(mski_thryvar:wski_thryvar) finMostowskiDecoration(v0->v0,d0->wskiArcs) ==> Theorem finGraphRepr0b: Svm(wski_thryvar) & (domain(wski_thryvar) = v0) & (FORALL w | (w in domain(wskiArcs)) ¥imp (((wski_thryvar~[w]) = { wski_thryvar~[cdr(p)] : p in (wskiArcs ¥ON {w}) }) & ((wski_thryvar~[w]) /= 0) )) & (0 in range(wski_thryvar)) & (FORALL y | (Y in range(wski_thryvar)) ¥imp Finite(Y)) & (FORALL x, y | (({X,Y} ¥incin v0) & ((wski_thryvar~[X]) = (wski_thryvar~[Y]))) ¥imp (X=Y)) & (FORALL y, x | (Y in v0) ¥imp (((wski_thryvar~[Y]) in (wski_thryvar~[X])) ¥eq ([X,Y] in wskiArcs))) -- -- -- Theorem finGraphRepr1: (([X,Y] in wskiArcs) or ([Y,X] in wskiArcs)) ¥eq ({X,Y} in e0). Proof: Suppose_not(x0,y0) ==> AUTO TfinGraphRepr0a(*) ==> Stat1: (wskiArcs ¥incin (v0 ¥PROD v0)) & Orientates(wskiArcs,v0,e0) Assump ==> e0 ¥incin {{x,y}: x in v0, y in v0-{x}} Suppose ==> Stat2: {{car(p),cdr(p)}: p in wskiArcs | p = [car(p), cdr(p)]} /= {{car(p),cdr(p)}: p in wskiArcs} p0-->Stat2(Stat1*) ==> (p0 in (v0 ¥PROD v0)) & (p0 /= [car(p0), cdr(p0)]) (p0,v0,v0)-->Tcartesian_0(Stat2*) ==> false Discharge ==> AUTO Use_def(Orientates) ==> Stat3: ((([x0,y0] in wskiArcs) or ([y0,x0] in wskiArcs)) ¥neq ({x0,y0} in {{car(p),cdr(p)}: p in wskiArcs})) Suppose ==> Stat4: ({x0,y0} in {{car(p),cdr(p)}: p in wskiArcs}) & (not(([x0,y0] in wskiArcs) or ([y0,x0] in wskiArcs))) p1-->Stat4(Stat1*) ==> Stat5: ({x0,y0} = {car(p1),cdr(p1)}) & (p1 in (v0 ¥PROD v0)) & (p1 in wskiArcs) (p1,v0,v0)-->Tcartesian_0(Stat5*) ==> (p1 = [car(p1),cdr(p1)]) & (((x0=car(p1)) & (y0=cdr(p1))) or ((x0=cdr(p1)) & (y0=car(p1)))) Suppose ==> (x0=car(p1)) & (y0=cdr(p1)) EQUAL ==> false; Discharge ==> (y0=car(p1)) & (x0=cdr(p1)) EQUAL ==> false; Discharge ==> AUTO Suppose ==> Stat6: ({x0,y0} notin {{car(p),cdr(p)}: p in wskiArcs}) & ([x0,y0] in wskiArcs) [x0,y0]-->Stat6(Stat6*) ==> false Discharge ==> Stat7: ({x0,y0} notin {{car(p),cdr(p)}: p in wskiArcs}) & ([y0,x0] in wskiArcs) [y0,x0]-->Stat7(Stat7*) ==> false Discharge ==> QED -- Theorem finGraphRepr2: ({X,Y} ¥incin v0) ¥imp ((((wski_thryvar~[Y]) in (wski_thryvar~[X])) or ((wski_thryvar~[X]) in (wski_thryvar~[Y]))) ¥eq ({X,Y} in e0)). Proof: Suppose_not(x0,y0) ==> AUTO TfinGraphRepr0b(*) ==> Stat1: (FORALL y, x | (y in v0) ¥imp (((wski_thryvar~[y]) in (wski_thryvar~[x])) ¥eq ([x,y] in wskiArcs))) (y0,x0)-->Stat1(*) ==> ((wski_thryvar~[y0]) in (wski_thryvar~[x0])) ¥eq ([x0,y0] in wskiArcs) (x0,y0)-->Stat1(*) ==> ((wski_thryvar~[x0]) in (wski_thryvar~[y0])) ¥eq ([y0,x0] in wskiArcs) (x0,y0)-->TfinGraphRepr1(*) ==> false Discharge ==> QED -- Theorem finGraphRepr3: (((wski_thryvar~[X]) * range(wski_thryvar)) /= 0) ¥imp ((wski_thryvar~[X]) ¥incin range(wski_thryvar)). Proof: Suppose_not(x0) ==> AUTO Use_def(range(wski_thryvar)) ==> AUTO ELEM ==> Stat1: ((wski_thryvar~[x0]) * {cdr(p): p in wski_thryvar} /= 0) & ((wski_thryvar~[x0]) ¥nincin {cdr(p): p in wski_thryvar}) z0-->Stat1(Stat1*) ==> Stat2: (z0 in {cdr(p): p in wski_thryvar}) & (z0 in (wski_thryvar~[x0])) p0-->Stat2(Stat2*) ==> (p0 in wski_thryvar) & (z0 = cdr(p0)) TfinGraphRepr0b(Stat2*) ==> Stat3: (FORALL y, x | (y in v0) ¥imp (((wski_thryvar~[y]) in (wski_thryvar~[x])) ¥eq ([x,y] in wskiArcs))) & (FORALL w | (w in domain(wskiArcs)) ¥imp (((wski_thryvar~[w]) = { wski_thryvar~[cdr(p)] : p in (wskiArcs ¥ON {w}) }) & ((wski_thryvar~[w]) /= 0) )) & Svm(wski_thryvar) & (domain(wski_thryvar) = v0) Loc_def ==> y0 = car(p0) (p0,wski_thryvar)-->Tdomain_2(Stat2*) ==> y0 in v0 (wski_thryvar,p0)-->Timage_4(Stat2*) ==> p0 = [car(p0),wski_thryvar~[car(p0)]] TELEM ==> cdr([car(p0),wski_thryvar~[car(p0)]]) = wski_thryvar~[car(p0)] EQUAL(Stat2) ==> z0 = wski_thryvar~[y0] (x0,y0,wskiArcs)-->Tdomain_3 ==> AUTO (y0,x0,x0)-->Stat3(*) ==> Stat5: { wski_thryvar~[cdr(p)] : p in (wskiArcs ¥ON {x0}) } ¥nincin range(wski_thryvar) TfinGraphRepr0a(Stat5*) ==> wskiArcs ¥incin (v0 ¥PROD v0) (wskiArcs,{x0})-->Trestr_0(Stat5*) ==> Stat6: (wskiArcs ¥ON {x0}) ¥incin (v0 ¥PROD v0) c-->Stat5(Stat5*) ==> Stat7: (c in { wski_thryvar~[cdr(p)] : p in (wskiArcs ¥ON {x0}) }) & (c notin range(wski_thryvar)) p1-->Stat7(Stat5*) ==> Stat8: (p1 in (v0 ¥PROD v0)) & ((wski_thryvar~[cdr(p1)]) notin range(wski_thryvar)) (p1,v0,v0)-->Tcartesian_0(Stat8*) ==> cdr(p1) in v0 wski_thryvar-->Timage_5(Stat3,Stat3*) ==> wski_thryvar = {[x,wski_thryvar~[x]]: x in domain(wski_thryvar)} EQUAL(Stat3) ==> wski_thryvar = {[x,wski_thryvar~[x]]: x in v0} Suppose ==> Stat9: [cdr(p1),wski_thryvar~[cdr(p1)]] notin {[x,wski_thryvar~[x]]: x in v0} (cdr(p1))-->Stat9(Stat8*) ==> false; Discharge ==> AUTO Use_def(range(wski_thryvar)) ==> AUTO (Stat8*)ELEM ==> Stat10: ((wski_thryvar~[cdr(p1)]) notin {cdr(p): p in wski_thryvar}) & ([cdr(p1),wski_thryvar~[cdr(p1)]] in wski_thryvar) ([cdr(p1),wski_thryvar~[cdr(p1)]])-->Stat10(Stat10*) ==> false Discharge ==> QED -- -- ENTER_THEORY Set_theory -- --DISPLAY finGraphRepr -- --THEORY finGraphRepr(v0,e0) -- (e0 ¥incin {{x,y}: x in v0, y in v0-{x}}) & (v0 /= 0) & Finite(v0) --==>(wski_thryvar) -- Svm(wski_thryvar) & (domain(wski_thryvar) = v0) -- 0 in range(wski_thryvar) -- (FORALL y | (Y in range(wski_thryvar)) ¥imp Finite(Y)) -- (FORALL x, y | (({X,Y} ¥incin v0) & ((wski_thryvar~[X]) = (wski_thryvar~[Y]))) ¥imp (X=Y)) -- (FORALL x, y | ({X,Y} ¥incin v0) ¥imp ((((wski_thryvar~[Y]) in (wski_thryvar~[X])) or ((wski_thryvar~[X]) in (wski_thryvar~[Y]))) ¥eq ({X,Y} in e0))) -- (FORALL x | (((wski_thryvar~[X]) * range(wski_thryvar)) /= 0) ¥imp ((wski_thryvar~[X]) ¥incin range(wski_thryvar))) --END finGraphRepr -- -- -- -- \section{Representation of a connected, claw-free graph as the membership digraph of a transitive set} -- -- \subsection{Extensional orientation of a connected, claw-free graph} -- Def clawFreeGraph: [Claw-freeness, as a property of graphs] ClawFreeG(V,E) := (FORALL w, x, y, z | (({w,x,y,z} ¥incin V) & ({w,y} in E) & ({y,x} in E) & ({y,z} in E)) ¥imp (not((x/=z) & (w notin {z,x}) & ({x,z} notin E) & ({z,w} notin E) & ({w,x} notin E)))) -- Theorem cClawFreeG_0: [Hereditarity of the claw-freeness property of graphs] (ClawFreeG(V,E) & (W ¥incin V)) ¥imp ClawFreeG(W,{a in E | a ¥incin W}). Proof: Suppose_not(v0,e0,w0) ==> Stat0: ClawFreeG(v0,e0) & (w0 ¥incin v0) & (not ClawFreeG(w0,{a in e0 | a ¥incin w0})) Loc_def ==> Stat1: e1 = {a in e0 | a ¥incin w0} EQUAL ==> not ClawFreeG(w0,e1) Set_monot ==> {a in e0 | a ¥incin w0} ¥incin {a in e0 | true} Use_def(ClawFreeG) ==> Stat2: (not (FORALL w, x, y, z | (({w,x,y,z} ¥incin w0) & ({w,y} in e1) & ({y,x} in e1) & ({y,z} in e1)) ¥imp (not((x/=z) & (w notin {z,x}) & ({x,z} notin e1) & ({z,w} notin e1) & ({w,x} notin e1))))) & (FORALL w, x, y, z | (({w,x,y,z} ¥incin v0) & ({w,y} in e0) & ({y,x} in e0) & ({y,z} in e0)) ¥imp (not((x/=z) & (w notin {z,x}) & ({x,z} notin e0) & ({z,w} notin e0) & ({w,x} notin e0)))) (Stat0*)ELEM ==> (w0 ¥incin v0) & (e1 ¥incin e0) (wp,xp,yp,zp,wp,xp,yp,zp)-->Stat2(Stat2*) ==> Stat3: ({wp,xp,yp,zp} ¥incin w0) & ({xp,zp} notin e1) & ({zp,wp} notin e1) & ({wp,xp} notin e1) & (not(({xp,zp} notin e0) & ({zp,wp} notin e0) & ({wp,xp} notin e0))) (Stat3,Stat1*)ELEM ==> Stat4: ({xp,zp} notin {a in e0 | a ¥incin w0}) & Stat5: ({zp,wp} notin {a in e0 | a ¥incin w0}) & Stat6: ({wp,xp} notin {a in e0 | a ¥incin w0}) ()-->Stat4(Stat3,Stat7*) ==> Stat7: ({xp,zp} notin e0) ()-->Stat5(Stat3,Stat8*) ==> Stat8: {zp,wp} notin e0 ()-->Stat6(Stat3,Stat7,Stat8*) ==> false Discharge ==> QED -- -- -- -- -- Theorem cClawFreeG_1: [Preservation of acyclicity and extensionality under adjunction of an outer vertex to a digraph whose underlying graph is connected and claw free] ((W = V+{U}) & (U notin V) & ({s in V | ((D ¥ON {s}) = 0) & ({s,U} in E)} = 0) & (E ¥incin {{x,y}: x in Z, y in Z-{x}}) & ClawFreeG(W,E) & HasSpanningTree(W,E) & Orientates(D,V,E) & Acyclic(V,D) & Extensional(V,D) & (D ¥incin (V ¥PROD V)) & (Dp = D + ({U} ¥PROD {t in V | {U,t} in E}))) ¥imp (Orientates(Dp,W,E) & Acyclic(W,Dp) & Extensional(W,Dp) & (Dp ¥incin (W ¥PROD W))). Proof: Suppose_not(v1,v0,x0,d0,e2,v2,d1) ==> Stat0: (not(Orientates(d1,v1,e2) & Acyclic(v1,d1) & Extensional(v1,d1) & (d1 ¥incin (v1 ¥PROD v1)))) & (x0 in v1) & (v0 = v1-{x0}) & ({s in v0 | ((d0 ¥ON {s}) = 0) & ({s,x0} in e2)} = 0) & (e2 ¥incin {{x,y}: x in v2, y in v2-{x}}) & ClawFreeG(v1,e2) & HasSpanningTree(v1,e2) & Orientates(d0,v0,e2) & Acyclic(v0,d0) & Extensional(v0,d0) & (d0 ¥incin (v0 ¥PROD v0)) & (d1 = d0 + ({x0} ¥PROD {t in v0 | {x0,t} in e2})) -- -- Suppose that $v1,v0,x0,d0,e2,v2,d1$ constitute a counterexample to the claim. We readily exclude the case that -- $not Acyclic(v1,d1)$ and the case that $not Orientates(d1,v1,e2)$. Also, through Theorem $xtensionalization_1$, -- we exclude that $d1 ¥nincin (v1 ¥PROD v1)$ and reduce the only possibility left, namely $not Extensional(v1,d1)$, to -- the condition $(EXISTS x in v0 | (FORALL z | ([x0,z] in d1) ¥eq ([x,z] in d0)))$. So, let -- $x1 in v0$ be such that $(FORALL z | ([x0,z] in d1) ¥eq ([x1,z] in d0))$. -- Set_monot ==> {t in v0 | true} incs {t in v0 | {x0,t} in e2} (Stat0*)ELEM ==> Stat1: (v1 = v0 + {x0}) & (v0 incs {t in v0 | {x0,t} in e2}) (v0,d0,x0,{t in v0 | {x0,t} in e2})-->Tacyclicity0(*) ==> Acyclic(v0+{x0},d0 + ({x0} ¥PROD {t in v0 | {x0,t} in e2})) EQUAL ==> Acyclic(v1,d1) (d0,v0,e2,v1,x0,d1)-->Torientation3(*) ==> Stat2: Orientates(d1,v1,e2) (v1,v0,x0,d0,e2,v2,d1)-->Txtensionalization_1(*) ==> Stat3: (EXISTS x in v0 | (FORALL z | ([x0,z] in d1) ¥eq ([x,z] in d0))) x1-->Stat3(*) ==> Stat4: (FORALL z | ([x0,z] in d1) ¥eq ([x1,z] in d0)) & (x1 in (v1-{x0})) -- -- The digraph $v1,d1$ is connected, hence $x0$ has at least one successor -- in $v1,d1$, witnessing that $x1$ has successors in $v0,d0$. -- Suppose ==> Stat5: {z in v0 | [x1,z] in d0} = 0 (Stat0,Stat4*)ELEM ==> HasSpanningTree(v1,e2) & (x0 in v1) & (v1-{x0} /= 0) & (e2 ¥incin {{x,y}: x in v2, y in v2-{x}}) (v1,e2,v2,x0)-->Tconnectivity_1(Stat0,Stat4*) ==> Stat6: (EXISTS w in v1-{x0} | {x0,w} in e2) y1-->Stat6(Stat6*) ==> Stat7: (y1 in (v1-{x0})) & ({x0,y1} in e2) Suppose ==> Stat8: [y1,x0] in d1 ([y1,x0],{x0},{t in v0 | {x0,t} in e2})-->Tcartesian_0(Stat8,Stat0,Stat7*) ==> Stat9: [y1,x0] in d0 (d0,v0,e2,y1,x0)-->Torientation6(Stat0,Stat9*) ==> false Discharge ==> AUTO (d1,v1,e2,x0,y1)-->Torientation7(Stat1*) ==> [x0,y1] in d1 y1-->Stat4(Stat6*) ==> [x1,y1] in d0 y1-->Stat5 ==> AUTO (Stat0*)Discharge ==> AUTO -- -- Since $v0,d0$ is acyclic, at least one successor $y0$ of $x1$ in $v0,d0$ -- has no successors in common with $x1$ in $v0,d0$. -- Use_def(Acyclic)(Stat0,Stat0) ==> Stat11: (FORALL w ¥incin v0 | (w /= 0) ¥imp (EXISTS t in w | 0 = {y in w | [t,y] in d0})) Set_monot(Stat11) ==> {z in v0 | [x1,z] in d0} ¥incin {z in v0 | true} {z in v0 | [x1,z] in d0}-->Stat11(Stat4*) ==> Stat12: (EXISTS t in {z in v0 | [x1,z] in d0} | 0 = {y in {z in v0 | [x1,z] in d0} | [t,y] in d0}) y0-->Stat12(Stat12*) ==> (y0 in {z in v0 | [x1,z] in d0}) & (0 = {y in {z in v0 | [x1,z] in d0} | [y0,y] in d0}) SIMPLF(Stat12) ==> Stat13: (y0 in {z in v0 | [x1,z] in d0}) & ({y in v0 | ([x1,y] in d0) & ([y0,y] in d0)} = 0) ()-->Stat13(Stat13*) ==> Stat14: (y0 in v0) & ([x1,y0] in d0) -- -- Being a successor of $x1$ in $d0$, $y0$ must also be a successor of $x0$ in $d1$; -- but then it must, in its turn, have a successor $z0$ in $d0$: this is because we have -- supposed at the outset that $x0$ is adjacent to no sink of $d0$. -- y0-->Stat4(Stat14*) ==> Stat15: [x0,y0] in d1 Suppose ==> Stat16: not(EXISTS z in v0 | [y0,z] in d0) (Stat0*)ELEM ==> Stat17: y0 notin {s in v0 | ((d0 ¥ON {s}) = 0) & ({s,x0} in e2)} (d1,v1,e2,x0,y0)-->Torientation6(Stat2,Stat15*) ==> {y0,x0} in e2 y0-->Stat17(Stat14*) ==> Stat18: (d0 ¥ON {y0}) /= 0 (d0,{y0})-->Trestr_0(Stat0,Stat0*) ==> (d0 ¥ON {y0}) ¥incin (v0 ¥PROD v0) p2-->Stat18(Stat18*) ==> (p2 in (d0 ¥ON {y0})) & (p2 in (v0 ¥PROD v0)) (p2,v0,v0)-->Tcartesian_0(Stat18*) ==> (p2 = [car(p2),cdr(p2)]) & (cdr(p2) in v0) (p2,car(p2),cdr(p2),d0,y0)-->Trestr_2(Stat18*) ==> [y0,cdr(p2)] in d0 (cdr(p2))-->Stat16 ==> AUTO (Stat18*)Discharge ==> Stat19: (EXISTS z in v0 | [y0,z] in d0) z0-->Stat19(Stat19*) ==> Stat20: (z0 in v0) & ([y0,z0] in d0) -- -- We will show next ${x0,x1,y0,z0}$ form a claw of $v1,e2$, which is untenable. -- To reach this (sought) contradiction we are to show (in addition to the already -- established facts that ${y0, x1}$, ${x0, y0}$, and ${y0, z0}$ are edges, -- to the already known inequalities $x1 /= x0$, $y0 /= x0$, $z0 /= x0$, and to the -- obvious consequences $y0 /= x1$, $y0 /= z0$ of the acyclicity of $d0$) -- that none of ${x0, x1}$, ${x1, z0}$, ${z0, x0}$ is an edge and that $x1 /= z0$. -- (Stat0,Stat4,Stat14,Stat20*)ELEM ==> Stat21: ({x0,x1,y0,z0} ¥incin v1) & (x0 notin {z0,x1}) -- -- In particular, why ${x0,x1}$ cannot be an edge? Suppose the contrary. It follows from -- $[x1, x1] notin d0$ that $[x0, x1] notin d0$; therefore, since $Orientates(d1, v1, e2)$ holds, -- we must have $[x1, x0] in d1$. Since all pairs in $d1-d0$ have first component $x0$, -- this implies $[x1, x0] in d0$. However, because of $Orientates(d0, v0, e2)$, -- this implies ${x1, x0} incin v0$, whereas we know that $x0 notin v0$. -- (d0,v0,e2,x1)-->Torientation8(Stat0,Stat0*) ==> [x1,x1] notin d0 x1-->Stat4(Stat21*) ==> [x0,x1] notin d1 Suppose ==> {x0,x1} in e2 (Stat2,Stat0,Stat4*)ELEM ==> Orientates(d1,v1,e2) & (x0 in v1-v0) & (x1 in (v1-{x0})) & Orientates(d0,v0,e2) (d1,v1,e2,x0,x1)-->Torientation7(Stat15*) ==> Stat22: [x1,x0] in d1 ([x1,x0],{x0},{t in v0 | {x0,t} in e2})-->Tcartesian_0(Stat4,Stat0,Stat22*) ==> [x1,x0] in d0 (d0,v0,e2,x1,x0)-->Torientation6 ==> AUTO (Stat15*)Discharge ==> AUTO (d1,v1,e2,x1,y0)-->Torientation6(Stat14,Stat0,Stat1,Stat2*) ==> {y0,x1} in e2 (d1,v1,e2,y0,z0)-->Torientation6(Stat20,Stat0,Stat1,Stat2*) ==> {y0,z0} in e2 (d1,v1,e2,x0,y0)-->Torientation6(Stat15,Stat2*) ==> {x0,y0} in e2 Suppose ==> x1 = z0 EQUAL(Stat14) ==> Stat23: [z0,y0] in d0 (v0,d0,y0,z0)-->Tacyclicity2(Stat0,Stat14,Stat20,Stat23*) ==> false Discharge ==> AUTO Use_def(ClawFreeG) ==> Stat24: (FORALL w, x, y, z | (({w,x,y,z} ¥incin v1) & ({w,y} in e2) & ({y,x} in e2) & ({y,z} in e2)) ¥imp (not((x/=z) & (w notin {z,x}) & ({x,z} notin e2) & ({z,w} notin e2) & ({w,x} notin e2)))) (x0,x1,y0,z0)-->Stat24(Stat21*) ==> Stat25: ({x1,z0} in e2) or ({z0,x0} in e2) Suppose ==> Stat26: [x0,z0] in d1 z0-->Stat4(Stat26,Stat13*) ==> Stat27: (z0 notin {y in v0 | ([x1,y] in d0) & ([y0,y] in d0)}) & ([x1,z0] in d0) z0-->Stat27 ==> AUTO (Stat20*)Discharge ==> Stat28: [x0,z0] notin d1 Suppose ==> Stat29: {x1,z0} in e2 (d0,v0,e2,x1,z0)-->Torientation7(Stat0,Stat4,Stat20,Stat29*) ==> (x1 = z0) or ([x1,z0] in d0) or ([z0,x1] in d0) Suppose ==> x1 = z0 (v0,d0,y0,x1)-->Tacyclicity2(Stat0,Stat4,Stat14*) ==> [y0,x1] notin d0 EQUAL(Stat20) ==> false Discharge ==> AUTO z0-->Stat4(Stat28*) ==> [z0,x1] in d0 (v0,d0,x1,y0,z0)-->Tacyclicity5(Stat0,Stat20,Stat14,Stat4*) ==> [z0,x1] notin d0 (Stat29*)Discharge ==> Stat30: {z0,x0} in e2 (d1,v1,e2,z0,x0)-->Torientation7(Stat2,Stat0,Stat20,Stat21,Stat30,Stat28*) ==> Stat31: [z0,x0] in d1 ([z0,x0],{x0},{t in v0 | {x0,t} in e2})-->Tcartesian_0(Stat21,Stat0,Stat31*) ==> Stat32: [z0,x0] in d0 (d0,v0,e2,z0,x0)-->Torientation6(Stat32,Stat0*) ==> false Discharge ==> QED -- -- Theorem cClawFreeG_2: [Acyclic extensional orientability of a connected and claw-free (finite) graph] (Finite(V) & HasSpanningTree(V,E) & (E ¥incin {{x,y}: x in V, y in V-{x}}) & ClawFreeG(V,E)) ¥imp (EXISTS d ¥incin (V ¥PROD V) | Orientates(d,V,E) & Acyclic(V,d) & Extensional(V,d)). Proof: Suppose_not(v2,e2) ==> AUTO -- -- Arguing by contradiction, suppose that there is a counterexample $v2,e2$ to the claim. -- Then, thanks to the finiteness hypothesis, we can take a minimal counterexample -- $v1,e1$ with $v1 ¥incin v2$ and $e1 = e2*{{x,y}: x in v1, y in v1}$. -- (e2,v2,v2)-->TvertexInduced_0(*) ==> Stat1: ((e2*{{x,y}: x in v2, y in v2}) = e2) & (e2 = (e2*{{x,y}: x in v2, y in v2-{x}})) EQUAL ==> HasSpanningTree(v2,e2*{{x,y}: x in v2, y in v2}) & ClawFreeG(v2,e2*{{x,y}: x in v2, y in v2}) & (not(EXISTS d ¥incin (v2 ¥PROD v2) | Orientates(d,v2,e2) & Acyclic(v2,d) & Extensional(v2,d))) APPLY(fin_thryvar:v1) finiteInduction(s0->v2,P(S)->(HasSpanningTree(S,e2*{{x,y}: x in S, y in S}) & ClawFreeG(S,e2*{{x,y}: x in S, y in S}) & (not(EXISTS d ¥incin (S ¥PROD S) | Orientates(d,S,e2) & Acyclic(S,d) & Extensional(S,d))))) ==> Stat3: (FORALL S | (S ¥incin v1) ¥imp ( Finite(S) & ( (HasSpanningTree(S,e2*{{x,y}: x in S, y in S}) & ClawFreeG(S,e2*{{x,y}: x in S, y in S}) & (not(EXISTS d ¥incin (S ¥PROD S) | Orientates(d,S,e2) & Acyclic(S,d) & Extensional(S,d)))) ¥eq (S = v1)) )) v1-->Stat3(Stat3*) ==> Stat4: (not(EXISTS d ¥incin (v1 ¥PROD v1) | Orientates(d,v1,e2) & Acyclic(v1,d) & Extensional(v1,d))) & HasSpanningTree(v1,e2*{{x,y}: x in v1, y in v1}) & ClawFreeG(v1,e2*{{x,y}: x in v1, y in v1}) -- -- We exclude that $v1$ can be a singleton, else a contradiction would arise. -- In this case, in fact, an extensional acyclic orientation of $v1,e1$ is -- the null set of edges. -- Suppose ==> v1 = {arb(v1)}; 0-->Stat4 ==> AUTO; (v1,arb(v1),e2)-->Tvoidgraph1 ==> AUTO; v1-->Tvoidgraph2 ==> AUTO; (Stat4*)Discharge ==> AUTO -- -- Since $v1$ is not a singleton, thanks to Theorem $connectivity_2$, we can consider a non-cut vertex $x0$ of $v1,e1$. -- (e2,v2,v1)-->TvertexInduced_0(Stat1*) ==> (e2*{{x,y}: x in v1, y in v1}) ¥incin {{x,y}: x in v1, y in v1-{x}} (v1,e2*{{x,y}: x in v1, y in v1})-->Tconnectivity_2(Stat4*) ==> Stat10: (EXISTS u in v1 | HasSpanningTree( v1-{u}, {a in (e2*{{x,y}: x in v1, y in v1}) | u notin a} )) x0-->Stat10(Stat10*) ==> (x0 in v1) & HasSpanningTree( v1-{x0}, {a in (e2*{{x,y}: x in v1, y in v1}) | x0 notin a} ) -- -- Now consider the graph $v0,e0$ induced by $v1,e1$ on the strict subset $v1-{x0}$ of the set of vertices. -- Before we can utilize the induction hypothesis, which trivially applies to this subgraph, -- in order to get an acyclic and extensional orientation $d0$ of its vertices, -- we must specify the set of edges of the induced subgraph in two convenient, equivalent ways. -- Suppose ==> Stat11: {a in (e2*{{x,y}: x in v1, y in v1}) | x0 notin a} /= e2*{{x,y}: x in v1-{x0}, y in v1-{x0}} a1-->Stat11 ==> AUTO Suppose ==> Stat12: a1 in {a in (e2*{{x,y}: x in v1, y in v1}) | x0 notin a} ()-->Stat12(Stat11*) ==> Stat13: (a1 in {{x,y}: x in v1, y in v1}) & (a1 notin {{x,y}: x in v1-{x0}, y in v1-{x0}}) & (x0 notin a1) (x4,y4,x4,y4)-->Stat13(Stat13*) ==> false (Stat12*)Discharge ==> Stat14: (a1 in {{x,y}: x in v1-{x0}, y in v1-{x0}}) & (a1 notin {a in (e2*{{x,y}: x in v1, y in v1}) | x0 notin a}) & (a1 in e2) (x5,y5,{x5,y5})-->Stat14(Stat14*) ==> Stat15: ({x5,y5} notin {{x,y}: x in v1, y in v1}) & (x5 in v1-{x0}) & (y5 in v1-{x0}) (x5,y5)-->Stat15(Stat15*) ==> false Discharge ==> {a in (e2*{{x,y}: x in v1, y in v1}) | x0 notin a} = e2*{{x,y}: x in v1-{x0}, y in v1-{x0}} -- Suppose ==> Stat16: {a in (e2*{{x,y}: x in v1, y in v1}) | x0 notin a} /= {a in (e2*{{x,y}: x in v1, y in v1}) | a ¥incin (v1-{x0})} a3-->Stat16(Stat16*) ==> Stat17: (a3 in {{x,y}: x in v1, y in v1}) & (x0 notin a3) & (a3 ¥nincin (v1-{x0})) (x6,y6)-->Stat17(Stat17*) ==> false; Discharge ==> {a in (e2*{{x,y}: x in v1, y in v1}) | x0 notin a} = {a in (e2*{{x,y}: x in v1, y in v1}) | a ¥incin (v1-{x0})} -- Suppose ==> not (HasSpanningTree( v1-{x0}, e2*{{x,y}: x in v1-{x0}, y in v1-{x0}} ) & ClawFreeG( v1-{x0}, e2*{{x,y}: x in v1-{x0}, y in v1-{x0}} )) (v1,e2*{{x,y}: x in v1, y in v1},v1-{x0})-->TcClawFreeG_0(Stat4*) ==> ClawFreeG(v1-{x0},{a in (e2*{{x,y}: x in v1, y in v1}) | a ¥incin (v1-{x0})}) EQUAL(Stat10) ==> false; Discharge ==> AUTO (v1-{x0})-->Stat3(Stat10*) ==> Stat18: (EXISTS d ¥incin ((v1-{x0}) ¥PROD (v1-{x0})) | Orientates(d,v1-{x0},e2) & Acyclic(v1-{x0},d) & Extensional(v1-{x0},d)) d0-->Stat18(Stat18*) ==> Orientates(d0,v1-{x0},e2) & Acyclic(v1-{x0},d0) & Extensional(v1-{x0},d0) & (d0 ¥incin ((v1-{x0}) ¥PROD (v1-{x0}))) -- -- We first deal with the case when the acyclic digraph $v1-{x0},d0$ -- has no sink adjacent to $x0$ through $e1$ -- In this case, as suggested by Theorem $cClawFreeG_1$, -- we orient the edges incident to $x0$ as out-going from $x0$, -- to obtain an extensional acyclic orientation for $v1,e1$. -- Note that the neighbors of $x0$ through $e1$ are ${t in v1 | {x0,t} in e1}$, -- hence $d1=d0+({x0}\PROD {t in v1 | {x0,t} in e1})$, although our specification -- of $d1$ will not be so transparent. -- Suppose ==> {s in v1-{x0} | ((d0 ¥ON {s}) = 0) & ({s,x0} in (e2*{{x,y}: x in v1, y in v1}))} = 0 (v1,v1-{x0},d0,e2)-->Torientation0(Stat18*) ==> Orientates(d0,v1-{x0},e2*{{x,y}: x in v1, y in v1}) Loc_def ==> d1 = d0 + ({x0} ¥PROD {t in v1-{x0} | {x0,t} in e2*{{x,y}: x in v1, y in v1}}) (Stat1*)ELEM ==> (e2 ¥incin {{x,y}: x in v2, y in v2-{x}}) & (v1 = v1-{x0}+{x0}) (v1,v1-{x0},x0,d0,e2*{{x,y}: x in v1, y in v1},v2,d1)-->TcClawFreeG_1(Stat4*) ==> Stat21: (d1 ¥incin (v1 ¥PROD v1)) & Orientates(d1,v1,e2*{{x,y}: x in v1, y in v1}) & Acyclic(v1,d1) & Extensional(v1,d1) (v1,v1,d1,e2)-->Torientation0(Stat18*) ==> Orientates(d1,v1,e2) ¥eq Orientates(d1,v1,e2*{{x,y}: x in v1, y in v1}) d1-->Stat4(Stat21*) ==> false Discharge ==> Stat22: {s in v1-{x0} | ((d0 ¥ON {s}) = 0) & ({s,x0} in (e2*{{x,y}: x in v1, y in v1}))} /= 0 -- -- Next we deal with the case when the acyclic digraph $v1-{x0},d0$ -- has its sink $s1$ adjacent to $x0$ through $e2$. -- In this case, as suggested by Theorem $xtensionalization_2$, -- we orient the edges incident to $x0$ as in-coming to $x0$. -- s1-->Stat22(Stat22*) ==> Stat23: ({s1,x0} in e2) & (s1 in v1-{x0}) & ((d0 ¥ON {s1}) = 0) Suppose ==> Stat24: s1 notin {t in v1 | {x0,t} in e2} s1-->Stat24(Stat23*) ==> false; Discharge ==> AUTO (v1,v1-{x0},x0,s1,d0,e2,v2)-->Txtensionalization_2(*) ==> Stat25: {y in (v1-{x0}) | [s1,y] in d0} /= 0 y7-->Stat25(Stat25*) ==> (y7 in (v1-{x0})) & ([s1,y7] in d0) ([s1,y7],s1,y7,d0,s1)-->Trestr_2(Stat23*) ==> false Discharge ==> QED -- -- -- \subsection{Result about representing claw-free graphs as transitive sets} -- Def heredFinite: [Hereditarily finite] HerFin(S) := Finite(S) & (FORALL x in S | HerFin(x)) -- -- -- Our next THEORY will combine the THEORY $finMostowskiDecoration$ seen above with -- Theorem $cClawFreeG_2$, in order to represent a claw-free graph by way -- of a membership digraph whose set of support is a transitive set. -- -- Specifically, we will label the vertices of a claw-free graph devoid of self-loops so that: -- * the labeling be injective; -- * the null set be the label of a vertex; -- * each doubleton ${V, W}$ of vertices be and edge if and only if the label of one -- of the two vertices belongs to the label of the other vertex; -- * the label of each vertex be a subset of the set of all labels; -- * the set of all labels be transitive; -- * each label be a hereditarily finite set. -- THEORY herfinCCFGraphRepr(v0,e0) (e0 ¥incin {{x,y}: x in v0, y in v0-{x}}) & Finite(v0) HasSpanningTree(v0,e0) & ClawFreeG(v0,e0) END herfinCCFGraphRepr -- ENTER_THEORY herfinCCFGraphRepr -- Theorem herfinCCFGraphRepr0: [Acyclic extensional orientation of current graph] (EXISTS d | (d ¥incin (v0 ¥PROD v0)) & Orientates(d,v0,e0) & Acyclic(v0,d) & Extensional(v0,d)). Proof: Suppose_not() ==> AUTO Assump ==> Finite(v0) & HasSpanningTree(v0,e0) & (e0 ¥incin {{x,y}: x in v0, y in v0-{x}}) & ClawFreeG(v0,e0) (v0,e0)-->TcClawFreeG_2(*) ==> Stat1: (EXISTS d ¥incin (v0 ¥PROD v0) | Orientates(d,v0,e0) & Acyclic(v0,d) & Extensional(v0,d)) & ( not(EXISTS d | (d ¥incin (v0 ¥PROD v0)) & Orientates(d,v0,e0) & Acyclic(v0,d) & Extensional(v0,d)) ) (d0,d0)-->Stat1(*) ==> false Discharge ==> QED -- APPLY(v1_thryvar:wskiArcs) Skolem() ==> Theorem herfinCCFGraphRepr0a: (wskiArcs ¥incin (v0 ¥PROD v0)) & Orientates(wskiArcs,v0,e0) & Acyclic(v0,wskiArcs) & Extensional(v0,wskiArcs) -- Theorem herfinCCFGraphRepr0b: (wskiArcs ¥incin (v0 ¥PROD v0)) & Orientates(wskiArcs,v0,e0) & Acyclic(v0,wskiArcs) & WExtensional(v0,wskiArcs) & (v0 /= 0) & Finite(v0). Proof: Suppose_not() ==> AUTO Assump ==> Finite(v0) & HasSpanningTree(v0,e0) (v0,e0)-->Tconnectivity_0(*) ==> v0 /= 0 ()-->TherfinCCFGraphRepr0a(*) ==> Extensional(v0,wskiArcs) & ((v0 ¥PROD v0) incs wskiArcs) & (not WExtensional(v0,wskiArcs)) (v0,wskiArcs)-->Textensionality0(*) ==> false Discharge ==> QED -- -- APPLY(mski_thryvar:trans_thryvar) finMostowskiDecoration(v0->v0,d0->wskiArcs) ==> Theorem herfinCCFGraphRepr0c: Svm(trans_thryvar) & (domain(trans_thryvar) = v0) & (FORALL w | (w in domain(wskiArcs)) ¥imp (((trans_thryvar~[w]) = { trans_thryvar~[cdr(p)] : p in (wskiArcs ¥ON {w}) }) & ((trans_thryvar~[w]) /= 0) )) & (0 in range(trans_thryvar)) & (FORALL y | (Y in range(trans_thryvar)) ¥imp Finite(Y)) & (FORALL x, y | (({X,Y} ¥incin v0) & ((trans_thryvar~[X]) = (trans_thryvar~[Y]))) ¥imp (X=Y)) & (FORALL y, x | (Y in v0) ¥imp (((trans_thryvar~[Y]) in (trans_thryvar~[X])) ¥eq ([X,Y] in wskiArcs))) -- Theorem herfinCCFGraphRepr0d: [Recursive characterization of the edges-to-membership translation] (trans_thryvar~[W]) = { trans_thryvar~[cdr(p)] : p in (wskiArcs ¥ON {W}) }. Proof: Suppose_not(w0) ==> Stat0: (trans_thryvar~[w0]) /= { trans_thryvar~[cdr(p)] : p in (wskiArcs ¥ON {w0}) } ()-->TherfinCCFGraphRepr0c(*) ==> Stat1: (FORALL w | (w in domain(wskiArcs)) ¥imp (((trans_thryvar~[w]) = { trans_thryvar~[cdr(p)] : p in (wskiArcs ¥ON {w}) }) & ((trans_thryvar~[w]) /= 0) )) & (domain(trans_thryvar) = v0) & (0 in range(trans_thryvar)) & Svm(trans_thryvar) Suppose ==> w0 in domain(wskiArcs) w0-->Stat1(*) ==> false; Discharge ==> AUTO Suppose ==> (trans_thryvar~[w0]) = 0 (Stat0*)ELEM ==> Stat2: { trans_thryvar~[cdr(p)] : p in (wskiArcs ¥ON {w0}) } /= 0 p0-->Stat2(Stat2*) ==> p0 in (wskiArcs ¥ON {w0}) (wskiArcs,{w0})-->Trestr_0(Stat2*) ==> p0 in wskiArcs (p0,wskiArcs,{w0})-->Trestr_1(Stat2*) ==> car(p0) = w0 (p0,wskiArcs)-->Tdomain_2(Stat1*) ==> false Discharge ==> AUTO (w0,trans_thryvar)-->Timage_3(*) ==> Stat4: ((trans_thryvar~[w0]) /= 0) & (w0 in domain(trans_thryvar)) Use_def(Extensional(v0,wskiArcs)) ==> AUTO Use_def(range)(Stat1) ==> Stat5: 0 in {cdr(p): p in trans_thryvar} trans_thryvar-->Timage_5(Stat1*) ==> trans_thryvar = {[x,trans_thryvar~[x]]: x in domain(trans_thryvar)} EQUAL(Stat5) ==> 0 in {cdr(p): p in {[x,trans_thryvar~[x]]: x in domain(trans_thryvar)}} SIMPLF(Stat5) ==> Stat6: 0 in {cdr([x,trans_thryvar~[x]]): x in domain(trans_thryvar)} x0-->Stat6(Stat6*) ==> ((trans_thryvar~[x0]) = 0) & (x0 in domain(trans_thryvar)) Suppose ==> x0 in domain(wskiArcs) x0-->Stat1(Stat6*) ==> false; Discharge ==> AUTO ()-->TherfinCCFGraphRepr0a(Stat6*) ==> Extensional(v0,wskiArcs) Suppose ==> x0 = w0 EQUAL(Stat4) ==> false; Discharge ==> AUTO (v0,wskiArcs,x0,w0)-->Textensionality2(Stat1*) ==> Stat7: not((FORALL z | [x0,z] notin wskiArcs) & (FORALL z | [w0,z] notin wskiArcs)) Suppose ==> Stat8: not (FORALL z | [w0,z] notin wskiArcs) z0-->Stat8(Stat8*) ==> [w0,z0] in wskiArcs (w0,z0,wskiArcs)-->Tdomain_3(Stat1*) ==> false Discharge ==> AUTO (Stat7*)ELEM ==> Stat9: not (FORALL z | [x0,z] notin wskiArcs) z1-->Stat9(Stat9*) ==> [x0,z1] in wskiArcs (x0,z1,wskiArcs)-->Tdomain_3(Stat6*) ==> false Discharge ==> QED -- -- Theorem herfinCCFGraphRepr1: (([X,Y] in wskiArcs) or ([Y,X] in wskiArcs)) ¥eq ({X,Y} in e0). Proof: Suppose_not(x0,y0) ==> AUTO ()-->TherfinCCFGraphRepr0a(*) ==> Stat1: (wskiArcs ¥incin (v0 ¥PROD v0)) & Orientates(wskiArcs,v0,e0) Assump ==> e0 ¥incin {{x,y}: x in v0, y in v0-{x}} Suppose ==> Stat2: {{car(p),cdr(p)}: p in wskiArcs | p = [car(p), cdr(p)]} /= {{car(p),cdr(p)}: p in wskiArcs} p0-->Stat2(Stat1*) ==> (p0 in (v0 ¥PROD v0)) & (p0 /= [car(p0), cdr(p0)]) (p0,v0,v0)-->Tcartesian_0(Stat2*) ==> false Discharge ==> AUTO Use_def(Orientates) ==> Stat3: ((([x0,y0] in wskiArcs) or ([y0,x0] in wskiArcs)) ¥neq ({x0,y0} in {{car(p),cdr(p)}: p in wskiArcs})) Suppose ==> Stat4: ({x0,y0} in {{car(p),cdr(p)}: p in wskiArcs}) & (not(([x0,y0] in wskiArcs) or ([y0,x0] in wskiArcs))) p1-->Stat4(Stat1*) ==> Stat5: ({x0,y0} = {car(p1),cdr(p1)}) & (p1 in (v0 ¥PROD v0)) & (p1 in wskiArcs) (p1,v0,v0)-->Tcartesian_0(Stat5*) ==> (p1 = [car(p1),cdr(p1)]) & (((x0=car(p1)) & (y0=cdr(p1))) or ((x0=cdr(p1)) & (y0=car(p1)))) Suppose ==> (x0=car(p1)) & (y0=cdr(p1)) EQUAL ==> false; Discharge ==> (y0=car(p1)) & (x0=cdr(p1)) EQUAL ==> false; Discharge ==> AUTO Suppose ==> Stat6: ({x0,y0} notin {{car(p),cdr(p)}: p in wskiArcs}) & ([x0,y0] in wskiArcs) [x0,y0]-->Stat6(Stat6*) ==> false; Discharge ==> Stat7: ({x0,y0} notin {{car(p),cdr(p)}: p in wskiArcs}) & ([y0,x0] in wskiArcs) [y0,x0]-->Stat7(Stat7*) ==> false Discharge ==> QED -- Theorem herfinCCFGraphRepr2: [Edges between vertices are modeled by membership under the translation] ({X,Y} ¥incin v0) ¥imp ((((trans_thryvar~[Y]) in (trans_thryvar~[X])) or ((trans_thryvar~[X]) in (trans_thryvar~[Y]))) ¥eq ({X,Y} in e0)). Proof: Suppose_not(x0,y0) ==> AUTO ()-->TherfinCCFGraphRepr0c(*) ==> Stat1: (FORALL y, x | (y in v0) ¥imp (((trans_thryvar~[y]) in (trans_thryvar~[x])) ¥eq ([x,y] in wskiArcs))) (y0,x0)-->Stat1(*) ==> ((trans_thryvar~[y0]) in (trans_thryvar~[x0])) ¥eq ([x0,y0] in wskiArcs) (x0,y0)-->Stat1(*) ==> ((trans_thryvar~[x0]) in (trans_thryvar~[y0])) ¥eq ([y0,x0] in wskiArcs) (x0,y0)-->TherfinCCFGraphRepr1(*) ==> false Discharge ==> QED -- -- The following theorem sets the ground for a proof that the range of the edges-to-membership translation is a transitive set. -- Theorem herfinCCFGraphRepr3: [Every image of the edges-to-membership translation is included in its range] (X in domain(trans_thryvar)) ¥imp ((trans_thryvar~[X]) ¥incin range(trans_thryvar)). Proof: Suppose_not(x0) ==> Stat0: ((trans_thryvar~[x0]) ¥nincin range(trans_thryvar)) & (x0 in domain(trans_thryvar)) ()-->TherfinCCFGraphRepr0c(*) ==> Stat1: Svm(trans_thryvar) & (domain(trans_thryvar) = v0) x0-->TherfinCCFGraphRepr0d ==> AUTO x1-->Stat0(Stat0*) ==> Stat2: (x1 in { trans_thryvar~[cdr(p)] : p in (wskiArcs ¥ON {x0}) }) & (x1 notin range(trans_thryvar)) (wskiArcs,{x0})-->Trestr_0(Stat2*) ==> (wskiArcs ¥ON {x0}) ¥incin wskiArcs ()-->TherfinCCFGraphRepr0a(Stat2*) ==> wskiArcs ¥incin (v0 ¥PROD v0) p1-->Stat2(Stat2*) ==> (p1 in (v0 ¥PROD v0)) & ((trans_thryvar~[cdr(p1)]) notin range(trans_thryvar)) (p1,v0,v0)-->Tcartesian_0(Stat2*) ==> cdr(p1) in v0 (cdr(p1),trans_thryvar~[cdr(p1)],trans_thryvar)-->Tdomain_3(Stat1*) ==> Stat3: [cdr(p1),trans_thryvar~[cdr(p1)]] notin trans_thryvar trans_thryvar-->Timage_5(Stat1,Stat1*) ==> trans_thryvar = {[x,trans_thryvar~[x]]: x in domain(trans_thryvar)} EQUAL(Stat3) ==> Stat4: [cdr(p1),trans_thryvar~[cdr(p1)]] notin {[x,trans_thryvar~[x]]: x in domain(trans_thryvar)} (cdr(p1))-->Stat4(Stat1*) ==> false Discharge ==> QED -- -- The following theorem states that the range of the edges-to-membership translation is a transitive set. -- Theorem herfinCCFGraphRepr4: [Transitivity of the range of the edges-to-membership translation] {y in range(trans_thryvar) | y ¥nincin range(trans_thryvar)} = 0. Proof: Suppose_not() ==> Stat0: {y in range(trans_thryvar) | y ¥nincin range(trans_thryvar)} /= 0 y0-->Stat0(*) ==> (y0 in range(trans_thryvar)) & (y0 ¥nincin range(trans_thryvar)) ()-->TherfinCCFGraphRepr0c(*) ==> Svm(trans_thryvar) & (domain(trans_thryvar) = v0) trans_thryvar-->Timage_5(*) ==> trans_thryvar = {[x,trans_thryvar~[x]]: x in domain(trans_thryvar)} Use_def(range) ==> y0 in {cdr(p): p in trans_thryvar} EQUAL ==> y0 in {cdr(p): p in {[x,trans_thryvar~[x]]: x in domain(trans_thryvar)}} SIMPLF ==> Stat1: y0 in {cdr([x,trans_thryvar~[x]]): x in domain(trans_thryvar)} x0-->Stat1(Stat1) ==> (y0 = (trans_thryvar~[x0])) & (x0 in domain(trans_thryvar)) x0-->TherfinCCFGraphRepr3(*) ==> false Discharge ==> QED -- -- The following theorem recapitulates some of the facts already proved in Theorem $herfinCCFGraphRepr0c$ (which cannot be exported -- from the present THEORY, because its claim involves the private symbol 'wskiArcs'); it also says something new, -- namely that the range of the edges-to-membership translation is a hereditarily finite set. -- Theorem herfinCCFGraphRepr5: [Compendium of properties of the edges-to-membership translation] Svm(trans_thryvar) & (domain(trans_thryvar) = v0) & (0 /= range(trans_thryvar)) & HerFin(range(trans_thryvar)). Proof: Suppose_not() ==> AUTO Use_def(HerFin(range(trans_thryvar))) ==> AUTO ()-->TherfinCCFGraphRepr0c(*) ==> Stat1: (FORALL y | (y in range(trans_thryvar)) ¥imp Finite(y)) & Svm(trans_thryvar) & (domain(trans_thryvar) = v0) & (not (Finite(range(trans_thryvar)) & (FORALL y in range(trans_thryvar) | HerFin(y)))) trans_thryvar-->Timage_5(Stat1*) ==> trans_thryvar = {[x,trans_thryvar~[x]]: x in domain(trans_thryvar)} -- -- The following TELEM step makes implicit use of the THEORY $isSvm$ seen at the beginning of this scenario. -- TELEM ==> range({[x,trans_thryvar~[x]]: x in domain(trans_thryvar)}) = {trans_thryvar~[x]: x in domain(trans_thryvar)} EQUAL(Stat1) ==> Stat2: (not (Finite({trans_thryvar~[x]: x in v0}) & (FORALL y in {trans_thryvar~[x]: x in v0} | HerFin(y)))) Assump ==> Finite(v0) APPLY() finiteImage(s0->v0,f(X)->(trans_thryvar~[X])) ==> Finite({trans_thryvar~[x]: x in v0}) (Stat2*)ELEM ==> Stat3: not (FORALL y in {trans_thryvar~[x]: x in v0} | HerFin(y)) y0-->Stat3(Stat3*) ==> Stat4: (y0 in {trans_thryvar~[x]: x in v0}) & (not HerFin(y0)) x0-->Stat4(Stat4*) ==> (x0 in v0) & (y0 = trans_thryvar~[x0]) & (not HerFin(y0)) EQUAL(Stat4) ==> not HerFin(trans_thryvar~[x0]) -- Loc_def ==> Stat5: a0 = arb({trans_thryvar~[x] : x in v0 | not HerFin(trans_thryvar~[x])}) Suppose ==> Stat6: {trans_thryvar~[x] : x in v0 | not HerFin(trans_thryvar~[x])} = 0 x0-->Stat6(Stat4*) ==> false Discharge ==> AUTO (Stat5)ELEM ==> Stat7: (a0 in {trans_thryvar~[x] : x in v0 | not HerFin(trans_thryvar~[x])}) & (a0 * {trans_thryvar~[x] : x in v0 | not HerFin(trans_thryvar~[x])} = 0) x1-->Stat7(Stat7*) ==> (x1 in v0) & (a0 = trans_thryvar~[x1]) & (not HerFin(trans_thryvar~[x1])) Use_def(HerFin(a0)) ==> AUTO EQUAL(Stat7) ==> Stat8: not (Finite(a0) & (FORALL x in a0 | HerFin(x))) Suppose ==> not Finite(a0) a0-->Stat1(Stat1*) ==> a0 notin range(trans_thryvar) (x1,a0,trans_thryvar)-->Tdomain_3(Stat8*) ==> [x1,a0] notin trans_thryvar trans_thryvar-->Timage_5(Stat1,Stat1*) ==> trans_thryvar = {[x,trans_thryvar~[x]]: x in domain(trans_thryvar)} EQUAL(Stat7) ==> Stat9: [x1,trans_thryvar~[x1]] notin {[x,trans_thryvar~[x]]: x in domain(trans_thryvar)} x1-->Stat9(Stat1*) ==> false Discharge ==> AUTO x1-->TherfinCCFGraphRepr0d(Stat7*) ==> a0 = { trans_thryvar~[cdr(p)] : p in (wskiArcs ¥ON {x1}) } (wskiArcs,{x1})-->Trestr_0(Stat8*) ==> (wskiArcs ¥ON {x1}) ¥incin wskiArcs ()-->TherfinCCFGraphRepr0a(Stat8*) ==> wskiArcs ¥incin (v0 ¥PROD v0) (Stat8)ELEM ==> Stat10: not (FORALL x in a0 | HerFin(x)) x2-->Stat10(Stat7*) ==> Stat11: (x2 in { trans_thryvar~[cdr(p)] : p in (wskiArcs ¥ON {x1}) }) & (x2 notin {trans_thryvar~[x] : x in v0 | not HerFin(trans_thryvar~[x])}) & (not HerFin(x2)) (p1,cdr(p1))-->Stat11(Stat11*) ==> (x2 = (trans_thryvar~[cdr(p1)])) & (p1 in (wskiArcs ¥ON {x1})) & (not HerFin(x2)) & (not((cdr(p1) in v0) & (not HerFin(trans_thryvar~[cdr(p1)])))) EQUAL(Stat11) ==> not HerFin(trans_thryvar~[cdr(p1)]) (Stat8*)ELEM ==> (p1 in (v0 ¥PROD v0)) & (cdr(p1) notin v0) (p1,v0,v0)-->Tcartesian_0(Stat11*) ==> false Discharge ==> QED -- ENTER_THEORY Set_theory -- --DISPLAY herfinCCFGraphRepr -- --THEORY herfinCCFGraphRepr(v0,e0) -- (e0 ¥incin {{x,y}: x in v0, y in v0-{x}}) & Finite(v0) -- HasSpanningTree(v0,e0) & ClawFreeG(v0,e0) --==>(trans_thryvar) -- Svm(trans_thryvar) & (domain(trans_thryvar) = v0) -- (FORALL x, y | (({X,Y} ¥incin v0) & ((trans_thryvar~[X]) = (trans_thryvar~[Y]))) ¥imp (X=Y)) -- (FORALL x, y | ({X,Y} ¥incin v0) ¥imp ((((trans_thryvar~[Y]) in (trans_thryvar~[X])) or ((trans_thryvar~[X]) in (trans_thryvar~[Y]))) ¥eq ({X,Y} in e0))) -- ({y in range(trans_thryvar) | y ¥nincin range(trans_thryvar)} = 0) -- (range(trans_thryvar) /= 0) & HerFin(range(trans_thryvar)) --END herfinCCFGraphRepr -- --END HERE