measures.golden

--- opening "measures.ma" ---
--- scope checking ---
--- type checking ---
type  Bool : Set
term  Bool.true : < Bool.true : Bool >
term  Bool.false : < Bool.false : Bool >
type  Nat : + Size -> Set
term  Nat.zero : .[s!ze : Size] -> .[i < s!ze] -> Nat s!ze
term  Nat.zero : .[i : Size] -> < Nat.zero i : Nat $i >
term  Nat.succ : .[s!ze : Size] -> .[i < s!ze] -> ^ Nat i -> Nat s!ze
term  Nat.succ : .[i : Size] -> ^(y1 : Nat i) -> < Nat.succ i y1 : Nat $i >
term  even : .[i : Size] -> Nat i -> Bool
term  even' : .[i : Size] -> Nat i -> Bool
term  odd' : .[i : Size] -> Nat i -> Bool
{ even [i] n = even' [i] n
}
{ even' [i] (Nat.zero [j < i]) = Bool.true
; even' [i] (Nat.succ [j < i] n) = odd' [j] n
}
{ odd' [i] (Nat.zero [j < i]) = Bool.false
; odd' [i] (Nat.succ [j < i] n) = even [j] n
}
--- evaluating ---
--- closing "measures.ma" ---