Library AdomLib

Require Import
  Utf8 String Bool
  ToString
  Maps
  LatticeSignatures.

Set Implicit Arguments.

Adding a bottom element to an abstract domain

Inductive botlift (A:Type) : Type := Bot | NotBot (x:A).
Implicit Arguments Bot [A].
Notation "t +⊥" := (botlift t) (at level 39).

Definition bot {A: Type} (l: weak_lattice (A +⊥)) : A+⊥ := Bot.

Instance lift_bot_wl {A:Type} (l:weak_lattice A) : weak_lattice (A+⊥) :=
{ leb :=
    (fun x y
      match x, y with
        | Bot, _true
        | NotBot x, NotBot yleb x y
        | _, _false
      end);
  top := (NotBot top);
  join :=
    (fun x y
      match x, y with
        | Bot, _y
        |_ , Botx
        | NotBot x, NotBot yNotBot (join x y)
      end);
  widen :=
    (fun x y
      match x, y with
        | Bot, _y
        |_ , Botx
        | NotBot x, NotBot yNotBot (widen x y)
      end)
}.

Instance lift_gamma (A B: Type) (G: gamma_op A B) : gamma_op (A+⊥) B :=
    (fun x
      match x with
      | Botfun _False
      | NotBot xγ x
      end).

Definition lift_bot {A B:Type} WL G (l:adom A B WL G) : adom (A+⊥) B _ _.

Definition botbind {A B} (f: A B+⊥) (a: A+⊥) : B+⊥ :=
  match a with
    | BotBot
    | NotBot xf x
  end.

Notation "'do' X <- A ; B" := (botbind (fun XB) A)
 (at level 200, X ident, A at level 100, B at level 200)
 : botbind_monad_scope.

Notation "'do_bot' X <- A ; B" := (botbind (fun XB) A)
 (at level 200, X ident, A at level 100, B at level 200).

Lemma botbind_spec {A A' B B':Type} {GA: gamma_op A A'} {GB: gamma_op B B'} :
   f:AB+⊥, x y, ( a, x γ ay γ (f a)) →
                     ( a, x γ ay γ (botbind f a)).

Definition botbind2 {A B C} (f: A B C+⊥) (a: A+⊥) (b: B+⊥) : C+⊥ :=
  botbind (fun xbotbind (f x) b) a.

Lemma botbind2_spec {A A' B B' C C':Type} {AD:gamma_op A A'} {BD:gamma_op B B'} {CD:gamma_op C C'}:
   f:ABC+⊥, x y z, ( x_ab y_ab, x γ x_aby γ y_abz γ (f x_ab y_ab)) →
                        ( x_ab y_ab, x γ x_aby γ y_abz γ (botbind2 f x_ab y_ab)).

Definition botlift_fun1 {A B:Type} (f:AB) (x:A+⊥) : B+⊥ :=
  botbind (@NotBot _ f) x.

Lemma botlift_fun1_spec {A A' B B':Type} {AD:gamma_op A A'} {BD:gamma_op B B'}:
   f:AB, x y, ( x_ab, x γ x_aby γ (f x_ab)) →
                  ( x_ab, x γ x_aby γ (botlift_fun1 f x_ab)).

Definition botlift_fun2 {A B C:Type} (f:ABC) (a:A+⊥) (b:B+⊥) : C+⊥ :=
  botbind (fun xbotlift_fun1 (f x) b) a.

Lemma botlift_fun2_spec {A A' B B' C C':Type} {AD:gamma_op A A'} {BD:gamma_op B B'} {CD:gamma_op C C'}:
   f:ABC, x y z, ( x_ab y_ab, x γ x_aby γ y_abz γ (f x_ab y_ab)) →
                      ( x_ab y_ab, x γ x_aby γ y_abz γ (botlift_fun2 f x_ab y_ab)).

Instance bot_lift_toString A `{ToString A} : ToString (A+⊥) :=
  { to_string x := match x with
                   | Bot ⇒ "⊥"%string
                   | NotBot x'to_string x'
                   end
  }.

Lemma union_list_bot A B WL G {AD: adom A B WL G} (z: A) (l: list (A+⊥)) :
  union_list (NotBot z) join l = Bot
   x, List.In x l x = Bot.

Lemma union_list_leb A (bot: A) join l (leb: A A bool) :
  ( x a b, leb x a = true leb x b = true leb x (join a b) = true)
   x,
    (l = nil leb x bot = true)
    ( y, List.In y l leb x y = true)
    leb x (union_list bot join l) = true.

Direct product of two abstract domains

Module WProd.
Section lat.
  Context {t1 t2 B: Type}.
  Context WL1 G1 (lat1 : adom t1 B WL1 G1).
  Context WL2 G2 (lat2 : adom t2 B WL2 G2).

  Definition A: Type := (t1×t2)%type.

  Definition leb: AAbool :=
    fun x y
      let (x1,x2) := x in
      let (y1,y2) := y in
        (leb x1 y1
      &&
        leb x2 y2)%bool.

  Definition top: A :=
    (top, top).

  Definition join: AAA :=
    fun x y
      let (x1,x2) := x in
      let (y1,y2) := y in
        (join x1 y1,
          join x2 y2).

  Definition widen: AAA :=
    fun x y
      let (x1,x2) := x in
      let (y1,y2) := y in
        (widen x1 y1,
          widen x2 y2).

  Definition gamma: ABProp :=
    fun x
      let (x1,x2) := x in
      γ x1 γ x2.

  Lemma gamma_monotone: a1 a2,
    leb a1 a2 = truegamma a1 gamma a2.

  Lemma gamma_top: x, gamma top x.

  Lemma join_sound: x y, gamma x gamma y gamma (join x y).

  Instance make_wl : weak_lattice A :=
   {leb := leb;
    top := top;
    join := join;
    widen := widen
   }.

  Lemma make : adom A B _ gamma.

End lat.
End WProd.

Abstract domain of pairs of concrete elements.

Module WTensor.
Section lat.
  Context {t1 t2 B1 B2: Type}.
  Context WL1 G1 (lat1 : adom t1 B1 WL1 G1).
  Context WL2 G2 (lat2 : adom t2 B2 WL2 G2).

  Definition A: Type := (t1×t2)%type.
  Definition B: Type := (B1×B2)%type.

  Instance gamma : gamma_op A B :=
    fun x y
      let (x1,x2) := x in
      let (y1,y2) := y in
      y1 γ x1 y2 γ x2.

  Lemma gamma_monotone: a1 a2,
    leb a1 a2 = truegamma a1 gamma a2.

  Lemma gamma_top: x, gamma top x.

  Lemma join_sound: x y, gamma x gamma y gamma (join x y).

  Lemma make : adom A B _ gamma.

  Instance toString `{ToString t1} `{ToString t2} : ToString (t1 × t2) :=
    { to_string x := let '(a,b) := x in ("(" ++ to_string a ++ " ⊗ " ++ to_string b ++ ")")%string }.

End lat.
End WTensor.

Exponentiation of an abstract domain to an abstract domain of total environments

Module WPFun (P:TREE).
Module PP := Tree_Properties P.

Section lat.
Context {t0 B: Type}.
Context WL G (lat : adom t0 B WL G).

Definition t := P.t t0.

Definition bot : t+⊥ := Bot.

Definition top : t := (P.empty _).

Definition get (m: t) (r: P.elt) : t0 :=
  match P.get r m with
    | None
    | Some ii
  end.

Definition set (m: t) (r: P.elt) (i:t0) : t := P.set r i m.

Definition leb0 (m1 m2:t) : bool :=
  PP.for_all m2 (fun x i2leb (get m1 x) i2).

Lemma leb_le: m1 m2,
  leb0 m1 m2 = true → ( p, (get m1 p) (get m2 p) = true
                                   get m2 p = ).

Definition join : ttt :=
  P.combine
    (fun x y
       match x, y with
         | None, _None
         |_ , NoneNone
         | Some x, Some ySome (join x y)
       end).

Definition widen: ttt :=
  P.combine
    (fun x y
       match x, y with
         | None, _None
         |_ , NoneNone
         | Some x, Some ySome (widen x y)
       end).

Instance gamma : gamma_op t (P.eltB) :=
  fun m rs
   r, γ (get m r) (rs r).

Lemma gamma_monotone: x y,
  leb0 x y = true
  gamma x gamma y.

  Lemma join_correct : (x y:t) b,
    gamma x b gamma y bgamma (join x y) b.

Instance make_wl : weak_lattice t :=
  { leb := leb0
  ; top := top
  ; join := join
  ; widen := widen
  }.

Lemma make : adom t (P.eltB) make_wl gamma.

Lemma gamma_set1 : (app:t) rs ab x,
  γ app rs
  γ ab (rs x) →
  γ (set app x ab) rs.

Lemma gamma_set2 : (app:t) rs ab v x,
  γ app rs
  γ ab v
  γ (set app x ab) (fun pif P.elt_eq p x then v else rs p).

Definition forget (app: t) (r: P.elt) : t := P.remove r app.

Lemma gamma_forget : (app:t) rs rs' x,
  γ app rs
  ( y, xyrs y = rs' y) →
  γ (forget app x) rs'.

Lemma gamma_app: (m: t) (rs: P.eltB),
  γ m rs
   r, γ (get m r) (rs r).

Instance toString `{ToString P.elt} `{ToString t0} : ToString (P.t t0) :=
  (λ x, P.fold (λ s k v, s ++ "["++ to_string k ++ "↦" ++ to_string v ++"]" ) x "{" ++ "}")%string.

End lat.

End WPFun.

Option type.
Inductive toplift (A: Type) := All | Just : A toplift A.
Notation "x +⊤" := (toplift x) (at level 39).

Definition toplift_bind {A B: Type} (f: A B+⊤) (x: A+⊤) : B+⊤ :=
  match x with
  | AllAll
  | Just x'f x'
  end.

Notation "'do' X <- A ; B" := (toplift_bind (fun XB) A)
 (at level 200, X ident, A at level 100, B at level 200)
 : top_monad_scope.

Notation "'do_top' X <- A ; B" := (toplift_bind (fun XB) A)
 (at level 200, X ident, A at level 100, B at level 200).

Lemma top_bind_case A B (a: A+⊤) (f: A B+⊤) :
   P : B+⊤ Prop,
    P All
    ( a', a = Just a' P (f a'))
    P (do_top x <- a; f x).

Definition top_lift {A B: Type} (f: A B) : A+⊤ B+⊤ :=
  toplift_bind (fun xJust (f x)).

Definition top_bind2 {A B C: Type} (f: A B C+⊤) (x: A+⊤) (y: B+⊤) : C+⊤ :=
  match x, y with
  | All, _ | _, AllAll
  | Just x', Just y'f x' y'
  end.

Definition top_lift2 {A B C: Type} (f: A B C) : A+⊤ B+⊤ C+⊤ :=
  top_bind2 (fun x yJust (f x y)).

Definition top_leb {A: Type} (leb: A A bool) (x y: A+⊤) : bool.html#B">B <="keyword">with
  | _, All
+⊤pe="ype_scope:x_'→'_x">+⊤pe="ype_scope:x_'→'_x">an class="idi.fr/distruation">+⊤pe="ype_scope:x_on+⊤pe="ype_scope:x_on+⊤pe="ype_scope:x_on+⊤pe="ype_scope:x_on+⊤pe="ype_scope:x_on+⊤pe="ype_scope:x_on+⊤pe="ype_scope:x_oiable">x A: +⊤ :=
  match x, +⊤pe="ype_scope:x_'→'_x">an class="idi.fr/distruation">+⊤pe="ype_scope:x_on+⊤pe="yppe="var">y+⊤pe="yppe="vapid" type="notation">+⊤B B B B B B B _, All+⊤pe="ype_scope:x_on+⊤pe="ype_scope:x_oiable">x Just y'= v x,
  <"AdomLib.html#C"><="keyword">with
  | B
A+⊤ rs
  +⊤ident, B +⊤ > ⇒C) : x +⊤{ef="AdomLib.html#type="vaa class="idref" href="AdomLihtml#C"><="keyword">withfun <="keyword">with
  | +⊤
> ⇒<="keyword">withfun +⊤ > ⇒fun +⊤ > ⇒t) (rs: rsB γ x rs
   x +⊤{>rss k level 39).

Definition
topli>topli>topli>topli>topli>topli>topli>topli>topli>topli>topli>topli>topli>topli>topli>topli>topli>toplift_bind {A"tatistdlib/Coq.Strings.String.html#:string_sco"definition">topli>topli>topli>topli>topli>topli>topli>topli>topli>topli>topli>topli>topli>topli>topli>topli>topli>toplift_variable">B B rss k topli>topli>topli>topli>topli>topli>topli>topli>topli>topli>topli>topli>topli>topli>topli>topli>topli>toplinicode.Utf8_core.html#:type_scope:x_'→'_"definition">topli}t">ident, pre_l classr">k +⊤{><="keyword">withk ass="id" type="constructor">Justef" href="AdomLib.html#typd">Definit>,
   ">+⊤pe="ype_scope:x_'→'_x">an class="idi.fr/distruation">+⊤pe="ype_scope:x_on+⊤pe="ype_sc">Justef" href="AdomLib.html#typd">Definit>,
   ">+⊤pe="ype_scope:x_'→'_x">an class="idi.fr/distruation">+⊤pe="ype_scope:x_on+⊤pe="ype_scass="id" type="var">A: +⊤;> span class="itruation">+⊤pe="ype_sc">Justef" href="AdomLib.html#typd">Definit>,
   ">+⊤pe="ype_scope:x_'→'_x">an class="idi.fr/distruation">+⊤pe="ype_scope:x_on+⊤pe="ype_sc">Justef" href="AdomLib.html#typd">Definit>,
   ">+⊤pe="ype_scope:x_'→'_x">an class="idi.fr/distruation">+⊤pe="ype_scope:x_on+⊤pe="ype_sc">Justef" href="AdomLib.html#typd">Definit>,+⊤;>+⊤pe="ype_sc">Justef" href="AdomLib.html#typd">Definit>,
   ">+⊤pe="ype_scope:x_'→'_x">an class="idi.fr/distruation">+⊤pe="ype_scope:x_on+⊤pe="ype_sc">Justef" href="AdomLib.html#typd">Definit>,
   ">+⊤pe="ype_scope:x_'→'_x">an class="idi.fr/distruation">+⊤pe="ype_scope:x_on+⊤pe="ype_sc">Justef" href="AdomLib.html#typd">Definit>,+⊤}t">t) (Degaan clan>: Degaan r">k at B"AdomLib.html#type="vaa class="idref" href="AdomLigaan _spl#C"><="keyword">with+⊤pe="ype_sc">Justef" href="AdomLib.html#typd">Definit>,
   idref" href="AdomLib.html#P">P (<="keyword">with x'f" href="AdomLib.html#typd">Definit>,s , All on">→ toString `{ToString r) (rs level 39).

Definition
an class="idi.fr/distruation">+⊤pe="ype_scope:x_on+⊤pe="yppe="var">y `{ToString r) (rs +⊤pe="ype_scass="id" type="var">A: <>B B s Recd" span class="id" tpre_l class_specf" href="AdomLib.html#typrecd" ">pre_l class_specr">k at +⊤pe="ype_scope:x_oiabpre_l classf" href="AdomLib.html#typrecd" ">pre_l classr">k <> x'f" href="AdomLib.html#typd">Definit>,B"AdomLib.html#type="vaa class="idref" href="AdomLigaan _spl#C"><="keyword">with+⊤pe="ype_sc">Justef" href="AdomLib.html#typd">Definit>,
   idref" href="AdomLib.html#P">P→#A">+⊤{>+⊤pe="ype_scn>+⊤ +⊤pe="ype_sc">Justef" href="AdomLib.html#typd">Definit>,+⊤pe="ype_scn>+⊤ <="keyword">withk trib/8.4pl5/stdlib/Coq.Unicode.Utf8_PLf" href="AdomLib.html#typd">DefinitPLym8_corspan c>A+⊤ +⊤pe="ype_scass="id" type="var">A: <>+⊤pe="yppe="var">y ⇒
   ">+⊤pe="ype_scope:x_'→'_x">an class="idi.fr/distruation">+⊤pe="ype_scope:x_ontopli>topli>topli>topli>topli>topli>topli>topli>topli>topli>topli>topli>topli>topli>topli>topli>topli>topli>topli>topli>topli>topli>topli>topli>topli>topli>topli>topli>topli>topli>topli>topli>toplinuation">+⊤pe="ype_scn>
+⊤ +⊤pe="ype_sc">Justlift2">top_lift2 {+⊤ s A+⊤ bool.html#B">k trib/8.4pl5/stdlib/Coq.">+⊤pe="ype_scope:x_'→'_x">an class="idi.fr/distruation">+⊤pe="ype_scope:x_ons A+⊤pe="ype_sca> bool.html#B">kation">+⊤;>_sound _soundspan class=itruation">+⊤pe="ype_scn>+⊤ +⊤pe="ype_scope:x_oiabef" href="AdomLib.html#typd">Definit>,+⊤pe="ype_scn>+⊤ s A+⊤s A s xpl.joi> span class="trib/8.4pl5/stdlib/Coq.Unicode.Utf8_PLf" href="AdomLib.html#typd">DefinitPLym8_corspan c>A+⊤ topli}t">) (k at +⊤pe="ype_scope:x_oiabpre_l classf" href="AdomLib.html#typrecd" ">pre_l classr">k <> x'f" href="AdomLib.html#typd">Definit>,C) : Definit>,+⊤ :=
  +⊤>topli>topli>topli>toplinicode.Utf8_core.html#:type_scoplass="id" type="keyword">match x, +⊤pe="ype_s>topli>topli>topli>toplift_bind {+⊤pe="ype_s>topli>topli>topli>toplift_bind {an class="idi.fr/distruation"_'→'_x">an class="idi.fr/distruion">+⊤pe="ype_s>topli>topli>topli>toplift_"AdomLib.html#type="variable">B B B fun Bv htmr">k trib/8.4pl5/stdlib/Coq.a class="idref" href="AdomLiBuild_weak_l classf" href="AdomLib.html#type="variable">:/Coq.Unicode.Utf8_core.html#:type_sca class="idref" href="AdomLiBuild_weak_l classf" href="AdomLib.html#type="variable">sp; | strib/8.4pl5/stdlib/Coq.Unicode.Utfa class="idref" href="AdomLiBuild_weak_l classf" href="AdomLib.html#type="variable">pl.htmr">k trib/8.4pl5/stdlib/Coq.a class="idref" href="AdomLiBuild_weak_l classf" href="AdomLib.html#type="variable">PLym8_corspantrib/8.4pl5/stdlib/Coq.a class="idref" href="AdomLiBuild_weak_l classf" href="AdomLib.html#type="variable">e="notation"" href="AdomLib.ht>toplitrib/8.4pl5/stdlib/Coq.a class="idref" href="AdomLiBuild_weak_l classf" href="AdomLib.html#type="variable">8_core.html#:type_scope:x_'→'_x">.Init.Logic.htmlrib/8.4pl5/stdlib/Coq.a class="idref" href="AdomLiBuild_weak_l classf" href="AdomLib.html#type="variable">:/Coq.Unicode.U_'→'_x">an class="idi.fr/distruion">+⊤pe="ype_s>toplitrib/8.4pl5/stdlib/Coq.a class="idref" href="AdomLiBuild_weak_l classf" href="AdomLib.html#type="variable">8_core.html#:type_scope:x_'→'_x">joi>span class="trib/8.4pl5/stdlib/Coq.a class="idref" href="AdomLiBuild_weak_l classf" href="AdomLib.html#type="variable">:/Coq.Unicode.Utf8_core.html#:type_sca class="idref" href="AdomLiBuild_weak_l classf" href="AdomLib.html#type="variable">joi>span class="trib/8.4pl5/stdlib/Coq.a class="idref" href="AdomLiBuild_weak_l classf" href="AdomLib.html#type="variable">strib/8.4pl5/stdlib/Coq.Unicode.Utfa class="idref" href="AdomLiBuild_weak_l classf" href="AdomLib.html#type="variable">pl.joi>span class="trib/8.4pl5/stdlib/Coq.a class="idref" href="AdomLiBuild_weak_l classf" href="AdomLib.html#type="variable">PLym8_corspantrib/8.4pl5/stdlib/Coq.a class="idref" href="AdomLiBuild_weak_l classf" href="AdomLib.html#type="variable">e="notation"" href="AdomLib.ht>toplitrib/8.4pl5/stdlib/Coq.a class="idref" href="AdomLiBuild_weak_l classf" href="AdomLib.html#type="variable">8_core.html#:type_scope:x_'→'_x">wan cspan class=trib/8.4pl5/stdlib/Coq.a class="idref" href="AdomLiBuild_weak_l classf" href="AdomLib.html#type="variable">:/Coq.Unicode.Utf8_core.html#:type_sca class="idref" href="AdomLiBuild_weak_l classf" href="AdomLib.html#type="variable">joi>span class="trib/8.4pl5/stdlib/Coq.a class="idref" href="AdomLiBuild_weak_l classf" href="AdomLib.html#type="variable">strib/8.4pl5/stdlib/Coq.Unicode.Utfa class="idref" href="AdomLiBuild_weak_l classf" href="AdomLib.html#type="variable">pl.wan cspan class="trib/8.4pl5/stdlib/Coq.a class="idref" href="AdomLiBuild_weak_l classf" href="AdomLib.html#type="variable">PLym8_corspantrib/8.4pl5/stdlib/Coq.a class="idref" href="AdomLiBuild_weak_l classf" href="AdomLib.html#type="variable">e="notation"" href="AdomLib.ht|}t">tLean r">kk at +⊤pe="ype_scope:x_oiabpre_l classf" href="AdomLib.html#typrecd" ">pre_l classr">k <> x'f" href="AdomLib.html#typd">Definit>,at +⊤pe="ype_scope:x_oiabpre_l class_specf" href="AdomLib.html#typrecd" ">pre_l class_specr">k DefinitPLym8_corspan c>ADefinitG,aomL="variable">C) : Definit>,s , All C) : k DefinitPLym8_corspan)>C) : Degaan clan>: Degaan r">k <>ADefinitG, k at DefinitTr">k <>Aan class="idi.fr/distruation">+⊤pe="ype_scope:x_onDefinitTr">k <>Aan class="idi.fr/distruation">+⊤pe="ype_scope:x_onA: Justpre_l classf" href="AdomLib.html#typrecd" ">pre_l classr">k <> xTf" href="AdomLib.html#typd">DefinitTr">k station">+⊤{ef="AdomLib.html#type="vapan> pl.htmr">k trib/8.4pl5/stdlib/Coq.pan> :/Coq.Unicode.Utf8_core.html#:type_scpan> adom.γ">8_core.html#:type_scope:x_'→'_x"> pl.joi>span class="trib/8.4pl5/stdlib/Coq.Unicode.Utf8_auild_pre_l classf" href="AdomLib.html#type="variable">s="id" type="notation">+⊤ trib/8.4pl5/s"uation">+⊤pe="ype_sca> :/Coq.Unicode.U"id" type="notation">→s="id" type="var">x,
  adom.γ">s="id" type="notation">+⊤
trib/8.4pl5/s""id" type="notation">→e">rs
  B s="id" type="n"id" type="notation">→ vapid" type="notation">+⊤8_core.html#:type_scope:x_'→'_x"> pl.wan cspan class="trib/8.4pl5/stdlib/Coq.Unicode.Utf8_auild_pre_l classf" href="AdomLib.html#type="variable">s="id" type="notation">+⊤ trib/8.4pl5/s"uation">+⊤pe="ype_sca> :/Coq.Unicode.U"id" type="notation">→s="id" type="var">x,
  adom.γ">s="id" type="notation">+⊤
trib/8.4pl5/s""id" type="notation">→e">rs
  B s="id" type="n"id" type="notation">→ vapid" type="notation">+⊤tLean r">kk at at +⊤ +⊤ B A+⊤ +⊤pe="ype_scass="id" type="var">A: <>+⊤pe="yppe="var">y ⇒ /ym8_coretistru>
   ">+⊤pe="ype_scope:x_'→'_x">an class="idi.fr/distruation">+⊤pe="ype_scope:x_onA
+⊤A: <>topli>topli>topli>topli>toplipe="ype_scope:x_on<="keyword">with+⊤pe="ype_sc">JustTf" href="AdomLib.html#typd">DefinitTr">k <>AP (pre_l class_specr">k C) : k B s DefinitG,ident, t k id" type="="var">_, AllB"AdomLib.html#type="va">Justpre_l classf" href="AdomLib.html#typrecd" ">pre_l classr">k <> xle">x B"AdomLib.html#type="va">Justpre_l classf" href="AdomLib.html#typrecd" ">pre_l classr">k <> xAdomLib.html#P">P (pre_l classr">k d">∀ x +⊤pe="yppe="var">y ⇒ k <> xAdomLib.html#P">P+⊤{ef="AdomLib.html#type="vapan> pl.htmr">k trib/8.4pl5/stdlib/Coq.pan> s="id" type="notation">+⊤ id" type=pl5/s"uation">+⊤pe="ype_sca> :/Coq.Unicode.U"id" type="notation">→lettistruat+⊤pe="ype_sca> 'strib/8.4pl5/stdlib/Coq.Unicode.Utfa> atrib/8.4pl5/stdlib/Coq.Unicode.Utfa> ,trib/8.4pl5/stdlib/Coq.Unicode.Utfa> btrib/8.4pl5/stdlib/Coq.Unicode.Utfa> e="notation">∀ :/Coq.Unicode.Utf8_core.html#:type_scpan> s="id" type="n"id" type="notation">→i>span cltlettistruat+⊤pe="ype_sca> 'strib/8.4pl5/stdlib/Coq.Unicode.Utfa> a'trib/8.4pl5/stdlib/Coq.Unicode.Utfa> ,trib/8.4pl5/stdlib/Coq.Unicode.Utfa> b'trib/8.4pl5/stdlib/Coq.Unicode.Utfa> e="notation">∀ :/Coq.Unicode.Utf8_core.html#:type_scpan> s'="id" type="n"id" type="notation">→i>span cl"definition">topli>topli>topli>topli>topli>topli>topli>topli>topli>topli>topli>topli>topli>topli>topli>topli>topli>topli>topli="AdomLib.html#type="vapan> pl.htmr">k trib/8.4pl5/stdlib/Coq.pan> P/span> ⇒ = atrib/8.4pl5id" type="notation">= ad" type=pl5/s"uation">+⊤pe="ype_sca> &amli>amli_core.html#:type_scope:x_'→'_x"> pl.htmr">k trib/8.4pl5/stdlib/Coq.pan> PBr">k trib/8.4pl5/stdlib/Coq.pan> mr">k trib/8.4pl5/stdlib/Coq.pan> b'trib/8.4pl5/ href="AdomLib.ht>toplitrib/8.4pl5/stdlib/Coq.pan> 8_core.html#:type_scope:x_'→'_x"> pl.joi>span class="trib/8.4pl5/stdlib/Coq.Unicode.Utf8_auild_pre_l classf" href="AdomLib.html#type="variable">s="id" type="notation">+⊤ s'="id" type="s"uation">+⊤pe="ype_sca> :/Coq.Unicode.U"id" type="notation">→lettistruat+⊤pe="ype_sca> 'strib/8.4pl5/stdlib/Coq.Unicode.Utfa> atrib/8.4pl5/stdlib/Coq.Unicode.Utfa> ,trib/8.4pl5/stdlib/Coq.Unicode.Utfa> btrib/8.4pl5/stdlib/Coq.Unicode.Utfa> e="notation">∀ :/Coq.Unicode.Utf8_core.html#:type_scpan> s="id" type="n"id" type="notation">→i>span cltlettistruat+⊤pe="ype_sca> 'strib/8.4pl5/stdlib/Coq.Unicode.Utfa> a'trib/8.4pl5/stdlib/Coq.Unicode.Utfa> ,trib/8.4pl5/stdlib/Coq.Unicode.Utfa> b'trib/8.4pl5/stdlib/Coq.Unicode.Utfa> e="notation">∀ :/Coq.Unicode.Utf8_core.html#:type_scpan> s'="id" type="n"id" type="notation">→i>span cl"definition">topli>topli>topli>topli>topli>topli>topli>topli>topli>topli>topli>topli>topli>topli>topli>topli>topli>topli>topliLib.ht>toplitrib/8.4pl5/stdlib/Coq.pan> doCoq.Unicode.Utf8_core.html#:type_scpan> α" type=pl5/s"uation">+⊤pe="ype_sca> <-_core.html#:type_scope:x_'→'_x"> pl.joi>span class="trib/8.4pl5/stdlib/Coq.Unicode.Utf8_auild_pre_l classf" href="AdomLib.html#type="variable">P/span> ⇒ = atrib/8.4pl5id" type="notation">= ad" type=pl5/trib/8.4pl5/stdlib/Coq.pan> 8_core.html#"definition">topli>topli>topli>topli>topli>topli>topli>topli>topli>topli>topli>topli>topli>topli>topli>topli>topli>topli>topliLib.ht>toplitrib/8.4pl5/stdlib/Coq.pan> doCoq.Unicode.Utf8_core.html#:type_scpan> β" type=pl5/s"uation">+⊤pe="ype_sca> <-_core.html#:type_scope:x_'→'_x"> pl.joi>span class="trib/8.4pl5/stdlib/Coq.Unico/a> PBr">k trib/8.4pl5/stdlib/Coq.pan> mr">k trib/8.4pl5/stdlib/Coq.pan> b'trib/8.4pl5/stdlib/Coq.Unicode.Utfa> 8_core.html#"definition">topli>topli>topli>topli>topli>topli>topli>topli>topli>topli>topli>topli>topli>topli>topli>topli>topli>topli>topliLib.ht>toplitrib/8.4pl5/stdlib/Coq.pan> B strib/8.4pl5/stdlib/Coq.Unicode.Utfa> α" type=pl5//stdlib/Coq.Unicode.Utfa> ,trib/8.4pl5.Utf8_core.html#:type_scpan> β" type=pl5//stdlib/Coq.Unicode.Utfa> e="notation"/ href="AdomLib.ht>toplitrib/8.4pl5/stdlib/Coq.pan> 8_core.html#:type_scope:x_'→'_x"> pl.wan cspan class="trib/8.4pl5/stdlib/Coq.Unicode.Utf8_auild_pre_l classf" href="AdomLib.html#type="variable">s="id" type="notation">+⊤ id" type=pl5/s"uation">+⊤pe="ype_sca> :/Coq.Unicode.U"id" type="notation">→lettistruat+⊤pe="ype_sca> 'strib/8.4pl5/stdlib/Coq.Unicode.Utfa> atrib/8.4pl5/stdlib/Coq.Unicode.Utfa> ,trib/8.4pl5/stdlib/Coq.Unicode.Utfa> btrib/8.4pl5/stdlib/Coq.Unicode.Utfa> e="notation">∀ :/Coq.Unicode.Utf8_core.html#:type_scpan> s="id" type="n"id" type="notation">→i>span cltlettistruat+⊤pe="ype_sca> 'strib/8.4pl5/stdlib/Coq.Unicode.Utfa> a'trib/8.4pl5/stdlib/Coq.Unicode.Utfa> ,trib/8.4pl5/stdlib/Coq.Unicode.Utfa> b'trib/8.4pl5/stdlib/Coq.Unicode.Utfa> e="notation">∀ :/Coq.Unicode.Utf8_core.html#:type_scpan> s'="id" type="n"id" type="notation">→i>span cl"definition">topli>topli>topli>topli>topli>topli>topli>topli>topli>topli>topli>topli>topli>topli>topli>topli>topli>topli>topliLib.ht>toplitrib/8.4pl5/stdlib/Coq.pan> doCoq.Unicode.Utf8_core.html#:type_scpan> α" type=pl5/s"uation">+⊤pe="ype_sca> <-_core.html#:type_scope:x_'→'_x"> pl.wan cspan class="trib/8.4pl5/stdlib/Coq.Unicode.Utf8_auild_pre_l classf" href="AdomLib.html#type="variable">P/span> ⇒ = atrib/8.4pl5id" type="notation">= ad" type=pl5/trib/8.4pl5/stdlib/Coq.pan> 8_core.html#"definition">topli>topli>topli>topli>topli>topli>topli>topli>topli>topli>topli>topli>topli>topli>topli>topli>topli>topli>topliLib.ht>toplitrib/8.4pl5/stdlib/Coq.pan> doCoq.Unicode.Utf8_core.html#:type_scpan> β" type=pl5/s"uation">+⊤pe="ype_sca> <-_core.html#:type_scope:x_'→'_x"> pl.wan cspan class="trib/8.4pl5/stdlib/Coq.Unicode.Utf8_auild_pre_l classf" href="AdomLib.html#type="variable">PBr">k trib/8.4pl5/stdlib/Coq.pan> mr">k trib/8.4pl5/stdlib/Coq.pan> b'trib/8.4pl5/stdlib/Coq.Unicode.Utfa> 8_core.html#"definition">topli>topli>topli>topli>topli>topli>topli>topli>topli>topli>topli>topli>topli>topli>topli>topli>topli>topli>topliLib.ht>toplitrib/8.4pl5/stdlib/Coq.pan> B strib/8.4pl5/stdlib/Coq.Unicode.Utfa> α" type=pl5//stdlib/Coq.Unicode.Utfa> ,trib/8.4pl5.Utf8_core.html#:type_scpan> β" type=pl5//stdlib/Coq.Unicode.Utfa> e="notation"/ href="AdomLib.ht|}t">t) (: _, kAllB"AdomLib.html#type="vaa class="idref" href="AdomLigaan _spl#C"><="keyword">with+⊤pe="ype_sc">Justle">x JustC clan>: B"AdomLib.html#type="vaa class="idref" href="AdomLigaan _spl#C"><="keyword">with+⊤pe="ype_sc">JustAdomLib.html#P">JustCbclan>: B"AdomLib.html#type="vaa class="idref" href="AdomLigaan _spl#C"><="keyword">with∀ x +⊤pe="yppe="var">y ⇒ k <> xAdomLib.html#P">Pd">∀ +⊤pe="yppe="var">yk <> xCbclan>: +⊤+⊤pe="yppe="var">y+⊤ pan c#:type_scope:x_'→'_x">+⊤pe="yppe="var">y+⊤ →lettistruat'Utf8_core.html#:type_scn+⊤pe="yppe="var">y ⇒ +⊤pe="yppe="var">yan cl>="id" tytf8_core.html#:type_scn+⊤pe="yppe="var">y ⇒ := c>Ai>span cltlettistruat'Utf8_core.html#:type_scn+⊤pe="yppe="var">y ⇒ +⊤pe="yppe="var">yan cl>'="id" tytf8_core.html#:type_scn+⊤pe="yppe="var">y ⇒ := c>A→i>span cl"definition">topli>topli>topli>topli>topli>topli>topli>topli>topli/pe:x_'→'_x">B"AdomLib.html#type="vaa class="idref" href="Aia.fr∈ k <> s pe="ype_scope:x_ons+⊤pe="ype_scope:x_'→'_x">an class="i an cl>'="id" t>B"AdomLib.html#type="vaa class="idref" href="Aia.fr∈ k <> s pe="ype_scope:x_on="id" t+x">Lean r">k_, k_, B"AdomLib.html#type="va">Justpre_l classf" href="AdomLib.html#typrecd" ">pre_l classr">k <> xle">x _, B"AdomLib.html#type="va">Justpre_l classf" href="AdomLib.html#typrecd" ">pre_l classr">k <> xAdomLib.html#P">AllB"AdomLib.html#type="vaa class="idref" href="AdomLigaan _spl#C"><="keyword">with+⊤pe="ype_sc">Justle">x JustC clan>: B"AdomLib.html#type="vaa class="idref" href="AdomLigaan _spl#C"><="keyword">with+⊤pe="ype_sc">JustAdomLib.html#P">JustCbclan>: B"AdomLib.html#type="va">Justpre_l class_specf" href="AdomLib.html#typrecd" ">pre_l class_specr">k x = x B"AdomLib.html#type="va">Justpre_l class_specf" href="AdomLib.html#typrecd" ">pre_l class_specr">k k trib/8.4pl5/stdlib/Coq.pan> P (pre_l class_specr">k C) : k x = k>Pd">∀ = x x">Mo>WPFun2r">k CkTREE="variable">x">Mo>Pr">k := c>ATree_Prclartiestrib/8.4pl5 trib/8.4pl5/stdlib/Coq.pan> Ttrib/8.4pl5x">→Sec' class="idref" href=WPFun2.el'f" href="AdomLib.html#typsec' cln>+⊤<"id" type="notation">→ContexttistruatC→Tyef:type_s)"definition">topli>topli>topli>topli>topli>topli>topli>topli>toplie="tactic">at +⊤pe="ype_scope:x_oiabWPFun2.pre_l classf" href="AdomLib.html#typrecd" ">pre_l classr">k <> xel'f" href="AdomLib.html#typs="id" typtopli>topli>topli>topli>topli>topli>topli>topli>toplie="tactic">at B"AdomLib.html#type="vaa class="idref" href="AdomLigaan _spl#C"><="keyword">with+⊤pe="ype_sc">Justel'f" href="AdomLib.html#typs="id" typ xAdomLib.html#P">"definition">topli>topli>topli>topli>topli>topli>topli>topli>toplie="tactic">at +⊤pe="ype_scope:x_oiabWPFun2.pre_l class_specf" href="AdomLib.html#typrecd" ">pre_l class_specr">k DefinitPLym8_corspan c>A+⊤<"id" type="notation">→ →Tyef:type_s>:= c>AA+⊤<"id" type="notation">→ k C+⊤pe="ype_scope:x_oiabT.el'f" href="AdomLib.html#typaximLf"T.+⊤pe="ype_scope:x_oiabWPFun2.'f" href="AdomLib.html#typan>
&nbttrib/8.4pl5>P
( (+⊤>+⊤<"id" type="notation">→match="id" t>B"AdomLib.html#type="va_scope:x_oiabT.ge'f" href="AdomLib.html#typaximLf"T.getr">k ">∀ +⊤pe="ype_sc">Just"AdomLib.html#::x_'+⊤'">with="id" tation">+⊤>+⊤ef="AdomLib.html#type="van+⊤pe="yppe="var">y ⇒ Soms="id" type="n"id" type="notation">an clr="id" t>⇒/span> (B an clr="id" tation">+⊤>+⊤ef="AdomLib.html#type="van+⊤pe="yppe="var">y ⇒ Nonspan <⇒/s"id" type="notation">→ef" href="" href="AdomLib.ht>topli/span><"id" type="notation">→end href="x">+⊤<"id" type="notation">→ k C+⊤pe="ype_scope:x_oiabWPFun2.'f" href="AdomLib.html#typan>
&nbttrib/8.4pl5>PC+⊤pe="ype_scope:x_oiabT.el'f" href="AdomLib.html#typaximLf"T.+⊤pe="ype_scope:x_oiabWPFun2.el'.el'f" href="AdomLib.html#typs="id" typ
(+⊤>+⊤<"id" type="notation">→match="id" t>B"AdomLib.html#type="va_scope:x_oiabvf" href="AdomLib.html#typs="id" typv="id" type="n"id" type="notation">→with="id" tation">+⊤>+⊤ef="id" type="notation">→ef" href=">⇒/span> (k ">∀ +⊤pe="ype_sc">Just"AdomLib.html#::x_'+⊤'">+⊤>+⊤ef="AdomLib.html#type="va_scope:x_oiabWPFun2.BB an clv' href=">⇒/span> (k ">∀ an clv' href=">ruation">+⊤pe="ype_sc">Just"AdomLib.html#::x_'+⊤'">+⊤>+⊤<"id" type="notation">→end href="x">+⊤<"id" type="notation">→Lean r">kan cl#:type_scope:x_'→'_x">:ation">+⊤>+⊤<"AdomLib.html#type="va_scope:x_oiabWPFun2.ge'f" href="AdomLib.html#typan>
&nbgetr">k
">∀ k C<"AdomLib.html#type="va_scope:x_oiabWPFun2.se'f" href="AdomLib.html#typan>
&nbsetr">k ruation">+⊤pe="ype_sc">Just"AdomLib.html#::x_'+⊤'">+⊤pe="ype_sc">Justvf" href="AdomLib.html#typs="id" typv="id" type="id" type="variable">s+⊤pe="ype_scope:x_'→'_x"><>
→s="id" type="var">x,
  BA
k ">∀ e">rs
   "AdomLib.html#type="va_scope:x_oiabWPFun2.ge'f" href="AdomLib.html#typan>
&nbgetr">k ">∀ k ruation">+⊤pe="ype_sc">Just"AdomLib.html#::x_'+⊤'">+⊤<"id" type="notation">→ :
&nbhtmr">k
(s+⊤pe="ype_scope:x_'→'_x">an class="idi.fr/distruation">+⊤pe="ype_scope:x_onAs+⊤pe="ype_scope:x_'→'_x">an class="idi.fr/distruation">+⊤pe="ype_scope:x_onA+⊤pe="yppe="var">y ⇒ : +⊤>+⊤+⊤pe="yppe="var">y+⊤ pan c#:type_scope:x_'→'_x">+⊤ +⊤>+⊤<"AdomLib.html#type="va_scope:x_oiabWPFun2.P.for_allclan>:
&nbP.for_allym8_coretis c>A
+⊤pe="yppe="var">y+⊤ pan ca"id" typ+⊤ →match="id" t>B"AdomLib.html#type="va_scope:x_oiabT.ge'f" href="AdomLib.html#typaximLf"T.getr">k ">∀ = with="id" tation">+⊤>+⊤/span>/span>/span>/span>/span>/span>/span>/span>/span>/span>/span>/span>/span>/span>/span>/span>/span>/span>/span>/span>ef="AdomLib.html#type="van+⊤pe="yppe="var">y ⇒ Soms="id" type="n"id" type="notation">an cla' href=">⇒/span> (k trib/8.4pl5/stdlib/Coq.pan> DefinitPLym8_corspan c"id" type="notation">an cla' href=">trib/8.4pl5/stdlib/Coq.pan> Definits="id" type=ation">+⊤>+⊤/span>/span>/span>/span>/span>/span>/span>/span>/span>/span>/span>/span>/span>/span>/span>/span>/span>/span>/span>/span>ef="AdomLib.html#type="van+⊤pe="yppe="var">y ⇒ Nonspan <⇒/s"AdomLib.html#type="van+⊤pe="yppe="var">y ⇒ fa+⊤>+⊤/span>/span>/span>/span>/span>/span>/span>/span>/span>/span>/span>/span>/span>/span>/span>/span>/span>/span>/span>/span><"id" type="notation">→end href=")x">+⊤<"id" type="notation">→Lean r">kk C+⊤pe="ype_scope:x_oiabWPFun2.'f" href="AdomLib.html#typan>
&nbttrib/8.4pl5>P+⊤
>+⊤<"AdomLib.html#type="va_scope:x_oiabWPFun2.lebclan>:

&nbhtmr">k ruation">+⊤pe="ype_sc">Just"AdomLib.html#::x_'+⊤'">s+⊤pe="ype_scope:x_'→'_x"><>
+⊤pe="yppe="var">y ⇒ arisrib/8.4pl5/sd" type="variable">s+⊤pe="ype_scope:x_'→'_x"><>+⊤pe="ype_scope:x_on<="id" type=ation">+⊤>+⊤<"AdomLib.html#type="va">+⊤pe="ype_scope:x_'→'_x">an clas'∀">+⊤ an clp:type_scetistruation">+⊤pe="ype_scope:x_oiabT.el'f" href="AdomLib.html#typaximLf"T.+⊤pe="ype_scope:x_'→'_x">an clas'∀">+⊤ k C<"AdomLib.html#type="va_scope:x_oiabWPFun2.pl.htmf" href="AdomLib.html#typprojec' cln>pl.htmr">k trib/8.4pl5/stdlib/Coq.pan> DefinitPLym8_corspan>Pd">∀ k ">∀ +⊤pe="ype_sc">Just"AdomLib.html#::x_'+⊤'">Pd">∀ k ">∀ +⊤pe="ype_sc">Justidref" href="http://coq.inria.fr/distrib/8.4pl5/"id" type="variable">s+⊤pe="ype_scope:x_'→'_x"><>+⊤pe="yppe="var">y ⇒ arisrib/8.4pl5/x">+⊤<"id" type="notation">→Lean r">k+⊤>+⊤/span>/span>/span>/span>pe="ype_scope:x_on+⊤pe="ype">+⊤pe="ype_scope:x_'→'_x">an clas'∀">+⊤ an cls="id" tystruation">+⊤pe="ype">+⊤pe="ype_scope:x_'→'_x">an clas'∀">+⊤ k trib/8.4pl5/stdlib/Coq.pan> DefinitPLym8_corspan ruation">+⊤pe="ype_sc">Just"AdomLib.html#::x_'+⊤'">+⊤pe="ype_scope:x_'→'_x"><>+⊤pe="yppe="var">y ⇒ arisrib/8.4pl5/>"definition">topli>topli>topli>topli>topli>topli>topliC+⊤pe="ype_scope:x_oiabWPFun2.'f" href="AdomLib.html#typan>
&nbttrib/8.4pl5>P
(
&nbhtmr">k ruation">+⊤pe="ype_sc">Just"AdomLib.html#::x_'+⊤'">+⊤pe="ype_scope:x_'→'_x"><>
+⊤pe="yppe="var">y ⇒ arisrib/8.4pl5/x">+⊤<"id" type="notation">→ clan>:
&nbjoi>span class="tpe="ype_scope:x_on
(s+⊤pe="ype_scope:x_'→'_x">an class="idi.fr/distruation">+⊤pe="ype_scope:x_on (s+⊤pe="ype_scope:x_'→'_x">an class="idi.fr/distruation">+⊤pe="ype_scope:x_on (+⊤>+⊤+⊤pe="ype_scope:x_oiabT.combinsf" href="AdomLib.html#typaximLf"T.combinsrib/8.4pl5/sC<"AdomLib.html#type="van+⊤pe="yppe="var">y+⊤ pan cu:type_scope:x_'→'_x">+⊤pe="yppe="var">y+⊤ →match="id" t>B"AdomLib.html#type="va_scope:x_oiabuAdomLib.html#::x_'+⊤'">B"AdomLib.html#type="va_scope:x_oiabvf" href="AdomLib.html#typs="id" typv="id" type="n"id" type="notation">→with="id" tation">+⊤>+⊤/span>/span>/span>/span>/span>/span>/span>/span>/span>/span>/span>/span>/span>/span>/span>/span>/span>/span>ef="AdomLib.html#type="van+⊤pe="yppe="var">y ⇒ Nonspan ,cope:x_'→'_x">+⊤>+⊤/span>/span>/span>/span>/span>/span>/span>/span>/span>/span>/span>/span>/span>/span>/span>/span>/span>/span>ef=pe:x_'→'_x">B"AdomLib.html#type="van+⊤pe="yppe="var">yNonspan <⇒/s"AdomLib.html#type="van+⊤pe="yppe="var">y ⇒ Nonspan ation">+⊤>+⊤/span>/span>/span>/span>/span>/span>/span>/span>/span>/span>/span>/span>/span>/span>/span>/span>/span>/span>ef="AdomLib.html#type="van+⊤pe="yppe="var">y ⇒ Soms="id" type="n"id" type="notation">an clu'="id" t,>B"AdomLib.html#type="van+⊤pe="yppe="var">y ⇒ Soms="id" type="n"id" type="notation">an clv' href=">⇒ation">+⊤>+⊤/span>/span>/span>/span>/span>/span>/span>/span>/span>/span>/span>/span>/span>/span>/span>/span>/span>/span>>+⊤<"id" type="notation">→match="id" t>B"AdomLib.html#type="va_scope:x_oiabff" href="AdomLib.html#typs="id" typf="id" type="n"id" type="notation">an clu'="id" ttr"id" type="notation">an clv' href=">r"id" type="notation">→with="id" tation">+⊤>+⊤/span>/span>/span>/span>/span>/span>/span>/span>/span>/span>/span>/span>/span>/span>/span>/span>/span>/span>/span>/span>ef="AdomLib.html#type="va_scope:x_oiabWPFun2.BB an clr="id" t<⇒/s"AdomLib.html#type="van+⊤pe="yppe="var">y ⇒ Soms="id" type="n"id" type="notation">an clr="id" tation">+⊤>+⊤/span>/span>/span>/span>/span>/span>/span>/span>/span>/span>/span>/span>/span>/span>/span>/span>/span>/span>/span>/span>ef="id" type="notation">→ef" href=">⇒/span> (+⊤pe="yppe="var">y ⇒ Nonspan ation">+⊤>+⊤/span>/span>/span>/span>/span>/span>/span>/span>/span>/span>/span>/span>/span>/span>/span>/span>/span>/span>>+⊤<"id" type="notation">→end href="ation">+⊤>+⊤/span>/span>/span>/span>/span>/span>/span>/span>/span>/span>/span>/span>/span>/span>/span>/span>/span>/span><"id" type="notation">→end href=")x">+⊤<"id" type="notation">→Lean r">k_mohttonsf" href="AdomLib.html#typlean cljoi>_mohttonsspan class="tpe="ype_scope:x_onk+⊤>+⊤<"AdomLib.html#type="va">+⊤pe="ype_scope:x_'→'_x">an class="idi.fr/distruation">+⊤pe="ype_scope:x_ostrib/8.4pl5/stdlib/Coq.Unicode.Utf">+⊤pe="ype_scope:x_'→'_x">an clas'∀">+⊤ an clu:type_scope:x_'→'_x">+⊤pe="yppe="var">yan clas'∀">+⊤ k trib/8.4pl5/stdlib/Coq.pan> DefinitPLym8_corspan ruation">+⊤pe="ype_sc">JustuAdomLib.html#::x_'+⊤'">B"AdomLib.html#type="va_scope:x_oiabvf" href="AdomLib.html#typs="id" typv="id" type="n>∀ +⊤pe="ype_scope:x_'→'_x"><>+⊤pe="yppe="var">y ⇒ arisrib/8.4pl5/ d" type="variable">s+⊤pe="ype_scope:x_'→'_x">an class="idi.fr/distruation">+⊤pe="ype_scope:x_on+⊤>+⊤/span>/span>/span>/span>/span>/span>/span>/span>d" type="variable">s+⊤pe="ype_scope:x_'→'_x">an class="i +⊤pe="ype_scope:x_'→'_x">an clas'∀">+⊤ an clw="id" ttr"id" type="notation">an clv' href="/stdlib/Coq.Unicode.Utf">+⊤pe="ype_scope:x_'→'_x">an clas'∀">+⊤ +⊤pe="ype_scope:x_'→'_x"><>B k ruation">+⊤pe="ype_sc">+⊤pe="ype_scope:x_'→'_x">an class="idi.fr/distruation">+⊤pe="ype_scope:x_on k trib/8.4pl5/stdlib/Coq.pan> DefinitPLym8_corspan ruation">+⊤pe="ype_sc">JustuAdomLib.html#::x_'+⊤'">B"AdomLib.html#type="va_scope:x_oiabvtrib/8.4pl5/stdlib/Coq.Strk ruation">+⊤pe="ype_sc">+⊤pe="ype_scope:x_'→'_x"><>+⊤pe="yppe="var">y ⇒ arisrib/8.4pl5/d" type="variable">s+⊤pe="ype_scope:x_'→'_x">an class="i s+⊤pe="ype_scope:x_'→'_x">an class="i s+⊤pe="ype_scope:x_'→'_x">an class="i +⊤pe="ype_scope:x_'→'_x">an clas'∀">+⊤ an clw="id" ttr"id" type="notation">an clv' href="/stdlib/Coq.Unicode.Utf">+⊤pe="ype_scope:x_'→'_x">an clas'∀">+⊤ +⊤pe="ype_scope:x_'→'_x"><>B k ruation">+⊤pe="ype_sc">+⊤pe="ype_scope:x_'→'_x">an class="idi.fr/distruation">+⊤pe="ype_scope:x_on k trib/8.4pl5/stdlib/Coq.pan> DefinitPLym8_corspan ruation">+⊤pe="ype_sc">JustuAdomLib.html#::x_'+⊤'">B"AdomLib.html#type="va_scope:x_oiabvtrib/8.4pl5/stdlib/Coq.Strk ruation">+⊤pe="ype_sc">+⊤pe="ype_scope:x_'→'_x"><>+⊤pe="yppe="var">y ⇒ arisrib/8.4pl5/d" type="variable">s+⊤pe="ype_scope:x_'→'_x">an class="i +⊤pe="ype_sc">+⊤pe="ype_scope:x_'→'_x">an class="idi.fr/distruation">+⊤pe="ype_scope:x_o)r">k ruation">+⊤pe="ype_sc">+⊤pe="ype_scope:x_'→'_x">an class="idi.fr/distruation">+⊤pe="ype_scope:x_on+⊤>+⊤<"AdomLib.html#type="va_scope:x_oiabWPFun2.lebclan>:
&nbhtmr">k ruation">+⊤pe="ype_sc">Just"AdomLib.html#::x_'+⊤'">=+⊤pe="ype_scope:x_'→'_x"><>
+⊤pe="yppe="var">y ⇒ arisrib/8.4pl5/ d" type="variable">s+⊤pe="ype_scope:x_'→'_x">an class="i k trib/8.4pl5/stdlib/Coq.pan> :
&nbhtmr">k ruation">+⊤pe="ype_sc">Just"AdomLib.html#::x_'+⊤'">k ruation">+⊤pe="ype_sc">+⊤pe="ype_scope:x_'→'_x"><>
+⊤pe="yppe="var">y ⇒ arisrib/8.4pl5/ d" type="variable">s+⊤pe="ype_scope:x_'→'_x">an class="idi.fr/distruation">+⊤pe="ype_scope:x_on+⊤>+⊤trib/8.4pl5/stdlib/Coq.pan> :
&nbhtmr">k ruation">+⊤pe="ype_sc">Just"AdomLib.html#::x_'+⊤'">
&nbjoi>span class="ttf8_core.html#:type_scpan>
= : k"id" type="variable">s+⊤pe="ype_scope:x_'→'_x"><>+⊤pe="yppe="var">y ⇒ arisrib/8.4pl5/x">+⊤<"id" type="notation">→Ief="Ador">k (+⊤>+⊤{ef="AdomLib.html#type="vaa class="idref" href="AdomLilebclan>: k <= c>A:
&nbhtmr">k/ href="AdomLib.ht/span>/span>/span>;f="AdomLib.html#type="vaa class="idref" href="AdomLitspl#C"><="keyword">withA
an cl_="id" tation">+⊤>+⊤/span>;f="AdomLib.html#type="vaa class="idref" href="AdomLijoi>clan>: span class="<= c>Aclan>:
&nbjoi>span class="C<"AdomLib.html#type="va_scope:x_oiabWPFun2.pl.joi>clan>:
pl.joi>span class="ttf8_core.html#:type_scpan> DefinitPLym8_corspan>ation">+⊤>+⊤/span>;f="AdomLib.html#type="vaa class="idref" href="AdomLiwide>clan>: span class="<= c>Aclan>:
&nbjoi>span class="C<"AdomLib.html#type="va_scope:x_oiabWPFun2.pl.wide>clan>:
pl.wide>span class="ttf8_core.html#:type_scpan> DefinitPLym8_corspan>ation">+⊤>+⊤|}x">+⊤<"id" type="notation">→Ief="Ador">k: B"AdomLib.html#type="vaa class="idref" href="AdomLigaan _spl#C"><="keyword">with+⊤pe="ype_sc">JustWPFun2.'f" href="AdomLib.html#typan>
&nbttrib/8.4pl5 C<"AdomLib.html#type="va_scope:x_oiabT.el'f" href="AdomLib.html#typaximLf"T.s+⊤pe="ype_scope:x_'→'_x">an class="idi.fr/distruation">+⊤pe="ype_scope:x_on
:tation">+⊤>+⊤+⊤pe="yppe="var">y+⊤ pan c#:type_scope:x_'→'_x">+⊤ +⊤pe="ype">+⊤pe="ype_scope:x_'→'_x">an clas'∀">+⊤ an cled" tyors="idref" href="http://n>an clas'∀">+⊤ s s sk ">∀ sJust"AdomLib.html#::x_'+⊤'">x">+⊤<"id" type="notation">→Lean r">kpan c#:type_scope:x_'→'_x">k+⊤>+⊤<"AdomLib.html#type="vaa class="idref" href="AdomLiγf" href="AdomLib.html#typan>
&nbγspan class="ruation">+⊤pe="ype_sc">Just"AdomLib.html#::x_'+⊤'">=+⊤pe="ype_scope:x_'→'_x">an class="idi.fr/distruation">+⊤pe="ype_scope:x_on+⊤>+⊤trib/8.4pl5/stdlib/Coq.a class="idref" href="AdomLiγf" href="AdomLib.html#typan>
&nbγspan class="ruation">+⊤pe="ype_sc">Justvf" href="AdomLib.html#typs="id" typv="id" type="C<"AdomLib.html#type="va_scope:x_oiabbclan>:
k ruation">+⊤pe="ype_scs="id" type="pf" href="AdomLib.html#typs="id" typpym8_coretis"id" type="variable">s+⊤pe="ype_scope:x_'→'_x">an class="idi.fr/distruation">+⊤pe="ype_scope:x_on+⊤>+⊤trib/8.4pl5/stdlib/Coq.">+⊤pe="ype_scope:x_'→'_x">an class="idi.fr/distruation">+⊤pe="ype_scope:x_ostrib/8.4pl5/stdlib/Coq.Unicode.Utf">+⊤pe="ype_scope:x_'→'_x">an clas'∀">+⊤ an clqd" tyors="idref" href="http://n>an clas'∀">+⊤ BAan class="i k ruation">+⊤pe="ype_scs="id" type="pf" href="AdomLib.html#typs="id" typpym8_coretisid" type="variable">s+⊤pe="ype_scope:x_'→'_x">an class="idi.fr/distruation">+⊤pe="ype_scope:x_on∀ = BA<>k ruation">+⊤pe="ype_scs="id" type="#type="variable">Bs+⊤pe="ype_scope:x_'→'_x">an class="idi.fr/distruation">+⊤pe="ype_scope:x_o)r">k ruation">+⊤pe="ype_sc">+⊤pe="ype_scope:x_'→'_x">an class="idi.fr/distruation">+⊤pe="ype_scope:x_on+⊤>+⊤<"AdomLib.html#type="vaa class="idref" href="AdomLiγf" href="AdomLib.html#typan>
&nbγspan class="C<"AdomLib.html#type="va_scope:x_oiabWPFun2.se'f" href="AdomLib.html#typan>
&nbsetr">k ruation">+⊤pe="ype_sc">Just"AdomLib.html#::x_'+⊤'">+⊤pe="ype_sc">Justvf" href="AdomLib.html#typs="id" typv="id" type="id" type="variable">s:
kx">+⊤<"id" type="notation">→Lean r">kpan c#:type_scope:x_'→'_x">k+⊤>+⊤<"AdomLib.html#type="vaa class="idref" href="AdomLiγf" href="AdomLib.html#typan>
&nbγspan class="ruation">+⊤pe="ype_sc">Just"AdomLib.html#::x_'+⊤'">=+⊤pe="ype_scope:x_'→'_x">an class="idi.fr/distruation">+⊤pe="ype_scope:x_on+⊤>+⊤trib/8.4pl5/stdlib/=+⊤pe="ype_scope:x_'→'_x">an class="idi.fr/distruation">+⊤pe="ype_scope:x_ostrib/8.4pl5/stdlib/Coq.Unicode.Utf">+⊤pe="ype_scope:x_'→'_x">an clas'∀">+⊤
an clqd" tyors="idref" href="http://n>an clas'∀">+⊤ BAan class="i k ruation">+⊤pe="ype_scs="id" type="pf" href="AdomLib.html#typs="id" typpym8_coretisid" type="variable">s+⊤pe="ype_scope:x_'→'_x">an class="idi.fr/distruation">+⊤pe="ype_scope:x_on∀ = BA<>k ruation">+⊤pe="ype_scs="id" type="#type="variable">Bs+⊤pe="ype_scope:x_'→'_x">an class="idi.fr/distruation">+⊤pe="ype_scope:x_o)r">k ruatioe="variable">s+⊤pe="ype_scope:x_'→'_x">an class="idi.fr/distruation">+⊤pe="ype_scope:x_on+⊤>+⊤<"AdomLib.html#type="vaa class="idref" href="AdomLiγf" href="AdomLib.html#typan>
&nbγspan class="C<"AdomLib.html#type="va_scope:x_oiabWPFun2.se'f" href="AdomLib.html#typan>
&nbsetr">k ruation">+⊤pe="ype_sc">Just"AdomLib.html#::x_'+⊤'">ef" href=""id" type="variable">s:
kx">+⊤<"id" type="notation">→Lean r">kB"AdomLib.html#type="vaa class="idref" href="AdomLiadmLf" href="AdomLib.html#typrecspan>admLtrib/8.4pl5.ruation">+⊤pe="ype_sc">JustWPFun2.'f" href="AdomLib.html#typan>
&nbttrib/8.4pl5 C<"AdomLib.html#type="va_scope:x_oiabT.el'f" href="AdomLib.html#typaximLf"T.s+⊤pe="ype_scope:x_'→'_x">an class="idi.fr/distruation">+⊤pe="ype_scope:x_on
ttf8_core.html#:type_scpan> +⊤<"id" type="notation">→Ief="Ador">k: B"AdomLib.html#type="vaToS→ngx_oiabToS→ngclan>: :tation">+⊤>+⊤C<"AdomLib.html#type="van+⊤pe="yppe="var">y+⊤ pan cs="id" tystruation">+⊤pe="ype">+⊤pe="ype_scope:x_'→'_x">+⊤ +⊤pe="ype_scope:x_oiabT.foldf" href="AdomLib.html#typaximLf"T.foldtrib/8.4pl5 C<"AdomLib.html#type="van+⊤pe="yppe="var">y+⊤ pan csr">kpan ck:type_scope:x_'→'_x">+⊤pe="yppe="var">y+⊤ +⊤pe="ype_scope:x_oiabsf" href="AdomLib.html#typs="id" typstrib/8.4pl5 d" type="variable">s+⊤pe="ype_scope:x_'→'_x">s+⊤pe="ype_scope:x_'→'_x">
&nbto_s→ng="id" type=tistruation">+⊤pe="ype_scope:x_oiabkf" href="AdomLib.html#typs="id" typktrib/8.4pl5 d" type="variable">s+⊤pe="ype_scope:x_'→'_x">s+⊤pe="ype_scope:x_'→'_x">
&nbto_s→ng="id" type=tistruation">+⊤pe="ype_scope:x_oiabvf" href="AdomLib.html#typs="id" typv="id" type="n>∀ +⊤pe="ype_scope:x_'→'_x"> ttf8_core.html#:type_scpan>
s+⊤pe="ype_scope:x_'→'_x">pan cs→ng="id" tx">End href=" <"AdomLib.html#type="va_scope:x_oiabWPFun2.el'> +⊤<"id" type="notation">→Opaque href=" <"AdomLib.html#type="va_scope:x_oiabWPFun2.ge'f" href="AdomLib.html#typan>
&nbgetr">k. >+⊤<"id" type="notation">→Opaque href=" <"AdomLib.html#type="va_scope:x_oiabWPFun2.se'f" href="AdomLib.html#typan>
&nbsetr">k. ation"<"id" type="notation">→End href=" <"AdomLib.html#type="va_scope:x_oiabWPFun2clan>:
+⊤pe="ype_scope:">e="docetisa<:x_vpa <:x_vpa <:bodysa<:_oia>