Index of /xml/Coq/romega/ReflOmegaCore

[ICO]NameLast modifiedSizeDescription
[PARENTDIR]Parent Directory  -  
[ ]sum.con.types.xml.gz2004-04-08 01:50 193  
[ ]term.ind.types.xml.gz2004-04-08 01:49 193  
[ ]step.ind.types.xml.gz2004-04-08 01:49 194  
[ ]eq_Z.con.types.xml.gz2004-04-08 01:49 196  
[ ]state.con.types.xml.gz2004-04-08 01:50 196  
[ ]t_omega.ind.types.xml.gz2004-04-08 01:49 197  
[ ]absurd.con.types.xml.gz2004-04-08 01:49 198  
[ ]e_step.ind.types.xml.gz2004-04-08 01:49 198  
[ ]eq_pos.con.types.xml.gz2004-04-08 01:49 198  
[ ]fusion.con.types.xml.gz2004-04-08 01:50 198  
[ ]h_step.ind.types.xml.gz2004-04-08 01:49 198  
[ ]p_step.ind.types.xml.gz2004-04-08 01:49 198  
[ ]reduce.con.types.xml.gz2004-04-08 01:50 198  
[ ]valid1.con.types.xml.gz2004-04-08 01:49 198  
[ ]valid2.con.types.xml.gz2004-04-08 01:49 198  
[ ]eq_nat.con.types.xml.gz2004-04-08 01:49 199  
[ ]nthProp.con.types.xml.gz2004-04-08 01:49 199  
[ ]rewrite.con.types.xml.gz2004-04-08 01:50 199  
[ ]eq_term.con.types.xml.gz2004-04-08 01:49 200  
[ ]PropList.ind.types.xml.gz2004-04-08 01:49 201  
[ ]term_rec.con.types.xml.gz2004-04-08 01:49 201  
[ ]Topp_one.con.types.xml.gz2004-04-08 01:50 202  
[ ]Topp_opp.con.types.xml.gz2004-04-08 01:49 202  
[ ]add_norm.con.types.xml.gz2004-04-08 01:50 202  
[ ]map_cons.con.types.xml.gz2004-04-08 01:50 202  
[ ]merge_eq.con.types.xml.gz2004-04-08 01:50 202  
[ ]nth_hyps.con.types.xml.gz2004-04-08 01:49 202  
[ ]step_rec.con.types.xml.gz2004-04-08 01:49 202  
[ ]t_fusion.ind.types.xml.gz2004-04-08 01:49 202  
[ ]direction.ind.types.xml.gz2004-04-08 01:49 203  
[ ]p_invert.con.types.xml.gz2004-04-08 01:51 203  
[ ]p_rewrite.con.types.xml.gz2004-04-08 01:51 203  
[ ]step_rect.con.types.xml.gz2004-04-08 01:49 203  
[ ]term_rect.con.types.xml.gz2004-04-08 01:49 203  
[ ]Tmult_sym.con.types.xml.gz2004-04-08 01:49 204  
[ ]Topp_plus.con.types.xml.gz2004-04-08 01:49 204  
[ ]Tplus_sym.con.types.xml.gz2004-04-08 01:49 204  
[ ]co_valid1.con.types.xml.gz2004-04-08 01:51 204  
[ ]T_OMEGA10.con.types.xml.gz2004-04-08 01:49 205  
[ ]T_OMEGA11.con.types.xml.gz2004-04-08 01:49 205  
[ ]T_OMEGA15.con.types.xml.gz2004-04-08 01:49 205  
[ ]T_OMEGA16.con.types.xml.gz2004-04-08 01:49 205  
[ ]e_step_rec.con.types.xml.gz2004-04-08 01:49 205  
[ ]h_step_rec.con.types.xml.gz2004-04-08 01:49 205  
[ ]move_right.con.types.xml.gz2004-04-08 01:50 205  
[ ]p_step_rec.con.types.xml.gz2004-04-08 01:49 205  
[ ]split_ineq.con.types.xml.gz2004-04-08 01:50 205  
[ ]T_OMEGA12.con.types.xml.gz2004-04-08 01:49 206  
[ ]T_OMEGA13.con.types.xml.gz2004-04-08 01:49 206  
[ ]Tminus_def.con.types.xml.gz2004-04-08 01:50 206  
[ ]apply_both.con.types.xml.gz2004-04-08 01:49 206  
[ ]apply_left.con.types.xml.gz2004-04-08 01:49 206  
[ ]proposition.ind.types.xml.gz2004-04-08 01:49 206  
[ ]t_omega_rec.con.types.xml.gz2004-04-08 01:49 206  
[ ]valid_hyps.con.types.xml.gz2004-04-08 01:49 206  
[ ]e_step_rect.con.types.xml.gz2004-04-08 01:49 207  
[ ]h_step_rect.con.types.xml.gz2004-04-08 01:49 207  
[ ]interp_full.con.types.xml.gz2004-04-08 01:50 207  
[ ]interp_hyps.con.types.xml.gz2004-04-08 01:49 207  
[ ]interp_term.con.types.xml.gz2004-04-08 01:49 207  
[ ]p_step_rect.con.types.xml.gz2004-04-08 01:49 207  
[ ]prop_stable.con.types.xml.gz2004-04-08 01:50 207  
[ ]scalar_norm.con.types.xml.gz2004-04-08 01:50 207  
[ ]term_stable.con.types.xml.gz2004-04-08 01:49 207  
[ ]Topp_mult_r.con.types.xml.gz2004-04-08 01:50 208  
[ ]apply_right.con.types.xml.gz2004-04-08 01:49 208  
[ ]concl_to_hyp.con.types.xml.gz2004-04-08 01:52 208  
[ ]constant_neg.con.types.xml.gz2004-04-08 01:50 208  
[ ]constant_nul.con.types.xml.gz2004-04-08 01:50 208  
[ ]decidability.con.types.xml.gz2004-04-08 01:50 208  
[ ]omega_tactic.con.types.xml.gz2004-04-08 01:52 208  
[ ]t_omega_rect.con.types.xml.gz2004-04-08 01:49 208  
[ ]valid_lhyps.con.types.xml.gz2004-04-08 01:51 208  
[ ]PropList_rec.con.types.xml.gz2004-04-08 01:49 209  
[ ]Tred_factor0.con.types.xml.gz2004-04-08 01:50 209  
[ ]Tred_factor1.con.types.xml.gz2004-04-08 01:50 209  
[ ]Tred_factor2.con.types.xml.gz2004-04-08 01:50 209  
[ ]Tred_factor3.con.types.xml.gz2004-04-08 01:50 209  
[ ]Tred_factor4.con.types.xml.gz2004-04-08 01:50 209  
[ ]Tred_factor5.con.types.xml.gz2004-04-08 01:49 209  
[ ]Tred_factor6.con.types.xml.gz2004-04-08 01:50 209  
[ ]apply_oper_1.con.types.xml.gz2004-04-08 01:49 209  
[ ]contradiction.con.types.xml.gz2004-04-08 01:50 209  
[ ]do_normalize.con.types.xml.gz2004-04-08 01:50 209  
[ ]exact_divide.con.types.xml.gz2004-04-08 01:50 209  
[ ]execute_omega.con.types.xml.gz2004-04-08 01:50 209  
[ ]p_apply_left.con.types.xml.gz2004-04-08 01:50 209  
[ ]reduce_lhyps.con.types.xml.gz2004-04-08 01:51 209  
[ ]t_fusion_rec.con.types.xml.gz2004-04-08 01:49 209  
[ ]to_contradict.con.types.xml.gz2004-04-08 01:50 209  
[ ]apply_oper_2.con.types.xml.gz2004-04-08 01:49 210  
[ ]direction_rec.con.types.xml.gz2004-04-08 01:49 210  
[ ]fusion_right.con.types.xml.gz2004-04-08 01:50 210  
[ ]PropList_rect.con.types.xml.gz2004-04-08 01:49 211  
[ ]Tmult_assoc_r.con.types.xml.gz2004-04-08 01:49 211  
[ ]Tplus_assoc_l.con.types.xml.gz2004-04-08 01:49 211  
[ ]Tplus_assoc_r.con.types.xml.gz2004-04-08 01:49 211  
[ ]Tplus_permute.con.types.xml.gz2004-04-08 01:49 211  
[ ]direction_rect.con.types.xml.gz2004-04-08 01:49 211  
[ ]fusion_cancel.con.types.xml.gz2004-04-08 01:50 211  
[ ]p_apply_right.con.types.xml.gz2004-04-08 01:50 211  
[ ]t_fusion_rect.con.types.xml.gz2004-04-08 01:49 211  
[ ]Tmult_opp_left.con.types.xml.gz2004-04-08 01:50 213  
[ ]decompose_solve.con.types.xml.gz2004-04-08 01:51 213  
[ ]normalize_hyps.con.types.xml.gz2004-04-08 01:51 213  
[ ]constant_not_nul.con.types.xml.gz2004-04-08 01:50 214  
[ ]extract_hyp_neg.con.types.xml.gz2004-04-08 01:51 214  
[ ]extract_hyp_pos.con.types.xml.gz2004-04-08 01:51 214  
[ ]proposition_rec.con.types.xml.gz2004-04-08 01:49 214  
[ ]scalar_norm_add.con.types.xml.gz2004-04-08 01:50 214  
[ ]valid_list_goal.con.types.xml.gz2004-04-08 01:49 214  
[ ]destructure_hyps.con.types.xml.gz2004-04-08 01:50 215  
[ ]interp_list_goal.con.types.xml.gz2004-04-08 01:49 215  
[ ]negate_contradict.con.types.xml.gz2004-04-08 01:50 215  
[ ]not_exact_divide.con.types.xml.gz2004-04-08 01:50 215  
[ ]valid_list_hyps.con.types.xml.gz2004-04-08 01:49 215  
[ ]Tmult_plus_distr.con.types.xml.gz2004-04-08 01:50 216  
[ ]interp_full_goal.con.types.xml.gz2004-04-08 01:50 216  
[ ]interp_list_hyps.con.types.xml.gz2004-04-08 01:49 216  
[ ]proposition_rect.con.types.xml.gz2004-04-08 01:49 216  
[ ]divide_and_approx.con.types.xml.gz2004-04-08 01:50 217  
[ ]do_normalize_list.con.types.xml.gz2004-04-08 01:50 217  
[ ]interp_goal_concl.con.types.xml.gz2004-04-08 01:49 217  
[ ]interp_proposition.con.types.xml.gz2004-04-08 01:49 219  
[ ]Tmult_assoc_reduced.con.types.xml.gz2004-04-08 01:50 221  
[ ]negate_contradict_inv.con.types.xml.gz2004-04-08 01:50 222  
[ ]Topp_one.con.xml.gz2004-04-08 01:50 286  
[ ]reduce_stable.con.xml.gz2004-04-08 01:50 287  
[ ]Topp_opp_stable.con.xml.gz2004-04-08 01:49 288  
[ ]reduce.con.xml.gz2004-04-08 01:50 288  
[ ]Tmult_sym.con.xml.gz2004-04-08 01:49 289  
[ ]Topp_one_stable.con.xml.gz2004-04-08 01:50 289  
[ ]Topp_opp.con.xml.gz2004-04-08 01:49 289  
[ ]Tplus_sym.con.xml.gz2004-04-08 01:49 289  
[ ]Tmult_sym_stable.con.xml.gz2004-04-08 01:49 290  
[ ]Tplus_sym_stable.con.xml.gz2004-04-08 01:49 290  
[ ]T_OMEGA11.con.xml.gz2004-04-08 01:49 291  
[ ]T_OMEGA12.con.xml.gz2004-04-08 01:49 291  
[ ]T_OMEGA15.con.xml.gz2004-04-08 01:49 291  
[ ]T_OMEGA16.con.xml.gz2004-04-08 01:49 291  
[ ]Topp_plus.con.xml.gz2004-04-08 01:49 291  
[ ]Tminus_def.con.xml.gz2004-04-08 01:50 292  
[ ]Topp_plus_stable.con.xml.gz2004-04-08 01:49 292  
[ ]Tred_factor0.con.xml.gz2004-04-08 01:50 292  
[ ]T_OMEGA10.con.xml.gz2004-04-08 01:49 293  
[ ]Tminus_def_stable.con.xml.gz2004-04-08 01:50 293  
[ ]T_OMEGA11_stable.con.xml.gz2004-04-08 01:49 294  
[ ]T_OMEGA13.con.xml.gz2004-04-08 01:49 294  
[ ]Tred_factor1.con.xml.gz2004-04-08 01:50 294  
[ ]Tred_factor2.con.xml.gz2004-04-08 01:50 294  
[ ]Tred_factor3.con.xml.gz2004-04-08 01:50 294  
[ ]Tred_factor4.con.xml.gz2004-04-08 01:50 294  
[ ]Tred_factor5.con.xml.gz2004-04-08 01:49 294  
[ ]T_OMEGA10_stable.con.xml.gz2004-04-08 01:49 295  
[ ]T_OMEGA12_stable.con.xml.gz2004-04-08 01:49 295  
[ ]T_OMEGA13_stable.con.xml.gz2004-04-08 01:49 295  
[ ]T_OMEGA15_stable.con.xml.gz2004-04-08 01:49 295  
[ ]T_OMEGA16_stable.con.xml.gz2004-04-08 01:49 295  
[ ]Topp_mult_r.con.xml.gz2004-04-08 01:50 295  
[ ]Topp_mult_r_stable.con.xml.gz2004-04-08 01:50 295  
[ ]Tplus_permute.con.xml.gz2004-04-08 01:49 295  
[ ]Tred_factor0_stable.con.xml.gz2004-04-08 01:50 295  
[ ]Tred_factor6.con.xml.gz2004-04-08 01:50 295  
[ ]Tred_factor6_stable.con.xml.gz2004-04-08 01:50 295  
[ ]Tmult_assoc_r.con.xml.gz2004-04-08 01:49 296  
[ ]Tplus_assoc_l.con.xml.gz2004-04-08 01:49 296  
[ ]Tplus_assoc_r.con.xml.gz2004-04-08 01:49 296  
[ ]absurd.con.xml.gz2004-04-08 01:49 296  
[ ]eq_nat.con.xml.gz2004-04-08 01:49 296  
[ ]Tred_factor1_stable.con.xml.gz2004-04-08 01:50 297  
[ ]Tred_factor2_stable.con.xml.gz2004-04-08 01:50 297  
[ ]Tred_factor3_stable.con.xml.gz2004-04-08 01:50 297  
[ ]Tred_factor4_stable.con.xml.gz2004-04-08 01:50 297  
[ ]Tmult_assoc_r_stable.con.xml.gz2004-04-08 01:49 298  
[ ]Tplus_assoc_l_stable.con.xml.gz2004-04-08 01:49 298  
[ ]Tplus_assoc_r_stable.con.xml.gz2004-04-08 01:49 298  
[ ]Tplus_permute_stable.con.xml.gz2004-04-08 01:49 298  
[ ]Tred_factor5_stable.con.xml.gz2004-04-08 01:49 298  
[ ]reduce_lhyps_valid.con.xml.gz2004-04-08 01:52 298  
[ ]Tmult_opp_left.con.xml.gz2004-04-08 01:50 299  
[ ]Tmult_opp_left_stable.con.xml.gz2004-04-08 01:50 300  
[ ]Tmult_plus_distr.con.xml.gz2004-04-08 01:50 300  
[ ]concl_to_hyp.con.xml.gz2004-04-08 01:52 301  
[ ]eq_Z.con.xml.gz2004-04-08 01:49 302  
[ ]rewrite.con.xml.gz2004-04-08 01:50 302  
[ ]Tmult_plus_distr_stable.con.xml.gz2004-04-08 01:50 303  
[ ]Tmult_assoc_reduced.con.xml.gz2004-04-08 01:50 306  
[ ]eq_pos.con.xml.gz2004-04-08 01:49 310  
[ ]Tmult_assoc_reduced_stable.con.xml.gz2004-04-08 01:50 311  
[ ]add_norm.con.xml.gz2004-04-08 01:50 312  
[ ]eq_term.con.xml.gz2004-04-08 01:49 313  
[ ]p_rewrite.con.xml.gz2004-04-08 01:51 313  
[ ]decidability.con.xml.gz2004-04-08 01:50 314  
[ ]move_right.con.xml.gz2004-04-08 01:50 314  
[ ]scalar_norm.con.xml.gz2004-04-08 01:50 317  
[ ]fusion_cancel.con.xml.gz2004-04-08 01:50 319  
[ ]scalar_norm_add.con.xml.gz2004-04-08 01:50 324  
[ ]merge_eq.con.xml.gz2004-04-08 01:50 327  
[ ]valid1.con.xml.gz2004-04-08 01:49 328  
[ ]term_stable.con.xml.gz2004-04-08 01:49 330  
[ ]apply_left.con.xml.gz2004-04-08 01:49 333  
[ ]state.con.xml.gz2004-04-08 01:50 333  
[ ]apply_right.con.xml.gz2004-04-08 01:49 334  
[ ]p_invert.con.xml.gz2004-04-08 01:51 334  
[ ]co_valid1.con.xml.gz2004-04-08 01:51 335  
[ ]nthProp.con.xml.gz2004-04-08 01:49 336  
[ ]prop_stable.con.xml.gz2004-04-08 01:50 336  
[ ]valid2.con.xml.gz2004-04-08 01:49 338  
[ ]direction.ind.xml.gz2004-04-08 01:49 341  
[ ]p_apply_left.con.xml.gz2004-04-08 01:50 341  
[ ]p_apply_right.con.xml.gz2004-04-08 01:50 342  
[ ]t_fusion.ind.xml.gz2004-04-08 01:49 351  
[ ]apply_both.con.xml.gz2004-04-08 01:49 353  
[ ]exact_divide.con.xml.gz2004-04-08 01:50 359  
[ ]fusion.con.xml.gz2004-04-08 01:50 360  
[ ]fusion_right.con.xml.gz2004-04-08 01:50 371  
[ ]divide_and_approx.con.xml.gz2004-04-08 01:50 375  
[ ]nth_hyps.con.xml.gz2004-04-08 01:49 376  
[ ]interp_term.con.xml.gz2004-04-08 01:49 378  
[ ]extract_hyp_neg.con.xml.gz2004-04-08 01:51 382  
[ ]extract_hyp_pos.con.xml.gz2004-04-08 01:51 382  
[ ]absurd.con.body.xml.gz2004-04-08 01:49 383  
[ ]PropList.ind.xml.gz2004-04-08 01:49 384  
[ ]h_step.ind.xml.gz2004-04-08 01:49 384  
[ ]constant_neg.con.xml.gz2004-04-08 01:50 393  
[ ]constant_nul.con.xml.gz2004-04-08 01:50 393  
[ ]normalize_hyps.con.xml.gz2004-04-08 01:51 396  
[ ]constant_not_nul.con.xml.gz2004-04-08 01:50 398  
[ ]sum.con.xml.gz2004-04-08 01:50 399  
[ ]reduce_lhyps.con.xml.gz2004-04-08 01:51 401  
[ ]rewrite_stable.con.xml.gz2004-04-08 01:50 403  
[ ]do_normalize.con.xml.gz2004-04-08 01:50 405  
[ ]move_right_valid.con.xml.gz2004-04-08 01:50 406  
[ ]p_rewrite_stable.con.xml.gz2004-04-08 01:51 406  
[ ]omega_valid.con.xml.gz2004-04-08 01:50 407  
[ ]execute_omega.con.xml.gz2004-04-08 01:50 408  
[ ]valid_hyps.con.xml.gz2004-04-08 01:49 408  
[ ]negate_contradict.con.xml.gz2004-04-08 01:50 409  
[ ]merge_eq_valid.con.xml.gz2004-04-08 01:50 410  
[ ]move_right_stable.con.xml.gz2004-04-08 01:51 410  
[ ]term_rec.con.body.xml.gz2004-04-08 01:49 410  
[ ]add_norm_stable.con.xml.gz2004-04-08 01:50 411  
[ ]contradiction.con.xml.gz2004-04-08 01:50 411  
[ ]step_rec.con.body.xml.gz2004-04-08 01:49 412  
[ ]h_step_rec.con.body.xml.gz2004-04-08 01:49 414  
[ ]term_ind.con.body.xml.gz2004-04-08 01:49 414  
[ ]constant_neg_valid.con.xml.gz2004-04-08 01:50 415  
[ ]decompose_solve.con.xml.gz2004-04-08 01:51 415  
[ ]e_step_rec.con.body.xml.gz2004-04-08 01:49 415  
[ ]p_step_rec.con.body.xml.gz2004-04-08 01:49 415  
[ ]step_ind.con.body.xml.gz2004-04-08 01:49 415  
[ ]PropList_ind.con.body.xml.gz2004-04-08 01:49 416  
[ ]Tred_factor6.con.body.xml.gz2004-04-08 01:50 416  
[ ]constant_nul_valid.con.xml.gz2004-04-08 01:50 416  
[ ]interp_proposition.con.xml.gz2004-04-08 01:49 416  
[ ]scalar_norm_stable.con.xml.gz2004-04-08 01:50 416  
[ ]PropList_rec.con.body.xml.gz2004-04-08 01:49 417  
[ ]h_step_ind.con.body.xml.gz2004-04-08 01:49 417  
[ ]t_omega_rec.con.body.xml.gz2004-04-08 01:49 417  
[ ]e_step_ind.con.body.xml.gz2004-04-08 01:49 418  
[ ]p_step_ind.con.body.xml.gz2004-04-08 01:49 418  
[ ]direction_rec.con.body.xml.gz2004-04-08 01:49 419  
[ ]t_fusion_rec.con.body.xml.gz2004-04-08 01:49 419  
[ ]constant_not_nul_valid.con.xml.gz2004-04-08 01:50 421  
[ ]interp_hyps.con.xml.gz2004-04-08 01:49 421  
[ ]t_omega_ind.con.body.xml.gz2004-04-08 01:49 421  
[ ]direction_ind.con.body.xml.gz2004-04-08 01:49 422  
[ ]fusion_cancel_stable.con.xml.gz2004-04-08 01:50 422  
[ ]t_fusion_ind.con.body.xml.gz2004-04-08 01:49 422  
[ ]apply_oper_1.con.xml.gz2004-04-08 01:49 424  
[ ]proposition_rec.con.body.xml.gz2004-04-08 01:49 424  
[ ]decompose_solve_valid.con.xml.gz2004-04-08 01:51 425  
[ ]destructure_hyps.con.xml.gz2004-04-08 01:50 425  
[ ]negate_contradict_inv.con.xml.gz2004-04-08 01:50 425  
[ ]do_normalize_list.con.xml.gz2004-04-08 01:50 426  
[ ]scalar_norm_add_stable.con.xml.gz2004-04-08 01:50 426  
[ ]proposition_ind.con.body.xml.gz2004-04-08 01:49 427  
[ ]destructure_hyps_valid.con.xml.gz2004-04-08 01:50 429  
[ ]T_OMEGA10_stable.con.proof_tree.xml.gz2004-04-09 18:52 433  
[ ]T_OMEGA11_stable.con.proof_tree.xml.gz2004-04-09 18:52 433  
[ ]T_OMEGA12_stable.con.proof_tree.xml.gz2004-04-09 18:52 433  
[ ]T_OMEGA16_stable.con.proof_tree.xml.gz2004-04-09 18:52 433  
[ ]map_cons.con.xml.gz2004-04-08 01:50 434  
[ ]to_contradict.con.xml.gz2004-04-08 01:50 434  
[ ]T_OMEGA15_stable.con.proof_tree.xml.gz2004-04-09 18:52 435  
[ ]state_valid.con.xml.gz2004-04-08 01:50 435  
[ ]Tminus_def_stable.con.proof_tree.xml.gz2004-04-09 18:52 437  
[ ]Tmult_sym_stable.con.proof_tree.xml.gz2004-04-09 18:52 437  
[ ]Tplus_sym_stable.con.proof_tree.xml.gz2004-04-09 18:52 437  
[ ]Topp_plus_stable.con.proof_tree.xml.gz2004-04-09 18:52 438  
[ ]Topp_opp_stable.con.proof_tree.xml.gz2004-04-09 18:52 439  
[ ]Tred_factor0_stable.con.proof_tree.xml.gz2004-04-09 18:52 439  
[ ]Tred_factor1_stable.con.proof_tree.xml.gz2004-04-09 18:52 439  
[ ]Tred_factor2_stable.con.proof_tree.xml.gz2004-04-09 18:52 439  
[ ]Tred_factor5_stable.con.proof_tree.xml.gz2004-04-09 18:52 439  
[ ]p_step.ind.xml.gz2004-04-08 01:49 439  
[ ]Tplus_permute_stable.con.proof_tree.xml.gz2004-04-09 18:52 440  
[ ]Tred_factor3_stable.con.proof_tree.xml.gz2004-04-09 18:52 440  
[ ]Tred_factor4_stable.con.proof_tree.xml.gz2004-04-09 18:52 440  
[ ]Tred_factor6_stable.con.proof_tree.xml.gz2004-04-09 18:52 440  
[ ]Topp_one_stable.con.proof_tree.xml.gz2004-04-09 18:52 441  
[ ]apply_oper_2.con.xml.gz2004-04-08 01:49 441  
[ ]valid_list_hyps.con.xml.gz2004-04-08 01:49 441  
[ ]Topp_mult_r_stable.con.proof_tree.xml.gz2004-04-09 18:52 442  
[ ]Tplus_assoc_l_stable.con.proof_tree.xml.gz2004-04-09 18:52 442  
[ ]interp_full_goal.con.xml.gz2004-04-08 01:50 442  
[ ]valid_list_goal.con.xml.gz2004-04-08 01:49 442  
[ ]interp_goal_concl.con.xml.gz2004-04-08 01:49 443  
[ ]Tmult_assoc_r_stable.con.proof_tree.xml.gz2004-04-09 18:52 445  
[ ]Tmult_opp_left_stable.con.proof_tree.xml.gz2004-04-09 18:52 445  
[ ]Tplus_assoc_r_stable.con.proof_tree.xml.gz2004-04-09 18:52 445  
[ ]do_normalize.con.body.xml.gz2004-04-08 01:50 445  
[ ]omega_tactic.con.xml.gz2004-04-08 01:52 445  
[ ]valid_lhyps.con.xml.gz2004-04-08 01:51 446  
[ ]Tmult_plus_distr_stable.con.proof_tree.xml.gz2004-04-09 18:52 448  
[ ]do_normalize_valid.con.xml.gz2004-04-08 01:50 448  
[ ]Tred_factor0.con.body.xml.gz2004-04-08 01:50 450  
[ ]interp_list_goal.con.xml.gz2004-04-08 01:49 450  
[ ]interp_list_hyps.con.xml.gz2004-04-08 01:49 451  
[ ]not_exact_divide.con.xml.gz2004-04-08 01:50 453  
[ ]Tmult_assoc_reduced_stable.con.proof_tree.xml.gz2004-04-09 18:52 455  
[ ]fusion_stable.con.xml.gz2004-04-08 01:50 456  
[ ]negate_contradict_valid.con.xml.gz2004-04-08 01:50 457  
[ ]apply_left_stable.con.xml.gz2004-04-08 01:49 464  
[ ]p_invert_stable.con.xml.gz2004-04-08 01:51 464  
[ ]apply_right_stable.con.xml.gz2004-04-08 01:49 466  
[ ]normalize_hyps_valid.con.xml.gz2004-04-08 01:51 470  
[ ]p_apply_left_stable.con.xml.gz2004-04-08 01:50 473  
[ ]contradiction_valid.con.xml.gz2004-04-08 01:50 475  
[ ]p_apply_right_stable.con.xml.gz2004-04-08 01:51 476  
[ ]interp_full.con.xml.gz2004-04-08 01:50 482  
[ ]exact_divide_valid.con.xml.gz2004-04-08 01:50 484  
[ ]negate_contradict_inv_valid.con.xml.gz2004-04-08 01:50 485  
[ ]Zne_left_2.con.xml.gz2004-04-08 01:50 487  
[ ]do_normalize_valid.con.body.xml.gz2004-04-08 01:50 489  
[ ]sum4.con.xml.gz2004-04-08 01:50 489  
[ ]direction_rec.con.xml.gz2004-04-08 01:49 501  
[ ]term.ind.xml.gz2004-04-08 01:49 501  
[ ]direction_rect.con.xml.gz2004-04-08 01:49 503  
[ ]direction_ind.con.xml.gz2004-04-08 01:49 507  
[ ]do_normalize_list_valid.con.xml.gz2004-04-08 01:50 513  
[ ]eq_nat_true.con.xml.gz2004-04-08 01:49 513  
[ ]nth_hyps.con.body.xml.gz2004-04-08 01:49 513  
[ ]eq_term_true.con.xml.gz2004-04-08 01:49 514  
[ ]apply_oper_1_valid.con.xml.gz2004-04-08 01:49 517  
[ ]sum_valid.con.xml.gz2004-04-08 01:50 518  
[ ]t_fusion_rec.con.xml.gz2004-04-08 01:49 518  
[ ]apply_both_stable.con.xml.gz2004-04-08 01:49 521  
[ ]t_fusion_rect.con.xml.gz2004-04-08 01:49 521  
[ ]eq_Z_true.con.xml.gz2004-04-08 01:49 522  
[ ]divide_and_approx_valid.con.xml.gz2004-04-08 01:50 523  
[ ]t_fusion_ind.con.xml.gz2004-04-08 01:49 525  
[ ]Tred_factor0_stable.con.body.xml.gz2004-04-08 01:50 528  
[ ]eq_pos_true.con.xml.gz2004-04-08 01:49 529  
[ ]Tred_factor6_stable.con.body.xml.gz2004-04-08 01:50 530  
[ ]extract_valid.con.xml.gz2004-04-08 01:51 531  
[ ]eq_nat_false.con.xml.gz2004-04-08 01:49 535  
[ ]eq_Z_false.con.xml.gz2004-04-08 01:49 537  
[ ]eq_term_false.con.xml.gz2004-04-08 01:49 537  
[ ]goal_valid.con.xml.gz2004-04-08 01:49 537  
[ ]h_step_rect.con.xml.gz2004-04-08 01:49 543  
[ ]not_exact_divide_valid.con.xml.gz2004-04-08 01:50 543  
[ ]h_step_rec.con.xml.gz2004-04-08 01:49 548  
[ ]concl_to_hyp.con.body.xml.gz2004-04-08 01:52 550  
[ ]h_step_ind.con.xml.gz2004-04-08 01:49 552  
[ ]eq_pos_false.con.xml.gz2004-04-08 01:49 553  
[ ]apply_oper_2_valid.con.xml.gz2004-04-08 01:49 554  
[ ]e_step.ind.xml.gz2004-04-08 01:49 555  
[ ]Zlt_left_inv.con.xml.gz2004-04-08 01:51 559  
[ ]split_ineq.con.xml.gz2004-04-08 01:50 570  
[ ]bool_ind2.con.xml.gz2004-04-08 01:49 571  
[ ]PropList_rect.con.xml.gz2004-04-08 01:49 576  
[ ]PropList_ind.con.xml.gz2004-04-08 01:49 577  
[ ]compose_term_stable.con.xml.gz2004-04-08 01:49 578  
[ ]PropList_rec.con.xml.gz2004-04-08 01:49 579  
[ ]sum1.con.xml.gz2004-04-08 01:50 584  
[ ]term_stable.con.body.xml.gz2004-04-08 01:49 605  
[ ]sum2.con.xml.gz2004-04-08 01:50 617  
[ ]sum3.con.xml.gz2004-04-08 01:50 617  
[ ]do_reduce_lhyps.con.xml.gz2004-04-08 01:52 622  
[ ]list_hyps_to_goal.con.xml.gz2004-04-08 01:49 626  
[ ]direction_ind.con.types.xml.gz2004-04-08 01:49 630  
[ ]nth_valid.con.xml.gz2004-04-08 01:49 631  
[ ]valid1.con.body.xml.gz2004-04-08 01:49 633  
[ ]proposition.ind.xml.gz2004-04-08 01:49 636  
[ ]relation_ind2.con.xml.gz2004-04-08 01:49 639  
[ ]decidable_correct.con.xml.gz2004-04-08 01:50 648  
[ ]prop_stable.con.body.xml.gz2004-04-08 01:50 648  
[ ]apply_oper_2.con.body.xml.gz2004-04-08 01:49 649  
[ ]do_normalize_valid.con.types.xml.gz2004-04-08 01:50 651  
[ ]list_goal_to_hyps.con.xml.gz2004-04-08 01:49 652  
[ ]step.ind.xml.gz2004-04-08 01:49 656  
[ ]co_valid1.con.body.xml.gz2004-04-08 01:51 665  
[ ]t_fusion_ind.con.types.xml.gz2004-04-08 01:49 669  
[ ]h_step_ind.con.types.xml.gz2004-04-08 01:49 673  
[ ]sum5.con.xml.gz2004-04-08 01:50 679  
[ ]map_cons_val.con.xml.gz2004-04-08 01:50 682  
[ ]Tmult_sym.con.body.xml.gz2004-04-08 01:49 683  
[ ]omega_tactic.con.body.xml.gz2004-04-08 01:52 683  
[ ]h_step_rect.con.body.xml.gz2004-04-08 01:49 684  
[ ]Tplus_sym.con.body.xml.gz2004-04-08 01:49 685  
[ ]direction_rect.con.body.xml.gz2004-04-08 01:49 685  
[ ]valid_hyps.con.body.xml.gz2004-04-08 01:49 685  
[ ]valid2.con.body.xml.gz2004-04-08 01:49 695  
[ ]p_step_rect.con.xml.gz2004-04-08 01:49 700  
[ ]Tminus_def.con.body.xml.gz2004-04-08 01:50 702  
[ ]p_step_rec.con.xml.gz2004-04-08 01:49 702  
[ ]do_omega.con.xml.gz2004-04-08 01:52 707  
[ ]p_step_ind.con.xml.gz2004-04-08 01:49 708  
[ ]valid_list_hyps.con.body.xml.gz2004-04-08 01:49 716  
[ ]execute_goal.con.body.xml.gz2004-04-08 01:50 720  
[ ]t_fusion_rect.con.body.xml.gz2004-04-08 01:49 721  
[ ]Topp_one.con.body.xml.gz2004-04-08 01:50 730  
[ ]valid_lhyps.con.body.xml.gz2004-04-08 01:51 739  
[ ]split_ineq_valid.con.xml.gz2004-04-08 01:50 740  
[ ]fusion_cancel.con.body.xml.gz2004-04-08 01:50 744  
[ ]interp_full_false.con.xml.gz2004-04-08 01:50 747  
[ ]append_goal.con.xml.gz2004-04-08 01:50 759  
[ ]add_norm.con.body.xml.gz2004-04-08 01:50 764  
[ ]append_valid.con.xml.gz2004-04-08 01:49 765  
[ ]scalar_norm.con.body.xml.gz2004-04-08 01:50 767  
[ ]PropList_ind.con.types.xml.gz2004-04-08 01:49 773  
[ ]scalar_norm_add.con.body.xml.gz2004-04-08 01:50 773  
[ ]hyps_to_goal.con.xml.gz2004-04-08 01:49 786  
[ ]apply_right.con.body.xml.gz2004-04-08 01:49 797  
[ ]goal_to_hyps.con.xml.gz2004-04-08 01:49 810  
[ ]interp_full.con.body.xml.gz2004-04-08 01:50 815  
[ ]execute_goal.con.xml.gz2004-04-08 01:50 830  
[ ]Tred_factor6_stable.con.types.xml.gz2004-04-08 01:50 833  
[ ]apply_left.con.body.xml.gz2004-04-08 01:49 835  
[ ]apply_both.con.body.xml.gz2004-04-08 01:49 838  
[ ]to_contradict_valid.con.xml.gz2004-04-08 01:50 842  
[ ]p_rewrite.con.body.xml.gz2004-04-08 01:51 856  
[ ]do_reduce_lhyps.con.body.xml.gz2004-04-08 01:52 863  
[ ]do_concl_to_hyp.con.xml.gz2004-04-08 01:52 865  
[ ]Tred_factor0_stable.con.types.xml.gz2004-04-08 01:50 866  
[ ]e_step_rect.con.xml.gz2004-04-08 01:49 888  
[ ]Topp_opp.con.body.xml.gz2004-04-08 01:49 889  
[ ]e_step_rec.con.xml.gz2004-04-08 01:49 891  
[ ]Tred_factor1.con.body.xml.gz2004-04-08 01:50 892  
[ ]e_step_ind.con.xml.gz2004-04-08 01:49 893  
[ ]valid_list_goal.con.body.xml.gz2004-04-08 01:49 912  
[ ]sum1.con.types.xml.gz2004-04-08 01:50 913  
[ ]normalize_hyps_goal.con.body.xml.gz2004-04-08 01:51 920  
[ ]normalize_hyps_goal.con.xml.gz2004-04-08 01:51 931  
[ ]to_contradict.con.body.xml.gz2004-04-08 01:50 935  
[ ]eq_nat.con.body.xml.gz2004-04-08 01:49 940  
[ ]PropList_rect.con.body.xml.gz2004-04-08 01:49 952  
[ ]normalize_goal.con.body.xml.gz2004-04-08 01:50 953  
[ ]normalize_goal.con.xml.gz2004-04-08 01:50 964  
[ ]Topp_plus.con.body.xml.gz2004-04-08 01:49 966  
[ ]sum1.con.body.xml.gz2004-04-08 01:50 967  
[ ]Tplus_assoc_r.con.body.xml.gz2004-04-08 01:49 1.0K 
[ ]Tplus_assoc_l.con.body.xml.gz2004-04-08 01:49 1.0K 
[ ]Tplus_permute.con.body.xml.gz2004-04-08 01:49 1.0K 
[ ]goal_valid.con.body.xml.gz2004-04-08 01:49 1.0K 
[ ]Tmult_assoc_r.con.body.xml.gz2004-04-08 01:49 1.0K 
[ ]interp_hyps.con.body.xml.gz2004-04-08 01:49 1.0K 
[ ]valid_goal.con.xml.gz2004-04-08 01:49 1.0K 
[ ]eq_Z.con.body.xml.gz2004-04-08 01:49 1.0K 
[ ]term_rect.con.xml.gz2004-04-08 01:49 1.0K 
[ ]term_rec.con.xml.gz2004-04-08 01:49 1.0K 
[ ]Tmult_plus_distr.con.body.xml.gz2004-04-08 01:50 1.0K 
[ ]term_ind.con.xml.gz2004-04-08 01:49 1.0K 
[ ]nthProp.con.body.xml.gz2004-04-08 01:49 1.0K 
[ ]p_apply_right.con.body.xml.gz2004-04-08 01:50 1.0K 
[ ]do_normalize_list.con.body.xml.gz2004-04-08 01:50 1.0K 
[ ]fusion_right.con.body.xml.gz2004-04-08 01:50 1.0K 
[ ]p_apply_left.con.body.xml.gz2004-04-08 01:50 1.0K 
[ ]t_omega.ind.xml.gz2004-04-08 01:49 1.0K 
[ ]p_step_ind.con.types.xml.gz2004-04-08 01:49 1.0K 
[ ]do_reduce_lhyps.con.types.xml.gz2004-04-08 01:52 1.1K 
[ ]interp_list_hyps.con.body.xml.gz2004-04-08 01:49 1.1K 
[ ]bool_ind2.con.body.xml.gz2004-04-08 01:49 1.1K 
[ ]eq_pos.con.body.xml.gz2004-04-08 01:49 1.1K 
[ ]interp_full_goal.con.body.xml.gz2004-04-08 01:50 1.1K 
[ ]interp_goal_concl.con.body.xml.gz2004-04-08 01:49 1.1K 
[ ]apply_oper_2_valid.con.body.xml.gz2004-04-08 01:49 1.1K 
[ ]bool_ind2.con.types.xml.gz2004-04-08 01:49 1.1K 
[ ]valid_goal.con.body.xml.gz2004-04-08 01:49 1.1K 
[ ]execute_goal.con.types.xml.gz2004-04-08 01:50 1.1K 
[ ]normalize_hyps.con.body.xml.gz2004-04-08 01:51 1.1K 
[ ]decidability.con.body.xml.gz2004-04-08 01:50 1.1K 
[ ]p_invert.con.body.xml.gz2004-04-08 01:51 1.1K 
[ ]rewrite.con.body.xml.gz2004-04-08 01:50 1.1K 
[ ]map_cons.con.body.xml.gz2004-04-08 01:50 1.1K 
[ ]fusion.con.body.xml.gz2004-04-08 01:50 1.1K 
[ ]compose_term_stable.con.body.xml.gz2004-04-08 01:49 1.2K 
[ ]interp_term.con.body.xml.gz2004-04-08 01:49 1.2K 
[ ]do_normalize_valid.con.proof_tree.xml.gz2004-04-09 18:52 1.2K 
[ ]p_step_rect.con.body.xml.gz2004-04-08 01:49 1.2K 
[ ]p_rewrite_stable.con.body.xml.gz2004-04-08 01:51 1.2K 
[ ]step_rec.con.xml.gz2004-04-08 01:49 1.2K 
[ ]Topp_mult_r.con.body.xml.gz2004-04-08 01:50 1.2K 
[ ]step_ind.con.xml.gz2004-04-08 01:49 1.2K 
[ ]apply_oper_1.con.body.xml.gz2004-04-08 01:49 1.2K 
[ ]step_rect.con.xml.gz2004-04-08 01:49 1.2K 
[ ]Tmult_opp_left.con.body.xml.gz2004-04-08 01:50 1.2K 
[ ]e_step_ind.con.types.xml.gz2004-04-08 01:49 1.3K 
[ ]do_omega.con.body.xml.gz2004-04-08 01:52 1.3K 
[ ]interp_list_goal.con.body.xml.gz2004-04-08 01:49 1.3K 
[ ]Tred_factor5.con.body.xml.gz2004-04-08 01:49 1.3K 
[ ]Zne_left_2.con.body.xml.gz2004-04-08 01:50 1.3K 
[ ]Zne_left_2.con.types.xml.gz2004-04-08 01:50 1.4K 
[ ]proposition_rec.con.xml.gz2004-04-08 01:49 1.4K 
[ ]proposition_ind.con.xml.gz2004-04-08 01:49 1.4K 
[ ]proposition_rect.con.xml.gz2004-04-08 01:49 1.4K 
[ ]Tred_factor2.con.body.xml.gz2004-04-08 01:50 1.4K 
[ ]Tred_factor3.con.body.xml.gz2004-04-08 01:50 1.4K 
[ ]move_right.con.body.xml.gz2004-04-08 01:50 1.4K 
[ ]do_normalize_list_valid.con.body.xml.gz2004-04-08 01:50 1.4K 
[ ]goal_to_hyps.con.body.xml.gz2004-04-08 01:49 1.5K 
[ ]relation_ind2.con.body.xml.gz2004-04-08 01:49 1.5K 
[ ]relation_ind2.con.types.xml.gz2004-04-08 01:49 1.5K 
[ ]Topp_one_stable.con.body.xml.gz2004-04-08 01:50 1.5K 
[ ]Tminus_def_stable.con.body.xml.gz2004-04-08 01:50 1.5K 
[ ]e_step_rect.con.body.xml.gz2004-04-08 01:49 1.5K 
[ ]Tmult_sym_stable.con.body.xml.gz2004-04-08 01:49 1.5K 
[ ]Tplus_sym_stable.con.body.xml.gz2004-04-08 01:49 1.5K 
[ ]sum1.con.proof_tree.xml.gz2004-04-09 18:52 1.5K 
[ ]Tmult_assoc_reduced.con.body.xml.gz2004-04-08 01:50 1.6K 
[ ]term_ind.con.types.xml.gz2004-04-08 01:49 1.6K 
[ ]apply_oper_2_valid.con.types.xml.gz2004-04-08 01:49 1.6K 
[ ]sum4.con.body.xml.gz2004-04-08 01:50 1.6K 
[ ]exact_divide.con.body.xml.gz2004-04-08 01:50 1.7K 
[ ]bool_ind2.con.proof_tree.xml.gz2004-04-09 18:52 1.7K 
[ ]interp_full_false.con.body.xml.gz2004-04-08 01:50 1.7K 
[ ]hyps_to_goal.con.body.xml.gz2004-04-08 01:49 1.7K 
[ ]execute_goal.con.proof_tree.xml.gz2004-04-09 18:52 1.7K 
[ ]list_goal_to_hyps.con.body.xml.gz2004-04-08 01:49 1.7K 
[ ]term_rect.con.body.xml.gz2004-04-08 01:49 1.7K 
[ ]goal_valid.con.types.xml.gz2004-04-08 01:49 1.8K 
[ ]compose_term_stable.con.types.xml.gz2004-04-08 01:49 1.8K 
[ ]interp_proposition.con.body.xml.gz2004-04-08 01:49 1.8K 
[ ]do_reduce_lhyps.con.proof_tree.xml.gz2004-04-09 18:52 1.8K 
[ ]normalize_goal.con.types.xml.gz2004-04-08 01:50 1.9K 
[ ]T_OMEGA16.con.body.xml.gz2004-04-08 01:49 1.9K 
[ ]p_rewrite_stable.con.types.xml.gz2004-04-08 01:51 1.9K 
[ ]normalize_hyps_goal.con.types.xml.gz2004-04-08 01:51 1.9K 
[ ]divide_and_approx.con.body.xml.gz2004-04-08 01:50 1.9K 
[ ]constant_neg.con.body.xml.gz2004-04-08 01:50 1.9K 
[ ]constant_not_nul.con.body.xml.gz2004-04-08 01:50 1.9K 
[ ]constant_nul.con.body.xml.gz2004-04-08 01:50 1.9K 
[ ]list_hyps_to_goal.con.body.xml.gz2004-04-08 01:49 1.9K 
[ ]Tred_factor4.con.body.xml.gz2004-04-08 01:50 2.0K 
[ ]t_omega_rect.con.xml.gz2004-04-08 01:49 2.0K 
[ ]t_omega_rec.con.xml.gz2004-04-08 01:49 2.0K 
[ ]t_omega_ind.con.xml.gz2004-04-08 01:49 2.0K 
[ ]rewrite_stable.con.body.xml.gz2004-04-08 01:50 2.0K 
[ ]sum4.con.types.xml.gz2004-04-08 01:50 2.1K 
[ ]relation_ind2.con.proof_tree.xml.gz2004-04-09 18:52 2.1K 
[ ]normalize_hyps_goal.con.proof_tree.xml.gz2004-04-09 18:52 2.1K 
[ ]not_exact_divide.con.body.xml.gz2004-04-08 01:50 2.2K 
[ ]apply_right_stable.con.body.xml.gz2004-04-08 01:49 2.2K 
[ ]step_ind.con.types.xml.gz2004-04-08 01:49 2.2K 
[ ]fusion_cancel_stable.con.body.xml.gz2004-04-08 01:50 2.2K 
[ ]eq_term.con.body.xml.gz2004-04-08 01:49 2.2K 
[ ]normalize_goal.con.proof_tree.xml.gz2004-04-09 18:52 2.2K 
[ ]T_OMEGA11.con.body.xml.gz2004-04-08 01:49 2.2K 
[ ]T_OMEGA12.con.body.xml.gz2004-04-08 01:49 2.2K 
[ ]map_cons_val.con.body.xml.gz2004-04-08 01:50 2.2K 
[ ]Zne_left_2.con.proof_tree.xml.gz2004-04-09 18:52 2.3K 
[ ]do_concl_to_hyp.con.proof_tree.xml.gz2004-04-09 18:52 2.3K 
[ ]fusion_stable.con.body.xml.gz2004-04-08 01:50 2.3K 
[ ]Zlt_left_inv.con.types.xml.gz2004-04-08 01:51 2.3K 
[ ]step_rect.con.body.xml.gz2004-04-08 01:49 2.3K 
[ ]proposition_ind.con.types.xml.gz2004-04-08 01:49 2.4K 
[ ]eq_nat_true.con.body.xml.gz2004-04-08 01:49 2.4K 
[ ]do_normalize_list_valid.con.types.xml.gz2004-04-08 01:50 2.4K 
[ ]apply_left_stable.con.body.xml.gz2004-04-08 01:49 2.4K 
[ ]to_contradict_valid.con.body.xml.gz2004-04-08 01:50 2.4K 
[ ]valid_goal.con.types.xml.gz2004-04-08 01:49 2.4K 
[ ]merge_eq.con.body.xml.gz2004-04-08 01:50 2.4K 
[ ]Zlt_left_inv.con.body.xml.gz2004-04-08 01:51 2.5K 
[ ]hyps_to_goal.con.types.xml.gz2004-04-08 01:49 2.5K 
[ ]proposition_rect.con.body.xml.gz2004-04-08 01:49 2.6K 
[ ]Zlt_left_inv.con.proof_tree.xml.gz2004-04-09 18:52 2.7K 
[ ]do_omega.con.types.xml.gz2004-04-08 01:52 2.7K 
[ ]add_norm_stable.con.body.xml.gz2004-04-08 01:50 2.7K 
[ ]scalar_norm_stable.con.body.xml.gz2004-04-08 01:50 2.7K 
[ ]scalar_norm_add_stable.con.body.xml.gz2004-04-08 01:50 2.7K 
[ ]nth_valid.con.body.xml.gz2004-04-08 01:49 2.7K 
[ ]Topp_opp_stable.con.body.xml.gz2004-04-08 01:49 2.7K 
[ ]goal_valid.con.proof_tree.xml.gz2004-04-09 18:52 2.8K 
[ ]list_hyps_to_goal.con.types.xml.gz2004-04-08 01:49 2.8K 
[ ]valid_goal.con.proof_tree.xml.gz2004-04-09 18:52 2.8K 
[ ]reduce_lhyps.con.body.xml.gz2004-04-08 01:51 2.9K 
[ ]Tred_factor1_stable.con.body.xml.gz2004-04-08 01:50 2.9K 
[ ]Topp_plus_stable.con.body.xml.gz2004-04-08 01:49 2.9K 
[ ]eq_nat_true.con.types.xml.gz2004-04-08 01:49 2.9K 
[ ]apply_oper_1_valid.con.body.xml.gz2004-04-08 01:49 2.9K 
[ ]sum2.con.body.xml.gz2004-04-08 01:50 2.9K 
[ ]append_goal.con.body.xml.gz2004-04-08 01:50 2.9K 
[ ]state.con.body.xml.gz2004-04-08 01:50 2.9K 
[ ]sum4.con.proof_tree.xml.gz2004-04-09 18:52 3.0K 
[ ]apply_both_stable.con.body.xml.gz2004-04-08 01:49 3.0K 
[ ]list_goal_to_hyps.con.types.xml.gz2004-04-08 01:49 3.0K 
[ ]Tplus_assoc_r_stable.con.body.xml.gz2004-04-08 01:49 3.0K 
[ ]Tplus_assoc_l_stable.con.body.xml.gz2004-04-08 01:49 3.0K 
[ ]Tplus_permute_stable.con.body.xml.gz2004-04-08 01:49 3.0K 
[ ]compose_term_stable.con.proof_tree.xml.gz2004-04-09 18:52 3.0K 
[ ]Tmult_assoc_r_stable.con.body.xml.gz2004-04-08 01:49 3.0K 
[ ]Tmult_plus_distr_stable.con.body.xml.gz2004-04-08 01:50 3.1K 
[ ]normalize_hyps_valid.con.body.xml.gz2004-04-08 01:51 3.1K 
[ ]eq_nat_false.con.body.xml.gz2004-04-08 01:49 3.1K 
[ ]apply_oper_2_valid.con.proof_tree.xml.gz2004-04-09 18:52 3.1K 
[ ]contradiction.con.body.xml.gz2004-04-08 01:50 3.1K 
[ ]p_rewrite_stable.con.proof_tree.xml.gz2004-04-09 18:52 3.2K 
[ ]execute_omega.con.body.xml.gz2004-04-08 01:50 3.3K 
[ ]do_concl_to_hyp.con.body.xml.gz2004-04-08 01:52 3.4K 
[ ]append_valid.con.body.xml.gz2004-04-08 01:49 3.4K 
[ ]do_omega.con.proof_tree.xml.gz2004-04-09 18:52 3.4K 
[ ]T_OMEGA15.con.body.xml.gz2004-04-08 01:49 3.4K 
[ ]map_cons_val.con.types.xml.gz2004-04-08 01:50 3.4K 
[ ]t_omega_ind.con.types.xml.gz2004-04-08 01:49 3.4K 
[ ]split_ineq.con.body.xml.gz2004-04-08 01:50 3.6K 
[ ]eq_nat_false.con.types.xml.gz2004-04-08 01:49 3.7K 
[ ]goal_to_hyps.con.types.xml.gz2004-04-08 01:49 3.8K 
[ ]t_omega_rect.con.body.xml.gz2004-04-08 01:49 3.8K 
[ ]negate_contradict.con.body.xml.gz2004-04-08 01:50 3.8K 
[ ]normalize_hyps_valid.con.types.xml.gz2004-04-08 01:51 3.8K 
[ ]eq_Z_true.con.body.xml.gz2004-04-08 01:49 3.9K 
[ ]list_hyps_to_goal.con.proof_tree.xml.gz2004-04-09 18:52 3.9K 
[ ]apply_right_stable.con.types.xml.gz2004-04-08 01:49 3.9K 
[ ]reduce.con.body.xml.gz2004-04-08 01:50 3.9K 
[ ]eq_nat_true.con.proof_tree.xml.gz2004-04-09 18:52 4.0K 
[ ]T_OMEGA13.con.body.xml.gz2004-04-08 01:49 4.0K 
[ ]eq_pos_true.con.body.xml.gz2004-04-08 01:49 4.0K 
[ ]apply_left_stable.con.types.xml.gz2004-04-08 01:49 4.1K 
[ ]fusion_cancel_stable.con.types.xml.gz2004-04-08 01:50 4.1K 
[ ]hyps_to_goal.con.proof_tree.xml.gz2004-04-09 18:52 4.1K 
[ ]negate_contradict_inv.con.body.xml.gz2004-04-08 01:50 4.1K 
[ ]T_OMEGA10.con.body.xml.gz2004-04-08 01:49 4.1K 
[ ]nth_valid.con.types.xml.gz2004-04-08 01:49 4.2K 
[ ]rewrite_stable.con.types.xml.gz2004-04-08 01:50 4.2K 
[ ]append_goal.con.types.xml.gz2004-04-08 01:50 4.2K 
[ ]goal_to_hyps.con.proof_tree.xml.gz2004-04-09 18:52 4.3K 
[ ]apply_right_stable.con.proof_tree.xml.gz2004-04-09 18:52 4.3K 
[ ]fusion_stable.con.types.xml.gz2004-04-08 01:50 4.5K 
[ ]list_goal_to_hyps.con.proof_tree.xml.gz2004-04-09 18:52 4.5K 
[ ]do_normalize_list_valid.con.proof_tree.xml.gz2004-04-09 18:52 4.6K 
[ ]add_norm_stable.con.types.xml.gz2004-04-08 01:50 4.6K 
[ ]scalar_norm_stable.con.types.xml.gz2004-04-08 01:50 4.6K 
[ ]apply_left_stable.con.proof_tree.xml.gz2004-04-09 18:52 4.6K 
[ ]scalar_norm_add_stable.con.types.xml.gz2004-04-08 01:50 4.6K 
[ ]to_contradict_valid.con.types.xml.gz2004-04-08 01:50 4.6K 
[ ]map_cons_val.con.proof_tree.xml.gz2004-04-09 18:52 4.7K 
[ ]decompose_solve.con.body.xml.gz2004-04-08 01:51 4.7K 
[ ]apply_both_stable.con.types.xml.gz2004-04-08 01:49 4.8K 
[ ]apply_oper_1_valid.con.types.xml.gz2004-04-08 01:49 4.8K 
[ ]append_valid.con.types.xml.gz2004-04-08 01:49 4.8K 
[ ]Topp_mult_r_stable.con.body.xml.gz2004-04-08 01:50 4.8K 
[ ]extract_hyp_pos.con.body.xml.gz2004-04-08 01:51 4.9K 
[ ]extract_hyp_neg.con.body.xml.gz2004-04-08 01:51 4.9K 
[ ]append_valid.con.proof_tree.xml.gz2004-04-09 18:52 5.0K 
[ ]Tmult_opp_left_stable.con.body.xml.gz2004-04-08 01:50 5.0K 
[ ]destructure_hyps.con.body.xml.gz2004-04-08 01:50 5.0K 
[ ]sum5.con.body.xml.gz2004-04-08 01:50 5.2K 
[ ]append_goal.con.proof_tree.xml.gz2004-04-09 18:52 5.2K 
[ ]fusion_stable.con.proof_tree.xml.gz2004-04-09 18:52 5.2K 
[ ]eq_Z_false.con.body.xml.gz2004-04-08 01:49 5.3K 
[ ]interp_full_false.con.types.xml.gz2004-04-08 01:50 5.3K 
[ ]fusion_cancel_stable.con.proof_tree.xml.gz2004-04-09 18:52 5.3K 
[ ]apply_both_stable.con.proof_tree.xml.gz2004-04-09 18:52 5.4K 
[ ]decidable_correct.con.body.xml.gz2004-04-08 01:50 5.6K 
[ ]eq_nat_false.con.proof_tree.xml.gz2004-04-09 18:52 5.6K 
[ ]eq_pos_false.con.body.xml.gz2004-04-08 01:49 5.7K 
[ ]interp_full_false.con.proof_tree.xml.gz2004-04-09 18:52 5.7K 
[ ]sum5.con.types.xml.gz2004-04-08 01:50 6.0K 
[ ]eq_Z_true.con.types.xml.gz2004-04-08 01:49 6.1K 
[ ]omega_valid.con.body.xml.gz2004-04-08 01:50 6.1K 
[ ]eq_Z_true.con.proof_tree.xml.gz2004-04-09 18:52 6.2K 
[ ]Tred_factor5_stable.con.body.xml.gz2004-04-08 01:49 6.2K 
[ ]move_right_valid.con.body.xml.gz2004-04-08 01:50 6.3K 
[ ]eq_pos_true.con.types.xml.gz2004-04-08 01:49 6.4K 
[ ]sum.con.body.xml.gz2004-04-08 01:50 6.6K 
[ ]Tplus_sym_stable.con.types.xml.gz2004-04-08 01:49 6.6K 
[ ]add_norm_stable.con.proof_tree.xml.gz2004-04-09 18:52 6.7K 
[ ]scalar_norm_stable.con.proof_tree.xml.gz2004-04-09 18:52 6.7K 
[ ]Tmult_sym_stable.con.types.xml.gz2004-04-08 01:49 6.7K 
[ ]scalar_norm_add_stable.con.proof_tree.xml.gz2004-04-09 18:52 6.7K 
[ ]Tminus_def_stable.con.types.xml.gz2004-04-08 01:50 6.8K 
[ ]eq_Z_false.con.types.xml.gz2004-04-08 01:49 6.9K 
[ ]Topp_one_stable.con.types.xml.gz2004-04-08 01:50 6.9K 
[ ]Tred_factor3_stable.con.body.xml.gz2004-04-08 01:50 7.0K 
[ ]Tred_factor2_stable.con.body.xml.gz2004-04-08 01:50 7.0K 
[ ]do_concl_to_hyp.con.types.xml.gz2004-04-08 01:52 7.0K 
[ ]eq_pos_true.con.proof_tree.xml.gz2004-04-09 18:52 7.0K 
[ ]rewrite_stable.con.proof_tree.xml.gz2004-04-09 18:52 7.1K 
[ ]to_contradict_valid.con.proof_tree.xml.gz2004-04-09 18:52 7.1K 
[ ]eq_pos_false.con.types.xml.gz2004-04-08 01:49 7.1K 
[ ]apply_oper_1_valid.con.proof_tree.xml.gz2004-04-09 18:52 7.2K 
[ ]nth_valid.con.proof_tree.xml.gz2004-04-09 18:52 7.3K 
[ ]sum2.con.types.xml.gz2004-04-08 01:50 7.7K 
[ ]Tmult_assoc_reduced_stable.con.body.xml.gz2004-04-08 01:50 7.7K 
[ ]normalize_hyps_valid.con.proof_tree.xml.gz2004-04-09 18:52 7.9K 
[ ]sum5.con.proof_tree.xml.gz2004-04-09 18:52 8.0K 
[ ]eq_Z_false.con.proof_tree.xml.gz2004-04-09 18:52 9.1K 
[ ]sum2.con.proof_tree.xml.gz2004-04-09 18:52 9.6K 
[ ]constant_not_nul_valid.con.body.xml.gz2004-04-08 01:50 9.7K 
[ ]constant_neg_valid.con.body.xml.gz2004-04-08 01:50 9.7K 
[ ]eq_pos_false.con.proof_tree.xml.gz2004-04-09 18:52 10K 
[ ]constant_nul_valid.con.body.xml.gz2004-04-08 01:50 10K 
[ ]decidable_correct.con.types.xml.gz2004-04-08 01:50 10K 
[ ]Tred_factor1_stable.con.types.xml.gz2004-04-08 01:50 11K 
[ ]p_apply_right_stable.con.body.xml.gz2004-04-08 01:51 12K 
[ ]p_apply_left_stable.con.body.xml.gz2004-04-08 01:50 12K 
[ ]T_OMEGA16_stable.con.body.xml.gz2004-04-08 01:49 12K 
[ ]omega_valid.con.types.xml.gz2004-04-08 01:50 12K 
[ ]divide_and_approx_valid.con.body.xml.gz2004-04-08 01:50 13K 
[ ]INDEX2005-07-05 08:11 13K 
[ ]exact_divide_valid.con.body.xml.gz2004-04-08 01:50 14K 
[ ]Tred_factor4_stable.con.body.xml.gz2004-04-08 01:50 14K 
[ ]not_exact_divide_valid.con.body.xml.gz2004-04-08 01:50 15K 
[ ]decidable_correct.con.proof_tree.xml.gz2004-04-09 18:52 15K 
[ ]split_ineq_valid.con.body.xml.gz2004-04-08 01:50 15K 
[ ]eq_term_true.con.body.xml.gz2004-04-08 01:49 17K 
[ ]p_apply_right_stable.con.proof_tree.xml.gz2004-04-09 18:52 17K 
[ ]p_apply_left_stable.con.proof_tree.xml.gz2004-04-09 18:52 17K 
[ ]Topp_opp_stable.con.types.xml.gz2004-04-08 01:49 17K 
[ ]T_OMEGA11_stable.con.body.xml.gz2004-04-08 01:49 18K 
[ ]T_OMEGA12_stable.con.body.xml.gz2004-04-08 01:49 18K 
[ ]Topp_plus_stable.con.types.xml.gz2004-04-08 01:49 18K 
[ ]move_right_stable.con.body.xml.gz2004-04-08 01:51 18K 
[ ]Tplus_assoc_r_stable.con.types.xml.gz2004-04-08 01:49 19K 
[ ]Tplus_permute_stable.con.types.xml.gz2004-04-08 01:49 19K 
[ ]Tplus_assoc_l_stable.con.types.xml.gz2004-04-08 01:49 19K 
[ ]Tmult_assoc_r_stable.con.types.xml.gz2004-04-08 01:49 19K 
[ ]merge_eq_valid.con.body.xml.gz2004-04-08 01:50 19K 
[ ]Tmult_plus_distr_stable.con.types.xml.gz2004-04-08 01:50 19K 
[ ]decompose_solve_valid.con.body.xml.gz2004-04-08 01:51 20K 
[ ]reduce_stable.con.body.xml.gz2004-04-08 01:50 21K 
[ ]move_right_valid.con.proof_tree.xml.gz2004-04-09 18:52 22K 
[ ]extract_valid.con.body.xml.gz2004-04-08 01:51 23K 
[ ]p_apply_right_stable.con.types.xml.gz2004-04-08 01:51 23K 
[ ]p_apply_left_stable.con.types.xml.gz2004-04-08 01:50 23K 
[ ]contradiction_valid.con.body.xml.gz2004-04-08 01:50 24K 
[ ]state_valid.con.body.xml.gz2004-04-08 01:50 26K 
[ ]eq_term_true.con.proof_tree.xml.gz2004-04-09 18:52 26K 
[ ]p_invert_stable.con.body.xml.gz2004-04-08 01:51 28K 
[ ]constant_nul_valid.con.proof_tree.xml.gz2004-04-09 18:52 31K 
[ ]constant_neg_valid.con.proof_tree.xml.gz2004-04-09 18:52 31K 
[ ]constant_not_nul_valid.con.proof_tree.xml.gz2004-04-09 18:52 31K 
[ ]eq_term_false.con.body.xml.gz2004-04-08 01:49 32K 
[ ]omega_valid.con.proof_tree.xml.gz2004-04-09 18:52 32K 
[ ]negate_contradict_valid.con.body.xml.gz2004-04-08 01:50 32K 
[ ]destructure_hyps_valid.con.body.xml.gz2004-04-08 01:50 33K 
[ ]eq_term_true.con.types.xml.gz2004-04-08 01:49 33K 
[ ]Topp_mult_r_stable.con.types.xml.gz2004-04-08 01:50 36K 
[ ]exact_divide_valid.con.proof_tree.xml.gz2004-04-09 18:52 37K 
[ ]sum3.con.body.xml.gz2004-04-08 01:50 37K 
[ ]move_right_valid.con.types.xml.gz2004-04-08 01:50 38K 
[ ]Tmult_opp_left_stable.con.types.xml.gz2004-04-08 01:50 38K 
[ ]negate_contradict_inv_valid.con.body.xml.gz2004-04-08 01:50 38K 
[ ]divide_and_approx_valid.con.proof_tree.xml.gz2004-04-09 18:52 39K 
[ ]eq_term_false.con.types.xml.gz2004-04-08 01:49 40K 
[ ]eq_term_false.con.proof_tree.xml.gz2004-04-09 18:52 40K 
[ ]not_exact_divide_valid.con.proof_tree.xml.gz2004-04-09 18:52 42K 
[ ]reduce_stable.con.proof_tree.xml.gz2004-04-09 18:52 43K 
[ ]T_OMEGA15_stable.con.body.xml.gz2004-04-08 01:49 44K 
[ ]Tred_factor5_stable.con.types.xml.gz2004-04-08 01:49 46K 
[ ]extract_valid.con.proof_tree.xml.gz2004-04-09 18:52 46K 
[ ]split_ineq_valid.con.proof_tree.xml.gz2004-04-09 18:52 47K 
[ ]move_right_stable.con.proof_tree.xml.gz2004-04-09 18:52 47K 
[ ]Tred_factor3_stable.con.types.xml.gz2004-04-08 01:50 48K 
[ ]Tred_factor2_stable.con.types.xml.gz2004-04-08 01:50 48K 
[ ]extract_valid.con.types.xml.gz2004-04-08 01:51 55K 
[ ]decompose_solve_valid.con.proof_tree.xml.gz2004-04-09 18:52 57K 
[ ]p_invert_stable.con.types.xml.gz2004-04-08 01:51 57K 
[ ]constant_not_nul_valid.con.types.xml.gz2004-04-08 01:50 61K 
[ ]destructure_hyps_valid.con.types.xml.gz2004-04-08 01:50 62K 
[ ]constant_nul_valid.con.types.xml.gz2004-04-08 01:50 62K 
[ ]constant_neg_valid.con.types.xml.gz2004-04-08 01:50 63K 
[ ]merge_eq_valid.con.proof_tree.xml.gz2004-04-09 18:52 63K 
[ ]sum_valid.con.body.xml.gz2004-04-08 01:50 64K 
[ ]Tmult_assoc_reduced_stable.con.types.xml.gz2004-04-08 01:50 65K 
[ ]T_OMEGA10_stable.con.body.xml.gz2004-04-08 01:49 68K 
[ ]destructure_hyps_valid.con.proof_tree.xml.gz2004-04-09 18:52 69K 
[ ]contradiction_valid.con.proof_tree.xml.gz2004-04-09 18:52 69K 
[ ]not_exact_divide_valid.con.types.xml.gz2004-04-08 01:50 70K 
[ ]T_OMEGA13_stable.con.body.xml.gz2004-04-08 01:49 70K 
[ ]p_invert_stable.con.proof_tree.xml.gz2004-04-09 18:52 73K 
[ ]divide_and_approx_valid.con.types.xml.gz2004-04-08 01:50 83K 
[ ]move_right_stable.con.types.xml.gz2004-04-08 01:51 84K 
[ ]negate_contradict_valid.con.proof_tree.xml.gz2004-04-09 18:52 84K 
[ ]state_valid.con.proof_tree.xml.gz2004-04-09 18:52 85K 
[ ]exact_divide_valid.con.types.xml.gz2004-04-08 01:50 88K 
[ ]reduce_stable.con.types.xml.gz2004-04-08 01:50 90K 
[ ]negate_contradict_inv_valid.con.proof_tree.xml.gz2004-04-09 18:52 96K 
[ ]T_OMEGA16_stable.con.types.xml.gz2004-04-08 01:49 111K 
[ ]reduce_lhyps_valid.con.proof_tree.xml.gz2004-04-09 18:52 116K 
[ ]Tred_factor4_stable.con.types.xml.gz2004-04-08 01:50 123K 
[ ]T_OMEGA11_stable.con.types.xml.gz2004-04-08 01:49 168K 
[ ]T_OMEGA12_stable.con.types.xml.gz2004-04-08 01:49 168K 
[ ]sum3.con.proof_tree.xml.gz2004-04-09 18:52 179K 
[ ]sum3.con.types.xml.gz2004-04-08 01:50 180K 
[ ]split_ineq_valid.con.types.xml.gz2004-04-08 01:50 194K 
[ ]contradiction_valid.con.types.xml.gz2004-04-08 01:50 194K 
[ ]sum_valid.con.proof_tree.xml.gz2004-04-09 18:52 214K 
[ ]negate_contradict_valid.con.types.xml.gz2004-04-08 01:50 242K 
[ ]merge_eq_valid.con.types.xml.gz2004-04-08 01:50 250K 
[ ]negate_contradict_inv_valid.con.types.xml.gz2004-04-08 01:50 266K 
[ ]decompose_solve_valid.con.types.xml.gz2004-04-08 01:51 271K 
[ ]T_OMEGA13_stable.con.proof_tree.xml.gz2004-04-09 18:52 284K 
[ ]reduce_lhyps_valid.con.body.xml.gz2004-04-08 01:52 375K 
[ ]state_valid.con.types.xml.gz2004-04-08 01:50 396K 
[ ]T_OMEGA15_stable.con.types.xml.gz2004-04-08 01:49 448K 
[ ]T_OMEGA13_stable.con.types.xml.gz2004-04-08 01:49 625K 
[ ]T_OMEGA10_stable.con.types.xml.gz2004-04-08 01:49 703K 
[ ]sum_valid.con.types.xml.gz2004-04-08 01:50 922K 
[ ]reduce_lhyps_valid.con.types.xml.gz2004-04-08 01:52 1.1M 
Apache/2.4.61 (Debian) Server at mowgli.cs.unibo.it Port 80