Problem:
 and P (all (\x. Q x)) -> all (\x. and P (Q x))
 and (all (\x. Q x)) P -> all (\x. and (Q x) P)
 or P (all (\x. Q x)) -> all (\x. or P (Q x))
 or (all (\x. Q x)) P -> all (\x. or (Q x) P)
 and P (ex (\x. Q x)) -> ex (\x. and P (Q x))
 and (ex (\x. Q x)) P -> ex (\x. and (Q x) P)
 or P (ex (\x. Q x)) -> ex (\x. or P (Q x))
 or (ex (\x. Q x)) P -> ex (\x. or (Q x) P)
 not (all (\x. Q x)) -> ex (\x. not (Q x))
 not (ex (\x. Q x)) -> all (\x. not (Q x))

Proof:
 Higher-Order Church Rosser Processor:
  and P (all (\x. Q x)) -> all (\x. and P (Q x))
  and (all (\x. Q x)) P -> all (\x. and (Q x) P)
  or P (all (\x. Q x)) -> all (\x. or P (Q x))
  or (all (\x. Q x)) P -> all (\x. or (Q x) P)
  and P (ex (\x. Q x)) -> ex (\x. and P (Q x))
  and (ex (\x. Q x)) P -> ex (\x. and (Q x) P)
  or P (ex (\x. Q x)) -> ex (\x. or P (Q x))
  or (ex (\x. Q x)) P -> ex (\x. or (Q x) P)
  not (all (\x. Q x)) -> ex (\x. not (Q x))
  not (ex (\x. Q x)) -> all (\x. not (Q x))
  critical peaks: 16
   all (\x. and (all (\x. 11 x)) (12 x)) <-[]-> all (\x. and (11 x) (all (\x. 12 x)))
   all (\x. and (ex (\x. 30 x)) (31 x)) <-[]-> ex (\x. and (30 x) (all (\x. 31 x)))
   all (\x. and (40 x) (all (\x. 41 x))) <-[]-> all (\x. and (all (\x. 40 x)) (41 x))
   all (\x. and (56 x) (ex (\x. 57 x))) <-[]-> ex (\x. and (all (\x. 56 x)) (57 x))
   all (\x. or (all (\x. 80 x)) (81 x)) <-[]-> all (\x. or (80 x) (all (\x. 81 x)))
   all (\x. or (ex (\x. 99 x)) (100 x)) <-[]-> ex (\x. or (99 x) (all (\x. 100 x)))
   all (\x. or (109 x) (all (\x. 110 x))) <-[]-> all (\x. or (all (\x. 109 x)) (110 x))
   all (\x. or (125 x) (ex (\x. 126 x))) <-[]-> ex (\x. or (all (\x. 125 x)) (126 x))
   ex (\x. and (all (\x. 152 x)) (153 x)) <-[]-> all (\x. and (152 x) (ex (\x. 153 x)))
   ex (\x. and (ex (\x. 168 x)) (169 x)) <-[]-> ex (\x. and (168 x) (ex (\x. 169 x)))
   ex (\x. and (178 x) (all (\x. 179 x))) <-[]-> all (\x. and (ex (\x. 178 x)) (179 x))
   ex (\x. and (196 x) (ex (\x. 197 x))) <-[]-> ex (\x. and (ex (\x. 196 x)) (197 x))
   ex (\x. or (all (\x. 221 x)) (222 x)) <-[]-> all (\x. or (221 x) (ex (\x. 222 x)))
   ex (\x. or (ex (\x. 237 x)) (238 x)) <-[]-> ex (\x. or (237 x) (ex (\x. 238 x)))
   ex (\x. or (247 x) (all (\x. 248 x))) <-[]-> all (\x. or (ex (\x. 247 x)) (248 x))
   ex (\x. or (265 x) (ex (\x. 266 x))) <-[]-> ex (\x. or (ex (\x. 265 x)) (266 x))
   
   Higher-Order Nonconfluence Processor:
    non-joinable conversion:
    all (\x. all (\291. and (11 291) (12 x))) *<- all (\x. and (all (\x. 11 x)) (12 x)) <- . -> 
    all (\x. and (11 x) (all (\x. 12 x))) ->* all (\x. all (\306. and (11 x) (12 306)))
    Qed