>>958
>α=β
>のときの
>|a=b|=∧[x∈VBξ+1,ξ<α](a(into(x))⇔b(into(x)))
=∧[x∈VBα](a(x)⇔b(x))
これに尽きますね
また
>>948
>x=(ξ,x),a=(α,a)
>が
>x∈a
>であるB真理値を
>|x∈a|=a(into(x)) for γ<α-1,a(x) for γ=α-1, 0 for γ≧α
γじゃなくてξの間違い
intoはidも含むことにしたし
そのあとの考察で1つズラしてるから
|x∈a|=a(into(x)) for ξ≦α, 0 for ξ>α
となるのだけど
ξ>αのときは
into(a)(x)
の方が適当に見えるかも知れないけど
ξ>α
のときは
x=(ξ,x)
のξが最小である（xが（idでない）intoの像にならない）ことから
into(a)(x)=0
なので
|x∈a|=a(into(x)) for ξ≦α, 0 for ξ>α
（ここのintoはidも含む）