Wiki Agenda Contact Version française

VerifyThis 2018: le rouge et le noir

solution to VerifyThis 2018 challenge 2


Authors: Raphaël Rieu-Helft

Topics: Array Data Structure / Algorithms / Mathematics

Tools: Why3

References: VerifyThis @ ETAPS 2018

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


VerifyThis @ ETAPS 2018 competition Challenge 2: Le rouge et le noir

Author: Raphaël Rieu-Helft (LRI, Université Paris Sud)

module ColoredTiles

use int.Int
use set.Fset
use set.FsetComprehension
use seq.Seq

type color = Red | Black

type coloring = seq color

predicate tworedneighbors (c: coloring) (i:int)
  = ((c[i-2] = Red /\ c[i-1] = Red /\ 2 <= i)
     \/ (c[i-1] = Red /\ c[i+1] = Red /\ 1 <= i <= length c - 2)
     \/ (c[i+1] = Red /\ c[i+2] = Red /\ i <= length c - 3))

predicate valid (c:coloring) =
  forall i. 0 <= i < length c -> c[i] = Red -> tworedneighbors c i

function black (n:int) : color = Black
function red (n:int) : color = Red

function colorings0 : set coloring = add (create 0 black) Fset.empty
function colorings1 : set coloring = add (create 1 black) Fset.empty
function colorings2 : set coloring = add (create 2 black) Fset.empty
function colorings3: set coloring =
         add (create 3 red) (add (create 3 black) Fset.empty)

lemma valid_contr:
  forall c i. valid c -> 0 <= i < length c -> not (tworedneighbors c i) -> c[i] = Black

lemma colo_0 : forall c: coloring. length c = 0 ->
      (valid c <-> mem c colorings0 by Seq.(==) c (create 0 black))

lemma colo_1 : forall c: coloring. length c = 1 ->
      (valid c <-> mem c colorings1
                   by c[0] = Black
                   so Seq.(==) c (create 1 black))

lemma colo_2 : forall c: coloring. length c = 2 ->
      (valid c <-> mem c colorings2
                   by c[0] = Black = c[1]
                   so Seq.(==) c (create 2 black)
                   so c = create 2 black)

lemma colo_3 : forall c: coloring. length c = 3 ->
      (valid c <-> mem c colorings3
                   by if c[0] = Black
                      then (c[0]=c[1]=c[2]=Black
                            so c == create 3 black
                            so c = create 3 black)
                      else (c[0]=c[1]=c[2]=Red
                            so c == create 3 red
                            so c = create 3 red))

let lemma valid_split_fb (c:coloring) (k: int)
  requires { 3 <= k < length c }
  requires { forall i. 0 <= i < k -> c[i] = Red }
  requires { valid c[k+1 ..] }
  ensures  { valid c }
= let c' = c[k+1 ..] in
  assert { forall i. k+1 <= i < length c -> c[i] = Red ->
             (tworedneighbors c i
              by c'[i - (k+1)] = Red
              so [@case_split] tworedneighbors c' (i - (k+1))) }

let lemma valid_restrict (c: coloring) (k: int)
  requires { valid c }
  requires { 0 <= k < length c }
  requires { c[k] = Black }
  ensures  { valid c[k+1 ..] }
= ()

(*1st black tile starting at i *)
let rec function first_black_tile (c:coloring) : int
  ensures { 0 <= result <= length c }
  ensures { forall j. 0 <= j < result <= length c
            -> c[j] = Red }
  ensures { result < length c -> c[result] = Black }
  ensures { valid c -> result = 0 \/ 3 <= result }
  variant { length c }
= if Seq.length c = 0 then 0
  else match c[0] with
       | Black -> 0
       | Red ->
           assert { valid c -> c[1]=Red /\ c[2] = Red };
           let r = first_black_tile c[1 ..] in
           assert { forall j. 1 <= j < 1+r
                    -> c[j] = Red
                       by c[1 ..][j-1] = Red };
           1+r end

let rec function addleft (nr:int) (c:coloring) : coloring
  variant { nr }
  ensures { nr >= 0 -> Seq.length result = Seq.length c + nr + 1 }
= if nr <= 0 then cons Black c
  else cons Red (addleft (nr-1) c)

(* add nr red tiles and a black tile to the left of each coloring *)
function mapaddleft (s:set coloring) (nr:int) : set coloring
=  map (addleft nr) s

lemma addleft_fb:
  forall c nr. 0 <= nr -> first_black_tile (addleft nr c) = nr

lemma mapaddleft_fb:
  forall s c nr. 0 <= nr -> mem c (mapaddleft s nr) -> first_black_tile c = nr

predicate reciprocal (f: 'a -> 'b) (g: 'b -> 'a)
  = forall y. g (f y) = y

let lemma bij_image (u: set 'a) (f: 'a -> 'b) (g: 'b -> 'a)
  requires { reciprocal f g }
  ensures  { subset u (map g (map f u)) }
= assert { forall x. mem x u -> mem (f x) (map f u)
                     -> mem (g (f x)) (map g (map f u))
                     -> mem x (map g (map f u)) }

let lemma bij_cardinal (u: set 'a) (f: 'a -> 'b) (g: 'b -> 'a)
  requires { reciprocal f g }
  ensures  { cardinal (map f u) = cardinal u }
= assert { cardinal (map f u) <= cardinal u };
  assert { cardinal (map g (map f u)) <= cardinal (map f u) };
  assert { cardinal u <= cardinal (map g (map f u)) }

function rmleft (nr:int) (c:coloring) : coloring = c[nr+1 ..]

use seq.FreeMonoid

lemma ext: forall c1 c2: coloring. Seq.(==) c1 c2 -> c1 = c2
lemma app_eq: forall c1 c2 c3 c4: coloring. c1 = c2 -> c3 = c4 -> c1 ++ c3 = c2 ++ c4

let rec lemma addleft_result (c:coloring) (nr:int)
  requires { 0 <= nr }
  ensures  { addleft nr c = (Seq.create nr red) ++ (cons Black c) }
  variant  { nr }
= if nr = 0 then assert { addleft nr c = (Seq.create nr red) ++ (cons Black c) }
  else begin
    let cnr = create nr red in
    let cnrm = create (nr - 1) red in
    addleft_result c (nr-1);
    assert { addleft (nr-1) c = cnrm ++ cons Black c };
    assert { cons Red cnrm = cnr
               by Seq.(==) (cons Red cnrm) cnr };
    assert { addleft nr c = cnr ++ cons Black c
             by addleft nr c
                = cons Red (addleft (nr-1) c)
                = cons Red (cnrm ++ cons Black c)
                = (cons Red cnrm) ++ cons Black c
                = cnr ++ cons Black c }
  end

let lemma addleft_bijective (nr:int)
  requires { 0 <= nr }
  ensures  { reciprocal (addleft nr) (rmleft nr) }
= assert { forall c i. 0 <= i < length c -> (rmleft nr (addleft nr c))[i] = c[i] };
  assert { forall c. Seq.(==) (rmleft nr (addleft nr c)) c }

let lemma mapaddleft_card (s: set coloring) (nr: int)
  requires { 0 <= nr }
  ensures  { cardinal (mapaddleft s nr) = cardinal s }
= addleft_bijective nr;
  bij_cardinal s (addleft nr) (rmleft nr)

let lemma addleft_valid (c:coloring) (nr:int)
  requires { nr = 0 \/ 3 <= nr }
  requires { valid c }
  ensures  { valid (addleft nr c) }
= addleft_result c nr;
  if nr = 0 then assert { valid (addleft 0 c) }
  else valid_split_fb (addleft nr c) nr

let lemma mapaddleft_valid (s: set coloring) (nr: int)
  requires { forall c. mem c s -> valid c }
  requires { nr = 0 \/ 3 <= nr }
  ensures  { forall c. mem c (mapaddleft s nr) -> valid c }
= assert { forall c. mem c (mapaddleft s nr) ->
                     valid c
                     by mem c (map (addleft nr) s)
                     so (exists y. mem y s /\ c = addleft nr y) }

let lemma mapaddleft_length (s: set coloring) (nr: int) (l1 l2: int)
  requires { forall c. mem c s -> Seq.length c = l1 }
  requires { 0 <= nr }
  requires { l2 = l1 + nr + 1 }
  ensures  { forall c. mem c (mapaddleft s nr) -> Seq.length c = l2 }
= ()

let rec disjoint_union (s1 s2: set coloring) : set coloring
  requires { forall x. mem x s1 -> not mem x s2 }
  ensures  { result = union s1 s2 }
  ensures  { cardinal result = cardinal s1 + cardinal s2 }
  variant  { cardinal s1 }
= if is_empty s1
  then begin
    assert { union s1 s2 = s2
             by (forall x. mem x (union s1 s2)
                -> mem x s1 \/ mem x s2 -> mem x s2)
             so subset (union s1 s2) s2 };
    s2
  end
  else
    let x = choose s1 in
    let s1' = remove x s1 in
    let s2' = add x s2 in
    let u = disjoint_union s1' s2' in
    assert { u = union s1 s2
             by u = union s1' s2'
             so (forall y. (mem y s2' <-> (mem y s2 \/ y = x)))
             so (forall y. ((mem y s1' \/ y = x) <-> mem y s1))
             so (forall y. mem y u <-> mem y s1' \/ mem y s2'
                       <-> mem y s1' \/ mem y s2 \/ y = x
                       <-> mem y s1 \/ mem y s2
                       <-> mem y (union s1 s2))
             so (forall y. mem y u <-> mem y (union s1 s2))
             so Fset.(==) u (union s1 s2)};
    u

use array.Array

let enum () : (count: array int, ghost sets: array (set coloring))
  ensures { Array.length count = 51 = Array.length sets
            /\ (forall i. 0 <= i <= 50 ->
               (forall c: coloring. Seq.length c = i ->
                          (valid c <-> mem c (sets[i]))))
            /\ (forall i. 0 <= i < 50 ->
                          count[i] = cardinal (sets[i])) }
= let count = Array.make 51 0 in
  let ghost sets : array (set coloring) = Array.make 51 Fset.empty in
  count[0] <- 1;
  sets[0] <- colorings0;
  assert { forall c. ((Seq.length c = 0 /\ valid c) <-> mem c (sets[0])) };
  count[1] <- 1;
  sets[1] <- colorings1;
  assert { forall i c. (i=0 \/ i=1)
           -> ((Seq.length c = i /\ valid c) <-> mem c (sets[i])) };
  count[2] <- 1;
  sets[2] <- colorings2;
  assert { forall i c. (i=0 \/ i=1 \/ i=2)
           -> ((Seq.length c = i /\ valid c) <-> mem c (sets[i])) };
  count[3] <- 2;
  sets[3] <- colorings3;
  assert { sets[3] = colorings3 };
  assert { forall i c. (i=0 \/ i=1 \/ i=2 \/ i = 3)
           -> ((Seq.length c = i /\ valid c) <-> mem c (sets[i])) };
  assert { cardinal colorings3 = 2 };
  for n = 4 to 50 do
    invariant { forall c i. 0 <= i < n -> Seq.length c = i ->
                         valid c -> mem c (sets[i]) }
    invariant { forall c i. 0 <= i < n -> mem c (sets[i]) ->
                         (Seq.length c = i /\ valid c) }
    invariant { forall i. 0 <= i < n ->
                         count[i] = cardinal (sets[i]) }
    label StartLoop in
    (* colorings with first_black_tile = 0 *)
    count[n] <- count[n-1];
    mapaddleft_valid (sets[n-1]) 0;
    sets[n] <- mapaddleft (sets[n-1]) 0;
    assert { forall i. 0 <= i < n -> sets[i] = sets[i] at StartLoop };
    assert { forall i. 0 <= i < n -> count[i] = count[i] at StartLoop };
    assert { forall c. Seq.length c = n -> valid c -> first_black_tile c < 3 ->
                       mem c sets[n]
                       by first_black_tile c = 0
                       so valid c[1 ..]
                       so mem c[1 ..] (sets[n-1])
                       so addleft 0 c[1 ..] = c
                       so mem c (mapaddleft sets[n-1] 0) };
    for k = 3 to n-1 do
      invariant { forall c i. 0 <= i < n -> Seq.length c = i ->
                           valid c -> mem c (sets[i]) }
      invariant { forall c i. 0 <= i < n -> mem c (sets[i]) ->
                             (Seq.length c = i /\ valid c) }
      invariant { forall i. 0 <= i < n ->
                            count[i] = cardinal (sets[i]) }
      invariant { forall c. (mem c (sets[n]) <->
                            (Seq.length c = n /\ valid c
                            /\ first_black_tile c < k)) }
      invariant { count[n] = cardinal (sets[n]) }
      label InnerLoop in
      (* colorings with first_black_tile = k *)
      count[n] <- count [n] + count [n-k-1];
      mapaddleft_length (sets[n-k-1]) k (n-k-1) n;
      mapaddleft_valid  (sets[n-k-1]) k;
      mapaddleft_card   (sets[n-k-1]) k;
      let ghost ns = mapaddleft sets[n-k-1] k in
      assert { forall c. mem c ns -> first_black_tile c = k };
      assert { forall c. Seq.length c = n -> valid c -> first_black_tile c = k
                         -> mem c ns
                         by valid c[k+1 ..]
                         so mem c[k+1 ..] (sets[n-k-1])
                         so let c' = addleft k c[k+1 ..] in
                            ((forall i. 0 <= i < n -> Seq.get c i = Seq.get c' i)
                             by c[k+1 ..] = c'[k+1 ..])
                         so Seq.(==) c' c
                         so c' = c
                         so mem c (mapaddleft sets[n-k-1] k) };
      sets[n] <- disjoint_union (sets[n]) ns;
      assert { forall i. 0 <= i < n -> sets[i] = sets[i] at InnerLoop };
      assert { forall i. 0 <= i < n -> count[i] = count[i] at InnerLoop };
    done;
    (* coloring with first_black_tile = n *)
    label LastAdd in
    let ghost r = Seq.create n red in
    let ghost sr = Fset.singleton r in
    assert { forall c. mem c sets[n] -> first_black_tile c < n };
    assert { first_black_tile r = n };
    assert { valid r /\ Seq.length r = n };
    count[n] <- count[n]+1;
    sets[n] <- disjoint_union (sets[n]) sr;
    assert { forall c. mem c sets[n] -> valid c /\ Seq.length c = n
                       by [@case_split] mem c (sets[n] at LastAdd) \/ mem c sr };
    assert { forall c. Seq.length c = n -> first_black_tile c = n ->
                       mem c sets[n]
                       by (forall k. 0 <= k < n -> Seq.get c k = Red)
                       so c == r so c = r };
    assert { forall i. 0 <= i < n -> sets[i] = sets[i] at LastAdd };
    assert { forall i. 0 <= i < n -> count[i] = count[i] at LastAdd };
  done;
  count, sets

end

download ZIP archive

Why3 Proof Results for Project "verifythis_2018_le_rouge_et_le_noir_1"

Theory "verifythis_2018_le_rouge_et_le_noir_1.ColoredTiles": fully verified

ObligationsAlt-Ergo 1.30Alt-Ergo 2.0.0CVC4 1.4Z3 4.5.0
valid_contr0.01---------
colo_0------------
split_vc
colo_0.0---------0.05
colo_0.1---------0.02
colo_0.2------------
unfold colorings0
colo_0.2.0------------
rewrite add_spec
colo_0.2.0.0---------0.23
colo_1------------
split_vc
colo_1.0---------0.04
colo_1.1---------0.13
colo_1.2---------0.03
colo_1.3------------
unfold colorings1
colo_1.3.0------------
rewrite add_spec
colo_1.3.0.0------------
left
colo_1.3.0.0.0---------0.04
colo_2------------
split_vc
colo_2.0---------0.03
colo_2.1---------0.02
colo_2.2---------0.03
colo_2.3---------0.05
colo_2.4---------0.03
colo_2.5------------
subst colorings2
colo_2.5.0------------
rewrite H
colo_2.5.0.0------------
rewrite add_spec
colo_2.5.0.0.0------------
left
colo_2.5.0.0.0.0---------0.05
colo_3------------
split_vc
colo_3.0---------0.04
colo_3.1---------0.03
colo_3.2---------0.04
colo_3.3---------0.02
colo_3.4---------0.03
colo_3.5---------0.05
colo_3.60.45---------
colo_3.7---------0.06
colo_3.8---------0.05
colo_3.9---------0.08
colo_3.10---------0.05
colo_3.11------------
subst colorings3
colo_3.11.0------------
rewrite add_spec
colo_3.11.0.0------------
eliminate_if
colo_3.11.0.0.0------------
case c[0]=Black
colo_3.11.0.0.0.0------------
right
colo_3.11.0.0.0.0.0------------
rewrite add_spec
colo_3.11.0.0.0.0.0.0------------
left
colo_3.11.0.0.0.0.0.0.0---------0.03
colo_3.11.0.0.0.1------------
left
colo_3.11.0.0.0.1.0---------0.04
VC valid_split_fb------------
split_vc
VC valid_split_fb.0---------0.03
VC valid_split_fb.1------------
split_vc
VC valid_split_fb.1.0---------0.03
VC valid_split_fb.1.1---------0.02
VC valid_split_fb.1.2------0.11---
VC valid_split_fb.20.09---------
VC valid_restrict------------
split_vc
VC valid_restrict.0------------
split_all_full
VC valid_restrict.0.0---------0.18
VC first_black_tile------------
split_vc
VC first_black_tile.0---------0.02
VC first_black_tile.1---------0.04
VC first_black_tile.2---------0.03
VC first_black_tile.3------------
split_vc
VC first_black_tile.3.0---------0.03
VC first_black_tile.3.1---------0.16
VC first_black_tile.40.02---------
VC first_black_tile.50.01---------
VC first_black_tile.60.28---------
VC first_black_tile.70.07---------
VC addleft------------
split_vc
VC addleft.0---------0.01
VC addleft.1---------0.04
addleft_fb------------
introduce_premises
addleft_fb.0------------
induction nr
addleft_fb.0.0---------0.04
addleft_fb.0.1------------
split_all_full
addleft_fb.0.1.0---------0.24
mapaddleft_fb---------0.05
VC bij_image------------
split_vc
VC bij_image.0---------0.04
VC bij_image.1---------0.34
VC bij_cardinal------------
split_vc
VC bij_cardinal.0---------0.03
VC bij_cardinal.1---------0.02
VC bij_cardinal.2---------0.04
VC bij_cardinal.3---------0.02
ext---------0.02
app_eq---------0.04
VC addleft_result------------
split_vc
VC addleft_result.0---------0.03
VC addleft_result.1---------0.01
VC addleft_result.2---------0.02
VC addleft_result.3---------0.02
VC addleft_result.4---------0.02
VC addleft_result.5------------
subst o
VC addleft_result.5.0------------
rewrite H
VC addleft_result.5.0.0------------
subst o1
VC addleft_result.5.0.0.0------------
subst o
VC addleft_result.5.0.0.0.0------------
unfold cnrm
VC addleft_result.5.0.0.0.0.0------------
apply app_eq
VC addleft_result.5.0.0.0.0.0.0---------0.01
VC addleft_result.5.0.0.0.0.0.1------------
apply ext
VC addleft_result.5.0.0.0.0.0.1.00.02---------
VC addleft_result.6------------
split_vc
VC addleft_result.6.00.40---------
VC addleft_result.6.1------------
apply ext
VC addleft_result.6.1.00.01---------
VC addleft_result.7------------
split_vc
VC addleft_result.7.0---------0.03
VC addleft_result.7.1------------
subst o
VC addleft_result.7.1.0------------
rewrite <- H1
VC addleft_result.7.1.0.0---------0.02
VC addleft_result.7.2------------
rewrite cons_def
VC addleft_result.7.2.0------------
rewrite cons_def
VC addleft_result.7.2.0.0------------
rewrite cons_def
VC addleft_result.7.2.0.0.0------------
rewrite associative
VC addleft_result.7.2.0.0.0.0------------
apply app_eq
VC addleft_result.7.2.0.0.0.0.0---------0.02
VC addleft_result.7.2.0.0.0.0.1------------
apply app_eq
VC addleft_result.7.2.0.0.0.0.1.0------------
apply ext
VC addleft_result.7.2.0.0.0.0.1.0.00.02---------
VC addleft_result.7.2.0.0.0.0.1.1---------0.01
VC addleft_result.7.3------------
subst o
VC addleft_result.7.3.0------------
rewrite H
VC addleft_result.7.3.0.0------------
apply app_eq
VC addleft_result.7.3.0.0.0---------0.03
VC addleft_result.7.3.0.0.1------------
apply ext
VC addleft_result.7.3.0.0.1.00.02---------
VC addleft_result.7.4---------0.02
VC addleft_result.8------------
split_all_full
VC addleft_result.8.0------------
case (nr = 0)
VC addleft_result.8.0.0---------0.04
VC addleft_result.8.0.1------------
eliminate_let
VC addleft_result.8.0.1.0------------
apply H
VC addleft_result.8.0.1.0.0---------0.02
VC addleft_bijective------------
split_vc
VC addleft_bijective.00.35---------
VC addleft_bijective.1------------
unfold rmleft
VC addleft_bijective.1.00.04---------
VC addleft_bijective.2---------0.02
VC mapaddleft_card------------
split_vc
VC mapaddleft_card.0---------0.02
VC mapaddleft_card.1---------0.04
VC mapaddleft_card.2---------0.03
VC addleft_valid------------
split_vc
VC addleft_valid.0---------0.02
VC addleft_valid.1------------
split_all_full
VC addleft_valid.1.0------4.16---
VC addleft_valid.2---------0.05
VC addleft_valid.3---------0.04
VC addleft_valid.4---------0.06
VC addleft_valid.5---------0.03
VC mapaddleft_valid------------
introduce_premises
VC mapaddleft_valid.0------------
split_goal_right
VC mapaddleft_valid.0.0------------
split_vc
VC mapaddleft_valid.0.0.0---------0.04
VC mapaddleft_valid.0.0.1---------0.21
VC mapaddleft_valid.0.0.2---------0.02
VC mapaddleft_valid.0.1---------0.01
VC mapaddleft_length------------
introduce_premises
VC mapaddleft_length.0------------
split_goal_right
VC mapaddleft_length.0.00.05---------
VC disjoint_union------------
split_goal_right
VC disjoint_union.0------------
split_vc
VC disjoint_union.0.0---------0.04
VC disjoint_union.0.1---------0.04
VC disjoint_union.0.20.02---------
VC disjoint_union.1---------0.02
VC disjoint_union.2---------0.04
VC disjoint_union.3------------
split_vc
VC disjoint_union.3.0---------0.02
VC disjoint_union.3.1---------0.04
VC disjoint_union.3.2---------0.03
VC disjoint_union.3.3---------0.04
VC disjoint_union.3.4---------0.03
VC disjoint_union.3.5---------0.04
VC disjoint_union.3.6---------0.04
VC disjoint_union.3.7---------0.04
VC disjoint_union.3.8---------0.04
VC disjoint_union.3.9---------0.03
VC disjoint_union.3.10---------0.05
VC disjoint_union.3.11---------0.03
VC disjoint_union.3.12---------0.05
VC disjoint_union.3.13---------0.04
VC disjoint_union.3.14---------0.03
VC disjoint_union.3.150.03---------
VC disjoint_union.3.16---------0.04
VC disjoint_union.4------------
split_all_full
VC disjoint_union.4.0---------0.04
VC disjoint_union.4.1------------
split_all_full
VC disjoint_union.4.1.0---------0.02
VC disjoint_union.4.1.1---------0.02
VC disjoint_union.4.1.2---------0.02
VC disjoint_union.4.1.3---------0.02
VC disjoint_union.50.02---------
VC enum------------
split_vc
VC enum.0---------0.01
VC enum.1---------0.01
VC enum.2---------0.02
VC enum.3---------0.02
VC enum.4---0.20------
VC enum.5---------0.02
VC enum.6---------0.02
VC enum.7------------
split_all_full
VC enum.7.0---0.22------
VC enum.7.1---0.09------
VC enum.7.2---0.56------
VC enum.8---------0.03
VC enum.9---------0.02
VC enum.10------------
case i=3
VC enum.10.0------------
rewrite h
VC enum.10.0.0------------
rewrite H1
VC enum.10.0.0.0------------
split_all_full
VC enum.10.0.0.0.0------------
introduce_premises
VC enum.10.0.0.0.0.0---------0.02
VC enum.10.0.0.0.1---0.02------
VC enum.10.0.0.0.2------------
introduce_premises
VC enum.10.0.0.0.2.0---------0.02
VC enum.10.1------------
split_all_full
VC enum.10.1.0---0.98------
VC enum.10.1.1---0.30------
VC enum.10.1.2---5.52------
VC enum.11---------0.02
VC enum.12---------0.02
VC enum.13------------
assert (forall m:array (set2 coloring), i v. m[i <- v][i] = v)
VC enum.13.0---0.03------
VC enum.13.1------------
subst sets
VC enum.13.1.0------------
subst o
VC enum.13.1.0.0------------
apply h
VC enum.14------------
case i=3
VC enum.14.0------------
rewrite h
VC enum.14.0.0------------
rewrite H1
VC enum.14.0.0.0------------
split_all_full
VC enum.14.0.0.0.0------------
introduce_premises
VC enum.14.0.0.0.0.0------------
apply colo_31
VC enum.14.0.0.0.0.0.0---------0.02
VC enum.14.0.0.0.0.0.1---------0.01
VC enum.14.0.0.0.1---0.22------
VC enum.14.0.0.0.2------------
introduce_premises
VC enum.14.0.0.0.2.0------------
apply colo_3
VC enum.14.0.0.0.2.0.0------------
apply H
VC enum.14.0.0.0.2.0.1---0.26------
VC enum.14.1------------
split_all_full
VC enum.14.1.0---0.21------
VC enum.14.1.1---0.38------
VC enum.14.1.2---0.51------
VC enum.15------------
split_all_full
VC enum.15.0---1.27------
VC enum.16---0.05------
VC enum.17---0.12------
VC enum.18------------
assert (i=0\/i=1\/i=2\/i=3)
VC enum.18.0---0.02---0.05
VC enum.18.1------------
revert h
VC enum.18.1.0------------
split_all_full
VC enum.18.1.0.0---0.22------
VC enum.18.1.0.1---0.26------
VC enum.18.1.0.2---0.24------
VC enum.18.1.0.3------------
introduce_premises
VC enum.18.1.0.3.0------------
replace i 3
VC enum.18.1.0.3.0.0------------
replace sets[3] colorings3
VC enum.18.1.0.3.0.0.0------------
rewrite H7
VC enum.18.1.0.3.0.0.0.0---0.04------
VC enum.18.1.0.3.0.0.1------------
apply H20
VC enum.18.1.0.3.0.1---------0.02
VC enum.19---------0.02
VC enum.20---------0.02
VC enum.21---------0.03
VC enum.22---------0.03
VC enum.23---------0.02
VC enum.24---------0.05
VC enum.25---------0.03
VC enum.26---0.02------
VC enum.27---0.11------
VC enum.28------------
split_vc
VC enum.28.0---------0.03
VC enum.28.1------0.25---
VC enum.28.2---0.19------
VC enum.28.3---------0.13
VC enum.28.4---------0.08
VC enum.28.5---0.03------
VC enum.29---0.04------
VC enum.30------------
case i=n
VC enum.30.0---------0.03
VC enum.30.1------------
split_all_full
VC enum.30.1.0---0.20------
VC enum.30.1.1---0.17------
VC enum.31---------0.04
VC enum.32------------
split_vc
VC enum.32.0---0.69------
VC enum.32.1---0.02------
VC enum.32.2---0.20------
VC enum.32.3------0.12---
VC enum.33---0.05------
VC enum.34---------0.02
VC enum.35---------0.02
VC enum.36---------0.02
VC enum.37---------0.03
VC enum.38------0.13---
VC enum.39---------0.03
VC enum.40---------0.02
VC enum.41---------0.02
VC enum.42---------0.04
VC enum.43---------0.02
VC enum.44---------0.04
VC enum.45---------0.04
VC enum.46---------0.03
VC enum.47------0.12---
VC enum.48------------
split_vc
VC enum.48.0---0.06------
VC enum.48.1---0.24------
VC enum.48.2---------0.91
VC enum.48.3------------
case i<k
VC enum.48.3.0---0.08------
VC enum.48.3.1------------
case i=k
VC enum.48.3.1.0---0.33------
VC enum.48.3.1.1------------
assert (get1 c i = get1 c[k+1 ..] (i-k-1))
VC enum.48.3.1.1.0---------0.95
VC enum.48.3.1.1.1------0.21---
VC enum.48.4------0.40---
VC enum.48.5------0.08---
VC enum.48.6---------0.08
VC enum.48.7---0.03------
VC enum.49---------0.02
VC enum.50------0.13---
VC enum.51---------0.03
VC enum.52---0.03------
VC enum.53---0.03------
VC enum.54---0.06------
VC enum.55------------
apply H21
VC enum.55.0---------0.04
VC enum.55.1---------0.02
VC enum.56---0.08------
VC enum.57------------
split_all_full
VC enum.57.0---0.28------
VC enum.57.1---0.36------
VC enum.57.2---0.30------
VC enum.57.3---0.06------
VC enum.58---0.09------
VC enum.59---------0.03
VC enum.60---0.11------
VC enum.61---0.11------
VC enum.62------------
introduce_premises
VC enum.62.0------------
inline_goal
VC enum.62.0.0---0.87------
VC enum.63---------0.03
VC enum.64---------0.04
VC enum.65---------0.03
VC enum.66---------0.32
VC enum.67---------0.03
VC enum.68------------
split_vc
VC enum.68.0---0.16------
VC enum.68.1---------0.95
VC enum.68.2---0.81------
VC enum.69------------
split_all_full
VC enum.69.0------0.16---
VC enum.69.1------0.73---
VC enum.69.2------0.12---
VC enum.69.3---0.09------
VC enum.70---0.03------
VC enum.71---0.02------
VC enum.72---0.33------
VC enum.73------------
split_all_full
VC enum.73.0---0.62------
VC enum.73.1---0.34------
VC enum.74---0.38------
VC enum.75---------0.06
VC enum.76---0.11------
VC enum.77---0.02------