Wiki Agenda Contact Version française

Koda-Ruskey's algorithm


Authors: Jean-Christophe Filliâtre / Mário Pereira

Topics: Trees

Tools: Why3

see also the index (by topic, by tool, by reference, by year)


Koda-Ruskey's algorithm

Authors: Mário Pereira (Université Paris Sud) Jean-Christophe Filliâtre (CNRS)

module KodaRuskey_Spec

  use map.Map
  use list.List
  use list.Append
  use int.Int

  type color = White | Black

  let eq_color (c1 c2:color) : bool
    ensures { result <-> c1 = c2 }
  = match c1,c2 with
    | White,White | Black,Black -> True
    | _ -> False
    end

  type forest =
    | E
    | N int forest forest

  type coloring = map int color

  function size_forest (f: forest) : int = match f with
    | E -> 0
    | N _ f1 f2 -> 1 + size_forest f1 + size_forest f2
    end

  lemma size_forest_nonneg : forall f.
    size_forest f >= 0

  predicate mem_forest (n: int) (f: forest) = match f with
    | E -> false
    | N i f1 f2 -> i = n || mem_forest n f1 || mem_forest n f2
    end

  predicate between_range_forest (i j: int) (f: forest) =
    forall n. mem_forest n f -> i <= n < j

  predicate disjoint (f1 f2: forest) =
    forall x. mem_forest x f1 -> mem_forest x f2 -> false

  predicate no_repeated_forest (f: forest) = match f with
    | E -> true
    | N i f1 f2 ->
      no_repeated_forest f1 && no_repeated_forest f2 &&
      not (mem_forest i f1) && not (mem_forest i f2) &&
      disjoint f1 f2
    end

  predicate valid_nums_forest (f: forest) (n: int) =
    between_range_forest 0 n f &&
    no_repeated_forest f

  predicate white_forest (f: forest) (c: coloring) = match f with
    | E -> true
    | N i f1 f2 ->
      c[i] = White && white_forest f1 c && white_forest f2 c
  end

  predicate valid_coloring (f: forest) (c: coloring) =
    match f with
    | E -> true
    | N i f1 f2 ->
      valid_coloring f2 c &&
      match c[i] with
      | White -> white_forest f1 c
      | Black -> valid_coloring f1 c
      end
    end

  function count_forest (f: forest) : int = match f with
    | E         -> 1
    | N _ f1 f2 -> (1 + count_forest f1) * count_forest f2
    end

  lemma count_forest_nonneg:
    forall f. count_forest f >= 1

  predicate eq_coloring (n: int) (c1 c2: coloring) =
    forall i. 0 <= i < n -> c1[i] = c2[i]

end

module Lemmas

  use map.Map
  use list.List
  use list.Append
  use int.Int
  use KodaRuskey_Spec

  type stack = list forest

  predicate mem_stack (n: int) (st: stack) = match st with
    | Nil       -> false
    | Cons f tl -> mem_forest n f || mem_stack n tl
    end

  lemma mem_app: forall n st1 [@induction] st2.
    mem_stack n (st1 ++ st2) -> mem_stack n st1 || mem_stack n st2

  function size_stack (st: stack) : int = match st with
    | Nil -> 0
    | Cons f st -> size_forest f + size_stack st
    end

  lemma size_stack_nonneg : forall st.
    size_stack st >= 0

  lemma white_forest_equiv:
    forall f c.
    white_forest f c <-> (forall i. mem_forest i f -> c[i] = White)

  predicate even_forest (f: forest) = match f with
    | E -> false
    | N _ f1 f2 -> not (even_forest f1) || even_forest f2
    end

  predicate final_forest (f: forest) (c: coloring) = match f with
    | E -> true
    | N i f1 f2 ->
      c[i] = Black && final_forest f1 c &&
      if not (even_forest f1) then white_forest f2 c
      else final_forest f2 c
    end

  predicate any_forest (f: forest) (c: coloring) =
    white_forest f c || final_forest f c

  lemma any_forest_frame:
    forall f c1 c2.
    (forall i. mem_forest i f -> c1[i] = c2[i]) ->
    (final_forest f c1 -> final_forest f c2) &&
    (white_forest f c1 -> white_forest f c2)

  predicate unchanged (st: stack) (c1 c2: coloring) =
    forall i. mem_stack i st -> c1[i] = c2[i]

  predicate inverse (st: stack) (c1 c2: coloring) =
    match st with
    | Nil -> true
    | Cons f st' ->
      (white_forest f c1 && final_forest f c2 ||
       final_forest f c1 && white_forest f c2) &&
      if even_forest f then
        unchanged st' c1 c2
      else
        inverse st' c1 c2
    end

  predicate any_stack (st: stack) (c: coloring) = match st with
    | Nil -> true
    | Cons f st -> (white_forest f c || final_forest f c) && any_stack st c
    end

  lemma any_stack_frame:
    forall st c1 c2.
    unchanged st c1 c2 ->
    any_stack st c1 -> any_stack st c2

  lemma inverse_frame:
    forall st c1 c2 c3.
    inverse   st c1 c2 ->
    unchanged st c2 c3 ->
    inverse   st c1 c3

  lemma inverse_frame2:
    forall st c1 c2 c3.
    unchanged st c1 c2 ->
    inverse   st c2 c3 ->
    inverse   st c1 c3

  let lemma inverse_any (st: stack) (c1 c2: coloring)
    requires { any_stack st c1 }
    requires { inverse st c1 c2 }
    ensures  { any_stack st c2 }
  = ()

  lemma inverse_final:
    forall f st c1 c2.
    final_forest f c1 ->
    inverse (Cons f st) c1 c2 ->
    white_forest f c2

  lemma inverse_white:
    forall f st c1 c2.
    white_forest f c1 ->
    inverse (Cons f st) c1 c2 ->
    final_forest f c2

  let lemma white_final_exclusive (f: forest) (c: coloring)
    requires { f <> E }
    ensures  { white_forest f c -> final_forest f c -> false }
  = match f with E -> () | N _ _ _ -> () end

  lemma final_unique:
    forall f c1 c2.
    final_forest f c1 ->
    final_forest f c2 ->
    forall i. mem_forest i f -> c1[i] = c2[i]

  let rec lemma inverse_inverse
    (st: stack) (c1 c2 c3: coloring)
    requires { inverse st c1 c2 }
    requires { inverse st c2 c3 }
    ensures  { unchanged st c1 c3 }
    variant  { st }
  = match st with
    | Nil -> ()
    | Cons E st' -> inverse_inverse st' c1 c2 c3
    | Cons f st' -> if even_forest f then () else inverse_inverse st' c1 c2 c3
    end

  inductive sub stack forest coloring =
  | Sub_reflex:
      forall f, c. sub (Cons f Nil) f c
  | Sub_brother:
      forall st i f1 f2 c.
      sub st f2 c -> sub st (N i f1 f2) c
  | Sub_append:
      forall st i f1 f2 c.
      sub st f1 c -> c[i] = Black ->
      sub (st ++ Cons f2 Nil) (N i f1 f2) c

  lemma sub_not_nil:
    forall st f c. sub st f c -> st <> Nil

  lemma sub_empty:
    forall st f0 c. st <> Nil -> sub (Cons E st) f0 c ->
    sub st f0 c

  lemma sub_mem:
    forall n st f c.
    mem_stack n st -> sub st f c -> mem_forest n f

  lemma sub_weaken1:
    forall st i f1 f2 f0 c.
    sub (Cons (N i f1 f2) st) f0 c ->
    sub (Cons         f2  st) f0 c

  lemma sub_weaken2:
    forall st i f1 f2 f0 c.
    sub (Cons (N i f1 f2) st) f0 c ->
    c[i] = Black ->
    sub (Cons f1 (Cons f2 st)) f0 c

  lemma not_mem_st: forall i f st c.
    not (mem_forest i f) -> sub st f c -> not (mem_stack i st)

  lemma sub_frame:
    forall st f0 c c'.
    no_repeated_forest f0 ->
    (forall i. not (mem_stack i st) -> mem_forest i f0 -> c'[i] = c[i]) ->
    sub st f0 c ->
    sub st f0 c'

  predicate disjoint_stack (f: forest) (st: stack) =
    forall i. mem_forest i f -> mem_stack i st -> false

  lemma sub_no_rep: forall f st' f0 c.
    sub (Cons f st') f0 c ->
    no_repeated_forest f0 ->
    no_repeated_forest f

  lemma sub_no_rep2: forall f st' f0 c.
    sub (Cons f st') f0 c ->
    no_repeated_forest f0 ->
    disjoint_stack f st'

  lemma white_valid: forall f c.
    white_forest f c -> valid_coloring f c

  lemma final_valid: forall f c.
    final_forest f c -> valid_coloring f c

  lemma valid_coloring_frame:
    forall f c1 c2.
    valid_coloring f c1 ->
    (forall i. mem_forest i f -> c2[i] = c1[i]) ->
    valid_coloring f c2

  lemma valid_coloring_set:
    forall f i c.
    valid_coloring f c ->
    not (mem_forest i f) ->
    valid_coloring f c[i <- Black]

  lemma head_and_tail:
    forall f1 f2: 'a, st1 st2: list 'a.
    Cons f1 st1 = st2 ++ Cons f2 Nil ->
    st2 <> Nil ->
    exists st. st1 = st ++ Cons f2 Nil /\ st2 = Cons f1 st

  lemma sub_valid_coloring_f1:
    forall i f1 f2 c i1.
    no_repeated_forest (N i f1 f2) ->
    valid_coloring (N i f1 f2) c ->
    c[i] = Black ->
    mem_forest i1 f1 ->
    valid_coloring f1 c[i1 <- Black] ->
    valid_coloring (N i f1 f2) c[i1 <- Black]

  lemma sub_valid_coloring:
    forall f0 i f1 f2 st c1.
    no_repeated_forest f0 ->
    valid_coloring f0 c1 ->
    sub (Cons (N i f1 f2) st) f0 c1 ->
    valid_coloring f0 c1[i <- Black]

  lemma sub_Cons_N:
    forall f st i f1 f2 c.
    sub (Cons f st) (N i f1 f2) c ->
    f = N i f1 f2 || (exists st'. sub (Cons f st') f1 c) || sub (Cons f st) f2 c

  lemma white_white:
    forall f c i.
    white_forest f c ->
    white_forest f c[i <- White]

  let rec lemma sub_valid_coloring_white
    (f0: forest) (i: int) (f1 f2: forest) (c1: coloring)
    requires { no_repeated_forest f0 }
    requires { valid_coloring f0 c1 }
    requires { white_forest f1 c1 }
    ensures  { forall st. sub (Cons (N i f1 f2) st) f0 c1 ->
               valid_coloring f0 c1[i <- White] }
    variant  { f0 }
  = match f0 with
    | E -> ()
    | N _ f10 f20 ->
       sub_valid_coloring_white f10 i f1 f2 c1;
       sub_valid_coloring_white f20 i f1 f2 c1
    end

  function count_stack (st: stack) : int = match st with
    | Nil        -> 1
    | Cons f st' -> count_forest f * count_stack st'
    end

  lemma count_stack_nonneg:
    forall st. count_stack st >= 1

  use seq.Seq as S

  type visited = S.seq coloring

  predicate stored_solutions
    (f0: forest) (bits: coloring) (st: stack) (v1 v2: visited) =
    let n = size_forest f0 in
    let start = S.length v1 in
    let stop  = S.length v2 in
    stop - start = count_stack st &&
    (forall j. 0 <= j < start ->
      eq_coloring n (S.get v2 j) (S.get v1 j)) &&
    forall j. start <= j < stop ->
      valid_coloring f0 (S.get v2 j) &&
      (forall i. 0 <= i < n -> not (mem_stack i st) ->
        (S.get v2 j)[i] = bits[i]) &&
      forall k. start <= k < stop -> j <> k ->
        not (eq_coloring n (S.get v2 j) (S.get v2 k))

  let lemma stored_trans1
      (f0: forest) (bits1 bits2: coloring) (i: int) (f1 f2: forest) (st: stack)
      (v1 v2 v3: visited)
    requires { valid_nums_forest f0 (size_forest f0) }
    requires { 0 <= i < size_forest f0 }
    requires { forall j. 0 <= j < size_forest f0 ->
               not (mem_stack j (Cons (N i f1 f2) st)) -> bits2[j] = bits1[j] }
    requires { forall j. S.length v1 <= j < S.length v2 ->
               (S.get v2 j)[i] = White }
    requires { forall j. S.length v2 <= j < S.length v3 ->
               (S.get v3 j)[i] = Black }
    requires { stored_solutions f0 bits1 (Cons f2 st) v1 v2 }
    requires { stored_solutions f0 bits2 (Cons f1 (Cons f2 st)) v2 v3 }
    ensures  { stored_solutions f0 bits2 (Cons (N i f1 f2) st) v1 v3 }
  = ()

  let lemma stored_trans2
      (f0: forest) (bits1 bits2: coloring) (i: int) (f1 f2: forest) (st: stack)
      (v1 v2 v3: visited)
    requires { valid_nums_forest f0 (size_forest f0) }
    requires { 0 <= i < size_forest f0 }
    requires { forall j. 0 <= j < size_forest f0 ->
       not (mem_stack j (Cons (N i f1 f2) st)) -> bits2[j] = bits1[j] }
    requires { forall j. S.length v1 <= j < S.length v2 ->
               (S.get v2 j)[i] = Black }
    requires { forall j. S.length v2 <= j < S.length v3 ->
               (S.get v3 j)[i] = White }
    requires { stored_solutions f0 bits1 (Cons f1 (Cons f2 st)) v1 v2 }
    requires { stored_solutions f0 bits2 (Cons f2 st) v2 v3 }
    ensures  { stored_solutions f0 bits2 (Cons (N i f1 f2) st) v1 v3 }
  = ()

end

module KodaRuskey

  use seq.Seq as S
  use list.List
  use KodaRuskey_Spec
  use Lemmas
  use map.Map as M
  use array.Array
  use int.Int
  use ref.Ref

  val ghost map_of_array (a: array 'a) : M.map int 'a
    ensures { result = a.elts }

  val ghost visited: ref visited

  let rec enum (bits: array color) (ghost f0: forest) (st: list forest) : unit
    requires { size_forest f0 = length bits }
    requires { valid_nums_forest f0 (length bits) }
    requires { sub st f0 bits.elts }
    requires { st <> Nil }
    requires { any_stack st bits.elts }
    requires { valid_coloring f0 bits.elts }
    variant  { size_stack st, st }
    ensures  { forall i.
                 not (mem_stack i st) -> bits[i] = (old bits)[i] }
    ensures  { inverse st (old bits).elts bits.elts }
    ensures  { valid_coloring f0 bits.elts }
    ensures  { stored_solutions f0 bits.elts st (old !visited) !visited }
  = match st with
    | Nil ->
        absurd
    | Cons E st' ->
       match st' with
       | Nil ->
           (* that's where we visit the next coloring *)
           assert { valid_coloring f0 bits.elts };
           ghost visited := S.snoc !visited (map_of_array bits);
           ()
       | _ ->
           enum bits f0 st'
       end
    | Cons (N i f1 f2 as f) st' ->
        assert { disjoint_stack f1 st' };
        assert { not (mem_stack i st') };
        let ghost visited1 = !visited in
        if eq_color bits[i] White then begin
          label A in
          enum bits f0 (Cons f2 st');
          assert { sub st f0 bits.elts };
          let ghost bits1 = map_of_array bits in
          let ghost visited2 = !visited in
          label B in
          bits[i] <- Black;
          assert { sub st f0 bits.elts };
          assert { white_forest f1 bits.elts };
          assert { unchanged (Cons f2 st') (bits at B).elts bits.elts};
          assert { inverse (Cons f2 st') (bits at A).elts bits.elts };
          label C in
          enum bits f0 (Cons f1 (Cons f2 st'));
          assert { bits[i] = Black };
          assert { final_forest f1 bits.elts };
          assert { if not (even_forest f1)
                   then inverse (Cons f2 st') (bits at C).elts bits.elts &&
                        white_forest f2 bits.elts
                   else unchanged (Cons f2 st') (bits at C).elts bits.elts &&
                        final_forest f2 bits.elts };
          ghost stored_trans1 f0 bits1 (map_of_array bits)
    i f1 f2 st' visited1 visited2 !visited
        end else begin
          assert { if not (even_forest f1) then white_forest f2 bits.elts
                   else final_forest f2 bits.elts };
          label A in
          enum bits f0 (Cons f1 (Cons f2 st'));
          assert { sub st f0 bits.elts };
          let ghost bits1 = map_of_array bits in
          let ghost visited2 = !visited in
          label B in
          bits[i] <- White;
          assert { unchanged (Cons f1 (Cons f2 st'))
                     (bits at B).elts bits.elts };
          assert { inverse (Cons f1 (Cons f2 st'))
                     (bits at A).elts bits.elts };
          assert { sub st f0 bits.elts };
          assert { if even_forest f1 || even_forest f2
                   then unchanged st' (bits at A).elts bits.elts
                   else inverse st' (bits at A).elts bits.elts };
          enum bits f0 (Cons f2 st');
          assert { bits[i] = White };
          assert { white_forest f  bits.elts };
          ghost stored_trans2 f0 bits1 (map_of_array bits)
    i f1 f2 st' visited1 visited2 !visited
       end
    end

  let main (bits: array color) (f0: forest)
    requires { white_forest f0 bits.elts }
    requires { size_forest f0 = length bits }
    requires { valid_nums_forest f0 (length bits) }
    ensures  { S.length !visited = count_forest f0 }
    ensures  { let n = S.length !visited  in
               forall j. 0 <= j < n ->
                 valid_coloring f0 (S.get !visited j) &&
                 forall k. 0 <= k < n -> j <> k ->
                   not (eq_coloring (length bits)
                         (S.get !visited j) (S.get !visited k)) }
  = visited := S.empty;
    enum bits f0 (Cons f0 Nil)

end

Independently, let's prove that count_forest is indeed the number of colorings.

(* wip
module CountCorrect

  use seq.Seq as S
  use map.Map as M
  use map.Const
  use list.List
  use int.Int
  use KodaRuskey_Spec
  use Lemmas
  use ref.Ref

  predicate id_forest (f: forest) (c1 c2: coloring) =
    forall j. mem_forest j f -> M.get c1 j = M.get c2 j

  (* valid coloring, all white outside of f *)
  predicate solution (f: forest) (c: coloring) =
    valid_coloring f c &&
    forall j. not (mem_forest j f) -> M.get c j = White

  lemma solution_eq:
    forall n f c1 c2.
    valid_nums_forest f n ->
    solution f c1 -> eq_coloring n c1 c2 -> solution f c2

  predicate is_product (i: int) (f1 f2: forest) (c1 c2 r: coloring) =
    solution (N i f1 f2) r &&
    M.get r i = Black &&
    id_forest f1 r c1 &&
    id_forest f2 r c2

  let product (n: int) (i: int) (f1 f2: forest) (c1 c2: coloring) : coloring
    requires { valid_nums_forest (N i f1 f2) n }
    requires { solution f1 c1 }
    requires { solution f2 c2 }
    ensures  { is_product i f1 f2 c1 c2 result }
  = let rec copy (acc: coloring) (f: forest)
      variant { f }
      ensures { forall i. M.get result i =
      	          if mem_forest i f then M.get c2 i else M.get acc i }
    = match f with
      | E -> acc
      | N i2 left2 right2 ->
      	  M.set (copy (copy acc left2) right2) i2 (M.get c2 i2)
      end
    in
    let c = copy c1 f2 in
    M.set c i Black

  lemma solution_product:
    forall n i f1 f2 c1 c2 c.
    valid_nums_forest (N i f1 f2) n ->
    solution f1 c1 -> solution f2 c2 ->
    is_product i f1 f2 c1 c2 c -> solution (N i f1 f2) c

  predicate solutions (n: int) (f: forest) (s: seq coloring) =
     (forall j. 0 <= j < length s -> solution f s[j]) &&
     (* colorings are disjoint *)
     (forall j. 0 <= j < length s ->
      	forall k. 0 <= k < length s -> j <> k ->
	not (eq_coloring n s[j] s[k]))

  let product_all (n: int) (i: int) (f1 f2: forest) (s1 s2: seq coloring)
    : seq coloring
    requires { valid_nums_forest (N i f1 f2) n }
    requires { solutions n f1 s1 }
    requires { solutions n f2 s2 }
    ensures  { solutions n (N i f1 f2) result }
    ensures  { forall j. 0 <= j < length s1 ->
               forall k. 0 <= k < length s2 ->
               is_product i f1 f2 s1[j] s2[k] result[j * length s2 + k] }
    ensures  { length result = length s1 * length s2 }
  = let s = ref empty in
    for j = 0 to length s1 - 1 do
      invariant { length !s = j * length s2 }
      invariant { solutions n (N i f1 f2) !s }
      invariant { forall j' k'. 0 <= j' < j -> 0 <= k' < length s2 ->
                  let c = !s[j' * length s2 + k'] in
                  is_product i f1 f2 s1[j'] s2[k'] c }
      for k = 0 to length s2 - 1 do
        invariant { length !s = j * length s2 + k }
        invariant { solutions n (N i f1 f2) !s }
        invariant { forall j' k'. 0 <= j' < j && 0 <= k' < length s2
                               || j' = j && 0 <= k' < k ->
                    let c = !s[j' * length s2 + k'] in
                    is_product i f1 f2 s1[j'] s2[k'] c }
        let p = product n i f1 f2 s1[j] s2[k] in
        assert { forall l. 0 <= l < length !s ->
                  not (eq_coloring n p !s[l]) };
        s := snoc !s p
      done
    done;
    !s

  lemma solution_white_or_black:
    forall n i f1 f2 c.
    valid_nums_forest (N i f1 f2) n ->
    solution (N i f1 f2) c ->
    match M.get c i with
    | White -> solution f2 c
    | Black -> exists c1 c2. is_product i f1 f2 c1 c2 c &&
                             solution f1 c1 && solution f2 c2
    end

  let rec enum (n: int) (f: forest) : seq coloring
    requires { valid_nums_forest f n }
    ensures  { length result = count_forest f }
    ensures  { solutions n f result }
    ensures  { forall c. solution f c <->
                 exists j. 0 <= j < length result && eq_coloring n c result[j] }
    variant  { f }
  = match f with
    | E ->
        cons (const White) empty
    | N i f1 f2 ->
        let s1 = enum n f1 in
        let s2 = enum n f2 in
        s2 ++ product_all n i f1 f2 s1 s2
   end

end
*)

download ZIP archive

Why3 Proof Results for Project "koda_ruskey"

Theory "koda_ruskey.KodaRuskey_Spec": fully verified

ObligationsAlt-Ergo 1.30CVC4 1.5
VC eq_color0.000.01
size_forest_nonneg------
induction_ty_lex
size_forest_nonneg.0---0.02
count_forest_nonneg------
induction_ty_lex
count_forest_nonneg.0---0.02

Theory "koda_ruskey.Lemmas": fully verified

ObligationsAlt-Ergo 1.30CVC3 2.4.1CVC4 1.4CVC4 1.5Z3 4.5.0
mem_app---------------
induction_ty_lex
mem_app.0---------------
split_goal_right
mem_app.0.0---------0.02---
mem_app.0.1---------0.04---
size_stack_nonneg---------------
induction_ty_lex
size_stack_nonneg.0---------------
split_goal_right
size_stack_nonneg.0.0---------0.01---
size_stack_nonneg.0.1---------0.03---
white_forest_equiv---------------
induction_ty_lex
white_forest_equiv.0---------0.04---
any_forest_frame---------------
induction_ty_lex
any_forest_frame.0---------------
split_goal_right
any_forest_frame.0.0---------0.02---
any_forest_frame.0.1---------0.02---
any_forest_frame.0.2---------0.06---
any_forest_frame.0.3---------0.03---
any_stack_frame---------------
induction_ty_lex
any_stack_frame.0---------------
split_goal_right
any_stack_frame.0.0---------0.02---
any_stack_frame.0.1---------------
introduce_premises
any_stack_frame.0.1.0---------------
compute_in_goal
any_stack_frame.0.1.0.0---------------
split_goal_right
any_stack_frame.0.1.0.0.0---------0.04---
any_stack_frame.0.1.0.0.1---0.06---------
inverse_frame---------------
induction_ty_lex
inverse_frame.00.04------------
inverse_frame2---------------
induction_ty_lex
inverse_frame2.00.06------------
VC inverse_any---------------
induction_ty_lex
VC inverse_any.00.02------0.04---
inverse_final---------------
compute_in_goal
inverse_final.0---------0.04---
inverse_white---------------
compute_in_goal
inverse_white.0---------0.04---
VC white_final_exclusive0.02------0.03---
final_unique---------------
induction_ty_lex
final_unique.0---------------
split_goal_right
final_unique.0.0---------0.02---
final_unique.0.1---------0.04---
VC inverse_inverse0.26------0.35---
sub_not_nil---------------
induction_pr
sub_not_nil.0---------0.03---
sub_not_nil.1------0.020.020.95
sub_not_nil.2------0.010.03---
sub_empty---------------
induction_pr
sub_empty.0---------0.03---
sub_empty.1------0.030.04---
sub_empty.2------0.670.10---
sub_mem---------------
induction_pr
sub_mem.0---------0.03---
sub_mem.1---------------
simplify_trivial_quantification
sub_mem.1.0------0.040.02---
sub_mem.2------0.020.05---
sub_weaken1---------------
induction_pr
sub_weaken1.0------0.040.05---
sub_weaken1.1---------0.04---
sub_weaken1.2------0.880.15---
sub_weaken2---------------
induction_pr
sub_weaken2.0------0.050.08---
sub_weaken2.1---------0.04---
sub_weaken2.2------2.950.34---
not_mem_st---------------
induction_pr
not_mem_st.0---------0.04---
not_mem_st.1---------0.03---
not_mem_st.2---------0.05---
sub_frame---------------
induction_pr
sub_frame.0---------0.03---
sub_frame.1------0.030.04---
sub_frame.2------0.040.08---
sub_no_rep---------------
induction_pr
sub_no_rep.0---------0.04---
sub_no_rep.1------0.130.03---
sub_no_rep.2------0.160.07---
sub_no_rep2---------------
induction_pr
sub_no_rep2.0---------------
split_goal_right
sub_no_rep2.0.00.01---0.02------
sub_no_rep2.1---------------
split_goal_right
sub_no_rep2.1.0------0.040.02---
sub_no_rep2.2------0.63------
white_valid---------------
induction_ty_lex
white_valid.0---------------
split_goal_right
white_valid.0.0---------0.03---
white_valid.0.1---------0.03---
final_valid---------------
induction_ty_lex
final_valid.0---------------
split_goal_right
final_valid.0.0---------0.02---
final_valid.0.1---------0.04---
valid_coloring_frame---------------
induction_ty_lex
valid_coloring_frame.0---------0.08---
valid_coloring_set---------------
induction_ty_lex
valid_coloring_set.0---------0.04---
head_and_tail---------------
induction_ty_lex
head_and_tail.0---------0.04---
sub_valid_coloring_f1---------0.04---
sub_valid_coloring---------------
induction_pr
sub_valid_coloring.0---------------
introduce_premises
sub_valid_coloring.0.0---------------
compute_in_goal
sub_valid_coloring.0.0.0---------------
split_goal_right
sub_valid_coloring.0.0.0.00.04------------
sub_valid_coloring.0.0.0.10.01------------
sub_valid_coloring.0.0.0.20.06------------
sub_valid_coloring.1---------------
introduce_premises
sub_valid_coloring.1.0---------------
simplify_trivial_quantification
sub_valid_coloring.1.0.0---------------
compute_in_goal
sub_valid_coloring.1.0.0.0---------------
split_goal_right
sub_valid_coloring.1.0.0.0.00.26---0.160.14---
sub_valid_coloring.1.0.0.0.1---------0.90---
sub_valid_coloring.1.0.0.0.2---------0.92---
sub_valid_coloring.2---------1.64---
sub_Cons_N---------------
induction_pr
sub_Cons_N.00.01------0.04---
sub_Cons_N.10.02---0.130.04---
sub_Cons_N.20.05---0.080.05---
white_white---------0.04---
VC sub_valid_coloring_white---------------
split_goal_right
VC sub_valid_coloring_white.00.01------0.04---
VC sub_valid_coloring_white.10.02------0.03---
VC sub_valid_coloring_white.20.02------0.04---
VC sub_valid_coloring_white.30.01------0.02---
VC sub_valid_coloring_white.40.02------0.04---
VC sub_valid_coloring_white.50.02------0.03---
VC sub_valid_coloring_white.60.02------0.04---
VC sub_valid_coloring_white.70.01------0.02---
VC sub_valid_coloring_white.8---------------
split_goal_right
VC sub_valid_coloring_white.8.0---------0.05---
VC sub_valid_coloring_white.8.1---------------
introduce_premises
VC sub_valid_coloring_white.8.1.0---------------
destruct_alg f0
VC sub_valid_coloring_white.8.1.0.0---------0.03---
VC sub_valid_coloring_white.8.1.0.1---------------
compute_in_goal
VC sub_valid_coloring_white.8.1.0.1.0---------------
split_goal_right
VC sub_valid_coloring_white.8.1.0.1.0.0---------1.37---
VC sub_valid_coloring_white.8.1.0.1.0.1---2.12---------
remove real,bool,tuple0,unit,tuple2,map,coloring,stack,zero,one,(-),(+),( * ),(<),(-),(>),(<=),(>=),get,set,([<-]),is_nil,length,mem,size_forest,between_range_forest,valid_nums_forest,count_forest,eq_coloring,size_stack,even_forest,final_forest,any_forest,unchanged,inverse,any_stack,disjoint_stack,x2,Assoc,Unit_def_l,Unit_def_r,Inv_def_l,Inv_def_r,Comm,Assoc1,Mul_distr_l,Mul_distr_r,Comm1,Unitary,NonTrivialRing,Refl,Trans,Antisymm,Total,ZeroLessOne,CompatOrderAdd,CompatOrderMult,is_nil_spec,Length_nonnegative,Length_nil,Append_assoc,Append_l_nil,Append_length,mem_append,mem_decomp,size_forest_nonneg,count_forest_nonneg,mem_app,size_stack_nonneg,any_forest_frame,any_stack_frame,inverse_frame,inverse_frame2,inverse_any,inverse_final,inverse_white,white_final_exclusive,final_unique,inverse_inverse,sub_not_nil,sub_empty,sub_weaken1,sub_weaken2,not_mem_st,sub_frame,sub_no_rep2,white_valid,final_valid,valid_coloring_set,head_and_tail,sub_valid_coloring_f1,sub_valid_coloring,white_white,H1,H2,H3
VC sub_valid_coloring_white.8.1.0.1.0.1.0---0.14---0.80---
VC sub_valid_coloring_white.8.1.0.1.0.2---------6.52---
count_stack_nonneg---------------
induction_ty_lex
count_stack_nonneg.0---------0.07---
VC stored_trans10.39------------
VC stored_trans20.39------------

Theory "koda_ruskey.KodaRuskey": fully verified

ObligationsAlt-Ergo 1.30CVC4 1.4CVC4 1.5Eprover 1.8-001
VC enum------------
split_goal_right
VC enum.00.02---0.04---
VC enum.10.02---0.04---
VC enum.20.02---0.04---
VC enum.30.02---0.08---
VC enum.40.01---0.05---
VC enum.50.04---------
VC enum.60.02---0.08---
VC enum.70.02---0.04---
VC enum.80.00---0.04---
VC enum.90.02---0.06---
VC enum.100.02---0.06---
VC enum.110.01---0.06---
VC enum.120.01---0.04---
VC enum.130.02---0.08---
VC enum.140.03---0.08---
VC enum.150.02---0.04---
VC enum.160.08---------
VC enum.170.54---0.16---
VC enum.180.04---0.18---
VC enum.19---------0.37
VC enum.200.04---0.10---
VC enum.210.02---0.04---
VC enum.220.02---0.04---
VC enum.230.06---0.06---
VC enum.240.02---0.04---
VC enum.250.23---0.08---
VC enum.260.02---0.04---
VC enum.271.26---0.23---
VC enum.28---------0.35
VC enum.290.38---0.42---
VC enum.30------0.480.15
VC enum.310.07---0.09---
VC enum.320.02---0.07---
VC enum.330.03---0.09---
VC enum.340.02---0.06---
VC enum.350.02---0.06---
VC enum.360.09---0.07---
VC enum.370.02---0.03---
VC enum.38---0.160.10---
VC enum.39---0.140.10---
VC enum.400.34---0.11---
VC enum.410.16---0.06---
VC enum.42---0.130.12---
VC enum.430.01---0.06---
VC enum.44---------0.57
VC enum.45------0.19---
VC enum.46---0.160.18---
VC enum.47---0.160.17---
VC enum.480.02---0.05---
VC enum.490.02---0.05---
VC enum.50---1.410.32---
VC enum.51------0.42---
VC enum.520.02---0.03---
VC enum.530.02---0.05---
VC enum.540.19---0.08---
VC enum.550.03---0.08---
VC enum.560.02---0.04---
VC enum.570.01---0.04---
VC enum.580.03---0.08---
VC enum.590.02---0.04---
VC enum.600.61---0.08---
VC enum.610.02---0.04---
VC enum.62------0.90---
VC enum.63---------0.39
VC enum.640.29---0.13---
VC enum.650.02---0.07---
VC enum.660.82---0.27---
VC enum.673.21---0.40---
VC enum.680.21---0.12---
VC enum.690.02---0.06---
VC enum.700.02---0.07---
VC enum.710.09---0.07---
VC enum.720.01---0.03---
VC enum.73------0.17---
VC enum.74------0.10---
VC enum.750.18---0.10---
VC enum.76------1.15---
VC enum.770.01---0.07---
VC enum.78---------0.61
VC enum.79---1.140.22---
VC enum.80---0.170.16---
VC enum.810.440.160.17---
VC enum.820.02---0.05---
VC enum.830.02---0.04---
VC enum.84---1.230.17---
VC enum.852.421.400.39---
VC enum.860.02---0.04---
VC enum.870.02---0.04---
VC main0.03---------