Exercices 4a

6. Extends the propositional language with conjunction (And).
   The new construct needs new rewriting rules called "split" and "destruct" (see below for full code):

let split            (hs,(And(p,q))::ps)       = (hs,p::q::ps);;
let destruct h h1 h2 ([...;h:And(p,q);...],ps) = ([h1:p;h2:q;...],ps);;

"split" says that if 2 facts has to be demonstrated then we have to prove each ones.
"destruct" says that if an hypothesis admits 2 things then each one can be admit individually.

Proof trees

Code for deduction rules

let split ((hs,p::ps):Seq):Seq = 
 match p with
 | And (p1,p2) -> (hs,p1::p2::ps)
 | _           -> (hs,p::ps);;

let destruct h h1 h2 (hs,ps) = 
 let v = List.filter (fun (k,r)->k=h) hs
 match v with
 | (_,And (p1,p2))::_ -> ((h1,p1)::(h2,p2)::hs,ps)
 | _                  -> (hs,ps);;

let (&&&) p1 p2 = And (p1,p2);;
let p = (A &&& B) ===> (B &&& C);;

7 - 12