Attention une mise à jour du serveur va être effectuée le lundi 17 mai entre 13h et 13h30. Cette mise à jour va générer une interruption du service de quelques minutes.

Commit b7cfc967 authored by MARCHE Claude's avatar MARCHE Claude

Merge branch 'master' into itp

Conflicts:
	Makefile.in
parents 0e32c288 0db24f49
......@@ -12,9 +12,13 @@ with contributions of
Sylvie Boldo
Martin Clochard
Simon Cruanes
Sylvain Dailler
Clément Fumex
Leon Gondelman
David Hauzar
Daisuke Ishii
Johannes Kanig
Mikhail Mandrykin
David Mentré
Benjamin Monate
Thi-Minh-Tuyen Nguyen
......
* marks an incompatible change
Tools
o why3 config now generates default proof strategies using the
installed provers. These are available under name "Auto level 1"
and "Auto level 2" in why3 ide.
Version 0.87.3, January ??, 2017
=================================
Version 0.87.3, January 12, 2017
================================
bug fixes
o
o fixed OCaml extraction with respect to ghost parameters
o assorted bug fixes
Provers
o support for Alt-Ergo 1.30 (released ??, 2016)
o support for Coq 8.6 (released ?, 2016)
o support for Gappa 1.3 (released ?, 2016)
provers
o support for Alt-Ergo 1.30 (released Nov 21, 2016)
o support for Coq 8.6 (released Dec 8, 2016)
o support for Gappa 1.3 (released Jul 20, 2016)
* discarded support for Isabelle 2015
o support for Isabelle 2016-1 (released Dec 2016)
o support for Z3 4.5.0 (released ? 2016)
o support for Z3 4.5.0 (released Nov 8, 2016)
Version 0.87.2, September 1, 2016
=================================
......
......@@ -1607,8 +1607,8 @@ endif
ALTERGODIR=src/trywhy3/alt-ergo
JSOCAMLC=ocamlfind ocamlc -package js_of_ocaml -package js_of_ocaml.syntax \
-syntax camlp4o -I src/trywhy3 \
JSOCAMLC=ocamlfind ocamlc -package js_of_ocaml -g -package js_of_ocaml.syntax \
-package ocplib-simplex -syntax camlp4o -I src/trywhy3 \
-I $(ALTERGODIR)/src/util \
-I $(ALTERGODIR)/src/structures \
-I $(ALTERGODIR)/src/parsing \
......@@ -1677,7 +1677,7 @@ src/trywhy3/alt_ergo_worker.js: src/trywhy3/alt_ergo_worker.byte
js_of_ocaml $(JSOO_DEBUG) +weak.js +nat.js +dynlink.js +toplevel.js $<
src/trywhy3/alt_ergo_worker.byte: $(ALTERGOCMO) src/trywhy3/worker_proto.cmo src/trywhy3/alt_ergo_worker.cmo
$(JSOCAMLC) -I +ocplib-simplex $(BFLAGS) -o $@ -linkpkg $(BLINKFLAGS) ocplibSimplex.cma $^
$(JSOCAMLC) $(BFLAGS) -o $@ -linkpkg $(BLINKFLAGS) $^
src/trywhy3/alt_ergo_worker.cmo: src/trywhy3/worker_proto.cmo
src/trywhy3/why3_worker.cmo: src/trywhy3/worker_proto.cmo
......@@ -2163,7 +2163,6 @@ MORE_DIST = configure install-sh doc/manual.pdf
dist: $(MORE_DIST)
rm -rf distrib/$(NAME)/ distrib/$(NAME).tar.gz
rm -rf distrib/$(EXTRANAME)/ distrib/$(EXTRANAME).tar.gz
mkdir -p distrib/
git archive --format tar --prefix $(NAME)/ HEAD | tar x -C distrib/
for f in $(MORE_DIST); do cp $$f distrib/$(NAME)/$$f; done
......
......@@ -108,7 +108,7 @@
%BEGIN LATEX
\begin{LARGE}
%END LATEX
Version \whyversion{}, September 2016
Version \whyversion{}, January 2017
%BEGIN LATEX
\end{LARGE}
%END LATEX
......
(** Binary sort
Binary sort is a variant of insertion sort where binary search is used
to find the insertion point. This lowers the number of comparisons
(from N^2 to N log(N)) and thus is useful when comparisons are costly.
For instance, Binary sort is used as an ingredient in Java 8's
TimSort implementation (which is the library sort for Object[]).
Author: Jean-Christophe Filliâtre (CNRS)
*)
module BinarySort
use import int.Int
use import int.ComputerDivision
use import ref.Ref
use import array.Array
use import array.ArrayPermut
let lemma occ_shift (m1 m2: M.map int 'a) (mid k: int) (x: 'a) : unit
requires { 0 <= mid <= k }
requires { forall i. mid < i <= k -> M.get m2 i = M.get m1 (i - 1) }
requires { M.get m2 mid = M.get m1 k }
ensures { M.Occ.occ x m1 mid (k+1) = M.Occ.occ x m2 mid (k+1) }
= for i = mid to Int.(-) k 1 do
invariant { M.Occ.occ x m1 mid i = M.Occ.occ x m2 (mid+1) (i+1) }
()
done;
assert { M.Occ.occ (M.get m1 k) m1 mid (k+1) =
1 + M.Occ.occ (M.get m1 k) m1 mid k };
assert { M.Occ.occ (M.get m1 k) m2 mid (k+1) =
1 + M.Occ.occ (M.get m1 k) m2 (mid+1) (k+1) };
assert { M.Occ.occ x m1 mid (k+1) = M.Occ.occ x m2 mid (k+1)
by x = M.get m1 k \/ x <> M.get m1 k }
let binary_sort (a: array int) : unit
ensures { forall i j. 0 <= i <= j < length a -> a[i] <= a[j] }
ensures { permut_sub (old a) a 0 (length a) }
=
'Init:
for k = 1 to length a - 1 do
(* a[0..k-1) is sorted; insert a[k] *)
invariant { forall i j. 0 <= i <= j < k -> a[i] <= a[j] }
invariant { permut_sub (at a 'Init) a 0 (length a) }
let v = a[k] in
let left = ref 0 in
let right = ref k in
while !left < !right do
invariant { 0 <= !left <= !right <= k }
invariant { forall i. 0 <= i < !left -> a[i] <= v }
invariant { forall i. !right <= i < k -> v < a[i] }
variant { !right - !left }
let mid = !left + div (!right - !left) 2 in
if v < a[mid] then right := mid else left := mid + 1
done;
(* !left is the place where to insert value v
so we move a[!left..k) one position to the right *)
'L:
self_blit a !left (!left + 1) (k - !left);
a[!left] <- v;
assert { permut_sub (at a 'L) a !left (k + 1) };
assert { permut_sub (at a 'L) a 0 (length a) };
done
end
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="CVC4" version="1.4" timelimit="6" steplimit="0" memlimit="1000"/>
<prover id="1" name="Alt-Ergo" version="1.30" timelimit="6" steplimit="0" memlimit="1000"/>
<file name="../binary_sort.mlw" expanded="true">
<theory name="BinarySort" sum="fdb3a37048a74a0a24a69ddbeedfed40" expanded="true">
<goal name="WP_parameter occ_shift" expl="VC for occ_shift" expanded="true">
<transf name="split_goal_wp">
<goal name="WP_parameter occ_shift.1" expl="1. assertion">
<proof prover="1"><result status="valid" time="0.01" steps="11"/></proof>
</goal>
<goal name="WP_parameter occ_shift.2" expl="2. assertion">
<proof prover="1"><result status="valid" time="0.02" steps="14"/></proof>
</goal>
<goal name="WP_parameter occ_shift.3" expl="3. assertion">
<proof prover="1"><result status="valid" time="0.00" steps="8"/></proof>
</goal>
<goal name="WP_parameter occ_shift.4" expl="4. postcondition">
<proof prover="1"><result status="valid" time="0.01" steps="8"/></proof>
</goal>
<goal name="WP_parameter occ_shift.5" expl="5. loop invariant init">
<proof prover="1"><result status="valid" time="0.01" steps="6"/></proof>
</goal>
<goal name="WP_parameter occ_shift.6" expl="6. loop invariant preservation">
<proof prover="1"><result status="valid" time="0.06" steps="83"/></proof>
</goal>
<goal name="WP_parameter occ_shift.7" expl="7. assertion">
<proof prover="1"><result status="valid" time="0.01" steps="11"/></proof>
</goal>
<goal name="WP_parameter occ_shift.8" expl="8. assertion">
<proof prover="0"><result status="valid" time="0.24"/></proof>
</goal>
<goal name="WP_parameter occ_shift.9" expl="9. assertion">
<proof prover="0"><result status="valid" time="0.50"/></proof>
</goal>
<goal name="WP_parameter occ_shift.10" expl="10. postcondition">
<proof prover="1"><result status="valid" time="0.01" steps="9"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter binary_sort" expl="VC for binary_sort">
<transf name="split_goal_wp">
<goal name="WP_parameter binary_sort.1" expl="1. postcondition">
<proof prover="1"><result status="valid" time="0.01" steps="6"/></proof>
</goal>
<goal name="WP_parameter binary_sort.2" expl="2. postcondition">
<proof prover="1"><result status="valid" time="0.01" steps="14"/></proof>
</goal>
<goal name="WP_parameter binary_sort.3" expl="3. loop invariant init">
<proof prover="1"><result status="valid" time="0.00" steps="6"/></proof>
</goal>
<goal name="WP_parameter binary_sort.4" expl="4. loop invariant init">
<proof prover="1"><result status="valid" time="0.01" steps="14"/></proof>
</goal>
<goal name="WP_parameter binary_sort.5" expl="5. type invariant">
<proof prover="1"><result status="valid" time="0.00" steps="6"/></proof>
</goal>
<goal name="WP_parameter binary_sort.6" expl="6. index in array bounds">
<proof prover="1"><result status="valid" time="0.00" steps="6"/></proof>
</goal>
<goal name="WP_parameter binary_sort.7" expl="7. loop invariant init">
<proof prover="1"><result status="valid" time="0.01" steps="7"/></proof>
</goal>
<goal name="WP_parameter binary_sort.8" expl="8. loop invariant init">
<proof prover="1"><result status="valid" time="0.00" steps="7"/></proof>
</goal>
<goal name="WP_parameter binary_sort.9" expl="9. loop invariant init">
<proof prover="1"><result status="valid" time="0.00" steps="7"/></proof>
</goal>
<goal name="WP_parameter binary_sort.10" expl="10. index in array bounds">
<proof prover="1"><result status="valid" time="0.01" steps="20"/></proof>
</goal>
<goal name="WP_parameter binary_sort.11" expl="11. loop invariant preservation">
<proof prover="1"><result status="valid" time="0.01" steps="50"/></proof>
</goal>
<goal name="WP_parameter binary_sort.12" expl="12. loop invariant preservation">
<proof prover="1"><result status="valid" time="0.04" steps="22"/></proof>
</goal>
<goal name="WP_parameter binary_sort.13" expl="13. loop invariant preservation">
<proof prover="1"><result status="valid" time="0.01" steps="23"/></proof>
</goal>
<goal name="WP_parameter binary_sort.14" expl="14. loop variant decrease">
<proof prover="1"><result status="valid" time="0.04" steps="35"/></proof>
</goal>
<goal name="WP_parameter binary_sort.15" expl="15. loop invariant preservation">
<proof prover="1"><result status="valid" time="0.02" steps="36"/></proof>
</goal>
<goal name="WP_parameter binary_sort.16" expl="16. loop invariant preservation">
<proof prover="1"><result status="valid" time="0.02" steps="69"/></proof>
</goal>
<goal name="WP_parameter binary_sort.17" expl="17. loop invariant preservation">
<proof prover="1"><result status="valid" time="0.01" steps="22"/></proof>
</goal>
<goal name="WP_parameter binary_sort.18" expl="18. loop variant decrease">
<proof prover="1"><result status="valid" time="0.02" steps="28"/></proof>
</goal>
<goal name="WP_parameter binary_sort.19" expl="19. precondition">
<proof prover="1"><result status="valid" time="0.00" steps="11"/></proof>
</goal>
<goal name="WP_parameter binary_sort.20" expl="20. precondition">
<proof prover="1"><result status="valid" time="0.01" steps="11"/></proof>
</goal>
<goal name="WP_parameter binary_sort.21" expl="21. index in array bounds">
<proof prover="1"><result status="valid" time="0.00" steps="15"/></proof>
</goal>
<goal name="WP_parameter binary_sort.22" expl="22. assertion">
<proof prover="1"><result status="valid" time="0.57" steps="174"/></proof>
</goal>
<goal name="WP_parameter binary_sort.23" expl="23. assertion">
<proof prover="1"><result status="valid" time="0.01" steps="26"/></proof>
</goal>
<goal name="WP_parameter binary_sort.24" expl="24. loop invariant preservation">
<proof prover="1"><result status="valid" time="0.12" steps="203"/></proof>
</goal>
<goal name="WP_parameter binary_sort.25" expl="25. loop invariant preservation">
<proof prover="1"><result status="valid" time="0.02" steps="65"/></proof>
</goal>
<goal name="WP_parameter binary_sort.26" expl="26. type invariant">
<proof prover="1"><result status="valid" time="0.00" steps="4"/></proof>
</goal>
<goal name="WP_parameter binary_sort.27" expl="27. postcondition">
<proof prover="1"><result status="valid" time="0.00" steps="13"/></proof>
</goal>
<goal name="WP_parameter binary_sort.28" expl="28. postcondition">
<proof prover="1"><result status="valid" time="0.01" steps="4"/></proof>
</goal>
</transf>
</goal>
</theory>
</file>
</why3session>
......@@ -13,20 +13,20 @@ module BubbleSort
let bubble_sort (a: array int)
ensures { permut_all (old a) a }
ensures { permut_all (old a) a }
ensures { sorted a }
= 'Init:
for i = length a - 1 downto 1 do
invariant { permut_all (at a 'Init) a }
invariant { sorted_sub a i (length a) }
invariant { forall k1 k2: int.
0 <= k1 <= i < k2 < length a -> a[k1] <= a[k2]
invariant { forall k1 k2: int.
0 <= k1 <= i < k2 < length a -> a[k1] <= a[k2]
}
for j = 0 to i - 1 do
invariant { permut_all (at a 'Init) a }
invariant { sorted_sub a i (length a) }
invariant { forall k1 k2: int.
0 <= k1 <= i < k2 < length a -> a[k1] <= a[k2]
invariant { forall k1 k2: int.
0 <= k1 <= i < k2 < length a -> a[k1] <= a[k2]
}
invariant { forall k. 0 <= k <= j -> a[k] <= a[j] }
if a[j] > a[j+1] then swap a j (j+1);
......@@ -35,7 +35,7 @@ module BubbleSort
let test1 () =
let a = make 3 0 in
a[0] <- 7; a[1] <- 3; a[2] <- 1;
a[0] <- 7; a[1] <- 3; a[2] <- 1;
bubble_sort a;
a
......
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below *)
Require Import BuiltIn.
Require BuiltIn.
Require map.Map.
Require int.Int.
Require list.List.
Require list.Length.
Require list.Mem.
Require list.Append.
(* Why3 assumption *)
Definition unit := unit.
(* Why3 assumption *)
Inductive color :=
| White : color
| Black : color.
Axiom color_WhyType : WhyType color.
Existing Instance color_WhyType.
(* Why3 assumption *)
Inductive forest :=
| E : forest
| N : Z -> forest -> forest -> forest.
Axiom forest_WhyType : WhyType forest.
Existing Instance forest_WhyType.
(* Why3 assumption *)
Definition coloring := (map.Map.map Z color).
(* Why3 assumption *)
Fixpoint size_forest (f:forest) {struct f}: Z :=
match f with
| E => 0%Z
| (N _ f1 f2) => ((1%Z + (size_forest f1))%Z + (size_forest f2))%Z
end.
Axiom size_forest_nonneg : forall (f:forest), (0%Z <= (size_forest f))%Z.
(* Why3 assumption *)
Fixpoint mem_forest (n:Z) (f:forest) {struct f}: Prop :=
match f with
| E => False
| (N i f1 f2) => (i = n) \/ ((mem_forest n f1) \/ (mem_forest n f2))
end.
(* Why3 assumption *)
Definition between_range_forest (i:Z) (j:Z) (f:forest): Prop := forall (n:Z),
(mem_forest n f) -> ((i <= n)%Z /\ (n < j)%Z).
(* Why3 assumption *)
Definition disjoint (f1:forest) (f2:forest): Prop := forall (x:Z),
(mem_forest x f1) -> ~ (mem_forest x f2).
(* Why3 assumption *)
Fixpoint no_repeated_forest (f:forest) {struct f}: Prop :=
match f with
| E => True
| (N i f1 f2) => (no_repeated_forest f1) /\ ((no_repeated_forest f2) /\
((~ (mem_forest i f1)) /\ ((~ (mem_forest i f2)) /\ (disjoint f1 f2))))
end.
(* Why3 assumption *)
Definition valid_nums_forest (f:forest) (n:Z): Prop := (between_range_forest
0%Z n f) /\ (no_repeated_forest f).
(* Why3 assumption *)
Fixpoint white_forest (f:forest) (c:(map.Map.map Z
color)) {struct f}: Prop :=
match f with
| E => True
| (N i f1 f2) => ((map.Map.get c i) = White) /\ ((white_forest f1 c) /\
(white_forest f2 c))
end.
(* Why3 assumption *)
Fixpoint valid_coloring (f:forest) (c:(map.Map.map Z
color)) {struct f}: Prop :=
match f with
| E => True
| (N i f1 f2) => (valid_coloring f2 c) /\ match (map.Map.get c
i) with
| White => (white_forest f1 c)
| Black => (valid_coloring f1 c)
end
end.
(* Why3 assumption *)
Fixpoint count_forest (f:forest) {struct f}: Z :=
match f with
| E => 1%Z
| (N _ f1 f2) => ((1%Z + (count_forest f1))%Z * (count_forest f2))%Z
end.
Axiom count_forest_nonneg : forall (f:forest), (1%Z <= (count_forest f))%Z.
(* Why3 assumption *)
Definition eq_coloring (n:Z) (c1:(map.Map.map Z color)) (c2:(map.Map.map Z
color)): Prop := forall (i:Z), ((0%Z <= i)%Z /\ (i < n)%Z) ->
((map.Map.get c1 i) = (map.Map.get c2 i)).
(* Why3 assumption *)
Definition stack := (list forest).
(* Why3 assumption *)
Fixpoint mem_stack (n:Z) (st:(list forest)) {struct st}: Prop :=
match st with
| Init.Datatypes.nil => False
| (Init.Datatypes.cons f tl) => (mem_forest n f) \/ (mem_stack n tl)
end.
Axiom mem_app : forall (n:Z) (st1:(list forest)) (st2:(list forest)),
(mem_stack n (Init.Datatypes.app st1 st2)) -> ((mem_stack n st1) \/
(mem_stack n st2)).
(* Why3 assumption *)
Fixpoint size_stack (st:(list forest)) {struct st}: Z :=
match st with
| Init.Datatypes.nil => 0%Z
| (Init.Datatypes.cons f st1) => ((size_forest f) + (size_stack st1))%Z
end.
Axiom size_stack_nonneg : forall (st:(list forest)),
(0%Z <= (size_stack st))%Z.
Axiom white_forest_equiv : forall (f:forest) (c:(map.Map.map Z color)),
(white_forest f c) <-> forall (i:Z), (mem_forest i f) -> ((map.Map.get c
i) = White).
(* Why3 assumption *)
Fixpoint even_forest (f:forest) {struct f}: Prop :=
match f with
| E => False
| (N _ f1 f2) => (~ (even_forest f1)) \/ (even_forest f2)
end.
(* Why3 assumption *)
Fixpoint final_forest (f:forest) (c:(map.Map.map Z
color)) {struct f}: Prop :=
match f with
| E => True
| (N i f1 f2) => ((map.Map.get c i) = Black) /\ ((final_forest f1 c) /\
(((~ (even_forest f1)) -> (white_forest f2 c)) /\ ((even_forest f1) ->
(final_forest f2 c))))
end.
(* Why3 assumption *)
Definition any_forest (f:forest) (c:(map.Map.map Z color)): Prop :=
(white_forest f c) \/ (final_forest f c).
Axiom any_forest_frame : forall (f:forest) (c1:(map.Map.map Z color))
(c2:(map.Map.map Z color)), (forall (i:Z), (mem_forest i f) ->
((map.Map.get c1 i) = (map.Map.get c2 i))) -> (((final_forest f c1) ->
(final_forest f c2)) /\ ((white_forest f c1) -> (white_forest f c2))).
(* Why3 assumption *)
Definition unchanged (st:(list forest)) (c1:(map.Map.map Z color))
(c2:(map.Map.map Z color)): Prop := forall (i:Z), (mem_stack i st) ->
((map.Map.get c1 i) = (map.Map.get c2 i)).
(* Why3 assumption *)
Fixpoint inverse (st:(list forest)) (c1:(map.Map.map Z color))
(c2:(map.Map.map Z color)) {struct st}: Prop :=
match st with
| Init.Datatypes.nil => True
| (Init.Datatypes.cons f st') => (((white_forest f c1) /\ (final_forest f
c2)) \/ ((final_forest f c1) /\ (white_forest f c2))) /\ (((even_forest
f) -> (unchanged st' c1 c2)) /\ ((~ (even_forest f)) -> (inverse st' c1
c2)))
end.
(* Why3 assumption *)
Fixpoint any_stack (st:(list forest)) (c:(map.Map.map Z
color)) {struct st}: Prop :=
match st with
| Init.Datatypes.nil => True
| (Init.Datatypes.cons f st1) => ((white_forest f c) \/ (final_forest f
c)) /\ (any_stack st1 c)
end.
Axiom any_stack_frame : forall (st:(list forest)) (c1:(map.Map.map Z color))
(c2:(map.Map.map Z color)), (unchanged st c1 c2) -> ((any_stack st c1) ->
(any_stack st c2)).
Axiom inverse_frame : forall (st:(list forest)) (c1:(map.Map.map Z color))
(c2:(map.Map.map Z color)) (c3:(map.Map.map Z color)), (inverse st c1
c2) -> ((unchanged st c2 c3) -> (inverse st c1 c3)).
Axiom inverse_frame2 : forall (st:(list forest)) (c1:(map.Map.map Z color))
(c2:(map.Map.map Z color)) (c3:(map.Map.map Z color)), (unchanged st c1
c2) -> ((inverse st c2 c3) -> (inverse st c1 c3)).
Axiom inverse_any : forall (st:(list forest)) (c1:(map.Map.map Z color))
(c2:(map.Map.map Z color)), ((any_stack st c1) /\ (inverse st c1 c2)) ->
(any_stack st c2).
Axiom inverse_final : forall (f:forest) (st:(list forest)) (c1:(map.Map.map Z
color)) (c2:(map.Map.map Z color)), (final_forest f c1) -> ((inverse
(Init.Datatypes.cons f st) c1 c2) -> (white_forest f c2)).
Axiom inverse_white : forall (f:forest) (st:(list forest)) (c1:(map.Map.map Z
color)) (c2:(map.Map.map Z color)), (white_forest f c1) -> ((inverse
(Init.Datatypes.cons f st) c1 c2) -> (final_forest f c2)).
Axiom white_final_exclusive : forall (f:forest) (c:(map.Map.map Z color)),
(~ (f = E)) -> ((white_forest f c) -> ~ (final_forest f c)).
Axiom final_unique : forall (f:forest) (c1:(map.Map.map Z color))
(c2:(map.Map.map Z color)), (final_forest f c1) -> ((final_forest f c2) ->
forall (i:Z), (mem_forest i f) -> ((map.Map.get c1 i) = (map.Map.get c2
i))).
Axiom inverse_inverse : forall (st:(list forest)) (c1:(map.Map.map Z color))
(c2:(map.Map.map Z color)) (c3:(map.Map.map Z color)), ((inverse st c1
c2) /\ (inverse st c2 c3)) -> (unchanged st c1 c3).
(* Why3 assumption *)
Inductive sub: (list forest) -> forest -> (map.Map.map Z color) -> Prop :=
| Sub_reflex : forall (f:forest) (c:(map.Map.map Z color)), (sub
(Init.Datatypes.cons f Init.Datatypes.nil) f c)
| Sub_brother : forall (st:(list forest)) (i:Z) (f1:forest) (f2:forest)
(c:(map.Map.map Z color)), (sub st f2 c) -> (sub st (N i f1 f2) c)
| Sub_append : forall (st:(list forest)) (i:Z) (f1:forest) (f2:forest)
(c:(map.Map.map Z color)), (sub st f1 c) -> (((map.Map.get c
i) = Black) -> (sub
(Init.Datatypes.app st (Init.Datatypes.cons f2 Init.Datatypes.nil))
(N i f1 f2) c)).
Axiom sub_not_nil : forall (f:forest) (c:(map.Map.map Z color)), ~ (sub
Init.Datatypes.nil f c).
Axiom sub_empty : forall (st:(list forest)) (f0:forest) (c:(map.Map.map Z
color)), (~ (st = Init.Datatypes.nil)) -> ((sub (Init.Datatypes.cons E st)
f0 c) -> (sub st f0 c)).
Axiom sub_mem : forall (n:Z) (st:(list forest)) (f:forest) (c:(map.Map.map Z
color)), (mem_stack n st) -> ((sub st f c) -> (mem_forest n f)).
Axiom sub_weaken1 : forall (st:(list forest)) (i:Z) (f1:forest) (f2:forest)
(f0:forest) (c:(map.Map.map Z color)), (sub (Init.Datatypes.cons (N i f1
f2) st) f0 c) -> (sub (Init.Datatypes.cons f2 st) f0 c).
Axiom sub_weaken2 : forall (st:(list forest)) (i:Z) (f1:forest) (f2:forest)
(f0:forest) (c:(map.Map.map Z color)), (sub (Init.Datatypes.cons (N i f1
f2) st) f0 c) -> (((map.Map.get c i) = Black) -> (sub
(Init.Datatypes.cons f1 (Init.Datatypes.cons f2 st)) f0 c)).
Axiom not_mem_st : forall (i: