定義37 zは、yの中でvが"自由"な範囲に、"束縛"された"変数"を持たない (define (IsNotBoundIn z y v) (not (∃ n ≦ (len y) (∃ m ≦ (len z) (∃ w ≦ z (and (= w (elm z m)) (IsBoundAt w n y) (IsFreeAt v n y))))))) こういうの見るとつい 束縛が入れ子にな…