Properties of“=” C=yDy=E 2.Fx=y2(y=22x=2 3. F=y)(S2A= S, A)where a and y are free for e in a 4.Fx=y(S2t=S2+) 5.}m1=91∧…∧x f(g1,., yn) for any n-ary function symbol f 6.x1=91A…∧xn )for any n-ary predicate symbol P Logic in Computer Science -p 4/15Properties of “=” 1. ` x = y ⊃ y = x 2. ` x = y ⊃ (y = z ⊃ x = z) 3. ` x = y ⊃ (SzxA ≡ SzyA) where x and y are free for z in A. 4. ` x = y ⊃ (Szxt = Szy t) 5. ` x1 = y1 ∧ · · · ∧ xn = yn ⊃ f(x1, · · · , xn) = f(y1, · · · , yn) for any n-ary function symbol f. 6. ` x1 = y1 ∧ · · · ∧ xn = yn ⊃ (P(x1, · · · , xn) ≡ P(y1, · · · , yn)) for any n-ary predicate symbol P. Logic in Computer Science – p.4/15