{-# OPTIONS --postfix-projections --safe --without-K #-}

open import Data.Empty using ()
open import Data.Product
open import Data.Sum
open import Relation.Binary.PropositionalEquality using (_≡_; refl)
open import Relation.Binary.Construct.Closure.ReflexiveTransitive using (ε; _◅_; _◅◅_)
open import Relation.Binary.Construct.Closure.Symmetric

module MAV.Example where

Atom : Set
Atom = 

open import MAV.Structure Atom
open import MAV.CutElim Atom using (cut-elim)
import MAV.Base.Reasoning Atom as MAV
import MAV.Symmetric Atom as SMAV

-- An example:
--
--  Normalising A proof that (`I `⊕ `I) `◁ (`I `& `I) ⊸ (`I `⊕ `I) `◁ (`I `& `I):

example₁ : Structure
example₁ = (`I `⊕ `I) `◁ (`I `& `I)

SMAV-proof-of-example₁ : (example₁ `⅋  example₁) SMAV.⟶⋆ `I
SMAV-proof-of-example₁ = SMAV.step (`axiom example₁)  ε
  where open SMAV

-- MAV-proof-of-example₁ : (example₁ `⅋ `¬ example₁) MAV.Deep.⟶⋆ `I
MAV-proof-of-example₁ : (example₁ `⅋  example₁) MAV.⟶⋆ `I
MAV-proof-of-example₁ = 
  -- {! Deep.to (cut-elim _ SMAV-proof-of-example₁) !}
  begin
    ((`I `⊕ `I) `◁ (`I `& `I)) `⅋ ((`I `& `I) `◁ (`I `⊕ `I)) 
  ∼⟨ emb `⅋-comm  
    ((`I `& `I) `◁ (`I `⊕ `I)) `⅋ ((`I `⊕ `I) `◁ (`I `& `I)) 
  ∼⟨ emb `⅋-comm  
    ((`I `⊕ `I) `◁ (`I `& `I)) `⅋ ((`I `& `I) `◁ (`I `⊕ `I)) 
  ∼⟨ emb `⅋-comm  
    ((`I `& `I) `◁ (`I `⊕ `I)) `⅋ ((`I `⊕ `I) `◁ (`I `& `I)) 
  ∼⟨ emb `⅋-comm  
    ((`I `⊕ `I) `◁ (`I `& `I)) `⅋ ((`I `& `I) `◁ (`I `⊕ `I)) 
  ∼⟨ emb `⅋-comm  
    ((`I `& `I) `◁ (`I `⊕ `I)) `⅋ ((`I `⊕ `I) `◁ (`I `& `I)) 
  ∼⟨ emb `⅋-comm  
    ((`I `⊕ `I) `◁ (`I `& `I)) `⅋ ((`I `& `I) `◁ (`I `⊕ `I)) 
  ∼⟨ emb `⅋-comm  
    ((`I `& `I) `◁ (`I `⊕ `I)) `⅋ ((`I `⊕ `I) `◁ (`I `& `I)) 
  ∼⟨ emb `⅋-comm  
    ((`I `⊕ `I) `◁ (`I `& `I)) `⅋ ((`I `& `I) `◁ (`I `⊕ `I)) 
  ∼⟨ emb `⅋-comm  
    ((`I `& `I) `◁ (`I `⊕ `I)) `⅋ ((`I `⊕ `I) `◁ (`I `& `I)) 
  ∼⟨ emb `⅋-comm  
    ((`I `⊕ `I) `◁ (`I `& `I)) `⅋ ((`I `& `I) `◁ (`I `⊕ `I)) 
  ∼⟨ emb `⅋-comm  
    ((`I `& `I) `◁ (`I `⊕ `I)) `⅋ ((`I `⊕ `I) `◁ (`I `& `I))
  ⟶⟨ emb `sequence 
      ((`I `& `I) `⅋ (`I `⊕ `I)) `◁ ((`I `⊕ `I) `⅋ (`I `& `I)) 
  ∼⟨ emb `⅋-comm `⟨◁  
    ((`I `⊕ `I) `⅋ (`I `& `I)) `◁ ((`I `⊕ `I) `⅋ (`I `& `I)) 
  ∼⟨ emb `⅋-comm `⟨◁  
    ((`I `& `I) `⅋ (`I `⊕ `I)) `◁ ((`I `⊕ `I) `⅋ (`I `& `I))
  ⟶⟨ emb `external `⟨◁ 
      ((`I `⅋ (`I `⊕ `I)) `& (`I `⅋ (`I `⊕ `I))) `◁  ((`I `⊕ `I) `⅋ (`I `& `I))  
  ∼⟨ (`&⟩ emb `⅋-comm) `⟨◁  
    ((`I `⅋ (`I `⊕ `I)) `& ((`I `⊕ `I) `⅋ `I)) `◁  ((`I `⊕ `I) `⅋ (`I `& `I))  
  ∼⟨ (`&⟩ emb `⅋-comm) `⟨◁  
    ((`I `⅋ (`I `⊕ `I)) `& (`I `⅋ (`I `⊕ `I))) `◁  ((`I `⊕ `I) `⅋ (`I `& `I))  
  ∼⟨ (`&⟩ emb `⅋-comm) `⟨◁ 
    ((`I `⅋ (`I `⊕ `I)) `& ((`I `⊕ `I) `⅋ `I)) `◁  ((`I `⊕ `I) `⅋ (`I `& `I))  
  ∼⟨ (`&⟩ emb `⅋-identityʳ) `⟨◁ 
    ((`I `⅋ (`I `⊕ `I)) `& (`I `⊕ `I)) `◁ ((`I `⊕ `I) `⅋ (`I `& `I))  
  ∼⟨ (emb `⅋-comm `⟨&) `⟨◁  
    (((`I `⊕ `I) `⅋ `I) `& (`I `⊕ `I)) `◁ ((`I `⊕ `I) `⅋ (`I `& `I))  
  ∼⟨ (emb `⅋-comm `⟨&) `⟨◁  
    ((`I `⅋ (`I `⊕ `I)) `& (`I `⊕ `I)) `◁ ((`I `⊕ `I) `⅋ (`I `& `I))  
  ∼⟨ (emb `⅋-comm `⟨&) `⟨◁ 
    (((`I `⊕ `I) `⅋ `I) `& (`I `⊕ `I)) `◁ ((`I `⊕ `I) `⅋ (`I `& `I))  
  ∼⟨ (emb `⅋-identityʳ `⟨&) `⟨◁ 
    ((`I `⊕ `I) `& (`I `⊕ `I)) `◁ ((`I `⊕ `I) `⅋ (`I `& `I))
  ⟶⟨ (`&⟩ emb `right) `⟨◁ 
    ((`I `⊕ `I) `& `I) `◁ ((`I `⊕ `I) `⅋ (`I `& `I))
  ⟶⟨ (emb `left `⟨&) `⟨◁  
    (`I `& `I) `◁ ((`I `⊕ `I) `⅋ (`I `& `I))
  ⟶⟨ emb `tidy `⟨◁ 
    `I `◁ ((`I `⊕ `I) `⅋ (`I `& `I)) 
  ∼⟨ emb `◁-identityˡ 
    (`I `⊕ `I) `⅋ (`I `& `I) 
  ∼⟨ emb `⅋-comm  
    (`I `& `I) `⅋ (`I `⊕ `I)
  ⟶⟨ emb `external 
      (`I `⅋ (`I `⊕ `I)) `& (`I `⅋ (`I `⊕ `I)) 
  ∼⟨ `&⟩ emb `⅋-comm   
    (`I `⅋ (`I `⊕ `I)) `& ((`I `⊕ `I) `⅋ `I)
  ⟶⟨ `&⟩ (emb `right `⟨⅋)  
    (`I `⅋ (`I `⊕ `I)) `& (`I `⅋ `I) 
  ∼⟨ `&⟩ emb `⅋-comm 
    (`I `⅋ (`I `⊕ `I)) `& (`I `⅋ `I) 
  ∼⟨ `&⟩ emb `⅋-identityʳ 
    (`I `⅋ (`I `⊕ `I)) `& `I 
  ∼⟨ emb `⅋-comm `⟨&  
    ((`I `⊕ `I) `⅋ `I) `& `I
  ⟶⟨ (emb `left `⟨⅋) `⟨& 
    (`I `⅋ `I) `& `I 
  ∼⟨ emb `⅋-comm `⟨& 
    (`I `⅋ `I) `& `I 
  ∼⟨ emb `⅋-identityʳ `⟨& 
    `I `& `I
  ⟶⟨ emb `tidy 
    `I
  
  -- where open MAV.Deep
  where open MAV

_ : cut-elim _ SMAV-proof-of-example₁  MAV-proof-of-example₁
_ = refl