Add proof about 'both' and pairing

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-04-13 12:25:59 -07:00 · 2024-04-13 12:25:59 -07:00 · b6e357787f
commit b6e357787f
parent ce3fa182fe
1 changed files with 5 additions and 1 deletions
--- a/Language.agda
+++ b/Language.agda
@ -278,7 +278,11 @@ module Graphs where
                 {P-Mono : MonotonicPredicate P}
                 {m₁ : MonotonicGraphFunction T₁} {m₂ : MonotonicGraphFunction T₂} →
                 always P m₁ → always Q m₂ → always (Both P Q) (m₁ ⟨⊗⟩ m₂)
-    ⟨⊗⟩-reason = {!!}
+    ⟨⊗⟩-reason {P-Mono = P-Mono} {m₁ = m₁} {m₂ = m₂} aP aQ g
+        with p ← aP g
+        with (g' , (t₁ , g⊆g')) ← m₁ g
+        with q ← aQ g'
+        with (g'' , (t₂ , g'⊆g'')) ← m₂ g' = (P-Mono _ _ _ g'⊆g'' p , q)

    module Construction where
        pushBasicBlock : List BasicStmt → MonotonicGraphFunction Graph.Index