CIS 301. Computing based on the distributivity law.

function DIST(eta1,eta2)

 precondition: eta1 and eta2 are in cnf (C) with generating gammar 
 L ::= p |  p 
 D ::= L | L  D 
 C ::= D | D  C 

 postcondition: DIST(eta1,eta2) computes a cnf for eta1  eta2 

  begin function
	case
	  eta1 is eta11  eta12 : return DIST(eta11,eta2)  DIST(eta12,eta2)
	  eta2 is eta21  eta22 : return DIST(eta1,eta21)  DIST(eta1,eta22)
	  otherwise (= no conjunctions) : return eta1  eta2
	end case
  end function

 If eta1 is a conjunction, then we apply the distributivity law	    
 (eta11  eta12)  eta2 ==> (eta11  eta2)  (eta12  eta2), but we have  
 to interpret the "" as calls to DIST as well, for the same reason why   
 we needed that subroutine to begin with.				    

 The second case is symmetric; now eta2 is a conjunction. Notice that	    
 the algorithm executes the FIRST case statement whose condition is true. 
 Thus, if eta1 and eta2 are conjunctions, the first clause applies. This  
 guarantees that the algorithm is DETERMINISTIC.			    

 If neither eta1 nor eta2 are conjunctions, then they have to be literals 
 as the algorithm's precondition ensures that both are in cnf. Thus,      
 their disjunction is a cnf by definition, so we may return just that.    

 negation normal form;
 conjunctive normal form.