Module theories.lemmas

Require Import Coq.Lists.List.
Import ListNotations.

Require Import Cap.
Require Import CapSets.
Require Import CapGroups.
Require Import Notations.

Ltac unfold_classes := repeat unfold
  alias, unalias,
  blob, blob_combine, blob_combine_one,
  elemOf, elemOf_union, elemOf_list, elemOf_bot,
  READABLE, NONWRITABLE, WRITABLE, STABLE, ISO, TRN, REF, VAL, BOX, TAG in *.
Ltac finish := solve [subst; unfold_classes; tauto].
Hint Extern 4 (~(_ = _)) => discriminate.
Hint Extern 4 ((_ = _)) => symmetry.
Hint Extern 4 => unfold_classes.

Tactic Notation "destruct_ecap" constr(e) :=
  (destruct e as [[]| |]).
Tactic Notation "destruct_ecap" constr(e1) "," constr(e2) :=
  (destruct_ecap e1 ; destruct_ecap e2).
Tactic Notation "destruct_ecap" constr(e1) "," constr(e2) "," constr(e3) :=
  (destruct_ecap e1 ; destruct_ecap e2 ; destruct_ecap e3).

Tactic Notation "destruct'" constr(H) := destruct H.
Tactic Notation "destruct'" constr(H) "by" tactic(tac) :=
  (let h := fresh "H" in assert H as h by tac; destruct h).
Tactic Notation "destruct'" constr(H) "as" simple_intropattern(pat) "by" tactic(tac) :=
  (let h := fresh "H" in assert H as h by tac; destruct h as pat).

Tactic Notation "replace'" constr(e1) "with" constr(e2) "by" tactic(tac) :=
  replace e1 with e2 in * by (symmetry; tac).

Lemma lemma1 {A} : forall (x y: A), In x [y] -> x = y.
Hint Resolve lemma1.

Lemma lemma2 {A} : forall (x: A) (xs: list A), In x (x::xs).
Hint Resolve lemma2.

Lemma lemma3 {A} : forall (x y: A) (xs: list A), In y xs -> In y (x::xs).
Hint Resolve lemma3.

Lemma lemma4 : forall λ λs κ,
  λ ∈ (λs ∘ κ) -> exists o λ0, λ0 ∈ λs /\ adapt o λ0 κ = Some λ.

Lemma lemma5: forall o λ0 λs κ λ1,
  λ0 ∈ λs -> adapt o λ0 κ = Some λ1 -> λ1 ∈ (λs ∘ κ).

Lemma lemma6: forall λ λ',
  subcap λ λ' -> subcap λ' λ -> λ = λ'.

Lemma lemma7: forall λ λ' λ'',
  subcap λ λ' -> subcap λ' λ'' -> subcap λ λ''.

Lemma lemma8: forall κ κ',
  unalias κ = unalias κ' -> κ = κ'.

Lemma lemma9: forall λs κ κ',
  λs ∈ (G κ) ->
  λs ∈ (G κ') ->
  κ = κ'.

Lemma lemma10: forall λ κ κ',
  adapt extract (unalias κ) κ' = Some λ ->
  unalias (alias λ) = λ.

Lemma lemma11: forall λ κ κ',
  adapt extract (unalias κ) κ' = None ->
  adapt read (unalias κ) κ' = Some λ ->
  unalias (alias λ) = λ.

Lemma lemma12: forall o λ0 λ0' κ λ1 λ1',
  subcap λ0 λ0' ->
  adapt o λ0 κ = Some λ1 ->
  adapt o λ0' κ = Some λ1' ->
  subcap λ1 λ1'.

Lemma lemma13: forall κ κ' λe λr,
  adapt extract (unalias κ) κ' = Some λe ->
  adapt read (unalias κ) κ' = Some λr ->
  subcap λe λr.

Lemma lemma14: forall λ κ λe,
  adapt extract λ κ = Some λe ->
  exists λr, adapt read λ κ = Some λr.

Lemma lemma15 : forall λs κ κ' λ,
  λs ∈ (G κ) ->
  adapt extract (unalias κ) κ' = Some λ ->
  (λs ∘ κ') ∈ (G (alias λ)).


Lemma lemma16 : forall λs κ κ' λ,
  λs ∈ (G κ) -> λ ∈ λs ->
  adapt extract (unalias κ) κ' = None ->
  adapt extract λ κ' = None.

Lemma lemma17 : forall λs κ κ' λ,
  λs ∈ (G κ) ->
  adapt extract (unalias κ) κ' = None ->
  adapt read (unalias κ) κ' = Some λ ->
  (λs ∘ κ') ∈ (G (alias λ)).

Lemma lemma18 : forall λs κ,
  (λs ∈ (G iso ∪ G trn ∪ G val)) ->
  (λs ∘ κ ∈ (G iso ∪ G trn ∪ G val) \/ κ = tag).

Lemma lemma19 : forall λs κs κ,
  λs ∘ (κs++[κ]) = λs ∘ κs ∘ κ.

Lemma lemma20: [C ref] ∈ (G ref).
Hint Resolve lemma20.

Lemma lemma21 {A}: forall (xs: list A),
  (forall x, x ∈ xs -> False) -> xs = [].

Lemma lemma22: forall (λs: capset) (κ: cap),
  λs ∈ TAG -> (λs ∘ κ) ∈ BOT.

Lemma lemma23: forall (λs: capset) (κ: cap),
  λs ∈ BOT -> (λs ∘ κ) ∈ BOT.

Lemma lemma24: forall (λs: capset) (κ: cap),
  λs ∈ READABLE -> exists κ', (λs ∘ κ) ∈ G(κ').

Lemma lemma25: forall λs (κ: cap),
  λs ∈ G κ -> λs ∈ STABLE.
Hint Resolve lemma25.

Lemma lemma26: forall λs (κ: cap),
  λs ∈ STABLE -> (λs ∘ κ) ∈ STABLE.
Hint Resolve lemma26.

Lemma lemma27: forall λs (κs: list cap),
  λs ∈ STABLE -> (λs ∘ κs) ∈ STABLE.
Hint Resolve lemma27.

Lemma lemma28: forall (λs: capset),
  λs ∈ READABLE -> λs ∘ tag ∈ TAG.

Lemma lemma29 : forall λs,
  λs ∈ STABLE -> λs ∘ tag ∈ TAG \/ λs ∘ tag ∈ BOT.

Lemma lemma30 : forall κ, [unalias κ] ∈ G κ.
Hint Resolve lemma30.

Lemma lemma31 : forall κ, [unalias κ] ∈ STABLE.
Hint Resolve lemma31.

Lemma lemma32 : [C ref] ∈ STABLE.
Hint Resolve lemma32.

Lemma lemma34 : forall (λs: capset) (κs: list cap),
  (λs ∈ (ISO ∪ TRN ∪ VAL)) ->
  λs ∘ κs ∈ (ISO ∪ TRN ∪ VAL)
  \/ (λs ∘ κs ∈ TAG /\ [C ref] ∘ κs ∈ TAG)
  \/ ([C ref] ∘ κs ∈ BOT).

Lemma lemma35 : forall λs (κs: list cap),
  λs ∈ (ISO ∪ TRN ∪ VAL) ->
  λs ∘ κs ∈ TAG ->
  [C ref] ∘ κs ∈ TAG ∪ BOT.

Lemma lemma36 : forall (λs: capset) (κ: cap),
  λs ∈ G κ -> λs ∈ BOT -> False.

Lemma lemma37 : forall (λs: capset) (κ: cap) (κ': cap),
  λs ∈ STABLE -> λs ∘ κ ∈ G κ' -> λs ∈ READABLE.

Lemma lemma38 : forall (λs λs': capset) (κ1: cap) (κ κ': cap),
  λs ∈ G κ -> λs' ∈ G κ -> λs ∘ κ1 ∈ G κ' ->
  λs' ∘ κ1 ∈ G κ'.

Lemma lemma39 (P: capset -> Prop):
  (forall λs, P λs) -> (forall λs (κ: cap), P λs -> P (λs ∘ κ)) -> forall λs κs, P (λs ∘ κs).

Lemma lemma40 : forall (λs: capset), λs ∈ READABLE -> exists κ, λs ∈ G κ.

Lemma lemma41 : forall (κ κ': cap) (λs λs': capset) (κs: list cap),
  λs ∈ G κ ->
  λs' ∈ G κ ->
  λs ∘ κs ∈ G κ' ->
  λs' ∘ κs ∈ G κ'.

Lemma lemma42 : forall λs (κs: list cap),
  λs ∈ WRITABLE ->
  λs ∘ κs ∈ TAG ->
  [C ref] ∘ κs ∈ TAG ∪ BOT.

Lemma lemma43 : forall (κ κ': cap),
  compatible (C κ) (C κ') ->
  compatible (unalias κ) (unalias κ').

Lemma lemma44 : forall (λ λ' λ'': ecap),
  compatible λ λ' ->
  subcap λ' λ'' ->
  compatible λ λ''.

Lemma lemma45 : forall (λ1 λ2: ecap),
  compatible λ1 λ2 ->
  compatible λ2 λ1.

Lemma lemma46 : forall (λ1 λ1' λ2 λ2': ecap),
  compatible λ1 λ2 ->
  subcap λ1 λ1' ->
  subcap λ2 λ2' ->
  compatible λ1' λ2'.

Lemma lemma47 : forall (κ κ': cap),
  compatible (unalias κ) (unalias κ') ->
  compatible (C κ) (C κ').

Lemma lemma48 : forall (λs λs': capset) (κ κ': cap),
  λs ∈ G κ ->
  λs' ∈ G κ' ->
  compatible (C κ) (C κ') ->
  compatible_set λs λs'.

Lemma lemma49 : forall (λs λs': capset) (κ κ': cap),
  λs ∈ G κ ->
  λs' ∈ G κ' ->
  compatible_set λs λs' ->
  compatible (C κ) (C κ').

Lemma lemma50 : forall (λs: capset),
  λs ∈ STABLE -> λs ∈ BOT \/ exists κ, λs ∈ G κ.

Lemma lemma52 : forall (λs λs': capset),
  λs ∈ BOT -> compatible_set λs λs'.

Lemma lemma54 : forall (λs: capset) (λ: ecap),
  λs ∈ TAG -> λ ∈ λs -> λ = C tag.

Lemma lemma55 : forall (λs λs': capset),
  λs ∈ TAG -> compatible_set λs λs'.

Lemma lemma56 : forall o λ λ' κ,
  adapt o λ κ = None ->
  subcap λ λ' ->
  adapt o λ' κ = None.

Lemma lemma57 : forall (λs: capset) (κ: cap),
  λs ∈ G κ ->
  unalias κ :: λs ∈ G κ.

Lemma lemma58 : forall λs κ κ',
  (unalias κ :: λs) ∈ (G κ) ->
  adapt extract (unalias κ) κ' = None ->
  adapt read (unalias κ) κ' = None ->
  (unalias κ :: λs) ∘ κ' ∈ BOT.

Lemma lemma59 : forall (λs: capset) (κ: cap) (λ: ecap) (λ1: ecap),
  λ1 ∈ λs ∘ κ ->
  λ1 ∈ (λ :: λs) ∘ κ.

Lemma lemma60 : forall (λs: capset) (κ: cap) (λ: ecap),
  (λ :: λs) ∘ κ ∈ BOT ->
  λs ∘ κ ∈ BOT.

Lemma lemma61 : forall (λs: capset) (κ κ': cap),
  λs ∈ (G κ) ->
  adapt extract (unalias κ) κ' = None ->
  adapt read (unalias κ) κ' = None ->
  λs ∘ κ' ∈ BOT.

Inductive group_adapt : cap -> cap -> cap -> Prop :=
| group_adapt_iso_iso : group_adapt iso iso iso
| group_adapt_iso_trn : group_adapt iso trn iso
| group_adapt_iso_ref : group_adapt iso ref iso
| group_adapt_iso_val : group_adapt iso val val
| group_adapt_iso_box : group_adapt iso box val
| group_adapt_iso_tag : group_adapt iso tag tag

| group_adapt_trn_iso : group_adapt trn iso iso
| group_adapt_trn_trn : group_adapt trn trn trn
| group_adapt_trn_ref : group_adapt trn ref trn
| group_adapt_trn_val : group_adapt trn val val
| group_adapt_trn_box : group_adapt trn box val
| group_adapt_trn_tag : group_adapt trn tag tag

| group_adapt_ref_iso : group_adapt ref iso iso
| group_adapt_ref_trn : group_adapt ref trn trn
| group_adapt_ref_ref : group_adapt ref ref ref
| group_adapt_ref_val : group_adapt ref val val
| group_adapt_ref_box : group_adapt ref box box
| group_adapt_ref_tag : group_adapt ref tag tag

| group_adapt_val_iso : group_adapt val iso val
| group_adapt_val_trn : group_adapt val trn val
| group_adapt_val_ref : group_adapt val ref val
| group_adapt_val_val : group_adapt val val val
| group_adapt_val_box : group_adapt val box val
| group_adapt_val_tag : group_adapt val tag tag

| group_adapt_box_iso : group_adapt box iso tag
| group_adapt_box_trn : group_adapt box trn box
| group_adapt_box_ref : group_adapt box ref box
| group_adapt_box_val : group_adapt box val val
| group_adapt_box_box : group_adapt box box box
| group_adapt_box_tag : group_adapt box tag tag
.
Hint Constructors group_adapt.

Lemma lemma62 : forall (λs: capset) (κ κ' κ'': cap),
  λs ∈ G κ ->
  λs ∘ κ' ∈ G κ'' <-> group_adapt κ κ' κ''.

Lemma lemma62a : forall (λs: capset) (κ κ' κ'': cap),
  λs ∈ G κ ->
  λs ∘ κ' ∈ G κ'' -> group_adapt κ κ' κ''.

Ltac destruct_group_adapt κ κ' κ'' :=
  let H := fresh "H" in
  eassert (group_adapt κ κ' κ'') as H; [apply -> lemma62 | inversion H].

Lemma lemma63 : forall (κ: cap),
  [C ref] ∘ κ ∈ ISO -> κ = iso.

Lemma lemma64 (κ: cap) : forall (λs λs': capset),
  λs ∈ STABLE ->
  λs' ∈ G κ ->
  compatible_set λs λs' ->
  match κ with
  | iso => λs ∈ TAG ∪ BOT
  | trn => λs ∈ BOX ∪ TAG ∪ BOT
  | ref => λs ∈ REF ∪ BOX ∪ TAG ∪ BOT
  | val => λs ∈ VAL ∪ BOX ∪ TAG ∪ BOT
  | box => λs ∈ TRN ∪ REF ∪ VAL ∪ BOX ∪ TAG ∪ BOT
  | tag => λs ∈ ISO ∪ TRN ∪ REF ∪ VAL ∪ BOX ∪ TAG ∪ BOT
  end.

Lemma lemma66 : forall (λs: capset),
  λs ∈ WRITABLE -> λs ∈ STABLE.
Hint Resolve lemma66.

Lemma lemma67 : forall λs (κs: list cap),
  λs ∈ (ISO ∪ TRN ∪ VAL) ->
  λs ∘ κs ∈ BOT ->
  [C ref] ∘ κs ∈ BOT.

Lemma lemma68 : forall λs (κs: list cap),
  λs ∈ WRITABLE ->
  λs ∘ κs ∈ BOT ->
  [C ref] ∘ κs ∈ BOT.

Lemma lemma69 : forall λs (κs: list cap),
  λs ∈ (ISO ∪ TRN ∪ VAL) ->
  λs ∘ κs ∈ BOX ->
  [C ref] ∘ κs ∈ BOT.

Lemma lemma70 : forall λs (κs: list cap),
  λs ∈ WRITABLE ->
  λs ∘ κs ∈ BOX ->
  [C ref] ∘ κs ∈ BOX ∪ BOT.

Lemma lemma71 : forall λs (κs: list cap),
  λs ∈ WRITABLE ->
  λs ∘ κs ∈ BOX ∪ TAG ∪ BOT ->
  [C ref] ∘ κs ∈ BOX ∪ TAG ∪ BOT.

Lemma lemma72 : forall λs (κs: list cap),
  λs ∈ WRITABLE ->
  λs ∘ κs ∈ TAG ∪ BOT ->
  [C ref] ∘ κs ∈ TAG ∪ BOT.

Lemma lemma73 : forall (λs1 λs2: capset),
  compatible_set λs1 λs2 ->
  compatible_set λs2 λs1.

Lemma lemma74 : forall (λs1 λs2: capset) (κ: cap),
  λs1 ∈ STABLE -> λs2 ∈ STABLE ->
  λs1 ∘ κ ∈ ISO ->
  λs2 ∘ κ ∈ TRN ∪ REF ->
  λs1 ∈ ISO /\ λs2 ∈ TRN ∪ REF.

Lemma lemma75 : forall (λs1 λs2: capset) (κs: list cap),
  λs1 ∈ STABLE -> λs2 ∈ STABLE ->
  λs1 ∘ κs ∈ ISO ->
  λs2 ∘ κs ∈ TRN ∪ REF ->
  λs1 ∈ ISO /\ λs2 ∈ TRN ∪ REF.

Lemma lemma76 : forall (λs: capset) (κ: cap),
  λs ∈ STABLE ->
  λs ∘ κ ∈ ISO ->
  λs ∈ ISO \/ κ = iso.

Lemma lemma77 : forall (κ κ': cap),
  [unalias κ] ∈ G κ' -> κ = κ'.

Lemma lemma78 : forall (λs: capset) (κ0 κ1 κ2: cap),
  λs ∈ G κ0 ->
  λs ∘ κ1 ∈ G κ2 ->
  adapt extract (unalias κ0) κ1 = Some (unalias κ2) \/
  adapt extract (unalias κ0) κ1 = None /\ adapt read (unalias κ0) κ1 = Some (unalias κ2).

Lemma lemma79: forall o λ0 λ0' κ λ1',
  subcap λ0 λ0' ->
  adapt o λ0' κ = Some λ1' ->
  exists λ1, adapt o λ0 κ = Some λ1 /\ subcap λ1 λ1'.

Lemma lemma81 : forall (κ: cap), alias (unalias κ) = κ.

Lemma lemma82 : forall (κ κ': cap) λ,
  adapt extract (unalias κ) κ' = Some λ ->
  exists κ'', λ = unalias κ''.

Lemma lemma83 : forall (κ κ': cap) λ,
  adapt extract (unalias κ) κ' = None ->
  adapt read (unalias κ) κ' = Some λ ->
  exists κ'', λ = unalias κ''.

Lemma lemma84 : forall (λs λs': capset) (κ0 κ0' κ1' κ: cap),
  λs ∈ G κ0 ->
  λs' ∈ G κ0' ->
  λs' ∘ κ ∈ G κ1' ->
  subcap (unalias κ0) (unalias κ0') ->
  exists κ1, λs ∘ κ ∈ G κ1 /\ subcap (unalias κ1) (unalias κ1').

Lemma lemma85 : forall (λs λs': capset) (κ0 κ0' κ1': cap) (κs: list cap),
  λs ∈ G κ0 ->
  λs' ∈ G κ0' ->
  λs' ∘ κs ∈ G κ1' ->
  subcap (unalias κ0) (unalias κ0') ->
  exists κ1, λs ∘ κs ∈ G κ1 /\ subcap (unalias κ1) (unalias κ1').

Lemma lemma86 : forall (λs: capset) (κs: list cap),
  λs ∈ WRITABLE ->
  [C ref] ∘ κs ∈ ISO ->
  λs ∘ κs ∈ ISO.

Lemma lemma87 : forall (λs: capset) (κ: cap),
  λs ∈ STABLE ->
  λs ∘ κ ∈ REF ->
  λs ∈ REF /\ κ = ref.

Lemma lemma89 {A} : forall (xs: list A) (x y: A),
  In x (xs ++ [y]) -> In x xs \/ x = y.
Hint Resolve lemma89.

Lemma lemma88 {A} : forall (xs: list A) (x y: A),
  In x xs -> In x (xs ++ [y]).
Hint Resolve lemma88.

Lemma lemma90 {A} : forall (xs: list A) (x: A),
  In x (xs ++ [x]).
Hint Resolve lemma90.

Lemma lemma91 : forall (λs: capset) (κs: list cap),
  λs ∈ STABLE ->
  λs ∘ κs ∈ REF ->
  λs ∈ REF /\ (forall κ, κ ∈ κs -> κ = ref).

Lemma lemma92 : forall (λs: capset) (κs: list cap),
  λs ∈ REF ->
  (forall κ, κ ∈ κs -> κ = ref) ->
  λs ∘ κs ∈ REF.

Lemma lemma94 : forall (λs: capset) (κs: list cap),
  λs ∈ STABLE ->
  λs ∘ κs ∈ REF ->
  λs ∈ REF /\ (forall κ, κ ∈ κs -> κ = ref).

Lemma lemma99: forall λs κ κ',
  λs ∈ G κ ->
  match κ, κ' with
  | iso, iso => λs ∘ κ' ∈ ISO
  | iso, trn => λs ∘ κ' ∈ ISO
  | iso, ref => λs ∘ κ' ∈ ISO
  | iso, val => λs ∘ κ' ∈ VAL
  | iso, box => λs ∘ κ' ∈ VAL
  | iso, tag => λs ∘ κ' ∈ TAG

  | trn, iso => λs ∘ κ' ∈ ISO
  | trn, trn => λs ∘ κ' ∈ TRN
  | trn, ref => λs ∘ κ' ∈ TRN
  | trn, val => λs ∘ κ' ∈ VAL
  | trn, box => λs ∘ κ' ∈ VAL
  | trn, tag => λs ∘ κ' ∈ TAG

  | ref, iso => λs ∘ κ' ∈ ISO
  | ref, trn => λs ∘ κ' ∈ TRN
  | ref, ref => λs ∘ κ' ∈ REF
  | ref, val => λs ∘ κ' ∈ VAL
  | ref, box => λs ∘ κ' ∈ BOX
  | ref, tag => λs ∘ κ' ∈ TAG

  | val, iso => λs ∘ κ' ∈ VAL
  | val, trn => λs ∘ κ' ∈ VAL
  | val, ref => λs ∘ κ' ∈ VAL
  | val, val => λs ∘ κ' ∈ VAL
  | val, box => λs ∘ κ' ∈ VAL
  | val, tag => λs ∘ κ' ∈ TAG

  | box, iso => λs ∘ κ' ∈ TAG
  | box, trn => λs ∘ κ' ∈ BOX
  | box, ref => λs ∘ κ' ∈ BOX
  | box, val => λs ∘ κ' ∈ VAL
  | box, box => λs ∘ κ' ∈ BOX
  | box, tag => λs ∘ κ' ∈ TAG
  | tag, _ => λs ∘ κ' ∈ BOT
  end.

Lemma lemma101 (A: Type): forall (P: A -> Prop) (x: A) (xs: list A),
  (forall y, In y (xs++[x]) -> P y) ->
  (forall y, In y xs -> P y).

Lemma lemma102 (A: Type): forall (P: A -> Prop) (x: A) (xs: list A),
  (forall y, In y (xs++[x]) -> P y) ->
  P x.

Lemma lemma104: forall λs, λs ∘ [] = λs.

Lemma lemma105: forall λs κ κ',
  λs ∈ G κ -> λs ∈ G κ' -> κ <> κ' -> False.

Lemma lemma100: forall λs (κ: cap),
  λs ∈ REF ∪ BOX ∪ TAG ∪ BOT ->
  (κ = ref \/ κ = box \/ κ = tag) ->
  λs ∘ κ ∈ REF ∪ BOX ∪ TAG ∪ BOT.

Lemma lemma103: forall λs (κs: list cap),
  λs ∈ REF ∪ BOX ∪ TAG ∪ BOT ->
  (forall κ, κ ∈ κs -> κ = ref) ->
  λs ∘ κs ∈ REF ∪ BOX ∪ TAG ∪ BOT.

Lemma lemma107: forall λs (κ: cap),
  λs ∈ STABLE ->
  λs ∘ κ ∈ BOT ->
  λs ∈ BOT ∪ TAG.

Lemma lemma109: forall λs,
  λs ∈ STABLE ->
  λs ∘ tag ∈ TAG ∪ BOT.

Lemma lemma114 : forall λs,
  λs ∈ STABLE ->
  compatible_set λs [C iso] ->
  λs ∈ TAG ∪ BOT.

Lemma lemma115 : forall λs,
  λs ∈ STABLE ->
  compatible_set λs [C trn] ->
  λs ∈ BOX ∪ TAG ∪ BOT.

Lemma lemma117: forall (λs: capset) (κ: cap),
  λs ∈ ISO ∪ TRN ∪ VAL ->
  (λs ∘ κ) ∈ TAG ->
  κ = tag.

Lemma lemma119: forall (λs: capset) (κ: cap),
  λs ∈ ISO ∪ TRN ∪ VAL ->
  (λs ∘ κ) ∈ TAG ->
  ([C ref] ∘ κ) ∈ TAG.

Lemma lemma121: forall (λs: capset) (κ: cap),
  λs ∈ ISO ∪ TRN ∪ VAL ->
  (λs ∘ κ) ∈ ISO ∪ TRN ∪ VAL \/ κ = tag.

Lemma lemma122: forall λs (κ: cap),
  λs ∈ TAG ∪ BOT ->
  λs ∘ κ ∈ BOT.

Lemma lemma123: forall (λs: capset) (κs: list cap),
  λs ∈ ISO ∪ TRN ∪ VAL ->
  (λs ∘ κs) ∈ ISO ∪ TRN ∪ VAL \/ ([C ref] ∘ κs) ∈ TAG ∪ BOT.

Lemma lemma124: forall (λs: capset) (κs: list cap),
  λs ∈ ISO ∪ TRN ∪ VAL ->
  (λs ∘ κs) ∈ TAG ∪ BOT ->
  ([C ref] ∘ κs) ∈ TAG ∪ BOT.

Lemma lemma125: forall (λs λs': capset) (κ: cap) (κs: list cap),
  λs ∈ G κ ->
  λs' ∈ G κ ->
  λs ∘ κs ∈ BOT ->
  λs' ∘ κs ∈ BOT.

Lemma lemma130: forall (λs: capset) (κs: list cap),
  λs ∈ WRITABLE ->
  (λs ∘ κs) ∈ TAG ∪ BOT ->
  ([C ref] ∘ κs) ∈ TAG ∪ BOT.

Lemma lemma133: forall (λs: capset) (κs: list cap),
  λs ∈ WRITABLE ->
  (λs ∘ κs) ∈ REF ∪ BOX ∪ TAG ∪ BOT ->
  ([C ref] ∘ κs) ∈ REF ∪ BOX ∪ TAG ∪ BOT.

Lemma lemma134: forall (λs1 λs2: capset),
  λs1 ∈ REF ∪ BOX ∪ TAG ∪ BOT ->
  λs2 ∈ REF ∪ BOX ∪ TAG ∪ BOT ->
  compatible_set λs1 λs2.

Lemma lemma135 : forall (λs: capset) (λ: ecap),
  λs ∈ STABLE ->
  safe_to_write λ ref ->
  compatible_set λs ([C (alias λ)]) ->
  λs ∈ REF ∪ BOX ∪ TAG ∪ BOT.

Lemma lemma150 : forall (κ: cap) (κs: list cap),
  [unalias κ] ∘ κs ∈ VAL ->
  (κ = val \/ κ = box) \/ (val ∈ κs \/ box ∈ κs).

Lemma lemma151 : forall (κ κ': cap),
  κ = val \/ κ = box ->
  subcap (C κ) (C κ') ->
  κ' = val \/ κ' = box \/ κ' = tag.

Lemma lemma152 : forall (λs: capset) (κ: cap),
  λs ∈ NONWRITABLE ->
  λs ∘ κ ∈ NONWRITABLE.

Lemma lemma153 : forall (λs: capset) (κs: list cap),
  λs ∈ NONWRITABLE ->
  λs ∘ κs ∈ NONWRITABLE.

Lemma lemma154 : forall (λs: capset) (κ: cap),
  λs ∈ STABLE ->
  κ = val \/ κ = box \/ κ = tag ->
  λs ∘ κ ∈ NONWRITABLE.

Lemma lemma155 : forall (λs: capset) (κ: cap) (κs: list cap),
  λs ∈ STABLE ->
  κ = val \/ κ = box \/ κ = tag ->
  λs ∘ κ ∘ κs ∈ NONWRITABLE.

Lemma lemma156: forall (λs: capset) (κ: cap),
  λs ∈ STABLE ->
  λs ∘ κ ∈ BOT ->
  λs ∈ TAG ∪ BOT.

Lemma lemma160 : forall (λs: capset) (κ: cap),
  λs ∈ STABLE ->
  λs ∘ κ ∈ NONWRITABLE ->
  λs ∈ NONWRITABLE \/ (κ = val \/ κ = box \/ κ = tag).

Lemma lemma161 : forall (λs: capset),
  λs ∈ WRITABLE ->
  λs ∈ NONWRITABLE ->
  False.

Lemma lemma162 : forall (λs: capset) (κs: list cap),
  λs ∈ WRITABLE ->
  λs ∘ κs ∈ NONWRITABLE ->
  [C ref] ∘ κs ∈ NONWRITABLE.

Lemma lemma163 : forall (λs1 λs2: capset),
  λs1 ∈ NONWRITABLE ->
  λs2 ∈ NONWRITABLE ->
  compatible_set λs1 λs2.

Lemma lemma164 : forall λs (κs: list cap) (κ: cap),
  λs ∘ (κ::κs) = λs ∘ κ ∘ κs.

Lemma lemma165 : forall (λs: capset) (κs: list cap),
  λs ∈ STABLE ->
  val ∈ κs \/ box ∈ κs ->
  λs ∘ κs ∈ NONWRITABLE.

Lemma lemma177 {A} : forall (x: A) (y: A),
  x <> y -> not (x ∈ [y]).
Hint Resolve lemma177.

Lemma lemma178 {A} : forall (x: A) (xs ys: list A),
  not (x ∈ xs) ->
  not (x ∈ ys) ->
  not (x ∈ xs ++ ys).
Hint Resolve lemma178.

Lemma lemma179 {A} : forall (x y: A) (xs: list A),
  not (y ∈ xs) ->
  x <> y ->
  not (y ∈ xs ++ [x]).
Hint Resolve lemma179.

Lemma lemma180 : forall (κ: cap) (κs: list cap),
  [unalias κ] ∘ κs ∈ BOX ->
  κ = box \/ box ∈ κs.

Lemma lemma181 : forall (κ: cap) (κs: list cap),
  [unalias κ] ∘ κs ∈ REF ∪ BOX ->
  κ <> val /\ not (val ∈ κs).

Lemma lemma182 : forall (λs: capset) (κ: cap),
  λs ∈ BOX ∪ TAG ∪ BOT ->
  κ <> val ->
  λs ∘ κ ∈ BOX ∪ TAG ∪ BOT.

Lemma lemma183 {A} : forall (x y: A) (xs: list A),
  not (y ∈ xs ++ [x]) ->
  x <> y.
Hint Resolve lemma183.

Lemma lemma184 : forall (λs: capset) (κs: list cap),
  λs ∈ BOX ∪ TAG ∪ BOT ->
  not (val ∈ κs) ->
  λs ∘ κs ∈ BOX ∪ TAG ∪ BOT.

Lemma lemma185 : forall (λs: capset) (κ: cap),
  λs ∈ REF ∪ BOX ∪ TAG ∪ BOT ->
  κ = box \/ κ = tag ->
  λs ∘ κ ∈ BOX ∪ TAG ∪ BOT.

Lemma lemma186 : forall (λs1 λs2: capset),
  λs1 ∈ BOX ∪ TAG ∪ BOT ->
  λs2 ∈ TRN ∪ REF ∪ VAL ∪ BOX ∪ TAG ∪ BOT ->
  compatible_set λs1 λs2.

Lemma lemma188 : forall (λs: capset) (λ: ecap),
  λs ∈ STABLE ->
  safe_to_write λ box ->
  compatible_set λs ([C (alias λ)]) ->
  λs ∈ REF ∪ BOX ∪ TAG ∪ BOT.

Lemma lemma189 : forall (λs: capset) (κ: cap),
  λs ∈ STABLE ->
  λs ∘ κ ∈ BOX ->
  (λs ∈ BOX /\ (κ = trn \/ κ = ref \/ κ = box)) \/
  (λs ∈ REF /\ (κ = box)).

Lemma lemma187 {A} : forall (P: A -> Prop),
  forall x, x ∈ [] -> P x.

Lemma lemma191 {A} : forall (P: A -> Prop) (xs ys: list A),
  (forall x, x ∈ xs -> P x) ->
  (forall x, x ∈ ys -> P x) ->
  (forall x, x ∈ xs ++ ys -> P x).

Lemma lemma192 {A} : forall (P: A -> Prop) (x: A),
  P x -> (forall y, y ∈ [x] -> P y).

Lemma lemma200 : forall (λs: capset) (κs: list cap),
  λs ∈ STABLE ->
  λs ∘ κs ∈ BOX ->
  (λs ∈ BOX /\ forall κ, κ ∈ κs -> κ = trn \/ κ = ref \/ κ = box) \/
  exists κs' κs'', (κs = κs' ++ [box] ++ κs'' /\ λs ∘ κs' ∈ REF /\ forall κ, κ ∈ κs'' -> κ = trn \/ κ = ref \/ κ = box).

Lemma lemma201 : forall (λs: capset) (κ: cap),
  λs ∈ BOX ∪ TAG ∪ BOT ->
  κ = trn \/ κ = ref \/ κ = box ->
  λs ∘ κ ∈ BOX ∪ TAG ∪ BOT.

Lemma lemma202 : forall (λs: capset) (κs: list cap),
  λs ∈ BOX ∪ TAG ∪ BOT ->
  (forall κ, κ ∈ κs -> κ = trn \/ κ = ref \/ κ = box) ->
  λs ∘ κs ∈ BOX ∪ TAG ∪ BOT.

Lemma lemma203 : forall λs κs κs',
  λs ∘ (κs++κs') = λs ∘ κs ∘ κs'.

Lemma lemma204 : forall (λs: capset) (κs κs': list cap),
  λs ∘ κs ∈ REF ∪ BOX ∪ TAG ∪ BOT ->
  (forall κ, κ ∈ κs' -> κ = trn \/ κ = ref \/ κ = box) ->
  λs ∘ (κs ++ [box] ++ κs') ∈ BOX ∪ TAG ∪ BOT.

Lemma lemma205 : [C ref] ∈ WRITABLE.
Hint Resolve lemma205.

Lemma lemma206 : forall (λs: capset) (κs: list cap),
  λs ∈ WRITABLE ->
  λs ∘ κs ∈ TRN ∪ REF ∪ VAL ∪ BOX ∪ TAG ∪ BOT ->
  [C ref] ∘ κs ∈ TRN ∪ REF ∪ VAL ∪ BOX ∪ TAG ∪ BOT.


Lemma lemmaB1 : forall (λs: capset) (κs1 κs3 κs4: list cap) (κ κ2: cap),
  λs ∈ WRITABLE ->
  compatible_set (λs ∘ κs4) ([unalias κ] ∘ κs3) ->
  [unalias κ] ∘ κs3 ∈ ISO ->
  compatible_set ([C ref] ∘ κs4) ([C ref] ∘ κs1 ∘ κ2 ∘ κs3).

Lemma lemmaB2 : forall (λs: capset) (λ: ecap) (κs1 κs3 κs4: list cap) (κ κ2: cap),
  λs ∈ WRITABLE ->
  subcap (unalias κ) (C κ2) ->
  safe_to_write λ κ ->
  compatible_set (λs ∘ κs4) ([unalias κ] ∘ κs3) ->
  compatible_set (λs ∘ κs1) ([C (alias λ)]) ->
  [unalias κ] ∘ κs3 ∈ TRN ->
  compatible_set ([C ref] ∘ κs4) ([C ref] ∘ κs1 ∘ κ2 ∘ κs3).

Lemma lemmaB3 : forall (λs: capset) (λ: ecap) (κs1 κs3 κs4: list cap) (κ κ2: cap),
  λs ∈ WRITABLE ->
  subcap (unalias κ) (C κ2) ->
  safe_to_write λ κ ->
  compatible_set (λs ∘ κs4) ([unalias κ] ∘ κs3) ->
  compatible_set (λs ∘ κs1) ([C (alias λ)]) ->
  [unalias κ] ∘ κs3 ∈ REF ->
  compatible_set ([C ref] ∘ κs4) ([C ref] ∘ κs1 ∘ κ2 ∘ κs3).

Lemma lemmaB4 : forall (λs: capset) (λ: ecap) (κs1 κs3 κs4: list cap) (κ κ2: cap),
  λs ∈ WRITABLE ->
  subcap (unalias κ) (C κ2) ->
  safe_to_write λ κ ->
  compatible_set (λs ∘ κs4) ([unalias κ] ∘ κs3) ->
  compatible_set (λs ∘ κs1) ([C (alias λ)]) ->
  [unalias κ] ∘ κs3 ∈ VAL ->
  compatible_set ([C ref] ∘ κs4) ([C ref] ∘ κs1 ∘ κ2 ∘ κs3).

Lemma lemmaB5 : forall (λs: capset) (λ: ecap) (κs1 κs3 κs4: list cap) (κ κ2: cap),
  λs ∈ WRITABLE ->
  subcap (unalias κ) (C κ2) ->
  safe_to_write λ κ ->
  compatible_set (λs ∘ κs4) ([unalias κ] ∘ κs3) ->
  compatible_set (λs ∘ κs1) ([C (alias λ)]) ->
  [unalias κ] ∘ κs3 ∈ BOX ->
  compatible_set ([C ref] ∘ κs4) ([C ref] ∘ κs1 ∘ κ2 ∘ κs3).

Lemma lemmaB : forall (λs: capset) (λ: ecap) (κs1 κs3 κs4: list cap) (κ κ2: cap),
  λs ∈ WRITABLE ->
  subcap (unalias κ) (C κ2) ->
  safe_to_write λ κ ->
  compatible_set (λs ∘ κs4) ([unalias κ] ∘ κs3) ->
  compatible_set (λs ∘ κs1) ([C (alias λ)]) ->
  compatible_set ([C ref] ∘ κs4) ([C ref] ∘ κs1 ∘ κ2 ∘ κs3).