Commit 9ea8a6a4 authored by Andrei Paskevich's avatar Andrei Paskevich

examples: add the missing proofs for type witnesses

Not done: double_wp/logic and avl/table.

The subgoal pairing changed in verifythis_2017_tree_buffer
in an unrelated VC (see the diff for why3session.xml). FIXME?
parent 0650b2ed
module A module A
use import int.Int use import int.Int
type t = private { a: int } invariant { a >= 0 } type t = private { a: int } invariant { a >= 0 } by { a = 0 }
end end
module B module B
use import int.Int use import int.Int
type t = { a: int; b: int } invariant { a >= b >= 0 } type t = { a: int; b: int } invariant { a >= b >= 0 } by { a = 0; b = 0 }
clone A with type t = t clone A with type t = t
end end
...@@ -172,6 +172,8 @@ module AVL ...@@ -172,6 +172,8 @@ module AVL
ghost m : m 'a; ghost m : m 'a;
} invariant { } invariant {
balanced repr /\ m = seq_model repr /\ m.hgt = real_height repr balanced repr /\ m = seq_model repr /\ m.hgt = real_height repr
} by {
repr = Empty; m = { seq = empty; hgt = 0 }
} }
meta coercion function m meta coercion function m
......
...@@ -18,7 +18,7 @@ ...@@ -18,7 +18,7 @@
<proof prover="0"><result status="valid" time="0.00" steps="1"/></proof> <proof prover="0"><result status="valid" time="0.00" steps="1"/></proof>
</goal> </goal>
</theory> </theory>
<theory name="AVL" sum="66e1443365a42b282492937f4d09bbb6"> <theory name="AVL" sum="c0b96d14d5a90bf2332d8dc606653492">
<goal name="M.M.assoc" expl=""> <goal name="M.M.assoc" expl="">
<proof prover="0"><result status="valid" time="0.00" steps="3"/></proof> <proof prover="0"><result status="valid" time="0.00" steps="3"/></proof>
</goal> </goal>
...@@ -50,6 +50,9 @@ ...@@ -50,6 +50,9 @@
</goal> </goal>
</transf> </transf>
</goal> </goal>
<goal name="VC t" expl="VC for t">
<proof prover="0" timelimit="5"><result status="valid" time="0.01" steps="9"/></proof>
</goal>
<goal name="VC height" expl="VC for height"> <goal name="VC height" expl="VC for height">
<proof prover="0"><result status="valid" time="0.02" steps="30"/></proof> <proof prover="0"><result status="valid" time="0.02" steps="30"/></proof>
</goal> </goal>
......
...@@ -121,6 +121,7 @@ module MapBase ...@@ -121,6 +121,7 @@ module MapBase
(** Extra invariant: sequence sorted *) (** Extra invariant: sequence sorted *)
type t 'a = { field : Sel.t 'a } invariant { selection_possible () field } type t 'a = { field : Sel.t 'a } invariant { selection_possible () field }
by { field = Sel.empty () }
type m 'a = { type m 'a = {
domn : K.t -> bool; domn : K.t -> bool;
......
...@@ -52,6 +52,7 @@ module ResizableArrayImplem (* : ResizableArraySpec *) ...@@ -52,6 +52,7 @@ module ResizableArrayImplem (* : ResizableArraySpec *)
invariant { 0 <= length <= A.length data } invariant { 0 <= length <= A.length data }
invariant { forall i: int. length <= i < A.length data -> invariant { forall i: int. length <= i < A.length data ->
A.([]) data i = dummy } A.([]) data i = dummy }
by { dummy = any 'a; length = 0; data = A.make 0 (any 'a) }
function ([]) (r: rarray 'a) (i: int) : 'a = A.([]) r.data i function ([]) (r: rarray 'a) (i: int) : 'a = A.([]) r.data i
......
...@@ -6,7 +6,10 @@ ...@@ -6,7 +6,10 @@
<file name="../resizable_array.mlw" expanded="true"> <file name="../resizable_array.mlw" expanded="true">
<theory name="ResizableArraySpec" sum="d41d8cd98f00b204e9800998ecf8427e" expanded="true"> <theory name="ResizableArraySpec" sum="d41d8cd98f00b204e9800998ecf8427e" expanded="true">
</theory> </theory>
<theory name="ResizableArrayImplem" sum="f6a8ce6d35230e1f00a4648b2f798bfe" expanded="true"> <theory name="ResizableArrayImplem" sum="d62174e0e2a371227338667fe7fd890f" expanded="true">
<goal name="VC rarray" expl="VC for rarray" expanded="true">
<proof prover="0"><result status="valid" time="0.00" steps="3"/></proof>
</goal>
<goal name="VC make" expl="VC for make" expanded="true"> <goal name="VC make" expl="VC for make" expanded="true">
<transf name="split_goal_wp" expanded="true"> <transf name="split_goal_wp" expanded="true">
<goal name="VC make.1" expl="array creation size"> <goal name="VC make.1" expl="array creation size">
......
...@@ -30,7 +30,10 @@ ...@@ -30,7 +30,10 @@
<proof prover="0"><result status="valid" time="0.08" steps="777"/></proof> <proof prover="0"><result status="valid" time="0.08" steps="777"/></proof>
</goal> </goal>
</theory> </theory>
<theory name="ITree" sum="7cd3f8370a8f73c6e8eaf6684fb82b17" expanded="true"> <theory name="ITree" sum="13f9be3f8d6ff6e1ef40a222286ad984" expanded="true">
<goal name="VC itree" expl="VC for itree" expanded="true">
<proof prover="0"><result status="valid" time="0.00" steps="6"/></proof>
</goal>
<goal name="VC create" expl="VC for create" expanded="true"> <goal name="VC create" expl="VC for create" expanded="true">
<proof prover="0"><result status="valid" time="0.00" steps="6"/></proof> <proof prover="0"><result status="valid" time="0.00" steps="6"/></proof>
</goal> </goal>
......
...@@ -5,7 +5,10 @@ ...@@ -5,7 +5,10 @@
<prover id="0" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" memlimit="1000"/> <prover id="0" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="6" name="Alt-Ergo" version="0.95.2" timelimit="5" steplimit="0" memlimit="1000"/> <prover id="6" name="Alt-Ergo" version="0.95.2" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../tower_of_hanoi.mlw" expanded="true"> <file name="../tower_of_hanoi.mlw" expanded="true">
<theory name="Hanoi" sum="ff68094fdd8f1e3a29decd895f45d1b6" expanded="true"> <theory name="Hanoi" sum="934ecac9b836a8bb7eba7c149be18efc" expanded="true">
<goal name="VC tower" expl="VC for tower" expanded="true">
<proof prover="0"><result status="valid" time="0.00" steps="2"/></proof>
</goal>
<goal name="VC move" expl="VC for move" expanded="true"> <goal name="VC move" expl="VC for move" expanded="true">
<transf name="split_goal_wp" expanded="true"> <transf name="split_goal_wp" expanded="true">
<goal name="VC move.1" expl="type invariant"> <goal name="VC move.1" expl="type invariant">
...@@ -97,11 +100,14 @@ ...@@ -97,11 +100,14 @@
</transf> </transf>
</goal> </goal>
</theory> </theory>
<theory name="Tower_of_Hanoi" sum="d2a79fec40fb0761056b76192fa05ccc" expanded="true"> <theory name="Tower_of_Hanoi" sum="f912cddeaa5714ba310fab811694e537" expanded="true">
<goal name="RevSorted.Transitive.Trans" expl=""> <goal name="RevSorted.Transitive.Trans" expl="">
<proof prover="0"><result status="valid" time="0.00" steps="3"/></proof> <proof prover="0"><result status="valid" time="0.00" steps="3"/></proof>
<proof prover="6"><result status="valid" time="0.01" steps="2"/></proof> <proof prover="6"><result status="valid" time="0.01" steps="2"/></proof>
</goal> </goal>
<goal name="VC tower" expl="VC for tower" expanded="true">
<proof prover="0"><result status="valid" time="0.00" steps="3"/></proof>
</goal>
<goal name="VC move" expl="VC for move" expanded="true"> <goal name="VC move" expl="VC for move" expanded="true">
<transf name="split_goal_wp" expanded="true"> <transf name="split_goal_wp" expanded="true">
<goal name="VC move.1" expl="type invariant"> <goal name="VC move.1" expl="type invariant">
......
...@@ -36,6 +36,12 @@ back +-+-+-+-------------------+ ...@@ -36,6 +36,12 @@ back +-+-+-+-------------------+
forall i : int. forall i : int.
0 <= i < card -> 0 <= i < card ->
0 <= back[i] < A.length values /\ index[back[i]] = i 0 <= back[i] < A.length values /\ index[back[i]] = i
} by {
values = A.make 0 (any 'a);
index = A.make 0 0;
back = A.make 0 0;
card = 0;
def = any 'a
} }
predicate is_elt (a: sparse_array 'a) (i: int) = predicate is_elt (a: sparse_array 'a) (i: int) =
......
...@@ -5,7 +5,10 @@ ...@@ -5,7 +5,10 @@
<prover id="2" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" memlimit="1000"/> <prover id="2" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="4" name="Z3" version="4.4.1" timelimit="1" steplimit="0" memlimit="1000"/> <prover id="4" name="Z3" version="4.4.1" timelimit="1" steplimit="0" memlimit="1000"/>
<file name="../vacid_0_sparse_array.mlw" expanded="true"> <file name="../vacid_0_sparse_array.mlw" expanded="true">
<theory name="SparseArray" sum="bac3050c05ed738e09d82910b1b02112" expanded="true"> <theory name="SparseArray" sum="e8b16cb41f767bffb87f7ca60d376375" expanded="true">
<goal name="VC sparse_array" expl="VC for sparse_array">
<proof prover="2"><result status="valid" time="0.00" steps="9"/></proof>
</goal>
<goal name="VC create" expl="VC for create"> <goal name="VC create" expl="VC for create">
<proof prover="2"><result status="valid" time="0.00" steps="25"/></proof> <proof prover="2"><result status="valid" time="0.00" steps="25"/></proof>
</goal> </goal>
......
...@@ -61,6 +61,7 @@ module DancingLinks ...@@ -61,6 +61,7 @@ module DancingLinks
represented by array indices *) represented by array indices *)
type dll = { prev: array int; next: array int; ghost n: int } type dll = { prev: array int; next: array int; ghost n: int }
invariant { length prev = length next = n } invariant { length prev = length next = n }
by { prev = make 0 0; next = make 0 0; n = 0 }
(** node [i] is a valid node i.e. it has consistent neighbors *) (** node [i] is a valid node i.e. it has consistent neighbors *)
predicate valid_in (l: dll) (i: int) = predicate valid_in (l: dll) (i: int) =
......
...@@ -4,7 +4,10 @@ ...@@ -4,7 +4,10 @@
<why3session shape_version="4"> <why3session shape_version="4">
<prover id="2" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" memlimit="1000"/> <prover id="2" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../verifythis_2015_dancing_links.mlw" expanded="true"> <file name="../verifythis_2015_dancing_links.mlw" expanded="true">
<theory name="DancingLinks" sum="4d6d9e4dce7f831bfe2d9977d64bab0d" expanded="true"> <theory name="DancingLinks" sum="6da03c19828ccafc3450812ec12bdd7d" expanded="true">
<goal name="VC dll" expl="VC for dll" expanded="true">
<proof prover="2"><result status="valid" time="0.00" steps="3"/></proof>
</goal>
<goal name="VC remove" expl="VC for remove" expanded="true"> <goal name="VC remove" expl="VC for remove" expanded="true">
<proof prover="2"><result status="valid" time="3.04" steps="1747"/></proof> <proof prover="2"><result status="valid" time="3.04" steps="1747"/></proof>
<transf name="split_goal_wp" expanded="true"> <transf name="split_goal_wp" expanded="true">
......
...@@ -63,6 +63,8 @@ module Caterpillar ...@@ -63,6 +63,8 @@ module Caterpillar
b.h = ch /\ b.h = ch /\
xs_len = length xs < ch /\ xs_len = length xs < ch /\
forall len. 0 <= len <= ch -> take len (xs ++ ys) = take len b.xs forall len. 0 <= len <= ch -> take len (xs ++ ys) = take len b.xs
} by {
ch = 1; xs = Nil; xs_len = 0; ys = Nil; b = empty 1
} }
(* for the three operations, the postcondition uses the default (* for the three operations, the postcondition uses the default
...@@ -126,6 +128,8 @@ module RealTime ...@@ -126,6 +128,8 @@ module RealTime
b.h = ch /\ b.h = ch /\
xs_len = length xs < ch /\ xs_len = length xs < ch /\
forall len. 0 <= len <= ch -> take len (xs ++ ys) = take len b.xs forall len. 0 <= len <= ch -> take len (xs ++ ys) = take len b.xs
} by {
ch = 1; xs = Nil; xs_len = 0; ys = Nil; b = empty 1
} }
(* garbage collection *) (* garbage collection *)
......
...@@ -47,7 +47,10 @@ ...@@ -47,7 +47,10 @@
</transf> </transf>
</goal> </goal>
</theory> </theory>
<theory name="Caterpillar" sum="9e3756c93ccea25c9afdad138a21988a"> <theory name="Caterpillar" sum="1d67f8a5b1422e0c9043537b5ab5d545" expanded="true">
<goal name="VC cat" expl="VC for cat">
<proof prover="0"><result status="valid" time="0.00" steps="6"/></proof>
</goal>
<goal name="VC cat_empty" expl="VC for cat_empty"> <goal name="VC cat_empty" expl="VC for cat_empty">
<proof prover="0"><result status="valid" time="0.01" steps="7"/></proof> <proof prover="0"><result status="valid" time="0.01" steps="7"/></proof>
</goal> </goal>
...@@ -102,7 +105,10 @@ ...@@ -102,7 +105,10 @@
<proof prover="0"><result status="valid" time="0.00" steps="8"/></proof> <proof prover="0"><result status="valid" time="0.00" steps="8"/></proof>
</goal> </goal>
</theory> </theory>
<theory name="RealTime" sum="229eeef95a917cea47a0cb02824e9fca" expanded="true"> <theory name="RealTime" sum="b99b5cbae9b2f754fab20d968a6639f3" expanded="true">
<goal name="VC rt" expl="VC for rt">
<proof prover="0"><result status="valid" time="0.00" steps="6"/></proof>
</goal>
<goal name="VC de_allocate" expl="VC for de_allocate"> <goal name="VC de_allocate" expl="VC for de_allocate">
<proof prover="0"><result status="valid" time="0.00" steps="1"/></proof> <proof prover="0"><result status="valid" time="0.00" steps="1"/></proof>
</goal> </goal>
......
...@@ -342,6 +342,7 @@ type suffixArray = { ...@@ -342,6 +342,7 @@ type suffixArray = {
invariant { values.length = suffixes.length /\ invariant { values.length = suffixes.length /\
permutation suffixes.elts suffixes.length /\ permutation suffixes.elts suffixes.length /\
SuffixSort.sorted values suffixes } SuffixSort.sorted values suffixes }
by { values = make 0 0; suffixes = make 0 0 }
let select (s:suffixArray) (i:int) : int let select (s:suffixArray) (i:int) : int
requires { 0 <= i < s.values.length } requires { 0 <= i < s.values.length }
......
...@@ -237,9 +237,8 @@ ...@@ -237,9 +237,8 @@
</goal> </goal>
<goal name="VC sort.14" expl="index in array bounds"> <goal name="VC sort.14" expl="index in array bounds">
<proof prover="3"><result status="valid" time="0.02"/></proof> <proof prover="3"><result status="valid" time="0.02"/></proof>
<proof prover="11"><result status="valid" time="0.42"/></proof> <proof prover="12"><result status="valid" time="0.00" steps="17"/></proof>
<proof prover="12"><result status="valid" time="0.01" steps="17"/></proof> <proof prover="13"><result status="valid" time="0.03"/></proof>
<proof prover="13"><result status="valid" time="0.00"/></proof>
<proof prover="14"><result status="valid" time="0.02"/></proof> <proof prover="14"><result status="valid" time="0.02"/></proof>
</goal> </goal>
<goal name="VC sort.15" expl="index in array bounds"> <goal name="VC sort.15" expl="index in array bounds">
...@@ -250,8 +249,9 @@ ...@@ -250,8 +249,9 @@
</goal> </goal>
<goal name="VC sort.16" expl="index in array bounds"> <goal name="VC sort.16" expl="index in array bounds">
<proof prover="3"><result status="valid" time="0.02"/></proof> <proof prover="3"><result status="valid" time="0.02"/></proof>
<proof prover="12"><result status="valid" time="0.00" steps="17"/></proof> <proof prover="11"><result status="valid" time="0.42"/></proof>
<proof prover="13"><result status="valid" time="0.03"/></proof> <proof prover="12"><result status="valid" time="0.01" steps="17"/></proof>
<proof prover="13"><result status="valid" time="0.00"/></proof>
<proof prover="14"><result status="valid" time="0.02"/></proof> <proof prover="14"><result status="valid" time="0.02"/></proof>
</goal> </goal>
<goal name="VC sort.17" expl="index in array bounds"> <goal name="VC sort.17" expl="index in array bounds">
...@@ -351,7 +351,10 @@ ...@@ -351,7 +351,10 @@
<proof prover="2"><result status="valid" time="0.08"/></proof> <proof prover="2"><result status="valid" time="0.08"/></proof>
</goal> </goal>
</theory> </theory>
<theory name="SuffixArray" sum="c7f7522f873a9c6b0d19391ef7745123"> <theory name="SuffixArray" sum="a43186b5d7cd87edd5fb3f19595e1847">
<goal name="VC suffixArray" expl="VC for suffixArray">
<proof prover="1"><result status="valid" time="0.01" steps="15"/></proof>
</goal>
<goal name="VC select" expl="VC for select"> <goal name="VC select" expl="VC for select">
<proof prover="3"><result status="valid" time="0.01"/></proof> <proof prover="3"><result status="valid" time="0.01"/></proof>
<proof prover="11"><result status="valid" time="0.01"/></proof> <proof prover="11"><result status="valid" time="0.01"/></proof>
......
...@@ -15,20 +15,19 @@ module AmortizedQueue ...@@ -15,20 +15,19 @@ module AmortizedQueue
type queue 'a = { front: list 'a; lenf: int; type queue 'a = { front: list 'a; lenf: int;
rear : list 'a; lenr: int; } rear : list 'a; lenr: int; }
invariant { length front = lenf >= length rear = lenr } invariant { length front = lenf >= length rear = lenr }
by { front = Nil; lenf = 0; rear = Nil; lenr = 0 }
function sequence (q: queue 'a) : list 'a = function sequence (q: queue 'a) : list 'a =
q.front ++ reverse q.rear q.front ++ reverse q.rear
let empty () ensures { sequence result = Nil } let empty () : queue 'a
= { front = Nil; lenf = 0; rear = Nil; lenr = 0 } : queue 'a ensures { sequence result = Nil }
= { front = Nil; lenf = 0; rear = Nil; lenr = 0 }
let head (q: queue 'a) let head (q: queue 'a)
requires { sequence q <> Nil } requires { sequence q <> Nil }
ensures { hd (sequence q) = Some result } ensures { hd (sequence q) = Some result }
= match q.front with = let Cons x _ = q.front in x
| Nil -> absurd
| Cons x _ -> x
end
let create (f: list 'a) (lf: int) (r: list 'a) (lr: int) let create (f: list 'a) (lf: int) (r: list 'a) (lr: int)
requires { lf = length f /\ lr = length r } requires { lf = length f /\ lr = length r }
...@@ -42,10 +41,8 @@ module AmortizedQueue ...@@ -42,10 +41,8 @@ module AmortizedQueue
let tail (q: queue 'a) let tail (q: queue 'a)
requires { sequence q <> Nil } requires { sequence q <> Nil }
ensures { tl (sequence q) = Some (sequence result) } ensures { tl (sequence q) = Some (sequence result) }
= match q.front with = let Cons _ r = q.front in
| Nil -> absurd create r (q.lenf - 1) q.rear q.lenr
| Cons _ r -> create r (q.lenf - 1) q.rear q.lenr
end
let enqueue (x: 'a) (q: queue 'a) let enqueue (x: 'a) (q: queue 'a)
ensures { sequence result = sequence q ++ Cons x Nil } ensures { sequence result = sequence q ++ Cons x Nil }
......
...@@ -4,7 +4,10 @@ ...@@ -4,7 +4,10 @@
<why3session shape_version="4"> <why3session shape_version="4">
<prover id="0" name="Alt-Ergo" version="1.30" timelimit="10" steplimit="0" memlimit="1000"/> <prover id="0" name="Alt-Ergo" version="1.30" timelimit="10" steplimit="0" memlimit="1000"/>
<file name="../vstte10_aqueue.mlw" expanded="true"> <file name="../vstte10_aqueue.mlw" expanded="true">
<theory name="AmortizedQueue" sum="e8b19e04718a27bcfcea7f31fb6f872e" expanded="true"> <theory name="AmortizedQueue" sum="5e3861c4755d0109a04d27e7daea0ce2" expanded="true">
<goal name="VC queue" expl="VC for queue" expanded="true">
<proof prover="0" timelimit="5"><result status="valid" time="0.00" steps="5"/></proof>
</goal>
<goal name="VC empty" expl="VC for empty" expanded="true"> <goal name="VC empty" expl="VC for empty" expanded="true">
<proof prover="0"><result status="valid" time="0.00" steps="17"/></proof> <proof prover="0"><result status="valid" time="0.00" steps="17"/></proof>
</goal> </goal>
......
...@@ -32,6 +32,7 @@ module RingBuffer ...@@ -32,6 +32,7 @@ module RingBuffer
(0 <= first + i - size -> (0 <= first + i - size ->
nth i sequence = Some data[first + i - size]) nth i sequence = Some data[first + i - size])
} }
by { first = 0; len = 0; data = make 1 (any 'a); sequence = Nil }
(* total capacity of the buffer *) (* total capacity of the buffer *)
function size (b: buffer 'a) : int = Array.length b.data function size (b: buffer 'a) : int = Array.length b.data
...@@ -165,6 +166,7 @@ module RingBufferSeq ...@@ -165,6 +166,7 @@ module RingBufferSeq
(0 <= first + i - size -> (0 <= first + i - size ->
S.get sequence i = data[first + i - size]) S.get sequence i = data[first + i - size])
} }
by { first = 0; len = 0; data = make 1 (any 'a); sequence = S.empty }
(* total capacity of the buffer *) (* total capacity of the buffer *)
function size (b: buffer 'a) : int = Array.length b.data function size (b: buffer 'a) : int = Array.length b.data
......
...@@ -8,7 +8,10 @@ ...@@ -8,7 +8,10 @@
<prover id="6" name="Z3" version="4.5.0" timelimit="5" steplimit="0" memlimit="1000"/> <prover id="6" name="Z3" version="4.5.0" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="9" name="Eprover" version="1.8-001" timelimit="5" steplimit="0" memlimit="1000"/> <prover id="9" name="Eprover" version="1.8-001" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../vstte12_ring_buffer.mlw" expanded="true"> <file name="../vstte12_ring_buffer.mlw" expanded="true">
<theory name="RingBuffer" sum="cf1afa8caf43dc4f538c9078462662fe" expanded="true"> <theory name="RingBuffer" sum="440c787407edb5055e7ccec38c6dd29c" expanded="true">
<goal name="VC buffer" expl="VC for buffer">
<proof prover="4"><result status="valid" time="0.00" steps="8"/></proof>
</goal>
<goal name="VC create" expl="VC for create"> <goal name="VC create" expl="VC for create">
<proof prover="4"><result status="valid" time="0.00" steps="24"/></proof> <proof prover="4"><result status="valid" time="0.00" steps="24"/></proof>
</goal> </goal>
...@@ -577,7 +580,10 @@ ...@@ -577,7 +580,10 @@
<proof prover="4"><result status="valid" time="0.08" steps="499"/></proof> <proof prover="4"><result status="valid" time="0.08" steps="499"/></proof>
</goal> </goal>
</theory> </theory>
<theory name="RingBufferSeq" sum="2e16fc317b01f2605ce592d18305265a"> <theory name="RingBufferSeq" sum="d5baed0f88a0b4cbc04d03e2e7c91df4">
<goal name="VC buffer" expl="VC for buffer">
<proof prover="4"><result status="valid" time="0.00" steps="7"/></proof>
</goal>
<goal name="VC create" expl="VC for create"> <goal name="VC create" expl="VC for create">
<proof prover="4"><result status="valid" time="0.01" steps="23"/></proof> <proof prover="4"><result status="valid" time="0.01" steps="23"/></proof>
</goal> </goal>
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment