Require Import Vbase Varith.
Require Import Relations Classical ClassicalDescription.
Require Import List Permutation Vlistbase Vlist extralib.
Require Import c11 fslassn fslmodel fslassnlemmas.
Require Import fslhmap step.
Set Implicit Arguments.
Definition hbpath := list hbcase.
Definition hbpath_wf (path: hbpath) :=
∀ path1 path2 edge1 edge2 (DECOMP: path = path1 ++ edge1 :: edge2 :: path2),
hb_snd edge1 = Some (hb_fst edge2).
Definition hbpath_valid lab sb rf hmap path :=
<< WFP: hbpath_wf path >> ∧
<< EVP: ∀ edge (IN: In edge path), edge_valid lab sb rf edge >> ∧
<< PVA: ∀ edge (IN: In edge path), hmap_valid lab sb rf hmap (hb_fst edge) >>.
Definition hbpath_connects lab sb rf hmap path a b :=
(a = b ∧ path = nil) ∨
hbpath_valid lab sb rf hmap path ∧
∃ fst lst, ohead path = some fst ∧ hb_fst fst = a ∧
olast path = some lst ∧ hb_snd lst = Some b.
Lemma hbpath_wf_one:
∀ edge, hbpath_wf (edge :: nil).
Lemma hbpath_wf_app:
∀ path1 path2, hbpath_wf (path1 ++ path2) → hbpath_wf path1 ∧ hbpath_wf path2.
Lemma hbpath_wf_cons:
∀ edge path, hbpath_wf (edge :: path) → hbpath_wf path.
Lemma hbpath_valid_nil:
∀ lab sb rf hmap, hbpath_valid lab sb rf hmap nil.
Lemma connects_implies_valid:
∀ lab sb rf hmap path a b, hbpath_connects lab sb rf hmap path a b → hbpath_valid lab sb rf hmap path.
Lemma hbpath_valid_app:
∀ lab sb rf hmap path1 path2, hbpath_valid lab sb rf hmap (path1 ++ path2) →
hbpath_valid lab sb rf hmap path1 ∧ hbpath_valid lab sb rf hmap path2.
Lemma hbpath_valid_cons:
∀ lab sb rf hmap edge path,
hbpath_valid lab sb rf hmap (edge :: path) → hbpath_valid lab sb rf hmap path.
Lemma hbpath_valid_cons_inv:
∀ lab sb rf hmap path (PV: hbpath_valid lab sb rf hmap path)
edge (EV: edge_valid lab sb rf edge) (VALIDa: hmap_valid lab sb rf hmap (hb_fst edge))
(VALIDb: ∀ b (SND: hb_snd edge = Some b), hmap_valid lab sb rf hmap b)
(CONNECT: ∀ edge´ (FST: ohead path = Some edge´), hb_snd edge = Some (hb_fst edge´)),
hbpath_valid lab sb rf hmap (edge :: path).
Lemma hbpath_connects_app1:
∀ lab sb rf hmap path1 path2 edge a b
(CONNECT: hbpath_connects lab sb rf hmap (path1 ++ edge :: path2) a b),
hbpath_connects lab sb rf hmap path1 a (hb_fst edge).
Lemma hbpath_connects_app2:
∀ lab sb rf hmap path1 path2 edge a b
(CONNECT: hbpath_connects lab sb rf hmap (path1 ++ edge :: path2) a b),
hbpath_connects lab sb rf hmap (edge :: path2) (hb_fst edge) b.
Lemma hbpath_connects_cons:
∀ lab sb rf hmap edge1 edge2 path a b
(CONNECT: hbpath_connects lab sb rf hmap (edge1 :: edge2 :: path) a b),
hbpath_connects lab sb rf hmap (edge2 :: path) (hb_fst edge2) b.
Lemma hbUrf_implies_hbpath:
∀ lab sb rf hmap V (VALID: hmap_valids lab sb rf hmap V) (HC: hist_closed sb rf V)
a b (HB: happens_before_union_rf sb rf a b) (IN: In b V),
∃ path, hbpath_connects lab sb rf hmap path a b.
Lemma hmap_defined_on_path:
∀ lab sb rf mo (CONS_RF: ConsistentRF_basic lab sb rf mo)
hmap path (PV: hbpath_valid lab sb rf hmap path)
edge (IN: In edge path),
∃ hf, hmap edge = Hdef hf.
Lemma nonatomic_loc_on_path:
∀ lab sb rf mo (CONS_RF: ConsistentRF_basic lab sb rf mo)
hmap path (PV: hbpath_valid lab sb rf hmap path)
l (ALL: ∀ edge (IN: In edge path) hf (MAP: hmap edge = Hdef hf), hf l ≠ HVnone)
(NAX: ∃ edge, << IN: In edge path >> ∧
<< NA: ∀ hf (MAP: hmap edge = Hdef hf), is_nonatomic (hf l) >>),
∀ edge (IN: In edge path) hf (MAP: hmap edge = Hdef hf), is_nonatomic (hf l).
Lemma sink_is_always_last :
∀ path (WF: hbpath_wf path) a (SIN: In (hb_sink a) path), olast path = Some (hb_sink a).
Lemma sink_is_always_last_alt:
∀ path edge (WF: hbpath_wf (path ++ edge :: nil)), ¬ ∃ edge´, In edge´ path ∧ is_sink edge´.
Lemma connects_implies_no_sink:
∀ lab sb rf hmap path a b,
hbpath_connects lab sb rf hmap path a b → ∀ e, ¬ In (hb_sink e) path.
Lemma connect_implies_hbUrf:
∀ lab sb rf hmap path a b (CONNECT: hbpath_connects lab sb rf hmap path a b),
clos_refl_trans _ (happens_before_union_rf sb rf) a b.
Lemma connect_implies_hbUrf_strong:
∀ lab sb rf hmap path a b (CONNECT: hbpath_connects lab sb rf hmap path a b),
path ≠ nil → happens_before_union_rf sb rf a b.
Lemma hb_trough_sb_path:
∀ lab sb rf mo path
(WF: hbpath_wf path) (NT: path ≠ nil) (EVP: ∀ edge (IN: In edge path), edge_valid lab sb rf edge)
(SB: ∀ edge (IN: In edge path), is_sb edge)
a (A: ∀ first (FST: ohead path = Some first), hb_fst first = a)
b (B: ∀ last (LST: olast path = Some last), hb_snd last = Some b),
happens_before lab sb rf mo a b.
Lemma HBuRF_trough_path:
∀ lab sb rf path
(WF: hbpath_wf path) (NT: path ≠ nil) (EVP: ∀ edge (IN: In edge path), edge_valid lab sb rf edge)
a (A: ∀ first (FST: ohead path = Some first), hb_fst first = a)
b (B: ∀ last (LST: olast path = Some last), hb_snd last = Some b),
happens_before_union_rf sb rf a b.
Lemma HBuRF_trough_path1 :
∀ lab sb rf path
(WF: hbpath_wf path) (NT: path ≠ nil) (EVP: ∀ edge (IN: In edge path), edge_valid lab sb rf edge)
first (FST: ohead path = Some first) last (LST: olast path = Some last),
clos_refl_trans _ (happens_before_union_rf sb rf) (hb_fst first) (hb_fst last).
Lemma NoDup_path :
∀ lab sb rf path
(ACYCLIC: IrreflexiveHBuRF sb rf)
(WF: hbpath_wf path)
(EVP: ∀ edge (IN: In edge path), edge_valid lab sb rf edge),
NoDup path.
Lemma hb_trough_sb_path1 :
∀ lab sb rf mo (ACYCLIC: IrreflexiveHBuRF sb rf) path
(WF: hbpath_wf path) (NT: path ≠ nil) (EVP: ∀ edge (IN: In edge path), edge_valid lab sb rf edge)
(SB: ∀ edge (IN: In edge path) (NL: olast path ≠ Some edge), is_sb edge)
first (FST: ohead path = Some first) last (LST: olast path = Some last),
clos_refl_trans _ (happens_before lab sb rf mo) (hb_fst first) (hb_fst last).
Lemma structure_of_triangled_path:
∀ lab sb rf mo
(ACYCLIC: IrreflexiveHBuRF sb rf) (CONS_RF: ConsistentRF_basic lab sb rf mo)
hmap path (PV: hbpath_valid lab sb rf hmap path)
l (DOM: ∀ edge (IN: In edge path) hf (MAP: hmap edge = Hdef hf), << NA: is_nonatomic (hf l) >> ∧
<< LAB: ¬ HVlabeled (hf l) HLnormal >>),
∃ path1 path2, << DECOMP: path = path1 ++ path2 >> ∧
<< LAB1: ∀ edge (IN: In edge path1) hf1 (MAP: hmap edge = Hdef hf1), HVlabeled (hf1 l) HLtriangle >> ∧
<< LAB2: ∀ edge (IN: In edge path2) hf2 (MAP: hmap edge = Hdef hf2), HVlabeled (hf2 l) HLnabla >>.
Lemma find_triangled_beginning:
∀ lab sb rf mo (CONS_RF: ConsistentRF_basic lab sb rf mo)
path hmap (PV: hbpath_valid lab sb rf hmap path)
l (DOM: ∀ edge (IN: In edge path) hf (MAP: hmap edge = Hdef hf), hf l ≠ HVnone),
∃ pathT pathR, << DECOMP: path = pathT ++ pathR >> ∧
<< NN: ∀ edge (IN: In edge pathT) hf (MAP: hmap edge = Hdef hf),
(¬ HVlabeled (hf l) HLnormal) >> ∧
<< MAX: ∀ edge (E: ohead pathR = Some edge) hf (MAP: hmap edge = Hdef hf),
(HVlabeled (hf l) HLnormal) >>.
Lemma sb_trough_path:
∀ lab sb rf hmap path edge1 edgeN (PV: hbpath_valid lab sb rf hmap (edge1 :: path ++ edgeN :: nil))
(pSB: ∀ edge (IN: In edge path), is_sb edge),
∀ a (SND: hb_snd edge1 = Some a), clos_refl_trans _ sb a (hb_fst edgeN).
Lemma only_first_nabla_is_rf:
∀ lab sb rf mo (CONS_RF: ConsistentRF_basic lab sb rf mo)
edge path hmap (PV: hbpath_valid lab sb rf hmap (edge :: path))
l (DOM: ∀ edge´ (IN: In edge´ (edge :: path)) hf (MAP: hmap edge´ = Hdef hf),
<< NA: is_nonatomic (hf l) >> ∧ << LAB: HVlabeled (hf l) HLnabla >>),
∀ edge´ (IN: In edge´ path), is_sb edge´ ∨ is_sink edge´.
Lemma hb_trough_path_simple:
∀ lab sb rf mo (ACYCLIC: IrreflexiveHBuRF sb rf) (CONS_RF: ConsistentRF_basic lab sb rf mo)
path edge1 edgeN hmap (PV: hbpath_valid lab sb rf hmap (edge1 :: path ++ edgeN :: nil))
l (NORMALfst: ∀ hf (MAPfst: hmap edge1 = Hdef hf), HVlabeled (hf l) HLnormal)
(NORMALlst: ∀ hf (MAPfst: hmap edgeN = Hdef hf), HVlabeled (hf l) HLnormal)
(MID: ∀ edge (IN: In edge path) hf (MAP: hmap edge = Hdef hf), ¬ HVlabeled (hf l) HLnormal)
(NA: ∀ edge (IN: In edge (edge1 :: path ++ edgeN :: nil)) hf (MAP: hmap edge = Hdef hf),
is_nonatomic (hf l)),
∀ b (SND: hb_snd edge1 = Some b), clos_refl_trans _ (happens_before lab sb rf mo) b (hb_fst edgeN).
Require Import Wf Wf_nat.
Lemma hb_trough_path:
∀ lab sb rf mo (ACYCLIC: IrreflexiveHBuRF sb rf) (CONS_RF: ConsistentRF_basic lab sb rf mo)
path edge1 edgeN hmap (PV: hbpath_valid lab sb rf hmap (edge1 :: path ++ edgeN :: nil))
l (NORMALfst: ∀ hf (MAPfst: hmap edge1 = Hdef hf), HVlabeled (hf l) HLnormal)
(NORMALlst: ∀ hf (MAPfst: hmap edgeN = Hdef hf), HVlabeled (hf l) HLnormal)
(NA: ∀ edge (IN: In edge (edge1 :: path ++ edgeN :: nil)) hf (MAP: hmap edge = Hdef hf),
is_nonatomic (hf l)),
∀ b (SND1: hb_snd edge1 = Some b), clos_refl_trans _ (happens_before lab sb rf mo) b (hb_fst edgeN).
Require Import Relations Classical ClassicalDescription.
Require Import List Permutation Vlistbase Vlist extralib.
Require Import c11 fslassn fslmodel fslassnlemmas.
Require Import fslhmap step.
Set Implicit Arguments.
Definition hbpath := list hbcase.
Definition hbpath_wf (path: hbpath) :=
∀ path1 path2 edge1 edge2 (DECOMP: path = path1 ++ edge1 :: edge2 :: path2),
hb_snd edge1 = Some (hb_fst edge2).
Definition hbpath_valid lab sb rf hmap path :=
<< WFP: hbpath_wf path >> ∧
<< EVP: ∀ edge (IN: In edge path), edge_valid lab sb rf edge >> ∧
<< PVA: ∀ edge (IN: In edge path), hmap_valid lab sb rf hmap (hb_fst edge) >>.
Definition hbpath_connects lab sb rf hmap path a b :=
(a = b ∧ path = nil) ∨
hbpath_valid lab sb rf hmap path ∧
∃ fst lst, ohead path = some fst ∧ hb_fst fst = a ∧
olast path = some lst ∧ hb_snd lst = Some b.
Lemma hbpath_wf_one:
∀ edge, hbpath_wf (edge :: nil).
Lemma hbpath_wf_app:
∀ path1 path2, hbpath_wf (path1 ++ path2) → hbpath_wf path1 ∧ hbpath_wf path2.
Lemma hbpath_wf_cons:
∀ edge path, hbpath_wf (edge :: path) → hbpath_wf path.
Lemma hbpath_valid_nil:
∀ lab sb rf hmap, hbpath_valid lab sb rf hmap nil.
Lemma connects_implies_valid:
∀ lab sb rf hmap path a b, hbpath_connects lab sb rf hmap path a b → hbpath_valid lab sb rf hmap path.
Lemma hbpath_valid_app:
∀ lab sb rf hmap path1 path2, hbpath_valid lab sb rf hmap (path1 ++ path2) →
hbpath_valid lab sb rf hmap path1 ∧ hbpath_valid lab sb rf hmap path2.
Lemma hbpath_valid_cons:
∀ lab sb rf hmap edge path,
hbpath_valid lab sb rf hmap (edge :: path) → hbpath_valid lab sb rf hmap path.
Lemma hbpath_valid_cons_inv:
∀ lab sb rf hmap path (PV: hbpath_valid lab sb rf hmap path)
edge (EV: edge_valid lab sb rf edge) (VALIDa: hmap_valid lab sb rf hmap (hb_fst edge))
(VALIDb: ∀ b (SND: hb_snd edge = Some b), hmap_valid lab sb rf hmap b)
(CONNECT: ∀ edge´ (FST: ohead path = Some edge´), hb_snd edge = Some (hb_fst edge´)),
hbpath_valid lab sb rf hmap (edge :: path).
Lemma hbpath_connects_app1:
∀ lab sb rf hmap path1 path2 edge a b
(CONNECT: hbpath_connects lab sb rf hmap (path1 ++ edge :: path2) a b),
hbpath_connects lab sb rf hmap path1 a (hb_fst edge).
Lemma hbpath_connects_app2:
∀ lab sb rf hmap path1 path2 edge a b
(CONNECT: hbpath_connects lab sb rf hmap (path1 ++ edge :: path2) a b),
hbpath_connects lab sb rf hmap (edge :: path2) (hb_fst edge) b.
Lemma hbpath_connects_cons:
∀ lab sb rf hmap edge1 edge2 path a b
(CONNECT: hbpath_connects lab sb rf hmap (edge1 :: edge2 :: path) a b),
hbpath_connects lab sb rf hmap (edge2 :: path) (hb_fst edge2) b.
Lemma hbUrf_implies_hbpath:
∀ lab sb rf hmap V (VALID: hmap_valids lab sb rf hmap V) (HC: hist_closed sb rf V)
a b (HB: happens_before_union_rf sb rf a b) (IN: In b V),
∃ path, hbpath_connects lab sb rf hmap path a b.
Lemma hmap_defined_on_path:
∀ lab sb rf mo (CONS_RF: ConsistentRF_basic lab sb rf mo)
hmap path (PV: hbpath_valid lab sb rf hmap path)
edge (IN: In edge path),
∃ hf, hmap edge = Hdef hf.
Lemma nonatomic_loc_on_path:
∀ lab sb rf mo (CONS_RF: ConsistentRF_basic lab sb rf mo)
hmap path (PV: hbpath_valid lab sb rf hmap path)
l (ALL: ∀ edge (IN: In edge path) hf (MAP: hmap edge = Hdef hf), hf l ≠ HVnone)
(NAX: ∃ edge, << IN: In edge path >> ∧
<< NA: ∀ hf (MAP: hmap edge = Hdef hf), is_nonatomic (hf l) >>),
∀ edge (IN: In edge path) hf (MAP: hmap edge = Hdef hf), is_nonatomic (hf l).
Lemma sink_is_always_last :
∀ path (WF: hbpath_wf path) a (SIN: In (hb_sink a) path), olast path = Some (hb_sink a).
Lemma sink_is_always_last_alt:
∀ path edge (WF: hbpath_wf (path ++ edge :: nil)), ¬ ∃ edge´, In edge´ path ∧ is_sink edge´.
Lemma connects_implies_no_sink:
∀ lab sb rf hmap path a b,
hbpath_connects lab sb rf hmap path a b → ∀ e, ¬ In (hb_sink e) path.
Lemma connect_implies_hbUrf:
∀ lab sb rf hmap path a b (CONNECT: hbpath_connects lab sb rf hmap path a b),
clos_refl_trans _ (happens_before_union_rf sb rf) a b.
Lemma connect_implies_hbUrf_strong:
∀ lab sb rf hmap path a b (CONNECT: hbpath_connects lab sb rf hmap path a b),
path ≠ nil → happens_before_union_rf sb rf a b.
Lemma hb_trough_sb_path:
∀ lab sb rf mo path
(WF: hbpath_wf path) (NT: path ≠ nil) (EVP: ∀ edge (IN: In edge path), edge_valid lab sb rf edge)
(SB: ∀ edge (IN: In edge path), is_sb edge)
a (A: ∀ first (FST: ohead path = Some first), hb_fst first = a)
b (B: ∀ last (LST: olast path = Some last), hb_snd last = Some b),
happens_before lab sb rf mo a b.
Lemma HBuRF_trough_path:
∀ lab sb rf path
(WF: hbpath_wf path) (NT: path ≠ nil) (EVP: ∀ edge (IN: In edge path), edge_valid lab sb rf edge)
a (A: ∀ first (FST: ohead path = Some first), hb_fst first = a)
b (B: ∀ last (LST: olast path = Some last), hb_snd last = Some b),
happens_before_union_rf sb rf a b.
Lemma HBuRF_trough_path1 :
∀ lab sb rf path
(WF: hbpath_wf path) (NT: path ≠ nil) (EVP: ∀ edge (IN: In edge path), edge_valid lab sb rf edge)
first (FST: ohead path = Some first) last (LST: olast path = Some last),
clos_refl_trans _ (happens_before_union_rf sb rf) (hb_fst first) (hb_fst last).
Lemma NoDup_path :
∀ lab sb rf path
(ACYCLIC: IrreflexiveHBuRF sb rf)
(WF: hbpath_wf path)
(EVP: ∀ edge (IN: In edge path), edge_valid lab sb rf edge),
NoDup path.
Lemma hb_trough_sb_path1 :
∀ lab sb rf mo (ACYCLIC: IrreflexiveHBuRF sb rf) path
(WF: hbpath_wf path) (NT: path ≠ nil) (EVP: ∀ edge (IN: In edge path), edge_valid lab sb rf edge)
(SB: ∀ edge (IN: In edge path) (NL: olast path ≠ Some edge), is_sb edge)
first (FST: ohead path = Some first) last (LST: olast path = Some last),
clos_refl_trans _ (happens_before lab sb rf mo) (hb_fst first) (hb_fst last).
Lemma structure_of_triangled_path:
∀ lab sb rf mo
(ACYCLIC: IrreflexiveHBuRF sb rf) (CONS_RF: ConsistentRF_basic lab sb rf mo)
hmap path (PV: hbpath_valid lab sb rf hmap path)
l (DOM: ∀ edge (IN: In edge path) hf (MAP: hmap edge = Hdef hf), << NA: is_nonatomic (hf l) >> ∧
<< LAB: ¬ HVlabeled (hf l) HLnormal >>),
∃ path1 path2, << DECOMP: path = path1 ++ path2 >> ∧
<< LAB1: ∀ edge (IN: In edge path1) hf1 (MAP: hmap edge = Hdef hf1), HVlabeled (hf1 l) HLtriangle >> ∧
<< LAB2: ∀ edge (IN: In edge path2) hf2 (MAP: hmap edge = Hdef hf2), HVlabeled (hf2 l) HLnabla >>.
Lemma find_triangled_beginning:
∀ lab sb rf mo (CONS_RF: ConsistentRF_basic lab sb rf mo)
path hmap (PV: hbpath_valid lab sb rf hmap path)
l (DOM: ∀ edge (IN: In edge path) hf (MAP: hmap edge = Hdef hf), hf l ≠ HVnone),
∃ pathT pathR, << DECOMP: path = pathT ++ pathR >> ∧
<< NN: ∀ edge (IN: In edge pathT) hf (MAP: hmap edge = Hdef hf),
(¬ HVlabeled (hf l) HLnormal) >> ∧
<< MAX: ∀ edge (E: ohead pathR = Some edge) hf (MAP: hmap edge = Hdef hf),
(HVlabeled (hf l) HLnormal) >>.
Lemma sb_trough_path:
∀ lab sb rf hmap path edge1 edgeN (PV: hbpath_valid lab sb rf hmap (edge1 :: path ++ edgeN :: nil))
(pSB: ∀ edge (IN: In edge path), is_sb edge),
∀ a (SND: hb_snd edge1 = Some a), clos_refl_trans _ sb a (hb_fst edgeN).
Lemma only_first_nabla_is_rf:
∀ lab sb rf mo (CONS_RF: ConsistentRF_basic lab sb rf mo)
edge path hmap (PV: hbpath_valid lab sb rf hmap (edge :: path))
l (DOM: ∀ edge´ (IN: In edge´ (edge :: path)) hf (MAP: hmap edge´ = Hdef hf),
<< NA: is_nonatomic (hf l) >> ∧ << LAB: HVlabeled (hf l) HLnabla >>),
∀ edge´ (IN: In edge´ path), is_sb edge´ ∨ is_sink edge´.
Lemma hb_trough_path_simple:
∀ lab sb rf mo (ACYCLIC: IrreflexiveHBuRF sb rf) (CONS_RF: ConsistentRF_basic lab sb rf mo)
path edge1 edgeN hmap (PV: hbpath_valid lab sb rf hmap (edge1 :: path ++ edgeN :: nil))
l (NORMALfst: ∀ hf (MAPfst: hmap edge1 = Hdef hf), HVlabeled (hf l) HLnormal)
(NORMALlst: ∀ hf (MAPfst: hmap edgeN = Hdef hf), HVlabeled (hf l) HLnormal)
(MID: ∀ edge (IN: In edge path) hf (MAP: hmap edge = Hdef hf), ¬ HVlabeled (hf l) HLnormal)
(NA: ∀ edge (IN: In edge (edge1 :: path ++ edgeN :: nil)) hf (MAP: hmap edge = Hdef hf),
is_nonatomic (hf l)),
∀ b (SND: hb_snd edge1 = Some b), clos_refl_trans _ (happens_before lab sb rf mo) b (hb_fst edgeN).
Require Import Wf Wf_nat.
Lemma hb_trough_path:
∀ lab sb rf mo (ACYCLIC: IrreflexiveHBuRF sb rf) (CONS_RF: ConsistentRF_basic lab sb rf mo)
path edge1 edgeN hmap (PV: hbpath_valid lab sb rf hmap (edge1 :: path ++ edgeN :: nil))
l (NORMALfst: ∀ hf (MAPfst: hmap edge1 = Hdef hf), HVlabeled (hf l) HLnormal)
(NORMALlst: ∀ hf (MAPfst: hmap edgeN = Hdef hf), HVlabeled (hf l) HLnormal)
(NA: ∀ edge (IN: In edge (edge1 :: path ++ edgeN :: nil)) hf (MAP: hmap edge = Hdef hf),
is_nonatomic (hf l)),
∀ b (SND1: hb_snd edge1 = Some b), clos_refl_trans _ (happens_before lab sb rf mo) b (hb_fst edgeN).
This page has been generated by coqdoc