List all the cases for the other direction
This commit is contained in:
parent
2c839db924
commit
eca6181494
11
Map.agda
11
Map.agda
|
@ -386,3 +386,14 @@ module _ (f : B → B → B) where
|
||||||
... | (_ , (bothᵘ (bothᵘ (single {v₁} v₁∈e₁) (single {v₂} v₂∈e₂)) (single {v₃} v₃∈e₃) , v₁v₂v₃∈m₁₂m₃))
|
... | (_ , (bothᵘ (bothᵘ (single {v₁} v₁∈e₁) (single {v₂} v₂∈e₂)) (single {v₃} v₃∈e₃) , v₁v₂v₃∈m₁₂m₃))
|
||||||
rewrite Map-functional {m = union f (union f m₁ m₂) m₃} k,v∈m₁₂m₃ v₁v₂v₃∈m₁₂m₃ =
|
rewrite Map-functional {m = union f (union f m₁ m₂) m₃} k,v∈m₁₂m₃ v₁v₂v₃∈m₁₂m₃ =
|
||||||
(f v₁ (f v₂ v₃) , (f-assoc v₁ v₂ v₃ , ImplInsert.union-combines f u₁ (ImplInsert.union-preserves-Unique f l₂ l₃ u₃) v₁∈e₁ (ImplInsert.union-combines f u₂ u₃ v₂∈e₂ v₃∈e₃)))
|
(f v₁ (f v₂ v₃) , (f-assoc v₁ v₂ v₃ , ImplInsert.union-combines f u₁ (ImplInsert.union-preserves-Unique f l₂ l₃ u₃) v₁∈e₁ (ImplInsert.union-combines f u₂ u₃ v₂∈e₂ v₃∈e₃)))
|
||||||
|
|
||||||
|
union-assoc₂ : ∀ (m₁ m₂ m₃ : Map) → subset (_≡_) (union f m₁ (union f m₂ m₃)) (union f (union f m₁ m₂) m₃)
|
||||||
|
union-assoc₂ m₁@(l₁ , u₁) m₂@(l₂ , u₂) m₃@(l₃ , u₃) k v k,v∈m₁m₂₃
|
||||||
|
with Expr-Provenance f k ((` m₁) ∪ ((` m₂) ∪ (` m₃))) (∈-cong proj₁ k,v∈m₁m₂₃)
|
||||||
|
... | (_ , (in₂ k∉ke₁ (in₂ k∉e₂ (single {v₃} v₁∈e₃)) , v₃∈m₁m₂₃)) = {!!}
|
||||||
|
... | (_ , (in₂ k∉ke₁ (in₁ (single {v₂} v₂∈e₂) k∉e₃) , v₂∈m₁m₂₃)) = {!!}
|
||||||
|
... | (_ , (in₂ k∉ke₁ (bothᵘ (single {v₂} v₂∈e₂) (single {v₃} v₁∈e₃)) , v₂v₃∈m₁m₂₃)) = {!!}
|
||||||
|
... | (_ , (in₁ (single {v₁} v₁∈e₁) k∉ke₁₂ , v₁∈m₁m₂₃)) = {!!}
|
||||||
|
... | (_ , (bothᵘ (single {v₁} v₁∈e₁) (in₂ k∉e₂ (single {v₃} v₁∈e₃)) , v₁v₃∈m₁m₂₃)) = {!!}
|
||||||
|
... | (_ , (bothᵘ (single {v₁} v₁∈e₁) (in₁ (single {v₂} v₂∈e₂) k∉e₃) , v₁v₂∈m₁m₂₃)) = {!!}
|
||||||
|
... | (_ , (bothᵘ (single {v₁} v₁∈e₁) (bothᵘ (single {v₂} v₂∈e₂) (single {v₃} v₁∈e₃)) , v₁v₂v₃∈m₁m₂₃)) = {!!}
|
||||||
|
|
Loading…
Reference in New Issue
Block a user