:: Recognizing Chordal Graphs: Lex BFS and MCS
::  by Broderick Arneson and Piotr Rudnicki
::
:: Received November 17, 2006
:: Copyright (c) 2006-2012 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies NUMBERS, FUNCT_1, CARD_1, RELAT_1, TARSKI, FUNCT_4, FUNCOP_1,
      XBOOLE_0, SUBSET_1, XXREAL_0, ARYTM_3, FINSET_1, XREAL_0, ORDINAL1,
      ARYTM_1, NAT_1, ZFMISC_1, FINSEQ_1, UPROOTS, VALUED_0, RELAT_2, BAGORDER,
      PRE_POLY, WELLORD1, GLIB_000, GLIB_001, ORDINAL4, PBOOLE, PARTFUN1,
      MCART_1, FUNCT_2, FINSUB_1, CHORD, TOPGEN_1, RCOMP_1, FINSEQ_4, GRAPH_1,
      MEMBERED, ABIAN, LEXBFS, MATROID0;
 notations TARSKI, XBOOLE_0, ZFMISC_1,
      XTUPLE_0, MCART_1, CARD_1, NUMBERS, SUBSET_1,
      XXREAL_0, VALUED_0, XREAL_0, RELAT_1, RELAT_2, WELLORD1, MEMBERED,
      XXREAL_2, PARTFUN1, FUNCT_1, FUNCT_2, PBOOLE, ORDINAL1, FINSET_1,
      XCMPLX_0, NAT_1, NAT_D, FUNCOP_1, FUNCT_4, GLIB_000, GLIB_001, BAGORDER,
      TERMORD, UPROOTS, CHORD, FINSEQ_1, DOMAIN_1, ABIAN, RELSET_1, RECDEF_1,
      FINSUB_1, RFUNCT_3, PRE_POLY;
 constructors DOMAIN_1, FUNCT_4, XXREAL_2, BAGORDER, TERMORD, UPROOTS, CHORD,
      RECDEF_1, RFUNCT_3, RELSET_1, PBOOLE, XTUPLE_0;
 registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, FUNCOP_1,
      FINSET_1, XXREAL_0, XREAL_0, XXREAL_2, NAT_1, INT_1, MEMBERED, FINSEQ_1,
      CARD_1, UPROOTS, GLIB_000, ABIAN, BAGORDER, TERMORD, GLIB_001, CHORD,
      VALUED_0, FINSUB_1, PARTFUN1, RELSET_1, PRE_POLY, XTUPLE_0;
 requirements NUMERALS, SUBSET, BOOLE, REAL, ARITHM;
 definitions GLIB_000, GLIB_001, FUNCOP_1, TARSKI, XTUPLE_0;
 theorems AXIOMS, CARD_1, CARD_2, FUNCOP_1, FINSEQ_1, FINSEQ_2, FINSEQ_3,
      FINSET_1, FUNCT_1, FUNCT_2, FUNCT_4, GLIB_000, GLIB_001, INT_1, NAT_1,
      BAGORDER, TERMORD, ORDINAL1, PARTFUN1, PBOOLE, NAT_D, XREAL_0, RELAT_1,
      RELSET_1, TARSKI, XBOOLE_0, XBOOLE_1, XREAL_1, ZFMISC_1, ENUMSET1, CHORD,
      NECKLACE, FINSEQ_4, WELLORD1, UPROOTS, CARD_FIN, TREES_1, NAT_2,
      XXREAL_0, XXREAL_2, VALUED_0, MCART_1, FINSUB_1, SYSREL, GRFUNC_1;
 schemes NAT_1, FUNCT_1, RECDEF_1, FRAENKEL, PBOOLE, FUNCT_2, CLASSES1;

begin :: Preliminaries
:: What should be the order of RELSET_1, FUNCT_1, FUNCT_2 such that the
:: qua Function and qua Relation are not needed.

Lm1: for F being Function, x,y being set holds dom(F+*(x.-->y)) = dom F \/ {x}
proof
  let F be Function, x,y be set;
  thus dom(F+*(x.-->y)) = dom F \/ dom(x.-->y) by FUNCT_4:def 1
    .= dom F \/ {x} by FUNCOP_1:13;
end;

Lm2: for f being one-to-one Function, X, Y being set st X c= Y for x being set
st x in dom ((f|X)") holds (f|X)".x = (f|Y)".x
proof
  let f be one-to-one Function, X, Y be set;
  assume X c= Y;
  then f|X c= f|Y by RELAT_1:75;
  then
A1: ((f|X) qua Relation)~ c= ((f|Y) qua Relation)~ by SYSREL:11;
  (f|X) is one-to-one by FUNCT_1:52;
  then
A2: ((f|X) qua Relation)~ = (f|X)" by FUNCT_1:def 5;
  (f|Y) is one-to-one by FUNCT_1:52;
  then
A3: ((f|Y) qua Relation)~ = (f|Y)" by FUNCT_1:def 5;
  let x be set;
  assume x in dom ((f|X)");
  hence thesis by A1,A2,A3,GRFUNC_1:2;
end;

:: More general than GRAPH_2:4

theorem
  for A,B being Element of NAT, X being non empty set for F being
Function of NAT, X st F is one-to-one holds card {F.w where w is Element of NAT
  : A <= w & w <= A + B} = B+1
proof
  let A,B be Element of NAT, X be non empty set;
  let F be Function of NAT, X such that
A1: F is one-to-one;
  defpred P[Element of NAT] means card { F.w where w is Element of NAT: A<= w
  & w<=A+$1 } = $1+1;
A2: dom F = NAT by FUNCT_2:def 1;
A3: for k being Element of NAT st P[k] holds P[k+1]
  proof
    let k be Element of NAT such that
A4: P[k];
    set Fwk = {F.w where w is Element of NAT: A<=w & w<=A+k};
    reconsider Fwk as finite set by A4;
    set Fwk1 = {F.w where w is Element of NAT: A<=w & w<=A+k+1};
A5: now
      let x be set;
      hereby
        assume x in Fwk1;
        then consider w being Element of NAT such that
A6:     x = F.w and
A7:     A <= w and
A8:     w<=A+k+1;
A9:     w = A+k+1 or w < A+k+1 by A8,XXREAL_0:1;
        per cases by A9,NAT_1:13;
        suppose
          w = A+k+1;
          then x in {F.(A+k+1)} by A6,TARSKI:def 1;
          hence x in Fwk \/ {F.(A+k+1)} by XBOOLE_0:def 3;
        end;
        suppose
          w <= A + k;
          then x in Fwk by A6,A7;
          hence x in Fwk \/ {F.(A+k+1)} by XBOOLE_0:def 3;
        end;
      end;
      assume
A10:  x in Fwk \/ {F.(A+k+1)};
      per cases by A10,XBOOLE_0:def 3;
      suppose
        x in Fwk;
        then consider w being Element of NAT such that
A11:    x = F.w and
A12:    A <= w and
A13:    w<=A+k;
        w <= A+k+1 by A13,NAT_1:13;
        hence x in Fwk1 by A11,A12;
      end;
      suppose
A14:    x in {F.(A+k+1)};
A15:    A <= A+(k+1) by NAT_1:11;
        x = F.(A+k+1) by A14,TARSKI:def 1;
        hence x in Fwk1 by A15;
      end;
    end;
    now
      assume F.(A+k+1) in Fwk;
      then consider w being Element of NAT such that
A16:  F.(A+k+1) = F.w and
      A <= w and
A17:  w <= A+k;
      A+k+1 = w by A1,A2,A16,FUNCT_1:def 4;
      hence contradiction by A17,NAT_1:13;
    end;
    then card (Fwk \/ {F.(A+k+1)}) = (k+1)+1 by A4,CARD_2:41;
    hence thesis by A5,TARSKI:1;
  end;
  now
    let x be set;
    hereby
      assume x in { F.w where w is Element of NAT: A <= w & w <= A+0};
      then consider w being Element of NAT such that
A18:  F.w = x and
A19:  A<=w and
A20:  w<=A+0;
      w = A by A19,A20,XXREAL_0:1;
      hence x in {F.A} by A18,TARSKI:def 1;
    end;
    assume x in {F.A};
    then x = F.A by TARSKI:def 1;
    hence x in {F.w where w is Element of NAT: A<=w & w<=A+0};
  end;
  then {F.w where w is Element of NAT: A<=w & w<=A+0} = {F.A} by TARSKI:1;
  then
A21: P[ 0 ] by CARD_1:30;
  for k being Element of NAT holds P[k] from NAT_1:sch 1(A21,A3);
  hence thesis;
end;

Lm3: for a,b,c being real number st a < b holds c-b+1 < c-a+1
proof
  let a,b,c be real number;
  assume a < b;
  then c-b < c-a by XREAL_1:10;
  hence thesis by XREAL_1:6;
end;

theorem Th2:
  for n,m,k being Nat st m <= k & n < m holds k -' m < k -' n
proof
  let n,m,k be Nat such that
A1: m <= k and
A2: n < m;
A3: k - m < k - n by A2,XREAL_1:15;
  k -' n = k - n by A1,A2,XREAL_1:233,XXREAL_0:2;
  hence thesis by A1,A3,XREAL_1:233;
end;

notation
  let S be set;
  synonym S is with_finite-elements for S is finite-membered;
end;

registration
  cluster non empty finite with_finite-elements for Subset of bool NAT;
  existence
  proof
    set x = {{1}};
    reconsider x as Subset of bool NAT;
    take x;
    thus x is non empty;
    thus x is finite;
    thus thesis;
  end;
end;

definition
 canceled;
  let f,g be Function;
  func f .\/ g -> Function means
  :Def2:
  dom it = dom f \/ dom g & for x being
  set st x in dom f \/ dom g holds it.x = f.x \/ g.x;
  existence
  proof
    defpred P[set,set] means f.$1 \/ g.$1 = $2;
    set A = dom f \/ dom g;
A1: for x being set st x in A ex y being set st P[x,y];
    ex f being Function st dom f = A & for x being set st x in A holds P[x
    ,f.x] from CLASSES1:sch 1(A1);
    then consider IT being Function such that
A2: dom IT = A and
A3: for x being set st x in A holds P[x,IT.x];
    take IT;
    thus dom IT = dom f \/ dom g by A2;
    thus thesis by A3;
  end;
  uniqueness
  proof
    let IT1,IT2 be Function such that
A4: dom IT1 = dom f \/ dom g and
A5: for x being set st x in dom f \/ dom g holds IT1.x = f.x \/ g.x and
A6: dom IT2 = dom f \/ dom g and
A7: for x being set st x in dom f \/ dom g holds IT2.x = f.x \/ g.x;
    now
      let x be set such that
A8:   x in dom IT1;
      IT1.x = f.x \/ g.x by A4,A5,A8;
      hence IT1.x = IT2.x by A4,A7,A8;
    end;
    hence thesis by A4,A6,FUNCT_1:2;
  end;
end;

theorem Th3:
  for m,n,k being Nat holds m in ((Seg k) \ Seg (k -' n)) iff k -'
  n < m & m <= k
proof
  let m,n,k be Nat;
  hereby
    assume
A1: m in ((Seg k) \ Seg (k -' n));
    then
A2: not m in Seg (k -' n) by XBOOLE_0:def 5;
A3: m in Seg k by A1,XBOOLE_0:def 5;
    then 1 <= m by FINSEQ_1:1;
    hence k -' n < m & m <= k by A3,A2,FINSEQ_1:1;
  end;
  assume that
A4: k -' n < m and
A5: m <= k;
  0+1 <= m by A4,NAT_1:13;
  then
A6: m in Seg k by A5,FINSEQ_1:1;
  not m in Seg (k -' n) by A4,FINSEQ_1:1;
  hence thesis by A6,XBOOLE_0:def 5;
end;

theorem Th4:
  for n,k,m being Nat st n <= m holds ((Seg k) \ Seg (k -' n)) c= (
  (Seg k) \ Seg (k -' m))
proof
  let n,k,m be Nat such that
A1: n <= m;
  per cases;
  suppose
A2: k < m;
A3: for x be set st x in ((Seg k)\Seg(k-'n))holds x in Seg k by XBOOLE_0:def 5;
    k -' m = 0 by A2,NAT_2:8;
    then Seg (k -' m) = {};
    hence thesis by A3,TARSKI:def 3;
  end;
  suppose
A4: m <= k;
    now
      let x be set such that
A5:   x in ((Seg k) \ Seg (k -' n));
      reconsider y = x as Element of NAT by A5;
A6:   k -' n < y by A5,Th3;
      per cases by A1,XXREAL_0:1;
      suppose
        m = n;
        hence x in ((Seg k) \ Seg (k -' m)) by A5;
      end;
      suppose
        n < m;
        then k -' m < k -' n by A4,Th2;
        then
A7:     k -' m < y by A6,XXREAL_0:2;
        y <= k by A5,Th3;
        hence x in ((Seg k) \ Seg (k -' m)) by A7,Th3;
      end;
    end;
    hence thesis by TARSKI:def 3;
  end;
end;

theorem Th5:
  for n,k being Nat st n < k holds ((Seg k) \ Seg (k -' n)) \/ {k
  -' n} = (Seg k) \ Seg (k -' (n+1))
proof
  let n, k be Nat such that
A1: n < k;
  set Sn1 = (Seg k) \ Seg (k -' (n+1));
  set Sn = (Seg k) \ Seg (k -' n);
  now
    let x be set such that
A2: x in Sn \/ {k -' n};
    per cases by A2,XBOOLE_0:def 3;
    suppose
A3:   x in Sn;
      n <= n+1 by NAT_1:13;
      then Sn c= Sn1 by Th4;
      hence x in Sn1 by A3;
    end;
    suppose
A4:   x in {k -' n};
      then reconsider y = x as Nat;
A5:   n < n + 1 by NAT_1:13;
      n+1 <= k by A1,NAT_1:13;
      then
A6:   k -' (n+1) < k -' n by A5,Th2;
A7:   x = k -' n by A4,TARSKI:def 1;
      then y <= k by NAT_D:35;
      hence x in Sn1 by A7,A6,Th3;
    end;
  end;
  then
A8: Sn \/ {k -' n} c= Sn1 by TARSKI:def 3;
  now
    let x be set such that
A9: x in Sn1;
    reconsider y = x as Element of NAT by A9;
A10: y <= k by A9,Th3;
A11: k -' (n+1) + 1 = k -' n by A1,NAT_D:59;
    k -' (n+1) < y by A9,Th3;
    then
A12: k -' n <= y by A11,NAT_1:13;
    per cases by A12,XXREAL_0:1;
    suppose
      k -' n = y;
      then y in {k -' n} by TARSKI:def 1;
      hence x in Sn \/ {k -' n} by XBOOLE_0:def 3;
    end;
    suppose
      k -' n < y;
      then y in Sn by A10,Th3;
      hence x in Sn \/ {k -' n} by XBOOLE_0:def 3;
    end;
  end;
  then Sn1 c= Sn \/ {k -' n} by TARSKI:def 3;
  hence thesis by A8,XBOOLE_0:def 10;
end;

definition
  let f be Relation;
  attr f is natsubset-yielding means
  :Def3:
  rng f c= bool NAT;
end;

registration
  cluster finite-yielding natsubset-yielding for Function;
  existence
  proof
    set F = NAT --> {};
    take F;
    for x be set st x in rng F holds x is finite;
    hence F is finite-yielding by FINSET_1:def 2;
    now
      let x be set;
      assume x in rng F;
      then x = {} by TARSKI:def 1;
      then x c= NAT by XBOOLE_1:2;
      hence x in bool NAT;
    end;
    then rng F c= bool NAT by TARSKI:def 3;
    hence thesis by Def3;
  end;
end;

definition
  let f be finite-yielding natsubset-yielding Function, x be set;
  redefine func f.x -> finite Subset of NAT;
  coherence
  proof
    per cases;
    suppose
A1:   x in dom f;
A2:   rng f c= bool NAT by Def3;
      f.x in rng f by A1,FUNCT_1:3;
      hence thesis by A2;
    end;
    suppose
      not x in dom f;
      then f.x = {} by FUNCT_1:def 2;
      hence thesis by XBOOLE_1:2;
    end;
  end;
end;

theorem Th6:
  for X being Ordinal, a, b be finite Subset of X st a <> b holds (
  a,1)-bag <> (b,1)-bag
proof
  let X be Ordinal, a,b be finite Subset of X such that
A1: a <> b;
  assume
A2: (a,1)-bag = (b,1)-bag;
  now
    let x be set;
    x in a iff (b,1)-bag.x = 1 by A2,UPROOTS:6,7;
    hence x in a iff x in b by UPROOTS:6,7;
  end;
  hence contradiction by A1,TARSKI:1;
end;

definition
  let F be natural-valued Function, S be set, k be Nat;
  func F.incSubset(S,k) -> natural-valued Function means
  :Def4:
  dom it = dom F
  & for y being set holds (y in S & y in dom F implies it.y = F.y + k) & (not y
  in S implies it.y = F.y);
  existence
  proof
    deffunc G(set) = F.$1 + k;
    consider H being Function such that
A1: dom H = S /\ dom F and
A2: for x being set st x in (S /\ dom F) holds H.x = G(x) from FUNCT_1
    :sch 3;
    now
      let x be set;
      assume x in rng H;
      then consider y being set such that
A3:   y in dom H and
A4:   H.y = x by FUNCT_1:def 3;
      H.y = F.y + k by A1,A2,A3;
      hence x in NAT by A4;
    end;
    then
A5: rng H c= NAT by TARSKI:def 3;
A6: rng (F+*H) c= rng F \/ rng H by FUNCT_4:17;
    rng F c= NAT by VALUED_0:def 6;
    then rng F \/ rng H c= NAT by A5,XBOOLE_1:8;
    then rng (F+*H) c= NAT by A6,XBOOLE_1:1;
    then reconsider IT = F+*H as natural-valued Function by VALUED_0:def 6;
    take IT;
    dom IT = dom F \/ (S /\ dom F) by A1,FUNCT_4:def 1;
    hence dom IT = dom F by XBOOLE_1:22;
    now
      let y be set;
A7:   now
        assume that
A8:     y in S and
A9:     y in dom F;
        y in dom H by A1,A8,A9,XBOOLE_0:def 4;
        then
A10:    IT.y = H.y by FUNCT_4:13;
        y in S /\ dom F by A8,A9,XBOOLE_0:def 4;
        hence IT.y = F.y + k by A2,A10;
      end;
      now
        assume not y in S;
        then not y in dom H by A1,XBOOLE_0:def 4;
        hence IT.y = F.y by FUNCT_4:11;
      end;
      hence (y in S & y in dom F implies IT.y = F.y + k) & (not y in S implies
      IT.y = F.y) by A7;
    end;
    hence thesis;
  end;
  uniqueness
  proof
    let IT1,IT2 be natural-valued Function such that
A11: dom IT1 = dom F and
A12: for y being set holds (y in S & y in dom F implies IT1.y = F.y +
    k) & (not y in S implies IT1.y = F.y) and
A13: dom IT2 = dom F and
A14: for y being set holds (y in S & y in dom F implies IT2.y = F.y +
    k) & (not y in S implies IT2.y = F.y);
    now
      let x be set such that
A15:  x in dom IT1;
      per cases by A11,A15;
      suppose
A16:    x in S & x in dom F;
        then IT1.x = F.x + k by A12;
        hence IT1.x = IT2.x by A14,A16;
      end;
      suppose
A17:    not x in S;
        then IT1.x = F.x by A12;
        hence IT1.x = IT2.x by A14,A17;
      end;
    end;
    hence thesis by A11,A13,FUNCT_1:2;
  end;
end;

definition
  let n be Ordinal, T be connected TermOrder of n, B be non empty finite
  Subset of Bags n;
  func max(B,T) -> bag of n means
  :Def5:
  it in B & for x being bag of n st x in B holds x <= it,T;
  existence
  proof
    consider p being FinSequence such that
A1: rng p = B by FINSEQ_1:52;
    defpred P[Nat] means $1 <= len p implies (ex a being Nat, A being bag of n
st a in dom p & a <= $1 & p.a = A & (for c being Nat, C being bag of n st c in
    dom p & c <= $1 & p.c = C holds C <= A, T));
A2: for k being non empty Nat st P[k] holds P[k+1]
    proof
      let k be non empty Nat such that
A3:   P[k];
      per cases;
      suppose
A4:     k < len p;
A5:     1 <= k+1 by CHORD:1;
        k+1 <= len p by A4,NAT_1:13;
        then
A6:     k+1 in dom p by A5,FINSEQ_3:25;
        then p.(k+1) in B by A1,FUNCT_1:def 3;
        then reconsider Ck = p.(k+1) as bag of n;
        consider a being Nat, A being bag of n such that
A7:     a in dom p and
A8:     a <= k and
A9:     p.a = A and
A10:    for c being Nat, C being bag of n st c in dom p & c <= k & p.
        c = C holds C <= A,T by A3,A4;
        set m = max(A,Ck,T);
A11:    A <= m,T by TERMORD:14;
        per cases by TERMORD:12;
        suppose
A12:      m = A;
A13:      now
            let c be Nat,C be bag of n such that
A14:        c in dom p and
A15:        c <= k+1 and
A16:        p.c = C;
            per cases by A15,XXREAL_0:1;
            suppose
              c = k+1;
              hence C <= m,T by A16,TERMORD:14;
            end;
            suppose
              c < k+1;
              then c <= k by NAT_1:13;
              then C <= A,T by A10,A14,A16;
              hence C <= m,T by A11,TERMORD:8;
            end;
          end;
          a <= k+1 by A8,NAT_1:13;
          hence thesis by A7,A9,A12,A13;
        end;
        suppose
A17:      m = Ck;
          now
            let c be Nat, C be bag of n such that
A18:        c in dom p and
A19:        c <= k+1 and
A20:        p.c = C;
            per cases by A19,XXREAL_0:1;
            suppose
              c = k+1;
              hence C <= m,T by A20,TERMORD:14;
            end;
            suppose
              c < k+1;
              then c <= k by NAT_1:13;
              then C <= A,T by A10,A18,A20;
              hence C <= m,T by A11,TERMORD:8;
            end;
          end;
          hence thesis by A6,A17;
        end;
      end;
      suppose
        k >= len p;
        hence thesis by NAT_1:13;
      end;
    end;
A21: p <> {} by A1;
A22: P[1]
    proof
A23:  1 in dom p by A1,FINSEQ_3:32;
      then p.1 in B by A1,FUNCT_1:def 3;
      then reconsider A = p.1 as bag of n;
      now
        let c be Nat, C be bag of n such that
A24:    c in dom p and
A25:    c <= 1 and
A26:    p.c = C;
        1 <= c by A24,FINSEQ_3:25;
        then C = A by A25,A26,XXREAL_0:1;
        hence C <= A,T by TERMORD:6;
      end;
      hence thesis by A23;
    end;
    for k being non empty Nat holds P[k] from NAT_1:sch 10(A22,A2);
    then consider a being Nat, A being bag of n such that
A27: a in dom p and
    a <= len p and
A28: p.a = A and
A29: for c being Nat, C being bag of n st c in dom p & c <= len p & p.
    c = C holds C <= A, T by A21;
    take A;
    thus A in B by A1,A27,A28,FUNCT_1:def 3;
    now
      let x be bag of n;
      assume x in B;
      then consider y being Nat such that
A30:  y in dom p and
A31:  p.y = x by A1,FINSEQ_2:10;
      y <= len p by A30,FINSEQ_3:25;
      hence x <= A,T by A29,A30,A31;
    end;
    hence thesis;
  end;
  uniqueness
  proof
    let IT1,IT2 be bag of n such that
A32: IT1 in B and
A33: for x being bag of n st x in B holds x <= IT1,T and
A34: IT2 in B and
A35: for x being bag of n st x in B holds x <= IT2,T;
A36: IT1 <= IT2,T by A32,A35;
    IT2 <= IT1,T by A33,A34;
    hence IT1 = IT2 by A36,TERMORD:7;
  end;
end;

registration
  let O be Ordinal;
  cluster InvLexOrder O -> connected;
  coherence
  proof
    InvLexOrder O is well-ordering by BAGORDER:25;
    hence thesis by WELLORD1:def 4;
  end;
end;

Lm4: for G being _Graph, W being Walk of G, e,v being set st e Joins W.last(),
v,G holds W.addEdge(e).length() = W.length() + 1
proof
  let G be _Graph, W be Walk of G, e,v be set;
  assume e Joins W.last(),v,G;
  then
A1: W.addEdge(e).edgeSeq() = W.edgeSeq()^<*e*> by GLIB_001:82;
  len <*e*> = 1 by FINSEQ_1:39;
  hence thesis by A1,FINSEQ_1:22;
end;

Lm5: for G being _Graph, W being Walk of G holds W.length() = W.reverse()
.length()
proof
  let G be _Graph, W be Walk of G;
A1: len W = 2*W.length() + 1 by GLIB_001:112;
  len W = len W.reverse() by GLIB_001:21;
  then 2*W.length()+1-1 = 2*W.reverse().length()+1-1 by A1,GLIB_001:112;
  hence thesis;
end;

Lm6: for G being _Graph, W being Walk of G for e,x being set st e Joins W
.last(),x,G for n being Nat st n in dom W holds W.addEdge(e).n = W.n & n in dom
W.addEdge(e)
proof
  let G be _Graph, W be Walk of G;
  let e,x be set such that
A1: e Joins W.last(),x,G;
  let n be Nat such that
A2: n in dom W;
  thus W.addEdge(e).n = W.n by A1,A2,GLIB_001:65;
A3: 1 <= n by A2,FINSEQ_3:25;
A4: len W < len W + 2 by XREAL_1:29;
  n <= len W by A2,FINSEQ_3:25;
  then
A5: n <= len W + 2 by A4,XXREAL_0:2;
  len W.addEdge(e) = len W + 2 by A1,GLIB_001:64;
  hence thesis by A3,A5,FINSEQ_3:25;
end;

begin :: More on Sequences

definition
  let s be ManySortedSet of NAT;
  attr s is iterative means
  :Def6:
  for k, n being Nat st s.k = s.n holds s.(k+ 1) = s.(n+1);
end;

definition
  let S be ManySortedSet of NAT;
  attr S is eventually-constant means
  :Def7:
  ex n being Nat st for m being Nat st n <= m holds S.n = S.m;
end;

registration
  cluster halting iterative eventually-constant for ManySortedSet of NAT;
  existence
  proof
    set Fa = NAT --> 1;
    reconsider F=Fa as ManySortedSet of NAT;
    take F;
    F.0 = 1 by FUNCOP_1:7;
    then F.0 = F.(0+1) by FUNCOP_1:7;
    hence F is halting by GLIB_000:def 54;
    now
      let n,k be Nat such that
      F.n = F.k;
      F.(n+1) = 1 by FUNCOP_1:7;
      hence F.(n+1) = F.(k+1) by FUNCOP_1:7;
    end;
    hence F is iterative by Def6;
    now
      let n be Nat such that
      0 <= n;
A1:   F.0 = 1 by FUNCOP_1:7;
      n in NAT by ORDINAL1:def 12;
      hence F.0 = F.n by A1,FUNCOP_1:7;
    end;
    hence thesis by Def7;
  end;
end;

theorem Th7:
  for Gs being ManySortedSet of NAT st Gs is halting & Gs is
  iterative holds Gs is eventually-constant
proof
  let Gs be ManySortedSet of NAT such that
A1: Gs is halting and
A2: Gs is iterative;
  set GL = Gs.Lifespan();
  defpred P[Nat] means Gs.GL = Gs.(GL+$1);
A3: for k being Nat st P[k] holds P[k+1]
  proof
    let k be Nat;
    assume P[k];
    then Gs.(GL+1) = Gs.(GL+k+1) by A2,Def6;
    hence thesis by A1,GLIB_000:def 55;
  end;
A4: P[ 0 ];
A5: for k being Nat holds P[k] from NAT_1:sch 2(A4,A3);
  now
    let n be Nat;
    assume GL <= n;
    then ex i being Nat st GL + i = n by NAT_1:10;
    hence Gs.GL = Gs.n by A5;
  end;
  hence thesis by Def7;
end;

registration
  cluster halting iterative -> eventually-constant for ManySortedSet of NAT;
  coherence by Th7;
end;

theorem Th8:
  for Gs being ManySortedSet of NAT st Gs is eventually-constant
  holds Gs is halting
proof
  let Gs be ManySortedSet of NAT;
  assume Gs is eventually-constant;
  then consider n being Nat such that
A1: for m being Nat st n <= m holds Gs.n = Gs.m by Def7;
  n <= n+1 by NAT_1:13;
  then Gs.n = Gs.(n+1) by A1;
  hence thesis by GLIB_000:def 54;
end;

registration
  cluster eventually-constant -> halting for ManySortedSet of NAT;
  coherence by Th8;
end;

theorem Th9:
  for Gs being iterative eventually-constant ManySortedSet of NAT
  for n being Nat st Gs.Lifespan() <= n holds Gs.(Gs.Lifespan()) = Gs.n
proof
  let Gs be iterative eventually-constant ManySortedSet of NAT;
  set GL = Gs.Lifespan();
  defpred P[Nat] means Gs.GL = Gs.(GL+$1);
  let n be Nat;
  assume GL <= n;
  then
A1: ex i being Nat st GL + i = n by NAT_1:10;
A2: for k being Nat st P[k] holds P[k+1]
  proof
    let k be Nat;
    assume P[k];
    then Gs.(GL+1) = Gs.(GL+k+1) by Def6;
    hence thesis by GLIB_000:def 55;
  end;
A3: P[ 0 ];
  for k being Nat holds P[k] from NAT_1:sch 2(A3,A2);
  hence thesis by A1;
end;

theorem Th10:
  for Gs being iterative eventually-constant ManySortedSet of NAT
  for n,m being Nat st Gs.Lifespan() <= n & n <= m holds Gs.m = Gs.n
proof
  let Gs be iterative eventually-constant ManySortedSet of NAT;
  let n,m be Nat such that
A1: Gs.Lifespan() <= n and
A2: n <= m;
  Gs.(Gs.Lifespan()) = Gs.m by A1,A2,Th9,XXREAL_0:2;
  hence thesis by A1,Th9;
end;

begin :: Vertex numbering sequences

definition
  let G be finite _Graph;
  mode preVNumberingSeq of G -> ManySortedSet of NAT means
    :Def8:
    for i being Nat holds it.i is PartFunc of the_Vertices_of G, NAT;
  existence
  proof
    deffunc F(set) = {};
    consider f being ManySortedSet of NAT such that
A1: for i being set st i in NAT holds f.i = F(i) from PBOOLE:sch 4;
    take f;
    let i be Nat;
    i in NAT by ORDINAL1:def 12;
    then f.i = {} by A1;
    hence thesis by RELSET_1:12;
  end;
end;

definition
  let G be finite _Graph, S be preVNumberingSeq of G, n be Nat;
  redefine func S.n -> PartFunc of the_Vertices_of G, NAT;
  coherence by Def8;
end;

definition
  let G be finite _Graph, S be preVNumberingSeq of G;
  attr S is vertex-numbering means
  :Def9:
  S.0 = {} & S is iterative & S is
  halting & S.Lifespan() = G.order() & for n being Nat st n < S.Lifespan() ex w
  being Vertex of G st not w in dom (S.n) & (S.(n+1)) = (S.n) +* (w .--> (S
  .Lifespan()-'n));
end;

registration
  let G be finite _Graph;
  cluster vertex-numbering for preVNumberingSeq of G;
  existence
  proof
    set N = card the_Vertices_of G;
    set vs = canFS the_Vertices_of G;
    deffunc F(Element of NAT) = N -' $1 +1;
    consider s being Function of NAT, NAT such that
A1: for n being Element of NAT holds s.n = F(n) from FUNCT_2:sch 4;
    defpred P[set,set] means ex n being Nat st $1 = n & $2 = s*((vs | Seg n)");
A2: for n being set st n in NAT ex j being set st P[n,j]
    proof
      let n be set;
      assume n in NAT;
      then reconsider n9 = n as Nat;
      take s*((vs | Seg n9)");
      thus thesis;
    end;
    consider S being ManySortedSet of NAT such that
A3: for n being set st n in NAT holds P[n,S.n] from PBOOLE:sch 3(A2);
A4: for n being Nat holds S.n = s*((vs | Seg n)")
    proof
      let n be Nat;
      n in NAT by ORDINAL1:def 12;
      then ex i9 being Nat st n = i9 & S.n = s*((vs | Seg i9)") by A3;
      hence thesis;
    end;
A5: for n being Nat st n >= len vs holds S.n = s*(vs")
    proof
A6:   dom vs = Seg len vs by FINSEQ_1:def 3;
      let n be Nat;
      assume n >= len vs;
      then dom vs c= Seg n by A6,FINSEQ_1:5;
      then vs | Seg n = vs by RELAT_1:68;
      hence thesis by A4;
    end;
A7: now
      let i be Nat;
      set Si = s*((vs | Seg i)");
      now
        let x be set;
        assume x in rng Si;
        then x in rng s by FUNCT_1:14;
        hence x in NAT;
      end;
      then
A8:   rng (Si) c= NAT by TARSKI:def 3;
      vs | Seg i is one-to-one by FUNCT_1:52;
      then
A9:   (vs | Seg i)~ = (vs | Seg i)" by FUNCT_1:def 5;
      now
        let x be set;
        assume x in dom Si;
        then x in dom ((vs | Seg i)") by FUNCT_1:11;
        then x in rng (vs | Seg i) by A9,RELAT_1:20;
        hence x in the_Vertices_of G;
      end;
      then
A10:  dom (Si) c= the_Vertices_of G by TARSKI:def 3;
      S.i = s*((vs | Seg i)") by A4;
      hence S.i is PartFunc of the_Vertices_of G, NAT by A10,A8,RELSET_1:4;
    end;
A11: dom s = NAT by FUNCT_2:def 1;
A12: for n being Nat st n <= len vs holds card (S.n) = n
    proof
      let n be Nat;
      assume n <= len vs;
      then
A13:  Seg n c= Seg len vs by FINSEQ_1:5;
A14:  vs | Seg n is one-to-one by FUNCT_1:52;
A15:  S.n = s*((vs | Seg n)") by A4;
A16:  card Seg n = n by FINSEQ_1:57;
      dom vs = Seg len vs by FINSEQ_1:def 3;
      then
A17:  dom (vs | Seg n) = Seg n by A13,RELAT_1:62;
      then rng ((vs | Seg n)") = Seg n by A14,FUNCT_1:33;
      then dom (s*((vs | Seg n)")) = dom ((vs | Seg n)") by A11,RELAT_1:27
        .= rng (vs | Seg n) by A14,FUNCT_1:33;
      then card dom (s*((vs | Seg n)")) = n by A14,A17,A16,CARD_1:70;
      hence thesis by A15,CARD_1:62;
    end;
    reconsider S as preVNumberingSeq of G by A7,Def8;
A18: len vs = N by UPROOTS:3;
A19: S is iterative
    proof
A20:  for k, n being Nat st k < n & S.k = S.n holds S.(k+1) = S.(n+1)
      proof
        let k, n be Nat such that
A21:    k < n and
A22:    S.k = S.n;
        per cases;
        suppose
A23:      n < N;
          then card (S.n) = n by A18,A12;
          hence thesis by A18,A12,A21,A22,A23,XXREAL_0:2;
        end;
        suppose
A24:      N <= n;
          per cases;
          suppose
A25:        k < N;
A26:        rng (vs") c= dom s
            proof
              let x be set;
              assume x in rng (vs");
              then x in rng ((vs qua Relation)~) by FUNCT_1:def 5;
              then x in dom vs by RELAT_1:20;
              then x in NAT;
              hence thesis by FUNCT_2:def 1;
            end;
A27:        S.n = (vs" qua Relation)*s by A18,A5,A24;
            card (S.n) = card dom (S.n) by CARD_1:62
              .= card dom (vs") by A27,A26,RELAT_1:27
              .= card rng vs by FUNCT_1:33
              .= card dom vs by CARD_1:70
              .= len vs by CARD_1:62;
            hence thesis by A18,A12,A22,A25;
          end;
          suppose
A28:        k >= N;
A29:        n+1 >= N by A24,NAT_1:13;
            k+1 >= N by A28,NAT_1:13;
            hence S.(k+1) = s*(vs") by A18,A5
              .= S.(n+1) by A18,A5,A29;
          end;
        end;
      end;
      let k, n be Nat such that
A30:  S.k = S.n;
      per cases by XXREAL_0:1;
      suppose
        k < n;
        hence S.(k+1) = S.(n+1) by A20,A30;
      end;
      suppose
        k > n;
        hence S.(k+1) = S.(n+1) by A20,A30;
      end;
      suppose
        k = n;
        hence thesis;
      end;
    end;
    reconsider N as Element of NAT;
A31: N <= N+1 by NAT_1:11;
A32: N >= len vs by UPROOTS:3;
    then
A33: S.N = s*(vs") by A5
      .= S.(N+1) by A5,A32,A31,XXREAL_0:2;
    then
A34: S is halting by GLIB_000:def 54;
A35: for n being Nat st S.n = S.(n+1) holds N <= n
    proof
      let n be Nat such that
A36:  S.n = S.(n+1) and
A37:  N > n;
A38:  n+1 <= N by A37,NAT_1:13;
      n = card (S.(n+1)) by A18,A12,A36,A37
        .= n+1 by A18,A12,A38;
      hence thesis;
    end;
    then
A39: S.Lifespan() = G.order() by A33,A34,GLIB_000:def 55;
A40: now
      let n be Nat such that
A41:  n < S.Lifespan();
      n < N by A33,A34,A35,A41,GLIB_000:def 55;
      then
A42:  n+1 <= N by NAT_1:13;
      set w = vs.(n+1);
A43:  0+1 <= n+1 by NAT_1:13;
      n+1 <= len vs by A42,UPROOTS:3;
      then
A44:  n+1 in dom vs by A43,FINSEQ_3:25;
      then w in rng vs by FUNCT_1:3;
      then reconsider w as Vertex of G;
      take w;
A45:  vs | Seg n is one-to-one by FUNCT_1:52;
      hereby
        assume w in dom (S.n);
        then w in dom (s*((vs | Seg n)")) by A4;
        then w in dom ((vs | Seg n)") by FUNCT_1:11;
        then w in rng (vs | Seg n) by A45,FUNCT_1:33;
        then consider x being set such that
A46:    x in dom (vs | Seg n) and
A47:    w = (vs | Seg n).x by FUNCT_1:def 3;
A48:    w = vs.x by A46,A47,FUNCT_1:47;
A49:    x in Seg n by A46,RELAT_1:57;
A50:    x in dom vs by A46,RELAT_1:57;
        reconsider x as Nat by A46;
        x <= n by A49,FINSEQ_1:1;
        then x <> n+1 by NAT_1:13;
        hence contradiction by A44,A48,A50,FUNCT_1:def 4;
      end;
A51:  vs | Seg (n+1) is one-to-one by FUNCT_1:52;
      n <= n+1 by NAT_1:11;
      then
A52:  Seg n c= Seg (n+1) by FINSEQ_1:5;
      now
        now
          let x be set;
          hereby
            assume x in dom (S.(n+1));
            then x in dom (s*((vs | Seg (n+1))")) by A4;
            then x in dom ((vs | Seg (n+1))") by FUNCT_1:11;
            then x in rng (vs | Seg (n+1)) by A51,FUNCT_1:33;
            then consider a being set such that
A53:        a in dom (vs | Seg (n+1)) and
A54:        x = (vs | Seg (n+1)).a by FUNCT_1:def 3;
A55:        a in Seg (n+1) by A53,RELAT_1:57;
A56:        dom ((S.n) +* (w .--> (S.Lifespan()-'n))) = dom (S.n) \/ dom
            (w .--> (S.Lifespan()-'n)) by FUNCT_4:def 1;
            reconsider a as Nat by A53;
A57:        a in dom vs by A53,RELAT_1:57;
A58:        a <= n+1 by A55,FINSEQ_1:1;
A59:        1 <= a by A55,FINSEQ_1:1;
            per cases by A58,NAT_1:8;
            suppose
              a <= n;
              then
A60:          a in Seg n by A59,FINSEQ_1:1;
              then
A61:          a in dom (vs | Seg n) by A57,RELAT_1:57;
A62:          (vs | Seg n).a = vs.a by A60,FUNCT_1:49
                .= x by A54,A55,FUNCT_1:49;
              then x in rng (vs | Seg n) by A61,FUNCT_1:3;
              then
A63:          x in dom ((vs | Seg n)") by A45,FUNCT_1:33;
              ((vs | Seg n)").x = a by A45,A61,A62,FUNCT_1:32;
              then ((vs | Seg n)").x in dom s by A11,ORDINAL1:def 12;
              then x in dom (s*((vs | Seg n)")) by A63,FUNCT_1:11;
              then x in dom (S.n) by A4;
              hence x in dom ((S.n) +* (w .--> (S.Lifespan()-'n))) by A56,
XBOOLE_0:def 3;
            end;
            suppose
              a = n+1;
              then x = w by A53,A54,FUNCT_1:47;
              then x in dom (w .--> (S.Lifespan()-'n)) by FUNCOP_1:74;
              hence x in dom ((S.n) +* (w .--> (S.Lifespan()-'n))) by A56,
XBOOLE_0:def 3;
            end;
          end;
          assume x in dom ((S.n) +* (w .--> (S.Lifespan()-'n)));
          then
A64:      x in dom (S.n) \/ dom (w .--> (S.Lifespan()-'n)) by FUNCT_4:def 1;
          per cases by A64,XBOOLE_0:def 3;
          suppose
A65:        x in dom (S.n);
            vs | Seg n c= vs | Seg (n+1) by A52,RELAT_1:75;
            then
A66:        rng (vs | Seg n) c= rng (vs | Seg (n+1)) by RELAT_1:11;
A67:        x in dom (s*((vs | Seg n)")) by A4,A65;
            then
A68:        x in dom ((vs | Seg n)") by FUNCT_1:11;
            then x in rng (vs | Seg n) by A45,FUNCT_1:33;
            then x in rng (vs | Seg (n+1)) by A66;
            then
A69:        x in dom ((vs | Seg (n+1))") by A51,FUNCT_1:33;
A70:        ((vs | Seg n)").x in dom s by A67,FUNCT_1:11;
            ((vs | Seg n)").x = ((vs | Seg (n+1))").x by A52,A68,Lm2;
            then x in dom (s*((vs | Seg (n+1))")) by A70,A69,FUNCT_1:11;
            hence x in dom (S.(n+1)) by A4;
          end;
          suppose
A71:        x in dom (w .--> (S.Lifespan()-'n));
A72:        rng ((vs | Seg (n+1))") = dom (vs | Seg (n+1)) by A51,FUNCT_1:33;
            x = w by A71,FUNCOP_1:75;
            then x in rng (vs | Seg (n+1)) by A44,FINSEQ_1:4,FUNCT_1:50;
            then
A73:        x in dom ((vs | Seg (n+1))") by A51,FUNCT_1:33;
            then ((vs | Seg (n+1))").x in rng ((vs | Seg (n+1))") by FUNCT_1:3
;
            then x in dom (s*((vs | Seg (n+1))")) by A11,A73,A72,FUNCT_1:11;
            hence x in dom (S.(n+1)) by A4;
          end;
        end;
        hence
A74:    dom (S.(n+1)) = dom ((S.n) +* (w .--> (S.Lifespan()-'n))) by TARSKI:1;
        let x be set such that
A75:    x in dom (S.(n+1));
A76:    x in dom (S.n) \/ dom (w .--> (S.Lifespan()-'n)) by A74,A75,
FUNCT_4:def 1;
A77:    S.(n+1) = s*((vs | Seg (n+1))") by A4;
A78:    S.n = s*((vs | Seg n)") by A4;
        per cases by A76,XBOOLE_0:def 3;
        suppose
A79:      x in dom (S.n);
          then
A80:      x in dom ((vs | Seg n)") by A78,FUNCT_1:11;
          then x in rng (vs | Seg n) by A45,FUNCT_1:33;
          then consider m being set such that
A81:      m in dom (vs | Seg n) and
A82:      (vs | Seg n).m = x by FUNCT_1:def 3;
A83:      m in Seg n by A81,RELAT_1:57;
          reconsider m as Nat by A81;
A84:      m in dom vs by A81,RELAT_1:57;
          m <= n by A83,FINSEQ_1:1;
          then
A85:      m < n+1 by NAT_1:13;
          vs.m = x by A81,A82,FUNCT_1:47;
          then
A86:      x <> w by A44,A84,A85,FUNCT_1:def 4;
          thus (S.(n+1)).x = s.(((vs | Seg (n+1))").x) by A75,A77,FUNCT_1:12
            .= s.(((vs | Seg n)").x) by A52,A80,Lm2
            .= (S.n).x by A78,A79,FUNCT_1:12
            .= ((S.n) +* (w .--> (S.Lifespan()-'n))).x by A86,FUNCT_4:83;
        end;
        suppose
A87:      x in dom (w .--> (S.Lifespan()-'n));
          n+1 in Seg (n+1) by FINSEQ_1:4;
          then
A88:      n+1 in dom (vs | Seg (n+1)) by A44,RELAT_1:57;
          then
A89:      (vs | Seg (n+1)).(n+1) = w by FUNCT_1:47;
A90:      x = w by A87,FUNCOP_1:75;
          then x in rng (vs | Seg (n+1)) by A44,FINSEQ_1:4,FUNCT_1:50;
          then
A91:      x in dom ((vs | Seg (n+1))") by A51,FUNCT_1:33;
A92:      ((S.n) +* (w .--> (S.Lifespan()-'n))).x = (w .--> (S
          .Lifespan()-'n)).x by A87,FUNCT_4:13
            .= (S.Lifespan()-'n) by A90,FUNCOP_1:72;
          (S.(n+1)).x = (s*((vs | Seg (n+1))")).x by A4
            .= s.(((vs | Seg (n+1))").x) by A91,FUNCT_1:13
            .= s.(n+1) by A51,A90,A88,A89,FUNCT_1:32
            .= N-'(n+1)+1 by A1
            .= N-(n+1)+1 by A42,XREAL_1:233
            .= N-n
            .= S.Lifespan() -' n by A39,A41,XREAL_1:233;
          hence (S.(n+1)).x = ((S.n) +* (w .--> (S.Lifespan()-'n))).x by A92;
        end;
      end;
      hence S.(n+1) = (S.n) +* (w .--> (S.Lifespan()-'n)) by FUNCT_1:2;
    end;
    take S;
    card (S.0) = 0 by A12;
    then S.0 = {};
    hence thesis by A19,A34,A39,A40,Def9;
  end;
end;

:: Facts hidden in the existence proof?

registration
  let G be finite _Graph;
  cluster vertex-numbering -> halting iterative for preVNumberingSeq of G;
  correctness by Def9;
end;

definition
  let G be finite _Graph;
  mode VNumberingSeq of G is vertex-numbering preVNumberingSeq of G;
end;

definition
  let G be finite _Graph, S be VNumberingSeq of G, n be Nat;
  func S.PickedAt(n) -> set means
  :Def10:
  it = choose the_Vertices_of G if n
  >= S.Lifespan() otherwise not it in dom (S.n) & S.(n+1) = S.n +* (it .--> (S
  .Lifespan()-'n));
  existence
  proof
    per cases;
    suppose
      n >= S.Lifespan();
      hence thesis;
    end;
    suppose
      n < S.Lifespan();
      then
      ex w being Vertex of G st ( not w in dom (S.n))& S.(n+1) = (S.n) +*
      (w .--> (S.Lifespan()-'n)) by Def9;
      hence thesis;
    end;
  end;
  uniqueness
  proof
    set VL1 = S.(n+1);
    set VLN = S.n;
    let IT1,IT2 be set;
    thus n >= S.Lifespan() & IT1 = choose (the_Vertices_of G) & IT2 = choose (
    the_Vertices_of G) implies IT1 = IT2;
    assume n < S.Lifespan();
    assume that
A1: not IT1 in dom VLN and
A2: VL1 = VLN +* (IT1 .--> (S.Lifespan()-'n));
    set f2 = IT2 .--> (S.Lifespan()-'n);
    set f1 = IT1 .--> (S.Lifespan()-'n);
    assume that
    not IT2 in dom VLN and
A3: VL1 = VLN +* (IT2 .--> (S.Lifespan()-'n));
    dom f2 = {IT2} by FUNCOP_1:13;
    then
A4: dom VL1 = dom VLN \/ {IT2} by A3,FUNCT_4:def 1;
    dom f1 = {IT1} by FUNCOP_1:13;
    then
A5: dom VL1 = dom VLN \/ {IT1} by A2,FUNCT_4:def 1;
    now
      assume IT1 <> IT2;
      then not IT1 in {IT2} by TARSKI:def 1;
      then
A6:   not IT1 in dom VL1 by A1,A4,XBOOLE_0:def 3;
      IT1 in {IT1} by TARSKI:def 1;
      hence contradiction by A5,A6,XBOOLE_0:def 3;
    end;
    hence thesis;
  end;
  consistency;
end;

theorem Th11:
  for G being finite _Graph, S being VNumberingSeq of G, n being
Nat st n < S.Lifespan() holds S.PickedAt(n) in dom (S.(n+1)) & dom (S.(n+1)) =
  dom (S.n) \/ {S.PickedAt(n)}
proof
  let G being finite _Graph, GS be VNumberingSeq of G, n be Nat such that
A1: n < GS.Lifespan();
  set f = (GS.PickedAt(n)) .--> (GS.Lifespan() -' n);
  set CN1 = GS.(n+1);
  set CSN = GS.n;
  set VLN = CSN;
  set VN1 = CN1;
A2: dom f = {GS.PickedAt(n)} by FUNCOP_1:13;
A3: GS.PickedAt(n) in {GS.PickedAt(n)} by TARSKI:def 1;
A4: VN1 = VLN +* (GS.PickedAt(n) .--> (GS.Lifespan() -' n)) by A1,Def10;
  then dom VN1 = dom VLN \/ {GS.PickedAt(n)} by A2,FUNCT_4:def 1;
  hence GS.PickedAt(n) in dom CN1 by A3,XBOOLE_0:def 3;
  thus thesis by A4,A2,FUNCT_4:def 1;
end;

theorem Th12:
  for G being finite _Graph, S being VNumberingSeq of G, n being
  Nat st n < S.Lifespan() holds (S.(n+1)).(S.PickedAt(n)) = S.Lifespan()-'n
proof
  let G being finite _Graph, GS be VNumberingSeq of G, n be Nat such that
A1: n < GS.Lifespan();
  set w = GS.PickedAt(n);
  set CN1 = GS.(n+1);
  set CSN = GS.n;
  set VLN = CSN;
  set VN1 = CN1;
  set f = w .--> (GS.Lifespan() -' n);
A2: f.w = GS.Lifespan() -' n by FUNCOP_1:72;
  dom f = {w} by FUNCOP_1:13;
  then
A3: w in dom f by TARSKI:def 1;
  VN1 = VLN +* (w .--> (GS.Lifespan() -' n)) by A1,Def10;
  hence thesis by A3,A2,FUNCT_4:13;
end;

theorem
  for G being finite _Graph, S being VNumberingSeq of G, n being Nat st
  n <= S.Lifespan() holds card dom (S.n) = n
proof
  let G be finite _Graph, S be VNumberingSeq of G, n be Nat such that
A1: n <= S.Lifespan();
  defpred P[Nat] means $1 <= S.Lifespan() implies card dom (S.$1) = $1;
A2: for k being Nat st k < S.Lifespan() & card dom (S.k) = k holds card dom
  (S.(k+1)) = k+1
  proof
    let k be Nat such that
A3: k < S.Lifespan() and
A4: card dom (S.k) = k;
    set w = S.PickedAt(k);
    set CK1 = S.(k+1);
    set CSK = S.k;
    set VLK = CSK;
    set VK1 = CK1;
    set wf = w .--> (S.Lifespan() -' k);
A5: dom wf = {w} by FUNCOP_1:13;
    VK1 = VLK +* (w .--> (S.Lifespan()-'k)) by A3,Def10;
    then
A6: dom VK1 = dom VLK \/ {w} by A5,FUNCT_4:def 1;
    not w in dom VLK by A3,Def10;
    hence thesis by A4,A6,CARD_2:41;
  end;
A7: for k being Nat st P[k] holds P[k+1]
  proof
    let k be Nat such that
A8: P[k];
    per cases;
    suppose
      k < S.Lifespan();
      hence thesis by A2,A8;
    end;
    suppose
      k >= S.Lifespan();
      hence thesis by NAT_1:13;
    end;
  end;
A9: P[ 0 ] by Def9,CARD_1:27,RELAT_1:38;
  for k being Nat holds P[k] from NAT_1:sch 2(A9,A7);
  hence thesis by A1;
end;

theorem Th14:
  for G being finite _Graph, S being VNumberingSeq of G, n being
  Nat holds rng (S.n) = (Seg S.Lifespan()) \ Seg (S.Lifespan()-'n)
proof
  let G be finite _Graph, S be VNumberingSeq of G, n be Nat;
  set CSN = S.n;
  set CSO = S.S.Lifespan();
  set GN = S.Lifespan();
  defpred P[Nat] means $1 <= GN implies rng (S.$1) = (Seg GN) \ Seg (GN-'$1);
A1: for k being Nat st P[k] holds P[k+1]
  proof
    let k be Nat such that
A2: P[k];
    set CK1 = S.(k+1);
    set CSK = S.k;
    set VLK = CSK;
    set VK1 = CK1;
    per cases;
    suppose
A3:   k+1 <= GN;
      set w = S.PickedAt(k);
      set wf = w .--> (GN -' k);
A4:   dom wf = {w} by FUNCOP_1:13;
A5:   k < GN by A3,NAT_1:13;
      then not w in dom VLK by Def10;
      then
A6:   dom wf misses dom VLK by A4,ZFMISC_1:50;
A7:   rng wf = {GN -' k} by FUNCOP_1:8;
      VK1 = VLK +* (w .--> (GN -' k)) by A5,Def10;
      then rng VK1 = rng VLK \/ {GN -' k} by A7,A6,NECKLACE:6;
      hence thesis by A2,A5,Th5;
    end;
    suppose
      GN < k+1;
      hence thesis;
    end;
  end;
A8: P[ 0 ]
  proof
    set CS0 = S.0;
    set VL0 = CS0;
A9: GN -' 0 = GN - 0 by XREAL_1:233;
    rng VL0 = {} by Def9,RELAT_1:38;
    hence thesis by A9,XBOOLE_1:37;
  end;
A10: for k being Nat holds P[k] from NAT_1:sch 2(A8,A1);
  per cases;
  suppose
    n <= GN;
    hence thesis by A10;
  end;
  suppose
A11: GN < n;
    then GN - n < n - n by XREAL_1:9;
    then GN -' n = 0 by XREAL_0:def 2;
    then
A12: GN -' GN = GN -' n by XREAL_1:232;
    CSO = CSN by A11,Th9;
    hence thesis by A10,A12;
  end;
end;

theorem Th15:
  for G being finite _Graph, S being VNumberingSeq of G, n being
Nat, x being set holds (S.n).x <= S.Lifespan() & (x in dom (S.n) implies 1 <= (
  S.n).x)
proof
  let G be finite _Graph, S be VNumberingSeq of G, n be Nat, x be set;
  set CSN = S.n;
  set VLN = CSN;
A1: now
    per cases;
    suppose
      not x in dom VLN;
      hence VLN.x <= S.Lifespan() by FUNCT_1:def 2;
    end;
    suppose
      x in dom VLN;
      then VLN.x in rng VLN by FUNCT_1:def 3;
      then VLN.x in (Seg S.Lifespan()) \ Seg (S.Lifespan() -'n ) by Th14;
      hence VLN.x <= S.Lifespan() by Th3;
    end;
  end;
  now
    assume x in dom (S.n);
    then VLN.x in rng VLN by FUNCT_1:def 3;
    then VLN.x in (Seg S.Lifespan()) \ Seg (S.Lifespan() -'n ) by Th14;
    then S.Lifespan() -' n < VLN.x by Th3;
    then 0+1 <= VLN.x by NAT_1:13;
    hence 1 <= VLN.x;
  end;
  hence thesis by A1;
end;

theorem Th16:
  for G being finite _Graph, S being VNumberingSeq of G, n,m being
Nat st S.Lifespan() -' n < m & m <= S.Lifespan() ex v being Vertex of G st v in
  dom (S.n) & (S.n).v = m
proof
  let G being finite _Graph, S be VNumberingSeq of G, n,m be Nat such that
A1: S.Lifespan() -' n < m and
A2: m <= S.Lifespan();
  set CSN = S.n;
  set VLN = CSN;
  m in (Seg S.Lifespan()) \ Seg (S.Lifespan()-'n) by A1,A2,Th3;
  then m in rng VLN by Th14;
  then consider v being set such that
A3: v in dom VLN and
A4: m = VLN.v by FUNCT_1:def 3;
  take v;
  thus v is Vertex of G by A3;
  thus v in dom CSN by A3;
  thus thesis by A4;
end;

theorem Th17:
  for G being finite _Graph, S being VNumberingSeq of G, m, n
  being Nat st m <= n holds S.m c= S.n
proof
  let G be finite _Graph, S be VNumberingSeq of G, m,n be Nat;
  assume m <= n;
  then
A1: ex j being Nat st n = m + j by NAT_1:10;
  set CSM = S.m;
  set VLM = CSM;
  defpred P[Nat] means VLM c= S.(m+$1);
A2: now
    let k be Nat;
    set CSK = S.k;
    set VLK = CSK;
    set CK1 = S.(k+1);
    set VK1 = CK1;
    per cases;
    suppose
A3:   k < S.Lifespan();
      set w = S.PickedAt(k);
      set wf = w .--> (S.Lifespan() -' k);
A4:   dom wf = {w} by FUNCOP_1:13;
      not w in dom VLK by A3,Def10;
      then
A5:   dom wf misses dom VLK by A4,ZFMISC_1:50;
      VK1 = VLK +* (w .--> (S.Lifespan()-'k)) by A3,Def10;
      hence VLK c= VK1 by A5,FUNCT_4:32;
    end;
    suppose
A6:   S.Lifespan() <= k;
      k <= k+1 by NAT_1:13;
      hence VLK c= VK1 by A6,Th10;
    end;
  end;
A7: for k being Nat st P[k] holds P[k+1]
  proof
    let k be Nat such that
A8: P[k];
    S.(m+k) c= S.(m+k+1) by A2;
    hence thesis by A8,XBOOLE_1:1;
  end;
A9: P[ 0 ];
  for k being Nat holds P[k] from NAT_1:sch 2(A9,A7);
  hence thesis by A1;
end;

theorem Th18:
  for G being finite _Graph, S being VNumberingSeq of G, n being
  Nat holds S.n is one-to-one
proof
  let G being finite _Graph, S be VNumberingSeq of G, n be Nat;
  defpred P[Nat] means S.$1 is one-to-one;
A1: for k being Nat st P[k] holds P[k+1]
  proof
    set GN = S.Lifespan();
    let k be Nat such that
A2: P[k];
    set w = S.PickedAt(k);
    set CK1 = S.(k+1);
    set CSK = S.k;
    set VLK = CSK;
    set VL1 = CK1;
    per cases;
    suppose
A3:   k < GN;
      set wf = w .--> (GN -' k);
A4:   now
        assume
A5:     GN -' k in rng VLK;
        rng VLK = (Seg GN) \ Seg (GN -' k) by Th14;
        hence contradiction by A5,Th3;
      end;
      rng wf = {GN -' k} by FUNCOP_1:8;
      then
A6:   rng wf misses rng VLK by A4,ZFMISC_1:50;
      VL1 = VLK +* (w .--> (GN -' k)) by A3,Def10;
      hence thesis by A2,A6,FUNCT_4:92;
    end;
    suppose
A7:   k >= GN;
      k <= k+1 by NAT_1:13;
      hence thesis by A2,A7,Th10;
    end;
  end;
A8: P[ 0 ] by Def9;
  for k being Nat holds P[k] from NAT_1:sch 2(A8,A1);
  hence thesis;
end;

theorem Th19:
  for G being finite _Graph, S being VNumberingSeq of G, m,n being
  Nat, v being set st v in dom (S.m) & v in dom (S.n) holds (S.m).v = (S.n).v
proof
  let G be finite _Graph, S be VNumberingSeq of G, m,n be Nat;
  let v be set such that
A1: v in dom (S.m) and
A2: v in dom (S.n);
  set VLM = S.m;
A3: [v,VLM.v] in VLM by A1,FUNCT_1:def 2;
  set VLN = S.n;
A4: [v,VLN.v] in VLN by A2,FUNCT_1:def 2;
  per cases;
  suppose
    m <= n;
    then VLM c= VLN by Th17;
    hence thesis by A2,A3,FUNCT_1:def 2;
  end;
  suppose
    m > n;
    then VLN c= VLM by Th17;
    hence thesis by A1,A4,FUNCT_1:def 2;
  end;
end;

theorem Th20:
  for G being finite _Graph, S being VNumberingSeq of G, m,n being
Nat, v being set st v in dom (S.m) & (S.m).v = n holds S.PickedAt(S.Lifespan()
  -'n) = v
proof
  let G be finite _Graph, S be VNumberingSeq of G, m,n be Nat, v be set;
  set CSM = S.m;
  set VLM = CSM;
  set j = S.Lifespan() -' n;
  set CJ1 = S.(j+1);
  set VJ1 = CJ1;
  assume that
A1: v in dom CSM and
A2: VLM.v = n;
  set w = S.PickedAt(j);
  n <= S.Lifespan() by A2,Th15;
  then
A3: S.Lifespan() -' n = S.Lifespan() - n by XREAL_1:233;
A4: 0 < n by A1,A2,Th15;
  then
A5: j < S.Lifespan() by A3,XREAL_1:44;
  then S.Lifespan() -' j = S.Lifespan() - (S.Lifespan() - n) by A3,XREAL_1:233;
  then
A6: VJ1.w = n by A4,A3,Th12,XREAL_1:44;
A7: VLM is one-to-one by Th18;
A8: w in dom CJ1 by A5,Th11;
  per cases;
  suppose
A9: m <= j;
    then m + n <= S.Lifespan() - n + n by A3,XREAL_1:6;
    then
A10: n + m - m <= S.Lifespan() - m by XREAL_1:9;
A11: rng VLM = (Seg S.Lifespan()) \ Seg (S.Lifespan() -' m) by Th14;
A12: n in rng VLM by A1,A2,FUNCT_1:def 3;
    S.Lifespan() - m = S.Lifespan() -' m by A5,A9,XREAL_1:233,XXREAL_0:2;
    hence thesis by A10,A12,A11,Th3;
  end;
  suppose
    j < m;
    then j+1 <= m by NAT_1:13;
    then
A13: VJ1 c= VLM by Th17;
    then
A14: dom VJ1 c= dom VLM by RELAT_1:11;
    [w,n] in VJ1 by A8,A6,FUNCT_1:def 2;
    then VLM.w = n by A8,A13,A14,FUNCT_1:def 2;
    hence thesis by A1,A2,A8,A7,A14,FUNCT_1:def 4;
  end;
end;

theorem Th21:
  for G being finite _Graph, S being VNumberingSeq of G, m, n
being Nat st n < S.Lifespan() & n < m holds S.PickedAt(n) in dom (S.m) & (S.m).
  (S.PickedAt(n)) = S.Lifespan() -' n
proof
  let G be finite _Graph, S be VNumberingSeq of G, m,n be Nat such that
A1: n < S.Lifespan() and
A2: n < m;
  set CN1 = S.(n+1);
  set VN1 = CN1;
  set v = S.PickedAt(n);
A3: VN1.v = S.Lifespan() -' n by A1,Th12;
  set CSM = S.m;
  set VLM = CSM;
  n+1 <= m by A2,NAT_1:13;
  then VN1 c= VLM by Th17;
  then
A4: dom VN1 c= dom VLM by RELAT_1:11;
  v in dom CN1 by A1,Th11;
  hence thesis by A3,A4,Th19;
end;

:: Inequalities relating the vlabel and the current iteration

theorem Th22:
  for G being finite _Graph, S being VNumberingSeq of G, m being
  Nat, v being set st v in dom (S.m) holds S.Lifespan() -' (S.m).v < m & S
  .Lifespan() -' m < (S.m).v
proof
  let G be finite _Graph, S be VNumberingSeq of G, m be Nat, v be set;
  set VLM = S.m;
  set j = S.Lifespan() -' VLM.v;
  set VLJ = S.j;
  assume
A1: v in dom VLM;
  then
A2: S.PickedAt(j) = v by Th20;
A3: 0 < VLM.v by A1,Th15;
A4: VLM.v <= S.Lifespan() by Th15;
  then j = S.Lifespan() - VLM.v by XREAL_1:233;
  then
A5: j < S.Lifespan() by A3,XREAL_1:44;
A6: now
    per cases;
    suppose
      m <= j;
      then VLM c= VLJ by Th17;
      then dom VLM c= dom VLJ by RELAT_1:11;
      hence S.Lifespan() -' VLM.v < m by A1,A2,A5,Def10;
    end;
    suppose
      m > j;
      hence S.Lifespan() -' VLM.v < m;
    end;
  end;
  now
    per cases;
    suppose
A7:   S.Lifespan() - m >= 0;
      S.Lifespan() - VLM.v < m by A4,A6,XREAL_1:233;
      then S.Lifespan() - VLM.v + VLM.v < m + VLM.v by XREAL_1:6;
      then S.Lifespan() - m < VLM.v + m - m by XREAL_1:9;
      hence S.Lifespan() -'m < VLM.v by A7,XREAL_0:def 2;
    end;
    suppose
      S.Lifespan() - m < 0;
      hence S.Lifespan() -'m < VLM.v by A3,XREAL_0:def 2;
    end;
  end;
  hence thesis by A6;
end;

:: If a vertex has a larger vlabel than we do at some point in the
:: algorithm, then it must have been in the vlabel when we were picked

theorem Th23:
  for G being finite _Graph, S being VNumberingSeq of G, i being
Nat, a,b being set st a in dom (S.i) & b in dom (S.i) & (S.i).a < (S.i).b holds
  b in dom (S.(S.Lifespan() -' (S.i).a))
proof
  let G be finite _Graph, S be VNumberingSeq of G;
  let i be Nat, a,b be set such that
A1: a in dom (S.i) and
A2: b in dom (S.i) and
A3: (S.i).a < (S.i).b;
  set GN = S.Lifespan();
  set CSI = S.i;
  set VLI = CSI;
  set j = S.Lifespan() -' VLI.a;
  set CSJ = S.j;
  set VLJ = CSJ;
  VLI.a <= GN by Th15;
  then
A4: GN -' VLI.a = GN - VLI.a by XREAL_1:233;
  then GN -' j = GN - (GN - VLI.a) by NAT_D:35,XREAL_1:233;
  then consider w being Vertex of G such that
A5: w in dom CSJ and
A6: VLJ.w = VLI.b by A3,Th15,Th16;
  now
    assume j >= i;
    then VLI c= VLJ by Th17;
    then
A7: dom VLI c= dom VLJ by RELAT_1:11;
    0 < VLI.a by A1,Th15;
    then
A8: j < GN by A4,XREAL_1:44;
    a = S.PickedAt(j) by A1,Th20;
    hence contradiction by A1,A7,A8,Def10;
  end;
  then
A9: VLJ c= VLI by Th17;
A10: [w,VLI.b] in VLJ by A5,A6,FUNCT_1:1;
  then
A11: VLI.w = VLI.b by A9,FUNCT_1:1;
A12: VLI is one-to-one by Th18;
  w in dom VLI by A9,A10,FUNCT_1:1;
  hence thesis by A2,A5,A11,A12,FUNCT_1:def 4;
end;

theorem Th24:
  for G being finite _Graph, S being VNumberingSeq of G, i being
Nat, a,b being set st a in dom (S.i) & (S.i).a < (S.i).b holds not a in dom (S.
  (S.Lifespan() -' (S.i).b))
proof
  let G be finite _Graph, S be VNumberingSeq of G, i be Nat, a,b being set
  such that
A1: a in dom (S.i) and
A2: (S.i).a < (S.i).b;
  set GN = S.Lifespan();
  set CSI = S.i;
  set VLI = CSI;
  set k = GN -' VLI.a;
  VLI.a <= GN by Th15;
  then
A3: k = GN - VLI.a by XREAL_1:233;
  set CSK = S.k;
  set j = GN -' VLI.b;
  set CSJ = S.j;
  set VLJ = CSJ;
  set VLK = CSK;
  VLI.b <= GN by Th15;
  then j = GN - VLI.b by XREAL_1:233;
  then j < k by A2,A3,XREAL_1:15;
  then VLJ c= VLK by Th17;
  then
A4: dom VLJ c= dom VLK by RELAT_1:11;
  assume
A5: a in dom CSJ;
  1 <= VLI.a by A1,Th15;
  then
A6: k < GN by A3,XREAL_1:44;
  S.PickedAt(k) = a by A1,Th20;
  hence contradiction by A6,A5,A4,Def10;
end;

begin :: Lexicographic Breadth-First Search

definition
  let X1,X3 be set, X2 be non empty set;
  let x be Element of [: PFuncs(X1,X3),X2 :];
  redefine func x`1 -> Element of PFuncs(X1,X3);
  coherence by MCART_1:10;
end;

definition
  let X1, X3 be non empty set, X2 be set;
  let x be Element of [: X1, Funcs(X2,X3) :];
  redefine func x`2 -> Element of Funcs(X2,X3);
  coherence by MCART_1:10;
end;

definition
  let G be _Graph;
  mode LexBFS:Labeling of G is Element of [: PFuncs(the_Vertices_of G, NAT),
    Funcs(the_Vertices_of G, Fin NAT) :];
end;

registration
  let G be finite _Graph, L be LexBFS:Labeling of G;
  cluster L`1 -> finite;
  coherence
  proof
    dom L`1 c= the_Vertices_of G;
    hence thesis by FINSET_1:10;
  end;
  cluster L`2 -> finite;
  coherence;
end;

definition
  let G be _Graph;
  func LexBFS:Init(G) -> LexBFS:Labeling of G equals
  [ {}, the_Vertices_of G
  --> {} ];
  coherence
  proof
    set f = the_Vertices_of G --> {};
A1: rng {} c= NAT;
    {} c= NAT;
    then {} in Fin NAT by FINSUB_1:def 5;
    then {{}} c= Fin NAT by ZFMISC_1:31;
    then
A2: rng f c= Fin NAT by XBOOLE_1:1;
    dom f = the_Vertices_of G by FUNCOP_1:13;
    then
A3: f in Funcs(the_Vertices_of G, Fin NAT) by A2,FUNCT_2:def 2;
    dom {} c= the_Vertices_of G by XBOOLE_1:2;
    then {} in PFuncs(the_Vertices_of G,NAT) by A1,PARTFUN1:def 3;
    hence thesis by A3,ZFMISC_1:def 2;
  end;
end;

definition
  let G be finite _Graph, L be LexBFS:Labeling of G;
  func LexBFS:PickUnnumbered(L) -> Vertex of G means
  :Def12:
  it = choose
the_Vertices_of G if dom L`1 = the_Vertices_of G otherwise ex S being non empty
finite Subset of bool NAT, B being non empty finite Subset of Bags NAT, F being
Function st S = rng F & F = L`2 | (the_Vertices_of G \ dom L`1) & (for x being
finite Subset of NAT holds x in S implies ((x,1)-bag in B)) & (for x being set
holds x in B implies ex y being finite Subset of NAT st y in S & x = (y,1)-bag)
  & it = choose (F " {support max(B,InvLexOrder NAT)});
  existence
  proof
    set VG = the_Vertices_of G;
    set V2G = L`2;
    set VLG = L`1;
    set F = V2G | (VG \ dom VLG);
    set S = rng F;
A1: ex f being Function st L`2 = f & dom f = VG & rng f c= Fin NAT by
FUNCT_2:def 2;
    per cases;
    suppose
      dom VLG = VG;
      hence thesis;
    end;
    suppose
A2:   dom VLG <> VG;
      dom F = dom V2G /\ (VG \ dom VLG) by RELAT_1:61;
      then
A3:   dom F = (VG /\ VG) \ dom VLG by A1,XBOOLE_1:49;
A4:   now
        assume dom F = {};
        then VG c= dom VLG by A3,XBOOLE_1:37;
        hence contradiction by A2,XBOOLE_0:def 10;
      end;
A5:   for x being set st x in S holds x is finite;
A6:   rng F c= rng V2G by RELAT_1:70;
      now
A7:     rng V2G c= bool NAT
        proof
          let x be set;
          assume x in rng V2G;
          then x c= NAT by FINSUB_1:def 5;
          hence thesis;
        end;
        let x be set such that
A8:     x in S;
        x in rng V2G by A6,A8;
        hence x in bool NAT by A7;
        thus x is finite by A8;
      end;
      then for x being set holds x in S implies x in bool NAT;
      then reconsider
      S as non empty finite with_finite-elements Subset of bool NAT
      by A4,A5,FINSET_1:def 6,RELAT_1:42,TARSKI:def 3;
      deffunc F(finite Subset of NAT) = ($1,1)-bag;
      set B = {F(x) where x is Element of S: x in S};
      consider z being set such that
A9:  z in S by XBOOLE_0:def 1;
      reconsider z as finite Subset of NAT by A9;
A10:  (z,1)-bag in B by A9;
A11:  S is finite;
A12:  B is finite from FRAENKEL:sch 21(A11);
      now
        let x be set;
        assume x in B;
        then ex y being Element of S st x = (y,1)-bag & y in S;
        hence x in Bags NAT;
      end;
      then reconsider B as non empty finite Subset of Bags NAT by A12,A10,
TARSKI:def 3;
A13:  for x being set holds x in B implies ex y being finite Subset of
      NAT st y in S & x = (y,1)-bag
      proof
        let x be set;
        assume x in B;
        then ex y being Element of S st x = (y,1)-bag & y in S;
        hence thesis;
      end;
      set mw = max(B,InvLexOrder NAT);
      mw in B by Def5;
      then consider y being finite Subset of NAT such that
A14:  y in S and
A15:  mw = (y,1)-bag by A13;
      set IT = choose (F " {support mw});
      y = support mw by A15,UPROOTS:8;
      then F " {support mw} is non empty by A14,FUNCT_1:72;
      then IT in dom F by FUNCT_1:def 7;
      then IT in dom V2G by RELAT_1:57;
      then reconsider IT as Vertex of G;
      for x being finite Subset of NAT holds x in S implies (x,1)-bag in B;
      then ex S being non empty finite Subset of bool NAT, B being non empty
finite Subset of Bags NAT, F being Function st S = rng F & F = (V2G | (VG \ dom
VLG)) & (for x being finite Subset of NAT holds x in S implies ((x,1)-bag in B)
) & (for x being set holds x in B implies ex y being finite Subset of NAT st y
in S & x = (y,1)-bag) & IT = choose (F " {support max(B,InvLexOrder NAT)}) & IT
      is Vertex of G by A13;
      hence thesis;
    end;
  end;
  uniqueness
  proof
    let IT1, IT2 be Vertex of G;
    set VG = the_Vertices_of G;
    set V2G = L`2;
    set VLG = L`1;
    thus dom VLG = VG & IT1 = choose VG & IT2 = choose VG implies IT1=IT2;
    assume dom VLG <> VG;
    assume ex S1 being non empty finite Subset of bool NAT, B1 being non
empty finite Subset of Bags NAT, F1 being Function st S1 = rng F1 & F1 = (V2G |
(VG \ dom VLG)) & (for x being finite Subset of NAT holds x in S1 implies ((x,1
)-bag in B1)) & (for x being set holds x in B1 implies ex y being finite Subset
    of NAT st y in S1 & x = (y,1)-bag) & IT1 = choose (F1 " {support max(B1,
    InvLexOrder NAT)});
    then consider
    S1 being non empty finite Subset of bool NAT, B1 being non empty
    finite Subset of Bags NAT, F1 being Function such that
A16: S1 = rng F1 and
A17: F1 = (V2G | (VG \ dom VLG)) and
A18: for x being finite Subset of NAT holds x in S1 implies (x,1)-bag in B1 and
A19: for x being set holds x in B1 implies ex y being finite Subset of
    NAT st y in S1 & x = (y,1)-bag and
A20: IT1 = choose (F1 " {support max(B1,InvLexOrder NAT)});
    assume ex S2 being non empty finite Subset of bool NAT, B2 being non
empty finite Subset of Bags NAT, F2 being Function st S2 = rng F2 & F2 = (V2G |
(VG \ dom VLG)) & (for x being finite Subset of NAT holds x in S2 implies ((x,1
)-bag in B2)) & (for x being set holds x in B2 implies ex y being finite Subset
    of NAT st y in S2 & x = (y,1)-bag) & IT2 = choose (F2 " {support max(B2,
    InvLexOrder NAT)});
    then consider
    S2 being non empty finite Subset of bool NAT, B2 being non empty
    finite Subset of Bags NAT, F2 being Function such that
A21: S2 = rng F2 and
A22: F2 = (V2G | (VG \ dom VLG)) and
A23: for x being finite Subset of NAT holds x in S2 implies (x,1)-bag in B2 and
A24: for x being set holds x in B2 implies ex y being finite Subset of
    NAT st y in S2 & x = (y,1)-bag and
A25: IT2 = choose (F2 " {support max(B2,InvLexOrder NAT)});
    now
      let x be set;
      assume x in B2;
      then
      ex y being finite Subset of NAT st y in S2 & x = (y,1)-bag by A24;
      hence x in B1 by A16,A17,A18,A21,A22;
    end;
    then
A26: B2 c= B1 by TARSKI:def 3;
    now
      let x be set;
      assume x in B1;
      then
      ex y being finite Subset of NAT st y in S1 & x = (y,1)-bag by A19;
      hence x in B2 by A16,A17,A21,A22,A23;
    end;
    then B1 c= B2 by TARSKI:def 3;
    hence thesis by A17,A20,A22,A25,A26,XBOOLE_0:def 10;
  end;
  consistency;
end;

definition
  let G be finite _Graph, L be LexBFS:Labeling of G, v be Vertex of G, n be
  Nat;
  func LexBFS:Update(L, v, n) -> LexBFS:Labeling of G equals
  [ L`1 +* (v .-->
(G.order()-'n)), L`2 .\/ ((G.AdjacentSet({v}) \ dom L`1) --> {G.order()-'n}) ];
  coherence
  proof
    set F = ((G.AdjacentSet({v}) \ dom L`1) --> {G.order()-'n});
    reconsider nn = G.order()-'n as Element of NAT;
    set L2 = L`2 .\/ ((G.AdjacentSet({v}) \ dom L`1) --> {G.order()-'n});
    set f = (v .--> (G.order()-'n));
    set L1 = L`1 +* f;
A1: dom f = {v} by FUNCOP_1:13;
    rng f c= {G.order()-'n} by FUNCOP_1:13;
    then rng f c= NAT by XBOOLE_1:1;
    then
A2: rng L`1 \/ rng f c= NAT by XBOOLE_1:8;
    rng L1 c= rng L`1 \/ rng f by FUNCT_4:17;
    then
A3: rng L1 c= NAT by A2,XBOOLE_1:1;
    dom L1 = dom L`1 \/ dom f by FUNCT_4:def 1;
    then dom L1 c= the_Vertices_of G by A1,XBOOLE_1:8;
    then
A4: L1 in PFuncs(the_Vertices_of G, NAT) by A3,PARTFUN1:def 3;
    {nn} in Fin NAT by FINSUB_1:def 5;
    then
A5: {{nn}} c= Fin NAT by ZFMISC_1:31;
    consider f being Function such that
A6: L`2 = f and
A7: dom f = the_Vertices_of G and
A8: rng f c= Fin NAT by FUNCT_2:def 2;
    rng F c= {{nn}} by FUNCOP_1:13;
    then
A9: rng F c= Fin NAT by A5,XBOOLE_1:1;
A10:  dom L2 = dom f \/ dom F by A6,Def2;
A11: rng L2 c= Fin NAT
    proof
      let y be set;
      assume y in rng L2;
      then consider x being set such that
A12:  x in dom L2 and
A13:  y = L2.x by FUNCT_1:def 3;
A14:  y = f.x \/ F.x by A6,A12,A13,Def2,A10;
      per cases by A12,A10,XBOOLE_0:def 3;
      suppose that
A15:    x in dom f and
A16:    not x in dom F;
A17:    F.x = {} by A16,FUNCT_1:def 2;
        f.x in rng f by A15,FUNCT_1:3;
        hence thesis by A8,A14,A17;
      end;
      suppose that
A18:    not x in dom f and
A19:    x in dom F;
A20:    f.x = {} by A18,FUNCT_1:def 2;
        F.x in rng F by A19,FUNCT_1:3;
        hence thesis by A9,A14,A20;
      end;
      suppose that
A21:    x in dom f and
A22:    x in dom F;
A23:    F.x in rng F by A22,FUNCT_1:3;
        f.x in rng f by A21,FUNCT_1:3;
        hence thesis by A8,A9,A14,A23,FINSUB_1:def 1;
      end;
    end;
    dom F = G.AdjacentSet({v}) \ dom L`1 by FUNCOP_1:13;
    then
A24: dom F c= the_Vertices_of G;
    dom L2 = dom f \/ dom F by A10;
    then dom L2 = the_Vertices_of G by A7,A24,XBOOLE_1:12;
    then L2 in Funcs(the_Vertices_of G, Fin NAT) by A11,FUNCT_2:def 2;
    hence thesis by A4,ZFMISC_1:def 2;
  end;
end;

theorem Th25:
  for G being finite _Graph, L being LexBFS:Labeling of G, v being
Vertex of G, x being set, k being Nat st not x in G.AdjacentSet({v}) holds L`2.
  x = (LexBFS:Update(L,v,k))`2.x
proof
  let G be finite _Graph, L be LexBFS:Labeling of G, v be Vertex of G, x be
  set, k be Nat such that
A1: not x in G.AdjacentSet({v});
  set F = (G.AdjacentSet({v}) \ dom L`1) --> {G.order()-'k};
A2: not x in dom F by A1,XBOOLE_0:def 5;
  then
A3: F.x = {} by FUNCT_1:def 2;
  set L2 = LexBFS:Update(L,v,k)`2;
A4: L2 = L`2 .\/ F by MCART_1:7;
  per cases;
  suppose
    x in dom L`2;
    then x in dom L`2 \/ dom F by XBOOLE_0:def 3;
    hence L2.x = L`2.x \/ F.x by A4,Def2
      .= L`2.x by A3;
  end;
  suppose
A5: not x in dom L`2;
    then not x in dom L`2 \/ dom F by A2,XBOOLE_0:def 3;
    then not x in dom L2 by A4,Def2;
    hence L2.x = {} by FUNCT_1:def 2
      .= L`2.x by A5,FUNCT_1:def 2;
  end;
end;

theorem Th26:
  for G being finite _Graph, L being LexBFS:Labeling of G, v being
Vertex of G, x being set, k being Nat st x in dom L`1 holds LexBFS:Update(L,v,k
  )`2.x = L`2.x
proof
  let G be finite _Graph, L be LexBFS:Labeling of G, v be Vertex of G, x be
  set, k be Nat such that
A1: x in dom L`1;
  set F = (G.AdjacentSet({v}) \ dom L`1) --> {G.order()-'k};
A2: not x in dom F by A1,XBOOLE_0:def 5;
  then
A3: F.x = {} by FUNCT_1:def 2;
  set L2 = LexBFS:Update(L,v,k)`2;
A4: L2 = L`2 .\/ F by MCART_1:7;
  per cases;
  suppose
    x in dom L`2;
    then x in dom L`2 \/ dom F by XBOOLE_0:def 3;
    hence L2.x = L`2.x \/ F.x by A4,Def2
      .= L`2.x by A3;
  end;
  suppose
A5: not x in dom L`2;
    then not x in dom L`2 \/ dom F by A2,XBOOLE_0:def 3;
    then not x in dom L2 by A4,Def2;
    hence L2.x = {} by FUNCT_1:def 2
      .= L`2.x by A5,FUNCT_1:def 2;
  end;
end;

theorem Th27:
  for G being finite _Graph, L being LexBFS:Labeling of G, v be
Vertex of G, x being set, k being Nat st x in G.AdjacentSet({v}) & not x in dom
  L`1 holds LexBFS:Update(L,v,k)`2.x = L`2.x \/ {G.order() -' k}
proof
  let G be finite _Graph, L be LexBFS:Labeling of G, v be Vertex of G, x be
  set, k be Nat such that
A1: x in G.AdjacentSet({v}) and
A2: not x in dom L`1;
A3: x in (G.AdjacentSet({v}) \ dom L`1) by A1,A2,XBOOLE_0:def 5;
  then x in dom ((G.AdjacentSet({v}) \ dom L`1) --> {G.order()-'k}) by
FUNCOP_1:13;
  then
A4: x in dom (L`2) \/ dom ((G.AdjacentSet({v})\dom L`1)-->{G.order()-'k}) by
XBOOLE_0:def 3;
  set L2 = LexBFS:Update(L,v,k)`2;
A5: L2 = L`2 .\/ ((G.AdjacentSet({v}) \ dom L`1) --> {G.order()-'k}) by
MCART_1:7;
  ((G.AdjacentSet({v}) \ dom L`1) --> {G.order()-'k}).x = {G.order()-'k}
  by A3,FUNCOP_1:7;
  hence thesis by A5,A4,Def2;
end;

definition
  let G be finite _Graph, L be LexBFS:Labeling of G;
  func LexBFS:Step(L) -> LexBFS:Labeling of G equals
  :Def14:
  L if G.order() <=
card (dom L`1) otherwise LexBFS:Update(L, LexBFS:PickUnnumbered(L), card dom L
  `1);
  coherence;
  consistency;
end;

definition
  let G be _Graph;
  mode LexBFS:LabelingSeq of G -> ManySortedSet of NAT means
    :Def15:
    for n being Nat holds it.n is LexBFS:Labeling of G;
  existence
  proof
    set L = the LexBFS:Labeling of G;
    deffunc F(set) = L;
    consider f being ManySortedSet of NAT such that
A1: for i being set st i in NAT holds f.i = F(i) from PBOOLE:sch 4;
    take f;
    let n be Nat;
    n in NAT by ORDINAL1:def 12;
    hence thesis by A1;
  end;
end;

definition
  let G be _Graph, S be LexBFS:LabelingSeq of G, n be Nat;
  redefine func S.n -> LexBFS:Labeling of G;
  coherence by Def15;
end;

definition
  let G be _Graph, S be LexBFS:LabelingSeq of G;
  redefine func S.Result() -> LexBFS:Labeling of G;
  coherence by Def15;
end;

definition
  let G be finite _Graph, S be LexBFS:LabelingSeq of G;
  func S``1 -> preVNumberingSeq of G means
  :Def16:
  for n being Nat holds it.n = (S.n)`1;
  existence
  proof
    deffunc F(set) = (S.$1)`1;
    consider f being ManySortedSet of NAT such that
A1: for i being set st i in NAT holds f.i = F(i) from PBOOLE:sch 4;
    now
      let i be Nat;
      i in NAT by ORDINAL1:def 12;
      then f.i = (S.i)`1 by A1;
      hence f.i is PartFunc of the_Vertices_of G, NAT;
    end;
    then reconsider f as preVNumberingSeq of G by Def8;
    take f;
    let n be Nat;
    n in NAT by ORDINAL1:def 12;
    hence thesis by A1;
  end;
  uniqueness
  proof
    let it1, it2 be preVNumberingSeq of G such that
A2: for n being Nat holds it1.n = (S.n)`1 and
A3: for n being Nat holds it2.n = (S.n)`1;
    now
      let i be set;
      assume i in NAT;
      then reconsider i9 = i as Nat;
      thus it1.i = (S.i9)`1 by A2
        .= it2.i by A3;
    end;
    hence it1 = it2 by PBOOLE:3;
  end;
end;

definition
  let G be finite _Graph;
  func LexBFS:CSeq(G) -> LexBFS:LabelingSeq of G means
  :Def17:
  it.0 = LexBFS:Init(G) & for n being Nat holds it.(n+1) = LexBFS:Step(it.n);
  existence
  proof
    defpred P[Element of NAT,set,set] means ($2 is LexBFS:Labeling of G
implies ex L being LexBFS:Labeling of G st $2 = L & $3 = LexBFS:Step(L)) & (not
    $2 is LexBFS:Labeling of G implies $3 = $2);
    now
      let n be Element of NAT,x be set;
      now
        per cases;
        suppose
          x is LexBFS:Labeling of G;
          then reconsider L = x as LexBFS:Labeling of G;
          LexBFS:Step(L) = LexBFS:Step(L);
          hence ex y being set st P[n,x,y];
        end;
        suppose
          not x is LexBFS:Labeling of G;
          hence ex y being set st P[n,x,y];
        end;
      end;
      hence ex y being set st P[n,x,y];
    end;
    then
A1: for n being Element of NAT for x being set ex y being set st P[n,x,y];
    consider IT being Function such that
A2: dom IT = NAT & IT.0 = LexBFS:Init(G) & for n being Element of NAT
    holds P[n,IT.n,IT.(n+1)] from RECDEF_1:sch 1(A1);
    reconsider IT as ManySortedSet of NAT by A2,PARTFUN1:def 2,RELAT_1:def 18;
    defpred P2[Nat] means IT.$1 is LexBFS:Labeling of G;
A3: now
      let n be Nat;
      assume
A4:   P2[n];
      n in NAT by ORDINAL1:def 12;
      then ex Gn being LexBFS:Labeling of G st IT.n = Gn & IT.(n+1) =
      LexBFS:Step(Gn) by A2,A4;
      hence P2[n+1];
    end;
A5: P2[ 0 ] by A2;
    for n being Nat holds P2[n] from NAT_1:sch 2(A5,A3);
    then reconsider IT as LexBFS:LabelingSeq of G by Def15;
    take IT;
    thus IT.0 = LexBFS:Init(G) by A2;
    let n be Nat;
    n in NAT by ORDINAL1:def 12;
    then ex Gn being LexBFS:Labeling of G st IT.n = Gn & IT.(n+1) =
    LexBFS:Step(Gn) by A2;
    hence thesis;
  end;
  uniqueness
  proof
    let IT1,IT2 be LexBFS:LabelingSeq of G such that
A6: IT1.0 = LexBFS:Init(G) and
A7: for n being Nat holds IT1.(n+1) = LexBFS:Step(IT1.n) and
A8: IT2.0 = LexBFS:Init(G) and
A9: for n being Nat holds IT2.(n+1) = LexBFS:Step(IT2.n);
    defpred P[Nat] means IT1.$1 = IT2.$1;
    now
      let n be Nat;
      assume P[n];
      then IT1.(n+1) = LexBFS:Step(IT2.n) by A7
        .= IT2.(n+1) by A9;
      hence P[n+1];
    end;
    then
A10: for n being Element of NAT st P[n] holds P[n+1];
A11: P[ 0 ] by A6,A8;
    for n being Element of NAT holds P[n] from NAT_1:sch 1(A11,A10);
    then for n being set st n in NAT holds IT1.n = IT2.n;
    hence IT1 = IT2 by PBOOLE:3;
  end;
end;

theorem Th28:
  for G being finite _Graph holds LexBFS:CSeq(G) is iterative
proof
  let G be finite _Graph;
  set CS = LexBFS:CSeq(G);
  let k,n be Nat such that
A1: CS.k = CS.n;
  CS.(k+1) = LexBFS:Step(CS.k) by Def17;
  hence CS.(k+1) = CS.(n+1) by A1,Def17;
end;

registration
  let G be finite _Graph;
  cluster LexBFS:CSeq(G) -> iterative;
  coherence by Th28;
end;

Lm7: for G being _Graph, v being set holds dom (LexBFS:Init(G))`2 =
the_Vertices_of G & (LexBFS:Init(G))`2.v = {}
proof
  let G be _Graph, v be set;
  set g = the_Vertices_of G --> {};
  set f = g;
  thus dom (LexBFS:Init(G))`2 = the_Vertices_of G by FUNCT_2:def 1;
A1: now
    let x be set;
    per cases;
    suppose
      x in dom f;
      hence f.x = {} by FUNCOP_1:7;
    end;
    suppose
      not x in dom f;
      hence f.x = {} by FUNCT_1:def 2;
    end;
  end;
  (LexBFS:Init(G))`2 = g by MCART_1:7;
  hence thesis by A1;
end;

definition
  let X, Y be set, f be Function of X, Fin Y, x be set;
  redefine func f.x -> finite Subset of Y;
  coherence
  proof
A1: dom f = X by FUNCT_2:def 1;
    per cases;
    suppose
      x in X;
      then f.x in Fin Y by FUNCT_2:5;
      hence thesis by FINSUB_1:def 5;
    end;
    suppose
      not x in X;
      then f.x = {} by A1,FUNCT_1:def 2;
      hence thesis by XBOOLE_1:2;
    end;
  end;
end;

:: the vertex picked has the largest v2label

theorem Th29:
  for G being finite _Graph, L be LexBFS:Labeling of G, x being
set st not x in dom L`1 & dom L`1 <> the_Vertices_of G holds (L`2.x,1)-bag <= (
  L`2.(LexBFS:PickUnnumbered(L)),1)-bag, InvLexOrder NAT
proof
  let G be finite _Graph, L be LexBFS:Labeling of G, x be set such that
A1: not x in dom L`1 and
A2: dom L`1 <> the_Vertices_of G;
  set VG = the_Vertices_of G;
  set V2G = L`2;
  set VLG = L`1;
  set w = LexBFS:PickUnnumbered(L);
  consider S being non empty finite Subset of bool NAT, B being non empty
  finite Subset of Bags NAT, F being Function such that
A3: S = rng F and
A4: F = V2G | (VG \ dom VLG) and
A5: for x being finite Subset of NAT holds x in S implies (x,1)-bag in B and
A6: for x being set holds x in B implies ex y being finite Subset of NAT
  st y in S & x = (y,1)-bag and
A7: w = choose (F " {support max(B,InvLexOrder NAT)}) by A2,Def12;
A8: dom F = dom V2G /\ (VG \ dom VLG) by A4,RELAT_1:61;
  set mw = max(B,InvLexOrder NAT);
  mw in B by Def5;
  then consider y being finite Subset of NAT such that
A9: y in S and
A10: mw = (y,1)-bag by A6;
A11: y = support mw by A10,UPROOTS:8;
  then
A12: F " {support mw} is non empty by A3,A9,FUNCT_1:72;
  then w in dom F by A7,FUNCT_1:def 7;
  then
A13: V2G.w = F.w by A4,FUNCT_1:47;
  F.w in {support mw} by A7,A12,FUNCT_1:def 7;
  then
A14: (V2G.w,1)-bag = mw by A10,A11,A13,TARSKI:def 1;
A15: dom V2G = the_Vertices_of G by FUNCT_2:def 1;
  per cases;
  suppose
    x in the_Vertices_of G;
    then x in VG \ dom VLG by A1,XBOOLE_0:def 5;
    then
A16: x in dom F by A15,A8,XBOOLE_0:def 4;
    then
A17: F.x in S by A3,FUNCT_1:def 3;
    F.x = V2G.x by A4,A16,FUNCT_1:47;
    then (V2G.x,1)-bag in B by A5,A17;
    hence thesis by A14,Def5;
  end;
  suppose
    not x in the_Vertices_of G;
    then V2G.x = {} by A15,FUNCT_1:def 2;
    then (V2G.x,1)-bag = EmptyBag NAT by UPROOTS:9;
    hence thesis by TERMORD:9;
  end;
end;

:: the vertex picked is not currently in the vlabel

theorem Th30:
  for G being finite _Graph, L be LexBFS:Labeling of G st dom L`1
  <> the_Vertices_of G holds not LexBFS:PickUnnumbered(L) in dom L`1
proof
  let G be finite _Graph, L be LexBFS:Labeling of G such that
A1: dom L`1 <> the_Vertices_of G;
  set VG = the_Vertices_of G;
  set V2G = L`2;
  set VLG = L`1;
  set w = LexBFS:PickUnnumbered(L);
  consider S being non empty finite Subset of bool NAT, B being non empty
  finite Subset of Bags NAT, F being Function such that
A2: S = rng F and
A3: F = V2G | (VG \ dom VLG) and
  for x being finite Subset of NAT holds x in S implies (x,1)-bag in B and
A4: for x being set holds x in B implies ex y being finite Subset of NAT
  st y in S & x = (y,1)-bag and
A5: w = choose (F " {support max(B,InvLexOrder NAT)}) by A1,Def12;
  set mw = max(B,InvLexOrder NAT);
  mw in B by Def5;
  then consider y being finite Subset of NAT such that
A6: y in S and
A7: mw = (y,1)-bag by A4;
  y = support mw by A7,UPROOTS:8;
  then F " {support mw} is non empty by A2,A6,FUNCT_1:72;
  then
A8: w in dom F by A5,FUNCT_1:def 7;
  assume w in dom VLG;
  then
A9: not w in VG \ dom VLG by XBOOLE_0:def 5;
  dom F = dom V2G /\ (VG \ dom VLG) by A3,RELAT_1:61;
  hence contradiction by A8,A9,XBOOLE_0:def 4;
end;

theorem Th31:
  for G being finite _Graph, n being Nat st card dom ((LexBFS:CSeq
(G)).n)`1 < G.order() holds ((LexBFS:CSeq(G)).(n+1))`1 = ((LexBFS:CSeq(G)).n)`1
  +* (LexBFS:PickUnnumbered((LexBFS:CSeq(G)).n) .--> (G.order()-'(card (dom ((
  LexBFS:CSeq(G)).n)`1))))
proof
  let G be finite _Graph, n be Nat;
  set CS = LexBFS:CSeq(G);
  assume
A1: card dom ((CS.n)`1) < G.order();
  set CN1 = CS.(n+1);
  set CSN = CS.n;
  set VLN = CSN`1;
  set w = LexBFS:PickUnnumbered(CSN);
  CN1 = LexBFS:Step(CSN) by Def17;
  then CN1 = LexBFS:Update(CSN, w, card (dom VLN)) by A1,Def14;
  hence thesis by MCART_1:7;
end;

theorem Th32:
  for G being finite _Graph, n being Nat st n <= G.order() holds
  card dom ((LexBFS:CSeq(G)).n)`1 = n
proof
  let G be finite _Graph, n be Nat such that
A1: n <= G.order();
  set CS = LexBFS:CSeq(G);
  defpred P[Nat] means $1 <= G.order() implies card dom ((CS.$1)`1) = $1;
A2: for k being Nat st k < G.order() & card dom ((CS.k)`1) = k holds card
  dom ((CS.(k+1))`1) = k+1
  proof
    let k be Nat such that
A3: k < G.order() and
A4: card dom ((CS.k)`1) = k;
    set CK1 = CS.(k+1);
    set CSK = CS.k;
    set VLK = CSK`1;
    set VK1 = CK1`1;
    set w = LexBFS:PickUnnumbered(CSK);
    set wf = w .--> (G.order() -' k);
A5: dom wf = {w} by FUNCOP_1:13;
    VK1 = VLK +* (w .--> (G.order()-'k)) by A3,A4,Th31;
    then dom VK1 = dom VLK \/ {w} by A5,FUNCT_4:def 1;
    hence thesis by A3,A4,Th30,CARD_2:41;
  end;
A6: for k being Nat st P[k] holds P[k+1]
  proof
    let k be Nat such that
A7: P[k];
    per cases;
    suppose
      k < G.order();
      hence thesis by A2,A7;
    end;
    suppose
      k >= G.order();
      hence thesis by NAT_1:13;
    end;
  end;
  CS.0 = LexBFS:Init(G) by Def17;
  then
A8: P[ 0 ] by CARD_1:27,MCART_1:7,RELAT_1:38;
  for k being Nat holds P[k] from NAT_1:sch 2(A8,A6);
  hence thesis by A1;
end;

theorem Th33:
  for G being finite _Graph, n being Nat st G.order() <= n holds (
  LexBFS:CSeq(G)).(G.order()) = (LexBFS:CSeq(G)).n
proof
  let G be finite _Graph, n be Nat;
  assume G.order() <= n;
  then
A1: ex i being Nat st G.order() + i = n by NAT_1:10;
  set CS = LexBFS:CSeq(G);
  defpred V[Nat] means G.order() = card dom (CS.(G.order()+$1))`1;
  defpred P[Nat] means (CS.(G.order())) = (CS.(G.order()+$1));
A2: for k being Nat st V[k] holds V[k+1]
  proof
    let k be Nat such that
A3: V[k];
    set CK1 = CS.(G.order()+k+1);
    set CSK = CS.(G.order()+k);
    CK1 = LexBFS:Step(CSK) by Def17;
    hence thesis by A3,Def14;
  end;
A4: V[ 0 ] by Th32;
A5: for k being Nat holds V[k] from NAT_1:sch 2(A4,A2);
A6: for k being Nat st P[k] holds P[k+1]
  proof
    let k be Nat such that
A7: P[k];
    set CK1 = CS.(G.order()+k+1);
    set CSK = CS.(G.order()+k);
    set VLK = CSK`1;
A8: CK1 = LexBFS:Step(CSK) by Def17;
    card dom VLK = G.order() by A5;
    hence thesis by A7,A8,Def14;
  end;
A9: P[ 0 ];
  for k being Nat holds P[k] from NAT_1:sch 2(A9,A6);
  hence thesis by A1;
end;

theorem Th34:
  for G being finite _Graph, m,n being Nat st G.order() <= m & m
  <= n holds (LexBFS:CSeq(G)).m = (LexBFS:CSeq(G)).n
proof
  let G be finite _Graph, m,n be Nat such that
A1: G.order() <= m and
A2: m <= n;
  (LexBFS:CSeq(G)).m = (LexBFS:CSeq(G)).(G.order()) by A1,Th33;
  hence thesis by A1,A2,Th33,XXREAL_0:2;
end;

theorem Th35:
  for G being finite _Graph holds LexBFS:CSeq(G) is eventually-constant
proof
  let G be finite _Graph;
  take G.order();
  let m be Nat;
  assume G.order() <= m;
  hence (LexBFS:CSeq(G)).(G.order()) = (LexBFS:CSeq(G)).m by Th33;
end;

registration
  let G be finite _Graph;
  cluster LexBFS:CSeq(G) -> eventually-constant;
  coherence by Th35;
end;

theorem Th36:
  for G being finite _Graph, n being Nat holds dom ((LexBFS:CSeq(G
  )).n)`1 = the_Vertices_of(G) iff G.order() <= n
proof
  let G be finite _Graph, n be Nat;
  set CS = LexBFS:CSeq(G);
  set CSN = CS.n;
  set VLN = CSN`1;
  set CSO = CS.G.order();
  set VLO = CSO`1;
  thus not dom VLN = the_Vertices_of G or not n < G.order() by Th32;
  card dom VLO = card the_Vertices_of G by Th32;
  then
A1: dom VLO = the_Vertices_of G by CARD_FIN:1;
  assume G.order() <= n;
  hence thesis by A1,Th34;
end;

theorem Th37:
  for G being finite _Graph holds (LexBFS:CSeq(G)).Lifespan() = G .order()
proof
  let G be finite _Graph;
  set CS = LexBFS:CSeq(G);
A1: for n being Nat st CS.n = CS.(n+1) holds G.order() <= n
  proof
    let n be Nat such that
A2: CS.n = CS.(n+1);
    set w = LexBFS:PickUnnumbered(CS.n);
    set VN1 = (CS.(n+1))`1;
    set VLN = (CS.n)`1;
    set j = card (dom VLN);
    set wf = w .--> (G.order() -' j);
    assume
A3: n < G.order();
    then dom VLN <> the_Vertices_of G by Th36;
    then
A4: not w in dom VLN by Th30;
    j < G.order() by A3,Th32;
    then
A5: VN1 = VLN +* (w .--> (G.order() -' j)) by Th31;
    dom wf = {w} by FUNCOP_1:13;
    then
A6: dom VN1 = dom VLN \/ {w} by A5,FUNCT_4:def 1;
    w in {w} by TARSKI:def 1;
    hence contradiction by A2,A4,A6,XBOOLE_0:def 3;
  end;
  G.order() <= G.order()+1 by NAT_1:13;
  then CS.(G.order()) = CS.(G.order()+1) by Th33;
  hence thesis by A1,GLIB_000:def 55;
end;

theorem Th38:
  for G being finite _Graph holds (LexBFS:CSeq(G))``1 is eventually-constant
proof
  let G be finite _Graph;
  set CS = (LexBFS:CSeq(G));
  set S = (LexBFS:CSeq(G))``1;
  now
    consider n being Nat such that
A1: for m being Nat st n <= m holds CS.n = CS.m by Def7;
    take n;
    let m be Nat such that
A2: n <= m;
    thus S.n = (CS.n)`1 by Def16
      .= (CS.m)`1 by A1,A2
      .= S.m by Def16;
  end;
  hence thesis by Def7;
end;

theorem Th39:
  for G being finite _Graph holds (LexBFS:CSeq(G))``1.Lifespan() =
  (LexBFS:CSeq(G)).Lifespan()
proof
  let G be finite _Graph;
  set S = LexBFS:CSeq(G);
  set VN = S``1;
  set ls = G.order();
A1: VN is eventually-constant by Th38;
A2: (S.(ls+1))`1 = S``1.(ls+1) by Def16;
A3: now
    let n be Nat such that
A4: VN.n = VN.(n+1) and
A5: ls > n;
    n+1 <= ls by A5,NAT_1:13;
    then
A6: card dom (S.(n+1))`1 = n+1 by Th32;
A7: (S.(n+1))`1 = VN.(n+1) by Def16;
A8: (S.n)`1 = VN.n by Def16;
    card dom (S.n)`1 = n by A5,Th32;
    hence contradiction by A4,A6,A8,A7;
  end;
  (S.ls)`1 = S``1.ls by Def16;
  then
A9: VN.ls = VN.(ls+1) by A2,Th33,NAT_1:11;
  S.Lifespan() = ls by Th37;
  hence thesis by A1,A9,A3,GLIB_000:def 55;
end;

registration
  let G be finite _Graph;
  cluster (LexBFS:CSeq(G))``1 -> vertex-numbering;
  correctness
  proof
    set S = (LexBFS:CSeq(G))``1;
    set CS = (LexBFS:CSeq(G));
A1: S.Lifespan() = CS.Lifespan() by Th39;
    thus S.0 = (CS.0)`1 by Def16
      .= (LexBFS:Init(G))`1 by Def17
      .= {} by MCART_1:7;
    now
      let k, n be Nat such that
A2:   S.k = S.n;
A3:   S.(k+1) = (CS.(k+1))`1 by Def16;
A4:   S.k = (CS.k)`1 by Def16;
A5:   S.(n+1) = (CS.(n+1))`1 by Def16;
A6:   S.n = (CS.n)`1 by Def16;
      per cases;
      suppose
A7:     k <= G.order() & n <= G.order();
        then card dom ((CS.n)`1) = n by Th32;
        hence S.(k+1) = S.(n+1) by A2,A4,A6,A7,Th32;
      end;
      suppose
A8:     k <= G.order() & n >= G.order();
        then
A9:     CS.n = CS.(G.order()) by Th33;
A10:    card dom ((CS.(G.order()))`1) = G.order() by Th32;
A11:    n+1 >= G.order() by A8,NAT_1:13;
        card dom ((CS.k)`1) = k by A8,Th32;
        then k+1 >= G.order() by A2,A4,A6,A9,A10,NAT_1:13;
        hence S.(k+1) = (CS.(G.order()))`1 by A3,Th33
          .= S.(n+1) by A5,A11,Th33;
      end;
      suppose
A12:    k >= G.order() & n <= G.order();
        then
A13:    CS.k = CS.(G.order()) by Th33;
A14:    card dom ((CS.(G.order()))`1) = G.order() by Th32;
        card dom ((CS.n)`1) = n by A12,Th32;
        then
A15:    n+1 >= G.order() by A2,A4,A6,A13,A14,NAT_1:13;
        k+1 >= G.order() by A12,NAT_1:13;
        hence S.(k+1) = (CS.(G.order()))`1 by A3,Th33
          .= S.(n+1) by A5,A15,Th33;
      end;
      suppose
A16:    k >= G.order() & n >= G.order();
        then
A17:    n+1 >= G.order() by NAT_1:13;
A18:    k+1 >= G.order() by A16,NAT_1:13;
        thus S.(k+1) = (CS.(k+1))`1 by Def16
          .= (CS.(G.order()))`1 by A18,Th33
          .= (CS.(n+1))`1 by A17,Th33
          .= S.(n+1) by Def16;
      end;
    end;
    hence S is iterative by Def6;
    S is eventually-constant by Th38;
    hence S is halting;
A19: CS.Lifespan() = G.order() by Th37;
    hence S.Lifespan() = G.order() by Th39;
    let n be Nat such that
A20: n < S.Lifespan();
A21: n < G.order() by A19,A20,Th39;
    take w = LexBFS:PickUnnumbered(CS.n);
A22: S.n = (CS.n)`1 by Def16;
A23: card dom ((CS.n)`1) = n by A21,Th32;
    hence not w in dom (S.n) by A21,A22,Th30;
    S.(n+1) = (CS.(n+1))`1 by Def16;
    hence thesis by A1,A19,A20,A22,A23,Th31;
  end;
end;

theorem Th40:
  for G being finite _Graph holds (LexBFS:CSeq(G))``1.Result() = (
  LexBFS:CSeq(G)).Result()`1
proof
  let G be finite _Graph;
  set S = LexBFS:CSeq(G);
  thus S``1.Result() = S``1.(S.Lifespan()) by Th39
    .= S.Result()`1 by Def16;
end;

theorem Th41:
  for G being finite _Graph, n being Nat st n < G.order() holds ((
  LexBFS:CSeq(G))``1).PickedAt(n) = LexBFS:PickUnnumbered((LexBFS:CSeq(G)).n)
proof
  let G be finite _Graph, n be Nat such that
A1: n < G.order();
  set CS = LexBFS:CSeq(G);
  set CSN = CS.n;
  set CS1 = CS.(n+1);
  set VLN = CSN`1;
  set VL1 = CS1`1;
A2: CS.Lifespan() = G.order() by Th37;
  set PU = LexBFS:PickUnnumbered(CSN);
  set f2 = PU .--> (CS.Lifespan()-'n);
A3: dom f2 = {PU} by FUNCOP_1:13;
  n = card dom VLN by A1,Th32;
  then VL1 = VLN +* (PU .--> (CS.Lifespan()-'n)) by A1,A2,Th31;
  then
A4: dom VL1 = dom VLN \/ {PU} by A3,FUNCT_4:def 1;
A5: CSN`1 = CS``1.n by Def16;
  set PA = CS``1.PickedAt(n);
  set f1 = PA .--> (CS.Lifespan()-'n);
A6: dom f1 = {PA} by FUNCOP_1:13;
A7: CS.Lifespan() = CS``1.Lifespan() by Th39;
  CS1`1 = CS``1.(n+1) by Def16;
  then VL1 = VLN +* (PA .--> (CS.Lifespan()-'n)) by A1,A2,A7,A5,Def10;
  then
A8: dom VL1 = dom VLN \/ {PA} by A6,FUNCT_4:def 1;
A9: not PA in dom VLN by A1,A2,A7,A5,Def10;
  now
    assume PA <> PU;
    then not PA in {PU} by TARSKI:def 1;
    then
A10: not PA in dom VL1 by A9,A4,XBOOLE_0:def 3;
    PA in {PA} by TARSKI:def 1;
    hence contradiction by A8,A10,XBOOLE_0:def 3;
  end;
  hence thesis;
end;

theorem Th42:
  for G being finite _Graph, n being Nat st n < G.order() ex w
  being Vertex of G st w = LexBFS:PickUnnumbered((LexBFS:CSeq(G)).n) & for v
being set holds (v in G.AdjacentSet({w}) & not v in dom ((LexBFS:CSeq(G)).n)`1
  implies ((LexBFS:CSeq(G)).(n+1)) `2.v = (((LexBFS:CSeq(G)).n))`2.v \/ {G
.order() -' n}) & ((not v in G.AdjacentSet({w}) or v in dom (((LexBFS:CSeq(G)).
  n))`1) implies ((LexBFS:CSeq(G)).(n+1)) `2.v = (((LexBFS:CSeq(G)).n))`2.v)
proof
  let G be finite _Graph, n be Nat such that
A1: n < G.order();
  set CS = (LexBFS:CSeq(G));
  set CSN = CS.n;
  set VLN = CSN`1;
  set V2N = CSN`2;
  set CN1 = CS.(n+1);
  set V21 = CN1`2;
  set w = LexBFS:PickUnnumbered(CSN);
  take w;
A2: CN1 = LexBFS:Step(CSN) by Def17;
  card dom VLN = n by A1,Th32;
  then
A3: CN1 = LexBFS:Update(CSN, w, n) by A1,A2,Def14;
  now
    let v be set;
    assume
A4: not v in G.AdjacentSet({w}) or v in dom VLN;
    per cases by A4;
    suppose
      not v in G.AdjacentSet({w});
      hence V21.v = V2N.v by A3,Th25;
    end;
    suppose
      v in dom VLN;
      hence V21.v = V2N.v by A3,Th26;
    end;
  end;
  hence thesis by A3,Th27;
end;

theorem Th43:
  for G being finite _Graph, i being Nat, v being set holds ((
  LexBFS:CSeq(G)).i)`2.v c= (Seg G.order()) \ Seg (G.order()-'i)
proof
  let G be finite _Graph, i be Nat, v be set;
  set CS = (LexBFS:CSeq(G));
  set CSI = CS.i;
  set V2I = CSI`2;
  set CSO = CS.(G.order());
  set V2O = CSO`2;
  defpred P[Nat] means $1 <= G.order() implies (((LexBFS:CSeq(G)).$1)`2).v c=
  (Seg G.order()) \ Seg (G.order() -' $1);
A1: for k being Nat st P[k] holds P[k+1]
  proof
    let k be Nat such that
A2: P[k];
    set CK1 = CS.(k+1);
    set CSK = CS.k;
    set V2K = CSK`2;
    set VLK = CSK`1;
    set V21 = CK1`2;
    per cases;
    suppose
      k+1 <= G.order();
      then
A3:   k < G.order() by NAT_1:13;
      then consider w being Vertex of G such that
      w = LexBFS:PickUnnumbered(CSK) and
A4:   for v being set holds (v in G.AdjacentSet({w}) & not v in dom
VLK implies V21.v = V2K.v \/ {G.order() -' k}) & (not v in G.AdjacentSet({w})
      or v in dom VLK implies V21.v = V2K.v) by Th42;
      per cases;
      suppose
A5:     v in G.AdjacentSet({w}) & not v in dom VLK;
A6:     ((Seg G.order()) \ Seg (G.order() -' k)) \/ {G.order() -' k} = (
        Seg G.order()) \ Seg (G.order() -' (k+1)) by A3,Th5;
        V21.v = V2K.v \/ {G.order() -' k} by A4,A5;
        hence thesis by A2,A6,NAT_1:13,XBOOLE_1:9;
      end;
      suppose
A7:     not v in G.AdjacentSet({w}) or v in dom VLK;
        k <= k+1 by NAT_1:13;
        then
A8:     (Seg G.order()) \ Seg (G.order() -' k) c= (Seg G.order()) \ Seg (
        G.order() -' (k+1)) by Th4;
        V21.v = V2K.v by A4,A7;
        hence thesis by A2,A8,NAT_1:13,XBOOLE_1:1;
      end;
    end;
    suppose
      G.order() < k+1;
      hence thesis;
    end;
  end;
  CS.0 = LexBFS:Init(G) by Def17;
  then (CS.0)`2.v = {} by Lm7;
  then
A9: P[ 0 ] by XBOOLE_1:2;
A10: for k being Nat holds P[k] from NAT_1:sch 2(A9,A1);
  per cases;
  suppose
    i <= G.order();
    hence thesis by A10;
  end;
  suppose
A11: i > G.order();
    then G.order() - i < i - i by XREAL_1:9;
    then G.order() -' i = 0 by XREAL_0:def 2;
    then
A12: G.order() -' G.order() = G.order() -' i by XREAL_1:232;
    V2O = V2I by A11,Th34;
    hence thesis by A10,A12;
  end;
end;

theorem Th44:
  for G being finite _Graph, x being set, i,j being Nat st i <= j
  holds ((LexBFS:CSeq(G)).i)`2.x c= ((LexBFS:CSeq(G)).j)`2.x
proof
  let G be finite _Graph, x be set, i,j be Nat;
  assume i <= j;
  then
A1: ex k being Nat st j = i+k by NAT_1:10;
  set CS = (LexBFS:CSeq(G));
  set CSI = CS.i, V2I = CSI`2;
  defpred P[Nat] means V2I.x c= (CS.(i+$1))`2.x;
A2: for k being Nat st P[k] holds P[k+1]
  proof
    let k be Nat such that
A3: P[k];
    set CK1 = CS.(i+k+1);
    set CSK = CS.(i+k);
    set V2K = CSK`2;
    set VLK = CSK`1;
    set V21 = CK1`2;
    per cases;
    suppose
      i+k+1 <= G.order();
      then i+k < G.order() by NAT_1:13;
      then consider w being Vertex of G such that
      w = LexBFS:PickUnnumbered(CSK) and
A4:   for v being set holds (v in G.AdjacentSet({w}) & not v in dom
VLK implies V21.v = V2K.v \/ {G.order() -' (i+k)}) & (not v in G.AdjacentSet({w
      }) or v in dom VLK implies V21.v = V2K.v) by Th42;
      per cases;
      suppose
        x in G.AdjacentSet({w}) & not x in dom VLK;
        then V21.x = V2K.x \/ {G.order() -' (i+k)} by A4;
        then V2K.x c= V21.x by XBOOLE_1:7;
        hence thesis by A3,XBOOLE_1:1;
      end;
      suppose
        not x in G.AdjacentSet({w}) or x in dom VLK;
        hence thesis by A3,A4;
      end;
    end;
    suppose
A5:   G.order() < i+k+1;
A6:   i+k <= i+k+1 by NAT_1:13;
      G.order() <= i+k by A5,NAT_1:13;
      hence thesis by A3,A6,Th34;
    end;
  end;
A7: P[ 0 ];
  for k being Nat holds P[k] from NAT_1:sch 2(A7,A2);
  hence thesis by A1;
end;

theorem Th45:
  for G being finite _Graph, m,n being Nat, x, y being set st n <
  G.order() & n < m & y = LexBFS:PickUnnumbered((LexBFS:CSeq(G)).n) & not x in
dom ((LexBFS:CSeq(G)).n)`1 & x in G.AdjacentSet({y}) holds (G.order() -' n) in
  ((LexBFS:CSeq(G)).m)`2.x
proof
  let G be finite _Graph;
  let m,n be Nat, x, y be set such that
A1: n < G.order() and
A2: n < m;
  set CS = (LexBFS:CSeq(G));
  set CSM = CS.m, V2M = CSM`2;
  set CN1 = CS.(n+1);
  set V21 = CN1`2;
  n+1 <= m by A2,NAT_1:13;
  then
A3: V21.x c= V2M.x by Th44;
A4: G.order() -' n in {G.order() -' n} by TARSKI:def 1;
  set CSN = CS.n, VLN = CSN`1, V2N = CSN`2;
  assume that
A5: y = LexBFS:PickUnnumbered(CSN) and
A6: not x in dom VLN and
A7: x in G.AdjacentSet({y});
  ex w being Vertex of G st w = LexBFS:PickUnnumbered(CSN) & for v
being set holds (v in G.AdjacentSet({w}) & not v in dom VLN implies V21.v = V2N
.v \/ {G.order() -' n}) & (not v in G.AdjacentSet({w}) or v in dom VLN implies
  V21.v = V2N.v) by A1,Th42;
  then V21.x = V2N.x \/ {G.order() -' n} by A5,A6,A7;
  then G.order() -' n in V21.x by A4,XBOOLE_0:def 3;
  hence thesis by A3;
end;

theorem Th46:
  for G being finite _Graph, m,n being Nat st m < n for x being
set st not G.order()-'m in ((LexBFS:CSeq(G)).(m+1))`2.x holds not G.order()-'m
  in ((LexBFS:CSeq(G)).n)`2.x
proof
  let G be finite _Graph, m,n be Nat;
  assume m < n;
  then m+1 <= n by NAT_1:13;
  then
A1: ex j being Nat st m+1+j = n by NAT_1:10;
  set CS = LexBFS:CSeq(G);
  set CSM = CS.(m+1);
  set V2M = CSM`2;
  let x be set such that
A2: not G.order() -' m in V2M.x;
  defpred P[Nat] means not G.order() -' m in (((LexBFS:CSeq(G)).(m+1+$1))`2).x;
A3: for k being Nat st P[k] holds P[k+1]
  proof
    let k be Nat such that
A4: P[k];
    set CSK = CS.(m+1+k);
    set VLK = CSK`1, V2K = CSK`2, CK1 = CS.(m+1+k+1);
    set V21 = CK1`2;
    now
      per cases;
      suppose
A5:     m+1+k < G.order();
        then consider w being Vertex of G such that
        w = LexBFS:PickUnnumbered(CSK) and
A6:     for v being set holds ( v in G.AdjacentSet({w}) & not v in dom
VLK implies V21.v = V2K.v \/ {G.order() -' (m+1+k)}) & ((not v in G.AdjacentSet
        ({w}) or v in dom VLK) implies V21.v = V2K.v) by Th42;
        per cases;
        suppose
A7:       x in G.AdjacentSet({w}) & not x in dom VLK;
          m+1 <= m+1+k by NAT_1:11;
          then m < m+1+k by XREAL_1:39;
          then G.order() -' m > G.order() -' (m+1+k) by A5,Th2;
          then
A8:       not G.order() -' m in {G.order() -' (m+1+k)} by TARSKI:def 1;
          V21.x = V2K.x \/ {G.order() -' (m+1+k)} by A6,A7;
          hence not G.order() -' m in V21.x by A4,A8,XBOOLE_0:def 3;
        end;
        suppose
          not x in G.AdjacentSet({w}) or x in dom VLK;
          hence not G.order() -' m in V21.x by A4,A6;
        end;
      end;
      suppose
A9:     G.order() <= m+1+k;
        m+1+k <= m+1+k+1 by NAT_1:13;
        hence not G.order() -' m in V21.x by A4,A9,Th34;
      end;
    end;
    hence thesis;
  end;
A10: P[ 0 ] by A2;
  for k being Nat holds P[k] from NAT_1:sch 2(A10,A3);
  hence thesis by A1;
end;

:: More general version of the above:
:: if the value added during step k doesn't appear in a later step (n),
:: then that value cannot appear in an even later step (m)

theorem Th47:
  for G being finite _Graph, m,n,k being Nat st k < n & n <= m for
x being set st not G.order()-'k in ((LexBFS:CSeq(G)).n)`2.x holds not G.order()
  -'k in ((LexBFS:CSeq(G)).m)`2.x
proof
  let G be finite _Graph, m,n,k be Nat such that
A1: k < n and
A2: n <= m;
  set CS = LexBFS:CSeq(G);
  set CSN = CS.n;
  set V2N = CSN`2;
  let x be set such that
A3: not G.order() -' k in V2N.x;
  set CK1 = CS.(k+1), V21 = CK1`2;
  k+1 <= n by A1,NAT_1:13;
  then V21.x c= V2N.x by Th44;
  then
A4: not G.order() -' k in V21.x by A3;
  k < m by A1,A2,XXREAL_0:2;
  hence thesis by A4,Th46;
end;

:: relates a value in a vertex's v2label to the vertex chosen at that time

theorem Th48:
  for G being finite _Graph, m,n being Nat, x being Vertex of G st
n in ((LexBFS:CSeq(G)).m)`2.x ex y being Vertex of G st (LexBFS:PickUnnumbered(
  (LexBFS:CSeq(G)).(G.order()-'n))) = y & not y in dom ((LexBFS:CSeq(G)).(G
  .order()-'n))`1 & x in G.AdjacentSet({y})
proof
  let G be finite _Graph, m, n be Nat;
  set CS = LexBFS:CSeq(G);
  set CSM = CS.m;
  set V2M = CSM`2;
  set CSN = CS.(G.order() -' n);
  set VLN = CSN`1;
  set V2N = CSN`2;
  set on1 = G.order() -' n + 1;
  set CN1 = CS.on1;
  set V21 = CN1`2;
  let x be Vertex of G such that
A1: n in V2M.x;
A2: V2M.x c= (Seg G.order()) \ Seg (G.order() -' m) by Th43;
  then
A3: G.order() -' m < n by A1,Th3;
  n <= G.order() by A1,A2,Th3;
  then
A4: G.order() -' n = G.order() - n by XREAL_1:233;
  then
A5: G.order() -' n < G.order() by A3,XREAL_1:44;
  then
A6: G.order() -' (G.order() -' n) = G.order() - (G.order() - n) by A4,
XREAL_1:233;
  then consider w being Vertex of G such that
A7: w = LexBFS:PickUnnumbered(CSN) and
A8: for v being set holds (v in G.AdjacentSet({w}) & not v in dom VLN
  implies V21.v = V2N.v\/{n}) & (not v in G.AdjacentSet({w}) or v in dom VLN
  implies V21.v = V2N.v) by A3,A4,Th42,XREAL_1:44;
  V2N.x c= (Seg G.order()) \ Seg (G.order() -' (G.order() -' n)) by Th43;
  then
A9: not n in V2N.x by A6,Th3;
A10: now
    per cases;
    suppose
      m <= G.order();
      then G.order() -' m = G.order() - m by XREAL_1:233;
      then G.order() - m + m < n + m by A3,XREAL_1:6;
      then G.order() - n < m + n - n by XREAL_1:9;
      hence on1 <= m by A4,NAT_1:13;
    end;
    suppose
      G.order() < m;
      then G.order() -' n < m by A5,XXREAL_0:2;
      hence on1 <= m by NAT_1:13;
    end;
  end;
A11: G.order() -' n < on1 by XREAL_1:39;
  assume
A12: not ex y being Vertex of G st LexBFS:PickUnnumbered(CSN) = y & not y
  in dom VLN & x in G.AdjacentSet({y});
  dom VLN <> the_Vertices_of G by A5,Th36;
  then not x in G.AdjacentSet({w}) by A12,A7,Th30;
  then not n in V21.x by A9,A8;
  hence contradiction by A1,A6,A10,A11,Th47;
end;

theorem Th49:
  for G being finite _Graph holds dom ((LexBFS:CSeq(G)).Result())
  `1 = the_Vertices_of G
proof
  let G be finite _Graph;
  set CS = LexBFS:CSeq(G);
  set CSO = CS.(G.order());
  CS.Result() = CSO by Th37;
  hence thesis by Th36;
end;

::$N Lexicographic_breadth-first_search
theorem Th50:
  for G being finite _Graph holds ((LexBFS:CSeq(G)).Result()`1)"
  is VertexScheme of G
proof
  let G be finite _Graph;
  set CS = LexBFS:CSeq(G);
  set CSO = CS.(G.order());
  set VLO = CSO`1;
  set VL = CS``1;
A1: CSO = (LexBFS:CSeq(G)).Result() by Th37;
A2: CS.Lifespan() = G.order() by Th37;
A3: VLO = VL.(G.order()) by Def16;
  then
A4: VLO is one-to-one by Th18;
  dom VLO = the_Vertices_of G by Th36;
  then
A5: rng (VLO") = the_Vertices_of G by A4,FUNCT_1:33;
  CS.Lifespan() = VL.Lifespan() by Th39;
  then
  rng (VL.(G.order())) = (Seg G.order()) \ Seg (G.order() -' G.order()) by A2
,Th14
    .= (Seg G.order()) \ Seg 0 by XREAL_1:232
    .= Seg G.order();
  then dom (VLO") = Seg G.order() by A3,A4,FUNCT_1:33;
  then VLO" is FinSequence by FINSEQ_1:def 2;
  then VLO" is FinSequence of the_Vertices_of G by A5,FINSEQ_1:def 4;
  hence thesis by A1,A4,A5,CHORD:def 12;
end;

:: A vertex with a vlabel of k must have had the largest v2label when chosen

theorem Th51:
  for G being finite _Graph, i,j being Nat, a,b being Vertex of G
  st a in dom ((LexBFS:CSeq(G)).i)`1 & b in dom ((LexBFS:CSeq(G)).i)`1 & ((
  LexBFS:CSeq(G)).i)`1.a < ((LexBFS:CSeq(G)).i)`1.b & j = G.order() -' ((
  LexBFS:CSeq(G)).i)`1.b holds (((LexBFS:CSeq(G)).j)`2.a,1)-bag <= ((((
  LexBFS:CSeq(G)).j)`2).b,1)-bag, InvLexOrder NAT
proof
  let G be finite _Graph;
  let i,j be Nat, a,b be Vertex of G such that
A1: a in dom ((LexBFS:CSeq(G)).i)`1 and
A2: b in dom ((LexBFS:CSeq(G)).i)`1 and
A3: ((LexBFS:CSeq(G)).i)`1.a < ((LexBFS:CSeq(G)).i)`1.b and
A4: j = G.order() -' ((LexBFS:CSeq(G)).i)`1.b;
  set VL = (LexBFS:CSeq(G))``1;
  set CSJ = (LexBFS:CSeq(G)).j;
  set VLI = VL.i, VLJ = VL.j;
A5: ((LexBFS:CSeq(G)).i)`1.b = ((LexBFS:CSeq(G))``1.i).b by Def16;
A6: a in the_Vertices_of G;
A7: ((LexBFS:CSeq(G)).i)`1 = ((LexBFS:CSeq(G))``1.i) by Def16;
A8: (LexBFS:CSeq(G)).Lifespan() = VL.Lifespan() by Th39;
A9: G.order() = (LexBFS:CSeq(G)).Lifespan() by Th37;
  then VLI.b <= G.order() by A8,Th15;
  then
A10: G.order() -' VLI.b = G.order() - VLI.b by XREAL_1:233;
  then
A11: G.order() -' j = G.order() - (G.order() - VLI.b) by A4,A5,NAT_D:35
,XREAL_1:233;
A12: now
    assume a in dom (CSJ`1);
    then
A13: a in dom VLJ by Def16;
    then VLI.b < VLJ.a by A9,A8,A11,Th22;
    hence contradiction by A1,A3,A7,A13,Th19;
  end;
  VL.PickedAt(j) = b by A2,A4,A7,A9,A8,Th20;
  then LexBFS:PickUnnumbered(CSJ) = b by A3,A4,A5,A10,Th41,XREAL_1:44;
  hence thesis by A6,A12,Th29;
end;

:: Any value in our v2label corresponds to a vertex that we are
:: adjacent to in our in our vlabel

theorem Th52:
  for G being finite _Graph, i,j being Nat,v being Vertex of G st
j in ((LexBFS:CSeq(G)).i)`2.v ex w being Vertex of G st w in dom ((LexBFS:CSeq(
  G)).i)`1 & (((LexBFS:CSeq(G)).i)`1).w = j & v in G.AdjacentSet{w}
proof
  let G be finite _Graph, i,j be Nat;
  let v be Vertex of G;
  set CSI = (LexBFS:CSeq(G)).i;
  set VLI = (LexBFS:CSeq(G))``1.i;
  set V2I = CSI`2;
  set n = G.order() -' j;
  set CSN = (LexBFS:CSeq(G)).n;
  set VLN = CSN`1;
A1: G.order() = (LexBFS:CSeq(G)).Lifespan() by Th37;
A2: (LexBFS:CSeq(G)).Lifespan() = (LexBFS:CSeq(G)``1).Lifespan() by Th39;
  assume
A3: j in V2I.v;
  then consider w being Vertex of G such that
A4: LexBFS:PickUnnumbered(CSN) = w and
  not w in dom VLN and
A5: v in G.AdjacentSet({w}) by Th48;
A6: V2I.v c= Seg G.order() \ Seg (G.order() -' i) by Th43;
  then
A7: G.order() -' i < j by A3,Th3;
A8: j <= G.order() by A3,A6,Th3;
  then
A9: G.order() -' j = G.order() - j by XREAL_1:233;
  then
A10: n < G.order() by A7,XREAL_1:44;
A11: G.order() - n = G.order() - (G.order() - j) by A8,XREAL_1:233;
  then G.order() - i < G.order() - n by A7,XREAL_0:def 2;
  then G.order() - i + i < G.order() - n + i by XREAL_1:6;
  then G.order() + n < G.order() + i - n + n by XREAL_1:6;
  then
A12: n + G.order() - G.order() < i + G.order() - G.order() by XREAL_1:9;
A13: w = ((LexBFS:CSeq(G))``1).PickedAt(n) by A4,A7,A9,Th41,XREAL_1:44;
  then
A14: VLI.w = G.order()-'n by A10,A1,A2,A12,Th21;
A15: CSI`1 = VLI by Def16;
  then w in dom CSI`1 by A10,A1,A2,A13,A12,Th21;
  hence thesis by A15,A5,A10,A11,A14,XREAL_1:233;
end;

definition
  let G be _Graph, F be PartFunc of the_Vertices_of G, NAT;
  attr F is with_property_L3 means
  :Def18:
  for a,b,c being Vertex of G st a in
  dom F & b in dom F & c in dom F & F.a < F.b & F.b < F.c & a,c are_adjacent &
  not b,c are_adjacent ex d being Vertex of G st d in dom F & F.c < F.d & b,d
  are_adjacent & not a,d are_adjacent & for e being Vertex of G st e <> d & e,b
  are_adjacent & not e,a are_adjacent holds F.e < F.d;
end;

theorem Th53:
  for G being finite _Graph, n being Nat holds ((LexBFS:CSeq(G)).n
  )`1 is with_property_L3
proof
  let G be finite _Graph, i be Nat;
  set CSi = (LexBFS:CSeq(G)).i;
  set VLi = (LexBFS:CSeq(G))``1.i;
A1: CSi`1 = VLi by Def16;
  now
A2: (LexBFS:CSeq(G)).Lifespan() = (LexBFS:CSeq(G))``1.Lifespan() by Th39;
A3: (LexBFS:CSeq(G)).Lifespan() = G.order() by Th37;
    let a, b, c be Vertex of G such that
A4: a in dom VLi and
A5: b in dom VLi and
A6: c in dom VLi and
A7: VLi.a < VLi.b and
A8: VLi.b < VLi.c and
A9: a,c are_adjacent and
A10: not b,c are_adjacent;
    defpred P[Nat] means ex v being Vertex of G st v in dom VLi & b,v
    are_adjacent & not a,v are_adjacent & VLi.c < VLi.v & VLi.v = $1;
A11: VLi.a < VLi.c by A7,A8,XXREAL_0:2;
    now
      set kc = G.order() -' VLi.c;
      set k = G.order() -' VLi.b;
      assume
A12:  for d being Vertex of G st d in dom VLi & VLi.c < VLi.d & d,b
      are_adjacent holds d,a are_adjacent;
      set VLc = (LexBFS:CSeq(G))``1.kc;
      set CSc = (LexBFS:CSeq(G)).kc;
      set VLb = (LexBFS:CSeq(G))``1.k;
      set CSb = (LexBFS:CSeq(G)).k;
      reconsider sb = CSb`2.b, sa = CSb`2.a as finite Subset of NAT;
A13:  (Seg G.order()) \ Seg (G.order() -' k) c= Seg G.order() by XBOOLE_1:36;
      sb c= (Seg G.order()) \ Seg (G.order() -' k) by Th43;
      then
A14:  sb c= Seg G.order() by A13,XBOOLE_1:1;
A15:  CSc`1 = VLc by Def16;
      sa c= (Seg G.order()) \ Seg (G.order() -' k) by Th43;
      then
A16:  sa c= Seg G.order() by A13,XBOOLE_1:1;
A17:  c in dom VLb by A5,A6,A8,A3,A2,Th23;
A18:  VLi.c <= G.order() by A3,A2,Th15;
      then
A19:  G.order() -' VLi.c = G.order() - VLi.c by XREAL_1:233;
      then
A20:  kc < G.order() by A8,XREAL_1:44;
      then
A21:  G.order() -' kc = G.order() - (G.order() - VLi.c) by A19,XREAL_1:233;
A22:  now
A23:    rng VLc=(Seg G.order()) \ Seg (G.order()-'kc) by A3,A2,Th14;
A24:    VLi.a < VLi.c by A7,A8,XXREAL_0:2;
        assume
A25:    a in dom VLc;
        then VLc.a in rng VLc by FUNCT_1:def 3;
        then VLi.c < VLc.a by A21,A23,Th3;
        hence contradiction by A4,A25,A24,Th19;
      end;
      (LexBFS:CSeq(G))``1.PickedAt(kc) = c by A6,A3,A2,Th20;
      then
A26:  c = LexBFS:PickUnnumbered(CSc) by A8,A19,Th41,XREAL_1:44;
A27:  kc < k by A8,A18,Th2;
      set j = VLb.c;
A28:  CSb`1 = VLb by Def16;
      a in G.AdjacentSet({c}) by A7,A8,A9,CHORD:52;
      then VLi.c in sa by A15,A20,A27,A26,A21,A22,Th45;
      then
A29:  VLb.c in sa by A6,A17,Th19;
A30:  not b in G.AdjacentSet({c}) by A10,CHORD:52;
A31:  now
        assume VLb.c in sb;
        then
A32:    ex z being Vertex of G st z in dom VLb & VLb.z = VLb.c & b in
        G.AdjacentSet({z}) by A28,Th52;
        VLb is one-to-one by Th18;
        hence contradiction by A30,A17,A32,FUNCT_1:def 4;
      end;
      then (sb,1)-bag.j = 0 by UPROOTS:6;
      then
A33:  (sb,1)-bag.j < (sa,1)-bag.j by A29,UPROOTS:7;
      [(sb,1)-bag,(sa,1)-bag] in InvLexOrder NAT
      proof
        per cases;
        suppose
          for k being Ordinal st j in k & k in NAT holds (sb,1)-bag.k
          = (sa,1)-bag.k;
          hence thesis by A33,BAGORDER:def 6;
        end;
        suppose
A34:      not for k being Ordinal st j in k & k in NAT holds (sb,1)
          -bag.k = (sa,1)-bag.k;
          defpred M[Nat] means j in $1 & (sb,1)-bag.$1 <> (sa,1)-bag.$1;
A35:      for k being Nat st M[k] holds k <= G.order()
          proof
            let k be Nat such that
A36:        M[k];
A37:        (sa,1)-bag.k = 1 or (sa,1)-bag.k = 0 by UPROOTS:6,7;
            k in NAT by ORDINAL1:def 12;
            then consider ok being Ordinal such that
A38:        ok = k and
            j in ok and
            ok in NAT and
A39:        (sb,1)-bag.ok <> (sa,1)-bag.ok by A36;
            per cases;
            suppose
              not ok in sb;
              then ok in sa by A38,A39,A37,UPROOTS:6;
              hence thesis by A16,A38,FINSEQ_1:1;
            end;
            suppose
              ok in sb;
              hence thesis by A14,A38,FINSEQ_1:1;
            end;
          end;
A40:      ex k being Nat st M[k] by A34;
          consider mm being Nat such that
A41:      M[mm] and
A42:      for i being Nat st M[i] holds i <= mm from NAT_1:sch 6(A35,
          A40 );
          reconsider mm as Element of NAT by ORDINAL1:def 12;
A43:      now
            let k be Ordinal such that
A44:        mm in k and
A45:        k in NAT;
            reconsider kk = k as Element of NAT by A45;
            mm in {y where y is Element of NAT : y < kk} by A44,AXIOMS:4;
            then
A46:        ex mmy being Element of NAT st mmy = mm & mmy < kk;
            assume (sb,1)-bag.k <> (sa,1)-bag.k;
            hence contradiction by A41,A42,A44,A46,ORDINAL1:10;
          end;
          j in {y where y is Element of NAT : y < mm} by A41,AXIOMS:4;
          then
A47:      ex jy being Element of NAT st jy = j & jy < mm;
A48:      now
            assume
A49:        (sb,1)-bag.mm = 1;
            then mm in sb by UPROOTS:6;
            then consider z being Vertex of G such that
A50:        z in dom (CSb`1) and
A51:        (CSb`1).z = mm and
A52:        b in G.AdjacentSet({z}) by Th52;
            set kc = G.order() -' VLi.z;
A53:        VLi.z <= G.order() by A3,A2,Th15;
            then
A54:        G.order() -' VLi.z = G.order() - VLi.z by XREAL_1:233;
            k < i by A5,A3,A2,Th22;
            then
A55:        CSb`1 c= CSi`1 by A1,A28,Th17;
            then
A56:        dom (CSb`1) c= dom (CSi`1) by RELAT_1:11;
            then
A57:        0 < VLi.z by A1,A50,Th15;
            then
A58:        kc < G.order() by A54,XREAL_1:44;
            then
A59:        G.order() -' kc = G.order() - (G.order() - VLi.z) by A54,
XREAL_1:233;
            set VLc = (LexBFS:CSeq(G))``1.kc;
            set CSc = (LexBFS:CSeq(G)).kc;
            z = (LexBFS:CSeq(G))``1.PickedAt(kc) by A1,A3,A2,A50,A56,Th20;
            then
A60:        z = LexBFS:PickUnnumbered(CSc) by A57,A54,Th41,XREAL_1:44;
A61:        [z,mm] in CSb`1 by A50,A51,FUNCT_1:def 2;
            then
A62:        VLi.z = mm by A1,A50,A55,A56,FUNCT_1:def 2;
A63:        [c,j] in CSb`1 by A28,A17,FUNCT_1:def 2;
            then
A64:        VLi.c = j by A1,A6,A55,FUNCT_1:def 2;
            then VLi.b < VLi.z by A8,A47,A62,XXREAL_0:2;
            then
A65:        kc < k by A53,Th2;
A66:        VLi.c < VLi.z by A1,A47,A50,A55,A56,A61,A64,FUNCT_1:def 2;
A67:        now
              VLi.a < VLi.c by A7,A8,XXREAL_0:2;
              then
A68:          VLi.a < VLi.z by A66,XXREAL_0:2;
A69:          rng VLc = (Seg G.order())\ Seg (G.order()-'kc) by A3,A2,Th14;
              assume
A70:          a in dom VLc;
              then VLc.a in rng VLc by FUNCT_1:def 3;
              then VLi.z < VLc.a by A59,A69,Th3;
              hence contradiction by A4,A70,A68,Th19;
            end;
A71:        VLi.c < VLi.z by A1,A6,A47,A55,A62,A63,FUNCT_1:def 2;
            b,z are_adjacent by A52,CHORD:52;
            then z,a are_adjacent by A1,A12,A47,A50,A56,A62,A64;
            then
A72:        a in G.AdjacentSet({z}) by A11,A71,CHORD:52;
            CSc`1 = VLc by Def16;
            then (G.order() -' kc) in (CSb`2).a by A72,A58,A65,A60,A67,Th45;
            hence contradiction by A41,A49,A62,A59,UPROOTS:7;
          end;
          (sb,1)-bag.mm = 0 or (sb,1)-bag.mm = 1 by UPROOTS:6,7;
          hence thesis by A41,A48,A43,BAGORDER:def 6;
        end;
      end;
      then
A73:  (sb,1)-bag <= (sa,1)-bag, InvLexOrder NAT by TERMORD:def 2;
      (sb,1)-bag <> (sa,1)-bag by A29,A31,Th6;
      then
A74:  (sb,1)-bag < (sa,1)-bag, InvLexOrder NAT by A73,TERMORD:def 3;
      (sa,1)-bag <= (sb,1)-bag, InvLexOrder NAT by A1,A4,A5,A7,Th51;
      hence contradiction by A74,TERMORD:5;
    end;
    then
A75: ex k being Nat st P[k];
A76: for k being Nat st P[k] holds k <= G.order()
    proof
      let k be Nat;
      assume P[k];
      then k in rng VLi by FUNCT_1:def 3;
      then
A77:  k in (Seg G.order()) \ Seg (G.order()-'i) by A3,A2,Th14;
      (Seg G.order()) \ Seg (G.order()-'i) c= Seg G.order() by XBOOLE_1:36;
      hence thesis by A77,FINSEQ_1:1;
    end;
    ex k being Nat st P[k] & for n being Nat st P[n] holds n <= k from
    NAT_1:sch 6(A76,A75);
    then consider k being Nat such that
A78: P[k] and
A79: for n being Nat st P[n] holds n <= k;
    consider v being Vertex of G such that
A80: v in dom VLi and
A81: b,v are_adjacent and
A82: not a,v are_adjacent and
A83: VLi.c < VLi.v and
A84: VLi.v = k by A78;
    for d being Vertex of G st d <> v & d,b are_adjacent & not d,a
    are_adjacent holds VLi.d < VLi.v
    proof
      let d be Vertex of G such that
A85:  d <> v and
A86:  d,b are_adjacent and
A87:  not d,a are_adjacent;
      per cases;
      suppose
        VLi.d <= VLi.c;
        hence thesis by A83,XXREAL_0:2;
      end;
      suppose
A88:    VLi.c < VLi.d;
        then
A89:    d in dom VLi by FUNCT_1:def 2;
        VLi is one-to-one by Th18;
        then
A90:    VLi.d <> VLi.v by A80,A85,A89,FUNCT_1:def 4;
        VLi.d <= k by A79,A86,A87,A88,A89;
        hence thesis by A84,A90,XXREAL_0:1;
      end;
    end;
    hence ex d being Vertex of G st d in dom VLi & VLi.c < VLi.d & b,d
are_adjacent & not a,d are_adjacent & for e being Vertex of G st e <> d & e,b
    are_adjacent & not e,a are_adjacent holds VLi.e < VLi.d by A80,A81,A82,A83;
  end;
  hence thesis by A1,Def18;
end;

theorem Th54: :: Theorem 4.3, Golumbic p. 86
  for G being finite chordal _Graph, L be PartFunc of
the_Vertices_of G, NAT st L is with_property_L3 & dom L = the_Vertices_of G for
  V being VertexScheme of G st V" = L holds V is perfect
proof
  let G be finite chordal _Graph, L be PartFunc of the_Vertices_of G, NAT such
  that
A1: L is with_property_L3 and
A2: dom L = the_Vertices_of G;
  let V be VertexScheme of G such that
A3: V" = L;
A4: V is one-to-one by CHORD:def 12;
A5: for x,y being Vertex of G, i,j being Nat st i in dom V & j in dom V & V
  /.i = x & V/.j = y holds i < j iff L.x < L.y
  proof
    let x,y being Vertex of G;
    let i,j be Nat such that
A6: i in dom V and
A7: j in dom V and
A8: V/.i = x and
A9: V/.j = y;
    V.j = y by A7,A9,PARTFUN1:def 6;
    then
A10: L.y = j by A3,A4,A7,FUNCT_1:34;
A11: V.i = x by A6,A8,PARTFUN1:def 6;
    hence i<j implies L.x < L.y by A3,A4,A6,A10,FUNCT_1:34;
    thus thesis by A3,A4,A6,A11,A10,FUNCT_1:34;
  end;
  defpred R[Nat] means ex P being Walk of G, v1,v2,v3,v4 being Vertex of G st
P is Path-like & P is open & P is chordless & P.length() = $1-1 & v1 = P.(len P
-2) & v2 = P.3 & v3 = P.last() & v4 = P.first() & L.v4 > L.v3 & L.v3 > L.v2 & L
  .v2 > L.v1 & (for x being set st x in P.vertices() holds L.x <= L.v4) & for x
being Vertex of G st x <> v4 & x,v2 are_adjacent & not x,v1 are_adjacent holds
  L.x < L.v4;
A12: for k being Nat st 4 <= k & R[k] holds R[k+1]
  proof
A13: 2*0+1 < 2*1+1;
    let kk be Nat such that
A14: 4 <= kk and
A15: R[kk];
    reconsider k=kk as non empty Nat by A14;
    consider P being Walk of G, v1,v2,v3,v4 being Vertex of G such that
A16: P is Path-like and
A17: P is open and
A18: P is chordless and
A19: P.length() = k-1 and
A20: v1 = P.(len P-2) and
A21: v2 = P.3 and
A22: v3 = P.last() and
A23: v4 = P.first() and
A24: L.v4 > L.v3 and
A25: L.v3 > L.v2 and
A26: L.v2 > L.v1 and
A27: for x being set st x in P.vertices() holds L.x <= L.v4 and
A28: for x being Vertex of G st x <> v4 & x,v2 are_adjacent & not x,
    v1 are_adjacent holds L.x < L.v4 by A15;
A29: len P = 2*(k-1) + 1 by A19,GLIB_001:112;
    2*k >= 2*4 by A14,XREAL_1:64;
    then
A30: 2*k-1 >= 8-1 by XREAL_1:9;
    then 1 <= len P by A29,XXREAL_0:2;
    then
A31: len P in dom P by FINSEQ_3:25;
    now
A32:  2*0+1 < len P by A29,A30,XXREAL_0:2;
      let e be set;
      assume e Joins v4,v3,G;
      then 1+2 = len P by A16,A17,A18,A22,A23,A32,CHORD:92;
      hence contradiction by A14,A29;
    end;
    then
A33: not v4,v3 are_adjacent by CHORD:def 3;
    3 < len P by A29,A30,XXREAL_0:2;
    then ex ez being set st ez Joins P.1,P.3,G by A16,A17,A18,A13,CHORD:92;
    then v4,v2 are_adjacent by A21,A23,CHORD:def 3;
    then consider v5 being Vertex of G such that
    v5 in dom L and
A34: L.v4 < L.v5 and
A35: v5,v3 are_adjacent and
A36: not v5,v2 are_adjacent and
A37: for x being Vertex of G st x <> v5 & x,v3 are_adjacent & not x,
    v2 are_adjacent holds L.x < L.v5 by A1,A2,A24,A25,A33,Def18;
    consider e being set such that
A38: e Joins P.last(),v5,G by A22,A35,CHORD:def 3;
    now
      L.v2 < L.v4 by A24,A25,XXREAL_0:2;
      then
A39:  L.v2 < L.v5 by A34,XXREAL_0:2;
      assume v5,v1 are_adjacent;
      then consider v6 being Vertex of G such that
      v6 in dom L and
A40:  L.v5 < L.v6 and
A41:  v6,v2 are_adjacent and
A42:  not v6,v1 are_adjacent and
      for x being Vertex of G st x <> v6 & x,v2 are_adjacent & not x,v1
      are_adjacent holds L.x < L.v6 by A1,A2,A26,A36,A39,Def18;
      thus contradiction by A28,A34,A40,A41,A42,XXREAL_0:2;
    end;
    then
A43: not ex e being set st e Joins P.(len P-2),v5,G by A20,CHORD:def 3;
    set Qr = P.addEdge(e);
    set Q = Qr.reverse();
A44: len Q = len Qr by GLIB_001:21;
A45: not v5 in P.vertices() by A27,A34;
    then Qr is open by A16,A17,A18,A38,A43,CHORD:97;
    then
A46: Q is open by GLIB_001:120;
    3 <= len P by A29,A30,XXREAL_0:2;
    then
A47: 3 in dom P by FINSEQ_3:25;
    then
A48: 3 in dom Qr by A38,Lm6;
    v2 = Qr.3 by A21,A38,A47,Lm6;
    then
A49: v2 = Q.(len Q-3+1) by A48,A44,GLIB_001:24;
    v4 = Qr.first() by A23,A38,GLIB_001:63;
    then
A50: v4 = Q.last() by GLIB_001:22;
A51: len Qr = len P + 2 by A38,GLIB_001:64;
    then
A52: len Qr-2 in dom Qr by A38,A31,Lm6;
    v3 = Qr.(len Qr - 2) by A22,A38,A51,A31,Lm6;
    then
A53: v3 = Q.(len Q-(len Qr-2)+1) by A52,A44,GLIB_001:24;
    v5 = Qr.last() by A38,GLIB_001:63;
    then
A54: v5 = Q.first() by GLIB_001:22;
    Qr is chordless by A16,A17,A18,A38,A45,A43,CHORD:97;
    then
A55: Q is chordless by CHORD:91;
    Qr.length() = k-1+1 by A19,A38,Lm4;
    then
A56: Q.length() = (k+1)-1 by Lm5;
A57: now
      let x be set;
      assume x in Q.vertices();
      then x in Qr.vertices() by GLIB_001:92;
      then
A58:  x in P.vertices() \/ {v5} by A38,GLIB_001:95;
      per cases by A58,XBOOLE_0:def 3;
      suppose
        x in P.vertices();
        then L.x <= L.v4 by A27;
        hence L.x <= L.v5 by A34,XXREAL_0:2;
      end;
      suppose
        x in {v5};
        hence L.x <= L.v5 by TARSKI:def 1;
      end;
    end;
    Qr is Path-like by A16,A17,A18,A38,A45,A43,CHORD:97;
    hence thesis by A24,A25,A34,A37,A46,A55,A56,A44,A49,A53,A50,A54,A57;
  end;
A59: 11 <= 11+G.order() by NAT_1:11;
  assume not V is perfect;
  then consider k being non empty Nat such that
A60: k <= len V and
A61: not for H being inducedSubgraph of G, V.followSet(k) for v being
  Vertex of H st v = V.k holds v is simplicial by CHORD:def 13;
  consider HH being (inducedSubgraph of G,V.followSet(k)), hv being Vertex of
  HH such that
A62: hv = V.k and
A63: not hv is simplicial by A61;
  consider ha,hb being Vertex of HH such that
A64: ha<>hb and
  hv<>ha and
  hv<>hb and
A65: hv,ha are_adjacent and
A66: hv,hb are_adjacent and
A67: not ha,hb are_adjacent by A63,CHORD:69;
A68: hv in the_Vertices_of HH;
A69: hb in the_Vertices_of HH;
  ha in the_Vertices_of HH;
  then reconsider v=hv,aa=ha,bb=hb as Vertex of G by A68,A69;
A70: V.followSet(k) is non empty Subset of the_Vertices_of G by A60,CHORD:107;
  then
A71: the_Vertices_of HH = V.followSet(k) by GLIB_000:def 37;
  now
A72: L.aa <> L.bb by A2,A3,A4,A64,FUNCT_1:def 4;
    per cases by A72,XXREAL_0:1;
    suppose
A73:  L.aa < L.bb;
      take aa, bb;
      thus aa in V.followSet(k) by A71;
      thus L.aa < L.bb by A73;
      thus v,aa are_adjacent by A65,A70,CHORD:45;
      thus v,bb are_adjacent by A66,A70,CHORD:45;
      thus not aa,bb are_adjacent by A67,A70,CHORD:45;
    end;
    suppose
A74:  L.aa > L.bb;
      take bb, aa;
      thus bb in V.followSet(k) by A71;
      thus L.aa > L.bb by A74;
      thus v,bb are_adjacent by A66,A70,CHORD:45;
      thus v,aa are_adjacent by A65,A70,CHORD:45;
      thus not bb,aa are_adjacent by A67,A70,CHORD:45;
    end;
  end;
  then consider a,bb being Vertex of G such that
A75: a in V.followSet(k) and
A76: L.a < L.bb and
A77: v,a are_adjacent and
A78: v,bb are_adjacent and
A79: not a,bb are_adjacent;
  defpred Q[Nat] means $1 in dom V & L.a < L.(V/.$1) & a <> V/.$1 & v,V/.$1
  are_adjacent & not a,V/.$1 are_adjacent;
A80: rng V = the_Vertices_of G by CHORD:def 12;
A81: ex k being Nat st Q[k]
  proof
    consider mbb being set such that
A82: mbb in dom V and
A83: bb = V.mbb by A80,FUNCT_1:def 3;
    reconsider mbb as Element of NAT by A82;
    take mbb;
    thus mbb in dom V by A82;
    thus L.a < L.(V/.mbb) by A76,A82,A83,PARTFUN1:def 6;
    thus a <> V/.mbb by A76,A82,A83,PARTFUN1:def 6;
    thus v,V/.mbb are_adjacent by A78,A82,A83,PARTFUN1:def 6;
    thus thesis by A79,A82,A83,PARTFUN1:def 6;
  end;
A84: for k being Nat st Q[k] holds k <= len V by FINSEQ_3:25;
  consider mb being Nat such that
A85: Q[mb] and
  for n being Nat st Q[n] holds n <= mb from NAT_1:sch 6(A84,A81);
  reconsider v,a,b = V/.mb as Vertex of G;
  consider ma being set such that
A86: ma in dom V and
A87: a = V.ma by A80,FUNCT_1:def 3;
  reconsider ma as Element of NAT by A86;
A88: a = V/.ma by A86,A87,PARTFUN1:def 6;
  0+1 <= k by NAT_1:13;
  then
A89: k in dom V by A60,FINSEQ_3:25;
A90: now
    assume ma <= k;
    then
A91: ma < k by A62,A78,A79,A87,XXREAL_0:1;
    a in the_Vertices_of G;
    then
A92: a in rng V by CHORD:def 12;
    V is one-to-one by CHORD:def 12;
    then a..V >= k by A75,A89,A92,CHORD:16;
    then a..V > ma by A91,XXREAL_0:2;
    hence contradiction by A86,A87,FINSEQ_4:24;
  end;
A93: v = V/.k by A62,A89,PARTFUN1:def 6;
  then
A94: L.v < L.a by A5,A89,A86,A88,A90;
A95: v <> b by A77,A85;
A96: R[4]
  proof
A97: L.a > L.v by A5,A89,A93,A86,A88,A90;
    consider c being Vertex of G such that
    c in dom L and
A98: L.b < L.c and
A99: c,a are_adjacent and
A100: not c,v are_adjacent and
A101: for x being Vertex of G st x <> c & x,a are_adjacent & not x,v
    are_adjacent holds L.x < L.c by A1,A2,A85,A94,Def18;
    consider P being Path of G,e1,e2 being set such that
A102: P is open and
A103: len P = 5 and
A104: P.length() = 2 and
    e1 Joins b,v,G and
    e2 Joins v,a,G and
    P.edges() = {e1,e2} and
A105: P.vertices() = {b,v,a} and
A106: P.1 = b and
A107: P.3 = v and
A108: P.5 = a by A77,A85,A95,CHORD:47;
    consider e being set such that
A109: e Joins P.last(),c,G by A99,A103,A108,CHORD:def 3;
    set Qr = P.addEdge(e);
    set Q = Qr.reverse();
A110: Qr.last() = c by A109,GLIB_001:63;
A111: len Qr = 5+2 by A103,A109,GLIB_001:64;
    then
A112: 1 in dom Qr by FINSEQ_3:25;
    5 in dom P by A103,FINSEQ_3:25;
    then
A113: Qr.5 = a by A108,A109,GLIB_001:65;
    5 in dom Qr by A111,FINSEQ_3:25;
    then
A114: a = Q.(7-5+1) by A111,A113,GLIB_001:24;
    7 in dom Qr by A111,FINSEQ_3:25;
    then c = Q.(7-7+1) by A111,A110,GLIB_001:24;
    then
A115: c = Q.first();
    3 in dom P by A103,FINSEQ_3:25;
    then
A116: Qr.3 = v by A107,A109,GLIB_001:65;
    Qr.length() = 2+1 by A104,A109,Lm4;
    then
A117: Q.length() = (3+1)-1 by Lm5;
    1 in dom P by A103,FINSEQ_3:25;
    then Qr.1 = b by A106,A109,GLIB_001:65;
    then b = Q.(len Qr-1+1) by A112,GLIB_001:24;
    then
A118: b = Q.last() by GLIB_001:21;
A119: len Q = len Qr by GLIB_001:21;
A120: P.first() = b by A106;
    P.last() = a by A103,A108;
    then
A121: P is chordless by A85,A103,A120,CHORD:90;
A122: now
      let x be set such that
A123: x in P.vertices();
      per cases by A105,A123,ENUMSET1:def 1;
      suppose
        x = b;
        hence L.x <= L.b;
      end;
      suppose
        x = v;
        hence L.x <= L.b by A85,A94,XXREAL_0:2;
      end;
      suppose
        x = a;
        hence L.x <= L.b by A85;
      end;
    end;
    then
A124: not c in P.vertices() by A98;
A125: not ex e being set st e Joins P.(len P-2),c,G by A100,A103,A107,
CHORD:def 3;
    then Qr is open by A102,A121,A109,A124,CHORD:97;
    then
A126: Q is open by GLIB_001:120;
A127: now
      let x be set;
      assume x in Q.vertices();
      then x in Qr.vertices() by GLIB_001:92;
      then
A128: x in P.vertices() \/ {c} by A109,GLIB_001:95;
      per cases by A128,XBOOLE_0:def 3;
      suppose
        x in P.vertices();
        then L.x <= L.b by A122;
        hence L.x <= L.c by A98,XXREAL_0:2;
      end;
      suppose
        x in {c};
        hence L.x <= L.c by TARSKI:def 1;
      end;
    end;
    3 in dom Qr by A111,FINSEQ_3:25;
    then v = Q.(7-3+1) by A111,A116,GLIB_001:24;
    then
A129: v = Q.(len Q-2) by A111,A119;
    Qr is chordless by A102,A121,A109,A124,A125,CHORD:97;
    then
A130: Q is chordless by CHORD:91;
    Qr is Path-like by A102,A121,A109,A124,A125,CHORD:97;
    hence thesis by A85,A98,A101,A126,A130,A117,A114,A129,A118,A115,A97,A127;
  end;
  for i being Nat st 4 <= i holds R[i] from NAT_1:sch 8(A96,A12);
  then R[G.order()+11] by A59,XXREAL_0:2;
  then consider P being Walk of G, v1,v2,v3,v4 being Vertex of G such that
A131: P is Path-like and
  P is open and
  P is chordless and
A132: P.length() = (G.order()+11)-1 and
  v1 = P.(len P-2) and
  v2 = P.3 and
  v3 = P.last() and
  v4 = P.first() and
  L.v4 > L.v3 and
  L.v3 > L.v2 and
  L.v2 > L.v1 and
  for x being Vertex of G st x <> v4 & x,v2 are_adjacent & not x,v1
  are_adjacent holds L.x < L.v4;
  len P = 2*(G.order()+10)+1 by A132,GLIB_001:112;
  then 2*G.order()+21 + 1 = 2*len P.vertexSeq() by GLIB_001:def 14;
  then G.order() + 11 <= G.order() + 1 by A131,GLIB_001:154;
  hence contradiction by XREAL_1:8;
end;

theorem :: Theorem 4.3, Golumbic p. 86
  for G being finite chordal _Graph holds (((LexBFS:CSeq(G)).Result())`1
  )" is perfect VertexScheme of G
proof
  let G be finite chordal _Graph;
  set Hh = ((LexBFS:CSeq(G)).Result())`1;
  reconsider V = Hh" as VertexScheme of G by Th50;
A1: dom Hh = the_Vertices_of G by Th49;
  Hh = (LexBFS:CSeq(G))``1.Result() by Th40;
  then Hh is one-to-one by Th18;
  then
A2: V" = Hh by FUNCT_1:43;
  Hh is with_property_L3 by Th53;
  hence thesis by A1,A2,Th54;
end;

begin :: The Maximum Cardinality Search algorithm

definition
  let G be _Graph;
  mode MCS:Labeling of G is Element of [: PFuncs(the_Vertices_of G, NAT),
    Funcs(the_Vertices_of G, NAT) :];
end;

definition
  let G be finite _Graph;
  func MCS:Init(G) -> MCS:Labeling of G equals
  [ {}, the_Vertices_of G --> 0 ];
  coherence
  proof
    set f = the_Vertices_of G --> 0;
A1: rng {} c= NAT;
A2: rng f c= NAT by RELAT_1:def 19;
    dom f = the_Vertices_of G by FUNCOP_1:13;
    then
A3: f in Funcs(the_Vertices_of G, NAT) by A2,FUNCT_2:def 2;
    dom {} c= the_Vertices_of G by XBOOLE_1:2;
    then {} in PFuncs(the_Vertices_of G,NAT) by A1,PARTFUN1:def 3;
    hence thesis by A3,ZFMISC_1:def 2;
  end;
end;

definition
  let G be finite _Graph, L be MCS:Labeling of G;
  func MCS:PickUnnumbered(L) -> Vertex of G means
  :Def20:
  it = choose
  the_Vertices_of G if dom L`1 = the_Vertices_of G otherwise ex S being finite
  non empty natural-membered set, F being Function st S = rng F & F = L`2 | (
  the_Vertices_of G \ dom (L`1)) & it = choose (F " {max S});
  existence
  proof
    set VG = the_Vertices_of G;
    set V2G = L`2;
    set VLG = L`1;
    set F = V2G | (VG \ dom VLG);
    set S = rng F;
    per cases;
    suppose
      dom VLG = VG;
      hence thesis;
    end;
    suppose
A1:   dom VLG <> VG;
A2:   dom F = dom V2G /\ (VG \ dom VLG) by RELAT_1:61;
      dom V2G = VG by FUNCT_2:def 1;
      then
A3:   dom F = (VG /\ VG) \ dom VLG by A2,XBOOLE_1:49;
      now
        assume dom F = {};
        then VG c= dom VLG by A3,XBOOLE_1:37;
        hence contradiction by A1,XBOOLE_0:def 10;
      end;
      then reconsider S as non empty finite natural-membered set by RELAT_1:42;
      set y = max S;
      set IT = choose (F " {max S});
      y in S by XXREAL_2:def 8;
      then F " {max S} is non empty by FUNCT_1:72;
      then IT in dom F by FUNCT_1:def 7;
      then IT in dom V2G by RELAT_1:57;
      then reconsider IT as Vertex of G;
      ex S being finite non empty natural-membered set, F being Function
st S = rng F & F = (L`2) | (the_Vertices_of G \ dom L`1) & IT = choose (F " {
      max S}) & IT is Vertex of G;
      hence thesis;
    end;
  end;
  uniqueness;
  consistency;
end;

definition
  let G be finite _Graph, L be MCS:Labeling of G, v be set;
  func MCS:LabelAdjacent(L, v) -> MCS:Labeling of G equals
  [ L`1, (L`2)
  .incSubset(G.AdjacentSet({v}) \ dom L`1, 1) ];
  coherence
  proof
    set V2G = L`2;
    set VLG = L`1;
    set f = V2G.incSubset(G.AdjacentSet({v})\ dom VLG,1);
    now
      let x be set;
      assume x in rng f;
      then ex y being set st y in dom f & f.y = x by FUNCT_1:def 3;
      hence x in NAT;
    end;
    then
A1: rng f c= NAT by TARSKI:def 3;
    dom f = dom V2G by Def4;
    then dom f = the_Vertices_of G by FUNCT_2:def 1;
    then f is Function of the_Vertices_of G, NAT by A1,FUNCT_2:2;
    then f in Funcs(the_Vertices_of G, NAT) by FUNCT_2:8;
    hence thesis by ZFMISC_1:87;
  end;
end;

definition
  let G be finite _Graph, L be MCS:Labeling of G, v be Vertex of G, n be Nat;
  func MCS:Update(L, v, n) -> MCS:Labeling of G means
  :Def22:
  ex M being
  MCS:Labeling of G st M = [L`1 +* (v .--> (G.order()-'n)), L`2] & it =
  MCS:LabelAdjacent(M, v);
  existence
  proof
    set k = G.order()-'n;
    set L1 = L`1 +* (v .--> k);
A1: dom L1 = dom L`1 \/ {v} by Lm1;
    rng (v .--> k) c= {k} by FUNCOP_1:13;
    then rng (v .--> k) c= NAT by XBOOLE_1:1;
    then
A2: rng L`1 \/ rng (v .--> k) c= NAT by XBOOLE_1:8;
    rng L1 c= rng L`1 \/ rng (v .--> k) by FUNCT_4:17;
    then rng L1 c= NAT by A2,XBOOLE_1:1;
    then L1 in PFuncs(the_Vertices_of G, NAT) by A1,PARTFUN1:def 3;
    then reconsider M = [L1, L`2] as MCS:Labeling of G by ZFMISC_1:87;
    MCS:LabelAdjacent(M, v) is MCS:Labeling of G;
    hence thesis;
  end;
  uniqueness;
end;

definition
  let G be finite _Graph, L be MCS:Labeling of G;
  func MCS:Step(L) -> MCS:Labeling of G equals
  :Def23:
  L if G.order() <= card
  dom (L`1) otherwise MCS:Update(L, MCS:PickUnnumbered(L), card dom (L`1));
  coherence;
  consistency;
end;

definition
  let G be _Graph;
  mode MCS:LabelingSeq of G -> ManySortedSet of NAT means
    :Def24:
    for n being Nat holds it.n is MCS:Labeling of G;
  existence
  proof
    set L = the MCS:Labeling of G;
    deffunc F(set) = L;
    consider f being ManySortedSet of NAT such that
A1: for i being set st i in NAT holds f.i = F(i) from PBOOLE:sch 4;
    take f;
    let n be Nat;
    n in NAT by ORDINAL1:def 12;
    hence thesis by A1;
  end;
end;

definition
  let G be _Graph, S be MCS:LabelingSeq of G, n be Nat;
  redefine func S.n -> MCS:Labeling of G;
  coherence by Def24;
end;

definition
  let G be _Graph, S be MCS:LabelingSeq of G;
  redefine func S.Result() -> MCS:Labeling of G;
  coherence by Def24;
end;

definition
  let G be finite _Graph, S be MCS:LabelingSeq of G;
  func S``1 -> preVNumberingSeq of G means
  :Def25:
  for n being Nat holds it.n = (S.n)`1;
  existence
  proof
    deffunc F(set) = (S.$1)`1;
    consider f being ManySortedSet of NAT such that
A1: for i being set st i in NAT holds f.i = F(i) from PBOOLE:sch 4;
    now
      let i be Nat;
      i in NAT by ORDINAL1:def 12;
      then f.i = (S.i)`1 by A1;
      hence f.i is PartFunc of the_Vertices_of G, NAT;
    end;
    then reconsider f as preVNumberingSeq of G by Def8;
    take f;
    let n be Nat;
    n in NAT by ORDINAL1:def 12;
    hence thesis by A1;
  end;
  uniqueness
  proof
    let it1, it2 be preVNumberingSeq of G such that
A2: for n being Nat holds it1.n = (S.n)`1 and
A3: for n being Nat holds it2.n = (S.n)`1;
    now
      let i be set;
      assume i in NAT;
      then reconsider i9 = i as Nat;
      thus it1.i = (S.i9)`1 by A2
        .= it2.i by A3;
    end;
    hence it1 = it2 by PBOOLE:3;
  end;
end;

definition
  let G be finite _Graph;
  func MCS:CSeq(G) -> MCS:LabelingSeq of G means
  :Def26:
  it.0 = MCS:Init(G) & for n being Nat holds it.(n+1) = MCS:Step(it.n);
  existence
  proof
    defpred P[set,set,set] means ($2 is MCS:Labeling of G & $1 is Nat & ex nn
being Nat,Gn,Gn1 being MCS:Labeling of G st $1 = nn & $2 = Gn & $3 = Gn1 & Gn1
= MCS:Step(Gn)) or ((not $2 is MCS:Labeling of G or not $1 is Nat) & $2 = $3);
    now
      let n,x be set;
      now
        per cases;
        suppose
A1:       x is MCS:Labeling of G & n is Nat;
          then reconsider Gn=x as MCS:Labeling of G;
          ex SGn being MCS:Labeling of G st SGn = MCS:Step(Gn);
          hence ex y being set st P[n,x,y] by A1;
        end;
        suppose
          not x is MCS:Labeling of G or not n is Nat;
          hence ex y being set st P[n,x,y];
        end;
      end;
      hence ex y being set st P[n,x,y];
    end;
    then
A2: for n being Element of NAT for x being set ex y being set st P[n,x,y];
    consider IT being Function such that
A3: dom IT = NAT & IT.0 = MCS:Init(G) & for n being Element of NAT
    holds P[n,IT.n,IT.(n+1)] from RECDEF_1:sch 1(A2);
    reconsider IT as ManySortedSet of NAT by A3,PARTFUN1:def 2,RELAT_1:def 18;
    defpred P2[Nat] means IT.$1 is MCS:Labeling of G;
A4: now
      let n be Nat;
      assume
A5:   P2[n];
      n in NAT by ORDINAL1:def 12;
      then ex nn being Nat, Gn,Gn1 being MCS:Labeling of G st n = nn & IT.n =
      Gn & IT.(n+1) = Gn1 & Gn1 = MCS:Step(Gn) by A3,A5;
      hence P2[n+1];
    end;
A6: P2[ 0 ] by A3;
    for n being Nat holds P2[n] from NAT_1:sch 2(A6,A4);
    then reconsider IT as MCS:LabelingSeq of G by Def24;
    take IT;
    thus IT.0 = MCS:Init(G) by A3;
    let n be Nat;
    n in NAT by ORDINAL1:def 12;
    then
    ex nn being Nat, Gn,Gn1 being MCS:Labeling of G st n = nn & IT.n =
    Gn & IT.(n+1) = Gn1 & Gn1 = MCS:Step(Gn) by A3;
    hence thesis;
  end;
  uniqueness
  proof
    let IT1,IT2 be MCS:LabelingSeq of G such that
A7: IT1.0 = MCS:Init(G) and
A8: for n being Nat holds IT1.(n+1) = MCS:Step(IT1.n) and
A9: IT2.0 = MCS:Init(G) and
A10: for n being Nat holds IT2.(n+1) = MCS:Step(IT2.n);
    defpred P[Nat] means IT1.$1 = IT2.$1;
    now
      let n be Nat;
      assume P[n];
      then IT1.(n+1) = MCS:Step(IT2.n) by A8
        .= IT2.(n+1) by A10;
      hence P[n+1];
    end;
    then
A11: for n being Element of NAT st P[n] holds P[n+1];
A12: P[ 0 ] by A7,A9;
    for n being Element of NAT holds P[n] from NAT_1:sch 1(A12,A11);
    then for n being set st n in NAT holds IT1.n = IT2.n;
    hence IT1 = IT2 by PBOOLE:3;
  end;
end;

theorem Th56:
  for G being finite _Graph holds MCS:CSeq(G) is iterative
proof
  let G be finite _Graph;
  set CS = MCS:CSeq(G);
  let k,n be Nat;
  CS.(k+1) = MCS:Step(CS.k) by Def26;
  hence thesis by Def26;
end;

registration
  let G be finite _Graph;
  cluster MCS:CSeq(G) -> iterative;
  coherence by Th56;
end;

theorem Th57:
  for G being finite _Graph, v being set holds ((MCS:Init(G))`2).v = 0
proof
  let G be finite _Graph, v be set;
  set g = the_Vertices_of G --> {};
  [{},g]`2 =g;
  then
A1: (MCS:Init(G))`2 = g;
  then dom (MCS:Init(G))`2 = the_Vertices_of G by FUNCOP_1:13;
  then reconsider f = g as PartFunc of the_Vertices_of G, rng g by A1,
RELSET_1:4;
  now
    let x be set;
    per cases;
    suppose
      x in dom f;
      hence f.x = {} by FUNCOP_1:7;
    end;
    suppose
      not x in dom f;
      hence f.x = {} by FUNCT_1:def 2;
    end;
  end;
  hence thesis by A1;
end;

theorem Th58:
  for G being finite _Graph, L be MCS:Labeling of G, x being set
  st not x in dom L`1 & dom L`1 <> the_Vertices_of G holds (L`2).x <= (L`2).(
  MCS:PickUnnumbered(L))
proof
  let G be finite _Graph, L be MCS:Labeling of G, x be set such that
A1: not x in dom L`1 and
A2: dom L`1 <> the_Vertices_of G;
  set VG = the_Vertices_of G;
  set V2G = L`2;
  set VLG = L`1;
  set w = MCS:PickUnnumbered(L);
  consider S being finite non empty natural-membered set, F being Function
  such that
A3: S = rng F and
A4: F = V2G | (VG \ dom VLG) and
A5: w = choose (F " {max S}) by A2,Def20;
A6: dom F = dom V2G /\ (VG \ dom VLG) by A4,RELAT_1:61;
  set y = max S;
  y in rng F by A3,XXREAL_2:def 8;
  then
A7: F " {max S} is non empty by FUNCT_1:72;
  then w in dom F by A5,FUNCT_1:def 7;
  then
A8: V2G.w = F.w by A4,FUNCT_1:47;
  F.w in {max S} by A5,A7,FUNCT_1:def 7;
  then
A9: V2G.w = y by A8,TARSKI:def 1;
A10: dom L`2 = the_Vertices_of G by FUNCT_2:def 1;
  per cases;
  suppose
    x in the_Vertices_of G;
    then x in VG \ dom VLG by A1,XBOOLE_0:def 5;
    then
A11: x in dom F by A10,A6,XBOOLE_0:def 4;
    then
A12: F.x in S by A3,FUNCT_1:def 3;
    F.x = V2G.x by A4,A11,FUNCT_1:47;
    hence thesis by A9,A12,XXREAL_2:def 8;
  end;
  suppose
    not x in the_Vertices_of G;
    hence thesis by A10,FUNCT_1:def 2;
  end;
end;

theorem Th59:
  for G being finite _Graph, L be MCS:Labeling of G st dom L`1 <>
  the_Vertices_of G holds not MCS:PickUnnumbered(L) in dom L`1
proof
  let G be finite _Graph, L be MCS:Labeling of G such that
A1: dom L`1 <> the_Vertices_of G;
  set VG = the_Vertices_of G;
  set V2G = L`2;
  set VLG = L`1;
  set w = MCS:PickUnnumbered(L);
  consider S being finite non empty natural-membered set, F being Function
  such that
A2: S = rng F and
A3: F = V2G | (VG \ dom VLG) and
A4: w = choose (F " {max S}) by A1,Def20;
  set y = max S;
  y in rng F by A2,XXREAL_2:def 8;
  then F " {max S} is non empty by FUNCT_1:72;
  then
A5: w in dom F by A4,FUNCT_1:def 7;
  assume w in dom VLG;
  then
A6: not w in VG \ dom VLG by XBOOLE_0:def 5;
  dom F = dom V2G /\ (VG \ dom VLG) by A3,RELAT_1:61;
  hence contradiction by A5,A6,XBOOLE_0:def 4;
end;

theorem Th60:
  for G being finite _Graph, L be MCS:Labeling of G, v,x being set
  st not x in G.AdjacentSet({v}) holds (L`2).x = (MCS:LabelAdjacent(L,v))`2.x
proof
  let G be finite _Graph, L be MCS:Labeling of G, v,x be set such that
A1: not x in G.AdjacentSet({v});
  set V2G = L`2;
  set VLG = L`1;
  set GL = MCS:LabelAdjacent(L,v);
  set V2 = GL`2;
  [L`1,(L`2).incSubset(G.AdjacentSet({v}) \ dom L`1, 1)]`2
     =(L`2).incSubset(G.AdjacentSet({v}) \ dom L`1, 1);
  then
A2: V2 = V2G.incSubset(G.AdjacentSet({v})\dom VLG,1);
  not x in G.AdjacentSet({v}) \ dom VLG by A1,XBOOLE_0:def 5;
  hence thesis by A2,Def4;
end;

theorem Th61:
  for G being finite _Graph, L be MCS:Labeling of G, v,x being set
  st x in dom L`1 holds L`2.x = (MCS:LabelAdjacent(L,v))`2.x
proof
  let G be finite _Graph, L be MCS:Labeling of G, v,x be set such that
A1: x in dom L`1;
  set V2G = L`2;
  set VLG = L`1;
  set GL = MCS:LabelAdjacent(L,v);
  set V2 = GL`2;
  [L`1,(L`2).incSubset(G.AdjacentSet({v}) \ dom L`1, 1)]`2
     =(L`2).incSubset(G.AdjacentSet({v}) \ dom L`1, 1);
  then
A2: V2 = V2G.incSubset(G.AdjacentSet({v})\dom VLG,1);
  not x in G.AdjacentSet({v}) \ dom VLG by A1,XBOOLE_0:def 5;
  hence thesis by A2,Def4;
end;

theorem Th62:
  for G being finite _Graph, L being MCS:Labeling of G, v,x being
  set st x in dom L`2 & x in G.AdjacentSet{v} & not x in dom L`1 holds (
  MCS:LabelAdjacent(L,v))`2.x = (L`2).x + 1
proof
  let G be finite _Graph, L being MCS:Labeling of G, v,x be set such that
A1: x in dom L`2 and
A2: x in G.AdjacentSet({v}) and
A3: not x in dom L`1;
  set V2G = L`2;
  set VLG = L`1;
  set GL = MCS:LabelAdjacent(L,v);
  set V2 = GL`2;
  [L`1,(L`2).incSubset(G.AdjacentSet({v}) \ dom L`1, 1)]`2
     =(L`2).incSubset(G.AdjacentSet({v}) \ dom L`1, 1);
  then
A4: V2 = V2G.incSubset(G.AdjacentSet({v})\dom VLG,1);
  x in G.AdjacentSet({v}) \ dom VLG by A2,A3,XBOOLE_0:def 5;
  hence thesis by A1,A4,Def4;
end;

theorem
  for G being finite _Graph, L being MCS:Labeling of G, v being set st
  dom L`2 = the_Vertices_of G holds dom (MCS:LabelAdjacent(L,v))`2 =
  the_Vertices_of G
proof
  let G be finite _Graph, L be MCS:Labeling of G, v be set such that
A1: dom L`2 = the_Vertices_of G;
  set V2G = L`2;
  set VLG = L`1;
  set GL = MCS:LabelAdjacent(L,v);
  set V2 = GL`2;
  [L`1,(L`2).incSubset(G.AdjacentSet({v}) \ dom L`1, 1)]`2
     =(L`2).incSubset(G.AdjacentSet({v}) \ dom L`1, 1);
  then
  V2 = V2G.incSubset(G.AdjacentSet({v})\dom VLG,1);
  hence thesis by A1,Def4;
end;

theorem Th64:
  for G being finite _Graph, n being Nat st card dom (((MCS:CSeq(G
  )).n))`1 < G.order() holds ((MCS:CSeq(G)).(n+1))`1 = ((MCS:CSeq(G)).n)`1 +* (
MCS:PickUnnumbered((MCS:CSeq(G)).n) .--> (G.order()-'(card (dom ((MCS:CSeq(G)).
  n)`1))))
proof
  let G be finite _Graph, n be Nat such that
A1: card (dom ((MCS:CSeq(G)).n)`1) < G.order();
  set CN1 = (MCS:CSeq(G)).(n+1);
  set CSN = (MCS:CSeq(G)).n;
  set VLN = CSN`1;
  set w = MCS:PickUnnumbered(CSN);
  set k = G.order() -' card (dom VLN);
  CN1 = MCS:Step(CSN) by Def26;
  then CN1 = MCS:Update(CSN, w, card (dom VLN)) by A1,Def23;
  then consider L being MCS:Labeling of G such that
A2: L = [CSN`1 +* (w .--> k), CSN`2] and
A3: CN1 = MCS:LabelAdjacent(L, w) by Def22;
  [L`1,(L`2).incSubset(G.AdjacentSet({w}) \ dom L`1, 1)]`1
     = L`1;
  then CN1`1 = [CSN`1 +* (w .--> k), CSN`2]`1 by A3,A2;
  hence thesis;
end;

theorem Th65:
  for G being finite _Graph, n being Nat st n <= G.order() holds
  card dom ((MCS:CSeq(G)).n)`1 = n
proof
  let G be finite _Graph, n be Nat such that
A1: n <= G.order();
  defpred P[Nat] means $1 <= G.order() implies card dom ((MCS:CSeq(G)).$1)`1 =
  $1;
A2: for k being Element of NAT st k < G.order() & card dom ((MCS:CSeq(G)).k)
  `1 = k holds card dom ((MCS:CSeq(G)).(k+1))`1 = k+1
  proof
    let k be Element of NAT such that
A3: k < G.order() and
A4: card dom ((MCS:CSeq(G)).k)`1 = k;
    set CK1 = (MCS:CSeq(G)).(k+1);
    set CSK = (MCS:CSeq(G)).k;
    set VLK = CSK`1;
    set VK1 = CK1`1;
    set w = MCS:PickUnnumbered(CSK);
    set wf = w .--> (G.order() -' k);
A5: dom wf = {w} by FUNCOP_1:13;
    VK1 = VLK +* (w .--> (G.order()-'k)) by A3,A4,Th64;
    then dom VK1 = dom VLK \/ {w} by A5,FUNCT_4:def 1;
    hence thesis by A3,A4,Th59,CARD_2:41;
  end;
A6: for k being Nat st P[k] holds P[k+1]
  proof
    let k be Nat such that
A7: P[k];
    per cases;
    suppose
      k < G.order();
      hence thesis by A2,A7;
    end;
    suppose
      k >= G.order();
      hence thesis by NAT_1:13;
    end;
  end;
A8: [ {}, the_Vertices_of G --> 0 ]`1 = {};
  (MCS:CSeq(G)).0 = MCS:Init(G) by Def26;
  then
A9: P[ 0 ] by A8;
  for k being Nat holds P[k] from NAT_1:sch 2(A9,A6);
  hence thesis by A1;
end;

theorem Th66:
  for G being finite _Graph, n being Nat st G.order() <= n holds (
  MCS:CSeq(G)).(G.order()) = (MCS:CSeq(G)).n
proof
  let G be finite _Graph, n be Nat;
  assume G.order() <= n;
  then
A1: ex i being Nat st G.order() + i = n by NAT_1:10;
  set CS = MCS:CSeq(G);
  defpred V[Nat] means G.order() = card (dom (CS.(G.order()+$1))`1);
  defpred P[Nat] means (CS.(G.order())) = (CS.(G.order()+$1));
A2: for k being Nat st V[k] holds V[k+1]
  proof
    let k be Nat such that
A3: V[k];
    set CK1 = (MCS:CSeq(G)).(G.order()+k+1);
    set CSK = (MCS:CSeq(G)).(G.order()+k);
    CK1 = MCS:Step(CSK) by Def26;
    hence thesis by A3,Def23;
  end;
A4: V[ 0 ] by Th65;
A5: for k being Nat holds V[k] from NAT_1:sch 2(A4,A2);
A6: for k being Nat st P[k] holds P[k+1]
  proof
    let k be Nat such that
A7: P[k];
    set CK1 = (MCS:CSeq(G)).(G.order()+k+1);
    set CSK = (MCS:CSeq(G)).(G.order()+k);
    set VLK = CSK`1;
A8: CK1 = MCS:Step(CSK) by Def26;
    card dom VLK = G.order() by A5;
    hence thesis by A7,A8,Def23;
  end;
A9: P[ 0 ];
  for k being Nat holds P[k] from NAT_1:sch 2(A9,A6);
  hence thesis by A1;
end;

theorem Th67:
  for G being finite _Graph, m,n being Nat st G.order() <= m & m
  <= n holds (MCS:CSeq(G)).m = (MCS:CSeq(G)).n
proof
  let G be finite _Graph, m,n be Nat such that
A1: G.order() <= m and
A2: m <= n;
  (MCS:CSeq(G)).m = (MCS:CSeq(G)).(G.order()) by A1,Th66;
  hence thesis by A1,A2,Th66,XXREAL_0:2;
end;

theorem Th68:
  for G being finite _Graph holds MCS:CSeq(G) is eventually-constant
proof
  let G be finite _Graph;
  take G.order();
  let m be Nat;
  assume G.order() <= m;
  hence (MCS:CSeq(G)).(G.order()) = (MCS:CSeq(G)).m by Th66;
end;

registration
  let G be finite _Graph;
  cluster MCS:CSeq(G) -> eventually-constant;
  coherence by Th68;
end;

theorem Th69:
  for G being finite _Graph, n being Nat holds dom ((MCS:CSeq(G)).
  n)`1 = the_Vertices_of G iff G.order() <= n
proof
  let G be finite _Graph, n be Nat;
  set VLN = ((MCS:CSeq(G)).n)`1;
  set CSO = (MCS:CSeq(G)).G.order();
  set VLO = CSO`1;
  thus dom VLN = the_Vertices_of G implies not n < G.order() by Th65;
  card dom VLO = card the_Vertices_of G by Th65;
  then
A1: dom VLO = the_Vertices_of G by CARD_FIN:1;
  assume G.order() <= n;
  hence thesis by A1,Th67;
end;

theorem Th70:
  for G being finite _Graph holds (MCS:CSeq(G)).Lifespan() = G .order()
proof
  let G be finite _Graph;
  set CS = MCS:CSeq(G);
A1: for n being Nat st CS.n = CS.(n+1) holds G.order() <= n
  proof
    let n be Nat such that
A2: CS.n = CS.(n+1);
    set w = MCS:PickUnnumbered(CS.n);
    set VN1 = (CS.(n+1))`1;
    set VLN = (CS.n)`1;
    set j = card (dom VLN);
    set wf = w .--> (G.order() -' j);
    assume
A3: n < G.order();
    then dom VLN <> the_Vertices_of G by Th69;
    then
A4: not w in dom VLN by Th59;
    j < G.order() by A3,Th65;
    then
A5: VN1 = VLN +* (w .--> (G.order() -' j)) by Th64;
    dom wf = {w} by FUNCOP_1:13;
    then
A6: dom VN1 = dom VLN \/ {w} by A5,FUNCT_4:def 1;
    w in {w} by TARSKI:def 1;
    hence contradiction by A2,A4,A6,XBOOLE_0:def 3;
  end;
  G.order() <= G.order()+1 by NAT_1:13;
  then CS.(G.order()) = CS.(G.order()+1) by Th66;
  hence thesis by A1,GLIB_000:def 55;
end;

theorem Th71:
  for G being finite _Graph holds (MCS:CSeq(G))``1 is eventually-constant
proof
  let G be finite _Graph;
  set CS = (MCS:CSeq(G));
  set S = CS``1;
  now
    consider n being Nat such that
A1: for m being Nat st n <= m holds CS.n = CS.m by Def7;
    take n;
    let m be Nat such that
A2: n <= m;
    thus S.n = (CS.n)`1 by Def25
      .= (CS.m)`1 by A1,A2
      .= S.m by Def25;
  end;
  hence thesis by Def7;
end;

theorem Th72:
  for G being finite _Graph holds (MCS:CSeq(G))``1.Lifespan() = (
  MCS:CSeq(G)).Lifespan()
proof
  let G be finite _Graph;
  set S = MCS:CSeq(G);
  set VN = S``1;
  set ls = G.order();
A1: VN is eventually-constant by Th71;
A2: (S.(ls+1))`1 = S``1.(ls+1) by Def25;
A3: now
    let n be Nat such that
A4: VN.n = VN.(n+1) and
A5: ls > n;
    n+1 <= ls by A5,NAT_1:13;
    then
A6: card dom (S.(n+1))`1 = n+1 by Th65;
A7: (S.(n+1))`1 = VN.(n+1) by Def25;
A8: (S.n)`1 = VN.n by Def25;
    card dom (S.n)`1 = n by A5,Th65;
    hence contradiction by A4,A6,A8,A7;
  end;
  (S.ls)`1 = S``1.ls by Def25;
  then
A9: VN.ls = VN.(ls+1) by A2,Th66,NAT_1:11;
  S.Lifespan() = ls by Th70;
  hence thesis by A1,A9,A3,GLIB_000:def 55;
end;

theorem Th73:
  for G being finite _Graph holds MCS:CSeq(G)``1 is vertex-numbering
proof
  let G be finite _Graph;
  set GS = MCS:CSeq(G);
  set S = GS``1;
A1: GS.0 = MCS:Init(G) by Def26;
A2: [ {}, the_Vertices_of G --> 0 ]`1 = {};
  S.0 = (GS.0)`1 by Def25;
  hence S.0 = {} by A1,A2;
  now
    let k, n be Nat such that
A3: S.k = S.n;
A4: S.(k+1) = (GS.(k+1))`1 by Def25;
A5: S.k = (GS.k)`1 by Def25;
A6: S.(n+1) = (GS.(n+1))`1 by Def25;
A7: S.n = (GS.n)`1 by Def25;
    per cases;
    suppose
A8:   k <= G.order() & n <= G.order();
      then card dom ((GS.n)`1) = n by Th65;
      hence S.(k+1) = S.(n+1) by A3,A5,A7,A8,Th65;
    end;
    suppose
A9:   k <= G.order() & n >= G.order();
      then
A10:   GS.n = GS.(G.order()) by Th66;
A11:  card dom ((GS.(G.order()))`1) = G.order() by Th65;
A12:  n+1 >= G.order() by A9,NAT_1:13;
      card dom ((GS.k)`1) = k by A9,Th65;
      then k+1 >= G.order() by A3,A5,A7,A10,A11,NAT_1:13;
      hence S.(k+1) = (GS.(G.order()))`1 by A4,Th66
        .= S.(n+1) by A6,A12,Th66;
    end;
    suppose
A13:  k >= G.order() & n <= G.order();
      then
A14:  GS.k = GS.(G.order()) by Th66;
A15:  card dom ((GS.(G.order()))`1) = G.order() by Th65;
      card dom ((GS.n)`1) = n by A13,Th65;
      then
A16:  n+1 >= G.order() by A3,A5,A7,A14,A15,NAT_1:13;
      k+1 >= G.order() by A13,NAT_1:13;
      hence S.(k+1) = (GS.(G.order()))`1 by A4,Th66
        .= S.(n+1) by A6,A16,Th66;
    end;
    suppose
A17:  k >= G.order() & n >= G.order();
      then
A18:  n+1 >= G.order() by NAT_1:13;
A19:  k+1 >= G.order() by A17,NAT_1:13;
      thus S.(k+1) = (GS.(k+1))`1 by Def25
        .= (GS.(G.order()))`1 by A19,Th66
        .= (GS.(n+1))`1 by A18,Th66
        .= S.(n+1) by Def25;
    end;
  end;
  hence S is iterative by Def6;
  S is eventually-constant by Th71;
  hence S is halting;
  GS.Lifespan() = S.Lifespan() by Th72;
  hence
A20: S.Lifespan() = G.order() by Th70;
  let n be Nat such that
A21: n < S.Lifespan();
  take w = MCS:PickUnnumbered(GS.n);
A22: (GS.n)`1 = S.n by Def25;
  then dom (S.n) <> the_Vertices_of G by A20,A21,Th69;
  hence not w in dom (S.n) by A22,Th59;
A23: (GS.(n+1))`1 = S.(n+1) by Def25;
  n = card dom (S.n) by A20,A21,A22,Th65;
  hence thesis by A20,A21,A22,A23,Th64;
end;

registration
  let G be finite _Graph;
  cluster (MCS:CSeq(G))``1 -> vertex-numbering;
  coherence by Th73;
end;

theorem Th74:
  for G being finite _Graph, n being Nat st n < G.order() holds ((
  MCS:CSeq(G))``1).PickedAt(n) = MCS:PickUnnumbered((MCS:CSeq(G)).n)
proof
  let G be finite _Graph, n be Nat such that
A1: n < G.order();
  set GS = MCS:CSeq(G);
  set CSN = GS.n;
  set CS1 = GS.(n+1);
  set VLN = CSN`1;
  set VL1 = CS1`1;
A2: GS.Lifespan() = G.order() by Th70;
  set PU = MCS:PickUnnumbered(CSN);
  set f2 = PU .--> (GS.Lifespan()-'n);
A3: dom f2 = {PU} by FUNCOP_1:13;
  n = card dom VLN by A1,Th65;
  then VL1 = VLN +* (PU .--> (GS.Lifespan()-'n)) by A1,A2,Th64;
  then
A4: dom VL1 = dom VLN \/ {PU} by A3,FUNCT_4:def 1;
A5: (GS``1).Lifespan() = GS.Lifespan() by Th72;
  set PA = (GS``1).PickedAt(n);
  set f1 = PA .--> (GS.Lifespan()-'n);
A6: dom f1 = {PA} by FUNCOP_1:13;
A7: VLN = (GS``1).n by Def25;
  VL1 = (GS``1).(n+1) by Def25;
  then VL1 = VLN +* (PA .--> (GS.Lifespan()-'n)) by A1,A2,A7,A5,Def10;
  then
A8: dom VL1 = dom VLN \/ {PA} by A6,FUNCT_4:def 1;
A9: not PA in dom VLN by A1,A2,A7,A5,Def10;
  now
    assume PA <> PU;
    then not PA in {PU} by TARSKI:def 1;
    then
A10: not PA in dom VL1 by A9,A4,XBOOLE_0:def 3;
    PA in {PA} by TARSKI:def 1;
    hence contradiction by A8,A10,XBOOLE_0:def 3;
  end;
  hence thesis;
end;

theorem Th75:
  for G being finite _Graph, n being Nat st n < G.order() ex w
being Vertex of G st w = MCS:PickUnnumbered((MCS:CSeq(G)).n) & for v being set
holds (v in G.AdjacentSet({w}) & not v in dom (((MCS:CSeq(G)).n)`1) implies (((
  MCS:CSeq(G)).(n+1))`2).v = (((MCS:CSeq(G)).n)`2).v + 1) & (not v in G
.AdjacentSet({w}) or v in dom (((MCS:CSeq(G)).n)`1) implies (((MCS:CSeq(G)).(n+
  1))`2).v = (((MCS:CSeq(G)).n)`2).v)
proof
  let G be finite _Graph, n be Nat such that
A1: n < G.order();
  set CSN = (MCS:CSeq(G)).n;
  set VLN = CSN`1;
A2: n = card dom VLN by A1,Th65;
  set k = G.order() -' n;
  set w = MCS:PickUnnumbered(CSN);
  set CN1 = (MCS:CSeq(G)).(n+1);
  set CSlv = [ CSN`1 +* (w .--> k), CSN`2 ];
  set CSlv1 = CSN`1 +* (w .--> k);
A3: dom CSlv1 = dom (CSN`1) \/ {w} by Lm1;
  rng (w .--> k) = {k} by FUNCOP_1:8;
  then
A4: rng (CSN`1) \/ rng (w .--> k) c= NAT by XBOOLE_1:8;
  rng CSlv1 c= rng (CSN`1) \/ rng (w .--> k) by FUNCT_4:17;
  then rng CSlv1 c= NAT by A4,XBOOLE_1:1;
  then CSlv1 in PFuncs(the_Vertices_of G, NAT) by A3,PARTFUN1:def 3;
  then reconsider CSlv as MCS:Labeling of G by ZFMISC_1:def 2;
A5: CN1 = MCS:Step(CSN) by Def26
    .= MCS:Update(CSN, w, n) by A1,A2,Def23
    .= MCS:LabelAdjacent(CSlv,w) by Def22;
  take w;
  set V2v = CSlv`2;
  set VLv = CSlv`1;
  set V21 = CN1`2;
  set V2N = CSN`2;
A6: [ CSN`1 +* (w .--> k), CSN`2 ]`1 = CSN`1 +* (w .--> k) &
   [ CSN`1 +* (w .--> k), CSN`2 ]`2 = CSN`2;
A7: V2v = V2N by A6;
  VLv = CSN`1 +* (w .--> k) by A6;
  then
A8: dom VLv = (dom CSN`1) \/ {w} by Lm1;
  then
A9: dom VLN c= dom VLv by XBOOLE_1:7;
A10: now
    let v be set;
    assume
A11: not v in G.AdjacentSet({w}) or v in dom VLN;
    per cases by A11;
    suppose
      not v in G.AdjacentSet({w});
      hence V21.v = V2N.v by A5,A7,Th60;
    end;
    suppose
      v in dom VLN;
      hence V21.v = V2N.v by A5,A7,A9,Th61;
    end;
  end;
A12: dom V2N = the_Vertices_of G by FUNCT_2:def 1;
  now
    let v be set;
    assume that
A13: v in G.AdjacentSet({w}) and
A14: not v in dom VLN;
    not v in {w} by A13,CHORD:49;
    then not v in dom VLv by A8,A14,XBOOLE_0:def 3;
    hence V21.v = V2N.v + 1 by A5,A7,A12,A13,Th62;
  end;
  hence thesis by A10;
end;

theorem Th76:
  for G being finite _Graph, n being Nat, x being set st not x in
dom ((MCS:CSeq(G)).n)`1 holds (((MCS:CSeq(G)).n)`2).x = card (G.AdjacentSet({x}
  ) /\ (dom ((MCS:CSeq(G)).n)`1))
proof
  let G be finite _Graph, n be Nat;
  set CN = (MCS:CSeq(G)).n;
  set VLN = CN`1;
  defpred P[Nat] means for x being set st not x in dom ((MCS:CSeq(G)).$1)`1
holds (((MCS:CSeq(G)).$1)`2).x = card (G.AdjacentSet({x}) /\ (dom ((MCS:CSeq(G)
  ).$1)`1));
A1: for k being Nat st P[k] holds P[k+1]
  proof
    let k be Nat such that
A2: P[k];
    set CS1 = (MCS:CSeq(G)).(k+1);
    set CSK = (MCS:CSeq(G)).k;
    set VLK = CSK`1;
    set VK2 = CSK`2;
    set VL1 = CS1`1;
    set V12 = CS1`2;
A3: k <= k+1 by XREAL_1:38;
    per cases;
    suppose
A4:   G.order() <= k;
      then
A5:   VK2 = V12 by A3,Th67;
      VLK = VL1 by A3,A4,Th67;
      hence thesis by A2,A5;
    end;
    suppose
A6:   k < G.order();
      set VL = (MCS:CSeq(G))``1;
A7:   G.order() = (MCS:CSeq(G)).Lifespan() by Th70;
A8:   VLK = VL.k by Def25;
A9:   (MCS:CSeq(G)).Lifespan() = VL.Lifespan() by Th72;
A10:  VL1 = VL.(k+1) by Def25;
      consider w being Vertex of G such that
A11:  w = MCS:PickUnnumbered(CSK) and
A12:  for v being set holds (v in G.AdjacentSet({w}) & not v in dom
VLK implies V12.v = VK2.v + 1) & (not v in G.AdjacentSet({w}) or v in dom VLK
      implies V12.v = VK2.v) by A6,Th75;
      w = (MCS:CSeq(G)``1).PickedAt(k) by A6,A11,Th74;
      then
A13:  dom CS1`1 = (dom CSK`1) \/ {w} by A6,A7,A8,A10,A9,Th11;
      now
        let x be set such that
A14:    not x in dom VL1;
A15:    not x in dom VLK by A13,A14,XBOOLE_0:def 3;
        then
A16:    card (G.AdjacentSet({x}) /\ dom VLK) = VK2.x by A2;
        per cases;
        suppose
A17:      x in G.AdjacentSet({w}) & not x in dom VLK;
          set GAS = G.AdjacentSet({x});
          w in GAS by A17,CHORD:53;
          then
A18:      {w} c= GAS by ZFMISC_1:31;
A19:      GAS /\ dom VL1 = (GAS /\ dom VLK) \/ (GAS /\ {w}) by A13,XBOOLE_1:23
            .= (GAS /\ dom VLK) \/ {w} by A18,XBOOLE_1:28;
          dom VLK <> the_Vertices_of G by A6,Th69;
          then not w in dom VLK by A11,Th59;
          then
A20:      not w in GAS /\ dom VLK by XBOOLE_0:def 4;
          V12.x = VK2.x + 1 by A12,A17;
          hence card (G.AdjacentSet({x}) /\ dom VL1) = V12.x by A16,A20,A19,
CARD_2:41;
        end;
        suppose
A21:      not x in G.AdjacentSet({w}) or x in dom VLK;
          set GAS = G.AdjacentSet({x});
A22:      not w in GAS by A13,A14,A21,CHORD:53,XBOOLE_0:def 3;
A23:      now
            assume GAS /\ {w} = {w};
            then w in GAS /\ {w} by TARSKI:def 1;
            hence contradiction by A22,XBOOLE_0:def 4;
          end;
          GAS /\ {w} c= {w} by XBOOLE_1:17;
          then GAS /\ {w} in bool {w};
          then
A24:      GAS /\ {w} in { {}, {w} } by ZFMISC_1:24;
A25:      V12.x = VK2.x by A12,A21;
          GAS /\ dom VL1 = (GAS /\ dom VLK) \/ (GAS /\ {w}) by A13,XBOOLE_1:23
            .= (GAS /\ dom VLK) \/ {} by A24,A23,TARSKI:def 2
            .= GAS /\ dom VLK;
          hence card (G.AdjacentSet({x}) /\ dom VL1) = V12.x by A2,A15,A25;
        end;
      end;
      hence thesis;
    end;
  end;
  now
    set C0 = (MCS:CSeq(G)).0;
    let x be set;
    set VL0 = C0`1;
    set V20 = C0`2;
    assume not x in dom VL0;
A26: C0 = MCS:Init(G) by Def26;
    [ {}, the_Vertices_of G --> 0 ]`1 = {};
    then dom VL0 = {} by A26;
    hence V20.x = card (G.AdjacentSet({x}) /\ dom VL0) by A26,Th57,CARD_1:27;
  end;
  then
A27: P[ 0 ];
A28: for k being Nat holds P[k] from NAT_1:sch 2(A27,A1);
  let x be set;
  assume not x in dom VLN;
  hence thesis by A28;
end;

definition
  let G be _Graph, F be PartFunc of the_Vertices_of G, NAT;
  attr F is with_property_T means
  :Def27:
  for a,b,c being Vertex of G st a in
  dom F & b in dom F & c in dom F & F.a < F.b & F.b < F.c & a,c are_adjacent &
  not b,c are_adjacent ex d being Vertex of G st d in dom F & F.b < F.d & b,d
  are_adjacent & not a,d are_adjacent;
end;

theorem
  for G being finite _Graph, n being Nat holds ((MCS:CSeq(G)).n)`1 is
  with_property_T
proof
  let G be finite _Graph, n be Nat;
  set CN = (MCS:CSeq(G)).n;
  set VLN = CN`1;
  set VL = (MCS:CSeq(G))``1;
  now
A1: (MCS:CSeq(G)).Lifespan() = VL.Lifespan() by Th72;
A2: VLN = VL.n by Def25;
    let a,b,c be Vertex of G such that
A3: a in dom VLN and
A4: b in dom VLN and
A5: c in dom VLN and
A6: VLN.a < VLN.b and
A7: VLN.b < VLN.c and
A8: a,c are_adjacent and
A9: not b,c are_adjacent;
A10: G.order() = (MCS:CSeq(G)).Lifespan() by Th70;
    now
      set bn = G.order() -' VLN.b;
      set CSB = (MCS:CSeq(G)).bn;
      set VLB = CSB`1;
      set VL2 = CSB`2;
      not c in G.AdjacentSet({b}) by A9,CHORD:52;
      then
A11:  not c in (G.AdjacentSet({b}) /\ dom VLB) by XBOOLE_0:def 4;
A12:  b = (MCS:CSeq(G)``1).PickedAt(bn) by A4,A10,A2,A1,Th20;
A13:  c in G.AdjacentSet({a}) by A6,A7,A8,CHORD:52;
A14:  VLB = VL.bn by Def25;
      then not a in dom VLB by A3,A6,A10,A2,A1,Th24;
      then
A15:  VL2.a = card (G.AdjacentSet({a}) /\ dom VLB) by Th76;
      bn < n by A4,A10,A2,A1,Th22;
      then VLB c= VLN by A2,A14,Th17;
      then
A16:  dom VLB c= dom VLN by RELAT_1:11;
      VLN.b <= G.order() by A10,A2,A1,Th15;
      then
A17:  G.order() -' VLN.b = G.order() - VLN.b by XREAL_1:233;
      then VLN.b = G.order() - (G.order() -' VLN.b);
      then
A18:  VLN.b = G.order() -' (G.order() -' VLN.b) by NAT_D:35,XREAL_1:233;
A19:  now
        assume
A20:    a in dom VLB;
        then VLN.b < VLB.a by A10,A1,A14,A18,Th22;
        hence contradiction by A3,A6,A2,A14,A20,Th19;
      end;
A21:  1 <= VLN.b by A4,A2,Th15;
      then
A22:  bn < G.order() by A17,XREAL_1:44;
      then
A23:  dom VLB <> the_Vertices_of G by Th69;
      assume
A24:  for d being Vertex of G st d in dom VLN & VLN.b < VLN.d & b,d
      are_adjacent holds a,d are_adjacent;
      now
        set CSB1 = (MCS:CSeq(G)).(bn+1);
        set VLB1 = CSB1`1;
        let x be set such that
A25:    x in G.AdjacentSet({b}) /\ dom VLB;
        reconsider d = x as Vertex of G by A25;
A26:    x in dom VLB by A25,XBOOLE_0:def 4;
        x in dom VLB by A25,XBOOLE_0:def 4;
        then
A27:    VLN.d = VLB.d by A2,A14,A16,Th19;
A28:    VLB1 = VL.(bn+1) by Def25;
        then b in dom VLB1 by A10,A1,A22,A12,Th11;
        then
A29:    VLN.b = VLB1.b by A4,A2,A28,Th19;
        bn < bn+1 by XREAL_1:39;
        then VLB c= VLB1 by A14,A28,Th17;
        then dom VLB c= dom VLB1 by RELAT_1:11;
        then
A30:    VLB.d = VLB1.d by A14,A26,A28,Th19;
        VLB.d in rng VLB by A26,FUNCT_1:def 3;
        then VLB.d in (Seg G.order()\Seg (G.order()-'bn)) by A10,A1,A14,Th14;
        then G.order() -' bn < VLB1.d by A30,Th3;
        then
A31:    VLN.b < VLN.d by A10,A1,A17,A21,A12,A28,A29,A27,A30,Th12,XREAL_1:44;
        d in G.AdjacentSet({b}) by A25,XBOOLE_0:def 4;
        then b,d are_adjacent by CHORD:52;
        then a,d are_adjacent by A24,A16,A26,A31;
        then d in G.AdjacentSet({a}) by A6,A31,CHORD:52;
        hence x in G.AdjacentSet({a}) /\ dom VLB by A26,XBOOLE_0:def 4;
      end;
      then
A32:  (G.AdjacentSet({b}) /\ dom VLB) c= (G.AdjacentSet({a}) /\ dom VLB)
      by TARSKI:def 3;
      c in dom VLB by A4,A5,A7,A10,A2,A1,A14,Th23;
      then c in (G.AdjacentSet({a}) /\ dom VLB) by A13,XBOOLE_0:def 4;
      then
A33:  (G.AdjacentSet({b}) /\ dom VLB) c< (G.AdjacentSet({a}) /\ dom VLB)
      by A11,A32,XBOOLE_0:def 8;
A34:  b = MCS:PickUnnumbered(CSB) by A17,A21,A12,Th74,XREAL_1:44;
      then VL2.b = card (G.AdjacentSet({b}) /\ dom VLB) by A23,Th59,Th76;
      hence contradiction by A23,A34,A19,A15,A33,Th58,TREES_1:6;
    end;
    hence ex d being Vertex of G st d in dom VLN & VLN.b < VLN.d & b,d
    are_adjacent & not a,d are_adjacent;
  end;
  hence thesis by Def27;
end;

theorem
  for G being finite _Graph holds ((LexBFS:CSeq(G)).Result())`1 is
  with_property_T
proof
  let G be finite _Graph;
  set CS = LexBFS:CSeq(G);
  set L = (CS.Result())`1;
A1: L is with_property_L3 by Th53;
  now
    let a,b,c be Vertex of G such that
A2: a in dom L and
A3: b in dom L and
A4: c in dom L and
A5: L.a < L.b and
A6: L.b < L.c and
A7: a,c are_adjacent and
A8: not b,c are_adjacent;
    consider d being Vertex of G such that
A9: d in dom L and
A10: L.c < L.d and
A11: b,d are_adjacent and
A12: not a,d are_adjacent and
    for e being Vertex of G st e <> d & e,b are_adjacent & not e,a
    are_adjacent holds L.e < L.d by A1,A2,A3,A4,A5,A6,A7,A8,Def18;
    take d;
    thus d in dom L by A9;
    thus L.b < L.d by A6,A10,XXREAL_0:2;
    thus b,d are_adjacent by A11;
    thus not a,d are_adjacent by A12;
  end;
  hence thesis by Def27;
end;

theorem :: Tarjan (SIAM Journal of Computing; 13(3):August 1984)
  for G being finite chordal _Graph, L being PartFunc of the_Vertices_of
  G, NAT st L is with_property_T & dom L = the_Vertices_of G for V being
  VertexScheme of G st V" = L holds V is perfect
proof
  let G be finite chordal _Graph, L be PartFunc of the_Vertices_of G, NAT such
  that
A1: L is with_property_T and
A2: dom L = the_Vertices_of G;
  defpred Q[Path of G] means len $1 >= 5 & $1 is open & $1 is chordless & L.(
$1.first()) > L.($1.last()) & L.($1.last()) > L.($1.3) & ex i being odd Element
of NAT st 1 < i & i < len $1 & (for j,k being odd Element of NAT st i <= j & j
  < k & k <= len $1 holds L.($1.j) < L.($1.k)) & (for j,k being odd Element of
  NAT st 1 <= j & j < k & k <= i holds L.($1.j) > L.($1.k));
  let V be VertexScheme of G such that
A3: V" = L;
A4: V is one-to-one by CHORD:def 12;
  len V = card the_Vertices_of G by CHORD:104;
  then dom V = Seg G.order() by FINSEQ_1:def 3;
  then
A5: rng L = Seg G.order() by A3,A4,FUNCT_1:33;
A6: now
    defpred M[Nat] means ex P being Path of G st Q[P] & L.(P.last()) = $1;
A7: for k being Nat st M[k] holds k <= G.order()
    proof
      let k be Nat;
      assume M[k];
      then consider P being Path of G such that
      Q[P] and
A8:   L.(P.last()) = k;
      L.(P.last()) in Seg G.order() by A2,A5,FUNCT_1:def 3;
      hence thesis by A8,FINSEQ_1:1;
    end;
    let R being Path of G;
    assume Q[R];
    then
A9: ex k being Nat st M[k];
    consider k being Nat such that
A10: M[k] and
A11: for n being Nat st M[n] holds n <= k from NAT_1:sch 6(A7,A9);
    consider P being Path of G such that
A12: Q[P] and
A13: L.(P.last()) = k by A10;
    3 <= len P by A12,XXREAL_0:2;
    then P.3 = P.vertexAt(2*1+1) by GLIB_001:def 8;
    then reconsider a = P.3 as Vertex of G;
A14: 3 < len P by A12,XXREAL_0:2;
    reconsider b = P.last() as Vertex of G;
    reconsider c = P.first() as Vertex of G;
A15: now
      2*0+1 < len P by A12,XXREAL_0:2;
      then
A16:  (ex e being set st e Joins P.1,P.(len P),G) iff 1+2=len P by A12,CHORD:92
;
      let e be set;
      assume e Joins c,b,G;
      hence contradiction by A12,A16;
    end;
    then
A17: not b,c are_adjacent by CHORD:def 3;
    2*0+1 < 2*1+1;
    then ex ez being set st ez Joins P.1,P.3,G by A12,A14,CHORD:92;
    then c,a are_adjacent by CHORD:def 3;
    then consider d being Vertex of G such that
    d in dom L and
A18: L.b < L.d and
A19: b,d are_adjacent and
A20: not a,d are_adjacent by A1,A2,A12,A17,Def27;
A21: L.d <> L.c by A2,A3,A4,A17,A19,FUNCT_1:def 4;
    consider i being odd Element of NAT such that
A22: 1 < i and
    i < len P and
A23: for j,k being odd Element of NAT st i <= j & j < k & k <= len P
    holds L.(P.j) < L.(P.k) and
A24: for j,k being odd Element of NAT st 1 <= j & j < k & k <= i holds
    L.(P.j) > L.(P.k) by A12;
A25: L.a < L.d by A12,A18,XXREAL_0:2;
A26: now
      assume d in P.vertices();
      then consider dn being odd Element of NAT such that
A27:  dn <= len P and
A28:  P.dn = d by GLIB_001:87;
A29:  1 <= dn by CHORD:2;
      dn <> 1 by A15,A19,A28,CHORD:def 3;
      then 2*0+1 < dn by A29,XXREAL_0:1;
      then 1+2 <= dn by CHORD:4;
      then
A30:  2*1+1 < dn by A12,A18,A28,XXREAL_0:1;
A31:  dn < len P by A18,A27,A28,XXREAL_0:1;
      per cases;
      suppose
        i <= dn;
        hence contradiction by A23,A18,A28,A31;
      end;
      suppose
        dn < i;
        hence contradiction by A24,A25,A28,A30;
      end;
    end;
    defpred Mi[Nat] means $1 is odd & 3 < $1 & $1 <= len P & ex e being set st
    e Joins P.$1,d,G;
    ex el being set st el Joins P.last(),d,G by A19,CHORD:def 3;
    then
A32: ex k being Nat st Mi[k] by A14;
    ex j being Nat st Mi[j] & for n being Nat st Mi[n] holds j <= n from
    NAT_1:sch 5(A32);
    then consider j being Nat such that
A33: j is odd and
A34: 3 < j and
A35: j <= len P and
A36: ex e being set st e Joins P.j,d,G and
A37: for i being Nat st Mi[i] holds j <= i;
    reconsider j as odd Element of NAT by A33,ORDINAL1:def 12;
    reconsider C = P.cut(1,j) as Path of G;
    consider e being set such that
A38: e Joins P.j,d,G by A36;
    2*0+1 < j by A34,XXREAL_0:2;
    then
A39: C is open chordless by A12,A35,CHORD:93;
A40: 2*0+1 <= j by CHORD:2;
    then
A41: len C + 1 = j + 1 by A35,GLIB_001:36;
A42: now
      let n be odd Element of NAT such that
A43:  n <= j;
      1 <= n by CHORD:2;
      then n in dom C by A41,A43,FINSEQ_3:25;
      then C.n = P.(1 + n - 1) by A35,A40,GLIB_001:47;
      hence C.n = P.n;
    end;
    2*1+1 < j by A34;
    then
A44: C.3 = a by A42;
A45: now
      len C > 2*1+1 by A34,A41;
      then
A46:  len C >= 3+2 by CHORD:4;
      let f be set such that
A47:  f Joins C.(len C-2),d,G;
      len C <> 5 by A20,A44,A47,CHORD:def 3;
      then len C > 5 by A46,XXREAL_0:1;
      then
A48:  3+2-2 < len C-2 by XREAL_1:9;
      then 0 < len C-2*1;
      then reconsider cc = len C - 2 as odd Element of NAT by INT_1:3;
A49:  cc < len C by XREAL_1:44;
      then
A50:  cc < len P by A35,A41,XXREAL_0:2;
      f Joins P.cc,d,G by A41,A42,A47,A49;
      hence contradiction by A37,A41,A48,A49,A50;
    end;
A51: e Joins C.last(),d,G by A35,A38,A40,GLIB_001:37;
    C.vertices() c= P.vertices() by A35,A40,GLIB_001:94;
    then
A52: not d in C.vertices() by A26;
    then reconsider D = C.addEdge(e) as Path of G by A51,A39,A45,CHORD:97;
    reconsider R = D.reverse() as Path of G;
A53: C.last() = P.j by A35,A40,GLIB_001:37;
    then
A54: len D = len C + 2 by A38,GLIB_001:64;
A55: now
      per cases;
      suppose
A56:    i < j;
        now
          per cases by A35,XXREAL_0:1;
          suppose
            j = len P;
            hence L.(P.j) <= L.b;
          end;
          suppose
            j < len P;
            hence L.(P.j) <= L.b by A23,A56;
          end;
        end;
        hence L.(P.j) < L.c by A12,XXREAL_0:2;
      end;
      suppose
A57:    i >= j;
        1 < 2*1+1;
        then L.(P.j) < L.(P.3) by A24,A34,A57;
        then L.(P.j) < L.b by A12,XXREAL_0:2;
        hence L.(P.j) < L.c by A12,XXREAL_0:2;
      end;
    end;
    C.first() = P.first() by A35,A40,GLIB_001:37;
    then
A58: D.first() = c by A38,A53,GLIB_001:63;
    then
A59: R.last() = c by GLIB_001:22;
    3 in dom C by A34,A41,FINSEQ_3:25;
    then
A60: D.3 = a by A38,A53,A44,GLIB_001:65;
A61: D is chordless by A52,A51,A39,A45,CHORD:97;
A62: D.last() = d by A38,A53,GLIB_001:63;
    then
A63: R.first() = d by GLIB_001:22;
A64: for n being odd Element of NAT st n <= len R holds R.n = D.(len D -
    n + 1) & len D - n + 1 is Element of NAT
    proof
      let n be odd Element of NAT such that
A65:  n <= len R;
      1 <= n by CHORD:2;
      then
A66:  n in dom R by A65,FINSEQ_3:25;
      hence R.n = D.(len D - n + 1) by GLIB_001:25;
      len D - n + 1 in dom D by A66,GLIB_001:25;
      hence thesis;
    end;
A67: now
      let n be odd Nat such that
A68:  n <= j;
      1 <= n by CHORD:2;
      then n in dom C by A41,A68,FINSEQ_3:25;
      hence C.n = D.n by A51,GLIB_001:65;
    end;
A69: ex i being odd Element of NAT st 1 < i & i < len D & (for j,k being
odd Element of NAT st i <= j & j < k & k <= len D holds L.(D.j) < L.(D.k)) &
for j,k being odd Element of NAT st 1 <= j & j < k & k <= i holds L.(D.j) > L.(
    D.k)
    proof
      per cases;
      suppose
A70:    j <= i;
A71:    now
          1 < 2*1+1;
          then
A72:      L.(P.3) > L.(P.j) by A24,A34,A70;
          let e,f be odd Element of NAT such that
A73:      j <= e and
A74:      e < f and
A75:      f <= len D;
          e < j + 2*1 by A41,A54,A74,A75,XXREAL_0:2;
          then e <= j + 2 - 2 by CHORD:3;
          then
A76:      e = j by A73,XXREAL_0:1;
          then D.e = C.j by A67;
          then
A77:      D.e = P.j by A42;
          len C + 2 <= f by A41,A74,A76,CHORD:4;
          then D.f = d by A54,A62,A75,XXREAL_0:1;
          hence L.(D.e) < L.(D.f) by A25,A77,A72,XXREAL_0:2;
        end;
        take j;
        now
          let e,f be odd Element of NAT such that
A78:      1 <= e and
A79:      e < f and
A80:      f <= j;
          D.e = C.e by A67,A79,A80,XXREAL_0:2;
          then
A81:      D.e = P.e by A42,A79,A80,XXREAL_0:2;
          D.f = C.f by A67,A80;
          then
A82:      D.f = P.f by A42,A80;
          f <= i by A70,A80,XXREAL_0:2;
          hence L.(D.e) > L.(D.f) by A24,A78,A79,A81,A82;
        end;
        hence thesis by A34,A41,A54,A71,XREAL_1:29,XXREAL_0:2;
      end;
      suppose
A83:    i < j;
        take i;
A84:    now
          let e,f be odd Element of NAT such that
A85:      i <= e and
A86:      e < f and
A87:      f <= len D;
          e < j + 2*1 by A41,A54,A86,A87,XXREAL_0:2;
          then
A88:      e <= j + 2 - 2 by CHORD:3;
          then
A89:      e <= len P by A35,XXREAL_0:2;
A90:      D.e = C.e by A67,A88;
          then
A91:      D.e = P.e by A42,A88;
          per cases by A87,XXREAL_0:1;
          suppose
A92:        f = len D;
            now
              per cases by A89,XXREAL_0:1;
              suppose
                e = len P;
                hence L.(D.e) <= L.b by A42,A88,A90;
              end;
              suppose
                e < len P;
                hence L.(D.e) <= L.b by A23,A85,A91;
              end;
            end;
            hence L.(D.e) < L.(D.f) by A18,A62,A92,XXREAL_0:2;
          end;
          suppose
            f < len D;
            then
A93:        f <= j + 2 - 2 by A41,A54,CHORD:3;
            then D.f = C.f by A67;
            then
A94:        D.f = P.f by A42,A93;
            f <= len P by A35,A93,XXREAL_0:2;
            hence L.(D.e) < L.(D.f) by A23,A85,A86,A91,A94;
          end;
        end;
A95:    now
          let e,f be odd Element of NAT such that
A96:      1 <= e and
A97:      e < f and
A98:      f <= i;
          D.f = C.f by A67,A83,A98,XXREAL_0:2;
          then
A99:      D.f = P.f by A42,A83,A98,XXREAL_0:2;
A100:     e <= i by A97,A98,XXREAL_0:2;
          then D.e = C.e by A67,A83,XXREAL_0:2;
          then D.e = P.e by A42,A83,A100,XXREAL_0:2;
          hence L.(D.e) > L.(D.f) by A24,A96,A97,A98,A99;
        end;
        len D > j by A41,A54,XREAL_1:29;
        hence thesis by A22,A83,A84,A95,XXREAL_0:2;
      end;
    end;
A101: ex i being odd Element of NAT st 1 < i & i < len R & (for j,k being
odd Element of NAT st i <= j & j < k & k <= len R holds L.(R.j) < L.(R.k)) &
for j,k being odd Element of NAT st 1 <= j & j < k & k <= i holds L.(R.j) > L.(
    R.k)
    proof
      consider i being odd Element of NAT such that
A102: 1 < i and
A103: i < len D and
A104: for j,k being odd Element of NAT st i <= j & j < k & k <= len
      D holds L.(D.j) < L.(D.k) and
A105: for j,k being odd Element of NAT st 1 <= j & j < k & k <= i
      holds L.(D.j) > L.(D.k) by A69;
      set ir = len D - i + 1;
      len D - 1 > len D - i by A102,XREAL_1:15;
      then
A106: len D - 1 + 1 > len D - i + 1 by XREAL_1:8;
      then
A107: ir < len R by GLIB_001:21;
A108: len D - len D < len D - i by A103,XREAL_1:15;
      then reconsider ir as odd Element of NAT by INT_1:3;
A109: now
        let ja,k be odd Element of NAT such that
A110:   1 <= ja and
A111:   ja < k and
A112:   k <= ir;
        set jr = len D - ja + 1;
A113:   k <= len R by A107,A112,XXREAL_0:2;
        then
A114:   ja <= len R by A111,XXREAL_0:2;
        then
A115:   R.ja = D.jr by A64;
        i + k <= len D - i + 1 + i by A112,XREAL_1:7;
        then
A116:   i + k - k <= len D + 1 - k by XREAL_1:9;
        set kr = len D - k + 1;
A117:   kr < jr by A111,Lm3;
        reconsider jr as odd Element of NAT by A64,A114;
        reconsider kr as odd Element of NAT by A64,A113;
        len D - ja <= len D - 1 by A110,XREAL_1:10;
        then jr <= len D - 1 + 1 by XREAL_1:7;
        then L.(D.kr) < L.(D.jr) by A104,A116,A117;
        hence L.(R.ja) > L.(R.k) by A64,A113,A115;
      end;
      take ir;
A118: now
        let j,k be odd Element of NAT such that
A119:   ir <= j and
A120:   j < k and
A121:   k <= len R;
        set kr = len D - k + 1;
A122:   R.k = D.kr by A64,A121;
        set jr = len D - j + 1;
A123:   j <= len R by A120,A121,XXREAL_0:2;
        then
A124:   R.j = D.jr by A64;
        reconsider kr as odd Element of NAT by A64,A121;
        i + j >= len D - i + 1 + i by A119,XREAL_1:7;
        then
A125:   i + j - j >= len D + 1 - j by XREAL_1:9;
        reconsider jr as odd Element of NAT by A64,A123;
        kr < jr by A120,Lm3;
        hence L.(R.j) < L.(R.k) by A105,A124,A122,A125,CHORD:2;
      end;
      0 + 1 < len D - i + 1 by A108,XREAL_1:8;
      hence thesis by A106,A118,A109,GLIB_001:21;
    end;
A126: len D >= 3+2 by A34,A41,A54,XREAL_1:7;
    then
A127: len R >= 3+2 by GLIB_001:21;
    then 3 <= len R by XXREAL_0:2;
    then 3 in dom R by FINSEQ_3:25;
    then R.3 = D.(len D - 3 + 1) by GLIB_001:25;
    then R.3 = C.j by A41,A54,A67;
    then
A128: L.(R.last()) > L.(R.3) by A42,A59,A55;
    d <> c by A15,A19,CHORD:def 3;
    then
A129: R is open by A63,A59,GLIB_001:def 24;
    D is open by A52,A51,A39,A45,CHORD:97;
    then L.c <= L.d by A11,A13,A18,A25,A61,A126,A58,A62,A60,A69;
    then
A130: L.c < L.d by A21,XXREAL_0:1;
    R is chordless by A61,CHORD:91;
    hence contradiction by A11,A12,A13,A130,A63,A59,A129,A127,A128,A101;
  end;
A131: L" = V by A3,A4,FUNCT_1:43;
  now
    let a,b,c be Vertex of G such that
A132: b<>c and
A133: a,b are_adjacent and
A134: a,c are_adjacent;
    let va,vb,vc be Nat such that
A135: va in dom V and
A136: vb in dom V and
A137: vc in dom V and
A138: V.va = a and
A139: V.vb = b and
A140: V.vc = c and
A141: va < vb and
A142: va < vc;
A143: L.a = va by A3,A4,A135,A138,FUNCT_1:34;
A144: c = V.(L.c) by A2,A3,A4,A131,FUNCT_1:34;
A145: b = V.(L.b) by A2,A3,A4,A131,FUNCT_1:34;
    assume
A146: not b,c are_adjacent;
A147: L.b = vb by A3,A4,A136,A139,FUNCT_1:34;
A148: L.c = vc by A3,A4,A137,A140,FUNCT_1:34;
    per cases by A132,A145,A144,XXREAL_0:1;
    suppose
A149: L.b < L.c;
A150: 2*1+1 is odd;
      consider P being Path of G, e1, e2 being set such that
A151: P is open and
A152: len P = 5 and
      P.length() = 2 and
      e1 Joins c,a,G and
      e2 Joins a,b,G and
      P.edges() = {e1,e2} and
      P.vertices() = {c,a,b} and
A153: P.1 = c and
A154: P.3 = a and
A155: P.5 = b by A132,A133,A134,A141,A142,A143,A147,A148,CHORD:47;
A156: P.first() = c by A153;
A157: now
        let j,k be odd Element of NAT such that
        1 <= j and
A158:   j < k and
A159:   k <= 3;
        j < 3 by A158,A159,XXREAL_0:2;
        then j = 1 by CHORD:7,XXREAL_0:2;
        hence L.(P.j) > L.(P.k) by A142,A143,A148,A153,A154,A158,A159,CHORD:7
,XXREAL_0:2;
      end;
A160: now
        let j,k be odd Element of NAT such that
A161:   3 <= j and
A162:   j < k and
A163:   k <= len P;
        j < 5 by A152,A162,A163,XXREAL_0:2;
        then j = 1 or j = 3 or j = 5 by CHORD:8,XXREAL_0:2;
        hence
        L.(P.j) < L.(P.k) by A141,A142,A143,A147,A148,A152,A153,A154,A155,A161
,A162,A163,CHORD:8,XXREAL_0:2;
      end;
      P.last() = b by A152,A155;
      then Q[P] by A146,A149,A151,A152,A156,A160,A157,A150,CHORD:90;
      hence contradiction by A6;
    end;
    suppose
A164: L.c < L.b;
A165: 2*1+1 is odd;
      consider P being Path of G, e1, e2 being set such that
A166: P is open and
A167: len P = 5 and
      P.length() = 2 and
      e1 Joins b,a,G and
      e2 Joins a,c,G and
      P.edges() = {e1,e2} and
      P.vertices() = {b,a,c} and
A168: P.1 = b and
A169: P.3 = a and
A170: P.5 = c by A132,A133,A134,A141,A142,A143,A147,A148,CHORD:47;
A171: P.first() = b by A168;
A172: now
        let j,k be odd Element of NAT such that
        1 <= j and
A173:   j < k and
A174:   k <= 3;
        j < 3 by A173,A174,XXREAL_0:2;
        then j = 1 by CHORD:7,XXREAL_0:2;
        hence L.(P.j) > L.(P.k) by A141,A143,A147,A168,A169,A173,A174,CHORD:7
,XXREAL_0:2;
      end;
A175: now
        let j,k be odd Element of NAT such that
A176:   3 <= j and
A177:   j < k and
A178:   k <= len P;
        j < 5 by A167,A177,A178,XXREAL_0:2;
        then j = 1 or j = 3 or j = 5 by CHORD:8,XXREAL_0:2;
        hence
        L.(P.j) < L.(P.k) by A141,A142,A143,A147,A148,A167,A168,A169,A170,A176
,A177,A178,CHORD:8,XXREAL_0:2;
      end;
      P.last() = c by A167,A170;
      then Q[P] by A146,A164,A166,A167,A171,A175,A172,A165,CHORD:90;
      hence contradiction by A6;
    end;
  end;
  hence thesis by CHORD:109;
end;