ゲーデルの不完全性定理の証明のアレをRacketで書いてみる (22)

定義27 xのn番目の要素をcで置き換えたもの

(define (substAtWith x n c)
  (Min z ≦ (M8 x c)
       (∃ a b ≦ x
          (and (= n (+ (len a) 1))
               (= x (** (** a (<> (elm x n))) b))
               (= z (** (** a c) b))))))

aという列があって
aとxのn番目の要素とbをつないだものがxになって
aとcとbをつなぐとzになるような
最小のz

うん、xのn番目の要素がcに置き換わってる

ただし、1≦n≦len(x)が前提
ちゃんとこういう前提が守られるように作っているのかな
assert入れとけば？（違う

ここでM8が再登場しているのはどうしてかなー

(define (M8 x y)
  (expt (P (+ (len x) (len y))) (+ x y)))

以前の定義は列の連結のところで出てました
xにcを連結したよりは短い
そういうことか