let rec appartenance f = function
   [] -> false
   | t::_ when t=f -> true
   | _::queue -> appartenance f queue ;;

let ajout f e =
   if appartenance f e then
      e
   else
      f::e ;;

let rec ajoutbis f e = match e with
   [] -> [f]
   | t::queue -> if f=t then
                     e
                  else
                     t::ajoutbis f queue ;;

let rec inclusion e1 e2 = match e1 with
   [] -> true
   | t::queue -> if appartenance t e2 then
                    inclusion queue e2
                 else
                    false;;


let egalite e1 e2 =
   if inclusion e1 e2 then
      inclusion e2 e1
   else
      false;;


let rec soustraction e1 e2 = match e1 with
   [] -> [] 
   | t::queue -> if appartenance t e2 then
                    soustraction queue e2
                 else
                    t::soustraction queue e2;;

let rec union e1 e2 = match e1 with
   [] -> e2 
   | t::queue -> if appartenance t e2 then
                    union queue e2
                 else
                    t::union queue e2;;
                    
let rec intersection e1 e2 = match e1 with
   [] -> [] 
   | t::queue -> if appartenance t e2 then
                    t::intersection queue e2
                 else
                    intersection queue e2;;

let comparaison (h1,c1) (h2,c2) =
   if egalite h1 h2 then
      egalite c1 c2
   else
      false;;

let rec appartenanceB gamma omega = match omega with
   [] -> false
   | gamma1::queue -> if comparaison gamma gamma1 then
                         true
                      else
                         appartenanceB gamma queue ;;

let ajoutB gamma omega =
   if appartenanceB gamma omega then
      omega
   else
      gamma::omega ;;


let rec inclusionB omega1 omega2 = match omega1 with
   [] -> true
   | t::queue -> if appartenanceB t omega2 then
                    inclusionB queue omega2
                 else
                    false;;


let egaliteB omega1 omega2 =
   if inclusionB omega1 omega2 then
      inclusionB omega2 omega1
   else
      false;;


let rec soustractionB omega1 omega2 = match omega1 with
   [] -> [] 
   | t::queue -> if appartenanceB t omega2 then
                    soustractionB queue omega2
                 else
                    t::soustractionB queue omega2;;

let rec unionB omega1 omega2 = match omega1 with
   [] -> omega2 
   | t::queue -> if appartenance t omega2 then
                    unionB queue omega2
                 else
                    t::unionB queue omega2;;
                    
let rec intersectionB omega1 omega2 = match omega1 with
   [] -> [] 
   | t::queue -> if appartenanceB t omega2 then
                    t::intersectionB queue omega2
                 else
                    intersectionB queue omega2;;


                    

let rec tautologie (h,c)=match h with
   []->false
   | f::queue -> if appartenance f  c then
                    true
                 else
                    tautologie (queue,c);;
                       

                    
                    
let rec elimination = function
   [] -> []
   | gamma::queue -> if tautologie gamma then
                        elimination queue
                     else
                        gamma::elimination queue;;


let rec absorbable (h,c) = function
   [] -> false
   | (h1,c1)::queue -> if  inclusion h1 h  & inclusion c1 c then
                          true
                       else
                          absorbable (h,c) queue;;
                          
let rec calcul omega1 = function
   [] -> omega1
   | gamma::queue -> if absorbable gamma omega1 or absorbable gamma queue then
                        calcul omega1 queue
                     else
                        calcul (gamma::omega1) queue;;
                        
let minimisation omega = calcul [] omega;;                        
                              
let rec construction (h1,c1) (h2,c2) = function
   [] -> [] 
   | f::e -> let h = union (soustraction h1 [f]) h2 in
             let c = union c1 (soustraction c2 [f]) in
             ajoutB  (h,c) (construction (h1,c1) (h2,c2) e);;


let triangle (h1,c1) (h2,c2) = let e=intersection h1 c2 in
   construction (h1,c1) (h2,c2) e;;


let triangle_s (h1,c1) (h2,c2) = match intersection h1 c2 with
        f::[] -> [union (soustraction h1 [f]) h2, union c1 (soustraction c2 [f])]
        |_->[];;

let rec composition (h1,c1) = function
   [] -> []
   | (h2,c2)::queue -> let omega1 = triangle (h1,c1) (h2,c2) in
                       let omega2 = triangle (h2,c2) (h1,c1) in
                       unionB (unionB omega1 omega2) (composition (h1,c1) queue);;

let rec composition_s (h1,c1) = function
   [] -> []
   | (h2,c2)::queue -> let omega1 = triangle_s (h1,c1) (h2,c2) in
                       let omega2 = triangle_s (h2,c2) (h1,c1) in
                       unionB (unionB omega1 omega2) (composition_s (h1,c1) queue);;

   
let rec deduction = function
   [] -> []
   | gamma::queue ->  ajoutB gamma (unionB (deduction queue) (composition gamma queue));;

let rec deduction_s = function
   [] -> []
   | gamma::queue ->  ajoutB gamma (unionB (deduction_s queue) (composition_s gamma queue));;


let completion omega = 
   let rec construire omega1 = function
      []-> omega1
      | gamma::queue -> let omega3=ajoutB gamma omega1 in
                        let nouveaux = soustractionB (composition gamma omega1) omega3 in
                           construire omega3 (unionB queue nouveaux)
   in construire [] omega ;;
                          

   
let interrogation V F Omega =
   let rec integration = function 
     [] -> []
     | (H,C)::queue -> (soustraction H V,soustraction C F)::integration queue in
   minimisation (integration (elimination (minimisation (completion Omega)))) ;;