次世代言語11[Rust Swift TypeScript Dart]

>>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))