module mutual-rec where


open import map
open import even-odd using (
  Even[_] ; Odd[_] ; ⊢Even ; ⊢Odd ; even-suc[_] ; even-zero[] ; odd-suc[_])
open import Data.List using ([] ; _∷_ ; [_])
open import Data.Vec renaming ([] to [||] ; _∷_ to _¦_  ; [_] to [|_|] )

We start with the declaration of variables that will be used in the call to adm.

β₁ : mix-var
β₁ = tvar 

Γβ₁ : type-context {mix-var}
Γβ₁ = ⟦ [| β₁ |] ⟧

f : mix-var
f = fvar 

We then define the term we would like to run adm on, and the specification with respect to which we are considering it.

t = even-suc[ odd-suc[ even-zero[] ] ]

⊢Even[β₁] : Γβ₁ ∥ ∅ ⊢ Even[ varᵀ β₁ ]
⊢Even[β₁] = ⊢Even (var-intro ∋-last)

C,s = adm t ⊢Even[β₁] [| varᵀ f |] (record { curr =  }) []