--BEGIN HERE -- -- \section{Basic laws on the union-set global operation} -- Def unionset: [Family of all members of members of a set] Un(X) := {u: v in X, u in v} -- -- -- We show here that the union set of a set $s$ is the set-theoretic 'upper bound' of all its elements, i.e. -- the smallest set which includes all these elements. -- Theorem 2: [Union set as an upper bound] ((X in S) 可mp (X 可ncin Un(S))) & ((FORALL y in S | y 可ncin X) 可mp (Un(S) 可ncin X)). Proof: Suppose_not(t,s) ==> ((t 叩incin Un(s)) & (t in s)) or ((FORALL y in s | y 可ncin t) & (Un(s) 叩incin t)) -- -- For if not, one of the two clauses of our theorem must be false. By definition of '$Un$', this -- cannot be the first clause, so it must be the second. -- Use_def(Un(s)) ==> AUTO Suppose ==> Stat1: (t 叩incin Un(s)) & (t in s) c-->Stat1 ==> Stat2: (c notin {z: y in s, z in y}) & (c in t) (t,c)-->Stat2 ==> false; Discharge ==> Stat3: (Un(s) 叩incin t) & (FORALL y in s | y 可ncin t) -- -- But a second use of the definition of '$Un$' shows that this case is also impossible, proving our theorem. -- d-->Stat3 ==> Stat4: (d in {z: y in s, z in y}) & (FORALL y in s | y 可ncin t) & (d notin t) (b,a,b)-->Stat4 ==> false; Discharge ==> QED -- THEORY imageOfDoubleton(f(X),x0,x1) END imageOfDoubleton -- ENTER_THEORY imageOfDoubleton -- Theorem imageOfDoubleton: [The image of a doubleton is either a doubleton or a singleton] ({f(v): v in 0 } = 0) & ({f(v): v in {x0} } = {f(x0)}) & ({f(v): v in {x0,x1} } = {f(x0),f(x1)}). Proof: Suppose_not() ==> AUTO -- -- Ref has the built-in ability to reduce ${f(v): v in 0}$ to $0$ and ${f(v): v in {x0}}$ to ${f(x0)}$; -- hence we are left with only the doubleton to consider. Let $c$ belong to one of -- ${f(v): v in {x0,x1}}$ and ${f(x0),f(x1)}$ but not the other. After excluding, through -- variable-substitution, the case $c notin {f(v): v in {x0,x1}}$, we easily discard both possibilities -- $c=f(x0)$ and $c=f(x1)$, through variable-substitution and equality propagation. -- SIMPLF ==> Stat1: {f(v): v in {x0,x1} } /= {f(x0),f(x1)} c-->Stat1 ==> (c in {f(v): v in {x0,x1}}) 叩eq (c in {f(x0),f(x1)}) Suppose ==> Stat2: (c notin {f(v): v in {x0,x1}}) & (c notin {f(v): v in {x0,x1}}) (x0,x1)-->Stat2 ==> AUTO Discharge ==> Stat3: (c in {f(v): v in {x0,x1}}) & (c notin {f(x0),f(x1)}) xp-->Stat3 ==> (xp in {x0,x1}) & (f(xp) /= f(x0)) & (f(xp) /= f(x1)) Suppose ==> xp = x0 EQUAL ==> false Discharge ==> xp = x1 EQUAL ==> false Discharge ==> QED -- ENTER_THEORY Set_theory -- --DISPLAY imageOfDoubleton -- --THEORY imageOfDoubleton(f(X),x0,x1) -- ({f(v): v in 0 } = 0) & ({f(v): v in {x0} } = {f(x0)}) & ({f(v): v in {x0,x1} } = {f(x0),f(x1)}) --END imageOfDoubleton -- Theorem 2a: [Union of doubletons and singletons] (Z = {X,Y}) 可mp (Un(Z) = (X + Y)). Proof: Suppose_not(z0,x0,y0) ==> Stat0: (z0 = {x0,y0}) & (Un(z0) /= (x0 + y0)) -- -- Under the assumption that $(z0 = {x0,y0}) & (Un(z0) /= (x0 + y0))$ can hold, two citations -- of Theorem 2 enable us to get $x0 可ncin Un(z0)$ and $y0 可ncin Un(z0)$ from $z0={x0,y0}$. -- (x0,z0)-->T2 ==> AUTO (y0,z0)-->T2 ==> AUTO -- -- A third citation of the same Theorem 2 enables us to derive from $Un(z0) /= (x0 + y0)$ that -- some element of $z0={x0,y0}$ is not included in $x0+y0$, which is manifestly absurd. -- (x0+y0,z0)-->T2(Stat0*) ==> Stat1: not(FORALL y in z0 | y 可ncin (x0+y0)) v-->Stat1(Stat0,Stat0*) ==> (v in {x0,y0}) & (v 叩incin (x0+y0)) (Stat1*)Discharge ==> QED -- Theorem 2b: [Union of union] Un(Un(X)) = Un({Un(y): y in X}). Proof: Suppose_not(x0) ==> AUTO Use_def(Un) ==> {z: y in {u: v in x0, u in v}, z in y} /= {s: r in {Un(y): y in x0}, s in r} SIMPLF ==> Stat1: {z: v in x0, u in v, z in u} /= {s: y in x0, s in Un(y)} z0-->Stat1 ==> AUTO Suppose ==> Stat3: (z0 in {z: v in x0, u in v, z in u}) & (z0 notin {s: y in x0, s in Un(y)}) Use_def(Un(v0)) ==> AUTO (v0,u0,z,v0,z0)-->Stat3(Stat1*) ==> Stat4: (z0 notin {z: u in v0, z in u}) & (v0 in x0) & (u0 in v0) & (z0 in u0) (u0,z0)-->Stat4(Stat4*) ==> false Discharge ==> Stat5: (z0 in {s: y in x0, s in Un(y)}) & Stat6: (z0 notin {z: v in x0, u in v, z in u}) Use_def(Un(y0)) ==> AUTO (y0,s0)-->Stat5(Stat5*) ==> Stat7: (z0 in {s: u in y0, s in u}) & (y0 in x0) (u1,s1)-->Stat7(Stat7*) ==> (z0 in u1) & (u1 in y0) (y0,u1,z0)-->Stat6(Stat7*) ==> false Discharge ==> QED -- Theorem 2c: [Additivity of monadic union] Un(X + Y) = (Un(X) + Un(Y)). Proof: Suppose_not(x0,y0) ==> AUTO {x0,y0}-->T2b ==> Un(Un({x0,y0})) = Un({Un(v): v in {x0,y0}}) APPLY() imageOfDoubleton(f(X)->Un(X),x0->x0,x1->y0) ==> {Un(v): v in {x0,y0}} = {Un(x0),Un(y0)} ({x0,y0},x0,y0)-->T2a ==> Un({x0,y0}) = (x0 + y0) ({Un(x0),Un(y0)},Un(x0),Un(y0))-->T2a ==> Un({Un(x0),Un(y0)}) = (Un(x0) + Un(y0)) EQUAL ==> false Discharge ==> QED -- Theorem 2d: [Monotonicity of monadic union] (X 可ncin Y) 可mp (Un(X) 可ncin Un(Y)). Proof: Suppose_not(x0,y0) ==> (y0 = (x0 + y0)) & (Un(x0) 叩incin Un(y0)) (x0,y0)-->T2c ==> AUTO EQUAL ==> Un(y0) = Un(x0) + Un(y0) Discharge ==> QED -- -- The statement of the following technical lemma may look unreasonably 'twisted'; -- however, this will offer the reward of versatility; in fact, by simple citation, this -- statement can be declined in at least three ways: -- $Un(X + {Y}) = (Y + Un(X))$, -- $(Y in Z) 可mp (Un(Z) = (Y + Un(Z - {Y})))$, -- $(Z /= 0) 可mp (Un(Z) = (arb(Z) + Un(Z - {arb(Z)})))$. -- Theorem 2q: [Union of union, 2] ((Y in Z) & (X in {Z, Z - {Y}})) 可mp (Un(Z) = (Y + Un(X))). Proof: Suppose_not(y0,z0,x0) ==> AUTO ELEM ==> z0 = x0 + {y0} EQUAL ==> Un(x0 + {y0}) /= (y0 + Un(x0)) ({y0},y0,y0)-->T2a ==> AUTO (x0,{y0})-->T2c ==> false Discharge ==> QED -- -- An alternative, self-contained proof of the following theorem, which is the proof actually shown -- in the proof-pearl paper, is saved after the line "--END HERE" marking at the end of this scenario. -- Theorem 2e: [Union of adjunction] Un(X + {Y}) = (Y + Un(X)). Proof: Suppose_not(x0,y0) ==> AUTO (y0,x0+{y0},x0)-->T2q(*) ==> false Discharge ==> QED -- -- -- \section{Transitive sets} -- -- Def transitivity: [Transitive, aka full, set] Trans(T) := {y in T | y 叩incin T} = 0 -- Theorem 3a: [The unionset of a transitive set is included in it] Trans(T) 占q (T incs Un(T)). Proof: Suppose_not(t) ==> AUTO Use_def(Un(t)) ==> AUTO Use_def(Trans(t)) ==> AUTO Suppose ==> Stat1: (t 叩incs Un(t)) & Trans(t) c-->Stat1(*) ==> Stat2: (c in {u: v in t, u in v}) & ({y in t | y 叩incin t} = 0) & (c notin t) (v,u,v)-->Stat2(Stat2*) ==> false Discharge ==> Stat3: ({y in t | y 叩incin t} /= 0) & (t incs {u: v in t, u in v}) Loc_def ==> a = arb(d - t) d-->Stat3(Stat3) ==> Stat4: (a notin {u: v in t, u in v}) & (d in t) & (a in d) & (a notin t) (d,a)-->Stat4(Stat4*) ==> false Discharge ==> QED -- Theorem 3c: [For a transitive set, elements are also subsets] (Trans(T) & (X in T)) 可mp (X 可ncin T). Proof: Suppose_not(t,x) ==> AUTO t-->T3a ==> Stat1: (t = t+{x}) & (not (Un(t) incs x + Un(t))) (t,x)-->T2e ==> AUTO EQUAL(Stat1) ==> false Discharge ==> QED -- Theorem 3d: [Trapping phenomenon for trivial sets] (Trans(S) & (X in S) & (Z in S) & (X notin Z) & (Z notin X) & ((S-{X,Z}) 可ncin {0,{0}})) 可mp (S 可ncin {0,{0},{{0}},{0,{0}}}). Proof: Suppose_not(s,x,z) ==> AUTO (s,x)-->T3c ==> AUTO (s,z)-->T3c ==> AUTO Discharge ==> QED -- -- Any strict subset of a transitive set $t$, owns a subset in $t$ which does not belong to it. -- -- Theorem 4a: [Peddicord's lemma] (Trans(T) & (S 可ncin T) & (S /= T) & (A = arb(T-S))) 可mp ((A 可ncin S) & (A in (T-S))). Proof: Suppose_not(t,s,a) ==> AUTO (t,a)-->T3c ==> a 可ncin t Discharge ==> QED -- Theorem 4b: [$0$ belongs to every non-null transitive set $t$, ${0}$ also does if $t 叩incin {0}$, and so on] (Trans(T) & (N in {0,{0},{0,{0}}}) & (T 叩incin N)) 可mp ((N 可ncin T) & ((N in T) or ((N = {0,{0}}) & ({{0}} in T)))). Proof: Suppose_not(t,n) ==> AUTO -- -- The '(*)' context restriction in the following -- three steps serves to hide the semantics of $arb$: -- which, to the limited extent necessary here, has been -- captured by the preceding Peddicord's lemma. -- (t,0,arb(t-0))-->T4a(*) ==> 0 in t (t,{0},arb(t-{0}))-->T4a(*) ==> {0} in t (t,{0,{0}},arb(t-{0,{0}}))-->T4a(*) ==> false Discharge ==> QED -- Theorem 4c: [Source removal from a transitive set does not disrupt transitivity] (Trans(S) & (S incs T) & ((S - T) * Un(S) = 0)) 可mp Trans(T). Proof: Suppose_not(s,t) ==> AUTO Use_def(Trans) ==> Stat1: ({y in t | y 叩incin t} /= 0) & ({y in s | y 叩incin s} = 0) -- -- Assuming that $s$ is transitive, that $t$ equals $s$ deprived of some sources and that $t$ is not transitive, -- there must be an element $y$ of $t$ which is not a subset of $t$, so that a $z in y$ exists which does -- not belong to $t$. Due to the transitivity of $s$, $y$ is included in $s$ and hence $z$ belongs to $s$; -- hence, under the assumption that $s - t$ and $Un(s)$ are disjoint, $z$ does not belong to $Un(s)$. -- (y,y)-->Stat1 ==> Stat2: (y 叩incin t) & (y in s) & (y 可ncin s) Use_def(Un(s)) ==> AUTO z-->Stat2 ==> Stat3: (z notin {u: v in s, u in v}) & (z in y) -- -- However, this is untenable. -- (y,z)-->Stat3 ==> false Discharge ==> QED -- \section{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 pow: [Family of all subsets of a given set] pow(S) := { x : x 可ncin S } -- Def Fin: [Finiteness property] Finite(F) := (FORALL g in (pow(pow(F)) - {0}) | (EXISTS m | (g * pow(m)) = {m})) -- Theorem 23: [Monotonicity of powerset] (S incs X) 可mp ((pow(X) + {0,X}) 可ncin pow(S)). Proof: Suppose_not(s0,x0) ==> AUTO Set_monot ==> { x : x 可ncin x0 } 可ncin { x : x 可ncin s0 } Use_def(pow) ==> Stat1: (0 notin { x : x 可ncin s0 }) or (x0 notin { x : x 可ncin s0 }) (0,x0)-->Stat1 ==> false Discharge ==> QED -- Theorem 24: [Monotonicity of finiteness] ((Y incs X) & Finite(Y)) 可mp Finite(X). Proof: Suppose_not(y0,x0) ==> AUTO (y0,x0)-->T23(*) ==> 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))-->T23(*) ==> 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 finiteInduction1: (EXISTS m | ({s 可ncin 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 可ncin s0 | P(s)})-->Stat1 ==> {s 可ncin s0 | P(s)} notin (pow(pow(s0)) - {0}) Suppose ==> Stat2: s0 notin {s 可ncin s0 | P(s)} s0-->Stat2 ==> false; Discharge ==> {s 可ncin s0 | P(s)} notin (pow(pow(s0))) Use_def(pow) ==> Stat3: {s 可ncin s0 | P(s)} notin {y: y 可ncin {z: z 可ncin s0}} ({s 可ncin s0 | P(s)})-->Stat3 ==> Stat4: {s 可ncin s0 | P(s)} 叩incin {z: z 可ncin s0} s1-->Stat4 ==> Stat5: (s1 in {s: s 可ncin s0 | P(s)}) & (s1 notin {z: z 可ncin s0}) (s,s1)-->Stat5(Stat5*) ==> false Discharge ==> QED -- APPLY(v1_thryvar:fin_thryvar) Skolem() ==> Theorem finiteInduction0: ({s 可ncin s0 | P(s)} * pow(fin_thryvar)) = {fin_thryvar} -- Theorem finiteInduction2: [Minimal finite set satisfying $P$] (S 可ncin fin_thryvar) 可mp( Finite(S) & ( P(S) 占q (S = fin_thryvar)) ). Proof: Suppose_not(s1) ==> AUTO ()-->TfiniteInduction0 ==> (({s 可ncin s0 | P(s)} * pow(fin_thryvar)) = {fin_thryvar}) & Stat1: (fin_thryvar in {s 可ncin s0 | P(s)}) ()-->Stat1 ==> (fin_thryvar 可ncin s0) & P(fin_thryvar) Assump ==> Finite(s0) (s0,fin_thryvar)-->T24 ==> Finite(fin_thryvar) (fin_thryvar,s1)-->T24 ==> P(s1) 叩eq (s1 = fin_thryvar) Suppose ==> s1 = fin_thryvar EQUAL ==> false; Discharge ==> (s1 notin ({s 可ncin s0 | P(s)} * pow(fin_thryvar))) & P(s1) Suppose ==> s1 notin pow(fin_thryvar) Use_def(pow) ==> Stat2: s1 notin {y: y 可ncin fin_thryvar} s1--> Stat2 ==> false Discharge ==> Stat3: s1 notin {s 可ncin 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 可ncin fin_thryvar) 可mp ( Finite(S) & ( P(S) 占q (S = fin_thryvar)) )) --END finiteInduction -- -- \section{Some combinatorics of the union-set operation} -- Theorem 31d: [Unionset of 0 and 1] (Y 可ncin {0}) 占q (Un(Y) = 0). Proof: Suppose_not(x0) ==> AUTO Use_def(Un(x0)) ==> AUTO Suppose ==> Stat1: { z: y in x0, z in y } /= 0 (y0,z1)-->Stat1 ==> false; Discharge ==> Stat2: (x0 叩incin {0}) & ({ z: y in x0, z in y } = 0) (y1,y1,arb(y1))-->Stat2 ==> false Discharge ==> QED -- Theorem 31e: [Monotonicity of a set obtained through removal] (Un(X-{Y}) incs (Un(X)-Y)) & (Un(X) incs Un(X-{Y})). Proof: Suppose_not(x,y) ==> AUTO (x-{y},x)-->T2d(*) ==> Stat1: Un(x-{y}) 叩incs (Un(x)-y) c-->Stat1(Stat1*) ==> Stat2: (c in (Un(x)-y)) & (c notin Un(x-{y})) Use_def(Un) ==> Stat3: (c in {u: v in x, u in v}) & (c notin {u: v in (x-{y}), u in v}) & (c notin y) (v0,u0,v0,u0)-->Stat3(Stat3*) ==> false Discharge ==> QED -- Theorem 31f: [Unionset of a set obtained through removal followed by adjunction] ((Un(M) incs P) & ((Q+R) = (P+S))) 可mp (Un((M-{P})+{Q,R}) = (Un(M) + S)). Proof: Suppose_not(m,p,q,r,s) ==> AUTO TELEM ==> ((m-{p})+{q})+{r} = (m-{p})+{q,r} EQUAL ==> Un(((m-{p})+{q})+{r}) = Un((m-{p})+{q,r}) (m-{p},q)-->T2e ==> AUTO ((m-{p})+{q},r)-->T2e(*) ==> Un((m-{p})+{q,r}) = Un(m-{p}) + (p+s) (m,p)-->T31e(*) ==> false Discharge ==> QED -- Theorem 31g: [Incomparability of pre-pivotal elements] ((Y in X) & (X in Z) & (X in S) & (Z in S)) 可mp (Y in Un(S*Un(S))). Proof: Suppose_not(y,x,z,s) ==> (Y in X) & (X in Z) & (X in S) & (Z in S) & (Y notin Un(S*Un(S))) Use_def(Un) ==> Stat1: y notin {v: u in s * Un(s), v in u} Use_def(Un(s)) ==> AUTO (x,y)-->Stat1(*) ==> Stat2: x notin {t: w in s, t in w} (z,x)-->Stat2(*) ==> false Discharge ==> QED -- -- Preparatory to a technique to which we will resort for extending perfect matchings, -- we introduce the following trivial combinatorial lemma: -- Theorem 31h: [Less-one lemma for unionset] ((Un(M) = T-{C}) & (S=T+X+{V}) & (Y in S*{C,V})) 可mp (EXISTS d | Un(M+{X+{Y}}) = S-{d}). Proof: Suppose_not(m,t,c,s,x,v,y) ==> Stat0: (not(EXISTS d | Un(m+{x+{y}}) = s-{d})) & (Un(m) = t-{c}) & (s=t+x+{v}) & ((y = v) or ((c = y) & (y in s))) -- -- For, supposing the contrary, $Un(m+{x+{y}})$ would differ from each of $s-{s}$, $s-{c}$, and $s-{v}$, the first of which equals $s$. -- Thanks to Theorem 2e, we can rewrite $Un(m+{x+{y}})$ as $x+{y}+Un(m)$; but then the decidable fragment of set theory known as -- 'multi-level syllogistic with singleton' immediately yields a contradiction. -- s-->Stat0(*) ==> Un(m+{x+{y}}) /= s c-->Stat0(*) ==> Un(m+{x+{y}}) /= (s-{c}) v-->Stat0(*) ==> Un(m+{x+{y}}) /= (s-{v}) (m,x+{y})-->T2e ==> AUTO EQUAL ==> Stat1: ((x+{y} + Un(m)) /= (s-{c})) & ((x+{y} + Un(m)) /= (s-{v})) & ((x+{y} + Un(m)) /= s) (Stat0,Stat1*)Discharge ==> QED -- -- -- Theorem 32: [Finite, non-null sets own sources] (Finite(F) & (F /= 0)) 可mp ((F - Un(F)) /= 0). Proof: Suppose_not(f1) ==> AUTO -- -- Arguing by contradiction, suppose that there are counterexamples to the claim. -- Then, by exploiting finite induction, we can pick a minimal counterexample, $f0$. -- APPLY(fin_thryvar:f0) finiteInduction(s0->f1,P(S)->((S/=0) & ((S - Un(S)) = 0))) ==> Stat0: (FORALL s | (s 可ncin f0) 可mp ( Finite(s) & ( ((s/=0) & ((s - Un(s)) = 0)) 占q (s = f0)) )) Loc_def ==> a = arb(f0) f0-->Stat0(Stat0) ==> Stat1: Finite(f0) & (a in f0) & (f0 - Un(f0) = 0) -- -- Momentarily supposing that $f0={a}$, one gets $Un(f0) 叩incin a$, because $Un(f0) 可ncin a$ would imply -- $f0-Un(f0) incs {a}-a$ and hence would imply the emptiness of ${a}-a$, entailing the manifest absurdity -- $a in a$. But, on the other hand, $Un({a}) 可ncin a$ trivially holds; therefore -- we must exclude that $f0$ is a singleton ${a}$. -- Suppose ==> (f0 = {a}) & (Un(f0) 叩incin a) EQUAL ==> Un({a}) 叩incin a Use_def(Un) ==> {u: v in {a}, u in v} 叩incin a SIMPLF ==> false Discharge ==> AUTO -- -- Due to our minimality assumption, the strict non-null subset $f0 - {arb(f0)}$ of $f0$ cannot be a -- counterexample to the claim; therefore it has sources and hence $f0 - Un(f0 - {arb(f0)}) /= 0$. -- (f0-{a},a)-->T2e(Stat1,Stat1*) ==> (Un((f0 - {a})+{a}) = Un(f0 - {a}) + a) & ((f0 - {a}) + {a} = f0) (f0-{a})-->Stat0(Stat1*) ==> Stat2: f0-Un(f0-{a}) /= 0 -- -- Since $arb(f0)$ does not intersect $f0$, the inequality just found conflicts with the equality -- $f0 - (Un(f0 - {arb(f0)}) + arb(f0)) = 0$ which one gets from Theorem 2e through equality propagation. -- EQUAL ==> (f0 - (Un(f0 - {a}) + a) = 0) & (a = arb(f0)) (Stat2)Discharge ==> QED -- -- -- \section{Claw-free, transitive sets and their pivots} -- -- An $in$-\emph{claw} is defined to be a pair $Y,F$ such that -- (1) $F$ has at least three elements, -- (2) no element of $F$ belongs to any other element of $F$, -- (3) either $Y$ belongs to all elements of $F$ or -- there is a $W$ in $Y$ such that $Y$ belongs to all elements of $F-{W}$. -- Def claw: [Pair characterizing an $in$-claw, possibly endowed with more than 3 el'ts] MembClaw(Y,F) := (F * Un(F) = 0) & (EXISTS x,z,w | (F incs {x,z,w}) & (x /= z) & (w notin {x,z}) & ({w} * Y incs {v in F | Y notin v})) -- -- The transitivity assumption is omitted here, but it will become explicit in the theorems -- pertaining to claw-freeness. -- Def clawFreeness: [Claw-freeness in a membership digraph] ClawFree(S) := (FORALL y in S, e 可ncin S | not MembClaw(y, e) ) -- Theorem clawFreeness_a: [Subsets of claw-free sets are claw-free] (ClawFree(S) & (T 可ncin S)) 可mp ClawFree(T). Proof: Suppose_not(s,t) ==> AUTO Use_def(ClawFree) ==> Stat1: (not((FORALL y in t, e 可ncin t | not MembClaw(y, e) ))) & (FORALL y in s, e 可ncin s | not MembClaw(y, e) ) (y,e,y,e)-->Stat1(*) ==> false Discharge ==> QED -- Theorem clawFreeness_b: [Any potential $in$-claw must have a bypass] (ClawFree(S) & (S incs {Y,X,Z,W}) & (Y in (X*Z)) & (W in Y) & (X notin Z+{Z}) & (Z notin X)) 可mp (W in (X+Z)). Proof: Suppose_not(s,y,x,z,w) ==> AUTO Use_def(ClawFree) ==> Stat0: (FORALL y in s, e 可ncin s | not MembClaw(y, e) ) & (x notin w) & (z notin w) & (x notin z) & (w notin x) & (w notin z) & (z notin x) & (x /= z) & (w in y) & (y in (x*z)) Loc_def ==> Stat1: e = {x,z,w} Use_def(MembClaw(y,e)) ==> AUTO (y,e)-->Stat0(*) ==> not((e * Un(e) = 0) & (EXISTS x,z,w | (e incs {x,z,w}) & (x /= z) & (w notin {x,z}) & ({w} * y incs {v in e | y notin v}))) EQUAL ==> Un(e) = Un({x,z,w}) Suppose ==> Stat2: e * Un(e) /= 0 Use_def(Un(e)) ==> AUTO c-->Stat2(Stat2*) ==> Stat3: (c in {u: v in e, u in v}) & (c in e) (v0,u0)-->Stat3(Stat1,Stat1*) ==> Stat4: (v0 in {x,z,w}) & (c in {x,z,w}) & (c in v0) (Stat0,Stat4*)Discharge ==> Stat5: (not (EXISTS x,z,w | (e incs {x,z,w}) & (x /= z) & (w notin {x,z}) & ({w} * y incs {v in e | y notin v}))) (x,z,w)-->Stat5(Stat0*) ==> Stat6: {w} * y 叩incs {v in e | y notin v} d-->Stat6(Stat6*) ==> Stat7: (d in {v in e | y notin v}) & (d notin {w} * y) ()-->Stat7(Stat1,Stat1*) ==> Stat8: (d in {x,z,w}) & (y notin d) (Stat0,Stat8,Stat7*)Discharge ==> QED -- THEORY pivotsForClawFreeness(s0) ClawFree(s0) & Finite(s0) & Trans(s0) s0 叩incin {0} END pivotsForClawFreeness -- ENTER_THEORY pivotsForClawFreeness -- -- -- -- By way of first approximation, we want to select from each finite transitive set $s$ not included in ${0}$ -- a 'pivotal pair' consisting of an element $x$ of maximum rank in $s$ and an element $y$ of maximum rank -- in $x$. To avoid introducing the recursive notion of rank of a set, we slightly generalize the idea: -- for any set $s$ (not necessarily finite or transitive) we define the \emph{frontier} of $s$ to consist of those -- elements $x$ of $s$ which own elements $y$ belonging to $s$ such that the length of no membership chain -- issuing from $y$, ending in $s$, and contained in $s$ ever exceeds 2. Any element $y$ which is thus -- related to an element $x$ of the frontier of $s$ will be called a \emph{pivot} of $s$. -- -- While entering this theory we do some preparatory work, by -- providing the definition of 'frontier' and the two main theorems about this notion: -- these are rather technical and hence they are being encapsulated inside the theory which uses them, -- although they do not depend on this theory; -- for the time being, in fact, we do not know whether the notion of frontier and the two theorems about it will -- turn out to be useful elsewhere, outside the THEORY pivotsForClawFreeness. -- -- Def frontier: [Frontier of a set] front(S) := { x in S | (x * S) - Un( S * Un(S)) /= 0 } -- Theorem frontier1: [Non-trivial finite sets have a non-null frontier] (Finite(S * Un(S)) & (S * Un(S) /= 0)) 可mp (front(S) /= 0). Proof: Suppose_not(s) ==> AUTO -- -- By Theorem 32, when $s*Un(s)$ is finite and non-null we can pick a $y in (s*Un(s)) - Un(s*Un(s))$, so that $y in s$, $y notin Un(s*Un(s))$, -- but $y in x$ holds for some $x in s$. -- (s*Un(s))-->T32 ==> Stat1: ((s*Un(s)) - Un(s*Un(s))) /= 0 Use_def(Un(s)) ==> AUTO y-->Stat1 ==> Stat2: (y in {u: v in s, u in v}) & (y in s) & (y notin Un(s*Un(s))) -- -- Supposing that $front(s)$ is empty and $x$ is as said, $x notin { x in s | (x * s) - Un( s * Un(s)) /= 0 }$ must hold, and -- hence no $y'$ belonging to $x*s$ can lie outside $Un( s * Un(s))$, which contradicts what we know about $y$. -- Use_def(front(s)) ==> AUTO (x,u)-->Stat2 ==> Stat3: (x notin {x1 in s | (x1 * s) - Un( s * Un(s)) /= 0 }) & (x in s) & (y in x) x-->Stat3 ==> false -- -- This contradiction gives us the desired conclusion. -- Discharge ==> QED -- -- Our next claim is that if we choose a pivot element $y$ of a transitive set $s$ from an element of the frontier of $s$, -- then removal of all predecessors of $y$ from $s$ leads to a transitive set $t$ such that $y$ is a source of $t$. -- Theorem frontier2: [Transitivity-preserving reduction of a transitive set] ( Trans(S) & (X in front(S)) & (Y in (X - Un(Un(S)))) & (T = {z in S | Y notin z}) ) 可mp (Trans(T) & (T 可ncin S) & (X notin T) & (Y in (T - Un(T)))). Proof: Suppose_not(s,x,y,t) ==> AUTO -- -- Arguing by contradiction, let $s,x,y,t$ be a counterexample to the claim. -- Taking the definition of $t$ into account to exploit monotonicity, we readily get $t 可ncin s$ and $x in t$. -- Set_monot ==> {z in s | y notin z} 可ncin {z: z in s} Suppose ==> Stat0: x in {z in s | y notin z} ()-->Stat0 ==> false; Discharge ==> x notin t -- -- Now taking the definition of $front$ into account, we can simplify our initial assumption to the following: -- Use_def(front) ==> Stat1: x in { xp in s | (xp * s) - Un( s * Un(s)) /= 0 } ()-->Stat1 ==> Trans(s) & (x in s) & ((x * s) - Un( s * Un(s) ) /= 0) & (y in (x - Un(Un(s)))) & (t = {z in s | y notin z}) & Trans(s) & (not (Trans(t) & (y in (t - Un(t))))) -- -- Since $s$ is transitive, if $t$ were not transitive then, by Theorem 4c, -- $s-t$ would have an element $z$ not being a source of $s$. -- But then $y$ would belong to $z in Un(s)$, which conflicts with $y$ being a pivot. -- Suppose ==> not Trans(t) (s,t)-->T4c ==> Stat2: (s-t) * Un(s) /= 0 Use_def(Un(s)) ==> AUTO z-->Stat2 ==> Stat3: (z in {up: wp in s, up in wp}) & (z notin {zp in s | y notin zp}) & (z in s) (v,a,z)-->Stat3(Stat3*) ==> (y in z) & (z in v) & (v in s) Use_def(Un(Un(s))) ==> AUTO EQUAL(Stat1) ==> y notin {u: w in {up: wp in s, up in wp}, u in w} SIMPLF ==> Stat4: y notin {u: wp in s, w in wp, u in w} (v,z,y)-->Stat4(Stat1*) ==> false Discharge ==> (y in Un(t)) or (y notin t) -- -- Now knowing that $Trans(t)$, we must consider the other possibily, namely that $y notin (t - Un(t))$. -- However, after expanding $t$ and $Un(t)$ according to their definitions,... -- Use_def(Un(t)) ==> AUTO Use_def(Trans(s)) ==> AUTO EQUAL ==> Stat5:({y in s | y 叩incin s} = 0) & ((y in {u: v in {z in s | y notin z}, u in v}) or (y notin {z in s | y notin z})) -- -- ...we see that neither the possibility $y in Un(t)$ nor the possibility $y notin t$ -- is tenable. -- x-->Stat5(Stat1*) ==> y in s SIMPLF ==> Stat6: (y in {u: v in s, u in v | y notin v}) or (y notin {z in s | y notin z}) (w,u,y)-->Stat6(Stat5*) ==> false Discharge ==> QED -- Def clawFreeness_frontEl: [Element in the frontier of a claw-free transitive non-trivial set] x_thryvar := arb(front(s0)) -- Def clawFreeness_pivotEl: [Pivotal element of a claw-free transitive non-trivial set] y_thryvar := arb(x_thryvar - Un(Un(s0))) -- Theorem clawFreeness_c: [$x_thryvar$ truly belongs to the frontier of $s0$] (x_thryvar in front(s0)) & (x_thryvar - Un(Un(s0)) /= 0) & (x_thryvar in s0). Proof: Suppose_not() ==> AUTO Assump ==> Stat0: ClawFree(s0) & Finite(s0 * Un(s0)) & Trans(s0) & (s0 叩incin {0}) s0-->T3a ==> s0 * Un(s0) = Un(s0) s0-->T31d ==> s0 * Un(s0) /= 0 s0-->Tfrontier1 ==> Stat1: front(s0) /= 0 Use_def(front(s0)) ==> AUTO Use_def(x_thryvar)(Stat1) ==> Stat2: (x_thryvar in { x in s0 | (x * s0) - Un( s0 * Un(s0)) /= 0 }) & (x_thryvar in front(s0)) ()-->Stat2(Stat2*) ==> (x_thryvar in s0) & (x_thryvar - Un( s0 * Un(s0)) /= 0) EQUAL ==> false Discharge ==> QED -- Theorem clawFreeness0: [Pivotal elements in a transitive claw-free set such as this one, own at most two predecessors] ((Y in (X - Un(Un(s0)))) & (X in s0)) 可mp (EXISTS z | {v in s0 | Y in v} = {X,z}). Proof: Suppose_not(y,x) ==> Stat1: (not(EXISTS z | {v in s0 | y in v} = {x,z})) & (x in s0) & (y in (x - Un(Un(s0)))) -- -- Suppose that $y,x$ constitute a counter-example, so that $y$ has, in addition to $x$, -- at least two predecessors $z$ and $w$ in $s0$. -- Suppose ==> Stat2: x notin {v in s0 | y in v} x-->Stat2(*) ==> false Discharge ==> AUTO x-->Stat1(*) ==> Stat3: {v in s0 | y in v} /= {x} z-->Stat3(*) ==> Stat4: (z in {v in s0 | y in v}) & (x /= z) ()-->Stat4(Stat4*) ==> Stat5: (z in s0) & (y in z) z-->Stat1(*) ==> Stat6: {v in s0 | y in v} /= {z,x} w-->Stat6(*) ==> Stat7: (w in {v in s0 | y in v}) & (w notin {x,z}) ()-->Stat7(Stat7*) ==> Stat8: (w in s0) & (y in w) Loc_def ==> e = {x,z,w} Suppose ==> Stat9: {v in e | y notin v} /= 0 v-->Stat9(Stat1*) ==> false; Discharge ==> AUTO -- -- By the transitivity of $s0$, since $y in x$ and $x in s0$, $y$ must belong to $s0$; -- therefore, in view of the claw-freeness of $s0$, $y$ and $e={x,z,w}$ do not form an $in$-claw. -- Assump ==> ClawFree(s0) & Trans(s0) Use_def(ClawFree) ==> Stat10: (FORALL y in s0, e 可ncin s0 | not MembClaw(y, e) ) (s0,x)-->T3c(*) ==> y in s0 (y,e)-->Stat10(*) ==> not MembClaw(y, e) -- -- It readily follows from the definition of a claw that ${x,z,w}$ and $Un({x,z,w})$ intersect; -- therefore, we can pick an element $a$ common to the two. -- Use_def(MembClaw) ==> Stat11: (not(EXISTS x,z,w | (e incs {x,z,w}) & (x /= z) & (w notin {x,z}) & ({w} * y incs {v in e | y notin v}))) or (e * Un(e) /= 0) (x,z,w)-->Stat11(Stat4*) ==> (e * Un(e) /= 0) EQUAL(Stat8) ==> Stat12: {x,z,w} * Un({x,z,w}) /= 0 a-->Stat12(Stat12*) ==> Stat13: (a in {x,z,w}) & (a in Un({x,z,w})) -- -- But then $y in a$, $a 可ncin Un(Un({x,z,w}))$, and $Un(Un({x,z,w})) 可ncin Un(Un(s0))$ must hold, -- implying that $y in Un(Un(s0))$; but we have started with the assumption that $y notin Un(Un(s0))$. -- This contradiction proves the claim. -- ({x,z,w},s0)-->T2d(Stat1,Stat5,Stat8,Stat13*) ==> (y in a) & (Un(s0) incs Un({x,z,w})) (Un({x,z,w}),Un(s0))-->T2d(Stat13*) ==> Un(Un(s0)) incs Un(Un({x,z,w})) (a,Un({x,z,w}))-->T2(Stat13*) ==> Stat14: y in Un(Un(s0)) (Stat1,Stat14*)Discharge ==> QED -- Theorem clawFreeness_d: [Shape of the frontier at a pivotal pair] (EXISTS z | ({v in s0 | y_thryvar in v} = {x_thryvar,z}) & (y_thryvar in z)). Proof: Suppose_not() ==> AUTO ()-->TclawFreeness_c ==> Stat1: (x_thryvar - Un(Un(s0)) /= 0) & (x_thryvar in s0) Use_def(y_thryvar) ==> y_thryvar in (x_thryvar - Un(Un(s0))) (y_thryvar,x_thryvar)-->TclawFreeness0 ==> Stat2: (EXISTS z | {v in s0 | y_thryvar in v} = {x_thryvar,z}) & (not(EXISTS z | ({v in s0 | y_thryvar in v} = {x_thryvar,z}) & (y_thryvar in z))) (z0,z0)-->Stat2 ==> Stat3: (z0 in {v in s0 | y_thryvar in v}) & (y_thryvar notin z0) ()-->Stat3 ==> false Discharge ==> QED -- -- Via Skolemization, we give a name to the third item in a pivotal tripleton: -- APPLY(v1_thryvar:z_thryvar) Skolem() ==> Theorem clawFreeness_e: ({v in s0 | y_thryvar in v} = {x_thryvar,z_thryvar}) & (y_thryvar in z_thryvar) -- Theorem clawFreeness_f: [Tripleton pivot in claw-free, transitive non-trivial set] ({v in s0 | y_thryvar in v} = {x_thryvar,z_thryvar}) & ({x_thryvar,y_thryvar,z_thryvar} 可ncin s0) & (y_thryvar in (x_thryvar * z_thryvar) - Un(Un(s0))) & (x_thryvar notin z_thryvar) & (z_thryvar notin x_thryvar). Proof: Suppose_not() ==> AUTO ()-->TclawFreeness_c ==> Stat3: (x_thryvar - Un(Un(s0))) /= 0 Use_def(y_thryvar)(Stat3) ==> (y_thryvar notin Un(Un(s0))) & (y_thryvar in x_thryvar) ()-->TclawFreeness_e ==> Stat1: (x_thryvar in {v: v in s0 | y_thryvar in v}) & (z_thryvar in {v: v in s0 | y_thryvar in v}) & ({v in s0 | y_thryvar in v} = {x_thryvar,z_thryvar}) & (y_thryvar in z_thryvar) (v0,v1)-->Stat1 ==> (x_thryvar in s0) & (z_thryvar in s0) Assump ==> Trans(s0) (s0,z_thryvar)-->T3c ==> y_thryvar in s0 s0-->T3a ==> s0 * Un(s0) = Un(s0) EQUAL ==> y_thryvar notin Un(s0 * Un(s0)) (y_thryvar,x_thryvar,z_thryvar,s0)-->T31g ==> x_thryvar notin z_thryvar (y_thryvar,z_thryvar,x_thryvar,s0)-->T31g ==> false Discharge ==> QED -- Def clawFreeness_remove: [Removal of elements above pivot from a transitive claw-free set] t_thryvar := {v in s0 | y_thryvar notin v} -- Theorem clawFreeness_g: [The removal of elements above pivot from a transitive claw-free set does not disrupt transitivity] Trans(t_thryvar) & ClawFree(t_thryvar) & (t_thryvar 可ncin s0) & (x_thryvar notin t_thryvar) & (y_thryvar in t_thryvar-Un(t_thryvar)) & (t_thryvar = s0 - {x_thryvar,z_thryvar}). Proof: Suppose_not() ==> AUTO Use_def(t_thryvar) ==> Stat1: t_thryvar = {v in s0 | y_thryvar notin v} Set_monot ==> {v in s0 | y_thryvar notin v} 可ncin {v: v in s0} Assump ==> Trans(s0) & ClawFree(s0) (s0,t_thryvar)-->TclawFreeness_a(Stat1*) ==> ClawFree(t_thryvar) ()-->TclawFreeness_c ==> x_thryvar in front(s0) ()-->TclawFreeness_f ==> Stat2: ({v in s0 | y_thryvar in v} = {x_thryvar,z_thryvar}) & (y_thryvar in x_thryvar - Un(Un(s0))) & (y_thryvar notin Un(Un(s0))) (s0,x_thryvar,y_thryvar,t_thryvar)-->Tfrontier2(*) ==> Stat3: (t_thryvar /= s0 - {x_thryvar,z_thryvar}) & Trans(t_thryvar) & (t_thryvar 可ncin s0) & (x_thryvar notin t_thryvar) & (y_thryvar in t_thryvar-Un(t_thryvar)) e-->Stat3(Stat3*) ==> (e in t_thryvar) 叩eq (e in s0 - {x_thryvar,z_thryvar}) Suppose ==> Stat4: (e in {v in s0 | y_thryvar notin v}) & (e notin s0 - {x_thryvar,z_thryvar}) ()-->Stat4(Stat2*) ==> Stat5: (e in {v in s0 | y_thryvar in v}) & (e in s0) & (y_thryvar notin e) ()-->Stat5(Stat5*) ==> false Discharge ==> Stat6: (e notin {v in s0 | y_thryvar in v}) & (e notin {v in s0 | y_thryvar notin v}) & (e in s0) (e,e)-->Stat6(Stat6*) ==> false Discharge ==> QED -- ENTER_THEORY Set_theory -- --DISPLAY pivotsForClawFreeness -- --THEORY pivotsForClawFreeness(s0) -- ClawFree(s0) & Finite(s0) & Trans(s0) -- s0 叩incin {0} --==>(x_thryvar,y_thryvar,z_thryvar,t_thryvar) -- (FORALL y, x | ((y in (x - Un(Un(s0)))) & (x in s0)) 可mp (EXISTS z | {v in s0 | y in v} = {x,z})) -- ({v in s0 | y_thryvar in v}={x_thryvar,z_thryvar}) & ({x_thryvar,y_thryvar,z_thryvar} 可ncin s0) & (y_thryvar in (x_thryvar * z_thryvar)-Un(Un(s0))) & (x_thryvar notin z_thryvar) & (z_thryvar notin x_thryvar) -- t_thryvar = {v in s0 | y_thryvar notin v} -- Trans(t_thryvar) & ClawFree(t_thryvar) & (t_thryvar 可ncin s0) & (x_thryvar notin t_thryvar) & (y_thryvar in t_thryvar-Un(t_thryvar)) & (t_thryvar = s0 - {x_thryvar,z_thryvar}) --END pivotsForClawFreeness -- -- \section{Hanks, cycles, and Hamiltonian cycles} -- -- -- The following notion approximately models the concept of a graph where every node has at least two incident edges. However, -- we neither require that (1) edges be doubletons, nor that -- (2) the set $H$ edges and the one of vertices---which is understood to be $Un(H)$---be disjoint. -- Def cycle0: [Collection of edges whose endpoints have degree greater than 1] Hank(H) := (0 notin H) & (FORALL e in H | e 可ncin Un( H - {e} )) -- Def cycle1: [Cycle (unless null)] Cycle(C) := Hank(C) & (FORALL d 可ncin C | (Hank(d) & (d /= 0)) 可mp (d = C)) -- Theorem hank0: [Alternative characterization of a hank] Hank(H) 占q ((0 notin H) & (FORALL e in H, x in e | (EXISTS q in H | (q /= e) & (x in q)))). Proof: Suppose_not(h) ==> AUTO Suppose ==> (not(FORALL e in h, x in e | (EXISTS q in h | (q /= e) & (x in q)))) & (FORALL e in h | e 可ncin Un(h - {e})) Use_def(Un) ==> Stat1: (not(FORALL e in h, x in e | (EXISTS q in h | (q /= e) & (x in q)))) & (FORALL e in h | e 可ncin {v: u in h-{e}, v in u}) (e0,x0,e0)-->Stat1 ==> Stat2: (x0 in {v: u in h-{e0}, v in u}) & (not(EXISTS q in h | (q /= e0) & (x0 in q))) & (e0 in h) & (x0 in e0) (q0,v0,q0)-->Stat2 ==> false Discharge ==> AUTO Use_def(Hank) ==> Stat3: (not(FORALL e in h | e 可ncin Un(h - {e}))) & (FORALL e in h, x in e | (EXISTS q in h | (q /= e) & (x in q))) e1-->Stat3 ==> Stat4: (e1 叩incin Un(h - {e1})) & (FORALL e in h, x in e | (EXISTS q in h | (q /= e) & (x in q))) & (e1 in h) Use_def(Un(h - {e1})) ==> AUTO (x1,e1,x1)-->Stat4 ==> Stat5: (EXISTS q in h | (q /= e1) & (x1 in q)) & (x1 notin {v: u in h-{e1}, v in u}) & (x1 in e1) (q1,q1,x1)-->Stat5 ==> false Discharge ==> QED -- Theorem hank1: [No singleton or doubleton set is a cycle] ((H 可ncin {X,U}) & Hank(H)) 可mp (H = 0). Proof: Suppose_not(h0,x0,u0) ==> Stat0: (h0 /= 0) & (h0 可ncin {x0,u0}) & Hank(h0) -- -- For, assuming that $h0$ is a hank, non-null, and a subset of a doubleton ${x0,u0}$ consisting of non-null sets, -- we will reach a contradiciton arguing as follows. If $a$ is one of the (at most two) elements of $h0$, since -- $a 可ncin Un(h0-{a})$ ensues from the definition of hank, $Un(h0-{a})$ must be non-null; hence $h0={a,b}$, where -- $b/=a$. But then $Un(h0-{a})=Un({b})$ and $Un(h0-{b})=Un({a})$, i.e., $Un(h0-{a})=b$ and $Un(h0-{b})=a$; -- therefore $a 可ncin b$ and $b 可ncin a$ ensue from the definition of hank, leading to the identity $a=b$, -- which contradicts an earlier inequality. -- a-->Stat0(Stat0*) ==> Stat1: a in h0 Use_def(Hank) ==> Stat2: (FORALL e in h0 | e 可ncin Un( h0 - {e} ) ) & (0 notin h0) a-->Stat2 ==> a 可ncin Un( h0 - {a} ) (h0-{a})-->T31d ==> Stat3: h0 /= {a} b-->Stat3 ==> Stat4: (b in h0) & ( b /= a ) b-->Stat2 ==> b 可ncin Un( h0 - {b} ) ({a},a,a)-->T2a ==> Un({a}) = a ({b},b,b)-->T2a ==> Un({b}) = b (Stat0,Stat1,Stat4*)ELEM ==> (h0 - {a} = {b}) & (h0 - {b} = {a}) EQUAL ==> false Discharge ==> QED -- Theorem hank2: [A membership chain and an extra edge form a hank (basic case)] ((X in Y) & (Y in Z)) 可mp Hank({{X,Y},{Y,Z},{Z,X}}). Proof: Suppose_not(x0,y0,z0) ==> AUTO Use_def(Hank) ==> Stat0: (not(FORALL e in {{x0,y0},{y0,z0},{z0,x0}} | e 可ncin Un( {{x0,y0},{y0,z0},{z0,x0}} - {e} ) )) & (x0 in y0) & (y0 in z0) e0-->Stat0 ==> (e0 in {{x0,y0},{y0,z0},{z0,x0}}) & (e0 叩incin Un( {{x0,y0},{y0,z0},{z0,x0}} - {e0} )) Suppose ==> (e0 = {x0,y0}) & ({{x0,y0},{y0,z0},{z0,x0}} - {e0} = {{y0,z0},{z0,x0}}) ({{y0,z0},{z0,x0}},{y0,z0},{z0,x0})-->T2a ==> Un({{y0,z0},{z0,x0}}) = {y0,z0,x0} EQUAL ==> {x0,y0} 叩incin {y0,z0,x0} Discharge ==> AUTO Suppose ==> (e0 = {y0,z0}) & ({{x0,y0},{y0,z0},{z0,x0}} - {e0} = {{x0,y0},{z0,x0}}) ({{x0,y0},{z0,x0}},{x0,y0},{z0,x0})-->T2a ==> Un({{x0,y0},{z0,x0}}) = {x0,y0,z0} EQUAL ==> {y0,z0} 叩incin {x0,y0,z0} Discharge ==> AUTO ({{x0,y0},{y0,z0}},{x0,y0},{y0,z0})-->T2a ==> (Un({{x0,y0},{y0,z0}}) = {x0,y0,z0}) & (e0 = {z0,x0}) & ({{x0,y0},{y0,z0},{z0,x0}} - {e0} = {{x0,y0},{y0,z0}}) EQUAL ==> {z0,x0} 叩incin {x0,y0,z0} Discharge ==> QED -- Theorem hank3: [Replacing an edge by a 2-path with the same endpoints does not disrupt a hank] (Hank(H) & ({W,Y} in H) & (W /= Y) & (X notin Un(H)) & (Hp = ((H - {{W,Y}}) + {{W,X},{X,Y}}))) 可mp Hank(Hp). Proof: Suppose_not(h0,w0,y0,x1,h1) ==> Stat0: (Hank(h0) & ({w0,y0} in h0) & (w0 /= y0) & (x1 notin Un(h0)) & (h1 = ((h0 - {{w0,y0}}) + {{w0,x1},{x1,y0}}))) & (not Hank(h1)) -- -- Suppose that the premisses are met by $h0,w0,y0,x1$, and $h1$. In order to prove $Hank(h1)$, we assume it to be false, -- so that the definition of hank implies the existence of an $e1 in h1$ and a $z1 in e1$ such that $z1 notin Un(h1-{e1})$. -- Use_def(Hank) ==> Stat1: (not (FORALL e in h1 | e 可ncin Un( h1 - {e} ) )) & Stat2: (FORALL e in h0 | e 可ncin Un( h0 - {e} ) ) (e1,e1)-->Stat1 ==> Stat3: (e1 叩incin Un( h1 - {e1} )) & (e1 in h1) & ((e1 in h0) 可mp (e1 可ncin Un( h0 - {e1} ))) Use_def(Un( h1 - {e1} )) ==> AUTO z1-->Stat3(Stat3*) ==> Stat4: (z1 notin {v: u in h1-{e1}, v in u}) & (z1 in e1) -- -- Since $x1$ belongs to the distinct edges ${w0,x1},{x1,y0}$ of $h1$, clearly $z1/=x1$. -- Suppose ==> z1 = x1 ({w0,x1},x1)-->Stat4 ==> {w0,x1} = e1 ({x1,y0},x1)-->Stat4 ==> false Discharge ==> AUTO -- -- Moreover, $e1$ cannot be one of the edges of $h1-h0$. -- Suppose ==> e1 in {{w0,x1},{x1,y0}} Use_def(Un( h0 - {{w0,y0}} )) ==> AUTO ({w0,y0})-->Stat2 ==> Stat5: z1 in {v: u in h0-{{w0,y0}}, v in u} (ep,zp)-->Stat5 ==> (ep in h0-{{w0,y0}}) & (z1 in ep) Use_def(Un(h0)) ==> AUTO (ep,z1)-->Stat4 ==> (x1 in ep) & Stat6: (x1 notin {v: u in h0, v in u}) (ep,x1)-->Stat6 ==> false Discharge ==> AUTO Use_def(Un( h0 - {e1} )) ==> AUTO -- -- We know, at this point, that $e1 in h0-{{w0,y0}}$. Since $h0$ is a hank, $z1$ has in $h0$ at least -- one incident edge different from $e1$; since the latter is no longer available in $h1-{e1}$, -- it must be ${w0,y0}$, and either $z1=w0$ or $z1=y0$ hence holds. Both cases lead to a contradiction, though; -- in fact ${w0,x1},{x1,y0}$ differ from $e1$ and these edges of $h1$ are, respectively, incident to $w0$ and to $y0$. -- (Stat0*)ELEM ==> (e1 in h0) & Stat7: (z1 in {v: u in h0-{e1}, v in u}) & (z1 notin {v: u in h1-{e1}, v in u}) (e0,z0,e0,z1)-->Stat7() ==> Stat8: z1 in {w0,y0} ({w0,x1},w0)-->Stat4 ==> z1 /= w0 ({x1,y0},y0)-->Stat4 ==> z1 /= y0 (Stat8*)Discharge ==> QED -- Theorem cycle0: [A membership 2-chain and an extra edge make a cycle] ((X in Y) & (Y in Z)) 可mp Cycle({{X,Y},{Y,Z},{Z,X}}). Proof: Suppose_not(x0,y0,z0) ==> AUTO Use_def(Cycle({{x0,y0},{y0,z0},{z0,x0}})) ==> AUTO (x0,y0,z0)-->Thank2(*) ==> Stat0: not(FORALL d 可ncin {{x0,y0},{y0,z0},{z0,x0}} | (Hank(d) & (d /= 0)) 可mp (d = {{x0,y0},{y0,z0},{z0,x0}})) d-->Stat0 ==> Stat2: Hank(d) & (d /= 0) & (d /= {{x0,y0},{y0,z0},{z0,x0}}) & (d 可ncin {{x0,y0},{y0,z0},{z0,x0}}) (d,{y0,z0},{z0,x0})-->Thank1(Stat2*) ==> d 叩incin {{y0,z0},{z0,x0}} (d,{x0,y0},{z0,x0})-->Thank1(Stat2,Stat2*) ==> d 叩incin {{x0,y0},{z0,x0}} (d,{x0,y0},{y0,z0})-->Thank1(Stat2*) ==> false Discharge ==> QED -- Theorem cycle1: [The replacement of an edge by a 2-path with the same endpoints does not disrupt a cycle] (Cycle(C) & ({W,Y} in C) & (W /= Y) & (X notin Un(C)) & (Cp = ((C - {{W,Y}}) + {{W,X},{X,Y}}))) 可mp Cycle(Cp). Proof: Suppose_not(h0,w0,y0,x1,h1) ==> AUTO -- -- Supposing that $h0,w0,y0,x1,h1$ constitute a counter-example to the claim, observe that $Hank(h1)$ must hold; -- hence we can consider a strictly smaller hank $d1$ than $h1$. It readily turns out that either ${w0,x1} in d1$ or ${x1,y0} in d1$; -- for otherwise $h0$ would strictly include $d1$, since $d1 /= h0$ follows from ${w0,y0} in h0 - h1$. -- (h0,w0,y0,x1,h1)-->Thank3 ==> AUTO Use_def(Cycle) ==> Stat0: ({w0,y0} in h0) & (w0 /= y0) & (x1 notin Un(h0)) & (h1 = ((h0 - {{w0,y0}}) + {{w0,x1},{x1,y0}})) & Stat1: (not (FORALL d 可ncin h1 | (Hank(d) & (d /= 0)) 可mp (d = h1))) & Stat2: (FORALL d 可ncin h0 | (Hank(d) & (d /= 0)) 可mp (d = h0)) & Hank(h0) & Hank(h1) (d1,d1)-->Stat1(Stat0*) ==> Stat3: (d1 可ncin h1) & (d1 /= h1) & (d1 /= 0) & Hank(d1) & (not(({w0,x1} notin d1) & ({x1,y0} notin d1))) -- Use_def(Un) ==> Stat4a: x1 notin {v: u in h0, v in u} Use_def(Un(h0)) ==> AUTO d1-->Thank0 ==> Stat4: (FORALL e in d1, x in e | (EXISTS q in d1 | (q /= e) & (x in q))) & Stat4a: (x1 notin {v: u in h0, v in u}) & (0 notin d1) -- -- Should one of ${w0,x1},{x1,y0}$, but not the other, belong to $d1$, we would easily -- get a contradiction: the two cases are treated symmetrically. -- ({w0,x1},x1,q0,q0,x1)-->Stat4(Stat0*) ==> not(({w0,x1} in d1) & ({x1,y0} notin d1)) ({x1,y0},x1,q1,q1,x1)-->Stat4(Stat0*) ==> Stat5: ({w0,x1} in d1) & ({x1,y0} in d1) -- -- At this point we have derived that both ${w0,x1}$ and ${x1,y0}$ belong to $d1$. -- We will show that the set $d0$ obtained by replacing ${w0,x1}$ and ${x1,y0}$ by ${w0,y0}$ in $d1$ -- is non-null and is a cycle strictly included in $h0$. Obviously $({w0,x1} /= {w0,y0}) & ({x1,y0} /= {w0,y0})$, -- because $x1$, $y0$, and $w0$ are distinct. -- ({w0,y0},x1)-->Stat4a(Stat0*) ==> Stat6: (x1 /= w0) & (x1 /= y0) & (w0 /= y0) & ({w0,y0} notin d1) Loc_def ==> Stat7: d0 = ((d1 + {{w0,y0}}) - {{w0,x1},{x1,y0}}) (Stat5,Stat7,Stat6,Stat3,Stat0,Stat4*)ELEM ==> (d0 可ncin h0) & (d0 /= 0) & (d0 /= h0) & (0 notin d0) Use_def(Un(d0)) ==> AUTO (d0,h0)-->T2d(Stat0*) ==> Stat8: x1 notin {u: v in d0, u in v} -- -- Despite us having assumed at the beginning that $h0$ contains no proper cycle, -- so that in particular $Hank(d0)$ cannot hold, due to an edge -- $e0$ of $d0$ and to an endpoint $x0$ of $e0$ which is not properly covered in $d0$,... -- d0-->Thank0 ==> AUTO d0-->Stat2(Stat7*) ==> Stat9: not(FORALL e in d0, x in e | (EXISTS q in d0 | (q /= e) & (x in q))) (e0,x0)-->Stat9 ==> Stat10: (not(EXISTS q in d0 | (q /= e0) & (x0 in q))) & (e0 in d0) & (x0 in e0) -- -- ...we now aim at showing that the offending edge $e0$ of $d0$ will also offend $d1$, which -- contradicts a fact noted at the beginning. Here we shortly digress to prove -- that $e0 = {w0,y0}$ must hold, else $e0$ would offend $d1$. -- Suppose ==> Stat11: e0 /= {w0,y0} -- -- Indeed, assuming $e0 /= {w0,y0}$, $e0$ would also belong to $d1$, and each one of its endpoints -- must have edges distinct from $e0$ incident to it in $d1$. However, it will turn out that -- this cannot be the case for the endpoint $x0$, which hence is not properly covered in $d1$. -- (e0,x0)-->Stat4(Stat7,Stat10,Stat11*) ==> Stat12: (EXISTS q in d1 | (q /= e0) & (x0 in q)) q2-->Stat12(Stat12*) ==> Stat13: (x0 in q2) & (q2 /= e0) & (q2 in d1) -- -- To see this, let $q2 /= e0$ be the edge that covers $x0$ in $d1$. -- Suppose ==> Stat14: (q2 = {w0,x1}) or (q2 = {x1,y0}) -- -- If this edge $q2$ were one of the two which have been removed, the edge -- ${w0,y0}$ would satisfactorily cover $x0$ in $d0$. -- ({w0,y0})-->Stat10(Stat7,Stat6,Stat11*) ==> Stat15: x0 notin {w0,y0} (e0,x0)-->Stat8 ==> AUTO (Stat10*)Discharge ==> Stat16: not((q2 = {w0,x1}) or (q2 = {x1,y0})) -- -- $q2$ must hence belong to $d0$; but again, -- this implies that $q2$ would satisfactorily cover $x0$ in $d0$. -- Therefore, $e0={w0,y0}$ must hold. -- q2-->Stat10(Stat7,Stat16,Stat13*) ==> false Discharge ==> Stat17: e0 = {w0,y0} -- -- The only remaining possibility, $e0 = {w0,y0}$, is also untenable. Indeed, $d1$ has two edges incident to $w0$, -- one of which is ${w0,x1}$; likewise, $d1$ has two edges incident to $y0$, one of which is ${x1,y0}$. -- For either one of the endpoints $w0,y0$ of $e0$, the second incident edge belongs to $d1$ and differs from ${w0,y0}$, -- so it must belong to $d0$ as well; -- since $d0$ also owns the edge ${w0,y0}$ incident to either endpoint, it is not true that $e0$ is an offending edge for $d0$, -- a fact that contradicts one of the assumptions made. -- ({w0,x1},w0,q4)-->Stat4(Stat5,Stat7,Stat6,Stat17*) ==> Stat19: (q4 /= e0) & (q4 in d0) & (w0 in q4) ({x1,y0},y0,q5)-->Stat4(Stat5,Stat5*) ==> Stat20: (y0 in q5) & (q5 /= {x1,y0}) & (q5 in d1) (Stat20,Stat7,Stat6,Stat17*)ELEM ==> Stat21: (q5 /= e0) & (q5 in d0) & (e0 in d0) q5-->Stat10(Stat21,Stat17,Stat20*) ==> Stat22: (x0 notin q5) & (x0 = w0) q4-->Stat10(Stat19,Stat22*) ==> false Discharge ==> QED -- Def hamiltonian1: [Hamiltonian cycle, in digraph devoid of isolated vertices] Hamiltonian(H,S,E) := Cycle(H) & (Un(H) = S) & (H 可ncin E) -- -- In our specialized context, where edges are 2-sets whose elements satisfy a peculiar membership -- constraint, we do not simply require that a Hamiltonian cycle $H$ touches every vertex, but also -- that every source has an incident membership edge in $H$. -- Def hamiltonian2: [Edges in squared membership] sqEdges(S) := {{x,y} : x in S, y in S-{x}, z in S*x | (y = z) or (y in z) or (z in y)} -- Def hamiltonian3: [Restraining condition for Hamiltonian cycles] SqHamiltonian(H,S) := Hamiltonian(H,S,sqEdges(S)) & (FORALL x in (S-Un(S)) | (EXISTS y in x | {x,y} in H)) -- Theorem hamiltonian1: [Enriched Hamiltonian cycles] ((S=T+{X}) & (X notin T) & (Y in X) & SqHamiltonian(H,T) & ({W,Y} in H) & ((W in Y) or ((Y in W) & (K /= Y) & ({W,K} in H) & (K in W)))) 可mp SqHamiltonian((H-{{W,Y}})+{{W,X},{X,Y}},S). Proof: Suppose_not(s0,t0,x1,y0,h0,w0,k0) ==> AUTO Use_def(SqHamiltonian) ==> Stat0: (FORALL x in (t0-Un(t0)) | (EXISTS y in x | {x,y} in h0)) & Hamiltonian(h0,t0,sqEdges(t0)) & (not(Hamiltonian((h0-{{w0,y0}})+{{w0,x1},{x1,y0}},s0,sqEdges(s0)) & (FORALL x in (s0-Un(s0)) | (EXISTS y in x | {x,y} in (h0-{{w0,y0}})+{{w0,x1},{x1,y0}})))) Suppose ==> Stat1: not(FORALL x in (s0-Un(s0)) | (EXISTS y in x | {x,y} in (h0-{{w0,y0}})+{{w0,x1},{x1,y0}})) -- -- Suppose that $s0,t0,x1,y0,h0,w0,k0$ make a counterexample to the claim. One reason why -- $SqHamiltonian((h0-{{w0,y0}})+{{w0,x1},{x1,y0}},s0)$ is violated might be -- $not(FORALL x in (s0-Un(s0)) | (EXISTS y in x | {x,y} in (h0-{{w0,y0}})+{{w0,x1},{x1,y0}}))$; if -- this is the case, we can choose an $xp$ witnessing this fact. -- xp-->Stat1 ==> Stat2: (not (EXISTS k in xp | {xp,k} in (h0-{{w0,y0}})+{{w0,x1},{x1,y0}})) & (xp in (s0-Un(s0))) -- -- To see that $xp in (t0-Un(t0))$ follows from the constraint $xp in (s0-Un(s0))$, we assume the contrary -- and argue as follows: -- (1) Unless $xp$ belongs to $t0$, we must have $xp=x1$, which however has an incident membership edge, -- namely ${x1,y0}$, in $(h0-{{w0,y0}})+{{w0,x1},{x1,y0}}$. -- (2) Thus, since $xp in t0$, we have $xp in (t0*Un(t0))$ and hence $xp in (s0*Un(s0))$, which -- contradicts the constraint on $xp$. -- Suppose ==> xp notin (t0-Un(t0)) y0-->Stat2(*) ==> (xp in t0) & (s0=t0+{x1}) & (x1 notin t0) & (y0 in x1) (t0,s0)-->T2d(Stat2*) ==> Un(s0) incs Un(t0) (Stat2*)Discharge ==> AUTO -- -- Knowing that $xp in (t0-Un(t0))$, we can find a $y1 in xp$ such that ${xp,y1} in h0$. Since this -- membership edge is no longer available after the modification of $h0$, it must be ${w0,y0}$; -- therefore, $xp=w0$, for otherwise $xp=y0$ would (in view of the fact $y0 in x1$) contradict the -- assumption $xp in (s0-Un(s0))$. -- (xp,y1)-->Stat0(*) ==> Stat3: (y1 in xp) & ({xp,y1} in h0) & (x1 in s0) & (y0 in x1) Use_def(Un(s0)) ==> AUTO y1-->Stat2(Stat3*) ==> Stat4: (xp notin {u: v in s0, u in v}) & ({xp,y1} = {w0,y0}) (x1,y0)-->Stat4(Stat2*) ==> xp = w0 -- -- If $xp in y0$, the assumption $xp in (s0-Un(s0))$ would be contradicted similarly: but then, -- by the initial assumption, we must have $({xp,k0} in h0) & (k0 /= y0) & (k0 in xp)$, -- conflicting with Stat2, because ${xp,k0}={w0,y0}$ would imply $k0=y0$. -- (x1,y0)-->Stat4(*) ==> (xp notin y0) & ({xp,k0} in h0) & (k0 in xp) & (k0 /= y0) k0-->Stat2(Stat4*) ==> false Discharge ==> Stat5: Hamiltonian(h0,t0,sqEdges(t0))& (not Hamiltonian((h0-{{w0,y0}})+{{w0,x1},{x1,y0}},s0,sqEdges(s0))) -- -- At this point the reason why $SqHamiltonian((h0-{{w0,y0}})+{{w0,x1},{x1,y0}},s0)$ -- is false must be that $Hamiltonian((h0-{{w0,y0}})+{{w0,x1},{x1,y0}},s0,sqEdges(s0))$ is false; -- however, we will derive a contradiction also in this case. -- Use_def(Hamiltonian(h0,t0,sqEdges(t0))) ==> AUTO ELEM ==> Stat6: (s0=t0+{x1}) & (x1 notin t0) & (y0 in x1) & ({w0,y0} in h0) & ((w0 in y0) or ((y0 in w0) & (k0 /= y0) & ({w0,k0} in h0) & (k0 in w0))) Loc_def ==> Stat7: h1 = ((h0-{{w0,y0}})+{{w0,x1},{x1,y0}}) Use_def(Hamiltonian(h1,s0,sqEdges(s0))) ==> AUTO EQUAL(Stat5) ==> Stat8: (Cycle(h0) & (Un(h0) = t0) & (h0 可ncin sqEdges(t0))) & (not(Cycle(h1) & (Un(h1) = s0) & (h1 可ncin sqEdges(s0)))) -- -- In fact, after observing that ${w0,y0} 可ncin Un(h0)$ must hold, we will be able to discard one by one -- each potential reason why $Hamiltonian((h0-{{w0,y0}})+{{w0,x1},{x1,y0}},s0,sqEdges(s0))$ should be false. -- (h0,w0,y0,x1,h1)-->Tcycle1(Stat6*) ==> Stat9: (Cycle(h0) & (Un(h0) = t0) & (h0 可ncin sqEdges(t0))) & (not((Un(h1) = s0) & (h1 可ncin sqEdges(s0)))) Suppose ==> Stat10: {w0,y0} 叩incin Un(h0) Use_def(Un(h0)) ==> AUTO b-->Stat10(Stat10*) ==> Stat11: (b notin {u: v in h0, u in v}) & (b in {w0,y0}) ({w0,y0},b)-->Stat11(Stat11,Stat6*) ==> false Discharge ==> Stat12: (w0 in t0) & (y0 in t0) Suppose ==> Stat13: h1 叩incin sqEdges(s0) Use_def(sqEdges(s0)) ==> AUTO e-->Stat13(Stat7*) ==> ((e in h0) or (e = {w0,x1}) or (e = {x1,y0})) & Stat14: (e notin {{x,y} : x in s0, y in s0-{x}, z in s0*x | (y = z) or (y in z) or (z in y)}) (Stat6,Stat12*)ELEM ==> Stat15: (x1 in s0) & (y0 in s0) & (w0 in s0) & (y0 in x1) & ((w0 in y0) or (y0 in w0)) & (x1 /= w0) (x1,y0,y0)-->Stat14(Stat15*) ==> e /= {x1,y0} (x1,w0,y0)-->Stat14(Stat15*) ==> e /= {w0,x1} Use_def(sqEdges(t0)) ==> AUTO (Stat8*)ELEM ==> Stat16: e in {{x,y} : x in t0, y in t0-{x}, z in t0*x | (y = z) or (y in z) or (z in y)} (x2,y2,z2)-->Stat16(Stat16*) ==> Stat17: (e = {x2,y2}) & (x2 in t0) & (y2 in t0) & (z2 in t0) & (x2 /= y2) & (z2 in x2) & ((y2 = z2) or (y2 in z2) or (z2 in y2)) (Stat6*)ELEM ==> s0 incs t0 (x2,y2,z2)-->Stat14(Stat17*) ==> false Discharge ==> Stat18: Un(h1) /= s0 -- -- We prove first that $Un(h1) 可ncin s0$. -- ({{w0,x1},{x1,y0}},{w0,x1},{x1,y0})-->T2a(Stat18*) ==> Un({{w0,x1},{x1,y0}}) = {w0,x1,y0} ((h0-{{w0,y0}}),{{w0,x1},{x1,y0}})-->T2c(Stat18*) ==> Un((h0-{{w0,y0}})+{{w0,x1},{x1,y0}}) = Un(h0-{{w0,y0}}) + Un({{w0,x1},{x1,y0}}) (h0-{{w0,y0}},h0)-->T2d(Stat8*) ==> (Un(h0) incs Un(h0-{{w0,y0}})) & ({w0,y0} 可ncin Un(h0)) EQUAL(Stat7) ==> Un(h1) = (Un(h0-{{w0,y0}}) + {w0,x1,y0}) (Stat6*)ELEM ==> Un(h1) 可ncin s0 -- -- The remaining case is $s0 叩incin Un(h1)$, which entails that we can find an $a in t0 - Un(h1)$. -- Use_def(Un(h1)) ==> AUTO a-->Stat18(Stat18*) ==> Stat23: (a notin {u: v in h1, u in v}) & (a in (s0-{x1})) -- -- Since $a in t0$ and $t0 = Un(h0)$, we can find an $ep in h0$ such that $a in ep$. -- Use_def(Un)(Stat8,Stat23,Stat6*) ==> Stat24: a in {u: v in h0, u in v} (ep,up)-->Stat24(Stat25*) ==> Stat25: (ep in h0) & (a in ep) -- -- Since $h1 = (h0-{{w0,y0}})+{{w0,x1},{x1,y0}}$, we conclude that $ep = {w0,y0}$ must hold. -- Hence, either $a = w0$ or $a = y0$ must hold, both of which yield a contradiction. -- (ep,a)-->Stat23(Stat7,Stat25*) ==> ep = {w0,y0} ({w0,x1},w0)-->Stat23(Stat7*) ==> a = y0 ({x1,y0},y0)-->Stat23(Stat7*) ==> false Discharge ==> QED -- -- -- Theorem hamiltonian2: [Doubly enriched Hamiltonian cycles] ((S=T+{X,Z}) & (({X,Z} * T) = 0) & (X /= Z) & (Y in (X*Z)) & SqHamiltonian(H,T) & ({W,Y} in H) & (W in (Y*X))) 可mp SqHamiltonian((H-{{W,Y}})+{{W,X},{X,Z},{Z,Y}},S). Proof: Suppose_not(s0,t0,x0,z0,y0,h0,w0) ==> AUTO (t0+{x0},t0,x0,y0,h0,w0,0)-->Thamiltonian1 ==> SqHamiltonian((h0-{{w0,y0}})+{{w0,x0},{x0,y0}},t0+{x0}) Loc_def ==> Stat1: (h1 = (h0-{{w0,y0}})+{{w0,x0},{x0,y0}}) & (t1 = t0+{x0}) ELEM ==> Stat2: (s0 = t1 + {z0}) & (x0 notin t0) EQUAL ==> SqHamiltonian(h1,t1) Suppose ==> {x0,y0} in h0 -- -- Notice that since $h0$ is a Hamiltonian path in $t0$, its unionset must equal $t0$; -- since $x0$ does not belong to $t0$,but it belongs to ${x0,y0}$, it follows that -- ${x0,y0}$ cannot belong to $h0$. -- Use_def(SqHamiltonian(h0,t0)) ==> AUTO Use_def(Hamiltonian(h0,t0,sqEdges(t0))) ==> AUTO Use_def(Un) ==> Stat3: x0 notin {u: v in h0, u in v} ({x0,y0},x0)-->Stat3(Stat2*) ==> false Discharge ==> ({x0,y0} notin h0) & ({x0,y0} /= {w0,x0}) & (z0 notin t1) & (y0 in z0) & (y0 in x0) & (w0 in y0) & (w0 in x0) (t1+{z0},t1,z0,y0,h1,x0,w0)-->Thamiltonian1(Stat1*) ==> SqHamiltonian((h1-{{x0,y0}})+{{x0,z0},{z0,y0}},t1+{z0}) (Stat1*)ELEM ==> (h1-{{x0,y0}}) = ((h0-{{w0,y0}})+{{w0,x0}}) (Stat1*)ELEM ==> ((h1-{{x0,y0}})+{{x0,z0},{z0,y0}}) = ((h0-{{w0,y0}})+{{w0,x0},{x0,z0},{z0,y0}}) EQUAL ==> false Discharge ==> QED -- -- -- Theorem hamiltonian3: [Trivial Hamiltonian cycles] ((S = {X,Y,Z}) & (X in Y) & (Y in Z)) 可mp SqHamiltonian({{X,Y},{Y,Z},{Z,X}},S). Proof: Suppose_not(s,x0,y0,z0) ==> AUTO -- -- Arguing by contradiction, assume that ${{x0,y0},{y0,z0},{z0,x0}}$ is not a 'square Hamiltonian' -- cycle for $s={x0,y0,z0}$, where $x0 in y0$ and $y0 in z0$ holds. We will first -- exclude the possibility that ${{x0,y0},{y0,z0},{z0,x0}}$ is not a Hamiltonian cycle in the -- 'square edges' of $s$; after discarding this, we will also exclude that this cycle may fail to -- satisfy the restraining condition that it has a genuine membership edge incident -- into each source of $s$. -- Use_def(SqHamiltonian({{x0,y0},{y0,z0},{z0,x0}},s)) ==> AUTO Use_def(Hamiltonian({{x0,y0},{y0,z0},{z0,x0}},s,sqEdges(s))) ==> AUTO (x0,y0,z0)-->Tcycle0 ==> AUTO ELEM ==> Stat1: (s = {x0,y0,z0}) & (x0 in y0) & (y0 in z0) Suppose ==> Stat8: {{x0,y0},{y0,z0},{z0,x0}} 叩incin sqEdges(s) Use_def(sqEdges(s)) ==> AUTO e0-->Stat8(Stat8*) ==> Stat9: (e0 notin {{x,y} : x in s, y in s-{x}, z in s*x | (y = z) or (y in z) or (z in y)}) & (e0 in {{x0,y0},{y0,z0},{z0,x0}}) (z0,y0,y0)-->Stat9(Stat1,Stat1*) ==> e0 /= {y0,z0} (z0,x0,y0)-->Stat9(Stat1,Stat9*) ==> e0 /= {z0,x0} (y0,x0,x0)-->Stat9(Stat1,Stat1*) ==> e0 /= {x0,y0} (Stat9*)Discharge ==> AUTO Suppose ==> Stat4: Un({{x0,y0},{y0,z0},{z0,x0}}) /= s (Stat1,Stat1*)ELEM ==> (s = {x0,y0,z0}) & ({{x0,y0},{y0,z0},{z0,x0}} = ({{x0,y0},{y0,z0}} + {{z0,x0}})) & (({x0,y0,z0} + {z0,x0}) = {x0,y0,z0}) ({{x0,y0},{y0,z0}},{{z0,x0}})-->T2c(Stat5*) ==> Stat5: Un({{x0,y0},{y0,z0}} + {{z0,x0}}) = Un({{x0,y0},{y0,z0}}) + Un({{z0,x0}}) ({{x0,y0},{y0,z0}},{x0,y0},{y0,z0})-->T2a(Stat6*) ==> Stat6: Un({{x0,y0},{y0,z0}}) = {x0,y0,z0} ({{z0,x0},{z0,x0}},{z0,x0},{z0,x0})-->T2a(Stat7*) ==> Stat7: (Un({{z0,x0},{z0,x0}}) = {z0,x0}) & ({{z0,x0},{z0,x0}} = {{z0,x0}}) EQUAL(Stat4) ==> false Discharge ==> Stat10: not(FORALL z in (s-Un(s)) | (EXISTS y in z | {z,y} in {{x0,y0},{y0,z0},{z0,x0}})) -- -- We conclude by checking that ${{x0,y0},{y0,z0},{z0,x0}}$ owns a genuine membership edge incident -- into each source of $s$; as a matter of fact, $z0$ is the only source of $s$ and ${y0,z0}$ is a -- membership edge. -- zp-->Stat10(Stat10*) ==> Stat11: (not(EXISTS y in zp | {zp,y} in {{x0,y0},{y0,z0},{z0,x0}})) & (zp in (s-Un(s))) y0-->Stat11(Stat11*) ==> Stat12: (y0 notin zp) or ({zp,y0} notin {{x0,y0},{y0,z0},{z0,x0}}) Use_def(Un)(Stat11) ==> Stat13: (zp notin {u: v in s, u in v}) & (zp in s) (z0,y0)-->Stat13(Stat12,Stat1*) ==> Stat14: zp = x0 (y0,x0)-->Stat13(Stat14,Stat13,Stat12,Stat1*) ==> false Discharge ==> QED -- -- -- Theorem hamiltonian4: [Any non-trivial transitive set whose square is devoid of Hamiltonian cycles must strictly comprise certain sets] (Trans(S) & (S 叩incin {0,{0}}) & (not (EXISTS h | SqHamiltonian(h,S)))) 可mp ((S /= {0,{0},{{0}}}) & (S /= {0,{0},{0,{0}}}) & (S /= {0,{0},{{0}},{0,{0}}}) & (S incs {0,{0}}) & (({{0}} in S) or ({0,{0}} in S))). Proof: Suppose_not(t) ==> AUTO -- -- Indeed, any set satisfying the premises of our present claim must, due to its transitivity and non-triviality, -- include either one of the Hamiltonian cycles endowed with the vertices $0,{0},{{0}}$ and $0,{0},{0,{0}}$, -- respectively; but it must also own additional elements, else the last premise would be falsified. -- Moreover, it cannot have exactly the elements $0,{0},{{0}},{0,{0}}$, because these form a Hamiltonian cycle. (t,{0,{0}})-->T4b ==> Stat1: (not (EXISTS h | SqHamiltonian(h,t))) & ((t incs {0,{0},{{0}}}) or (t incs {0,{0},{0,{0}}})) -- -- The cases $t = {0,{0},{{0}}}$ and $t = {0,{0},{0,{0}}}$ must be excluded, because we have the respective Hamiltonian cycles -- ${{0,{0}},{{0},{{0}}},{{{0}},0}}$, -- ${{0,{0}},{{0},{0,{0}}},{{0,{0}},0}}$. -- (t,0,{0},{{0}})-->Thamiltonian3 ==> AUTO ({{0,{0}},{{0},{{0}}},{{{0}},0}})-->Stat1(*) ==> t /= {0,{0},{{0}}} (t,0,{0},{0,{0}})-->Thamiltonian3 ==> AUTO ({{0,{0}},{{0},{0,{0}}},{{0,{0}},0}})-->Stat1(*) ==> Stat2: t = {0,{0},{{0}},{0,{0}}} -- -- Having thus established that $t = {0,{0},{{0}},{0,{0}}}$, -- we can now exploit Theorem hamiltonian1 to enrich the Hamiltonian cycle for ${0,{0},{{0}}}$ -- into one which does to our case. -- ({0,{0},{{0}}},0,{0},{{0}})-->Thamiltonian3(Stat2*) ==> SqHamiltonian({{0,{0}},{{0},{{0}}},{{{0}},0}},{0,{0},{{0}}}) ({0,{0},{{0}}},0,{0},{{0}})-->Thamiltonian3 ==> Stat22: SqHamiltonian({{0,{0}},{{0},{{0}}},{{{0}},0}},{0,{0},{{0}}}) ({0,{0},{{0}},{0,{0}}},{0,{0},{{0}}},{0,{0}},{0},{{0,{0}},{{0},{{0}}},{{{0}},0}},0)-->Thamiltonian1(Stat2*) ==> SqHamiltonian(({{0,{0}},{{0},{{0}}},{{{0}},0}}-{{0,{0}}})+{{0,{0,{0}}},{{0,{0}},{0}}},{0,{0},{{0}},{0,{0}}}) EQUAL(Stat2) ==> SqHamiltonian(({{0,{0}},{{0},{{0}}},{{{0}},0}}-{{0,{0}}})+{{0,{0,{0}}},{{0,{0}},{0}}},t) (({{0,{0}},{{0},{{0}}},{{{0}},0}}-{{0,{0}}})+{{0,{0,{0}}},{{0,{0}},{0}}})-->Stat1(Stat2*) ==> false Discharge ==> QED -- -- \section{Every claw-free set has a Hamiltonian cycle in its square} -- Theorem clawFreeness1: [Every non-trivial claw-free finite transitive set has a Hamiltonian cycle in its square] ( Finite(S) & Trans(S) & ClawFree(S) & (S 叩incin {0,{0}}) ) 可mp (EXISTS h | SqHamiltonian(h,S)). Proof: Suppose_not(s1) ==> AUTO -- -- For, assuming the contrary, there would exist an inclusion-minimal finite transitive non-trivial claw-free set $s0$ -- whose square lacks a Hamiltonian cycle. -- APPLY(fin_thryvar:s0) finiteInduction(s0->s1,P(S)->(Trans(S) & ClawFree(S) & (S 叩incin {0,{0}}) & (not (EXISTS h | SqHamiltonian(h,S))))) ==> Stat1: (FORALL s | (s 可ncin s0) 可mp (Finite(s) & ((Trans(s) & ClawFree(s) & (s 叩incin {0,{0}}) & (not (EXISTS h | SqHamiltonian(h,s)))) 占q (s = s0)))) s0-->Stat1(Stat1*) ==> Stat2: (not (EXISTS h | SqHamiltonian(h,s0))) & Finite(s0) & Trans(s0) & ClawFree(s0) & (s0 叩incin {0,{0}}) -- -- Thanks to the finiteness of $s0$, the THEORY pivotsForClawFreeness can be applied to $s0$. -- We thereby pick an element $x$ from the frontier of $s0$, and -- an element $y$ of $x$ which is pivotal relative to $s0$. -- This $y$ will have at most two $in$-predecessors (one of the two being $x$) in $s0$. We denote by $z$ a predecessor -- of $y$ in $s0$, such that $z$ differs from $x$ if possible. Observe, among others, that neither one of $x,z$ can belong to the other. -- APPLY(x_thryvar:x,y_thryvar:y,z_thryvar:z,t_thryvar:t) pivotsForClawFreeness(s0->s0) ==> Stat3: ({v in s0 | y in v} = {x,z}) & (z in s0) & (y in z) & (y in x) & (y in s0) & (x in s0) & (not(y in Un(Un(s0)))) & (t = {u in s0 | y notin u}) & Trans(t) & ClawFree(t) & (x notin t) & (y in t-Un(t)) & (t = s0 - {x,z}) & (x notin z) & (z notin x) -- -- Thus it turns out readily that removal of $x,z$ from $s0$ leads to a set $t$ to which, unless $t$ is 'trivial' (i.e. a subset of ${0,{0}}$), -- the inductive hypothesis applies; hence, by that hypothesis, there is a Hamiltonian cycle $h0$ for $t$. -- Suppose ==> t 可ncin {0,{0}} -- -- In order that $t$ be trivial, we should have $s0 可ncin {0,{0},{{0}},{0,{0}}}$; but then, as -- already shown in the proof of Theorem hamiltonian4, we have the ability, either directly, or -- by enrichment of a Hamiltonian cycle for ${0,{0},{{0}}}$, to construct a Hamiltonian cycle for $s0$, -- thus, if we suppose $t 可ncin {0,{0}}$ the we get a contradiction. -- (s0,x,z)-->T3d(Stat2*) ==> Stat7: s0 可ncin {0,{0},{{0}},{0,{0}}} s0-->Thamiltonian4(Stat2,Stat7*) ==> false Discharge ==> AUTO t-->Stat1(Stat3*) ==> Stat9: (EXISTS h | SqHamiltonian(h,t)) & (t 叩incin {0,{0}}) h0-->Stat9(Stat9*) ==> Stat10: SqHamiltonian(h0,t) Use_def(Hamiltonian(h0,t,sqEdges(t))) ==> AUTO Use_def(SqHamiltonian) ==> Stat11: (FORALL x in (t-Un(t)) | (EXISTS y in x | {x,y} in h0)) & Cycle(h0) & (Un(h0) = t) & (h0 可ncin sqEdges(t)) -- -- It follows from $y$ being a source of $t = Un(h0)$ that there is an edge ${y,w}$, with $w in y$, in $h0$, -- If $x=z$, we get a Hamiltonian cycle $h1$ for $s0$ (a fact conflicting with the inductive hypothesis) simply by -- taking $h1=h0-{{y,w}}+{{x,y},{x,w}}$, where ${x,w}$ is a square edge as $w in y$ and $y in x$ both hold. -- On the other hand, if $x/=z$, claw-freeness implies that either $w in x$ or $w in z$ must hold. -- Assume the former for definiteness, and put $h2=h0-{{y,w}}+{{y,z},{z,x},{x,w}}$, where ${x,z}$ is a square edge -- and ${x,w}$ and ${y,z}$ are genuine edges incident in the sources $x,z$. We are again facing a contradiction, -- as $h2$ is a Hamiltonian cycle for $s0$. -- (y,w)-->Stat11(Stat3*) ==> Stat12: (w in y) & ({w,y} in h0) Suppose ==> x = z (s0,t,x,y,h0,w,0)-->Thamiltonian1(Stat3*) ==> SqHamiltonian((h0-{{w,y}})+{{w,x},{x,y}},s0) ((h0-{{w,y}})+{{w,x},{x,y}})-->Stat2(Stat2*) ==> false Discharge ==> Stat13: x /= z -- (s0,y)-->T3c(Stat2*) ==> Stat14: w in s0 (s0,y,x,z,w)-->TclawFreeness_b(Stat2,Stat3,Stat12,Stat13,Stat14*) ==> w in (x+z) Suppose ==> Stat15: w in x (s0,t,x,z,y,h0,w)-->Thamiltonian2(Stat3,Stat13,Stat10,Stat12,Stat15*) ==> SqHamiltonian((h0-{{w,y}})+{{w,x},{x,z},{z,y}},s0) ((h0-{{w,y}})+{{w,x},{x,z},{z,y}})-->Stat2(Stat2*) ==> false Discharge ==> Stat16: w in z (s0,t,z,x,y,h0,w)-->Thamiltonian2(Stat3,Stat13,Stat10,Stat12,Stat16*) ==> SqHamiltonian((h0-{{w,y}})+{{w,z},{z,x},{x,y}},s0) ((h0-{{w,y}})+{{w,z},{z,x},{x,y}})-->Stat2(Stat2*) ==> false Discharge ==> QED -- -- \section{Matchings} -- -- Next we introduce the notion of \emph{matching}. This is a partition consisting of doubletons -- one of whose elements belongs to the other. Special cases of a matching are: the empty set -- and, more generally, all subsets of a matching. -- -- Def matching: [Set of disjoint membership pairs] Matching(M) := (FORALL p in M | (EXISTS x in p, y in x | (FORALL q in M | ((x in q) or (y in q)) 可mp ({x,y} = q)))) -- Theorem matching0: [The null set is a matching] Matching(0). Proof: Suppose_not() ==> AUTO Use_def(Matching) ==> Stat0: not(FORALL p in 0 | (EXISTS x in p, y in x | (FORALL q in 0 | ((x in q) or (y in q)) 可mp ({x,y} = q)))) p1-->Stat0 ==> false Discharge ==> QED -- Theorem matching1: [Matchings consist of doubletons proper] (Matching(M) & (P in M)) 可mp (P notin {0,{X}}). Proof: Suppose_not(m,p0,x0) ==> AUTO Use_def(Matching) ==> Stat1: (FORALL p in m | (EXISTS x in p, y in x | (FORALL q in m | ((x in q) or (y in q)) 可mp ({x,y} = q)))) (p0,x,y,p0)-->Stat1(*) ==> false Discharge ==> QED -- Theorem matching2: [All subsets of a matching are matchings] (Matching(M) & (M incs N)) 可mp Matching(N). Proof: Suppose_not(m,n) ==> AUTO Set_monot ==> (FORALL p in m | (EXISTS x in p, y in x | (FORALL q in m | ((x in q) or (y in q)) 可mp ({x,y} = q)))) 可mp (FORALL p in n | (EXISTS x in p, y in x | (FORALL q in n | ((x in q) or (y in q)) 可mp ({x,y} = q)))) Use_def(Matching) ==> false Discharge ==> QED -- -- By adjoining a pair ${x,y}$ with $y in x$ to a matching none of whose blocks has either -- $x$ or $y$ as an element, we always obtain a matching. -- Theorem matching3: [Bottom-up assembly of a finite matching] (Matching(M) & (X notin Un(M)) & (Y notin Un(M)) & (Y in X)) 可mp Matching(M+{{X,Y}}). Proof: Suppose_not(m,x0,y0) ==> Stat2: Matching(m) & (x0 notin Un(m)) & (y0 notin Un(m)) & (y0 in x0) & (not Matching(m+{{x0,y0}})) Suppose ==> Stat3: not(FORALL q in m | (x0 notin q) and (y0 notin q)) Use_def(Un) ==> Stat4: (x0 notin {v: u in m, v in u}) & (y0 notin {v: u in m, v in u}) q2-->Stat3(Stat3*) ==> (q2 in m) & ((x0 in q2) or (y0 in q2)) (q2,x0,q2,y0)-->Stat4(Stat4*) ==> false Discharge ==> Stat5: (FORALL q in m | (x0 notin q) and (y0 notin q)) Use_def(Matching)(Stat2*) ==> Stat6: (not(FORALL p in (m+{{x0,y0}}) | (EXISTS x in p, y in x | (FORALL q in (m+{{x0,y0}}) | ((x in q) or (y in q)) 可mp ({x,y} = q))))) & Stat7: (FORALL p in m | (EXISTS x in p, y in x | (FORALL q in m | ((x in q) or (y in q)) 可mp ({x,y} = q)))) p0-->Stat6(Stat6*) ==> Stat8: (not(EXISTS x in p0, y in x | (FORALL q in (m+{{x0,y0}}) | ((x in q) or (y in q)) 可mp ({x,y} = q)))) & (p0 in (m+{{x0,y0}})) Suppose ==> Stat9: p0 = {x0,y0} (x0,y0)-->Stat8(Stat2,Stat9*) ==> Stat10: not(FORALL q in (m+{{x0,y0}}) | ((x0 in q) or (y0 in q)) 可mp ({x0,y0} = q)) q1-->Stat9(Stat9*) ==> (q1 in m) & ((x0 in q1) or (y0 in q1)) q1-->Stat5(Stat10*) ==> false Discharge ==> AUTO (p0,x1,y1)-->Stat7 ==> AUTO (x1,y1)-->Stat8(Stat8*) ==> Stat13: (not(FORALL q in (m+{{x0,y0}}) | ((x1 in q) or (y1 in q)) 可mp ({x1,y1} = q))) & Stat12: (FORALL q in m | ((x1 in q) or (y1 in q)) 可mp ({x1,y1} = q)) & (p0 in m) & (x1 in p0) & (y1 in x1) (q0,q0)-->Stat13(Stat13*) ==> Stat14: (q0 = {x0,y0}) & ((x1 in q0) or (y1 in q0)) p0-->Stat5(*) ==> (x0 notin p0) & (y0 notin p0) p0-->Stat12(Stat13,Stat13*) ==> {x1,y1} = p0 (Stat14*)Discharge ==> QED -- -- If we replace, in a matching $m$, one of its blocks ${y,w}$ by pairs -- ${y,z}, {x,w}$, under suitable conditions ensuring disjointness between blocks -- and membership within each block, then we get a matching again. -- Theorem matching4: [Deviated matching] (Matching(M) & ({Y,W} in M) & (X notin Un(M)) & (Z notin Un(M)) & (Y in Z) & (X /= Z) & (W in X)) 可mp Matching((M-{{Y,W}}) + {{Y,Z},{X,W}}). Proof: Suppose_not(m,y0,w0,x0,z0) ==> AUTO -- -- For assuming that $m,y0,w0,x0,z0$ are a counterexample to the claim, we could get a contradiction arguing as follows. -- Begin by observing that neither $y0$ nor $w0$ can belong to the unionset of the submatching $m-{{y0,w0}}$ of $m$. -- Suppose ==> Stat1: {y0,w0} * Un(m-{{y0,w0}}) /= 0 Use_def(Matching) ==> Stat2: (FORALL p in m | (EXISTS x in p, y in x | (FORALL q in m | ((x in q) or (y in q)) 可mp ({x,y} = q)))) Use_def(Un(m-{{y0,w0}})) ==> AUTO w1-->Stat1 ==> Stat3: (w1 in {u: v in m-{{y0,w0}}, u in v}) & (w1 in {y0,w0}) (p0,w2)-->Stat3 ==> (p0 in m-{{y0,w0}}) & (w1 in p0) (p0,x2,y2)-->Stat2 ==> Stat4: (FORALL q in m | ((x2 in q) or (y2 in q)) 可mp ({x2,y2} = q)) & (x2 in p0) & (y2 in x2) p0-->Stat4 ==> p0 = {x2,y2} ({y0,w0})-->Stat4 ==> false Discharge ==> AUTO (m,m-{{y0,w0}})-->Tmatching2 ==> Matching(m-{{y0,w0}}) -- -- Thus, taking into account that $w0 in x0$ and that $x0 notin Un(m)$ which is a superset of $Un(m-{{y0,w0}})$, -- we can extend the matching $m-{{y0,w0}}$ with the doubleton ${x0,w0}$. -- (m-{{y0,w0}},m)-->T2d ==> x0 notin Un(m-{{y0,w0}}) (m-{{y0,w0}},x0,w0)-->Tmatching3 ==> Matching((m-{{y0,w0}})+{{x0,w0}}) -- -- Observe next that $x0 /= y0$ and $z0 /= w0$, because $x0 notin Un(m)$ and $z0 notin Un(m)$ -- whereas $y0 in Un(m)$ and $z0 in Un(m)$. It then follows from $z0 /= w0$, -- thanks to the assumption $z0 /= x0$, that $z0$ does not belong to the -- unionset of the matching $(m-{{y0,w0}})+{{x0,w0}}$. -- Suppose ==> (x0 = y0) or (z0 = w0) Use_def(Un) ==> Stat5: (z0 notin {u: v in m, u in v}) & (x0 notin {u: v in m, u in v}) ({y0,w0},w0,{y0,w0},y0)-->Stat5 ==> false Discharge ==> AUTO Suppose ==> z0 in Un((m-{{y0,w0}})+{{x0,w0}}) (m-{{y0,w0}},m)-->T2d ==> z0 notin Un(m-{{y0,w0}}) (m-{{y0,w0}},{x0,w0})-->T2e ==> false Discharge ==> AUTO -- -- $y0$ cannot equal $w0$ either, the reason being that the set ${y0,w0}$ is a block of a -- matching, and hence it cannot be a singleton. If follows, thanks to -- the assumption $y0 in x0$ (entailing $y0 /= x0$), that $y0$ does not belong to -- $Un((m-{{y0,w0}})+{{x0,w0}})$ either. -- (m,{y0,w0},w0)-->Tmatching1 ==> y0 /= w0 (m-{{y0,w0}},{x0,w0})-->T2e ==> y0 notin Un((m-{{y0,w0}})+{{x0,w0}}) -- -- We now know that the matching $(m-{{y0,w0}})+{{x0,w0}}$ can be extended with -- the doubleton ${y0,z0}$, which readily leads us to the sought contradiction. -- ((m-{{y0,w0}})+{{x0,w0}},z0,y0)-->Tmatching3 ==> Matching((m-{{y0,w0}})+{{x0,w0}}+{{y0,z0}}) & ((m-{{y0,w0}})+{{x0,w0}}+{{y0,z0}} = (m-{{y0,w0}}) + {{y0,z0},{x0,w0}}) EQUAL ==> false Discharge ==> QED -- -- -- \section{Every claw-free set of even cardinality owns a perfect matching} -- Theorem clawFreeness2: [Every claw-free finite transitive set has a perfect matching (possibly omitting one of its elements)] ( Finite(S) & Trans(S) & ClawFree(S) ) 可mp (EXISTS m, y | Matching(m) & (S-{y} = Un(m))). Proof: Suppose_not(s1) ==> AUTO -- -- For, supposing the contrary, there would be an inclusion-minimal finite set $s0$ which is transitive and claw-free, -- and such that no matching $m$ partitions the set $s0$ possibly deprived of an element $y0$. -- APPLY(fin_thryvar:s0) finiteInduction(s0->s1,P(S)->(Trans(S) & ClawFree(S) & (not (EXISTS m, y | Matching(m) & (S-{y} = Un(m)))))) ==> Stat1: (FORALL s | (s 可ncin s0) 可mp ( Finite(s) & ( Trans(s) & ClawFree(s) & (not(EXISTS m, y | Matching(m) & (s-{y} = Un(m)))) 占q (s = s0)) )) s0-->Stat1(Stat1*) ==> Stat2: (not(EXISTS m, y | Matching(m) & (s0-{y} = Un(m)))) & Trans(s0) & ClawFree(s0) & Finite(s0) -- -- We observe that such an $s0$ cannot equal $0$ or ${0}$, else the null matching would cover it. -- 0-->T31d ==> AUTO; ()-->Tmatching0 ==> AUTO; (0,0)-->Stat2 ==> s0 叩incin {0} -- -- Thanks to the finiteness of $s0$, the THEORY pivotsForClawFreeness can be applied to $s0$. -- We thereby pick an element $x$ from the frontier of such an $s0$ and an element $y$ of $x$ which is pivotal relative to $s0$. -- This $y$ will have at most two $in$-predecessors (one of the two being $x$) in $s0$. -- We denote by $z$ a predecessor of $y$ in $s0$, such that $z$ differs from $x$ if possible. -- APPLY(x_thryvar:x,y_thryvar:y,z_thryvar:z,t_thryvar:tp) pivotsForClawFreeness(s0->s0) ==> Stat3: ({v in s0 | y in v} = {x,z}) & (z in s0) & (y in z) & (y in x) & (y in s0) & (x in s0) & (not(y in Un(Un(s0)))) & (tp = {z in s0 | y notin z}) & Trans(tp) & ClawFree(tp) & (x notin tp) & (y in tp-Un(tp)) & (tp = s0 - {x,z}) & (x notin z) & (z notin x) -- -- Moreover, we take $tp$ to be $s0$ deprived of the predecessors of $y$ and, if $x/=z$, we take $t=tp$ else we take $t=tp-{y}$. -- Loc_def ==> t = if x = z then tp-{y} else tp end if -- -- Thus it turns out readily that $t$ is transitive; hence, by the inductive hypothesis, there is a perfect matching $m0$ for $t$. -- (tp,t)-->T4c ==> AUTO; (tp,t)-->TclawFreeness_a(Stat3*) ==> Stat4: Trans(t) & ClawFree(t) & (x notin t) t-->Stat1(Stat3*) ==> Stat5: (EXISTS m, y | Matching(m) & (t-{y} = Un(m))) (m0,y0)-->Stat5(Stat5) ==> Stat6: Matching(m0) & (Un(m0) = t-{y0}) -- -- The possibility that $y$ does not belong to $Un(m0)$ is then discarded; in fact, if this were the case, then by adding -- the pair ${x,y}$ to $m0$ we would get a perfect matching for $s0$, while we have assumed that such a matching does not exist. -- From the fact $y in Un(m0)$ it follows that $y$ belongs to $t$, hence that $t=tp$ and that $x,z$ are distinct. -- Use_def(Un(m0)) ==> AUTO Suppose ==> Stat7: y notin Un(m0) (m0,x,y)-->Tmatching3(Stat6,Stat4,Stat7,Stat3*) ==> Matching(m0+{{x,y}}) (m0+{{x,y}},d0)-->Stat2(Stat7) ==> Stat8: Un(m0 + {{x,y}}) /= s0-{d0} Loc_def ==> v = if x = z then y else z end if (m0,t,y0,s0,{x},v,y)-->T31h(Stat3*) ==> Stat9: (EXISTS d | Un(m0 + {{x}+{y}}) = s0-{d}) d0-->Stat9(Stat9) ==> (Un(m0 + {{x}+{y}}) = s0-{d0}) & ({x}+{y} = {x,y}) EQUAL(Stat8) ==> false Discharge ==> Stat11: (y in {h: p in m0, h in p}) & (y in x * z) & (x /= z) & (t = tp) & (x notin z) & (z notin x) & (Un(m0) = {h: p in m0, h in p}) -- -- It also follows that $y$ is the tail of that arc $p1$ of $m0$ to which it belongs. -- In fact, if $y$ were instead the head of $p1$, then -- the tail $x2$ of $p1$, which must belong to $Un(m0)$ would belong to $s0-{x,z}$, -- hence would be inside $s0$ but outside the set of predecessors of $y$, which -- is absurd. -- Suppose ==> Stat12: not(EXISTS w | ({y,w} in m0) & (w in y)) (p1,h1)-->Stat11(Stat12*) ==> (p1 in m0) & (y in p1) Use_def(Matching)(Stat6,Stat6) ==> Stat13: (FORALL p in m0 | (EXISTS x in p, y in x | (FORALL q in m0 | ((x in q) or (y in q)) 可mp ({x,y} = q)))) (p1,x2,w2,p1)-->Stat13(Stat12*) ==> (x2 in p1) & (w2 in x2) & (p1 in m0) & ({x2,w2} = p1) w2-->Stat12(Stat12*) ==> Stat14: (y in x2) & ({y,x2} in m0) Suppose ==> Stat15: x2 notin {u: v in m0, u in v} ({y,x2},x2)-->Stat15(Stat14*) ==> false Discharge ==> Stat16: (x2 notin {v in s0 | y in v}) & (x2 in s0) & ({v in s0 | y in v} = {x,z}) & (x2 in Un(m0)) x2-->Stat16(Stat14*) ==> false Discharge ==> Stat17: (EXISTS w | ({y,w} in m0) & (w in y)) -- -- Call $w$ the head of the arc issuing from $y$ in $m0$. Then $y,x,z,w$ form a potential -- $in$-claw; this implies, since $s0$ is claw-free that either $w in x$ or $w in z$. -- w-->Stat17(Stat17*) ==> Stat18: (w in y) & ({y,w} in m0) (s0,y)-->T3c(Stat2,Stat3,Stat18*) ==> Stat19: (w in s0) & (y in s0) & (x in s0) & (z in s0) Loc_def ==> y1 = if y0 in {x,z} then s0 else y0 end if (Stat19*)ELEM ==> (s0-{x,z,y0}) + {z,x} = s0 - {y1} (s0,y,x,z,w)-->TclawFreeness_b(Stat2,Stat11,Stat18,Stat19*) ==> w in x+z -- -- Obviously, $w in Un(m0)$. -- Moreover, through elementary reasoning we derive $(Un(m0) + {z,x}) = s0 - {y1}$, -- where $y1$ lies outside $s0$ if both $x$ and $z$ has been covered by the matching $m0$, -- otherwise $y1$ equals the one of $x,z$ (which might be the same set) left over -- by $m0$. -- Suppose ==> Stat20: w notin {u: v in m0, u in v} ({y,w},w)-->Stat20(Stat18,Stat18*) ==> false Discharge ==> AUTO (Stat6,Stat11,Stat4,Stat3*)ELEM ==> Stat21: (x notin Un(m0)) & (z notin Un(m0)) & ((Un(m0) + {z,x}) = (s0-{x,z,y0}) + {z,x}) EQUAL(Stat11) ==> Stat22: ((Un(m0) + {z,x}) = s0 - {y1}) & (w in Un(m0)) -- -- If there is an arc between $w$ and $x$, then we deviate the perfect matching by replacing -- ${y,w}$ by ${y,z}$ and ${x,w}$; otherwise we replace ${y,w}$ by ${y,x}$ and ${z,w}$. Plainly -- we get a perfect matching for $s0$ in either case, which leads us to the desired contradiction. -- Suppose ==> Stat23: w in x (m0,y,w,x,z)-->Tmatching4(Stat6,Stat11,Stat18,Stat23,Stat21*) ==> Stat24: Matching((m0-{{y,w}}) + {{y,z},{x,w}}) (m0,{y,w},{y,z},{x,w},{z,x})-->T31f(Stat11,Stat22*) ==> Un((m0-{{y,w}}) + {{y,z},{x,w}}) = (s0 - {y1}) ((m0-{{y,w}}) + {{y,z},{x,w}},y1)-->Stat2(Stat24*) ==> false Discharge ==> Stat25: w in z (m0,y,w,z,x)-->Tmatching4(Stat6,Stat11,Stat18,Stat25,Stat21*) ==> Stat26: Matching((m0-{{y,w}}) + {{y,x},{z,w}}) (m0,{y,w},{y,x},{z,w},{z,x})-->T31f(Stat11,Stat22*) ==> Un((m0-{{y,w}}) + {{y,x},{z,w}}) = (s0 - {y1}) ((m0-{{y,w}}) + {{y,x},{z,w}},y1)-->Stat2(Stat26*) ==> false Discharge ==> QED -- -- \section{An outward look} -- -- -- The following two representation THEORYs (not yet developed formally -- with Referee) explain why we can work with membership as a convenient -- surrogate for the edge relationship of general graphs. Thanks to the second -- of these THEORYs, in particular, the above-proved existence results about -- perfect matchings and Hamiltonian cycles can be transferred from a realm -- of special membership digraphs to the apparently more general realm of -- connected claw-free (undirected) graphs. -- -- --DISPLAY finGraphRepr -- --THEORY finGraphRepr(v0,e0) -- Finite(v0) & (e0 可ncin {{x,y}: x,y in v0 | x /= y}) --==>(rho_thryvar) -- one_1_map(rho_thryvar) & ( domain(rho_thryvar) = v0 ) -- (FORALL x in v0, y in v0 | ({x,y} in e0) 占q (((rho_thryvar~[x]) in (rho_thryvar~[y])) or ((rho_thryvar~[x]) in (rho_thryvar~[y])))) -- { x in range(rho_thryvar) | x * range(rho_thryvar) /= 0 } 可ncin pow( range(rho_thryvar) ) --END finGraphRepr -- --DISPLAY cfGraphRepr -- --THEORY cfGraphRepr(v0,e0) -- Finite(v0) & (e0 可ncin {{x,y}: x,y in v0 | x /= y}) -- (FORALL x in v0, y in v0 | ((x /= y) & ({x,y} notin e0)) 可mp (EXISTS p 可ncin e0 | Cycle( p + {{y,x}} ))) -- (FORALL w in v0, x in v0, y in v0, z in v0 | (({w,y} in e0) & ({y,x} in e0) & ({y,z} in e0)) 可mp ((x = z) or (w in {z,x}) or ({x,z} in e0) or ({z,w} in e0) or ({w,x} in e0))) --==>(rho_thryvar) -- one_1_map(rho_thryvar) & ( domain(rho_thryvar) = v0 ) -- (FORALL x in v0, y in v0 | ({x,y} in e0) 占q (((rho_thryvar~[x]) in (rho_thryvar~[y])) or ((rho_thryvar~[x]) in (rho_thryvar~[y])))) -- Trans( range(rho_thryvar) ) & ClawFree( range(rho_thryvar) ) --END cfGraphRepr -- -- --END HERE -- -- The following is an alternative proof of Theorem 2e, not relying on Theorem 2q. -- Theorem 2e: [Union of adjunction] Un(X + {Y}) = (Y + Un(X)). Proof: Suppose_not(x0,y0) ==> Stat0: Un(x0 + {y0}) /= (y0 + Un(x0)) a-->Stat0 ==> (a in Un(x0 + {y0})) 叩eq (a in (y0 + Un(x0))) -- -- Arguing by contradiction, let $x0,y0$ be a counterexample, so that in either one of -- $Un(x0 + {y0})$ and $y0 + Un(x0)$ there is an $a$ not belonging to the other set. -- Taking the definition of $Un$ into account, by monotonicity we must exclude the possibility -- that $a in Un(x0)-Un(x0+{y0})$; through variable-substitution, we must also discard -- the possibility that $a in Un(x0+{y0})-Un(x0)-y0$. -- Set_monot ==> {u: v in x0, u in v} 可ncin {u: v in x0 + {y0}, u in v} Suppose ==> Stat1: (a in {u: v in x0 + {y0}, u in v}) & (a notin {u: v in x0, u in v}) & (a notin y0) (v0,u0,v0,u0)-->Stat1 ==> false; Discharge ==> AUTO Use_def(Un) ==> Stat2: (a notin {u: v in x0 + {y0}, u in v}) & (a in y0) -- -- The only possibility left, namely that $a in y0-Un(x0+{y0})$, is also manifestly absurd. -- This contradiction leads us to the desired conclusion. -- (y0,a)-->Stat2 ==> false Discharge ==> QED -- -- The earlier proofs of Theorem 3c and Theorem 3d relied on Theorem 3b, which has then been removed. -- Theorem 3b: [Incomparable elements $x,z$ of a transitive set $t$ are subsets of $t-{x,z}$] (Trans(T) & (X in T) & (Z in T) & (X notin Z) & (Z notin X)) 可mp (X 可ncin (T-{X,Z})). Proof: Suppose_not(t,x,z) ==> AUTO t-->T3a ==> Stat1: (t = (t+{z})+{x}) & (not (Un(t) incs x + (z + Un(t)))) (t+{z},x)-->T2e ==> AUTO (t,z)-->T2e ==> AUTO EQUAL(Stat1) ==> false Discharge ==> QED -- Theorem 3c: [For a transitive set, elements are also subsets] (Trans(T) & (X in T)) 可mp (X 可ncin T). Proof: Suppose_not(t,x) ==> AUTO (t,x,x)-->T3b ==> AUTO Discharge ==> QED -- Theorem 3d: [Trapping phenomenon for trivial sets] (Trans(S) & (X in S) & (Z in S) & (X notin Z) & (Z notin X) & ((S-{X,Z}) 可ncin {0,{0}})) 可mp (S 可ncin {0,{0},{{0}},{0,{0}}}). Proof: Suppose_not(s,x,z) ==> AUTO (s,x,z)-->T3b ==> x 可ncin {0,{0}} (s,z,x)-->T3b ==> z 可ncin {0,{0}} Discharge ==> QED -- Theorem 31h: [Less-one lemma for unionset] ((Un(M) = T-{C}) & (S=T+X+{V}) & ((Y = V) or ((C = Y) & (Y in S)))) 可mp (EXISTS d | Un(M+{X+{Y}}) = S-{d}). Proof: Suppose_not(m,t,c,s,x,v,y) ==> Stat0: (not(EXISTS d | Un(m+{x+{y}}) = s-{d})) & (Un(m) = t-{c}) & (s=t+x+{v}) & ((y = v) or ((c = y) & (y in s))) -- -- For, supposing the contrary, $Un(m+{x+{y}})$ would differ from each of $s-{s}$, $s-{c}$, and $s-{v}$, the first of which equals $s$. -- Thanks to Theorem 2e, we can rewrite $Un(m+{x+{y}})$ as $x+{y}+Un(m)$; but then the decidable fragment of set theory known as -- 'multi-level syllogistic with singleton' immediately yields a contradiction. -- s-->Stat0(*) ==> Un(m+{x+{y}}) /= s c-->Stat0(*) ==> Un(m+{x+{y}}) /= (s-{c}) v-->Stat0(*) ==> Un(m+{x+{y}}) /= (s-{v}) (m,x+{y})-->T2e ==> AUTO EQUAL ==> Stat1: ((x+{y} + Un(m)) /= (s-{c})) & ((x+{y} + Un(m)) /= (s-{v})) & ((x+{y} + Un(m)) /= s) (Stat0,Stat1*)Discharge ==> QED -- -- -- The following earlier version of the proof of Theorem 32 consisted of fewer steps but -- it had a dependency from Theorem 31d and its verification took slightly longer. -- Theorem 32: [Finite, non-null sets own sources] (Finite(F) & (F /= 0)) 可mp ((F - Un(F)) /= 0). Proof: Suppose_not(f1) ==> AUTO -- -- Arguing by contradiction, suppose that there are counterexamples to the claim. -- Then, by exploiting finite induction, we can pick a minimal such counterexample, $f0$. -- APPLY(fin_thryvar:f0) finiteInduction(s0->f1,P(S)->((S/=0) & ((S - Un(S)) = 0))) ==> Stat0: (FORALL s | (s 可ncin f0) 可mp ( Finite(s) & ( ((s/=0) & ((s - Un(s)) = 0)) 占q (s = f0)) )) f0-->Stat0(Stat0) ==> Stat1: Finite(f0) & ((f0 - {arb(f0)}) 可ncin f0) & ((f0 - {arb(f0)}) /= f0) & ((f0 - Un(f0)) = 0) -- -- We must exclude that $f0$ is a singleton; for, otherwise, $arb(f0)$ would be its source. -- Suppose ==> f0 = {arb(f0)} (0,arb(f0))-->T2e(*) ==> (Un(0+{arb(f0)}) = (Un(0) + arb(f0))) 0-->T31d(*) ==> (Un(0 + {arb(f0)}) = arb(f0)) & ((0 + {arb(f0)}) = {arb(f0)}) EQUAL ==> Un(f0) = arb(f0) Discharge ==> AUTO -- -- Due to our minimality assumption, the strict subset $f0 - {arb(f0)}$ of $f0$ cannot be a -- counterexample to the claim; therefore it has sources and hence $f0 - Un(f0 - {arb(f0)}) /= 0$. -- (f0 - {arb(f0)})-->Stat0(Stat1*) ==> Stat2: (f0 - Un(f0 - {arb(f0)}) /= 0) & ((f0 - {arb(f0)}) + {arb(f0)} = f0) -- -- It hence follows that -- (f0-{arb(f0)},arb(f0))-->T2e(Stat2) ==> Un((f0 - {arb(f0)})+{arb(f0)}) = (Un(f0 - {arb(f0)}) + arb(f0)) EQUAL ==> f0 - (Un(f0 - {arb(f0)}) + arb(f0)) = 0 (Stat2*)Discharge ==> QED -- -- -- The following alternative version of the proof of Theorem 32 has fewer context restrictions and -- does not echo the literal $a = arb(f0)$ in its penultimate step: it is hence more elegant, -- but its verification takes longer. -- Theorem 32: [Finite, non-null sets own sources] (Finite(F) & (F /= 0)) 可mp ((F - Un(F)) /= 0). Proof: Suppose_not(f1) ==> AUTO -- -- Arguing by contradiction, suppose that there are counterexamples to the claim. -- Then, by exploiting finite induction, we can pick a minimal counterexample, $f0$. -- APPLY(fin_thryvar:f0) finiteInduction(s0->f1,P(S)->((S/=0) & ((S - Un(S)) = 0))) ==> Stat0: (FORALL s | (s 可ncin f0) 可mp ( Finite(s) & ( ((s/=0) & ((s - Un(s)) = 0)) 占q (s = f0)) )) Loc_def ==> a = arb(f0) f0-->Stat0 ==> Stat1: Finite(f0) & (a in f0) & (f0 - Un(f0) = 0) -- -- Momentarily supposing that $f0={a}$, one gets $Un(f0) 叩incin a$, because $Un(f0) 可ncin a$ would imply -- $f0-Un(f0) incs {a}-a$ and hence would imply the emptiness of ${a}-a$, entailing the manifest absurdity -- $a in a$. But, on the other hand, $Un({a}) 可ncin a$ trivially holds; therefore -- we must exclude that $f0$ is a singleton ${a}$. -- Suppose ==> (f0 = {a}) & (Un(f0) 叩incin a) EQUAL ==> Un({a}) 叩incin a Use_def(Un) ==> {u: v in {a}, u in v} 叩incin a SIMPLF ==> false Discharge ==> AUTO -- -- Due to our minimality assumption, the strict non-null subset $f0 - {arb(f0)}$ of $f0$ cannot be a -- counterexample to the claim; therefore it has sources and hence $f0 - Un(f0 - {arb(f0)}) /= 0$. -- (f0-{a},a)-->T2e(*) ==> (Un((f0 - {a})+{a}) = Un(f0 - {a}) + a) & ((f0 - {a}) + {a} = f0) (f0-{a})-->Stat0(*) ==> f0-Un(f0-{a}) /= 0 -- -- Since $arb(f0)$ does not intersect $f0$, the inequality just found conflicts with the equality -- $f0 - (Un(f0 - {arb(f0)}) + arb(f0)) = 0$ which one gets from Theorem 2e through equality propagation. -- EQUAL ==> f0 - (Un(f0 - {a}) + a) = 0 Discharge ==> QED -- -- The following Theorem lied inside the THEORY pivotsForClawFreeness, but it turned out to be not so useful. -- Theorem clawFreeness_h: (T in {t_thryvar, t_thryvar-{y_thryvar}}) 可mp (Trans(T) & ClawFree(T)). Proof: Suppose_not(t0) ==> AUTO TclawFreeness_g ==> Trans(t_thryvar) & ClawFree(t_thryvar) & (y_thryvar in t_thryvar-Un(t_thryvar)) Suppose ==> t0 = t_thryvar EQUAL ==> false; Discharge ==> t0 = t_thryvar-{y_thryvar} (t_thryvar,t0)-->T4c ==> AUTO (t_thryvar,t0)-->TclawFreeness_a ==> false Discharge ==> QED -- -- The following two proofs are older versions, which have been revised; in one case, the new claim is more general than the older one. -- Theorem hank1: [No singleton-or-doubleton of doubletons is a cycle] ((E={X,Y}) & (F={U,V}) & (H = {E,F})) 可mp (not Hank(H)). Proof: Suppose_not(e0,x0,x1,e1,u0,u1,h0) ==> AUTO -- -- For, assuming that $h0={e0,e1}$ is not a hank, where $e0$ and $e1$ are the doubletons ${x0,x1}$ and ${u0,u1}$, -- the definition of hank implies $h0-{{x0,x1}} /= 0$ and hence ${x0,x1} /= {u0,u1}$. -- Use_def(Hank) ==> Stat1: (FORALL e in h0 | e 可ncin Un( h0 - {e} ) ) ({x0,x1})-->Stat1 ==> {x0,x1} 可ncin Un( h0 - {{x0,x1}} ) (h0 - {{x0,x1}})-->T31d ==> ({x0,x1} /= {u0,u1}) & (h0 - {{x0,x1}} = {{u0,u1}}) & (h0 - {{u0,u1}} = {{x0,x1}}) ({u0,u1})-->Stat1 ==> {u0,u1} 可ncin Un( h0 - {{u0,u1}} ) -- -- Using the definition of hank again, it follows that ${x0,x1} 可ncin {u0,u1}$ and symmetrically; -- but then ${x0,x1} = {u0,u1}$, and we have a contradiction. -- ({{u0,u1}},{u0,u1},{u0,u1})-->T2a ==> Un({{u0,u1}}) = {u0,u1} ({{x0,x1}},{x0,x1},{x0,x1})-->T2a ==> Un({{x0,x1}}) = {x0,x1} EQUAL ==> false Discharge ==> QED -- Theorem cycle0: [A membership 2-chain and an extra edge make a cycle] ((X in Y) & (Y in Z)) 可mp Cycle({{X,Y},{Y,Z},{Z,X}}). Proof: Suppose_not(x0,y0,z0) ==> AUTO Use_def(Cycle({{x0,y0},{y0,z0},{z0,x0}})) ==> AUTO (x0,y0,z0)-->Thank2(*) ==> Stat0: not(FORALL d 可ncin {{x0,y0},{y0,z0},{z0,x0}} | (Hank(d) & (d /= 0)) 可mp (d = {{x0,y0},{y0,z0},{z0,x0}})) d-->Stat0 ==> Stat2: Hank(d) & (d /= 0) & (d /= {{x0,y0},{y0,z0},{z0,x0}}) & (d 可ncin {{x0,y0},{y0,z0},{z0,x0}}) ({x0,y0},x0,y0,{x0,y0},x0,y0,d)-->Thank1(Stat2*) ==> d /= {{x0,y0}} ({y0,z0},y0,z0,{y0,z0},y0,z0,d)-->Thank1(Stat2,Stat2*) ==> d /= {{y0,z0}} ({z0,x0},z0,x0,{z0,x0},z0,x0,d)-->Thank1(Stat2,Stat2*) ==> d /= {{z0,x0}} ({x0,y0},x0,y0,{y0,z0},y0,z0,d)-->Thank1(Stat2,Stat2*) ==> d /= {{x0,y0},{y0,z0}} ({y0,z0},y0,z0,{z0,x0},z0,x0,d)-->Thank1(Stat2,Stat2*) ==> d /= {{y0,z0},{z0,x0}} ({x0,y0},x0,y0,{z0,x0},z0,x0,d)-->Thank1(Stat2,Stat2*) ==> d /= {{x0,y0},{z0,x0}} (Stat0*)ELEM ==> false Discharge ==> QED -- -- An earlier version of the present proof of Theorem clawFreeness0, which made use of an intermediate lemma, ran as shown by the two -- proofs which follow: -- Theorem clawFreeness0a: [Pivotal elements in a claw-free set own at most two predecessors therein] ( ClawFree(S) & (X in S) & (Y in ((X*S) - Un(S*Un(S)))) ) 可mp (EXISTS z in S| ( {v in S | Y in v} = {X,z} ) & (Y in z)). Proof: Suppose_not(s,x,y) ==> Stat1: (not(EXISTS z in s | ({v in s | y in v} = {x,z}) & (y in z) )) & ClawFree(s) & (x in s) & (y in ((x*s) - Un(s*Un(s)))) Suppose ==> Stat2: x notin {v in s | y in v} x-->Stat2(*) ==> false Discharge ==> AUTO x-->Stat1(*) ==> Stat3: {v in s | y in v} /= {x} z-->Stat3(*) ==> Stat4: (z in {v in s | y in v}) & (x /= z) ()-->Stat4(Stat4*) ==> Stat5: (z in s) & (y in z) z-->Stat1(*) ==> Stat6: {v in s | y in v} /= {z,x} w-->Stat6(*) ==> Stat7: (w in {v in s | y in v}) & (w notin {x,z}) ()-->Stat7(Stat7*) ==> Stat8: (w in s) & (y in w) Loc_def ==> e = {x,z,w} Suppose ==> Stat9: {v in e | y notin v} /= 0 v-->Stat9(Stat1*) ==> false; Discharge ==> AUTO Use_def(ClawFree) ==> Stat10: (FORALL y in s, e 可ncin s | not MembClaw(y, e) ) (y,e)-->Stat10(Stat1*) ==> not MembClaw(y, e) Use_def(Claw) ==> Stat11: (not(EXISTS x,z,w | (e incs {x,z,w}) & (x /= z) & (w notin {x,z}) & ({w} * y incs {v in e | y notin v}))) or (e * Un(e) /= 0) (x,z,w)-->Stat11(Stat4*) ==> (e * Un(e) /= 0) EQUAL(Stat8) ==> Stat12: {x,z,w} * Un({x,z,w}) /= 0 a-->Stat12(Stat12*) ==> Stat13: (a in Un({x,z,w})) & (a in {x,z,w}) Use_def(Un)(Stat13) ==> Stat14: (a in {v: u in {x,z,w}, v in u}) & (a in {x,z,w}) (u,b)-->Stat14(Stat14*) ==> Stat15: (u in {x,z,w}) & (a in u) Use_def(Un(s*Un(s))) ==> AUTO (Stat1*)ELEM ==> Stat16: y notin {v: t in (s*Un(s)), v in t} Use_def(Un) ==> Stat17: Un(s) = {d: c in s, d in c} (a,y)-->Stat16(Stat1,Stat8,Stat5,Stat17,Stat14*) ==> Stat18: a notin {d: c in s, d in c} (u,a)-->Stat18(Stat15,Stat1,Stat5,Stat8*) ==> false Discharge ==> QED -- -- The following claim, which is a trivial specialization of the preceding one, shows a better way of encapsulating the preceding theorem in the current THEORY. -- Theorem clawFreeness0: [Pivotal elements in a transitive claw-free set such as this one, own at most two predecessors] ((Y in (X - Un(Un(s0)))) & (X in s0)) 可mp (EXISTS z in s0 | ( {v in s0 | Y in v} = {X,z} ) & (Y in z)). Proof: Suppose_not(y,x) ==> (x in s0) & (y in (x - Un(Un(s0)))) & (not(EXISTS z in s0 | ( {v in s0 | y in v} = {x,z} ) & (y in z))) Assump ==> ClawFree(s0) & Trans(s0) (s0,x)-->T3c ==> x * s0 = x s0-->T3a ==> s0 * Un(s0) = Un(s0) EQUAL ==> y in ((x*s0) - Un(s0*Un(s0))) (s0,x,y)-->TclawFreeness0a ==> false Discharge ==> QED -- Theorem silly0: [Instrumental to the proof of Theorem clawFreeness2] ((X in S) & (Z in S) & (W = if (Y in {X,Z}) then S else Y end if)) 可mp (((S - {X,Z,Y}) + {Z,X}) = (S - {W})). Proof: Suppose_not(x,s,z,y,w) ==> AUTO Discharge ==> QED --