{-# OPTIONS --cubical-compatible #-}
module Padova2025-zh-TW.ProvingBasics.Termination where

良基遞迴#

import Padova2025-zh-TW.ProvingBasics.Termination.Intro
import Padova2025-zh-TW.ProvingBasics.Termination.Ordering
import Padova2025-zh-TW.ProvingBasics.Termination.Gas
import Padova2025-zh-TW.ProvingBasics.Termination.WellFounded
import Padova2025-zh-TW.ProvingBasics.Termination.BoveCapretta