P1_P2_commute_type.txt

P1_P2_commute
	 : ∀ (A P : Type) (zeroP : P) (eqA lteA : brel A) 
         (eqP : brel P) (addP : binary_op P),
         A
         → P
           → ∀ fA : A → A,
               brel_not_trivial A eqA fA
               → brel_congruence A eqA eqA
                 → brel_reflexive A eqA
                   → brel_symmetric A eqA
                     → brel_transitive A eqA
                       → brel_congruence P eqP eqP
                         → bop_congruence P eqP addP
                           → brel_reflexive P eqP
                             → brel_symmetric P eqP
                               → brel_transitive P eqP
                                 → brel_congruence A eqA lteA
                                   → brel_reflexive A lteA
                                     → brel_transitive A lteA
                                       → brel_not_total A lteA
                                         → bop_associative P eqP addP
                                           → bop_commutative P eqP addP
                                             → (∀ p : P,
                                                 eqP (addP zeroP p) p = true)
                                               → (∀ p : P,
                                                 eqP (addP p zeroP) p = true)
                                                 → 
						 (* This is idempotence *)
                                                 (∀ x y : P, eqP x y = true
                                                 → 
                                                 eqP (addP x y) y = true)
                                                 → 
                                                 ∀ X : finite_set (A * P),
                                                 eqSAP A P eqA eqP
                                                 (uop_manger_phase_2 lteA
                                                 (uop_manger_phase_1 eqA addP
                                                 X))
                                                 (uop_manger_phase_1 eqA addP
                                                 (uop_manger_phase_2 lteA X)) =
                                                 true