## Koda-Ruskey's algorithm

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]

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
*)
```

# Why3 Proof Results for Project "koda_ruskey"

## Theory "koda_ruskey.KodaRuskey_Spec": fully verified

 Obligations Alt-Ergo 2.0.0 CVC4 1.5 VC eq_color 0.00 0.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

 Obligations Alt-Ergo 2.0.0 CVC3 2.4.1 CVC4 1.4 CVC4 1.5 Z3 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.0 0.04 --- --- --- --- inverse_frame2 --- --- --- --- --- induction_ty_lex inverse_frame2.0 0.06 --- --- --- --- VC inverse_any --- --- --- --- --- induction_ty_lex VC inverse_any.0 0.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_exclusive 0.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_inverse 0.26 --- --- 0.35 --- sub_not_nil --- --- --- --- --- induction_pr sub_not_nil.0 --- --- --- 0.03 --- sub_not_nil.1 --- --- 0.02 0.02 0.95 sub_not_nil.2 --- --- 0.01 0.03 --- sub_empty --- --- --- --- --- induction_pr sub_empty.0 --- --- --- 0.03 --- sub_empty.1 --- --- 0.03 0.04 --- sub_empty.2 --- --- 0.67 0.10 --- sub_mem --- --- --- --- --- induction_pr sub_mem.0 --- --- --- 0.03 --- sub_mem.1 --- --- --- --- --- simplify_trivial_quantification sub_mem.1.0 --- --- 0.04 0.02 --- sub_mem.2 --- --- 0.02 0.05 --- sub_weaken1 --- --- --- --- --- induction_pr sub_weaken1.0 --- --- 0.04 0.05 --- sub_weaken1.1 --- --- --- 0.04 --- sub_weaken1.2 --- --- 0.88 0.15 --- sub_weaken2 --- --- --- --- --- induction_pr sub_weaken2.0 --- --- 0.05 0.08 --- sub_weaken2.1 --- --- --- 0.04 --- sub_weaken2.2 --- --- 2.36 0.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.03 0.04 --- sub_frame.2 --- --- 0.04 0.08 --- sub_no_rep --- --- --- --- --- induction_pr sub_no_rep.0 --- --- --- 0.04 --- sub_no_rep.1 --- --- 0.13 0.03 --- sub_no_rep.2 --- --- 0.16 0.07 --- sub_no_rep2 --- --- --- --- --- induction_pr sub_no_rep2.0 --- --- --- --- --- split_goal_right sub_no_rep2.0.0 0.01 --- 0.02 --- --- sub_no_rep2.1 --- --- --- --- --- split_goal_right sub_no_rep2.1.0 --- --- 0.04 0.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.0 0.04 --- --- --- --- sub_valid_coloring.0.0.0.1 0.01 --- --- --- --- sub_valid_coloring.0.0.0.2 0.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.0 0.26 --- 0.16 0.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.20 --- sub_Cons_N --- --- --- --- --- induction_pr sub_Cons_N.0 0.01 --- --- 0.04 --- sub_Cons_N.1 0.02 --- 0.13 0.04 --- sub_Cons_N.2 0.05 --- 0.08 0.05 --- white_white --- --- --- 0.04 --- VC sub_valid_coloring_white --- --- --- --- --- split_goal_right VC sub_valid_coloring_white.0 0.01 --- --- 0.04 --- VC sub_valid_coloring_white.1 0.02 --- --- 0.03 --- VC sub_valid_coloring_white.2 0.02 --- --- 0.04 --- VC sub_valid_coloring_white.3 0.01 --- --- 0.02 --- VC sub_valid_coloring_white.4 0.02 --- --- 0.04 --- VC sub_valid_coloring_white.5 0.02 --- --- 0.03 --- VC sub_valid_coloring_white.6 0.02 --- --- 0.04 --- VC sub_valid_coloring_white.7 0.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.07 --- --- --- 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 --- --- --- 7.51 --- count_stack_nonneg --- --- --- --- --- induction_ty_lex count_stack_nonneg.0 --- --- --- 0.07 --- VC stored_trans1 0.39 --- --- --- --- VC stored_trans2 0.39 --- --- --- ---

## Theory "koda_ruskey.KodaRuskey": fully verified

 Obligations Alt-Ergo 2.0.0 CVC4 1.4 CVC4 1.5 Eprover 1.8-001 VC enum --- --- --- --- split_goal_right VC enum.0 0.02 --- 0.04 --- VC enum.1 0.02 --- 0.04 --- VC enum.2 0.02 --- 0.04 --- VC enum.3 0.02 --- 0.08 --- VC enum.4 0.01 --- 0.05 --- VC enum.5 0.04 --- --- --- VC enum.6 0.02 --- 0.08 --- VC enum.7 0.02 --- 0.04 --- VC enum.8 0.00 --- 0.04 --- VC enum.9 0.02 --- 0.06 --- VC enum.10 0.02 --- 0.06 --- VC enum.11 0.01 --- 0.06 --- VC enum.12 0.01 --- 0.04 --- VC enum.13 0.02 --- 0.08 --- VC enum.14 0.03 --- 0.08 --- VC enum.15 0.02 --- 0.04 --- VC enum.16 0.08 --- --- --- VC enum.17 0.54 --- 0.16 --- VC enum.18 0.04 --- 0.18 --- VC enum.19 --- --- --- 0.37 VC enum.20 0.04 --- 0.10 --- VC enum.21 0.02 --- 0.04 --- VC enum.22 0.02 --- 0.04 --- VC enum.23 0.06 --- 0.06 --- VC enum.24 0.02 --- 0.04 --- VC enum.25 0.23 --- 0.08 --- VC enum.26 0.02 --- 0.04 --- VC enum.27 0.71 --- 0.23 --- VC enum.28 --- --- --- 0.35 VC enum.29 0.38 --- 0.42 --- VC enum.30 --- --- 0.48 0.15 VC enum.31 0.07 --- 0.09 --- VC enum.32 0.02 --- 0.07 --- VC enum.33 0.03 --- 0.09 --- VC enum.34 0.02 --- 0.06 --- VC enum.35 0.02 --- 0.06 --- VC enum.36 0.09 --- 0.07 --- VC enum.37 0.02 --- 0.03 --- VC enum.38 --- 0.16 0.10 --- VC enum.39 --- 0.14 0.10 --- VC enum.40 0.34 --- 0.11 --- VC enum.41 0.16 --- 0.06 --- VC enum.42 --- 0.13 0.12 --- VC enum.43 0.01 --- 0.06 --- VC enum.44 --- --- --- 0.57 VC enum.45 --- --- 0.19 --- VC enum.46 --- 0.16 0.18 --- VC enum.47 --- 0.16 0.17 --- VC enum.48 0.02 --- 0.05 --- VC enum.49 0.02 --- 0.05 --- VC enum.50 --- 1.41 0.32 --- VC enum.51 --- --- 0.42 --- VC enum.52 0.02 --- 0.03 --- VC enum.53 0.02 --- 0.05 --- VC enum.54 0.19 --- 0.08 --- VC enum.55 0.03 --- 0.08 --- VC enum.56 0.02 --- 0.04 --- VC enum.57 0.01 --- 0.04 --- VC enum.58 0.03 --- 0.08 --- VC enum.59 0.02 --- 0.04 --- VC enum.60 0.61 --- 0.08 --- VC enum.61 0.02 --- 0.04 --- VC enum.62 --- --- 0.90 --- VC enum.63 --- --- --- 0.39 VC enum.64 0.29 --- 0.13 --- VC enum.65 0.02 --- 0.07 --- VC enum.66 0.82 --- 0.27 --- VC enum.67 3.21 --- 0.40 --- VC enum.68 0.21 --- 0.12 --- VC enum.69 0.02 --- 0.06 --- VC enum.70 0.02 --- 0.07 --- VC enum.71 0.09 --- 0.07 --- VC enum.72 0.01 --- 0.03 --- VC enum.73 --- --- 0.17 --- VC enum.74 --- --- 0.10 --- VC enum.75 0.18 --- 0.10 --- VC enum.76 --- --- 1.15 --- VC enum.77 0.01 --- 0.07 --- VC enum.78 --- --- --- 0.61 VC enum.79 --- 1.14 0.22 --- VC enum.80 --- 0.17 0.16 --- VC enum.81 0.44 0.16 0.17 --- VC enum.82 0.02 --- 0.05 --- VC enum.83 0.02 --- 0.04 --- VC enum.84 --- 1.23 0.17 --- VC enum.85 2.07 1.40 0.39 --- VC enum.86 0.02 --- 0.04 --- VC enum.87 0.02 --- 0.04 --- VC main 0.03 --- --- ---