in progress: formalization of why3 logic

examples/in_progress/why3_logic/logic_typing.mlw

+
+module Env
+  
+  use import logic_syntax.VarsIn
+  use import logic_syntax.Substs
+  use import logic_syntax.SubstList
+  use import int.Int
+  use import list.List
+  use import list.Length
+  use import list.Nth
+  use import list.Mem
+  use import option.Option
+  use import support.Bind
+  use import support.HO
+  use import support.Choice
+  
+  (* Typing environment. *)
+  type ty_env 'tv 'tyv 'tys 'ls = {
+    (* Type symbols belonging to the environment. *)
+    tys_belong : 'tys -> bool;
+    (* Type symbol arities. *)
+    tys_arity : 'tys -> int;
+    (* Set of known constructors associated to the type.
+       If there is one, then the set is exhaustive. *)
+    tys_constr : 'tys -> 'ls -> bool;
+    (* Built-in type symbol for propositions. *)
+    tys_prop : 'tys;
+    (* Logical symbols belonging to the environment. *)
+    ls_belong : 'ls -> bool;
+    (* Logical symbols which are constructors. *)
+    ls_constr : 'ls -> bool;
+    (* Logical symbols arity with respect to types. *)
+    ls_ty_arity : 'ls -> int;
+    (* Types for logical symbols arguments. *)
+    ls_args : 'ls -> list (ty (bind 'tyv int) 'tys);
+    (* Types for logical symbols return values. *)
+    ls_ret : 'ls -> ty (bind 'tyv int) 'tys;
+    (* Term variables currently in the environment. *)
+    tv_belong : 'tv -> bool;
+    (* Types of variables currently in the environment. *)
+    tv_ty : 'tv -> ty 'tyv 'tys;
+  }
+  
+  (* Well-formedness of types: respect arities and all type
+     symbols belong to the environment. *)
+  predicate ty_wf (g:ty_env 'tv 'tyv 'tys 'ls) (ty:ty 'tyv2 'tys) =
+    match ty with
+    | TyVar _ -> true
+    | TyApp f l -> g.tys_belong f /\
+      g.tys_arity f = length l /\
+      tyl_wf g l
+    end
+  
+  with tyl_wf (g:ty_env 'tv 'tyv 'tys 'ls) (tyl:list (ty 'tyv2 'tys)) =
+    match tyl with
+    | Nil -> true
+    | Cons x q -> ty_wf g x /\ tyl_wf g q
+    end
+  
+  function constr_ty_list (a b:int) : list (ty (bind 'tyv int) 'tys)
+  axiom constr_ty_list_empty : forall a.
+    constr_ty_list a a = (Nil:list (ty (bind 'tyv int) 'tys))
+  axiom constr_ty_list_succ : forall a b. a < b ->
+    (constr_ty_list a b:list (ty (bind 'tyv int) 'tys)) =
+    Cons (TyVar (Fresh a)) (constr_ty_list (a+1) b)
+  
+  let rec lemma constr_ty_list_length_nth (a b:int) : unit
+    requires { a <= b }
+    ensures { let l = (constr_ty_list a b:list (ty (bind 'tyv int) 'tys)) in
+      length l = b - a /\
+      forall n. 0 <= n < b - a -> nth n l = Some (TyVar (Fresh (a+n))) }
+    variant { b - a }
+  = if a < b then constr_ty_list_length_nth (a+1) b
+  
+  (* Well-formedness of environment. *)
+  predicate env_wf (g:ty_env 'tv 'tyv 'tys 'ls) =
+    (* Positive arities for types symbols. *)
+    (forall f. g.tys_belong f -> g.tys_arity f >= 0) /\
+    (* Proposition is a type symbol of arity 0. *)
+    g.tys_belong g.tys_prop /\
+    g.tys_arity g.tys_prop = 0 /\
+    (* Constructors are also logical symbols, and are indeed associated
+       to their respective return types. *)
+    (forall f. g.ls_constr f -> g.ls_belong f /\
+      match g.ls_ret f with
+      | TyApp tys _ -> g.tys_constr tys f
+      | _ -> false
+      end) /\
+    (forall tys f. g.tys_belong tys /\ g.tys_constr tys f ->
+      g.ls_constr f /\
+      g.ls_ret f = TyApp tys (constr_ty_list 0 (g.ls_ty_arity f))) /\
+    (*(* Constructors type arguments are entirely determined by their
+       return type, e.g every type argument occur in the result type
+       (which can then be deduced by unification). *)
+    (forall f tyvs tyss n. g.ls_constr f /\
+      ty_vars_in tyvs tyss (g.ls_ret f) /\
+      0 <= n < g.ls_ty_arity f -> tyvs (Fresh n)) /\*)
+    (forall f. g.ls_belong f -> let n = g.ls_ty_arity f in
+      (* Positive type arities for logical symbols. *)
+      n >= 0 /\
+      (* Arguments and return types are well-formed, and does not
+         contain unbound type variables. *)
+      ty_vars_in (bfold all (range 0 n)) g.tys_belong (g.ls_ret f) /\
+      tyl_vars_in (bfold all (range 0 n)) g.tys_belong (g.ls_args f) /\
+      ty_wf g (g.ls_ret f) /\
+      tyl_wf g (g.ls_args f))
+  
+  (* Useful functions giving the real type arguments/return types
+     of logical symbols given their scheme and their type arguments. *)
+  function ty_subst_args (tyl:list (ty 'tyv 'tys))
+    (ty_args:list (ty (bind 'tyv int) 'tys)) : list (ty 'tyv 'tys) =
+    tyl_subst (bfold TyVar (list_nth tyl (const default))) identity ty_args
+  
+  function ty_subst_ret (tyl:list (ty 'tyv 'tys))
+    (ty_ret:ty (bind 'tyv int) 'tys) : ty 'tyv 'tys =
+    ty_subst (bfold TyVar (list_nth tyl (const default))) identity ty_ret
+  
+  function ty_args (g:ty_env 'tv 'tyv 'tys 'ls)
+    (f:'ls) (tyl:list (ty 'tyv 'tys)): list (ty 'tyv 'tys) =
+    ty_subst_args tyl (g.ls_args f)
+  
+  function ty_ret (g:ty_env 'tv 'tyv 'tys 'ls)
+    (f:'ls) (tyl:list (ty 'tyv 'tys)) : ty 'tyv 'tys =
+    ty_subst_ret tyl (g.ls_ret f)
+  
+  function ty_prop (g:ty_env 'tv 'tyv 'tys 'ls) : ty 'tyv 'tys =
+    TyApp g.tys_prop Nil
+  
+  (* Well-formedness dependencies. *)
+  predicate env_ty_congruence (a:'tys -> bool) (g1:ty_env 'tv 'tyv 'tys 'ls)
+    (g2:ty_env 'tv2 'tyv2 'tys 'ls2) =
+    forall x. a x -> (g1.tys_belong x <-> g2.tys_belong x) /\
+                     g1.tys_arity x = g2.tys_arity x
+  
+  let rec lemma ty_wf_independence (a:'tyv -> bool) (b:'tys -> bool)
+    (g1:ty_env 'tv 'tyv2 'tys 'ls)
+    (g2:ty_env 'tv2 'tyv3 'tys 'ls2)
+    (ty:ty 'tyv 'tys) : unit
+    requires { env_ty_congruence b g1 g2 }
+    requires { ty_vars_in a b ty }
+    requires { ty_wf g1 ty }
+    ensures { ty_wf g2 ty }
+    variant { ty }
+  = match ty with
+    | TyApp _ l -> tyl_wf_independence a b g1 g2 l
+    | _ -> ()
+    end
+  
+  with lemma tyl_wf_independence (a:'tyv -> bool) (b:'tys -> bool)
+    (g1:ty_env 'tv 'tyv2 'tys 'ls)
+    (g2:ty_env 'tv2 'tyv3 'tys 'ls2)
+    (tyl:list (ty 'tyv 'tys)) : unit
+    requires { env_ty_congruence b g1 g2 }
+    requires { tyl_vars_in a b tyl }
+    requires { tyl_wf g1 tyl }
+    ensures { tyl_wf g2 tyl }
+    variant { tyl }
+  = match tyl with
+    | Cons x q -> ty_wf_independence a b g1 g2 x;tyl_wf_independence a b g1 g2 q
+    | _ -> ()
+    end
+  
+  let rec lemma ty_wf_subst (a:'tyv -> bool) (b:'tys -> bool)
+    (fa:'tyv -> ty 'tyv2 'tys2)
+    (fb:'tys -> 'tys2)
+    (g:ty_env 'tv 'tyv3 'tys 'ls)
+    (g2:ty_env 'tv2 'tyv4 'tys2 'ls2)
+    (ty:ty 'tyv 'tys) : unit
+    requires { ty_wf g ty }
+    requires { ty_vars_in a b ty }
+    requires { forall x. a x -> ty_wf g2 (fa x) }
+    requires { forall x. b x -> g.tys_belong x /\ g2.tys_belong (fb x) /\
+      g2.tys_arity (fb x) = g.tys_arity x }
+    ensures { ty_wf g2 (ty_subst fa fb ty) }
+    variant { ty }
+  = match ty with
+    | TyApp _ l -> tyl_wf_subst a b fa fb g g2 l
+    | _ -> ()
+    end
+  
+  with lemma tyl_wf_subst (a:'tyv -> bool) (b:'tys -> bool)
+    (fa:'tyv -> ty 'tyv2 'tys2)
+    (fb:'tys -> 'tys2)
+    (g:ty_env 'tv 'tyv3 'tys 'ls)
+    (g2:ty_env 'tv2 'tyv4 'tys2 'ls2)
+    (tyl:list (ty 'tyv 'tys)) : unit
+    requires { tyl_wf g tyl }
+    requires { tyl_vars_in a b tyl }
+    requires { forall x. a x -> ty_wf g2 (fa x) }
+    requires { forall x. b x -> g.tys_belong x /\ g2.tys_belong (fb x) /\
+      g2.tys_arity (fb x) = g.tys_arity x }
+    ensures { tyl_wf g2 (tyl_subst fa fb tyl) }
+    variant { tyl }
+  = match tyl with
+    | Cons x q -> ty_wf_subst a b fa fb g g2 x;tyl_wf_subst a b fa fb g g2 q
+    | _ -> ()
+    end
+  
+end
+
+(* Pattern typing, which includes exhaustivity checking. *)
+module Pattern
+  
+  use import logic_syntax.Substs
+  use import logic_syntax.FreeVarsIn
+  use import int.Int
+  use import list.List
+  use import list.Length
+  use import list.Nth
+  use import list.Mem
+  use import option.Option
+  use import support.PartialMap
+  use import support.Bind
+  use import support.HO
+  use import support.Choice
+  use import Env
+  
+  (* Simple syntactic criterion for the absence of conflicts
+     between patterns variables.
+     Conflicts may be of two kinds:
+     - Presence on only one side of a or pattern.
+     - Presence on several sides of a multi-pattern. *)
+  predicate pat_no_conflict (pat:pattern 'pv 'tyv 'tys 'ls) =
+    match pat with
+    | PAs p x -> not pat_pv_free_var p x /\ pat_no_conflict p
+    | POr p1 p2 -> pat_no_conflict p1 /\ pat_no_conflict p2 /\
+      forall x. pat_pv_free_var p1 x <-> pat_pv_free_var p2 x
+    | PApp _ _ pl -> patl_no_conflict pl
+    | _ -> true
+    end
+  
+  with patl_no_conflict (patl:list (pattern 'pv 'tyv 'tys 'ls)) =
+    match patl with
+    | Nil -> true
+    | Cons p q -> pat_no_conflict p /\ patl_no_conflict q /\
+      forall x. not (pat_pv_free_var p x /\ patl_pv_free_var q x)
+    end
+  
+  (* Well-typed patterns. *)
+  predicate pat_wty (g:ty_env 'tv 'tyv 'tys 'ls)
+    (pat:pattern 'pv 'tyv 'tys 'ls)
+    (ty:ty 'tyv 'tys) =
+    match pat with
+    | PAs p _ -> pat_wty g p ty
+    | POr p1 p2 -> pat_wty g p1 ty /\ pat_wty g p2 ty
+    | PApp f tyl pl -> patl_wty g pl (ty_args g f tyl) /\
+      g.ls_ty_arity f = length tyl /\ g.ls_constr f /\ ty_ret g f tyl = ty
+    | _ -> true
+    end
+  
+  with patl_wty (g:ty_env 'tv 'tyv 'tys 'ls)
+    (patl:list (pattern 'pv 'tyv 'tys 'ls))
+    (tyl:list (ty 'tyv 'tys)) =
+    match patl , tyl with
+    | Cons p q , Cons typ tyq -> pat_wty g p typ /\ patl_wty g q tyq
+    | Nil , Nil -> true
+    | _ -> false
+    end
+  
+  (* Collect types of variables occuring in a pattern. *)
+  function pat_ty_collector (g:ty_env 'tv 'tyv 'tys 'ls)
+    (pat:pattern 'pv 'tyv 'tys 'ls)
+    (ty:ty 'tyv 'tys) : 'pv -> option (ty 'tyv 'tys) = 
+    match pat with
+    | PWild -> const None
+    | PVar x -> (const None)[x <- Some ty]
+    | PAs p x -> (pat_ty_collector g p ty)[x <- Some ty]
+    | POr p1 _ -> pat_ty_collector g p1 ty
+    | PApp f tyl pl -> patl_ty_collector g pl (ty_args g f tyl)
+    end
+  
+  with patl_ty_collector (g:ty_env 'tv 'tyv 'tys 'ls)
+    (patl:list (pattern 'pv 'tyv 'tys 'ls))
+    (tyl:list (ty 'tyv 'tys)) : 'pv -> option (ty 'tyv 'tys) =
+    match patl , tyl with
+    | Nil , _ | _ , Nil -> const None
+    | Cons x q , Cons y r -> let m1 = pat_ty_collector g x y in
+      let m2 = patl_ty_collector g q r in
+      extend m1 m2
+    end
+  
+  (* Variables collected and variables occuring in a well-formed pattern
+     are the same thing. *)
+  let rec lemma pat_ty_collector_dom (g:ty_env 'tv 'tyv 'tys 'ls)
+    (pat:pattern 'pv 'tyv 'tys 'ls)
+    (ty:ty 'tyv 'tys)
+    (x:'pv) : unit
+    requires { pat_no_conflict pat }
+    requires { pat_wty g pat ty }
+    ensures { pat_pv_free_var pat x <-> pat_ty_collector g pat ty x <> None }
+    variant { pat }
+  = match pat with
+    | PAs p _ -> pat_ty_collector_dom g p ty x
+    | POr p1 _ -> pat_ty_collector_dom g p1 ty x
+    | PApp f tyl pl -> patl_ty_collector_dom g pl (ty_args g f tyl) x
+    | _ -> ()
+    end
+  
+  with lemma patl_ty_collector_dom (g:ty_env 'tv 'tyv 'tys 'ls)
+    (patl:list (pattern 'pv 'tyv 'tys 'ls))
+    (tyl:list (ty 'tyv 'tys))
+    (x:'pv) : unit
+    requires { patl_no_conflict patl }
+    requires { patl_wty g patl tyl }
+    ensures { patl_pv_free_var patl x <->
+      patl_ty_collector g patl tyl x <> None }
+    variant { patl }
+  = match patl , tyl with
+    | Cons p q , Cons typ tyq -> pat_ty_collector_dom g p typ x;
+      patl_ty_collector_dom g q tyq x;
+      let m1 = pat_ty_collector g p typ in
+      let m2 = patl_ty_collector g q tyq in
+      assert { not (patl_ty_collector g patl tyl x <> None <->
+        m1 x <> None \/ m2 x <> None) -> match m1 x , m2 x with
+          | Some _ , _ | _ , Some _ -> ("keep_on_simp" true) && false
+          | _ -> false end }
+    | Nil , Nil -> ()
+    | _ -> assert { "keep_on_simp" true }
+    end
+  
+  (* Now, let us move to pattern-matching exhaustiveness.
+     The simplest syntactic way to define it is to ask that any structural
+     pattern of the right type can be structurally unified with one of the
+     initial patterns.
+     (a structural pattern is a pattern containing only constructors and
+     wildcards).
+     Any other way would requires some form of pattern compilation,
+     which we want to avoid. *)
+  
+  predicate pat_structural (pat:pattern 'pv 'tyv 'tys 'ls) =
+    match pat with
+    | PWild -> true
+    | PApp _ _ pl -> patl_structural pl
+    | _ -> false
+    end
+  
+  with patl_structural (patl:list (pattern 'pv 'tyv 'tys 'ls)) =
+    match patl with
+    | Nil -> true
+    | Cons x q -> pat_structural x /\ patl_structural q
+    end
+  
+  predicate pat_structural_match (p1 p2:pattern 'pv 'tyv 'tys 'ls) =
+    match p1 , p2 with
+    | PWild , _ | _ , PWild | _ , PVar _ -> true
+    | _ , PAs p2 _ -> pat_structural_match p1 p2
+    | _ , POr p2 p3 -> pat_structural_match p1 p2 \/ pat_structural_match p1 p3
+    | PApp f1 _ l1 , PApp f2 _ l2 -> f1 = f2 /\ patl_structural_match l1 l2
+    | _ -> false
+    end
+  
+  with patl_structural_match (p1 p2:list (pattern 'pv 'tyv 'tys 'ls)) =
+    match p1 , p2 with
+    | Nil , Nil -> true
+    | Cons h1 t1 , Cons h2 t2 -> pat_structural_match h1 h2 /\
+      patl_structural_match t1 t2
+    | _ -> false
+    end
+  
+  predicate case_structural_match (p1:pattern int 'tyv 'tys 'ls)
+    (brl:list (branch 'tv 'tyv 'tys 'ls)) = match brl with
+    | Nil -> false
+    | Cons (h,_) t -> pat_structural_match p1 h \/ case_structural_match p1 t
+    end
+  
+  predicate exhaustive (g:ty_env 'tv 'tyv 'tys 'ls)
+    (brl:list (branch 'tv 'tyv 'tys 'ls))
+    (ty:ty 'tyv 'tys) =
+    forall pat. pat_structural pat /\ pat_wty g pat ty ->
+      case_structural_match pat brl
+  
+end
+
+(* Term typing. *)
+module Term
+  
+  use import logic_syntax.Substs
+  use import logic_syntax.FreeVarsIn
+  use import int.Int
+  use import list.List
+  use import list.Length
+  use import list.Nth
+  use import list.Mem
+  use import option.Option
+  use import support.PartialMap
+  use import support.Bind
+  use import support.HO
+  use import support.Choice
+  use import Env
+  use import Pattern
+  
+  predicate t_wf (g:ty_env 'tv 'tyv 'tys 'ls)
+    (t:term 'tv 'tyv 'tys 'ls)
+    (ty:ty 'tyv 'tys) =
+    match t with
+    | TVar x -> g.tv_belong x /\ g.tv_ty x = ty
+    | TApp f tyl tl -> g.ls_belong f /\ g.ls_ty_arity f = length tyl /\
+      tl_wf g tl (ty_args g f tyl) /\ ty_ret g f tyl = ty
+    | TIf b t e -> t_wf g b g.ty_prop /\ t_wf g t ty /\ t_wf g e ty
+    | TLet t1 t2 -> exists ty0. t_wf g t1 ty0 /\ ty_wf g ty0 /\
+      let g' = { g with tv_belong = bfold g.tv_belong all;
+        tv_ty = bfold g.tv_ty (const ty0) } in
+      t_wf g' t2 ty
+    | TCase t brl -> exists ty0. t_wf g t ty0 /\ ty_wf g ty0 /\
+      brl_wf g brl ty0 ty /\ exhaustive g brl ty0
+    | TForall tyl t | TExists tyl t ->
+      let g' = { g with tv_belong = bfold g.tv_belong (range 0 (length tyl));
+        tv_ty = bfold g.tv_ty (list_nth tyl (const default)) } in
+      t_wf g' t ty /\ g.ty_prop = ty
+    | TAnd t1 t2 | TOr t1 t2 | TImplies t1 t2 | TIff t1 t2 ->
+      g.ty_prop = ty /\ t_wf g t1 ty /\ t_wf g t2 ty
+    | TNot t -> g.ty_prop = ty /\ t_wf g t ty
+    | TTrue | TFalse -> g.ty_prop = ty
+    end
+  
+  with tl_wf (g:ty_env 'tv 'tyv 'tys 'ls)
+    (tl:list (term 'tv 'tyv 'tys 'ls))
+    (tyl:list (ty 'tyv 'tys)) =
+    match tl , tyl with
+    | Nil , Nil-> true
+    | Cons ht qt , Cons hty qty -> t_wf g ht hty /\ tl_wf g qt qty
+    | _ , _ -> false
+    end
+  
+  with brl_wf (g:ty_env 'tv 'tyv 'tys 'ls)
+    (brl:list (branch 'tv 'tyv 'tys 'ls))
+    (tyc:ty 'tyv 'tys)
+    (ty:ty 'tyv 'tys) =
+    match brl with
+    | Nil -> true
+    | Cons h q -> br_wf g h tyc ty /\ brl_wf g q tyc ty
+    end
+  
+  with br_wf (g:ty_env 'tv 'tyv 'tys 'ls)
+    (br:branch 'tv 'tyv 'tys 'ls)
+    (tyc:ty 'tyv 'tys)
+    (ty:ty 'tyv 'tys) =
+    match br with
+    | (pat,right) -> pat_no_conflict pat /\ pat_wty g pat tyc /\
+      let m = pat_ty_collector g pat tyc in
+      let g' = { g with tv_belong = bfold g.tv_belong (domain m);
+        tv_ty = bfold g.tv_ty (complete m (const default)) } in
+      t_wf g' right ty
+    end
+  
+  (* Q: which lemmas are useful here ? *)
+  
+  predicate env_coherent_ext (g:ty_env 'tv 'tyv 'tys 'ls)
+    (dom:'ntv -> bool)
+    (ext:'ntv -> ty 'tyv 'tys) =
+    forall x. dom x -> ty_wf g (ext x)
+  
+  let lemma env_extension_wf (g:ty_env 'tv 'tyv 'tys 'ls)
+    (g':ty_env (bind 'tv 'ntv) 'tyv 'tys 'ls)
+    (dom:'ntv -> bool)
+    (ext:'ntv -> ty 'tyv 'tys) : unit
+    requires { env_wf g }
+    requires { env_coherent_ext g dom ext }
+    requires { g' = { g with tv_belong = bfold g.tv_belong dom;
+                             tv_ty = bfold g.tv_ty ext } }
+    ensures { env_wf g' }
+  = assert { env_ty_congruence all g g' &&
+      forall f. g'.ls_belong f ->
+        g.ls_belong f &&
+        ty_wf g (g.ls_ret f) && tyl_wf g (g.ls_args f) &&
+        ty_vars_in all all (g.ls_ret f) && tyl_vars_in all all (g.ls_args f) &&
+        ty_wf g' (g'.ls_ret f) && tyl_wf g' (g'.ls_args f)
+    }
+  
+end
+
+

examples/in_progress/why3_logic/logic_typing/why3session.xml

+<?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="Alt-Ergo" version="0.99.1" timelimit="5" memlimit="1000"/>
+<prover id="1" name="CVC3" version="2.4.1" timelimit="5" memlimit="1000"/>
+<prover id="2" name="Z3" version="4.3.1" timelimit="5" memlimit="1000"/>
+<file name="../logic_typing.mlw" expanded="true">
+<theory name="Env" sum="c9b6dd55389ebfd832ea23fa9c6a7092" expanded="true">
+ <goal name="WP_parameter constr_ty_list_length_nth" expl="VC for constr_ty_list_length_nth" expanded="true">
+ <transf name="split_goal_wp" expanded="true">
+  <goal name="WP_parameter constr_ty_list_length_nth.1" expl="1. variant decrease">
+  <proof prover="0"><result status="valid" time="0.09" steps="2"/></proof>
+  </goal>
+  <goal name="WP_parameter constr_ty_list_length_nth.2" expl="2. precondition">
+  <proof prover="0"><result status="valid" time="0.05" steps="2"/></proof>
+  </goal>
+  <goal name="WP_parameter constr_ty_list_length_nth.3" expl="3. postcondition" expanded="true">
+  <proof prover="1"><result status="valid" time="0.66"/></proof>
+  </goal>
+  <goal name="WP_parameter constr_ty_list_length_nth.4" expl="4. postcondition">
+  <proof prover="0"><result status="valid" time="0.10" steps="7"/></proof>
+  </goal>
+ </transf>
+ </goal>
+ <goal name="WP_parameter ty_wf_independence" expl="VC for ty_wf_independence">
+ <proof prover="0"><result status="valid" time="0.08" steps="47"/></proof>
+ </goal>
+ <goal name="WP_parameter tyl_wf_independence" expl="VC for tyl_wf_independence">
+ <proof prover="0"><result status="valid" time="0.08" steps="76"/></proof>
+ </goal>
+ <goal name="WP_parameter ty_wf_subst" expl="VC for ty_wf_subst">
+ <proof prover="0"><result status="valid" time="0.14" steps="136"/></proof>
+ </goal>
+ <goal name="WP_parameter tyl_wf_subst" expl="VC for tyl_wf_subst">
+ <proof prover="0"><result status="valid" time="0.34" steps="221"/></proof>
+ </goal>
+</theory>
+<theory name="Pattern" sum="92dff16c51685f061e7216d7ae6d75f1">
+ <goal name="WP_parameter pat_ty_collector_dom" expl="VC for pat_ty_collector_dom">
+ <proof prover="0"><result status="valid" time="0.85" steps="964"/></proof>
+ </goal>
+ <goal name="WP_parameter patl_ty_collector_dom" expl="VC for patl_ty_collector_dom">
+ <transf name="split_goal_wp">
+  <goal name="WP_parameter patl_ty_collector_dom.1" expl="1. variant decrease">
+  <proof prover="0"><result status="valid" time="0.08" steps="24"/></proof>
+  </goal>
+  <goal name="WP_parameter patl_ty_collector_dom.2" expl="2. precondition">
+  <proof prover="0"><result status="valid" time="0.07" steps="13"/></proof>
+  </goal>
+  <goal name="WP_parameter patl_ty_collector_dom.3" expl="3. precondition">
+  <proof prover="0"><result status="valid" time="0.08" steps="13"/></proof>
+  </goal>
+  <goal name="WP_parameter patl_ty_collector_dom.4" expl="4. variant decrease">
+  <proof prover="0"><result status="valid" time="0.07" steps="27"/></proof>
+  </goal>
+  <goal name="WP_parameter patl_ty_collector_dom.5" expl="5. precondition">
+  <proof prover="0"><result status="valid" time="0.07" steps="18"/></proof>
+  </goal>
+  <goal name="WP_parameter patl_ty_collector_dom.6" expl="6. precondition">
+  <proof prover="0"><result status="valid" time="0.08" steps="18"/></proof>
+  </goal>
+  <goal name="WP_parameter patl_ty_collector_dom.7" expl="7. assertion">
+  <transf name="split_goal_wp">
+   <goal name="WP_parameter patl_ty_collector_dom.7.1" expl="1. assertion">
+   <proof prover="0"><result status="valid" time="0.06" steps="0"/></proof>
+   </goal>
+   <goal name="WP_parameter patl_ty_collector_dom.7.2" expl="2. assertion">
+   <proof prover="0"><result status="valid" time="0.09" steps="76"/></proof>
+   </goal>
+   <goal name="WP_parameter patl_ty_collector_dom.7.3" expl="3. assertion">
+   <proof prover="0"><result status="valid" time="0.10" steps="0"/></proof>
+   </goal>
+   <goal name="WP_parameter patl_ty_collector_dom.7.4" expl="4. assertion">
+   <proof prover="0"><result status="valid" time="0.09" steps="64"/></proof>
+   </goal>
+   <goal name="WP_parameter patl_ty_collector_dom.7.5" expl="5. assertion">
+   <proof prover="0"><result status="valid" time="0.06" steps="0"/></proof>
+   </goal>
+   <goal name="WP_parameter patl_ty_collector_dom.7.6" expl="6. assertion">
+   <proof prover="0"><result status="valid" time="0.07" steps="64"/></proof>
+   </goal>
+   <goal name="WP_parameter patl_ty_collector_dom.7.7" expl="7. assertion">
+   <proof prover="0"><result status="valid" time="0.08" steps="51"/></proof>
+   </goal>
+  </transf>
+  </goal>
+  <goal name="WP_parameter patl_ty_collector_dom.8" expl="8. postcondition">
+  <proof prover="0"><result status="valid" time="0.08" steps="32"/></proof>
+  </goal>
+  <goal name="WP_parameter patl_ty_collector_dom.9" expl="9. assertion">
+  <proof prover="0"><result status="valid" time="0.07" steps="0"/></proof>
+  </goal>
+  <goal name="WP_parameter patl_ty_collector_dom.10" expl="10. postcondition">
+  <proof prover="0"><result status="valid" time="0.08" steps="11"/></proof>
+  </goal>
+  <goal name="WP_parameter patl_ty_collector_dom.11" expl="11. postcondition">
+  <proof prover="0"><result status="valid" time="0.13" steps="10"/></proof>
+  </goal>
+  <goal name="WP_parameter patl_ty_collector_dom.12" expl="12. assertion">
+  <proof prover="0"><result status="valid" time="0.06" steps="0"/></proof>
+  </goal>
+  <goal name="WP_parameter patl_ty_collector_dom.13" expl="13. postcondition">
+  <proof prover="0"><result status="valid" time="0.12" steps="20"/></proof>
+  </goal>
+ </transf>
+ </goal>
+</theory>
+<theory name="Term" sum="e9e65ea0476b241aba871f9ce9907bb3">
+ <goal name="WP_parameter env_extension_wf" expl="VC for env_extension_wf">
+ <transf name="split_goal_wp">
+  <goal name="WP_parameter env_extension_wf.1" expl="1. assertion">
+  <transf name="split_goal_wp">
+   <goal name="WP_parameter env_extension_wf.1.1" expl="1.">
+   <proof prover="0"><result status="valid" time="0.10" steps="19"/></proof>
+   </goal>
+   <goal name="WP_parameter env_extension_wf.1.2" expl="2.">
+   <proof prover="0"><result status="valid" time="0.13" steps="15"/></proof>
+   </goal>
+   <goal name="WP_parameter env_extension_wf.1.3" expl="3.">
+   <proof prover="1"><result status="valid" time="0.26"/></proof>
+   </goal>
+   <goal name="WP_parameter env_extension_wf.1.4" expl="4.">
+   <proof prover="1"><result status="valid" time="0.25"/></proof>
+   </goal>
+   <goal name="WP_parameter env_extension_wf.1.5" expl="5.">
+   <proof prover="0"><result status="valid" time="0.18" steps="21"/></proof>