; Succeeded tests
; ⊕ flatten, idempotency, neultral elements, falsification
;(traces Process-red (term (⊕ e_1  e_1 )))  ;OK
;(traces Process-red (term (⊕ e  t )))  ;OK
;(traces Process-red (term (⊕ e e t e_0 t e t e_2 e_3 t e e_4 t))) 
;(traces Process-red (term (⊕ e_0 (¬ e) t e_2 e_3 t e e_4))) 
;(traces Process-red (term (⊕ e_0 e_1 e_2 t (¬ e_1) t))) 
;(traces Process-red (term (⊕ e_1 e_2 e_3 t))) 
;(traces Process-red (term (⊕ e_1 e_2 e_3 f))) 
;(traces Process-red (term (⊕ f e_1 e_2 e_3 ))) 
;(traces Process-red (term (⊕ t e_1 f e_2 e_3 )))
;(traces Process-red (term (⊕ t e_2  t e_3 e_4 t))) 
;(traces Process-red (term (⊕ e_1 f (¬ e_2) e_3 )))
;(traces Process-red (term (⊕ e_1 (¬ e_2) e_2 e_3 e_3 )))
;(traces Process-red (term (⊕ e_1 (¬ e_2) e_2 e_3 ))) 
;(traces Process-red (term (⊕ e_1 e_2 (⊕ e_2  e_3))))

;distributivity
;(traces Process-red (term (⊕ e_0 (e_2 ⊥ e_3)))) 
;(traces Process-red (term (⊕ (e_2 ⊥ e_3) e_1))) 
;(traces Process-red (term (⊕ e_0 t e_1 ( ⊥ e_2 e_3 e_4 e_5 e_6 e_7))))  
;(traces Process-red (term (⊥ e_1  (⊕ e_1  e_2))))  
;(traces Process-red (term (⊥ e_1  (⊕ e_1 (⊥ e_2 (⊕ e_2  e_3))))))
;(traces Process-red (term (⊥ e_1  (⊕ e_1 (⊕ e_2 (⊕ e_2  e_3))))))
;(traces Process-red (term (⊥ e_1 e_2 (⊥ e_2  e_3) e_3 (⊥ e_3  e_4)))) 

; metafunction
;(term (δ (⊕ e_2 e_1 e_5 e_0 e_7 e_8 e_3))) 

;⊥ flatten, idempotency, neultral elements
;(traces Process-red (term (⊥ e_1 e_2 e_3 t))) 
;(traces Process-red (term (⊥ e_1 e_2 e_3 f))) 
;(traces Process-red (term (⊥ f e_1 e_2 e_3 ))) 
;(traces Process-red (term (⊥ e_1 f e_2 f e_3 )))






; Theorem of maximality
;(term (µ (⊥ (⊕ e_5 (¬ e_6)) (⊕ e_1 e_2 e_3)(⊕ e_7 e_8)(⊕ e_1 (¬ e_2))(⊕ (¬ e_2) e_10))))  
;(term (µ (⊥ (⊕ e_1 (¬ e_2)  (⊕ e_2  e_3))  (⊕ e_1  (⊕ (¬ e_2)  (⊕(¬ e_2)  e_3)))))) marche pas
;(term (µ (⊥ (⊕ e_1 (¬ e_2))  (⊕ e_1  (⊕ (¬ e_2)  (⊕(¬ e_2)  e_3)))))) ;OK au double plus pres
;(term (µ (⊥ (⊕ e_1 (¬ e_2))  (⊕ e_1   e_2))))

; maximal absorption
;(traces Process-red (term  (⊥ (⊕ e_1  e_3) e_1 e_4))) 
;(traces Process-red (term  (⊥ e_0 (⊕ e_5 e_6) (⊕ e_1  e_2 e_3) (⊕ e_1 e_2) e_4))) 
;(traces Process-red (term  (⊥ e_1  (⊕ e_5 e_6) (⊕ e_1 e_2) (⊕ e_1  e_2 e_3) e_4))) 

;(traces Process-red (term  (⊕ e_8 t (⊕ e_1 t  (⊕ (¬ e_2) (⊕ e_2  t e_3))) (⊕ e_1  (⊕ (¬ e_4)  (⊕ e_2 t e_3))) e_9)  )) 
;(traces Process-red (term  (⊥ (⊥ e_1 (¬ e_2)  e_2  (e_3 ⊥d e_1)  (¬ e_2)  (¬ e_2)  e_3) e_1))) 
;(traces Process-red (term (⊥ (⊕ e_3  (¬ e_2) e_2  e_3) (⊕ e_1  (¬ e_2) (¬ e_2) e_3) (⊕ (¬ e_1)  e_2 e_2  (¬ e_3)) (⊕ (¬ e_1) e_2  (¬ e_2)  e_3)))) 

;(traces Process-red (term (⊕ (e_1 ⊥d e_2)  (e_2 ⊥d e_3) (e_3 ⊥d e_4) )))

; flatten idempotency, neutral element and lexicographical order 
;(traces Process-red (term (⊕(⊕ e_1 e_9) t  f (⊕ e_2 t  e_3 (⊕ e_8 t  e_3  e_10 ))  )))
;(traces Process-red (term (⊥ e_1 (⊥ e_1 e_9)  (⊥ e_8  e_3  e_10 ))  ))
; Conflicts
;(traces Process-red (term (⊕ (e_1 ⊥d e_2)  (⊕ t  e_1)))) 
;(traces Process-red (term (⊥ e_1 e_2 e_3 e_4 e_5))) 
;(traces Process-red (term (⊥ e_1 e_2))) 
;(traces Process-red (term (⊕ e_1 e_2 e_3))) 
;(traces Process-red (term (⊕ b_1 b_2 b_3 (b_2 ≺ (⊥ e_3 e_2))(b_3 ≺ e_6) (b_6 ≺ e_7)))) 
;(traces Process-red (term (⊕ b_1 b_2 b_3 (b_2 ≺ (⊥ e_3 e_2)) (e_2 ≺ b_6) (e_6 ≺ b_7) (b_7 ≺ e_7) (e_4 ≺ b_5)(b_5 ≺ e_5) (b_3 ≺ e_6)   )))
;(traces Process-red (term (⊕ b_1 b_2 b_3 (b_2 ≺ (⊥ e_3 e_2))(e_2 ≺ b_6) (e_6 ≺ b_7) (b_7 ≺ e_7) (e_4 ≺ b_5)(b_5 ≺ e_5) (b_3 ≺ e_6) (e_2 ≺ b_6) (e_6 ≺ b_7) (b_7 ≺ e_7) (e_4 ≺ b_5) (b_5 ≺ e_5)  )))

(traces Process-red (term (⊕ b_1 b_2 b_3 (b_2 ≺ (⊥ e_3 e_2)) (b_1 ≺ e_1)(e_1 ≺ b_4) (e_2 ≺ b_6) (e_6 ≺ b_7) (b_7 ≺ e_7) (e_4 ≺ b_5)(b_5 ≺ e_5)(b_3 ≺ (⊥ e_4 e_6))((⊕ b_3 b_6) ≺ e_6)   ((⊕ b_3 b_4) ≺ e_4) ))) ;OK marche reste a faire marcher les distributivités