module Control.WellFounded import Data.Natimport Data.List public exportdata Accessible : (rel : a -> a -> Type) -> (x : a) -> Type where  Access : (rec : (y : a) -> rel y x -> Accessible rel y) ->           Accessible rel x public exportinterface WellFounded (rel : a -> a -> Type) where  wellFounded : (x : a) -> Accessible rel x exportaccRec : {0 rel : (arg1 : a) -> (arg2 : a) -> Type} ->         (step : (x : a) -> ((y : a) -> rel y x -> b) -> b) ->         (z : a) -> (0 acc : Accessible rel z) -> baccRec step z (Access f) =  step z $ \yarg, lt => accRec step yarg (f yarg lt) exportaccInd : {0 rel : a -> a -> Type} -> {0 P : a -> Type} ->         (step : (x : a) -> ((y : a) -> rel y x -> P y) -> P x) ->         (z : a) -> (0 acc : Accessible rel z) -> P zaccInd step z (Access f) =  step z $ \y, lt => accInd step y (f y lt) exportwfRec : WellFounded rel =>        (step : (x : a) -> ((y : a) -> rel y x -> b) -> b) ->        a -> bwfRec step x = accRec step x (wellFounded {rel} x) exportwfInd : WellFounded rel => {0 P : a -> Type} ->        (step : (x : a) -> ((y : a) -> rel y x -> P y) -> P x) ->        (myz : a) -> P myzwfInd step myz = accInd step myz (wellFounded {rel} myz) public exportinterface Sized a where  size : a -> Nat public exportSmaller : Sized a => a -> a -> TypeSmaller x y = size x `LT` size y public exportSizeAccessible : Sized a => a -> TypeSizeAccessible = Accessible Smaller exportsizeAccessible : Sized a => (x : a) -> SizeAccessible xsizeAccessible x = Access (acc $ size x)  where    acc : (sizeX : Nat) -> (y : a) -> (size y `LT` sizeX) -> SizeAccessible y    acc (S x') y (LTESucc yLEx')        = Access (\z, zLTy => acc x' z (lteTransitive zLTy yLEx')) exportsizeInd : Sized a => {0 P : a -> Type} ->          (step : (x : a) -> ((y : a) -> Smaller y x -> P y) -> P x) ->          (z : a) ->          P zsizeInd step z = accInd step z (sizeAccessible z) exportsizeRec : Sized a =>          (step : (x : a) -> ((y : a) -> Smaller y x -> b) -> b) ->          (z : a) -> bsizeRec step z = accRec step z (sizeAccessible z) exportimplementation Sized Nat where  size = \x => x exportimplementation Sized (List a) where  size = length exportimplementation (Sized a, Sized b) => Sized (Pair a b) where  size (x,y) = size x + size y