Theory "fmap_utils"

Parents     finite_map

Theorems

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))