staload "$PATSHOMELOCS/atscntrb-hx-intinf/SATS/intinf_vt.sats" fun choose_ats {n:nat}{ m : nat | m <= n } : (int(n), int(m)) -> Intinf = "mac#" fun double_factorial_ats {n:nat} : int(n) -> Intinf = "mac#" fun factorial_ats {n:nat} : int(n) -> Intinf = "mac#" fun catalan_ats {n:nat} : int(n) -> Intinf = "mac#" fun derangements_ats {n:nat} : int(n) -> Intinf = "mac#" fun permutations_ats {n:nat}{ k : nat | k <= n && k > 0 } : (int(n), int(k)) -> Intinf = "mac#" fun max_regions_ats {n:nat} : int(n) -> Intinf = "mac#"