Commit 01f3e01b authored by Sylvain Dailler's avatar Sylvain Dailler
Browse files

Fix obsolete session and coq proofs

parent 5e28a254
......@@ -23,7 +23,7 @@
</theory>
<theory name="BinarySearchInt32" proved="true">
<goal name="VC binary_search" expl="VC for binary_search" proved="true">
<proof prover="0"><result status="valid" time="2.65" steps="9890"/></proof>
<proof prover="0"><result status="valid" time="0.50" steps="1797"/></proof>
</goal>
</theory>
<theory name="BinarySearchBoolean" proved="true">
......
......@@ -778,13 +778,13 @@
<proof prover="0"><result status="valid" time="0.05"/></proof>
<proof prover="4"><result status="valid" time="0.11"/></proof>
<proof prover="5"><result status="valid" time="0.01"/></proof>
<proof prover="6" timelimit="5"><result status="valid" time="0.09" steps="81"/></proof>
<proof prover="6" timelimit="5"><result status="valid" time="0.09" steps="80"/></proof>
</goal>
<goal name="VC ascii.1" expl="assertion" proved="true">
<proof prover="0"><result status="valid" time="0.10"/></proof>
</goal>
<goal name="VC ascii.2" expl="assertion" proved="true">
<proof prover="6"><result status="valid" time="0.18" steps="403"/></proof>
<proof prover="6"><result status="valid" time="0.18" steps="432"/></proof>
</goal>
<goal name="VC ascii.3" expl="assertion" proved="true">
<transf name="split_goal_right" proved="true" >
......@@ -795,7 +795,7 @@
</goal>
<goal name="VC ascii.3.1" expl="assertion" proved="true">
<proof prover="4"><result status="valid" time="0.14"/></proof>
<proof prover="6" timelimit="5"><result status="valid" time="0.04" steps="157"/></proof>
<proof prover="6" timelimit="5"><result status="valid" time="0.04" steps="158"/></proof>
</goal>
<goal name="VC ascii.3.2" expl="assertion" proved="true">
<proof prover="0"><result status="valid" time="0.17"/></proof>
......@@ -812,12 +812,12 @@
</goal>
<goal name="VC ascii.5" expl="postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.11"/></proof>
<proof prover="4"><result status="valid" time="1.91"/></proof>
<proof prover="4"><result status="valid" time="1.41"/></proof>
</goal>
<goal name="VC ascii.6" expl="postcondition" proved="true">
<proof prover="4"><result status="valid" time="0.71"/></proof>
<proof prover="5"><result status="valid" time="0.06"/></proof>
<proof prover="6"><result status="valid" time="0.21" steps="374"/></proof>
<proof prover="6"><result status="valid" time="0.21" steps="378"/></proof>
</goal>
</transf>
</goal>
......
......@@ -166,7 +166,7 @@
<proof prover="11"><result status="valid" time="0.80"/></proof>
</goal>
<goal name="VC peek.17" expl="loop invariant preservation" proved="true">
<proof prover="2"><result status="valid" time="0.25" steps="651"/></proof>
<proof prover="2"><result status="valid" time="0.25" steps="652"/></proof>
</goal>
<goal name="VC peek.18" expl="loop invariant preservation" proved="true">
<proof prover="11"><result status="valid" time="0.03"/></proof>
......@@ -239,17 +239,17 @@
<goal name="VC poke_8bit_array.5.0" expl="postcondition" proved="true">
<transf name="case" proved="true" arg1="(div i 8 = o)">
<goal name="VC poke_8bit_array.5.0.0" expl="true case (postcondition)" proved="true">
<proof prover="0"><result status="valid" time="0.15" steps="267"/></proof>
<proof prover="0"><result status="valid" time="0.15" steps="265"/></proof>
</goal>
<goal name="VC poke_8bit_array.5.0.1" expl="false case (postcondition)" proved="true">
<proof prover="0"><result status="valid" time="0.12" steps="181"/></proof>
<proof prover="0"><result status="valid" time="0.12" steps="182"/></proof>
</goal>
</transf>
</goal>
</transf>
</goal>
<goal name="VC poke_8bit_array.6" expl="postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.10" steps="174"/></proof>
<proof prover="0"><result status="valid" time="0.10" steps="170"/></proof>
</goal>
</transf>
</goal>
......
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="5">
<file name="../138.mlw">
<why3session shape_version="6">
<file>
<path name=".."/>
<path name="138.mlw"/>
<theory name="Test">
<goal name="VC f" expl="VC for f">
</goal>
......
......@@ -220,10 +220,10 @@
<proof prover="0"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC add_big.2" expl="integer overflow" proved="true">
<proof prover="0"><result status="valid" time="0.04"/></proof>
<proof prover="0"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC add_big.3" expl="integer overflow" proved="true">
<proof prover="0"><result status="valid" time="0.03"/></proof>
<proof prover="0"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC add_big.4" expl="type invariant" proved="true">
<proof prover="0"><result status="valid" time="0.03"/></proof>
......@@ -260,10 +260,10 @@
<proof prover="0"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC add_big.10" expl="integer overflow" proved="true">
<proof prover="0"><result status="valid" time="0.03"/></proof>
<proof prover="0"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC add_big.11" expl="integer overflow" proved="true">
<proof prover="0"><result status="valid" time="0.04"/></proof>
<proof prover="0"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC add_big.12" expl="type invariant" proved="true">
<proof prover="0"><result status="valid" time="0.04"/></proof>
......@@ -321,10 +321,10 @@
<proof prover="0"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC delta.11" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.05"/></proof>
<proof prover="0"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC delta.12" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.04"/></proof>
<proof prover="0"><result status="valid" time="0.05"/></proof>
</goal>
<goal name="VC delta.13" expl="integer overflow" proved="true">
<proof prover="0"><result status="valid" time="0.02"/></proof>
......@@ -367,7 +367,7 @@
<proof prover="0"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC fulcrum.2" expl="loop invariant init" proved="true">
<proof prover="0"><result status="valid" time="0.03"/></proof>
<proof prover="0"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC fulcrum.3" expl="index in array bounds" proved="true">
<proof prover="0"><result status="valid" time="0.03"/></proof>
......@@ -394,7 +394,7 @@
<proof prover="0"><result status="valid" time="0.05"/></proof>
</goal>
<goal name="VC fulcrum.11" expl="loop invariant init" proved="true">
<proof prover="0"><result status="valid" time="0.04"/></proof>
<proof prover="0"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC fulcrum.12" expl="loop invariant init" proved="true">
<proof prover="0"><result status="valid" time="0.02"/></proof>
......@@ -436,7 +436,7 @@
<proof prover="0"><result status="valid" time="0.20"/></proof>
</goal>
<goal name="VC fulcrum.25" expl="loop invariant preservation" proved="true">
<proof prover="3"><result status="valid" time="1.34"/></proof>
<proof prover="3"><result status="valid" time="0.05"/></proof>
</goal>
<goal name="VC fulcrum.26" expl="loop invariant preservation" proved="true">
<proof prover="0"><result status="valid" time="0.04"/></proof>
......@@ -445,7 +445,7 @@
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC fulcrum.28" expl="loop invariant preservation" proved="true">
<proof prover="2"><result status="valid" time="0.01" steps="61"/></proof>
<proof prover="2"><result status="valid" time="0.01" steps="58"/></proof>
</goal>
<goal name="VC fulcrum.29" expl="loop invariant preservation" proved="true">
<proof prover="0"><result status="valid" time="0.02"/></proof>
......@@ -454,16 +454,16 @@
<proof prover="0"><result status="valid" time="0.18"/></proof>
</goal>
<goal name="VC fulcrum.31" expl="loop invariant preservation" proved="true">
<proof prover="3"><result status="valid" time="0.49"/></proof>
<proof prover="3"><result status="valid" time="0.17"/></proof>
</goal>
<goal name="VC fulcrum.32" expl="loop invariant preservation" proved="true">
<proof prover="0"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC fulcrum.33" expl="loop invariant preservation" proved="true">
<proof prover="2"><result status="valid" time="0.02" steps="51"/></proof>
<proof prover="2"><result status="valid" time="0.02" steps="48"/></proof>
</goal>
<goal name="VC fulcrum.34" expl="loop invariant preservation" proved="true">
<proof prover="2"><result status="valid" time="0.01" steps="55"/></proof>
<proof prover="2"><result status="valid" time="0.01" steps="52"/></proof>
</goal>
<goal name="VC fulcrum.35" expl="postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.02"/></proof>
......@@ -472,10 +472,10 @@
<proof prover="0"><result status="valid" time="0.06"/></proof>
</goal>
<goal name="VC fulcrum.37" expl="out of loop bounds" proved="true">
<proof prover="0"><result status="valid" time="0.03"/></proof>
<proof prover="0"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC fulcrum.38" expl="out of loop bounds" proved="true">
<proof prover="0"><result status="valid" time="0.04"/></proof>
<proof prover="0"><result status="valid" time="0.03"/></proof>
</goal>
</transf>
</goal>
......
......@@ -60,7 +60,7 @@
</theory>
<theory name="McCarthy91Mach" proved="true">
<goal name="VC f91" expl="VC for f91" proved="true">
<proof prover="3" timelimit="5"><result status="valid" time="0.07" steps="667"/></proof>
<proof prover="3" timelimit="5"><result status="valid" time="0.07" steps="293"/></proof>
</goal>
<goal name="VC f91_nonrec" expl="VC for f91_nonrec" proved="true">
<transf name="split_vc" proved="true" >
......@@ -68,22 +68,22 @@
<proof prover="3"><result status="valid" time="0.00" steps="6"/></proof>
</goal>
<goal name="VC f91_nonrec.1" expl="integer overflow" proved="true">
<proof prover="3"><result status="valid" time="0.00" steps="15"/></proof>
<proof prover="3"><result status="valid" time="0.00" steps="13"/></proof>
</goal>
<goal name="VC f91_nonrec.2" expl="loop variant decrease" proved="true">
<proof prover="3"><result status="valid" time="0.00" steps="13"/></proof>
<proof prover="3"><result status="valid" time="0.00" steps="11"/></proof>
</goal>
<goal name="VC f91_nonrec.3" expl="loop invariant preservation" proved="true">
<proof prover="3"><result status="valid" time="0.02" steps="72"/></proof>
<proof prover="3"><result status="valid" time="0.02" steps="58"/></proof>
</goal>
<goal name="VC f91_nonrec.4" expl="integer overflow" proved="true">
<proof prover="3"><result status="valid" time="0.01" steps="14"/></proof>
<proof prover="3"><result status="valid" time="0.01" steps="12"/></proof>
</goal>
<goal name="VC f91_nonrec.5" expl="loop variant decrease" proved="true">
<proof prover="3"><result status="valid" time="0.00" steps="13"/></proof>
<proof prover="3"><result status="valid" time="0.00" steps="11"/></proof>
</goal>
<goal name="VC f91_nonrec.6" expl="loop invariant preservation" proved="true">
<proof prover="3"><result status="valid" time="2.60" steps="3489"/></proof>
<proof prover="3"><result status="valid" time="1.60" steps="1960"/></proof>
</goal>
<goal name="VC f91_nonrec.7" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.00" steps="22"/></proof>
......@@ -91,7 +91,7 @@
</transf>
</goal>
<goal name="VC f91_pseudorec" expl="VC for f91_pseudorec" proved="true">
<proof prover="3" timelimit="5"><result status="valid" time="0.08" steps="311"/></proof>
<proof prover="3" timelimit="5"><result status="valid" time="0.08" steps="222"/></proof>
</goal>
</theory>
</file>
......
......@@ -5,265 +5,10 @@ Require BuiltIn.
Require HighOrd.
Require int.Int.
Require map.Map.
Axiom fset : forall (a:Type), Type.
Parameter fset_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (fset a).
Existing Instance fset_WhyType.
Parameter mem: forall {a:Type} {a_WT:WhyType a}, a -> fset a -> Prop.
(* Why3 assumption *)
Definition infix_eqeq {a:Type} {a_WT:WhyType a} (s1:fset a) (s2:fset a) :
Prop :=
forall (x:a), mem x s1 <-> mem x s2.
Axiom extensionality :
forall {a:Type} {a_WT:WhyType a},
forall (s1:fset a) (s2:fset a), infix_eqeq s1 s2 -> (s1 = s2).
(* Why3 assumption *)
Definition subset {a:Type} {a_WT:WhyType a} (s1:fset a) (s2:fset a) : Prop :=
forall (x:a), mem x s1 -> mem x s2.
Axiom subset_refl :
forall {a:Type} {a_WT:WhyType a}, forall (s:fset a), subset s s.
Axiom subset_trans :
forall {a:Type} {a_WT:WhyType a},
forall (s1:fset a) (s2:fset a) (s3:fset a), subset s1 s2 -> subset s2 s3 ->
subset s1 s3.
(* Why3 assumption *)
Definition is_empty {a:Type} {a_WT:WhyType a} (s:fset a) : Prop :=
forall (x:a), ~ mem x s.
Parameter empty: forall {a:Type} {a_WT:WhyType a}, fset a.
Axiom is_empty_empty :
forall {a:Type} {a_WT:WhyType a}, is_empty (empty : fset a).
Axiom empty_is_empty :
forall {a:Type} {a_WT:WhyType a},
forall (s:fset a), is_empty s -> (s = (empty : fset a)).
Parameter add: forall {a:Type} {a_WT:WhyType a}, a -> fset a -> fset a.
Axiom add_def :
forall {a:Type} {a_WT:WhyType a},
forall (x:a) (s:fset a) (y:a), mem y (add x s) <-> mem y s \/ (y = x).
Axiom mem_singleton :
forall {a:Type} {a_WT:WhyType a},
forall (x:a) (y:a), mem y (add x (empty : fset a)) -> (y = x).
Parameter remove: forall {a:Type} {a_WT:WhyType a}, a -> fset a -> fset a.
Axiom remove_def :
forall {a:Type} {a_WT:WhyType a},
forall (x:a) (s:fset a) (y:a), mem y (remove x s) <-> mem y s /\ ~ (y = x).
Axiom add_remove :
forall {a:Type} {a_WT:WhyType a},
forall (x:a) (s:fset a), mem x s -> ((add x (remove x s)) = s).
Axiom remove_add :
forall {a:Type} {a_WT:WhyType a},
forall (x:a) (s:fset a), ((remove x (add x s)) = (remove x s)).
Axiom subset_remove :
forall {a:Type} {a_WT:WhyType a},
forall (x:a) (s:fset a), subset (remove x s) s.
Parameter union:
forall {a:Type} {a_WT:WhyType a}, fset a -> fset a -> fset a.
Axiom union_def :
forall {a:Type} {a_WT:WhyType a},
forall (s1:fset a) (s2:fset a) (x:a),
mem x (union s1 s2) <-> mem x s1 \/ mem x s2.
Axiom subset_union_1 :
forall {a:Type} {a_WT:WhyType a},
forall (s1:fset a) (s2:fset a), subset s1 (union s1 s2).
Axiom subset_union_2 :
forall {a:Type} {a_WT:WhyType a},
forall (s1:fset a) (s2:fset a), subset s2 (union s1 s2).
Parameter inter:
forall {a:Type} {a_WT:WhyType a}, fset a -> fset a -> fset a.
Axiom inter_def :
forall {a:Type} {a_WT:WhyType a},
forall (s1:fset a) (s2:fset a) (x:a),
mem x (inter s1 s2) <-> mem x s1 /\ mem x s2.
Axiom subset_inter_1 :
forall {a:Type} {a_WT:WhyType a},
forall (s1:fset a) (s2:fset a), subset (inter s1 s2) s1.
Axiom subset_inter_2 :
forall {a:Type} {a_WT:WhyType a},
forall (s1:fset a) (s2:fset a), subset (inter s1 s2) s2.
Parameter diff: forall {a:Type} {a_WT:WhyType a}, fset a -> fset a -> fset a.
Axiom diff_def :
forall {a:Type} {a_WT:WhyType a},
forall (s1:fset a) (s2:fset a) (x:a),
mem x (diff s1 s2) <-> mem x s1 /\ ~ mem x s2.
Axiom subset_diff :
forall {a:Type} {a_WT:WhyType a},
forall (s1:fset a) (s2:fset a), subset (diff s1 s2) s1.
Parameter pick: forall {a:Type} {a_WT:WhyType a}, fset a -> a.
Axiom pick_def :
forall {a:Type} {a_WT:WhyType a},
forall (s:fset a), ~ is_empty s -> mem (pick s) s.
(* Why3 assumption *)
Definition disjoint {a:Type} {a_WT:WhyType a} (s1:fset a) (s2:fset a) : Prop :=
forall (x:a), ~ mem x s1 \/ ~ mem x s2.
Axiom disjoint_inter_empty :
forall {a:Type} {a_WT:WhyType a},
forall (s1:fset a) (s2:fset a), disjoint s1 s2 <-> is_empty (inter s1 s2).
Axiom disjoint_diff_eq :
forall {a:Type} {a_WT:WhyType a},
forall (s1:fset a) (s2:fset a), disjoint s1 s2 <-> ((diff s1 s2) = s1).
Axiom disjoint_diff_s2 :
forall {a:Type} {a_WT:WhyType a},
forall (s1:fset a) (s2:fset a), disjoint (diff s1 s2) s2.
Parameter filter:
forall {a:Type} {a_WT:WhyType a}, fset a -> (a -> Init.Datatypes.bool) ->
fset a.
Axiom filter_def :
forall {a:Type} {a_WT:WhyType a},
forall (s:fset a) (p:a -> Init.Datatypes.bool) (x:a),
mem x (filter s p) <-> mem x s /\ ((p x) = Init.Datatypes.true).
Axiom subset_filter :
forall {a:Type} {a_WT:WhyType a},
forall (s:fset a) (p:a -> Init.Datatypes.bool), subset (filter s p) s.
Parameter map:
forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b}, (a -> b) ->
fset a -> fset b.
Axiom map_def :
forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b},
forall (f:a -> b) (u:fset a) (y:b),
mem y (map f u) <-> (exists x:a, mem x u /\ (y = (f x))).
Axiom mem_map :
forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b},
forall (f:a -> b) (u:fset a), forall (x:a), mem x u -> mem (f x) (map f u).
Parameter cardinal:
forall {a:Type} {a_WT:WhyType a}, fset a -> Numbers.BinNums.Z.
Axiom cardinal_nonneg :
forall {a:Type} {a_WT:WhyType a},
forall (s:fset a), (0%Z <= (cardinal s))%Z.
Axiom cardinal_empty :
forall {a:Type} {a_WT:WhyType a},
forall (s:fset a), is_empty s <-> ((cardinal s) = 0%Z).
Axiom cardinal_add :
forall {a:Type} {a_WT:WhyType a},
forall (x:a), forall (s:fset a),
(mem x s -> ((cardinal (add x s)) = (cardinal s))) /\
(~ mem x s -> ((cardinal (add x s)) = ((cardinal s) + 1%Z)%Z)).
Axiom cardinal_remove :
forall {a:Type} {a_WT:WhyType a},
forall (x:a), forall (s:fset a),
(mem x s -> ((cardinal (remove x s)) = ((cardinal s) - 1%Z)%Z)) /\
(~ mem x s -> ((cardinal (remove x s)) = (cardinal s))).
Axiom cardinal_subset :
forall {a:Type} {a_WT:WhyType a},
forall (s1:fset a) (s2:fset a), subset s1 s2 ->
((cardinal s1) <= (cardinal s2))%Z.
Axiom subset_eq :
forall {a:Type} {a_WT:WhyType a},
forall (s1:fset a) (s2:fset a), subset s1 s2 ->
((cardinal s1) = (cardinal s2)) -> (s1 = s2).
Axiom cardinal1 :
forall {a:Type} {a_WT:WhyType a},
forall (s:fset a), ((cardinal s) = 1%Z) -> forall (x:a), mem x s ->
(x = (pick s)).
Axiom cardinal_union :
forall {a:Type} {a_WT:WhyType a},
forall (s1:fset a) (s2:fset a),
((cardinal (union s1 s2)) =
(((cardinal s1) + (cardinal s2))%Z - (cardinal (inter s1 s2)))%Z).
Axiom cardinal_inter_disjoint :
forall {a:Type} {a_WT:WhyType a},
forall (s1:fset a) (s2:fset a), disjoint s1 s2 ->
((cardinal (inter s1 s2)) = 0%Z).
Axiom cardinal_diff :
forall {a:Type} {a_WT:WhyType a},
forall (s1:fset a) (s2:fset a),
((cardinal (diff s1 s2)) = ((cardinal s1) - (cardinal (inter s1 s2)))%Z).
Axiom cardinal_filter :
forall {a:Type} {a_WT:WhyType a},
forall (s:fset a) (p:a -> Init.Datatypes.bool),
((cardinal (filter s p)) <= (cardinal s))%Z.
Axiom cardinal_map :
forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b},
forall (f:a -> b) (s:fset a), ((cardinal (map f s)) <= (cardinal s))%Z.
Parameter min_elt: fset Numbers.BinNums.Z -> Numbers.BinNums.Z.
Axiom min_elt_def :
forall (s:fset Numbers.BinNums.Z), ~ is_empty s ->
mem (min_elt s) s /\
(forall (x:Numbers.BinNums.Z), mem x s -> ((min_elt s) <= x)%Z).
Parameter max_elt: fset Numbers.BinNums.Z -> Numbers.BinNums.Z.
Axiom max_elt_def :
forall (s:fset Numbers.BinNums.Z), ~ is_empty s ->
mem (max_elt s) s /\
(forall (x:Numbers.BinNums.Z), mem x s -> (x <= (max_elt s))%Z).
Parameter interval:
Numbers.BinNums.Z -> Numbers.BinNums.Z -> fset Numbers.BinNums.Z.
Axiom interval_def :
forall (l:Numbers.BinNums.Z) (r:Numbers.BinNums.Z) (x:Numbers.BinNums.Z),
mem x (interval l r) <-> (l <= x)%Z /\ (x < r)%Z.
Axiom cardinal_interval :
forall (l:Numbers.BinNums.Z) (r:Numbers.BinNums.Z),
((l <= r)%Z -> ((cardinal (interval l r)) = (r - l)%Z)) /\
(~ (l <= r)%Z -> ((cardinal (interval l r)) = 0%Z)).
Axiom set : Type.
Parameter set_WhyType : WhyType set.
Existing Instance set_WhyType.
Parameter to_fset: set -> fset Numbers.BinNums.Z.
Parameter choose: set -> Numbers.BinNums.Z.
Axiom choose_spec :
forall (s:set), ~ is_empty (to_fset s) -> mem (choose s) (to_fset s).
Require set.Fset.
Require set.FsetInt.
Require set.SetApp.
Require set.SetAppInt.
(* Why3 assumption *)
Inductive ref (a:Type) :=
......@@ -329,68 +74,99 @@ Axiom no_duplicate :
Theorem VC_t3 :
forall (col:Numbers.BinNums.Z -> Numbers.BinNums.Z) (k:Numbers.BinNums.Z)
(sol:Numbers.BinNums.Z -> Numbers.BinNums.Z -> Numbers.BinNums.Z)
(s:Numbers.BinNums.Z) (a:set) (b:set) (c:set),
(0%Z <= k)%Z -> ((k + (cardinal (to_fset a)))%Z = n) -> (0%Z <= s)%Z ->
(s:Numbers.BinNums.Z) (a:set.SetAppInt.set) (b:set.SetAppInt.set)
(c:set.SetAppInt.set),
(0%Z <= k)%Z ->
((k + (set.Fset.cardinal (set.SetAppInt.to_fset a)))%Z = n) ->
(0%Z <= s)%Z ->
(forall (i:Numbers.BinNums.Z),
mem i (to_fset a) <->
set.Fset.mem i (set.SetAppInt.to_fset a) <->
((0%Z <= i)%Z /\ (i < n)%Z) /\
(forall (j:Numbers.BinNums.Z), (0%Z <= j)%Z /\ (j < k)%Z ->
~ ((col j) = i))) ->
(forall (i:Numbers.BinNums.Z), (0%Z <= i)%Z ->
~ mem i (to_fset b) <->
~ set.Fset.mem i (set.SetAppInt.to_fset b) <->
(forall (j:Numbers.BinNums.Z), (0%Z <= j)%Z /\ (j < k)%Z ->
~ ((col j) = ((i + j)%Z - k)%Z))) ->
(forall (i:Numbers.BinNums.Z), (0%Z <= i)%Z ->
~ mem i (to_fset c) <->
~ set.Fset.mem i (set.SetAppInt.to_fset c) <->
(forall (j:Numbers.BinNums.Z), (0%Z <= j)%Z /\ (j < k)%Z ->
~ ((col j) = ((i + k)%Z - j)%Z))) ->
partial_solution k col -> ~ is_empty (to_fset a) -> forall (o:set),
((to_fset o) = (diff (to_fset a) (to_fset b))) -> forall (o1:set),
((to_fset o1) = (diff (to_fset o) (to_fset c))) ->
partial_solution k col -> ~ set.