Advertisement
Not a member of Pastebin yet?
Sign Up,
it unlocks many cool features!
- mutual
- data Simple : ℕ → Type → Set where
- compl : Simple zero compl
- intcompl : Simple zero (δcompl int)
- realcompl : Simple zero (δcompl real)
- lift : ∀{n t} → (φ : Simple n t) → (m : ℕ) → (¬Lift φ) → Simple (suc (n + m)) t
- _⇨_ : ∀{n t t′} → Simple n t → Simple n t′ → Simple (suc n) (t ⇨ t′)
- data ¬Lift : ∀{n t} → Simple n t → Set where
- compl : ¬Lift compl
- intcompl : ¬Lift intcompl
- realcompl : ¬Lift realcompl
- _⇨_ : ∀{n t t′} → (φ : Simple n t) → (φ′ : Simple n t′) → ¬Lift (φ ⇨ φ′)
- -- Non terminating
- ss' : {t : Type} → {n : ℕ} → (φ : Simple n t) → ℕ
- ss' compl = 0
- ss' intcompl = 0
- ss' realcompl = 0
- ss' (lift φ _ _) = 0
- ss' (φ ⇨ compl) = 0
- ss' (φ ⇨ intcompl) = 0
- ss' (φ ⇨ realcompl) = 0
- ss' (φ ⇨ lift _ _ _) = ss' φ
- ss' (φ ⇨ (φ′ ⇨ φ″)) = ss' (φ′ ⇨ φ″)
Advertisement
Add Comment
Please, Sign In to add comment
Advertisement