- top_sorted_abs_mem
-
|- top_sorted_abs R (vtx1::G) ∧ MEM vtx2 G ⇒ ¬R vtx2 vtx1
- top_sorted_cons
-
|- top_sorted_abs R (vtx::G) ⇒ top_sorted_abs R G
- individual_weight_less_eq_lp
-
|- geq_arg g ⇒ w vtx ≤ wlp R w g f vtx G
- lp_geq_lp_from_successor
-
|- ∀vtx1.
geq_arg f ∧ geq_arg g ∧ (∀vtx. MEM vtx G ⇒ ¬R vtx vtx) ∧ R vtx2 vtx1 ∧
MEM vtx1 G ∧ top_sorted_abs R G ⇒
f (w vtx2) (wlp R w g f vtx1 G) ≤ wlp R w g f vtx2 G
- weight_fun_leq_imp_lp_leq
-
|- ∀vtx.
increasing f ∧ increasing g ∧ (∀vtx. MEM vtx G ⇒ w1 vtx ≤ w2 vtx) ∧
w1 vtx ≤ w2 vtx ⇒
wlp R w1 g f vtx G ≤ wlp R w2 g f vtx G
- wlp_congruence_rule
-
|- ∀l1 l2 R1 R2 w1 w2 g1 g2 f1 f2 x1 x2.
(l1 = l2) ∧ (∀y. MEM y l2 ⇒ (R1 x1 y ⇔ R2 x2 y)) ∧
(∀y. MEM y l2 ⇒ (R1 y x1 ⇔ R2 y x2)) ∧ (w1 x1 = w2 x2) ∧
(∀y1 y2. (y1 = y2) ⇒ (f1 (w1 x1) y1 = f2 (w2 x2) y2)) ∧
(∀y1 y2 z1 z2.
(y1 = y2) ∧ (z1 = z2) ⇒
(g1 (f1 (w1 x1) y1) z1 = g2 (f2 (w2 x2) y2) z2)) ∧
(∀x y. MEM x l2 ∧ MEM y l2 ⇒ (R1 x y ⇔ R2 x y)) ∧
(∀x. MEM x l2 ⇒ (w1 x = w2 x)) ∧
(∀x y z. MEM x l2 ⇒ (g1 (f1 (w1 x) y) z = g2 (f2 (w2 x) y) z)) ∧
(∀x y. MEM x l2 ⇒ (f1 (w1 x) y = f2 (w1 x) y)) ⇒
(wlp R1 w1 g1 f1 x1 l1 = wlp R2 w2 g2 f2 x2 l2)
- wlp_ite_weights
-
|- ∀x.
(∀y. MEM y l1 ⇒ P y) ∧ P x ⇒
(wlp R (λy. if P y then w1 y else w2 y) g f x l1 = wlp R w1 g f x l1)
- map_wlp_ite_weights
-
|- (∀x. MEM x l1 ⇒ P x) ∧ (∀x. MEM x l2 ⇒ P x) ⇒
(MAP (λx. wlp R (λy. if P y then w1 y else w2 y) g f x l1) l2 =
MAP (λx. wlp R w1 g f x l1) l2)
- wlp_weight_lamda_exp
-
|- ∀x. wlp R w g f x l = wlp R (λy. w y) g f x l
- img_wlp_ite_weights
-
|- (∀x. MEM x l ⇒ P x) ∧ (∀x. x ∈ s ⇒ P x) ⇒
(IMAGE (λx. wlp R (λy. if P y then w1 y else w2 y) g f x l) s =
IMAGE (λx. wlp R w1 g f x l) s)