Attempt to prove unrolling.thm4.5a

2 files changed, 15 insertions, 2 deletions

diff --git a/src/Cfe/Expression/Base.agda b/src/Cfe/Expression/Base.agda
index 1cd57a7..aabab1b 100644
--- a/src/Cfe/Expression/Base.agda
+++ b/src/Cfe/Expression/Base.agda
@@ -100,5 +100,5 @@ rank (μ e) = suc (rank e)
 
 infix 4 _<ᵣₐₙₖ_
 
-_<ᵣₐₙₖ_ : ∀ {n} → Rel (Expression n) _
-_<ᵣₐₙₖ_ = ℕ._<_ on rank
+_<ᵣₐₙₖ_ : ∀ {m n} → REL (Expression m) (Expression n) _
+e <ᵣₐₙₖ e′ = rank e ℕ.< rank e′
diff --git a/src/Cfe/Expression/Properties.agda b/src/Cfe/Expression/Properties.agda
index d1e2869..f21fe72 100644
--- a/src/Cfe/Expression/Properties.agda
+++ b/src/Cfe/Expression/Properties.agda
@@ -231,3 +231,16 @@ e₂<ᵣₐₙₖe₁∨e₂ e₁ e₂ = begin-strict
   rank (e₁ ∨ e₂)            ∎
   where
   open ≤-Reasoning
+
+-- ⟦ e ⟧ (⟦ μ e ⟧ [] ∷ []) ≤ ⟦ μ e ⟧ []
+-- l ∈ ⟦ e ⟧ (⟦ μ e ⟧ [] ∷ []) → l ∈ ⟦ μ e ⟧ []
+-- l ∈ ⟦ e ⟧ (⟦ μ e ⟧ [] ∷ []) → l ∈ ⋃ (λ x → ⟦ e ⟧ (x ∷ []))
+-- l ∈ ⟦ e′ ⟧ (⟦ μ e ⟧ [] ∷ []) → ∃[ n ] l ∈ ⟦ e′ ⟧ ((λ X → ⟦ e ⟧ (X ∷ [])) ^ n ∷ [])
+-- e-unroll : ∀ {n} (e : Expression (suc n)) e′ i γ → ⟦ e [ e′ / i ] ⟧ γ L.≤ ∃[ n ] (⟦ e ⟧ )
+-- e-unroll ⊥ = ?
+-- e-unroll ε = ?
+-- e-unroll (Char x) = ?
+-- e-unroll (e ∨ e₁) = {!!}
+-- e-unroll (e ∙ e₁) = {!!}
+-- e-unroll (Var x) = {!!}
+-- e-unroll (μ e) = {!!}