## Maximize product of adjacent numbers in a matrix

Find in a matrix the four numbers, adjacent in the same direction, that maximize their product.

**Authors:** Sylvain Dailler

**Topics:** Matrices

**Tools:** Why3

**References:** Project Euler

**See also:** Maximal sum in a matrix / Euler Project problem 11, SPARK/Ada version

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

# Euler Project, problem11

In the 20×20 grid below, four numbers along a diagonal line have been marked in red.

08 02 22 97 38 15 00 40 00 75 04 05 07 78 52 12 50 77 91 08 49 49 99 40 17 81 18 57 60 87 17 40 98 43 69 48 04 56 62 00 81 49 31 73 55 79 14 29 93 71 40 67 53 88 30 03 49 13 36 65 52 70 95 23 04 60 11 42 69 24 68 56 01 32 56 71 37 02 36 91 22 31 16 71 51 67 63 89 41 92 36 54 22 40 40 28 66 33 13 80 24 47 32 60 99 03 45 02 44 75 33 53 78 36 84 20 35 17 12 50 32 98 81 28 64 23 67 10 26 38 40 67 59 54 70 66 18 38 64 70 67 26 20 68 02 62 12 20 95 63 94 39 63 08 40 91 66 49 94 21 24 55 58 05 66 73 99 26 97 17 78 78 96 83 14 88 34 89 63 72 21 36 23 09 75 00 76 44 20 45 35 14 00 61 33 97 34 31 33 95 78 17 53 28 22 75 31 67 15 94 03 80 04 62 16 14 09 53 56 92 16 39 05 42 96 35 31 47 55 58 88 24 00 17 54 24 36 29 85 57 86 56 00 48 35 71 89 07 05 44 44 37 44 60 21 58 51 54 17 58 19 80 81 68 05 94 47 69 28 73 92 13 86 52 17 77 04 89 55 40 04 52 08 83 97 35 99 16 07 97 57 32 16 26 26 79 33 27 98 66 88 36 68 87 57 62 20 72 03 46 33 67 46 55 12 32 63 93 53 69 04 42 16 73 38 25 39 11 24 94 72 18 08 46 29 32 40 62 76 36 20 69 36 41 72 30 23 88 34 62 99 69 82 67 59 85 74 04 36 16 20 73 35 29 78 31 90 01 74 31 49 71 48 86 81 16 23 57 05 54 01 70 54 71 83 51 54 69 16 92 33 48 61 43 52 01 89 19 67 48

The product of these numbers is 26 × 63 × 78 × 14 = 1788696.

What is the greatest product of four adjacent numbers in the same direction (up, down, left, right, or diagonally) in the 20×20 grid?

module ProductFour use import int.Int use import ref.Ref use import matrix.Matrix use import option.Option

Direction of the product checked

type direction = | Left_bottom | Right_bottom | Bottom | Right

Math functions about the result of a product. Incomplete product generate None

function left_diag (m: matrix int) (i: int) (j: int) : option int = if (i < m.rows /\ j >= 0 /\ i >= 3 /\ j < m.columns - 3) then Some (((get m i j) * (get m (i - 1) (j + 1)) * (get m (i - 2) (j + 2)) * (get m (i-3) (j+3)))) else None function right_diag (m: matrix int) (i: int) (j: int) : option int = if (i < m.rows - 3 /\ i >= 0 /\ j < m.columns - 3 /\ j >= 0) then Some (((get m i j) * (get m (i + 1) (j + 1)) * (get m (i + 2) (j + 2)) * (get m (i+3) (j+3)))) else None function line (m: matrix int) (i: int) (j: int) : option int = if (0 <= j < m.columns /\ i >= 0 /\ i < m.rows - 3) then Some ((get m i j) * (get m (i+1) j) * (get m (i+2) j) * (get m (i+3) j)) else None function column (m: matrix int) (i: int) (j: int) : option int = if (0 <= i < m.rows /\ j >= 0 /\ j < m.columns - 3) then Some ((get m i j) * (get m i (j+1)) * (get m i (j+2)) * (get m i (j + 3))) else None

Computational functions for the product in each direction

let right_diag_c m i j : option int = ensures {result = right_diag m i j} if (i < m.rows - 3 && i >= 0 && j < m.columns - 3 && j >= 0) then Some (((get m i j) * (get m (i + 1) (j + 1)) * (get m (i + 2) (j + 2)) * (get m (i+3) (j+3)))) else None let left_diag_c m i j : option int = ensures {result = left_diag m i j} if (i < m.rows && j >= 0 && i >= 3 && j < m.columns - 3) then Some (((get m i j) * (get m (i - 1) (j + 1)) * (get m (i - 2) (j + 2)) * (get m (i-3) (j+3)))) else None let line_c m i j : option int = ensures {result = line m i j} if (0 <= j && j < m.columns && i >= 0 && i < m.rows - 3) then Some ((get m i j) * (get m (i+1) j) * (get m (i+2) j) * (get m (i+3) j)) else None let column_c m i j : option int = ensures {result = column m i j} if (0 <= i && i < m.rows && j >= 0 && j < m.columns - 3) then Some ((get m i j) * (get m i (j+1)) * (get m i (j+2)) * (get m i (j + 3))) else None (* function compute4 (m: matrix int) (i: int) (j: int) (d: direction) : option int = *) (* match d with *) (* | Left_bottom -> left_diag m i j *) (* | Right_bottom -> right_diag m i j *) (* | Bottom -> column m i j *) (* | Right -> line m i j *) (* end *) (* TODO Failed attempt at pattern matching above. Combination of mathematical product result functions *) function compute4 (m: matrix int) (i: int) (j: int) (d: direction) : option int = if (d = Left_bottom) then left_diag m i j else if (d = Right_bottom) then right_diag m i j else if (d = Bottom) then column m i j else if (d = Right) then line m i j else None

A product is_valid if each elements of the product is in the matrix

(* predicate is_valid (m: matrix int) (i: int) (j: int) (d: direction) = *) (* match d with *) (* | Left_bottom -> i < m.rows /\ j >= 0 /\ i >= 3 /\ j < m.columns - 3 *) (* | Right_bottom -> i >= 0 /\ j >= 0 /\ i < m.rows - 3 /\ j < m.columns - 3 *) (* | Bottom -> 0 <= i /\ i < m.rows /\ j >= 0 /\ j < m.columns - 3 *) (* | Right -> 0 <= j /\ j < m.columns /\ i >= 0 /\ i < m.rows - 3 *) (* end *)

Return the maximum product of 4 for matrix m

let find_max (m: matrix int) = requires {m.rows > 4 /\ m.columns > 4} ensures {forall i j d. match (compute4 m i j d) with | None -> true | Some v -> v <= result end} ensures {exists i j d. Some result = compute4 m i j d}

Current max and element of the matrix for which it is attained

let cur_max = ref ( match (line_c m 0 0) with | None -> 0 (* TODO should not happen *) | Some v -> v end) in let cur_i = ref 0 in let cur_j = ref 0 in let cur_d = ref Right in for i = 0 to (m.rows - 1) do (* Cur_max is greater than each product already seen *) invariant { forall i' j' d. (0 <= i' < i /\ 0 <= j' < m.columns) -> match (compute4 m i' j' d) with | None -> true | Some v -> v <= !cur_max end} (* cur_max is actually the product at (cur_i, cur_j, cur_d) *) invariant {Some !cur_max = compute4 m !cur_i !cur_j !cur_d} for j = 0 to (m.columns - 1) do (* cur_max is actually the product at (cur_i, cur_j, cur_d) *) invariant {Some !cur_max = compute4 m !cur_i !cur_j !cur_d} (* Cur_max is greater than each product already seen *) invariant { forall i' j' d. ((i' = i /\ 0 <= j' /\ j' < j) \/ (0 <= i' < i /\ 0 <= j' < m.columns)) -> match (compute4 m i' j' d) with | None -> true | Some v -> v <= !cur_max end} (* Computation of the product for each direction *) match (left_diag_c m i j) with | None -> () | Some v -> if (v > !cur_max) then begin cur_max := v; cur_i := i; cur_j := j; cur_d := Left_bottom; end end; match (right_diag_c m i j) with | None -> () | Some v -> if (v > !cur_max) then begin cur_max := v; cur_i := i; cur_j := j; cur_d := Right_bottom; end end; match (line_c m i j) with | None -> () | Some v -> if (v > !cur_max) then begin cur_max := v; cur_i := i; cur_j := j; cur_d := Right; end end; match (column_c m i j) with | None -> () | Some v -> if (v > !cur_max) then begin cur_max := v; cur_i := i; cur_j := j; cur_d := Bottom; end end; done; done;

Assert implying directly the postcondition

assert { Some !cur_max = compute4 m !cur_i !cur_j !cur_d}; !cur_max;; end

download ZIP archive

# Why3 Proof Results for Project "euler011"

## Theory "euler011.ProductFour": fully verified in 43.19 s

Obligations | Alt-Ergo (1.30) | |||||||

VC for right_diag_c | 0.05 | |||||||

VC for left_diag_c | 0.08 | |||||||

VC for line_c | 0.04 | |||||||

VC for column_c | 0.04 | |||||||

VC for find_max | --- | |||||||

split_goal_wp | ||||||||

assertion | 0.00 | |||||||

postcondition | --- | |||||||

split_goal_wp | ||||||||

postcondition | 0.01 | |||||||

postcondition | 0.00 | |||||||

loop invariant init | 0.01 | |||||||

loop invariant init | 0.00 | |||||||

loop invariant preservation | 0.00 | |||||||

loop invariant preservation | 0.00 | |||||||

loop invariant init | 0.00 | |||||||

loop invariant init | 0.02 | |||||||

loop invariant preservation | 0.01 | |||||||

loop invariant preservation | --- | |||||||

split_goal_wp | ||||||||

loop invariant preservation | 0.07 | |||||||

loop invariant preservation | 0.01 | |||||||

loop invariant preservation | --- | |||||||

split_goal_wp | ||||||||

loop invariant preservation | 0.15 | |||||||

loop invariant preservation | 0.01 | |||||||

loop invariant preservation | --- | |||||||

split_goal_wp | ||||||||

loop invariant preservation | 0.14 | |||||||

loop invariant preservation | 0.01 | |||||||

loop invariant preservation | --- | |||||||

split_goal_wp | ||||||||

loop invariant preservation | 0.07 | |||||||

loop invariant preservation | 0.01 | |||||||

loop invariant preservation | --- | |||||||

split_goal_wp | ||||||||

loop invariant preservation | --- | |||||||

introduce_premises | ||||||||

loop invariant preservation | --- | |||||||

inline_goal | ||||||||

loop invariant preservation | 0.11 | |||||||

loop invariant preservation | 0.02 | |||||||

loop invariant preservation | --- | |||||||

split_goal_wp | ||||||||

loop invariant preservation | --- | |||||||

introduce_premises | ||||||||

loop invariant preservation | --- | |||||||

inline_goal | ||||||||

loop invariant preservation | 0.13 | |||||||

loop invariant preservation | 0.00 | |||||||

loop invariant preservation | --- | |||||||

split_goal_wp | ||||||||

loop invariant preservation | 0.10 | |||||||

loop invariant preservation | 0.01 | |||||||

loop invariant preservation | --- | |||||||

split_goal_wp | ||||||||

loop invariant preservation | 0.15 | |||||||

loop invariant preservation | 0.01 | |||||||

loop invariant preservation | --- | |||||||

split_goal_wp | ||||||||

loop invariant preservation | 0.13 | |||||||

loop invariant preservation | 0.01 | |||||||

loop invariant preservation | --- | |||||||

split_goal_wp | ||||||||

loop invariant preservation | 0.17 | |||||||

loop invariant preservation | 0.01 | |||||||

loop invariant preservation | --- | |||||||

split_goal_wp | ||||||||

loop invariant preservation | --- | |||||||

introduce_premises | ||||||||

loop invariant preservation | --- | |||||||

inline_goal | ||||||||

loop invariant preservation | 0.15 | |||||||

loop invariant preservation | 0.01 | |||||||

loop invariant preservation | --- | |||||||

split_goal_wp | ||||||||

loop invariant preservation | --- | |||||||

introduce_premises | ||||||||

loop invariant preservation | --- | |||||||

inline_goal | ||||||||

loop invariant preservation | 0.12 | |||||||

loop invariant preservation | 0.02 | |||||||

loop invariant preservation | --- | |||||||

split_goal_wp | ||||||||

loop invariant preservation | --- | |||||||

introduce_premises | ||||||||

loop invariant preservation | --- | |||||||

inline_goal | ||||||||

loop invariant preservation | 0.13 | |||||||

loop invariant preservation | 0.02 | |||||||

loop invariant preservation | --- | |||||||

split_goal_wp | ||||||||

loop invariant preservation | --- | |||||||

introduce_premises | ||||||||

loop invariant preservation | --- | |||||||

inline_goal | ||||||||

loop invariant preservation | 0.14 | |||||||

loop invariant preservation | 0.01 | |||||||

loop invariant preservation | --- | |||||||

split_goal_wp | ||||||||

loop invariant preservation | 0.13 | |||||||

loop invariant preservation | 0.01 | |||||||

loop invariant preservation | --- | |||||||

split_goal_wp | ||||||||

loop invariant preservation | --- | |||||||

introduce_premises | ||||||||

loop invariant preservation | --- | |||||||

inline_goal | ||||||||

loop invariant preservation | 0.11 | |||||||

loop invariant preservation | 0.01 | |||||||

loop invariant preservation | --- | |||||||

split_goal_wp | ||||||||

loop invariant preservation | 0.11 | |||||||

loop invariant preservation | 0.01 | |||||||

loop invariant preservation | 0.11 | |||||||

loop invariant preservation | 0.01 | |||||||

loop invariant preservation | 0.11 | |||||||

loop invariant preservation | 0.01 | |||||||

loop invariant preservation | 0.11 | |||||||

loop invariant preservation | 0.01 | |||||||

loop invariant preservation | --- | |||||||

split_goal_wp | ||||||||

loop invariant preservation | 0.11 | |||||||

loop invariant preservation | 0.01 | |||||||

loop invariant preservation | --- | |||||||

split_goal_wp | ||||||||

loop invariant preservation | --- | |||||||

introduce_premises | ||||||||

loop invariant preservation | --- | |||||||

inline_goal | ||||||||

loop invariant preservation | 0.11 | |||||||

loop invariant preservation | 0.01 | |||||||

loop invariant preservation | 0.10 | |||||||

loop invariant preservation | 0.01 | |||||||

loop invariant preservation | 0.11 | |||||||

loop invariant preservation | 0.00 | |||||||

loop invariant preservation | --- | |||||||

split_goal_wp | ||||||||

loop invariant preservation | 0.10 | |||||||

loop invariant preservation | 0.01 | |||||||

loop invariant preservation | 0.14 | |||||||

loop invariant preservation | 0.00 | |||||||

loop invariant preservation | 0.13 | |||||||

loop invariant preservation | 0.01 | |||||||

loop invariant preservation | --- | |||||||

split_goal_wp | ||||||||

loop invariant preservation | 0.13 | |||||||

loop invariant preservation | 0.01 | |||||||

loop invariant preservation | --- | |||||||

split_goal_wp | ||||||||

loop invariant preservation | --- | |||||||

introduce_premises | ||||||||

loop invariant preservation | --- | |||||||

inline_goal | ||||||||

loop invariant preservation | 0.12 | |||||||

loop invariant preservation | 0.01 | |||||||

loop invariant preservation | --- | |||||||

split_goal_wp | ||||||||

loop invariant preservation | --- | |||||||

introduce_premises | ||||||||

loop invariant preservation | --- | |||||||

inline_goal | ||||||||

loop invariant preservation | 0.09 | |||||||

loop invariant preservation | 0.01 | |||||||

loop invariant preservation | --- | |||||||

split_goal_wp | ||||||||

loop invariant preservation | --- | |||||||

introduce_premises | ||||||||

loop invariant preservation | --- | |||||||

inline_goal | ||||||||

loop invariant preservation | 0.14 | |||||||

loop invariant preservation | 0.02 | |||||||

loop invariant preservation | --- | |||||||

split_goal_wp | ||||||||

loop invariant preservation | --- | |||||||

introduce_premises | ||||||||

loop invariant preservation | --- | |||||||

inline_goal | ||||||||

loop invariant preservation | 0.15 | |||||||

loop invariant preservation | 0.01 | |||||||

loop invariant preservation | 0.15 | |||||||

loop invariant preservation | 0.01 | |||||||

loop invariant preservation | --- | |||||||

split_goal_wp | ||||||||

loop invariant preservation | 0.16 | |||||||

loop invariant preservation | 0.01 | |||||||

loop invariant preservation | 0.13 | |||||||

loop invariant preservation | 0.01 | |||||||

loop invariant preservation | --- | |||||||

split_goal_wp | ||||||||

loop invariant preservation | 0.13 | |||||||

loop invariant preservation | 0.01 | |||||||

loop invariant preservation | --- | |||||||

split_goal_wp | ||||||||

loop invariant preservation | --- | |||||||

introduce_premises | ||||||||

loop invariant preservation | --- | |||||||

inline_goal | ||||||||

loop invariant preservation | 0.14 | |||||||

loop invariant preservation | 0.01 | |||||||

loop invariant preservation | --- | |||||||

split_goal_wp | ||||||||

loop invariant preservation | --- | |||||||

introduce_premises | ||||||||

loop invariant preservation | --- | |||||||

inline_goal | ||||||||

loop invariant preservation | 0.12 | |||||||

loop invariant preservation | 0.02 | |||||||

loop invariant preservation | 0.12 | |||||||

loop invariant preservation | 0.01 | |||||||

loop invariant preservation | 0.14 | |||||||

loop invariant preservation | 0.02 | |||||||

loop invariant preservation | --- | |||||||

split_goal_wp | ||||||||

loop invariant preservation | 0.52 | |||||||

loop invariant preservation | 0.02 | |||||||

loop invariant preservation | 0.52 | |||||||

loop invariant preservation | 0.01 | |||||||

loop invariant preservation | 0.13 | |||||||

loop invariant preservation | 0.01 | |||||||

loop invariant preservation | --- | |||||||

split_goal_wp | ||||||||

loop invariant preservation | 0.49 | |||||||

loop invariant preservation | 0.02 | |||||||

loop invariant preservation | --- | |||||||

split_goal_wp | ||||||||

loop invariant preservation | --- | |||||||

introduce_premises | ||||||||

loop invariant preservation | --- | |||||||

inline_goal | ||||||||

loop invariant preservation | 0.49 | |||||||

loop invariant preservation | 0.02 | |||||||

loop invariant preservation | 0.14 | |||||||

loop invariant preservation | 0.02 | |||||||

loop invariant preservation | 0.15 | |||||||

loop invariant preservation | 0.01 | |||||||

loop invariant preservation | --- | |||||||

split_goal_wp | ||||||||

loop invariant preservation | 0.13 | |||||||

loop invariant preservation | 0.02 | |||||||

loop invariant preservation | --- | |||||||

split_goal_wp | ||||||||

loop invariant preservation | --- | |||||||

introduce_premises | ||||||||

loop invariant preservation | --- | |||||||

inline_goal | ||||||||

loop invariant preservation | --- | |||||||

eliminate_definition | ||||||||

loop invariant preservation | 0.13 | |||||||

loop invariant preservation | 0.02 | |||||||

loop invariant preservation | --- | |||||||

split_goal_wp | ||||||||

loop invariant preservation | 0.49 | |||||||

loop invariant preservation | 0.01 | |||||||

loop invariant preservation | 0.36 | |||||||

loop invariant preservation | 0.02 | |||||||

loop invariant preservation | 0.18 | |||||||

loop invariant preservation | 0.02 | |||||||

loop invariant preservation | 0.52 | |||||||

loop invariant preservation | 0.01 | |||||||

loop invariant preservation | --- | |||||||

split_goal_wp | ||||||||

loop invariant preservation | 0.49 | |||||||

loop invariant preservation | 0.01 | |||||||

loop invariant preservation | --- | |||||||

split_goal_wp | ||||||||

loop invariant preservation | --- | |||||||

introduce_premises | ||||||||

loop invariant preservation | --- | |||||||

inline_goal | ||||||||

loop invariant preservation | 0.10 | |||||||

loop invariant preservation | 0.02 | |||||||

loop invariant preservation | --- | |||||||

split_goal_wp | ||||||||

loop invariant preservation | 0.07 | |||||||

loop invariant preservation | 0.00 | |||||||

loop invariant preservation | --- | |||||||

split_goal_wp | ||||||||

loop invariant preservation | 0.11 | |||||||

loop invariant preservation | 0.01 | |||||||

loop invariant preservation | 0.15 | |||||||

loop invariant preservation | 0.01 | |||||||

loop invariant preservation | 0.14 | |||||||

loop invariant preservation | 0.01 | |||||||

loop invariant preservation | --- | |||||||

split_goal_wp | ||||||||

loop invariant preservation | --- | |||||||

introduce_premises | ||||||||

loop invariant preservation | --- | |||||||

inline_goal | ||||||||

loop invariant preservation | 0.13 | |||||||

loop invariant preservation | 0.00 | |||||||

loop invariant preservation | --- | |||||||

split_goal_wp | ||||||||

loop invariant preservation | --- | |||||||

introduce_premises | ||||||||

loop invariant preservation | --- | |||||||

inline_goal | ||||||||

loop invariant preservation | 0.16 | |||||||

loop invariant preservation | 0.01 | |||||||

loop invariant preservation | 0.15 | |||||||

loop invariant preservation | 0.00 | |||||||

loop invariant preservation | 0.13 | |||||||

loop invariant preservation | 0.01 | |||||||

loop invariant preservation | 0.15 | |||||||

loop invariant preservation | 0.01 | |||||||

loop invariant preservation | 0.18 | |||||||

loop invariant preservation | 0.01 | |||||||

loop invariant preservation | --- | |||||||

split_goal_wp | ||||||||

loop invariant preservation | 0.15 | |||||||

loop invariant preservation | 0.01 | |||||||

loop invariant preservation | --- | |||||||

split_goal_wp | ||||||||

loop invariant preservation | 0.14 | |||||||

loop invariant preservation | 0.01 | |||||||

loop invariant preservation | --- | |||||||

split_goal_wp | ||||||||

loop invariant preservation | 0.51 | |||||||

loop invariant preservation | 0.01 | |||||||

loop invariant preservation | 0.48 | |||||||

loop invariant preservation | 0.01 | |||||||

loop invariant preservation | 0.13 | |||||||

loop invariant preservation | 0.01 | |||||||

loop invariant preservation | 0.52 | |||||||

loop invariant preservation | 0.01 | |||||||

loop invariant preservation | 0.49 | |||||||

loop invariant preservation | 0.01 | |||||||

loop invariant preservation | --- | |||||||

split_goal_wp | ||||||||

loop invariant preservation | 0.13 | |||||||

loop invariant preservation | 0.01 | |||||||

loop invariant preservation | 0.14 | |||||||

loop invariant preservation | 0.01 | |||||||

loop invariant preservation | 0.17 | |||||||

loop invariant preservation | 0.02 | |||||||

loop invariant preservation | 0.15 | |||||||

loop invariant preservation | 0.01 | |||||||

loop invariant preservation | 0.47 | |||||||

loop invariant preservation | 0.01 | |||||||

loop invariant preservation | 0.46 | |||||||

loop invariant preservation | 0.01 | |||||||

loop invariant preservation | 0.11 | |||||||

loop invariant preservation | 0.02 | |||||||

loop invariant preservation | 0.35 | |||||||

loop invariant preservation | 0.01 | |||||||

loop invariant preservation | 0.32 | |||||||

loop invariant preservation | --- | |||||||

split_goal_wp | ||||||||

loop invariant preservation | 0.02 | |||||||

loop invariant preservation | 0.01 | |||||||

assertion | 0.00 | |||||||

postcondition | 0.01 | |||||||

postcondition | 0.01 | |||||||

assertion | 0.01 | |||||||

postcondition | 0.01 | |||||||

postcondition | 0.01 | |||||||

loop invariant init | 0.00 | |||||||

loop invariant init | 0.00 | |||||||

loop invariant preservation | 0.01 | |||||||

loop invariant preservation | 0.00 | |||||||

loop invariant init | 0.00 | |||||||

loop invariant init | --- | |||||||

split_goal_wp | ||||||||

loop invariant init | --- | |||||||

introduce_premises | ||||||||

loop invariant init | --- | |||||||

inline_goal | ||||||||

loop invariant init | 0.02 | |||||||

loop invariant preservation | 0.00 | |||||||

loop invariant preservation | --- | |||||||

split_goal_wp | ||||||||

loop invariant preservation | --- | |||||||

introduce_premises | ||||||||

loop invariant preservation | --- | |||||||

inline_goal | ||||||||

loop invariant preservation | 0.11 | |||||||

loop invariant preservation | 0.01 | |||||||

loop invariant preservation | --- | |||||||

split_goal_wp | ||||||||

loop invariant preservation | --- | |||||||

introduce_premises | ||||||||

loop invariant preservation | --- | |||||||

inline_goal | ||||||||

loop invariant preservation | 0.21 | |||||||

loop invariant preservation | 0.01 | |||||||

loop invariant preservation | --- | |||||||

split_goal_wp | ||||||||

loop invariant preservation | --- | |||||||

introduce_premises | ||||||||

loop invariant preservation | --- | |||||||

inline_goal | ||||||||

loop invariant preservation | 0.20 | |||||||

loop invariant preservation | 0.00 | |||||||

loop invariant preservation | --- | |||||||

split_goal_wp | ||||||||

loop invariant preservation | --- | |||||||

introduce_premises | ||||||||

loop invariant preservation | --- | |||||||

inline_goal | ||||||||

loop invariant preservation | 0.15 | |||||||

loop invariant preservation | 0.00 | |||||||

loop invariant preservation | --- | |||||||

split_goal_wp | ||||||||

loop invariant preservation | --- | |||||||

introduce_premises | ||||||||

loop invariant preservation | --- | |||||||

inline_goal | ||||||||

loop invariant preservation | 0.12 | |||||||

loop invariant preservation | 0.01 | |||||||

loop invariant preservation | 0.14 | |||||||

loop invariant preservation | 0.00 | |||||||

loop invariant preservation | --- | |||||||

split_goal_wp | ||||||||

loop invariant preservation | --- | |||||||

introduce_premises | ||||||||

loop invariant preservation | --- | |||||||

inline_goal | ||||||||

loop invariant preservation | 0.12 | |||||||

loop invariant preservation | 0.01 | |||||||

loop invariant preservation | --- | |||||||

split_goal_wp | ||||||||

loop invariant preservation | 0.13 | |||||||

loop invariant preservation | 0.01 | |||||||

loop invariant preservation | 0.13 | |||||||

loop invariant preservation | 0.01 | |||||||

loop invariant preservation | --- | |||||||

split_goal_wp | ||||||||

loop invariant preservation | 0.28 | |||||||

loop invariant preservation | 0.01 | |||||||

loop invariant preservation | --- | |||||||

split_goal_wp | ||||||||

loop invariant preservation | 0.14 | |||||||

loop invariant preservation | 0.01 | |||||||

loop invariant preservation | --- | |||||||

split_goal_wp | ||||||||

loop invariant preservation | 0.14 | |||||||

loop invariant preservation | 0.01 | |||||||

loop invariant preservation | 0.19 | |||||||

loop invariant preservation | 0.01 | |||||||

loop invariant preservation | --- | |||||||

split_goal_wp | ||||||||

loop invariant preservation | 0.27 | |||||||

loop invariant preservation | 0.02 | |||||||

loop invariant preservation | --- | |||||||

split_goal_wp | ||||||||

loop invariant preservation | 0.25 | |||||||

loop invariant preservation | 0.01 | |||||||

loop invariant preservation | 0.22 | |||||||

loop invariant preservation | 0.01 | |||||||

loop invariant preservation | --- | |||||||

split_goal_wp | ||||||||

loop invariant preservation | 0.23 | |||||||

loop invariant preservation | 0.01 | |||||||

loop invariant preservation | --- | |||||||

split_goal_wp | ||||||||

loop invariant preservation | 0.33 | |||||||

loop invariant preservation | 0.01 | |||||||

loop invariant preservation | 0.27 | |||||||

loop invariant preservation | 0.01 | |||||||

loop invariant preservation | 0.11 | |||||||

loop invariant preservation | 0.01 | |||||||

loop invariant preservation | 0.13 | |||||||

loop invariant preservation | 0.02 | |||||||

loop invariant preservation | --- | |||||||

split_goal_wp | ||||||||

loop invariant preservation | 0.31 | |||||||

loop invariant preservation | 0.01 | |||||||

loop invariant preservation | 0.19 | |||||||

loop invariant preservation | 0.01 | |||||||

loop invariant preservation | --- | |||||||

split_goal_wp | ||||||||

loop invariant preservation | 0.27 | |||||||

loop invariant preservation | 0.01 | |||||||

loop invariant preservation | --- | |||||||

split_goal_wp | ||||||||

loop invariant preservation | --- | |||||||

introduce_premises | ||||||||

loop invariant preservation | --- | |||||||

inline_goal | ||||||||

loop invariant preservation | 0.24 | |||||||

loop invariant preservation | 0.02 | |||||||

loop invariant preservation | --- | |||||||

split_goal_wp | ||||||||

loop invariant preservation | 0.22 | |||||||

loop invariant preservation | 0.01 | |||||||

loop invariant preservation | --- | |||||||

split_goal_wp | ||||||||

loop invariant preservation | 0.29 | |||||||

loop invariant preservation | 0.02 | |||||||

loop invariant preservation | --- | |||||||

split_goal_wp | ||||||||

loop invariant preservation | --- | |||||||

introduce_premises | ||||||||

loop invariant preservation | --- | |||||||

inline_goal | ||||||||

loop invariant preservation | 0.09 | |||||||

loop invariant preservation | 0.01 | |||||||

loop invariant preservation | --- | |||||||

split_goal_wp | ||||||||

loop invariant preservation | --- | |||||||

introduce_premises | ||||||||

loop invariant preservation | --- | |||||||

inline_goal | ||||||||

loop invariant preservation | 0.18 | |||||||

loop invariant preservation | 0.01 | |||||||

loop invariant preservation | --- | |||||||

split_goal_wp | ||||||||

loop invariant preservation | --- | |||||||

introduce_premises | ||||||||

loop invariant preservation | --- | |||||||

inline_goal | ||||||||

loop invariant preservation | 0.21 | |||||||

loop invariant preservation | 0.01 | |||||||

loop invariant preservation | 0.13 | |||||||

loop invariant preservation | 0.02 | |||||||

loop invariant preservation | 0.13 | |||||||

loop invariant preservation | 0.02 | |||||||

loop invariant preservation | 0.19 | |||||||

loop invariant preservation | 0.01 | |||||||

loop invariant preservation | --- | |||||||

split_goal_wp | ||||||||

loop invariant preservation | --- | |||||||

introduce_premises | ||||||||

loop invariant preservation | --- | |||||||

inline_goal | ||||||||

loop invariant preservation | 0.17 | |||||||

loop invariant preservation | 0.01 | |||||||

loop invariant preservation | --- | |||||||

split_goal_wp | ||||||||

loop invariant preservation | --- | |||||||

introduce_premises | ||||||||

loop invariant preservation | --- | |||||||

inline_goal | ||||||||

loop invariant preservation | 0.13 | |||||||

loop invariant preservation | 0.02 | |||||||

loop invariant preservation | 0.13 | |||||||

loop invariant preservation | 0.01 | |||||||

loop invariant preservation | --- | |||||||

split_goal_wp | ||||||||

loop invariant preservation | 0.12 | |||||||

loop invariant preservation | 0.02 | |||||||

loop invariant preservation | 0.12 | |||||||

loop invariant preservation | 0.01 | |||||||

loop invariant preservation | 0.12 | |||||||

loop invariant preservation | 0.01 | |||||||

loop invariant preservation | --- | |||||||

split_goal_wp | ||||||||

loop invariant preservation | 0.16 | |||||||

loop invariant preservation | 0.03 | |||||||

loop invariant preservation | --- | |||||||

split_goal_wp | ||||||||

loop invariant preservation | --- | |||||||

introduce_premises | ||||||||

loop invariant preservation | --- | |||||||

inline_goal | ||||||||

loop invariant preservation | 1.01 | |||||||

loop invariant preservation | 0.01 | |||||||

loop invariant preservation | --- | |||||||

split_goal_wp | ||||||||

loop invariant preservation | --- | |||||||

introduce_premises | ||||||||

loop invariant preservation | --- | |||||||

inline_goal | ||||||||

loop invariant preservation | 0.97 | |||||||

loop invariant preservation | 0.01 | |||||||

loop invariant preservation | 0.18 | |||||||

loop invariant preservation | 0.02 | |||||||

loop invariant preservation | --- | |||||||

split_goal_wp | ||||||||

loop invariant preservation | --- | |||||||

introduce_premises | ||||||||

loop invariant preservation | --- | |||||||

inline_goal | ||||||||

loop invariant preservation | 0.71 | |||||||

loop invariant preservation | 0.01 | |||||||

loop invariant preservation | --- | |||||||

split_goal_wp | ||||||||

loop invariant preservation | --- | |||||||

introduce_premises | ||||||||

loop invariant preservation | --- | |||||||

inline_goal | ||||||||

loop invariant preservation | 0.76 | |||||||

loop invariant preservation | 0.01 | |||||||

loop invariant preservation | 0.13 | |||||||

loop invariant preservation | 0.01 | |||||||

loop invariant preservation | --- | |||||||

split_goal_wp | ||||||||

loop invariant preservation | 0.12 | |||||||

loop invariant preservation | 0.01 | |||||||

loop invariant preservation | 0.15 | |||||||

loop invariant preservation | 0.02 | |||||||

loop invariant preservation | 0.15 | |||||||

loop invariant preservation | 0.02 | |||||||

loop invariant preservation | --- | |||||||

split_goal_wp | ||||||||

loop invariant preservation | --- | |||||||

introduce_premises | ||||||||

loop invariant preservation | --- | |||||||

inline_goal | ||||||||

loop invariant preservation | 0.94 | |||||||

loop invariant preservation | 0.01 | |||||||

loop invariant preservation | --- | |||||||

split_goal_wp | ||||||||

loop invariant preservation | --- | |||||||

introduce_premises | ||||||||

loop invariant preservation | --- | |||||||

inline_goal | ||||||||

loop invariant preservation | 0.78 | |||||||

loop invariant preservation | 0.01 | |||||||

loop invariant preservation | 0.12 | |||||||

loop invariant preservation | 0.01 | |||||||

loop invariant preservation | --- | |||||||

split_goal_wp | ||||||||

loop invariant preservation | --- | |||||||

introduce_premises | ||||||||

loop invariant preservation | --- | |||||||

inline_goal | ||||||||

loop invariant preservation | 0.61 | |||||||

loop invariant preservation | 0.01 | |||||||

loop invariant preservation | --- | |||||||

split_goal_wp | ||||||||

loop invariant preservation | --- | |||||||

introduce_premises | ||||||||

loop invariant preservation | --- | |||||||

inline_goal | ||||||||

loop invariant preservation | 0.60 | |||||||

loop invariant preservation | 0.00 | |||||||

loop invariant preservation | 0.10 | |||||||

loop invariant preservation | 0.01 | |||||||

loop invariant preservation | --- | |||||||

split_goal_wp | ||||||||

loop invariant preservation | --- | |||||||

introduce_premises | ||||||||

loop invariant preservation | --- | |||||||

inline_goal | ||||||||

loop invariant preservation | 0.19 | |||||||

loop invariant preservation | 0.01 | |||||||

loop invariant preservation | --- | |||||||

split_goal_wp | ||||||||

loop invariant preservation | --- | |||||||

introduce_premises | ||||||||

loop invariant preservation | --- | |||||||

inline_goal | ||||||||

loop invariant preservation | 0.19 | |||||||

loop invariant preservation | 0.01 | |||||||

loop invariant preservation | 0.17 | |||||||

loop invariant preservation | 0.01 | |||||||

loop invariant preservation | --- | |||||||

split_goal_wp | ||||||||

loop invariant preservation | --- | |||||||

introduce_premises | ||||||||

loop invariant preservation | --- | |||||||

inline_goal | ||||||||

loop invariant preservation | 0.18 | |||||||

loop invariant preservation | 0.01 | |||||||

loop invariant preservation | 0.19 | |||||||

loop invariant preservation | 0.01 | |||||||

loop invariant preservation | 0.17 | |||||||

loop invariant preservation | 0.01 | |||||||

loop invariant preservation | 0.20 | |||||||

loop invariant preservation | 0.01 | |||||||

loop invariant preservation | 0.17 | |||||||

loop invariant preservation | 0.01 | |||||||

loop invariant preservation | 0.12 | |||||||

loop invariant preservation | 0.01 | |||||||

loop invariant preservation | --- | |||||||

split_goal_wp | ||||||||

loop invariant preservation | 0.14 | |||||||

loop invariant preservation | 0.01 | |||||||

loop invariant preservation | 0.17 | |||||||

loop invariant preservation | 0.01 | |||||||

loop invariant preservation | 0.17 | |||||||

loop invariant preservation | 0.01 | |||||||

loop invariant preservation | --- | |||||||

split_goal_wp | ||||||||

loop invariant preservation | --- | |||||||

introduce_premises | ||||||||

loop invariant preservation | --- | |||||||

inline_goal | ||||||||

loop invariant preservation | 0.64 | |||||||

loop invariant preservation | 0.01 | |||||||

loop invariant preservation | --- | |||||||

split_goal_wp | ||||||||

loop invariant preservation | --- | |||||||

introduce_premises | ||||||||

loop invariant preservation | --- | |||||||

inline_goal | ||||||||

loop invariant preservation | 0.58 | |||||||

loop invariant preservation | 0.01 | |||||||

loop invariant preservation | 0.15 | |||||||

loop invariant preservation | 0.01 | |||||||

loop invariant preservation | --- | |||||||

split_goal_wp | ||||||||

loop invariant preservation | --- | |||||||

introduce_premises | ||||||||

loop invariant preservation | --- | |||||||

inline_goal | ||||||||

loop invariant preservation | 0.91 | |||||||

loop invariant preservation | 0.01 | |||||||

loop invariant preservation | --- | |||||||

split_goal_wp | ||||||||

loop invariant preservation | --- | |||||||

introduce_premises | ||||||||

loop invariant preservation | --- | |||||||

inline_goal | ||||||||

loop invariant preservation | 0.98 | |||||||

loop invariant preservation | 0.01 | |||||||

loop invariant preservation | 0.12 | |||||||

loop invariant preservation | 0.01 | |||||||

loop invariant preservation | 0.13 | |||||||

loop invariant preservation | 0.01 | |||||||

loop invariant preservation | 0.14 | |||||||

loop invariant preservation | 0.01 | |||||||

loop invariant preservation | --- | |||||||

split_goal_wp | ||||||||

loop invariant preservation | --- | |||||||

introduce_premises | ||||||||

loop invariant preservation | --- | |||||||

inline_goal | ||||||||

loop invariant preservation | 0.15 | |||||||

loop invariant preservation | 0.01 | |||||||

loop invariant preservation | --- | |||||||

split_goal_wp | ||||||||

loop invariant preservation | --- | |||||||

introduce_premises | ||||||||

loop invariant preservation | --- | |||||||

inline_goal | ||||||||

loop invariant preservation | 0.82 | |||||||

loop invariant preservation | 0.01 | |||||||

loop invariant preservation | --- | |||||||

split_goal_wp | ||||||||

loop invariant preservation | --- | |||||||

introduce_premises | ||||||||

loop invariant preservation | --- | |||||||

inline_goal | ||||||||

loop invariant preservation | 0.64 | |||||||

loop invariant preservation | 0.00 | |||||||

loop invariant preservation | --- | |||||||

split_goal_wp | ||||||||

loop invariant preservation | --- | |||||||

introduce_premises | ||||||||

loop invariant preservation | --- | |||||||

inline_goal | ||||||||

loop invariant preservation | 0.12 | |||||||

loop invariant preservation | 0.01 | |||||||

loop invariant preservation | --- | |||||||

split_goal_wp | ||||||||

loop invariant preservation | --- | |||||||

introduce_premises | ||||||||

loop invariant preservation | --- | |||||||

inline_goal | ||||||||

loop invariant preservation | 0.52 | |||||||

loop invariant preservation | 0.01 | |||||||

loop invariant preservation | --- | |||||||

split_goal_wp | ||||||||

loop invariant preservation | --- | |||||||

introduce_premises | ||||||||

loop invariant preservation | --- | |||||||

inline_goal | ||||||||

loop invariant preservation | 0.55 | |||||||

loop invariant preservation | 0.04 | |||||||

loop invariant preservation | 0.01 | |||||||

assertion | --- | |||||||

split_goal_wp | ||||||||

assertion | --- | |||||||

introduce_premises | ||||||||

assertion | --- | |||||||

inline_goal | ||||||||

assertion | --- | |||||||

split_goal_wp | ||||||||

assertion | --- | |||||||

introduce_premises | ||||||||

assertion | --- | |||||||

inline_goal | ||||||||

assertion | 0.08 | |||||||

postcondition | 1.89 | |||||||

postcondition | 0.01 |