Hi All, if I have a simple goal to proof, for example:
g` ( X0 /\ X1 /\ X2 /\ X3 /\ X4 /\ X5 /\ X6 /\ X7 /\ X8 /\ X9 /\ (X0 = (r0 /\ nc0)) /\ (X1 = (r1 /\ nc1)) /\ (X2 = (r0 /\ c0 /\ nm_eq_m /\ uf1_eq_0)) /\ (X3 = (r0 /\ c0 /\ nm_eq_x /\ uf1_eq_1)) /\ (X4 = (r0 /\ c1 /\ nm_eq_x)) /\ (X5 = (r1 /\ nm_eq_max)) /\ (X6 = (r0 /\ c0 /\ nM_eq_x /\ uf2_eq_0)) /\ (X7 = (r0 /\ c0 /\ nM_eq_M /\ uf2_eq_1)) /\ (X8 = (r0 /\ c1 /\ nM_eq_x)) /\ (X9 = (r1 /\ nM_eq_min)) ) ==> ( ( (r0 /\ nc0) \/ (r1 /\ nc1) \/ (r0 /\ c0 /\ nm_eq_m /\ uf1_eq_0) \/ (r0 /\ c0 /\ nm_eq_x /\ uf1_eq_1) \/ (r0 /\ c1 /\ nm_eq_x) \/ (r1 /\ nm_eq_max) \/ (r0 /\ c0 /\ nM_eq_x /\ uf2_eq_0) \/ (r0 /\ c0 /\ nM_eq_M /\ uf2_eq_1) \/ (r0 /\ c1 /\ nM_eq_x) \/ (r1 /\ nM_eq_min) )= ( (r0 \/ ~X0) /\ (nc0 \/ ~X0) /\ (~r0 \/ ~nc0 \/ X0) /\ (r1 \/ ~X1) /\ (nc1 \/ ~X1) /\ (~r1 \/ ~nc1 \/ X1) /\ (r0 \/ ~X2) /\ (c0 \/ ~X2) /\ (nm_eq_m \/ ~X2) /\ (uf1_eq_0 \/ ~X2) /\ (~r0 \/ ~c0 \/ ~nm_eq_m \/ ~uf1_eq_0 \/ X2) /\ (r0 \/ ~X3) /\ (c0 \/ ~X3) /\ (nm_eq_x \/ ~X3) /\ (uf1_eq_1 \/ ~X3) /\ (~r0 \/ ~c0 \/ ~nm_eq_x \/ ~uf1_eq_1 \/ X3) /\ (r0 \/ ~X4) /\ (c1 \/ ~X4) /\ (nm_eq_x \/ ~X4) /\ (~r0 \/ ~c1 \/ ~nm_eq_x \/ X4) /\ (r1 \/ ~X5) /\ (nm_eq_max \/ ~X5) /\ (~r1 \/ ~nm_eq_max \/ X5) /\ (r0 \/ ~X6) /\ (c0 \/ ~X6) /\ (nM_eq_x \/ ~X6) /\ (uf2_eq_0 \/ ~X6) /\ (~r0 \/ ~c0 \/ ~nM_eq_x \/ ~uf2_eq_0 \/ X6) /\ (r0 \/ ~X7) /\ (c0 \/ ~X7) /\ (nM_eq_M \/ ~X7) /\ (uf2_eq_1 \/ ~X7) /\ (~r0 \/ ~c0 \/ ~nM_eq_M \/ ~uf2_eq_1 \/ X7) /\ (r0 \/ ~X8) /\ (c1 \/ ~X8) /\ (nM_eq_x \/ ~X8) /\ (~r0 \/ ~c1 \/ ~nM_eq_x \/ X8) /\ (r1 \/ ~X9) /\ (nM_eq_min \/ ~X9) /\ (~r1 \/ ~nM_eq_min \/ X9) /\ (X0 \/ X1 \/ X2 \/ X3 \/ X4 \/ X5 \/ X6 \/ X7 \/ X8 \/ X9) )) `; time e(DECIDE_TAC); It really works fine. but when i try same kind of proof with bigger values in assumption,antecedent and consequent so that, assumptions => (antecedent = consequent) then HOL4 gives an error saying "memory exceeds". g` ( <big assumption> ) => ( (<big antecedent>) = (<big consequent>) ); time e(DECIDE_TAC); I need to know the time for the prove e.g. DECIDE_TAC. I don't need to see the output or proof steps. any suggestion ? regards -- Khaza Anuarul Hoque, B.Sc Engr M.A.Sc Student, Dept. of ECE Concordia University, Montreal, Canada Web: http://users.encs.concordia.ca/~k_hoque ------------------------------------------------------------------------------ Return on Information: Google Enterprise Search pays you back Get the facts. http://p.sf.net/sfu/google-dev2dev _______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
