- finite_dom_always_has_mapping
-
|- ∀s. FINITE s ⇒ ∃f. FDOM f = s
- scc_lemma_1_4_1_1_2_1_1_1_1
-
|- ∀fdom vs v f.
v ∉ vs ∧ FDOM f ⊆ fdom ∧ v ∈ FDOM f ⇒
v ∈ FDOM (DRESTRICT f (fdom DIFF vs))
- vtx_cut_main_lemma_1_1_1_1_1
-
|- ∀x. FDOM (SND x) ≠ ∅ ⇒ (λx. x ≠ (FEMPTY,FEMPTY)) x
- graph_plan_lemma_1_1_1
-
|- ∀fm1 fm2 vs. fm2 ⊑ fm1 ⇒ DRESTRICT fm2 vs ⊑ DRESTRICT fm1 vs
- drestrict_subset_submap
-
|- ∀fm1 fm2. fm2 ⊑ fm1 ∧ vs2 ⊆ vs1 ⇒ DRESTRICT fm2 vs2 ⊑ DRESTRICT fm1 vs1
- drestrict_subset_submap_2
-
|- ∀fm1 fm2. FDOM fm2 ⊆ vs ∧ fm2 ⊑ fm1 ⇒ fm2 ⊑ DRESTRICT fm1 vs
- graph_plan_lemma_1_2_1
-
|- ∀fm1 fm2 vs.
vs ⊆ FDOM fm1 ∧ (fm2 = fm1) ⇒ (DRESTRICT fm2 vs = DRESTRICT fm1 vs)
- graph_plan_lemma_1_2_2
-
|- ∀x vs s. DISJOINT (FDOM x) vs ⇒ (DRESTRICT s vs = DRESTRICT (x ⊌ s) vs)
- DRESTRICTED_FUNION_2
-
|- DRESTRICT (f1 ⊌ f2) s = DRESTRICT f1 s ⊌ DRESTRICT f2 s
- graph_plan_lemma_1_3
-
|- ∀x vs. (FDOM (DRESTRICT x vs) = ∅) ⇔ DISJOINT (FDOM x) vs
- graph_plan_lemma_2_1
-
|- ∀PROB vs. FINITE vs ⇒ CARD (FDOM (DRESTRICT s vs)) ≤ CARD vs
- graph_plan_lemma_2_3_7_2_1
-
|- ∀x vs y. x ∈ vs ⇒ (x ∈ FDOM (DRESTRICT y vs) ⇔ x ∈ FDOM y)
- graph_plan_lemma_2_3_8_3
-
|- ∀x y vs. FDOM x ⊆ FDOM y ⇒ FDOM (DRESTRICT x vs) ⊆ FDOM (DRESTRICT y vs)
- graph_plan_lemma_2_3_8_4
-
|- ∀s s' vs.
(FDOM s = FDOM s') ⇒ (FDOM (DRESTRICT s vs) = FDOM (DRESTRICT s' vs))
- graph_plan_lemma_2_3_8_5
-
|- ∀x vs. FDOM x ⊆ vs ⇒ (DRESTRICT x vs = x)
- graph_plan_lemma_5
-
|- ∀s s' vs.
(DRESTRICT s (FDOM s DIFF vs) = DRESTRICT s' (FDOM s' DIFF vs)) ∧
(DRESTRICT s vs = DRESTRICT s' vs) ⇒
(s = s')
- eq_restricted_eq_full
-
|- ∀s s' vs.
(DRESTRICT s vs1 = DRESTRICT s' vs1) ∧
(DRESTRICT s vs2 = DRESTRICT s' vs2) ∧ FDOM s ⊆ vs1 ∪ vs2 ∧
FDOM s' ⊆ vs1 ∪ vs2 ⇒
(s = s')
- graph_plan_lemma_9_1_1_1
-
|- ∀x s vs. DRESTRICT x vs ⊑ s ⇔ DRESTRICT x vs ⊑ DRESTRICT s vs
- graph_plan_lemma_12_1
-
|- ∀s s' vs x.
(DRESTRICT s vs = DRESTRICT s' vs) ⇒
(DRESTRICT x vs ⊑ s ⇔ DRESTRICT x vs ⊑ s')
- graph_plan_lemma_12_4
-
|- ∀fm1 fm2 vs. fm2 ⊑ fm1 ⇒ DRESTRICT fm2 vs ⊑ fm1
- graph_plan_lemma_14_1
-
|- ∀x. SND ((λa. (DRESTRICT (FST a) vs,SND a)) x) = SND x
- child_parent_lemma_1_1_3
-
|- ∀x vs. FDOM (DRESTRICT x vs) ≠ ∅ ⇒ FDOM x ≠ ∅
- bound_child_parent_lemma_1_1_1_1_3
-
|- ∀x y z. (FDOM x = FDOM y) ⇒ (FDOM (DRESTRICT x z) = FDOM (DRESTRICT y z))
- graph_plan_lemma_23_1
-
|- ∀x s vs. x ⊑ DRESTRICT s vs ⇒ x ⊑ s
- bound_child_parent_lemma_1_1_1_3_1_1_1
-
|- ∀vs a s s'.
(DRESTRICT s vs = DRESTRICT s' vs) ∧ a ⊑ s ⇒ DRESTRICT a vs ⊑ s'
- bound_child_parent_lemma_1_1_1_3_1_2
-
|- ∀vs a s.
FDOM a ⊆ FDOM s ∧ DRESTRICT a vs ⊑ s ∧ DRESTRICT a (FDOM s DIFF vs) ⊑ s ⇒
a ⊑ s
- submap_drestrict_diff
-
|- ∀vs a s fdom.
FDOM a ⊆ fdom ∧ FDOM s ⊆ fdom ∧ DRESTRICT a vs ⊑ s ∧
DRESTRICT a (fdom DIFF vs) ⊑ s ⇒
a ⊑ s
- FDOM_INTER_NEQ_DRESTRICT_NEQ
-
|- FDOM s ∩ vs1 ≠ FDOM s2 ∩ vs2 ⇒ DRESTRICT s vs1 ≠ DRESTRICT s2 vs2
- limited_dom_neq_restricted_neq
-
|- FDOM f1 ⊆ vs ∧ f1 ⊌ f2 ≠ f2 ⇒ DRESTRICT (f1 ⊌ f2) vs ≠ DRESTRICT f2 vs
- submap_subset
-
|- f1 ⊑ f2 ⇒ FDOM f1 ⊆ FDOM f2
- submap_drestrict_eq
-
|- ∀fm1 fm2 vs.
vs ⊆ FDOM fm1 ∧ fm1 ⊑ fm2 ⇒ (DRESTRICT fm1 vs = DRESTRICT fm2 vs)
- two_submaps_are_submap
-
|- fm1 ⊑ fm3 ∧ fm2 ⊑ fm3 ⇒ fm1 ⊌ fm2 ⊑ fm3
- union_of_submaps_is_submap
-
|- (∀fm. MEM fm fmList ⇒ fm ⊑ fm') ⇒ FOLDR FUNION FEMPTY fmList ⊑ fm'
- SUBMAP_FUNION_DRESTRICT
-
|- fma ⊑ s ∧ fmb ⊑ s ∧ vsa ⊆ FDOM fma ∧ vsb ⊆ FDOM fmb ∧
(DRESTRICT fm vsa = DRESTRICT fma (vsa ∩ vs)) ∧
(DRESTRICT fm vsb = DRESTRICT fmb (vsb ∩ vs)) ⇒
(DRESTRICT fm (vsa ∪ vsb) = DRESTRICT (fma ⊌ fmb) ((vsa ∪ vsb) ∩ vs))
- UNION_FUNION_DRESTRICT
-
|- (DRESTRICT fm vsa = DRESTRICT fma vs) ∧
(DRESTRICT fm vsb = DRESTRICT fmb vs) ⇒
(DRESTRICT fm (vsa ∪ vsb) = DRESTRICT (fma ⊌ fmb) vs)
- FUNION_DRESTRICT_UNION
-
|- (fm1 = DRESTRICT fm vs1) ∧ (fm2 = DRESTRICT fm vs2) ⇒
(fm1 ⊌ fm2 = DRESTRICT fm (vs1 ∪ vs2))