The Axiomatization of Overriding and Update✩
Online Appendix: Human-Readable Proofs
Jasper Berendsen, David N. Jansen∗, Julien Schmaltz, Frits W. Vaandrager∗∗
Institute for Computing and Information Sciences
Radboud University Nijmegen, The Netherlands
Abstract
This document contains human-readable proofs for the derived laws in Figure 3 of the article published under the
same title in the Journal of Applied Logic. The proofs are mostly based on the ones provided by I.
In the following, we provide equational proofs for all laws in Figure 3. Lemmas are tagged with the number of
the law and with a letter to indicate the order of proofs: in each proof, only laws with an earlier letter may be used. If
a rule is only applied to a part of the formula, the part that is going to be replaced is red and underlined, and the part
that has just been replaced is blue and overlined. The proofs are mostly based on the ones provided by I; they
differ mainly if the automatic proof for one law contains (most of) the proof for another.
We assume left-associativity and the usual priorities: @ binds strongest and ⊲ binds weakest.
The axioms are:
x⊲x= x
x−x=∅
(Ax 1)
(Ax 2)
x−y⊲y=y⊲x
(Ax 3)
x − (y − z) = x − y ⊲ x @ z
(x ⊲ y) − z = x − z ⊲ y − z
(Ax 4)
(Ax 5)
The operator @ is defined as an abbreviation:
x @ y = x − (x − y)
(@)
1. Proof based on Axioms 1–3
∅ ⊲ x =Ax 2
= x − x ⊲ x =Ax 3
= x ⊲ x =Ax 1
=x
(A/8)
✩
Research supported by NWO/EW project 612.000.103 Fault-tolerant Real-time Algorithms Analyzed Incrementally (FRAAI). The research
leading to these results has received funding from the European Community’s Seventh Framework Programme under grant agreement no 214755
(QUASIMODO).
∗ Corresponding author for this appendix.
∗∗ Corresponding author for the main article.
Email addresses: [email protected] (David N. Jansen), [email protected] (Frits W. Vaandrager)
1
2. Proofs based on Axioms 1–3 and 5
∅ − x =A/8
= ∅ ⊲ ∅ − x =Ax 3
= ∅ − x − ∅ ⊲ ∅ =Ax 2
= ∅ − x − ∅ ⊲ ∅ − ∅ =Ax 5
= (∅ − x ⊲ ∅) − ∅ =Ax 2
= (∅ − x ⊲ x − x) − ∅ =Ax 5
= (∅ ⊲ x) − x − ∅ =A/8
= x − x − ∅ =Ax 2
= ∅ − ∅ =Ax 2
=∅
(B/10)
x ⊲ ∅ =Ax 3
= ∅ − x ⊲ x =B/10
= ∅ ⊲ x =A/8
=x
(C/7)
x − ∅ =C/7
= x − ∅ ⊲ ∅ =Ax 3
= ∅ ⊲ x =A/8
=x
(D/9)
x @ x =@
= x − (x − x) =Ax 2
= x − ∅ =D/9
=x
(E/13)
(x ⊲ y) − x =Ax 5
= x − x ⊲ y − x =Ax 2
= ∅ ⊲ y − x =A/8
=y−x
(F/)
(x ⊲ y) − y =Ax 5
= x − y ⊲ y − y =Ax 2
= x − y ⊲ ∅ =C/7
= x−y
2
(G/)
(x ⊲ y ⊲ z) − x =Ax 5
= (x ⊲ y) − x ⊲ z − x =F/
=y−x⊲z−x
(H/18)
x ⊲ y − x =Ax 3
= y − x − x ⊲ x =G/
= (y − x ⊲ x) − x ⊲ x =Ax 3
= x ⊲ (y − x ⊲ x) =Ax 3
= x ⊲ (x ⊲ y) =Ax 3
= (x ⊲ y) − x ⊲ x =F/
= y − x ⊲ x =Ax 3
= x⊲y
(I/31)
3. Proofs based on Axioms 1–5
x − y ⊲ x =I/31
= x − y ⊲ x − (x − y) =@,Ax 4
= x − (y − y) =Ax 2
= x − ∅ =D/9
=x
(J/30)
x @ y ⊲ x − y =@
= x − (x − y) ⊲ x − y =Ax 3
= x − y ⊲ x =J/30
=x
(K/24)
x − (y − x) =Ax 4
= x − y ⊲ x @ x =E/13
= x − y ⊲ x =J/30
=x
(L/27)
x − y − z =C/7
= x − y − z ⊲ ∅ =Ax 2
= x − y − z ⊲ x − y − (x − y) =L/27
= x − y − z ⊲ x − y − (x − y − (y − (x − y))) =L/27
= x − y − z ⊲ x − y − (x − y − y) =@,Ax 4
= x − y − (z − y)
3
(M/)
x − y − (z − x) =Ax 4,@
= x − y − z ⊲ x − y − (x − y − x) =G/
= x − y − z ⊲ x − y − ((x − y ⊲ x) − x) =J/30
= x − y − z ⊲ x − y − (x − x) =Ax 2
= x − y − z ⊲ x − y − ∅ =D/9
= x − y − z ⊲ x − y =J/30
= x−y
(N/)
x − (y − (z − x)) =Ax 4,@
= x − y ⊲ x − (x − (z − x)) =L/27
= x − y ⊲ x − x =Ax 2
= x − y ⊲ ∅ =C/7
= x−y
(O/)
x − z − y =M/
= x − z − (y − z) =F/
= (y − z ⊲ x − z) − (y − z) =Ax 5,N/
= (y ⊲ x) − z − (y − z − (x − y)) =Ax 3,M/
= (x − y ⊲ y) − z − (y − z − (x − y − z)) =Ax 5
= (x − y − z ⊲ y − z) − (y − z − (x − y − z)) =Ax 3
= (y − z − (x − y − z) ⊲ x − y − z) − (y − z − (x − y − z)) =F/
= x − y − z − (y − z − (x − y − z)) =L/27
= x−y−z
(P/19)
x − (y ⊲ z) =L/27,@
= x − (y ⊲ z) − (y − (x − (y ⊲ z))) =Ax 4
= x − (y ⊲ z) − (y − x ⊲ y − (y − (y ⊲ z))) =G/
= x − (y ⊲ z) − (y − x ⊲ y − ((y ⊲ (y ⊲ z)) − (y ⊲ z))) =Ax 3
= x − (y ⊲ z) − (y − x ⊲ y − (((y ⊲ z) − y ⊲ y) − (y ⊲ z))) =F/
= x − (y ⊲ z) − (y − x ⊲ y − ((z − y ⊲ y) − (y ⊲ z))) =Ax 3
= x − (y ⊲ z) − (y − x ⊲ y − ((y ⊲ z) − (y ⊲ z))) =Ax 2
= x − (y ⊲ z) − (y − x ⊲ y − ∅) =D/9
= x − (y ⊲ z) − (y − x ⊲ y) =J/30
= x − (y ⊲ z) − y =P/19
= x − y − (y ⊲ z) =L/27
= x − y − (y − (x − y) ⊲ z) =O/
= x − y − ((y − (x − y) ⊲ z) − (y − (x − y))) =F/
= x − y − (z − (y − (x − y))) =O/
= x−y−z
4
(Q/26)
x − x @ y =K/24,@
= (x − (x − y) ⊲ x − y) − (x − (x − y)) =F/
= x − y − (x − (x − y)) =L/27
= x−y
(R/)
x ⊲ y − z =I/31
= x ⊲ y − z − x =P/19
= x ⊲ y − x − z =Q/26
= x ⊲ y − (x ⊲ z) =I/31
= x ⊲ y − (x ⊲ z − x) =Q/26
= x ⊲ y − x − (z − x) =P/19
= x ⊲ y − (z − x) − x =I/31
= x ⊲ y − (z − x) =L/27
= x − (z − x) ⊲ y − (z − x) =Ax 5
= (x ⊲ y) − (z − x)
(S/)
x − y ⊲ x − z =S/
= (x − y ⊲ x) − (z − (x − y)) =J/30
= x − (z − (x − y)) =Ax 4,@
= x − z ⊲ x − (x − (x − y)) =@,R/
= x−z⊲x−y
(T/21)
x − y ⊲ x @ y =@
= x − y ⊲ x − (x − y) =I/31
= x − y ⊲ x =J/30
=x
(U/25)
x ⊲ y @ x =@
= x ⊲ y − (y − x) =Ax 3
= y − (y − x) − x ⊲ x =P/19
= y − x − (y − x) ⊲ x =Ax 2
= ∅ ⊲ x =A/8
=x
5
(V/28)
x ⊲ x − y =Ax 3
= x − y − x ⊲ x =G/
= (x − y ⊲ x) − x ⊲ x =J/30
= x − x ⊲ x =Ax 2
= ∅ ⊲ x =A/8
=x
(W/29)
x @ y − y =@
= x − (x − y) − y =P/19
= x − y − (x − y) =Ax 2
=∅
(X/6)
x ⊲ y ⊲ z =U/25
= (x ⊲ y ⊲ z) − x ⊲ (x ⊲ y ⊲ z) @ x =H/18
= y − x ⊲ z − x ⊲ (x ⊲ y ⊲ z) @ x =Ax 5,@
= (y ⊲ z) − x ⊲ (x ⊲ y ⊲ z) − ((x ⊲ y ⊲ z) − x) =H/18
= (y ⊲ z) − x ⊲ (x ⊲ y ⊲ z) − (y − x ⊲ z − x) =Q/26
= (y ⊲ z) − x ⊲ (x ⊲ y ⊲ z) − (y − x) − (z − x) =Ax 5
= (y ⊲ z) − x ⊲ ((x ⊲ y) − (y − x) ⊲ z − (y − x)) − (z − x) =Ax 5
= (y ⊲ z) − x ⊲ (x − (y − x) ⊲ y − (y − x) ⊲ z − (y − x)) − (z − x) =L/27
= (y ⊲ z) − x ⊲ (x ⊲ y − (y − x) ⊲ z − (y − x)) − (z − x) =V/28
= (y ⊲ z) − x ⊲ (x ⊲ z − (y − x)) − (z − x) =L/27
= (y ⊲ z) − x ⊲ (x − (y − x) ⊲ z − (y − x)) − (z − x) =Ax 5
= (y ⊲ z) − x ⊲ (x ⊲ z) − (y − x) − (z − x) =P/19
= (y ⊲ z) − x ⊲ (x ⊲ z) − (z − x) − (y − x) =Ax 5
= (y ⊲ z) − x ⊲ (x − (z − x) ⊲ z − (z − x)) − (y − x) =L/27
= (y ⊲ z) − x ⊲ (x ⊲ z − (z − x)) − (y − x) =V/28
= (y ⊲ z) − x ⊲ x − (y − x) =L/27
= (y ⊲ z) − x ⊲ x =Ax 3
= x ⊲ (y ⊲ z)
(Y/11)
x − (y − z) =Ax 4,@
= x − y ⊲ x − (x − z) =T/21
= x − (x − z) ⊲ x − y =@
= x@z⊲x−y
6
(Z/)
x @ (y @ z) =@
= x @ (y − (y − z)) =@
= x − (x − (y − (y − z))) =Z/
= x − (x @ (y − z) ⊲ x − y) =Q/26
= x − x @ (y − z) − (x − y) =P/19
= x − (x − y) − x @ (y − z) =@
= x − (x − y) − (x − (x − (y − z))) =Z/
= x − (x − y) − (x − (x @ z ⊲ x − y)) =Q/26
= x − (x − y) − (x − x @ z − (x − y)) =Q/26
= x − (x − y ⊲ x − x @ z − (x − y)) =R/
= x − (x − y ⊲ x − z − (x − y)) =P/19
= x − (x − y ⊲ x − (x − y) − z) =Q/26
= x − (x − y) − (x − (x − y) − z) =@
= (x − (x − y)) @ z =@
= x@y@z
(a/12)
x − (y − z) − (x − z) =Z/
= (x @ z ⊲ x − y) − (x − z) =Ax 5
= x @ z − (x − z) ⊲ x − y − (x − z) =L/27,P/19
= x @ z − (x − z − (x − (x − z))) ⊲ x − (x − z) − y =@,@
= x @ z − (x − z − x @ z) ⊲ x @ z − y =L/27
= x @ z ⊲ x @ z − y =W/29
= x@z
(b/)
(x ⊲ y) @ z =@
= (x ⊲ y) − ((x ⊲ y) − z) =Ax 5
= (x ⊲ y) − (x − z ⊲ y − z) =Ax 5
= x − (x − z ⊲ y − z) ⊲ y − (x − z ⊲ y − z) =Q/26,Q/26
= x − (x − z) − (y − z) ⊲ y − (x − z) − (y − z) =P/19
= x − (y − z) − (x − z) ⊲ y − (x − z) − (y − z) =b/,b/
= x@z⊲y@z
(c/14)
x @ (y ⊲ z) =@
= x − (x − (y ⊲ z)) =Q/26
= x − (x − y − z) =Z/,@
= x − (x − z) ⊲ x − (x − y) =T/21
= x − (x − y) ⊲ x − (x − z) =@
= x@y⊲x@z
7
(d/15)
x @ y − z =@
= x − (x − y) − z =P/19
= x − z − (x − y) =Q/26
= x − (z ⊲ x − y) =I/31
= x − (z ⊲ x − y − z) =P/19
= x − (z ⊲ x − z − y) =Q/26
= x − (z ⊲ x − (z ⊲ y)) =I/31
= x − (z ⊲ x − (z ⊲ y − z)) =Q/26
= x − z − (x − (z ⊲ y − z)) =Q/26
= x − z − (x − z − (y − z)) =@
= (x − z) @ (y − z)
(e/16)
x ⊲ y @ z =V/28
= x ⊲ y @ x ⊲ y @ z =Y/11
= x ⊲ (y @ x ⊲ y @ z) =W/29,d/15
= x ⊲ x − (x − z) ⊲ y @ (x ⊲ z) =E/13,@
= x @ x ⊲ x @ z ⊲ y @ (x ⊲ z) =d/15
= x @ (x ⊲ z) ⊲ y @ (x ⊲ z) =c/14
= (x ⊲ y) @ (x ⊲ z)
(f/17)
x − (y ⊲ z) =Q/26
= x − y − z =P/19
= x − z − y =Q/26
= x − (z ⊲ y)
(g/20)
x @ y @ z =@
= (x − (x − y)) @ z =@
= x − (x − y) − (x − (x − y) − z) =Q/26
= x − (x − y ⊲ x − (x − y) − z) =P/19
= x − (x − y ⊲ x − z − (x − y)) =I/31
= x − (x − y ⊲ x − z) =Q/26
= x − (x − y) − (x − z)
(h/)
x @ y @ z =h/
= x − (x − y) − (x − z) =P/19
= x − (x − z) − (x − y) =h/
= x@z@y
8
(i/22)
x − y ⊲ x − z =T/21
= x − z ⊲ x − y =S/
= (x − z ⊲ x) − (y − (x − z)) =J/30,Z/
= x − (y @ z ⊲ y − x) =S/
= x − ((y @ z ⊲ y) − (x − y @ z)) =@
= x − ((y − (y − z) ⊲ y) − (x − y @ z)) =J/30,J/30
= (x − y @ z ⊲ x) − (y − (x − y @ z)) =S/
= x − y @ z ⊲ x − y =T/21
= x − y ⊲ x − y @ z =S/
= (x − y ⊲ x) − (y @ z − (x − y)) =J/30,@
= x − (y − (y − z) − (x − y)) =N/
= x − (y − (y − z)) =@
= x−y@z
(j/)
x − y @ z =j/
= x − y ⊲ x − z =T/21
= x − z ⊲ x − y =j/
= x−z@y
(k/23)
(x − y) @ z =@
= x − y − (x − y − z) =P/19
= x − y − (x − z − y) =Q/26
= x − (y ⊲ x − z − y) =I/31
= x − (y ⊲ x − z) =Q/26
= x − y − (x − z) =P/19
= x − (x − z) − y =@
= x@z−y
(l/32)
x @ (y − z) =@
= x − (x − (y − z)) =Z/
= x − (x − (x − z) ⊲ x − y) =Q/26
= x − (x − (x − z)) − (x − y) =R/
= x − z − (x − y) =P/19
= x − (x − y) − z =@
= x@y−z
9
(m/33)

AN OVERPARTITION ANALOGUE OF THE q-BINOMIAL

TU-Da

Document 1718984