module A201903.3-5-Properties-BigStep-HAO where
open import A201903.2-1-Semantics-BigStep
open HAO public
import A201903.3-3-Properties-BigStep-CBV as CBV
na←nawnf-cbv-⟱ : ∀ {n} {e : Tm n} {e′} → NAWNF e → e CBV.⟱ e′ → NA e′
na←nawnf-cbv-⟱ var CBV.var = var
na←nawnf-cbv-⟱ (app p₁ p₂) (CBV.applam r₁ r₂ r) = case p₁′ of λ ()
where
p₁′ = nawnf←wnf (CBV.wnf-⟱ r₁) (na←nawnf-cbv-⟱ p₁ r₁)
na←nawnf-cbv-⟱ (app p₁ p₂) (CBV.app r₁ p₁′ r₂) = app
na←nawnf-⟱ : ∀ {n} {e : Tm n} {e′} → NAWNF e → e ⟱ e′ → NA e′
na←nawnf-⟱ var var = var
na←nawnf-⟱ (app p₁ p₂) (applam r₁ r₂ r) = case (na←nawnf-cbv-⟱ p₁ r₁) of λ ()
na←nawnf-⟱ (app p₁ p₂) (app r₁ p₁′ r₁′ r₂) = app
na←wnf-⟱ : ∀ {n} {e : Tm n} {e′} → WNF e → NA e → e ⟱ e′ → NA e′
na←wnf-⟱ lam () r
na←wnf-⟱ (wnf p) p′ r = na←nawnf-⟱ p r
nf-⟱ : ∀ {n} {e : Tm n} {e′} → e ⟱ e′ → NF e′
nf-⟱ (applam r₁ r₂ r) = nf-⟱ r
nf-⟱ var = nf var
nf-⟱ (lam r) = lam (nf-⟱ r)
nf-⟱ (app r₁ p₁′ r₁′ r₂) = nf (app p₁ (nf-⟱ r₂))
where
p₁ = nanf←nf (nf-⟱ r₁′) (na←wnf-⟱ (CBV.wnf-⟱ r₁) p₁′ r₁′)
mutual
refl-⟱ : ∀ {n} {e : Tm n} → NF e → e ⟱ e
refl-⟱ (lam p) = lam (refl-⟱ p)
refl-⟱ (nf p) = refl-⟱′ p
refl-⟱′ : ∀ {n} {e : Tm n} → NANF e → e ⟱ e
refl-⟱′ (var) = var
refl-⟱′ (app p₁ p₂) = app (CBV.refl-⟱′ (nawnf←nanf p₁)) (na←nanf p₁) (refl-⟱′ p₁) (refl-⟱ p₂)