596(1): デフォルトの名無しさん [sage] 2018/06/18(月) 19:23:14.64 ID:xdRdwSco(4/4) AAS
>>595
＞すまない。俺はバカなんだ。分からないんで教えて下さい。

辞書順を保ったまま <n, 0 <n,1> をそれぞれ 2*n, 2*n+1 で置き換えられる
3*nとか4nでもいいけど2つしかないから2nで十分

例

fun f
{n:nat} .<3*n>.
(n: int n) : bool =
if n = 0 then true else g (n-1)
and g
{n:nat} .<3*n+2>.
(n: int n) : bool = not (h (n))
and h
{n:nat} .<3*n+1>.
(n: int n) : bool = not (f (n))