Theory "acyclicity"

Parents     indexedLists   patternMatches

Signature

Constant Type
geq_arg :(num -> num -> num) -> bool
increasing :(num -> num -> num) -> bool
top_sorted_abs :(α -> α -> bool) -> α list -> bool
wlp :(β -> β -> bool) -> (β -> α) -> (γ -> α -> α) -> (α -> α -> γ) -> β -> β list -> α

Definitions

top_sorted_abs_def
|- (∀R vtx1 G.
      top_sorted_abs R (vtx1::G) ⇔
      EVERY (λvtx2. ¬R vtx2 vtx1) G ∧ top_sorted_abs R G) ∧
   ∀R. top_sorted_abs R [] ⇔ T
wlp_def
|- (∀R w g f vtx1 vtx2 G.
      wlp R w g f vtx1 (vtx2::G) =
      if R vtx1 vtx2 then
        g (f (w vtx1) (wlp R w g f vtx2 G)) (wlp R w g f vtx1 G)
      else wlp R w g f vtx1 G) ∧ ∀R w g f vtx1. wlp R w g f vtx1 [] = w vtx1
geq_arg_def
|- ∀f. geq_arg f ⇔ ∀x y. x ≤ f x y ∧ y ≤ f x y
increasing_def
|- ∀f. increasing f ⇔ ∀e b c d. e ≤ c ∧ b ≤ d ⇒ f e b ≤ f c d


Theorems

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)