| and(P, forall(λx46:term.Q · x46)) | ⇒ | forall(λx45:term.and(P, Q · x45))
|
| and(forall(λx48:term.Q · x48), P) | ⇒ | forall(λx47:term.and(Q · x47, P))
|
| and(P, exists(λx50:term.Q · x50)) | ⇒ | exists(λx49:term.and(P, Q · x49))
|
| and(exists(λx52:term.Q · x52), P) | ⇒ | exists(λx51:term.and(Q · x51, P))
|
| or(P, forall(λx54:term.Q · x54)) | ⇒ | forall(λx53:term.or(P, Q · x53))
|
| or(forall(λx56:term.Q · x56), P) | ⇒ | forall(λx55:term.or(Q · x55, P))
|
| or(P, exists(λx58:term.Q · x58)) | ⇒ | exists(λx57:term.or(P, Q · x57))
|
| or(exists(λx60:term.Q · x60), P) | ⇒ | exists(λx59:term.or(Q · x59, P))
|
| not(forall(λx62:term.Q · x62)) | ⇒ | exists(λx61:term.not(Q · x61))
|
| not(exists(λx64:term.Q · x64)) | ⇒ | forall(λx63:term.not(Q · x63))
|