(*
 * Description:
 *
 * Copyright (c) 2000 by
 *  David Blei			blei@cs.berkeley.edu
 *  Chris Harrelson		chrishtr@cs.berkeley.edu
 *  Ranjit Jhala		jhala@cs.berkeley.edu
 *  Rupak Majumdar		rupak@cs.berkeley.edu
 *  George C. Necula	necula@cs.berkeley.edu
 *  Shree P. Rahul		sprahul@cs.berkeley.edu
 * 	Wes Weimer			weimer@cs.berkeley.edu
 *  Dror Weitz			dror@cs.berkeley.edu
 *   
 * All rights reserved.  Permission to use, copy, modify and distribute
 * this software for research purposes only is hereby granted, 
 * provided that the following conditions are met: 
 * 1.  Redistributions of source code must retain the above copyright notice, 
 * this list of conditions and the following disclaimer. 
 * 2. Redistributions in binary form must reproduce the above copyright notice, 
 * this list of conditions and the following disclaimer in the documentation 
 * and/or other materials provided with the distribution. 
 * 3. The name of the authors may not be used to endorse or promote products derived from 
 * this software without specific prior written permission. 
 *
 * DISCLAIMER:
 * THIS SOFTWARE IS PROVIDED BY THE AUTHORS ``AS IS'' AND ANY EXPRESS OR IMPLIED 
 * WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF 
 * MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. 
 * IN NO EVENT SHALL THE AUTHORS BE LIABLE FOR ANY DIRECT, INDIRECT, 
 * INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, 
 * BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS 
 * OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY 
 * THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT 
 * (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF 
 * THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
 *
 *)
open Pretty
module E = Errormsg
module I = Input


(* In order to maintain a compact representation of proofs we represent a 
 * proof node as the name of the axiom along with a list of arguments. An 
 * exception is made for the hypothetical and parametric proof nodes. *)
type parg = 
    I of int                            (* An integer argument *)
  | E of I.exp                          (* An expression argument *)
  | P of proof                          (* A subproof *)
  | F of I.pred                         (* A predicate argument *)

and proof = 
    Hyp of Input.var                    (* A hypothesis, 
                                           introduced with Impi*) 
  | Alli of Input.var * proof
  | Impi of Input.var * Input.pred * proof (* bind var to a hypothetical 
                                            * proof of the pred. The last 
                                            * argument is a proof of the 
                                            * right hand side, possibly 
                                            * refering to var *)

                                        (* Bind var to a proof of the 
                                         * negation of pred. The second 
                                         * argument is a proof of false *)
  | Contra of Input.var * Input.atom * proof

  | G of string * parg list             (* This is a generic proof 
                                         * constructor *)
  | Unimplemented                       (* We'll expand the proof language as 
                                         * needed in the future. Use 
                                         * Unimplemented until then *)


(***** Pretty printing *****)
exception ProofCheck of proof;;

let rec dp () = function
    Hyp v -> text v
  | Impi(v,p1,d2) -> 
      if !I.printLFSyntax then
        dprintf "(impi @[[%s : pf %a]@?%a@])" v I.dp p1 dp d2
      else
        dprintf "impi(@[%s : %a,@?%a@])" v I.dp p1 dp d2
        
  | Alli(v,d) -> 
      if !I.printLFSyntax then
        dprintf "(alli @[([%s : exp]@!%a@])" v dp d
      else
        dprintf "alli(@[%s.\n@]%a)" v dp d
        
  | Contra(v,a,d) ->  begin
      let preamble = 
        match a with
          I.Eq(e1,e2) -> dprintf "= %a %a" I.de e1 I.de e2
        | I.Neq(e1,e2) -> dprintf "<> %a %a" I.de e1 I.de e2
        | I.Lt(e1,e2) -> dprintf "< %a %a" I.de e1 I.de e2
        | I.Leq(e1,e2) -> dprintf "<= %a %a" I.de e1 I.de e2
        | I.Gt(e1,e2) -> dprintf "> %a %a" I.de e1 I.de e2
        | I.Geq(e1,e2) -> dprintf ">= %a %a" I.de e1 I.de e2
        | I.BFun(n,args) -> dprintf " %a" I.da a
        | I.NotBFun _ -> E.s (E.unimp "Unsupported contradiction proof")
      in
      dprintf "(con@[tra%a ([%s : pf _]@! %a@]))" insert preamble v dp d
  end
 
  | G(name, args) ->
      if 0 = List.length args then
        text name
      else
        if !I.printLFSyntax then
          dprintf "(%s @[%a@])" name (docList break dpa) args
        else
          dprintf "%s(@[%a@])" name (docList (chr ',' ++ break) dpa) args
  | _ -> E.s (E.unimp "Proof.dp")

and dpa = function
    I(i) -> num i
  | E(e) -> I.de () e
  | F(p) -> I.dp () p
  | P(d) -> dp () d

(* begin circular dependency hack: *)

let simp_and_subtract_is_zero = ref (function a -> function b-> (failwith "bug in proof.infer #1"))
let simp_and_subtract_is_at_least_zero = ref (function a -> function b -> (failwith "bug in proof.infer #2"))

(* end circular dependency hack *)
(* Jhala: Function to check the equality of two lists !! *)

let eqList l1 l2 = (l1 = l2)
      
	
(****** Type inference *****)
let rec infer vars hyps d = 
  let rec i d = 
    match d with  
	G("truei", []) -> I.True
    | G("andi",  [P d1; P d2]) -> I.And(i d1, i d2)
    | G("andel", [P d]) -> begin
        match i d with
          I.And(p1,_) -> p1
        | _ -> raise (ProofCheck d)
    end
    | G("ander", [P d]) -> begin
        match i d with
          I.And(_,p2) -> p2
        | _ -> raise (ProofCheck d)
    end
    | Alli(v,d) -> I.All(v, infer (v :: vars) hyps d)
    | Impi(v,p1,d2) -> I.Imp(p1, infer vars ((v,p1) :: hyps) d2)
    | Contra(v,a,dd) -> begin
		    let result = infer vars ((v, I.Atom (I.negate a)) :: hyps) dd in
				match result with
          I.False -> I.Atom a
        | _ -> 
					ignore (printf "Proof.Infer:Contra: got %a\n" Input.dp result) ;
					raise (ProofCheck d)
    end
    | (Hyp v) as d -> begin
        try 
          let (_, p) = List.find (fun (v',_) -> v = v') hyps in
          p
        with Not_found -> raise (ProofCheck d)
    end

	(* general contradiction *)

    (* false elimination *)
    | G("falsee", [ F p ; P pff ]) -> begin
        match i pff with
        I.False -> p
    |   _ -> raise (ProofCheck d)
    end


	  (* arithmetic axioms *)
    | G("geq0", []) -> I.Atom (I.Geq (I.Int 0, I.Int 0))
    | G("eqi", [P d1; P d2]) -> begin
	match (i d1, i d2) with
	  (I.Atom (I.Geq (e1,e2)), I.Atom (I.Geq (e_2, e_1))) ->
	    if (e1 = e_1) && (e2 = e_2) then
	      I.Atom (I.Eq (e1,e2))
	    else 
	      raise (ProofCheck d)
	| _ -> raise (ProofCheck d)
    end
    | G("eqgeq", [P d1]) -> begin
	match i d1 with
	  I.Atom (I.Eq (e1,e2)) -> I.Atom (I.Geq (e1,e2))
	| _ -> raise (ProofCheck d)
    end
    | G("eqgeqr", [P d1]) -> begin
	match i d1 with
	  I.Atom (I.Eq (e1,e2)) -> I.Atom (I.Geq (e2,e1))
	| _ -> raise (ProofCheck d)
    end
    | G("ltgeq", [P d1]) -> begin
	match i d1 with
	  I.Atom (I.Lt (e1,e2)) -> I.Atom (I.Geq (e2, I.Plus (e1, I.Int 1)))
	| _ -> raise (ProofCheck d)
    end
    | G("leqgeq", [P d1]) -> begin
	match i d1 with
	  I.Atom (I.Leq (e1,e2)) -> I.Atom (I.Geq (e2,e1))
	| _ -> raise (ProofCheck d)
    end
    | G("gtgeq", [P d1]) -> begin
	match i d1 with
	  I.Atom (I.Gt (e1,e2)) -> I.Atom (I.Geq (e1, I.Plus (e2, I.Int 1)))
	| _ -> raise (ProofCheck d)
    end
    | G("geq*>=", [I n; P d1; P d2]) -> begin
	match (i d1, i d2) with
	  (I.Atom (I.Geq (e1,e2)), I.Atom (I.Geq (e_1,e_2))) ->
	    I.Atom (I.Geq (I.Plus (I.Times (I.Int n, e1), e_1), I.Plus (I.Times (I.Int n, e2), e_2)))
	| _ -> raise (ProofCheck d)
    end
    | G("geq*i", [P d1; P d2]) -> begin
	match i d1 with
	  I.Atom (I.Eq (I.Plus (I.Times (I.Int n, I.Minus (e1,e2)), I.Minus (I.Int r, I.Int 1)), I.Minus (e_1, e_2))) ->
	    if n>=r && n>= 1 then begin
	      match i d2 with
		I.Atom (I.Geq (f1,f2)) ->
(*
            let _ = Pretty.printf "e_1 = %a\n" Input.de e_1 and
                _ = Pretty.printf "f1 = %a\n" Input.de f1 and
                _ = Pretty.printf "e_2 = %a\n" Input.de e_2 and
                _ = Pretty.printf "f2 = %a\n" Input.de f2 in
*)
		  if (e_1 = f1) && (e_2 = f2) then
		    I.Atom (I.Geq (e1,e2))
		  else
		    raise (ProofCheck d)
	      |	_ -> raise (ProofCheck d)
	    end
	    else
	      raise (ProofCheck d)
	| _ -> raise (ProofCheck d)
    end
	| G("noInt_FI", [P d1; P d2]) -> begin
		let noIntInInterval (an,ad, bn,bd) = (* no integer in the interval [cc/c; bb/b]  *)
			let lower = Num.div_num (Num.num_of_int an) (Num.num_of_int ad)
			and upper = Num.div_num (Num.num_of_int bn) (Num.num_of_int bd)
			in  (Num.eq_num (Num.floor_num lower) (Num.floor_num upper)) && 
				(Num.eq_num (Num.ceiling_num lower) (Num.ceiling_num upper)) &&
            	(not(Num.is_integer_num lower) && not(Num.is_integer_num upper))
		in
	match (i d1, i d2) with
	  (I.Atom (I.Geq (I.Times (I.Int c, e1), Input.Int cc)), I.Atom (I.Geq (Input.Int bb, I.Times (I.Int b, e2)))) -> 
	    if (e1 = e2) && (noIntInInterval(cc,c,bb,b)) then
	      I.False
	    else 
	      raise (ProofCheck d)
	  | (I.Atom (I.Geq (I.Times (e1, I.Int c), Input.Int cc)), I.Atom (I.Geq (Input.Int bb, I.Times (e2, I.Int b)))) ->
	    if (e1 = e2) && (noIntInInterval(cc,c,bb,b)) then
	      I.False
	    else 
	      raise (ProofCheck d)
	| _ -> raise (ProofCheck d)
	end
	| G("pathSplit_FI", [P d1; P d2; P d3]) -> begin
(*
	let _ = Pretty.printf "pathSplit_FI: LHS = %a\n" I.dp (i d1) and
	_ = Pretty.printf "pathSplit_FI: LHS = %a\n" I.dp (i d2) and
	_ = Pretty.printf "pathSplit_FI: RHS = %a\n" I.dp (i d3) in
*)
		match i d1 with
			I.Atom (I.Neq (c1, c2)) -> begin
				match (i d2, i d3) with
					(I.Imp(I.Atom(I.Geq(I.Minus(e1, I.Plus(e2, I.Int 1)), I.Int 0)),I.False) , 
					 I.Imp(I.Atom(I.Geq(I.Minus(f1, I.Plus(f2, I.Int 1)), I.Int 0)),I.False)) -> 
							if(c1 = e1 && e1 = f2 && e2 = f1 && c2 = e2) then
								I.False
							else raise (ProofCheck d)
				| _ -> raise (ProofCheck d)
			end
		| _ -> raise (ProofCheck d)
	end
    | G("geqLt_FI", [P d1; P d2]) -> begin
(*
	let _ = Pretty.printf "geqLt_FI: LHS = %a\n" I.dp (i d1) and
	_ = Pretty.printf "geqLt_FI: RHS = %a\n" I.dp (i d2) in
*)
	match (i d1, i d2) with
	  (I.Atom (I.Geq (e1,e2)), I.Atom (I.Geq (e_2, I.Plus (e_1, I.Int 1)))) ->
	    if (e1 = e_1) && (e2 = e_2) then
	      I.False
	    else 
	      raise (ProofCheck d)
	| _ -> raise (ProofCheck d)
    end
    | G ("eqCheck", [E e1; E e2]) ->
	if (!simp_and_subtract_is_zero) e1 e2 then
	  I.Atom (I.Eq (e1, e2))
	else
	  raise (ProofCheck d)
    | G ("geqCheck", [E e1; E e2]) ->
	if (!simp_and_subtract_is_at_least_zero) e1 e2 then
	  I.Atom (I.Geq (e1, e2))
	else
	  raise (ProofCheck d)
	        (* arithmetic ends *)
	    (* Congruence begins *)
    | G ("not_FI",[P p1; P p2]) ->
	( match ((i p1),(i p2)) with
		(I.Atom (I.Eq (e1,e2)),I.Atom (I.Neq (e3,e4))) ->
			if (e1 = e3) & (e2 = e4) then I.False
	    else (ignore (E.warn "not_FI.Eq not right") ; raise (ProofCheck d))
		| (I.Atom (I.Geq (e1,e2)),I.Atom (I.Lt (e3,e4))) ->
		  if (e1 = e3) & (e2 = e4) then I.False
	    else (ignore (E.warn "not_FI.Geq/Lt not right") ; raise (ProofCheck d))

	  | (I.Atom (I.BFun (f1,l1)),I.Atom (I.NotBFun (f2,l2))) ->
	    if (f1 = f2 ) & (l1 = l2) then I.False
	    else (
				(if (f1 <> f2) then (ignore (E.warn "Proof.Infer:not_FI: %s =?= %s\n" f1 f2))) ;
				(if (l1 <> l2) then (ignore (E.warn "Proof.Infer:not_FI: arg lists for %s:@!%a@!%a" f1 (docList (chr ',' ++ break) (I.de ())) l1 (docList (chr ',' ++ break) (I.de ())) l2
				))) ;
	      (ignore (E.warn "Proof: not_FI:BFun Proof.infer says invalid proof:@!%a\n" dp (G ("not_FI",[P p1; P p2]))); raise (ProofCheck d) ) 
				)
		| _ -> (ignore (E.warn "Proof: not_FI: ???\n"); raise (ProofCheck d) )
	      )
    | G ("eqNeq_FI",[P p1;P p2]) ->
	(
	match ((i p1),(i p2)) with
	  (I.Atom (I.Eq (e1,e2)),I.Atom (I.Neq (e3,e4))) ->
	    if (e1 = e3) & (e2 = e4) then I.False
	    else
	      (ignore (E.warn "eqNeq_FI:Eq  Proof.infer says %a is not a valid proof" dp (G ("eqNeq_FI",[P p1;P p2])));
		
	       raise (ProofCheck d) )
		
	| (I.Atom (I.BFun (f1,l1)),I.Atom (I.NotBFun (f2,l2))) -> (
	    
	      if (f1 = f2 ) & (l1 = l2) then I.False
	      else
		(ignore (E.warn "eqNeq_FI:BFun Proof.infer says %a is not a valid proof" dp (G ("eqNeq_FI",[P p1;P p2])));raise (ProofCheck d) )
	    	  )
	| _ -> 	(ignore (E.warn "eqNeq_FI: ??? invalid use of axiom! in %a" dp (G ("eqNeq_FI",[P p1;P p2]))); raise (ProofCheck d))
		  )
 (*[Jhala: Note that boolean equalities should never be used for a contra proof] *)	  
    | G ("=id",[E e]) -> I.Atom(I.Eq (e,e))
    | G ("b=id",[F (I.Atom a)]) -> I.Atom(I.Beq (a,a))
    | G ("=sym",[P p]) ->
	(
	match i p with
	  I.Atom (I.Eq (e1,e2)) -> I.Atom (I.Eq (e2,e1))
	| _ -> (ignore (E.warn "=sym: invalid use of axiom! in %a" dp (G ("=sym",[P p]))); raise (ProofCheck d))
	      )
    | G ("b=sym",[P p]) ->
	(
	match i p with
	  I.Atom (I.Beq (e1,e2)) -> I.Atom (I.Beq (e2,e1))
	| _ -> (ignore (E.warn "b=sym: invalid use of axiom! in %a" dp (G ("=sym",[P p]))); raise (ProofCheck d))
	      )  
    | G ("=tr",[P p1;P p2]) -> (
	match (i p1,i p2) with
	  (I.Atom (I.Eq (e1,e2)),I.Atom (I.Eq (e3,e4))) ->
	    if e2 = e3 then I.Atom (I.Eq (e1,e4))
	    else (ignore (E.warn "=tr: invalid use of axiom! in %a" dp (G ("=tr",[P p1;P p2]))); raise (ProofCheck d))
	| _ -> (ignore (E.warn "=tr: invalid use of axiom! in %a" dp (G ("=tr",[P p1;P p2]))); raise (ProofCheck d))
	      )
    | G ("b=tr",[P p1;P p2]) -> (
	match (i p1,i p2) with
	  (I.Atom (I.Beq (e1,e2)),I.Atom (I.Beq (e3,e4))) ->
	    if e2 = e3 then I.Atom (I.Beq (e1,e4))
	    else (ignore (E.warn "b=tr: invalid use of axiom! in %a" dp (G ("b=tr",[P p1;P p2]))); raise (ProofCheck d))
	| _ -> (ignore (E.warn "b=tr: invalid use of axiom! in %a" dp (G ("b=tr",[P p1;P p2]))); raise (ProofCheck d))
	      )
    (* [Jhala: My little cheat ...] *)
    | G ("cong", (e1::e2::ls)) -> 
	let argCheck a1 a2 = I.Atom (I.Eq (a1,a2)) in
	let deParg x =
	  match x with
	    P p -> p
	  | _ -> E.s (E.bug "Proof: Invalid Call to deParg")
	in
	let congCheckAtom a1 a2 pl = 
	  let l = List.map deParg pl in
	  (match (a1,a2) with
	    (I.Beq (a11,a12), I.Beq (a21,a22)) ->
	      ignore (E.warn "Proof: [Jhala CC] Congruence on Beq !!"); eqList [I.Atom (I.Beq (a11,a21));I.Atom (I.Beq (a12,a22))]  (List.map i l)
	  | (I.Eq (e11,e12), I.Eq (e21,e22)) -> eqList [I.Atom (I.Eq (e11,e21));I.Atom (I.Eq (e12,e22))] (List.map i l)
	  | (I.Neq (e11,e12), I.Neq (e21,e22)) -> eqList [I.Atom (I.Eq (e11,e21));I.Atom (I.Eq (e12,e22))] (List.map i l)
	  | (I.Geq (e11,e12), I.Geq (e21,e22)) -> eqList [I.Atom (I.Eq (e11,e21));I.Atom (I.Eq (e12,e22))] (List.map i l)
	  | (I.Gt (e11,e12), I.Gt (e21,e22)) -> eqList [I.Atom (I.Eq (e11,e21));I.Atom (I.Eq (e12,e22))] (List.map i l)
	  | (I.Leq (e11,e12), I.Leq (e21,e22)) -> eqList [I.Atom (I.Eq (e11,e21));I.Atom (I.Eq (e12,e22))] (List.map i l)
	  | (I.Lt (e11,e12), I.Lt (e21,e22)) -> eqList [I.Atom (I.Eq (e11,e21));I.Atom (I.Eq (e12,e22))] (List.map i l)
	  | (I.BFun (f1,arg1), I.BFun (f2,arg2)) ->
	      (try
		(f1 = f2) & (eqList (List.map2 argCheck arg1 arg2) (List.map i l))
	      with
		Invalid_argument _ -> false)
	  | (I.NotBFun (f1,arg1), I.NotBFun (f2,arg2)) ->
	      (try
		(f1 = f2) & (eqList (List.map2 argCheck arg1 arg2) (List.map i l))
	      with
		Invalid_argument _ -> false)
	  | _ -> false)

	in
	let congCheckExp e1 e2 pl =
	  let l = List.map deParg pl in
	  (match (e1,e2) with
	    (I.Var(x),I.Var(y)) -> ignore (E.warn "Proof: congCheckExp with Var !!"); x=y
	  | (I.Int(x),I.Int(y)) -> ignore (E.warn "Proof: congCheckExp with Int !!"); x=y
	  | (I.Plus(e11,e12),I.Plus(e21,e22)) -> eqList [(argCheck e11 e21);(argCheck e12 e22)] (List.map i l)
	  | (I.Minus(e11,e12),I.Minus(e21,e22)) -> eqList [(argCheck e11 e21);(argCheck e12 e22)] (List.map i l)
	  | (I.Times(e11,e12),I.Times(e21,e22)) -> eqList [(argCheck e11 e21);(argCheck e12 e22)] (List.map i l)
	  | (I.Div(e11,e12),I.Div(e21,e22)) -> (eqList [(argCheck e12 e22)] (List.map i l)) & (e11=e21)
	  | (I.Mod(e11,e12),I.Mod(e21,e22)) -> (eqList [(argCheck e12 e22)] (List.map i l)) & (e11=e21)
	  | (I.Floor(e11,e12),I.Floor(e21,e22)) -> (eqList [(argCheck e12 e22)] (List.map i l)) & (e11=e21)
	  | (I.Ceil(e11,e12),I.Ceil(e21,e22)) -> (eqList [(argCheck e12 e22)] (List.map i l)) & (e11=e21)
	  | (I.Fun (f1,arg1), I.Fun (f2,arg2)) ->
	      (try
		(f1 = f2) & (eqList (List.map2 argCheck arg1 arg2) (List.map i l))
	      with
		Invalid_argument _ -> false)
	  | _ -> false)
		
	in 
	(match (e1,e2) with 
	  (F (I.Atom a),F (I.Atom b)) ->
	    if (congCheckAtom a b ls) then  I.Atom(I.Beq (a,b)) else (ignore (E.warn "Proof: cong: Atom invalid use of axiom! in %a" dp (G ("cong", (e1::e2::ls)))); raise (ProofCheck d))
	| (E e11,E e22) ->
	    if (congCheckExp e11 e22 ls) then I.Atom(I.Eq (e11,e22)) else (ignore (E.warn "Proof: cong: Exp invalid use of axiom! in %a" dp (G ("cong", (e1::e2::ls)))); raise (ProofCheck d))
	| _ -> (ignore (E.warn "Proof: cong: ??? invalid use of axiom! in %a" dp (G ("cong", (e1::e2::ls)))); raise (ProofCheck d))
	      )
	    
    | G ("bIffMP",[P p1; P p2]) -> (
	match ((i p1),(i p2)) with
	  (I.Atom a, I.Atom (I.Beq(a1,a2))) -> if a=a1 then (I.Atom a2) else (ignore (E.warn "Proof: bIffMP: Invalid use of axiom! in %a" dp (G ("bIffMP",[P p1; P p2]))); raise (ProofCheck d))
	| _ -> (ignore (E.warn "Proof: bIffMP ???: Invalid use of axiom! in %a" dp (G ("bIffMP",[P p1; P p2]))); raise (ProofCheck d))
     )

    | G ("bIff_NotBFun",[P p1; P p2]) ->
	(match ((i p1),(i p2)) with
	  (I.Atom (I.NotBFun (f,args)),I.Atom (I.Beq (I.BFun (f1,args1), I.BFun (f2,args2)))) ->
	    if (f = f1) & (f=f2) & (args = args1) then (I.Atom (I.NotBFun (f2,args2)))
	    else (ignore (E.warn "Proof: bIff_NotBFun: Invalid use of axiom! in %a" dp (G ("bIffMP",[P p1; P p2]))); raise (ProofCheck d))
	|  _ -> (ignore (E.warn "Proof: bIff_NotBFun: ??? Invalid use of axiom! in %a" dp (G ("bIffMP",[P p1; P p2]))); raise (ProofCheck d))
	      )
    | G ("bIff_BFun",[P p1; P p2]) ->
	(match ((i p1),(i p2)) with
	  (I.Atom (I.BFun (f,args)),I.Atom (I.Beq (I.NotBFun (f1,args1), I.NotBFun (f2,args2)))) ->
	    if (f = f1) & (f=f2) & (args = args1) then (I.Atom (I.BFun (f2,args2)))
	    else (ignore (E.warn "Proof: bIff_BFun: Invalid use of axiom! in %a" dp (G ("bIffMP",[P p1; P p2]))); raise (ProofCheck d))
	|  _ -> (ignore (E.warn "Proof: bIff_BFun: ??? Invalid use of axiom! in %a" dp (G ("bIffMP",[P p1; P p2]))); raise (ProofCheck d))
	      )
	    (* Congruence ends   *)

		(* Wessy saferd, safewr, ofsel *)
		(* note that the memory parameter of safeWr is unbound at this point,
		 * so we have to unify that above with not_FI *)
		| G("safeWr", [(E symbol_MEM);(P aa);(P bb);(P cc);(P dd);(P ee)]) ->
			(* a == pf (of E T')
			 * b == pf (= ADDR (+ A I))
			 * c == pf (fieldOf T SIZET OFF T') 
			 * d == pf (addIdx I L SIZET OFF)
			 * e == pf (of A (array rw T L))
			 * conclusion == pf (safewr4 M ADDR E)
			 *)
			let a_check = i aa in
			let b_check = i bb in
			let c_check = i cc in
			let d_check = i dd in
			let e_check = i ee in
			(* ignore (printf "Proof.Infer:SafeWr: a = %a\n" I.dp a_check) ; 
			ignore (printf "Proof.Infer:SafeWr: b = %a\n" I.dp b_check) ;
			ignore (printf "Proof.Infer:SafeWr: c = %a\n" I.dp c_check) ;
			ignore (printf "Proof.Infer:SafeWr: d = %a\n" I.dp d_check) ;
			ignore (printf "Proof.Infer:SafeWr: e = %a\n" I.dp e_check) ; *) 
			let symbol_E = (match a_check with 
				(I.Atom(I.BFun("of",[aa;bb]))) -> aa
			| _ -> raise (ProofCheck d)) in
			let symbol_TPRIME = (match a_check with 
				(I.Atom(I.BFun("of",[aa;bb]))) -> bb
			| _ -> raise (ProofCheck d)) in
			let symbol_ADDR = (match b_check with
				(I.Atom(I.Eq(aaa,bbb))) -> aaa
			| _ -> raise (ProofCheck d)) in
			let symbol_A = (match b_check with
				(I.Atom(I.Eq(aaa,I.Plus(bbb,ccc)))) -> bbb
			| _ -> raise (ProofCheck d)) in
			let symbol_I = (match b_check with
				(I.Atom(I.Eq(aaa,I.Plus(bbb,ccc)))) -> ccc
			| _ -> raise (ProofCheck d)) in
			let symbol_T = (match c_check with
				(I.Atom(I.BFun("fieldOf",[aa;bb;cc;dd]))) -> aa
			| _ -> raise (ProofCheck d)) in
			let symbol_SIZET = (match c_check with
				(I.Atom(I.BFun("fieldOf",[aa;bb;cc;dd]))) -> bb
			| _ -> raise (ProofCheck d)) in
			let symbol_OFF = (match c_check with
				(I.Atom(I.BFun("fieldOf",[aa;bb;cc;dd]))) 
					when dd = symbol_TPRIME -> cc
			| _ -> raise (ProofCheck d)) in
			let symbol_L = (match d_check with
				(I.Atom(I.BFun("arrIdx",[aa;bb;cc;dd]))) when
					(aa = symbol_I) & (cc = symbol_SIZET) & (dd = symbol_OFF) -> bb
			| _ -> raise (ProofCheck d)) in
			let symbol_rw = (match e_check with
				(I.Atom(I.BFun("of",[aa;(I.Fun("array",[bb;cc;dd]))]))) when
					(aa = symbol_A) & (cc = symbol_T) & (dd = symbol_L) & 
					(bb = I.Fun("rw",[])) -> bb
			| _ -> raise (ProofCheck d)) in
			(I.Atom(I.BFun("safewr4",[symbol_MEM;symbol_ADDR;symbol_E])))

		(* note that the memory parameter of safeRd is unbound at this point,
		 * so we have to unify that above with not_FI *)
		| G("safeRd", [(E symbol_MEM);(P aa);(P bb);(P cc);(P dd)]) ->
			(* a == pf (= ADDR (+ A I)) 
       * b == pf (fieldOf T SIZET OFF T')
       * c == pf (arrIdx I L SIZET OFF) 
       * d == pf (of A (array RO T L)) 
       * conclusion == pf (saferd4 M ADDR)
       *)
			let a_check = i aa in
			let b_check = i bb in
			let c_check = i cc in
			let d_check = i dd in
			(* ignore (printf "Proof.Infer:SafeRd: a = %a\n" I.dp a_check) ; 
			ignore (printf "Proof.Infer:SafeRd: b = %a\n" I.dp b_check) ;
			ignore (printf "Proof.Infer:SafeRd: c = %a\n" I.dp c_check) ;
			ignore (printf "Proof.Infer:SafeRd: d = %a\n" I.dp d_check) ; *) 
			let symbol_ADDR = (match a_check with
				(I.Atom(I.Eq(aaa,bbb))) -> aaa
			| _ -> raise (ProofCheck d)) in
			let symbol_A = (match a_check with
				(I.Atom(I.Eq(aaa,I.Plus(bbb,ccc)))) -> bbb
			| _ -> raise (ProofCheck d)) in
			let symbol_I = (match a_check with
				(I.Atom(I.Eq(aaa,I.Plus(bbb,ccc)))) -> ccc
			| _ -> raise (ProofCheck d)) in
			let symbol_T = (match b_check with
				(I.Atom(I.BFun("fieldOf",[aa;bb;cc;dd]))) -> aa
			| _ -> raise (ProofCheck d)) in
			let symbol_SIZET = (match b_check with
				(I.Atom(I.BFun("fieldOf",[aa;bb;cc;dd]))) -> bb
			| _ -> raise (ProofCheck d)) in
			let symbol_OFF = (match b_check with
				(I.Atom(I.BFun("fieldOf",[aa;bb;cc;dd]))) -> cc
			| _ -> raise (ProofCheck d)) in
			let symbol_TPRIME = (match b_check with
				(I.Atom(I.BFun("fieldOf",[aa;bb;cc;dd]))) -> dd
			| _ -> raise (ProofCheck d)) in
			let symbol_L = (match c_check with
				(I.Atom(I.BFun("arrIdx",[aa;bb;cc;dd]))) when
					(aa = symbol_I) & (cc = symbol_SIZET) & (dd = symbol_OFF) -> bb
			| _ -> raise (ProofCheck d)) in
			let symbol_RO = (match d_check with
				(I.Atom(I.BFun("of",[aa;(I.Fun("array",[bb;cc;dd]))]))) when
					(aa = symbol_A) & (cc = symbol_T) & (dd = symbol_L) -> bb
			| _ -> raise (ProofCheck d)) in
			(I.Atom(I.BFun("saferd4",[symbol_MEM;symbol_ADDR])))
		(* end of safeRd checking rule *)

		(* note that the memory parameter of ofSel is unbound at this point,
		 * so we have to unify that above with not_FI *)
		| G("ofSel", [(E symbol_MEM);(P aa);(P bb);(P cc);(P dd)]) ->
		  (* note: same hypotheses as saferd *)
			(* a == pf (= ADDR (+ A I)) 
       * b == pf (fieldOf T SIZET OFF T')
       * c == pf (arrIdx I L SIZET OFF) 
       * d == pf (of A (array RO T L)) 
       * conclusion == pf (saferd4 M ADDR)
       *)
			let a_check = i aa in
			let b_check = i bb in
			let c_check = i cc in
			let d_check = i dd in
			(* ignore (printf "Proof.Infer:SafeRd: a = %a\n" I.dp a_check) ; 
			ignore (printf "Proof.Infer:SafeRd: b = %a\n" I.dp b_check) ;
			ignore (printf "Proof.Infer:SafeRd: c = %a\n" I.dp c_check) ;
			ignore (printf "Proof.Infer:SafeRd: d = %a\n" I.dp d_check) ; *) 
			let symbol_ADDR = (match a_check with
				(I.Atom(I.Eq(aaa,bbb))) -> aaa
			| _ -> raise (ProofCheck d)) in
			let symbol_A = (match a_check with
				(I.Atom(I.Eq(aaa,I.Plus(bbb,ccc)))) -> bbb
			| _ -> raise (ProofCheck d)) in
			let symbol_I = (match a_check with
				(I.Atom(I.Eq(aaa,I.Plus(bbb,ccc)))) -> ccc
			| _ -> raise (ProofCheck d)) in
			let symbol_T = (match b_check with
				(I.Atom(I.BFun("fieldOf",[aa;bb;cc;dd]))) -> aa
			| _ -> raise (ProofCheck d)) in
			let symbol_SIZET = (match b_check with
				(I.Atom(I.BFun("fieldOf",[aa;bb;cc;dd]))) -> bb
			| _ -> raise (ProofCheck d)) in
			let symbol_OFF = (match b_check with
				(I.Atom(I.BFun("fieldOf",[aa;bb;cc;dd]))) -> cc
			| _ -> raise (ProofCheck d)) in
			let symbol_TPRIME = (match b_check with
				(I.Atom(I.BFun("fieldOf",[aa;bb;cc;dd]))) -> dd
			| _ -> raise (ProofCheck d)) in
			let symbol_L = (match c_check with
				(I.Atom(I.BFun("arrIdx",[aa;bb;cc;dd]))) when
					(aa = symbol_I) & (cc = symbol_SIZET) & (dd = symbol_OFF) -> bb
			| _ -> raise (ProofCheck d)) in
			let symbol_RO = (match d_check with
				(I.Atom(I.BFun("of",[aa;(I.Fun("array",[bb;cc;dd]))]))) when
					(aa = symbol_A) & (cc = symbol_T) & (dd = symbol_L) -> bb
			| _ -> raise (ProofCheck d)) in
			(I.Atom(I.BFun("of",[(I.Fun("sel4",[symbol_MEM;symbol_ADDR]));
				symbol_TPRIME])))
		(* end of ofSel checking rule *)

		| G("ofPtrOpt",[(P aa);(P bb)]) ->
			(* a == pf (<> A 0)
			 * b == pf (of A (ptropt T LEN))
			 * conclusion = pf (of A (array rw T LEN))
			 *)
			let a_check = i aa in
			let b_check = i bb in
			let symbol_A = (match a_check with
				(I.Atom(I.Neq(xxx,I.Int 0))) -> xxx
			| _ -> raise (ProofCheck d)) in
			let symbol_T = (match b_check with
				(I.Atom(I.BFun("of",[xxx;I.Fun("ptropt",[yyy;zzz])]))) 
					when (xxx = symbol_A) -> yyy
			| _ -> raise (ProofCheck d)) in
			let symbol_LEN = (match b_check with
				(I.Atom(I.BFun("of",[xxx;I.Fun("ptropt",[yyy;zzz])]))) -> zzz
			| _ -> raise (ProofCheck d)) in
			(I.Atom(I.BFun("of",[symbol_A;I.Fun("array",[I.Fun("rw",[]);symbol_T;symbol_LEN])])))

		| G("ofArrPOpt",[(P aa)]) ->
			(* a == pf (of A (array rw T LEN))
			 * conclusion =  pf (of A (ptropt T LEN))
			 * 
			*)
		    let a_check = i aa in
                    let (symbol_A,symbol_T,symbol_LEN) = 
                      (match a_check with
                        (I.Atom(I.BFun("of",[xxx;I.Fun("array",[_;yyy;zzz])]))) ->
                          (xxx,yyy,zzz) 
                      | _ -> raise (ProofCheck d)) in
                    I.Atom(I.BFun("of",[symbol_A;I.Fun("ptropt",[symbol_T;symbol_LEN])]))
                          
		| G("aIdx", [(E symbol_ELen_in);(E symbol_Off_in);(P aa);(P bb);(P cc)]) ->
			(* a == pf (>= I 0)
			 * b == pf (>= Len I)
			 * c == pf (= (mod I ELen) Off) 
			 * conclusion = pf (arrIdx I Len ELen Off)
			 *)
			let a_check = i aa in
			let b_check = i bb in
			let c_check = i cc in
			(* ignore (printf "aIdx a = %a\n" I.dp a_check) ; 
			ignore (printf "aIdx b = %a\n" I.dp b_check) ; 
			ignore (printf "aIdx c = %a\n" I.dp c_check) ; *) 
			let symbol_I = (match a_check with
				(I.Atom(I.Geq(xxx,I.Int 0))) -> xxx
		  | _ -> raise (ProofCheck d)) in
			let symbol_Len = (match b_check with
				(I.Atom(I.Geq(xxx,iii))) when iii = symbol_I -> xxx
		  | _ -> raise (ProofCheck d)) in
			let symbol_ELen = (match c_check with
				(I.Atom(I.Eq(I.Mod(xxx,iii),yyy))) when (iii = symbol_I) &
						(I.Int xxx = symbol_ELen_in) -> I.Int xxx
		  | _ -> raise (ProofCheck d)) in
			let symbol_Off = (match c_check with
				(I.Atom(I.Eq(I.Mod(xxx,iii),yyy))) when yyy = symbol_Off_in -> yyy
		  | _ -> raise (ProofCheck d)) in
			let result = (I.Atom(I.BFun("arrIdx",[symbol_I;symbol_Len;symbol_ELen;symbol_Off]))) in
			result

		(* field-of inference rules *)
		| G("fo10",[P aa]) -> (
			match i aa with
			  (I.Atom(I.BFun("size4",[t]))) -> 
					(I.Atom(I.BFun("fieldOf",[t;I.Int 4;I.Int 0;t])))
			| _ -> raise (ProofCheck d))

		| G("fo20",[P aa;P bb]) -> 
			let a_check = i aa in
			let b_check = i bb in
			let symbol_T1 = (match a_check with
				(I.Atom(I.BFun("size4",[xxx]))) -> xxx
		  | _ -> raise (ProofCheck d)) in
			let symbol_T2 = (match b_check with
				(I.Atom(I.BFun("size4",[xxx]))) -> xxx
		  | _ -> raise (ProofCheck d)) in
			(I.Atom(I.BFun("fieldOf",[I.Fun("tuple2",[symbol_T1;symbol_T2]) ; 
				I.Int 8 ; I.Int 0 ; symbol_T1])))
		| G("fo21",[P aa;P bb]) -> 
			let a_check = i aa in
			let b_check = i bb in
			let symbol_T1 = (match a_check with
				(I.Atom(I.BFun("size4",[xxx]))) -> xxx
		  | _ -> raise (ProofCheck d)) in
			let symbol_T2 = (match b_check with
				(I.Atom(I.BFun("size4",[xxx]))) -> xxx
		  | _ -> raise (ProofCheck d)) in
			(I.Atom(I.BFun("fieldOf",[I.Fun("tuple2",[symbol_T1;symbol_T2]) ; 
				I.Int 8 ; I.Int 4 ; symbol_T2])))

		| G("fo30",[P aa;P bb;P cc]) -> 
			let a_check = i aa in
			let b_check = i bb in
			let c_check = i cc in
			let symbol_T1 = (match a_check with
				(I.Atom(I.BFun("size4",[xxx]))) -> xxx
		  | _ -> raise (ProofCheck d)) in
			let symbol_T2 = (match b_check with
				(I.Atom(I.BFun("size4",[xxx]))) -> xxx
		  | _ -> raise (ProofCheck d)) in
			let symbol_T3 = (match c_check with
				(I.Atom(I.BFun("size4",[xxx]))) -> xxx
		  | _ -> raise (ProofCheck d)) in
			(I.Atom(I.BFun("fieldOf",[I.Fun("tuple3",[symbol_T1;symbol_T2;
					symbol_T3]) ; I.Int 12 ; I.Int 0 ; symbol_T1])))

		| G("fo31",[P aa;P bb;P cc]) -> 
			let a_check = i aa in
			let b_check = i bb in
			let c_check = i cc in
			let symbol_T1 = (match a_check with
				(I.Atom(I.BFun("size4",[xxx]))) -> xxx
		  | _ -> raise (ProofCheck d)) in
			let symbol_T2 = (match b_check with
				(I.Atom(I.BFun("size4",[xxx]))) -> xxx
		  | _ -> raise (ProofCheck d)) in
			let symbol_T3 = (match c_check with
				(I.Atom(I.BFun("size4",[xxx]))) -> xxx
		  | _ -> raise (ProofCheck d)) in
			(I.Atom(I.BFun("fieldOf",[I.Fun("tuple3",[symbol_T1;symbol_T2;
					symbol_T3]) ; I.Int 12 ; I.Int 4 ; symbol_T2])))

		| G("fo32",[P aa;P bb;P cc]) -> 
			let a_check = i aa in
			let b_check = i bb in
			let c_check = i cc in
			let symbol_T1 = (match a_check with
				(I.Atom(I.BFun("size4",[xxx]))) -> xxx
		  | _ -> raise (ProofCheck d)) in
			let symbol_T2 = (match b_check with
				(I.Atom(I.BFun("size4",[xxx]))) -> xxx
		  | _ -> raise (ProofCheck d)) in
			let symbol_T3 = (match c_check with
				(I.Atom(I.BFun("size4",[xxx]))) -> xxx
		  | _ -> raise (ProofCheck d)) in
			(I.Atom(I.BFun("fieldOf",[I.Fun("tuple3",[symbol_T1;symbol_T2;
					symbol_T3]) ; I.Int 12 ; I.Int 8 ; symbol_T3])))

		| G("fo43",[P aa;P bb;P cc;P dd]) -> 
			let a_check = i aa in
			let b_check = i bb in
			let c_check = i cc in
			let d_check = i dd in
			let symbol_T1 = (match a_check with
				(I.Atom(I.BFun("size4",[xxx]))) -> xxx
		  | _ -> raise (ProofCheck d)) in
			let symbol_T2 = (match b_check with
				(I.Atom(I.BFun("size4",[xxx]))) -> xxx
		  | _ -> raise (ProofCheck d)) in
			let symbol_T3 = (match c_check with
				(I.Atom(I.BFun("size4",[xxx]))) -> xxx
		  | _ -> raise (ProofCheck d)) in
			let symbol_T4 = (match d_check with
				(I.Atom(I.BFun("size4",[xxx]))) -> xxx
		  | _ -> raise (ProofCheck d)) in
			(I.Atom(I.BFun("fieldOf",[I.Fun("tuple4",[symbol_T1;symbol_T2;
					symbol_T3;symbol_T4]) ; I.Int 16 ; I.Int 12 ; symbol_T4])))

		| G("fo40",[P aa;P bb;P cc;P dd]) -> 
			let a_check = i aa in
			let b_check = i bb in
			let c_check = i cc in
			let d_check = i dd in
			let symbol_T1 = (match a_check with
				(I.Atom(I.BFun("size4",[xxx]))) -> xxx
		  | _ -> raise (ProofCheck d)) in
			let symbol_T2 = (match b_check with
				(I.Atom(I.BFun("size4",[xxx]))) -> xxx
		  | _ -> raise (ProofCheck d)) in
			let symbol_T3 = (match c_check with
				(I.Atom(I.BFun("size4",[xxx]))) -> xxx
		  | _ -> raise (ProofCheck d)) in
			let symbol_T4 = (match d_check with
				(I.Atom(I.BFun("size4",[xxx]))) -> xxx
		  | _ -> raise (ProofCheck d)) in
			(I.Atom(I.BFun("fieldOf",[I.Fun("tuple4",[symbol_T1;symbol_T2;
					symbol_T3;symbol_T4]) ; I.Int 16 ; I.Int 0 ; symbol_T1])))

		| G("fo41",[P aa;P bb;P cc;P dd]) -> 
			let a_check = i aa in
			let b_check = i bb in
			let c_check = i cc in
			let d_check = i dd in
			let symbol_T1 = (match a_check with
				(I.Atom(I.BFun("size4",[xxx]))) -> xxx
		  | _ -> raise (ProofCheck d)) in
			let symbol_T2 = (match b_check with
				(I.Atom(I.BFun("size4",[xxx]))) -> xxx
		  | _ -> raise (ProofCheck d)) in
			let symbol_T3 = (match c_check with
				(I.Atom(I.BFun("size4",[xxx]))) -> xxx
		  | _ -> raise (ProofCheck d)) in
			let symbol_T4 = (match d_check with
				(I.Atom(I.BFun("size4",[xxx]))) -> xxx
		  | _ -> raise (ProofCheck d)) in
			(I.Atom(I.BFun("fieldOf",[I.Fun("tuple4",[symbol_T1;symbol_T2;
					symbol_T3;symbol_T4]) ; I.Int 16 ; I.Int 4 ; symbol_T2])))


		| G("fo42",[P aa;P bb;P cc;P dd]) -> 
			let a_check = i aa in
			let b_check = i bb in
			let c_check = i cc in
			let d_check = i dd in
			let symbol_T1 = (match a_check with
				(I.Atom(I.BFun("size4",[xxx]))) -> xxx
		  | _ -> raise (ProofCheck d)) in
			let symbol_T2 = (match b_check with
				(I.Atom(I.BFun("size4",[xxx]))) -> xxx
		  | _ -> raise (ProofCheck d)) in
			let symbol_T3 = (match c_check with
				(I.Atom(I.BFun("size4",[xxx]))) -> xxx
		  | _ -> raise (ProofCheck d)) in
			let symbol_T4 = (match d_check with
				(I.Atom(I.BFun("size4",[xxx]))) -> xxx
		  | _ -> raise (ProofCheck d)) in
			(I.Atom(I.BFun("fieldOf",[I.Fun("tuple4",[symbol_T1;symbol_T2;
					symbol_T3;symbol_T4]) ; I.Int 16 ; I.Int 8 ; symbol_T3])))

		(* simple typing begins *)
		| G("ofIntAny", [E symbol_E]) ->
			(I.Atom(I.BFun("of",[symbol_E;I.Fun("int",[])])))

    | G("ofBool1", []) -> (I.Atom(I.BFun("of",[I.Int 1; I.Fun("bool",[])])))
    | G("ofBool0", []) -> (I.Atom(I.BFun("of",[I.Int 0; I.Fun("bool",[])])))
    | G("ofExn0", []) -> (I.Atom(I.BFun("of",[I.Int 0; I.Fun("exn",[])])))
    | G("ofExn1", []) -> (I.Atom(I.BFun("of",[I.Int 1; I.Fun("exn",[])])))
    | G("ofExn2", []) -> (I.Atom(I.BFun("of",[I.Int 2; I.Fun("exn",[])])))
    | G("ofExn3", []) -> (I.Atom(I.BFun("of",[I.Int 3; I.Fun("exn",[])])))
    | G("ofExn4", []) -> (I.Atom(I.BFun("of",[I.Int 4; I.Fun("exn",[])])))
    | G("ofExn5", []) -> (I.Atom(I.BFun("of",[I.Int 5; I.Fun("exn",[])])))
    | G("szint", []) -> (I.Atom(I.BFun("size4",[I.Fun("int",[])])))
    | G("szbool", []) -> (I.Atom(I.BFun("size4",[I.Fun("bool",[])])))
    | G("szarr",[E ro; E t; E len]) -> I.Atom(I.BFun("size4",[I.Fun("array",
                                         [ro;t;len])]))

    | G("ofIntAny",[E e]) -> (I.Atom(I.BFun("of",[e;I.Fun("int",[])])))
		(* typing ends *)
          
		(* bi-dimensional yada begins *)
    | G("bidim1", [P aa;P bb;P cc]) ->
	let a_check = i aa in
	let b_check = i bb in
	let c_check = i cc in
	let symbol_LX = (match a_check with
	  (I.Atom(I.Gt(I.Minus(xxx,yyy),I.Int 0))) -> xxx
	| _ -> raise (ProofCheck d)) in
	let symbol_J = (match a_check with
	  (I.Atom(I.Gt(I.Minus(xxx,yyy),I.Int 0))) -> yyy
	| _ -> raise (ProofCheck d)) in
	let symbol_LY = (match b_check with
	  (I.Atom(I.Gt(I.Minus(xxx,yyy),I.Int 0))) -> xxx
	| _ -> raise (ProofCheck d)) in
	let symbol_I = (match b_check with
	  (I.Atom(I.Gt(I.Minus(xxx,yyy),I.Int 0))) -> yyy
	| _ -> raise (ProofCheck d)) in
	let sym_zero = (match c_check with
	  (I.Atom(I.Geq(xxx,I.Int 0))) when (xxx = symbol_I) -> I.Int 0
	| _ -> raise (ProofCheck d)) in
	I.Atom(I.Geq(I.Minus(I.Times(I.Int 4,I.Times(symbol_LX,symbol_LY)),
			     (I.Int 4)),
		     (I.Times(I.Plus(symbol_I,I.Times(symbol_LY,symbol_J)),
			      (I.Int 4)))))
          
    | G("bidim3", [P aa;P bb; P cc]) ->
	let a_check = i aa in
	let b_check = i bb in
	let c_check = i cc in
	let symbol_X = (match a_check with
	  (I.Atom(I.Geq(xxx,I.Int 0))) -> xxx
	| _ -> raise (ProofCheck d)) in
	let symbol_Y = (match b_check with
	  (I.Atom(I.Geq(xxx,I.Int 0))) -> xxx
	| _ -> raise (ProofCheck d)) in
	let symbol_Z = (match c_check with
	  (I.Atom(I.Geq(xxx,I.Int 0))) -> xxx
	| _ -> raise (ProofCheck d)) in
	I.Atom(I.Geq(I.Times(I.Plus(symbol_X,I.Times(symbol_Y,symbol_Z)),
			     I.Int 4),I.Int 0))
		(* bi-dimensional yada ends *) 
          
		(* modular arithmetic begins *)
    | G("modCt", [(E (I.Int int_N));(E (I.Int int_E));(E (I.Int int_RES))]) -> 
	if (int_N > 0) & (int_RES >= 0) & (int_N > int_RES) & 
	  ((int_E mod int_N) = int_RES) then 
	  I.Atom((I.Eq(I.Mod(int_N,I.Int int_E),I.Int int_RES)))
	else (ignore (E.warn "Proof.infer:modCt numbers do not work %d %d %d\n" int_N int_E int_RES) ; raise (ProofCheck d))
            
    | G("modGte0",[(E (I.Int x));(E y);(P zz)]) ->
	let z_check = i zz in
	let symbol_Z = (match z_check with
	  (I.Atom(I.Geq(xxx,I.Int 0))) -> xxx
	| _ -> raise (ProofCheck d)) in
	I.Atom(I.Geq(I.Times(I.Mod(x,y),symbol_Z),I.Int 0))
          
          
          
    | G("modCt", [(E (I.Int int_N));(E (I.Int int_E));(E (I.Int int_RES))]) -> 
	if (int_N > 0) & (int_RES >= 0) & (int_N > int_RES) & 
	  ((int_E mod int_N) = int_RES) then 
	  I.Atom((I.Eq(I.Mod(int_N,I.Int int_E),I.Int int_RES)))
	else (ignore (E.warn "Proof.infer:modCt numbers do not work %d %d %d\n" int_N int_E int_RES) ; raise (ProofCheck d))
            
	  (* modCt special cases *)
    | G("modCt", [(E (I.Int int_N));(E (I.Times(x,y)));(E (I.Int int_RES))])
      when (y = I.Int int_N) & (int_RES = 0) -> 
	I.Atom((I.Eq(I.Mod(int_N,I.Times(x,y)),I.Int int_RES)))
    | G("modCt", [(E (I.Int int_N));(E (I.Minus(I.Times(x,y),z)));(E(I.Int
		                                                       int_RES))]) when (y = I.Int int_N) & (int_RES = 0) ->
				                                         I.Atom((I.Eq(I.Mod(int_N,I.Minus(I.Times(x,y),z)),I.Int int_RES)))
    | G("modCt", [(E (I.Int int_N));(E (I.Plus(I.Times(x,y),z)));
		   (E (I.Int int_RES))]) when
		     (y = I.Int int_N) & (z = I.Int int_RES) ->
		       I.Atom((I.Eq(I.Mod(int_N,(I.Plus(I.Times(x,y),z))),I.Int int_RES)))
                         
    | G("modCt", [(E (I.Int int_N));(E (I.Plus(I.Times(x,y),z)));
		   (E (I.Int 0))]) when
		     (y = I.Int int_N) & (z = I.Int int_N) ->
		       I.Atom((I.Eq(I.Mod(int_N,(I.Plus(I.Times(x,y),z))),I.Int 0)))
                         
                         
    | G("modCt",[(E (I.Int int_N));(E I.Plus(I.Times(I.Minus(I.Times(x,I.Int n1),y) ,I.Int n2),I.Int n3));E(I.Int n4)])
      when (n1-1)*n2 = int_N && n3=n4 ->
	I.Atom(I.Eq(I.Mod(int_N,I.Plus(I.Times(I.Minus(I.Times(x,I.Int n1),y) ,I.Int n2),I.Int n3)),I.Int n4))
          
    | G("modCt",[(E (I.Int int_N));(E I.Times(I.Minus(I.Times(x,I.Int n1),y) ,I.Int n2));E(I.Int 0)])
      when (n1-1)*n2 = int_N -> I.Atom(I.Eq(I.Mod(int_N,I.Times(I.Minus(I.Times(x,I.Int n1),y), I.Int n2)),I.Int 0))
          
		(* modCt general case *)
    | G("modCt", [(E (I.Int int_N));(E (I.Plus(I.Int 0,(I.Times(x,y)))));
		   (E (I.Int int_RES))])
      when (y = I.Int int_N) & (int_RES = 0) -> 
	I.Atom((I.Eq(I.Mod(int_N, (I.Plus(I.Int 0,I.Times(x,y)))), I.Int int_RES)))
          
    | G("divCt", [(E (I.Int int_N));(E (I.Int int_E));(E (I.Int int_RES))]) -> 
	if (int_N > 0) & ((int_E / int_N) = int_RES) then 
	  I.Atom((I.Eq(I.Div(int_N,I.Int int_E),I.Int int_RES)))
	else (ignore (E.warn "Proof.infer:divCT numbers do not work %d %d %d\n" int_N int_E int_RES) ; raise (ProofCheck d))
		| G("modLeq", [(E (I.Int int_Nm1));(E (I.Int int_N));(E (I.Int int_E))]) -> 
		    if (int_N > 0) & (int_Nm1 = int_N - 1) then 
		      I.Atom((I.Geq(I.Int int_Nm1,(I.Mod(int_N,I.Int int_E)))))
		    else (ignore (E.warn "Proof.infer:modLeq numbers do not work %d %d %d\n" int_Nm1 int_N int_E) ; raise (ProofCheck d))
		| G("modGeq", [(E (I.Int int_N));(E symbol_E)]) -> 
		    if (int_N > 0) then 
		      I.Atom((I.Geq(I.Mod(int_N,symbol_E),I.Int 0)))
		    else (ignore (E.warn "Proof.infer:modGeq numbers do not work %d\n" int_N) ; raise (ProofCheck d))
		| G("mod*+", [(E symbol_E);(E (I.Int int_Np));(E (I.Int int_N));
			       (E (I.Int int_F));(E (I.Int int_DV))]) -> 
			         if ((int_N mod int_DV) = int_Np) & ((int_F mod int_DV) = 0) then
				   I.Atom((I.Eq(I.Mod(int_DV, (I.Plus(I.Int int_N,(I.Times(symbol_E,I.Int int_F))))),(I.Int int_Np))))
			         else (ignore (E.warn "Proof.infer:mod*+ numbers do not work %d %d %d %d\n" int_Np int_N int_F int_DV) ; raise (ProofCheck d))
		| G("mod*", [(E symbol_E);(E (I.Int int_F));(E (I.Int int_DV))]) -> 
		    if ((int_F mod int_DV) = 0) then 
		      I.Atom(I.Eq(I.Mod(int_DV,(I.Times(symbol_E,I.Int int_F))),
				  I.Int 0))
		    else (ignore (E.warn "Proof.infer:mod* numbers do not work %d %d\n" int_F int_DV) ; raise (ProofCheck d))
		| G("div+", [(E symbol_E);(E (I.Int int_Fp));(E (I.Int int_N));
			      (E (I.Int int_Np));(E (I.Int int_F));(E (I.Int int_DV))]) -> 
			        if ((int_F mod int_DV) = 0) & ((int_N / int_DV) = int_Np) &
				  ((int_F / int_DV) = int_Fp) then 
				  I.Atom(I.Eq(I.Div(int_DV,(I.Plus(I.Int int_N,(I.Times(symbol_E,I.Int int_F))))),
					      I.Plus(I.Int int_Np,(I.Times(symbol_E,I.Int int_Fp)))))
			        else (ignore (E.warn "Proof.infer:div+ numbers do not work %d %d %d %d %d\n" int_Fp int_N int_Np int_F int_DV) ; raise (ProofCheck d))
                                    
		(* modular arithmetic ends *)
                | _ -> E.s (E.unimp "Proof.infer cannot check@!%a\n" dp d )
  in
  try 
    i d
  with (ProofCheck e) -> E.s (E.bug "Proof.infer says invalid proof:@!%a" dp e)