MiniAgda by Andreas Abel and Karl Mehltretter --- opening "AccCoqTermination.ma" --- --- scope checking --- --- type checking --- type Acc : ^(A : Set) -> ^(Lt : A -> A -> Set) -> ^ A -> Set term Acc.acc : .[A : Set] -> .[Lt : A -> A -> Set] -> .[b : A] -> ^(y1 : (a : A) -> Lt a b -> Acc A Lt a) -> < Acc.acc b y1 : Acc A Lt b > type Nat : Set term Nat.zero : < Nat.zero : Nat > term Nat.succ : ^(y0 : Nat) -> < Nat.succ y0 : Nat > type R : ^ Nat -> ^ Nat -> Set term R.r1 : .[x : Nat] -> < R.r1 x : R (Nat.succ (Nat.succ x)) (Nat.succ Nat.zero) > term R.r2 : < R.r2 : R (Nat.succ Nat.zero) Nat.zero > term acc2 : (n : Nat) -> Acc Nat R (Nat.succ (Nat.succ n)) term acc2 = \ n -> Acc.acc [Nat.succ (Nat.succ n)] (\ a -> \ p -> case p : R a (Nat.succ (Nat.succ n)) {}) term aux1 : (a : Nat) -> (p : R a (Nat.succ Nat.zero)) -> Acc Nat R a { aux1 (Nat.succ (Nat.succ x)) (R.r1 [.x]) = acc2 x } term acc1 : Acc Nat R (Nat.succ Nat.zero) term acc1 = Acc.acc [Nat.succ Nat.zero] aux1 term aux0 : (a : Nat) -> (p : R a Nat.zero) -> Acc Nat R a { aux0 .(succ zero) R.r2 = acc1 } term acc0 : Acc Nat R Nat.zero term acc0 = Acc.acc [Nat.zero] aux0 term accR : (n : Nat) -> Acc Nat R n { accR Nat.zero = acc0 ; accR (Nat.succ Nat.zero) = acc1 ; accR (Nat.succ (Nat.succ n)) = acc2 n } term acc_dest : (n : Nat) -> (p : Acc Nat R n) -> (m : Nat) -> R m n -> Acc Nat R m { acc_dest .n (Acc.acc [n] p) = p } term f : (x : Nat) -> Acc Nat R x -> Nat { f x (Acc.acc [.x] p) = case x : Nat { Nat.zero -> f (Nat.succ x) (p (Nat.succ x) R.r2) ; Nat.succ Nat.zero -> f (Nat.succ x) (p (Nat.succ x) (R.r1 [Nat.zero])) ; Nat.succ (Nat.succ y) -> Nat.zero } } term g : (x : Nat) -> .[Acc Nat R x] -> Nat { g x [p] = case x : Nat { Nat.zero -> g (Nat.succ x) [acc_dest Nat.zero p (Nat.succ x) R.r2] ; Nat.succ Nat.zero -> g (Nat.succ x) [acc_dest (Nat.succ Nat.zero) p (Nat.succ x) (R.r1 [Nat.zero])] ; Nat.succ (Nat.succ y) -> Nat.zero } } error during typechecking: Termination check for function g fails