]> matita.cs.unibo.it Git - helm.git/commit
update in static_2
authorFerruccio Guidi <ferruccio.guidi@unibo.it>
Sat, 18 Jul 2020 18:49:45 +0000 (20:49 +0200)
committerFerruccio Guidi <ferruccio.guidi@unibo.it>
Sat, 18 Jul 2020 18:49:45 +0000 (20:49 +0200)
commitb118146b97959e6a6dde18fdd014b8e1e676a2d1
tree2566afa5f7684c612619514c1db91072d611528e
parent613d8642b1154dde0c026cbdcd96568910198251
update in static_2

+ generic equivalence generalizes syntactic equivalence and sort-irrelevant equivalence
+ minor corrections
212 files changed:
matita/matita/contribs/lambdadelta/apps_2/examples/ex_rpx_fwd.ma
matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_teqx.ma
matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_teqx_conf.ma
matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_teqx_trans.ma
matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpms_conf.ma
matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpms_teqx.ma
matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpms_teqx_conf.ma
matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpmuwe.ma
matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_eval.ma
matita/matita/contribs/lambdadelta/basic_2/etc/teqx/cpms_reqx.etc [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/etc/teqx/cpr_teqx.etc [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/etc/teqx/cpx_feqx.etc [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/etc/teqx/cpx_req.etc [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/etc/teqx/cpx_reqx.etc [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/etc/teqx/cpxs_feqx.etc [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/etc/teqx/cpxs_reqx.etc [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/etc/teqx/cpxs_teqx.etc [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/etc/teqx/csx_feqx.etc [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/etc/teqx/csx_reqx.etc [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/etc/teqx/fpb_feqx.etc [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/etc/teqx/fpb_reqx.etc [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/etc/teqx/fsb_feqx.etc [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/etc/teqx/lpx_reqx.etc [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/etc/teqx/lpxs_feqx.etc [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/etc/teqx/lpxs_reqx.etc [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/rt_computation/cnuw.ma
matita/matita/contribs/lambdadelta/basic_2/rt_computation/cnuw_cnuw.ma
matita/matita/contribs/lambdadelta/basic_2/rt_computation/cnuw_drops.ma
matita/matita/contribs/lambdadelta/basic_2/rt_computation/cnuw_simple.ma
matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms_fpbg.ma
matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms_reqg.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms_reqx.ma [deleted file]
matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpmuwe_csx.ma
matita/matita/contribs/lambdadelta/basic_2/rt_computation/cprs_teqw.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/rt_computation/cprs_tweq.ma [deleted file]
matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_cnx.ma
matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_feqg.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_feqx.ma [deleted file]
matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_fqus.ma
matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_reqg.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_reqx.ma [deleted file]
matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_teqg.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_teqo.ma
matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_teqo_vector.ma
matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_teqx.ma [deleted file]
matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx.ma
matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_aaa.ma
matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_cpxs.ma
matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_csx.ma
matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_feqg.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_feqx.ma [deleted file]
matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_fpbq.ma
matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_reqg.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_reqx.ma [deleted file]
matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_simple.ma
matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_simple_teqo.ma
matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg.ma
matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg_cpxs.ma
matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg_fpbs.ma
matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg_fqup.ma
matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg_lpxs.ma
matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs.ma
matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_cpx.ma
matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_cpxs.ma
matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_fqup.ma
matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_lpxs.ma
matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb_csx.ma
matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb_feqg.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb_feqx.ma [deleted file]
matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb_fpbg.ma
matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs_feqg.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs_feqx.ma [deleted file]
matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs_reqg.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs_reqx.ma [deleted file]
matita/matita/contribs/lambdadelta/basic_2/rt_computation/rsx.ma
matita/matita/contribs/lambdadelta/basic_2/rt_computation/rsx_csx.ma
matita/matita/contribs/lambdadelta/basic_2/rt_computation/rsx_drops.ma
matita/matita/contribs/lambdadelta/basic_2/rt_computation/rsx_fqup.ma
matita/matita/contribs/lambdadelta/basic_2/rt_computation/rsx_length.ma
matita/matita/contribs/lambdadelta/basic_2/rt_computation/rsx_lpxs.ma
matita/matita/contribs/lambdadelta/basic_2/rt_computation/rsx_rsx.ma
matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnr_teqg.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnr_teqx.ma
matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnx.ma
matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnx_cnx.ma
matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnx_drops.ma
matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm_teqx.ma
matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpr_teqg.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpr_teqx.ma [deleted file]
matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_feqg.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_feqx.ma [deleted file]
matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_fqus.ma
matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_req.ma [deleted file]
matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_reqg.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_reqx.ma [deleted file]
matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpb.ma
matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpb_feqg.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpb_feqx.ma [deleted file]
matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpb_reqg.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpb_reqx.ma [deleted file]
matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpbq.ma
matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpbq_aaa.ma
matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpbq_fpb.ma
matita/matita/contribs/lambdadelta/basic_2/rt_transition/lpx_reqg.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/rt_transition/lpx_reqx.ma [deleted file]
matita/matita/contribs/lambdadelta/basic_2/rt_transition/rpx_lpx.ma
matita/matita/contribs/lambdadelta/basic_2/rt_transition/rpx_reqg.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/rt_transition/rpx_reqx.ma
matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl
matita/matita/contribs/lambdadelta/refile.sh
matita/matita/contribs/lambdadelta/replace.sh
matita/matita/contribs/lambdadelta/static_2/etc/teqx/feqx_feqx.etc [new file with mode: 0644]
matita/matita/contribs/lambdadelta/static_2/etc/teqx/feqx_fqup.etc [new file with mode: 0644]
matita/matita/contribs/lambdadelta/static_2/etc/teqx/feqx_fqus.etc [new file with mode: 0644]
matita/matita/contribs/lambdadelta/static_2/etc/teqx/feqx_req.etc [new file with mode: 0644]
matita/matita/contribs/lambdadelta/static_2/etc/teqx/req.etc [new file with mode: 0644]
matita/matita/contribs/lambdadelta/static_2/etc/teqx/req_drops.etc [new file with mode: 0644]
matita/matita/contribs/lambdadelta/static_2/etc/teqx/req_fqup.etc [new file with mode: 0644]
matita/matita/contribs/lambdadelta/static_2/etc/teqx/req_length.etc [new file with mode: 0644]
matita/matita/contribs/lambdadelta/static_2/etc/teqx/reqx_drops.etc [new file with mode: 0644]
matita/matita/contribs/lambdadelta/static_2/etc/teqx/reqx_fqup.etc [new file with mode: 0644]
matita/matita/contribs/lambdadelta/static_2/etc/teqx/reqx_fqus.etc [new file with mode: 0644]
matita/matita/contribs/lambdadelta/static_2/etc/teqx/reqx_length.etc [new file with mode: 0644]
matita/matita/contribs/lambdadelta/static_2/i_static/rexs_lex.ma
matita/matita/contribs/lambdadelta/static_2/notation/relations/approxeqsn_3.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/static_2/notation/relations/approxeqsn_6.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/static_2/notation/relations/ideq_3.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/static_2/notation/relations/stareq_2.ma [deleted file]
matita/matita/contribs/lambdadelta/static_2/notation/relations/stareq_3.ma
matita/matita/contribs/lambdadelta/static_2/notation/relations/stareq_4.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/static_2/notation/relations/stareqsn_3.ma [deleted file]
matita/matita/contribs/lambdadelta/static_2/notation/relations/stareqsn_4.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/static_2/notation/relations/stareqsn_6.ma [deleted file]
matita/matita/contribs/lambdadelta/static_2/notation/relations/stareqsn_7.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/static_2/notation/relations/tilde_2.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/static_2/notation/relations/tildeminus_2.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/static_2/notation/relations/topiso_2.ma [deleted file]
matita/matita/contribs/lambdadelta/static_2/relocation/lifts_teqg.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/static_2/relocation/lifts_teqw.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/static_2/relocation/lifts_teqx.ma
matita/matita/contribs/lambdadelta/static_2/relocation/lifts_tweq.ma [deleted file]
matita/matita/contribs/lambdadelta/static_2/relocation/seq.ma
matita/matita/contribs/lambdadelta/static_2/relocation/seq_length.ma
matita/matita/contribs/lambdadelta/static_2/relocation/seq_seq.ma
matita/matita/contribs/lambdadelta/static_2/s_transition/fqu_teqg.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/static_2/s_transition/fqu_teqx.ma [deleted file]
matita/matita/contribs/lambdadelta/static_2/static/aaa_feqg.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/static_2/static/aaa_feqx.ma [deleted file]
matita/matita/contribs/lambdadelta/static_2/static/aaa_reqg.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/static_2/static/aaa_reqx.ma [deleted file]
matita/matita/contribs/lambdadelta/static_2/static/feqg.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/static_2/static/feqg_feqg.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/static_2/static/feqg_fqup.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/static_2/static/feqg_fqus.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/static_2/static/feqx.ma
matita/matita/contribs/lambdadelta/static_2/static/feqx_feqx.ma [deleted file]
matita/matita/contribs/lambdadelta/static_2/static/feqx_fqup.ma [deleted file]
matita/matita/contribs/lambdadelta/static_2/static/feqx_fqus.ma [deleted file]
matita/matita/contribs/lambdadelta/static_2/static/feqx_req.ma [deleted file]
matita/matita/contribs/lambdadelta/static_2/static/remove/feqx_req.etc [new file with mode: 0644]
matita/matita/contribs/lambdadelta/static_2/static/remove/req_drops.etc [new file with mode: 0644]
matita/matita/contribs/lambdadelta/static_2/static/remove/req_fqup.etc [new file with mode: 0644]
matita/matita/contribs/lambdadelta/static_2/static/remove/req_fsle.etc [new file with mode: 0644]
matita/matita/contribs/lambdadelta/static_2/static/remove/req_length.etc [new file with mode: 0644]
matita/matita/contribs/lambdadelta/static_2/static/remove/reqx_req.etc [new file with mode: 0644]
matita/matita/contribs/lambdadelta/static_2/static/req.ma
matita/matita/contribs/lambdadelta/static_2/static/req_drops.ma [deleted file]
matita/matita/contribs/lambdadelta/static_2/static/req_fqup.ma [deleted file]
matita/matita/contribs/lambdadelta/static_2/static/req_fsle.ma [deleted file]
matita/matita/contribs/lambdadelta/static_2/static/req_length.ma [deleted file]
matita/matita/contribs/lambdadelta/static_2/static/req_req.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/static_2/static/reqg.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/static_2/static/reqg_drops.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/static_2/static/reqg_fqup.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/static_2/static/reqg_fqus.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/static_2/static/reqg_length.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/static_2/static/reqg_reqg.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/static_2/static/reqx.ma
matita/matita/contribs/lambdadelta/static_2/static/reqx_drops.ma [deleted file]
matita/matita/contribs/lambdadelta/static_2/static/reqx_fqup.ma [deleted file]
matita/matita/contribs/lambdadelta/static_2/static/reqx_fqus.ma [deleted file]
matita/matita/contribs/lambdadelta/static_2/static/reqx_length.ma [deleted file]
matita/matita/contribs/lambdadelta/static_2/static/reqx_req.ma [deleted file]
matita/matita/contribs/lambdadelta/static_2/static/reqx_reqx.ma
matita/matita/contribs/lambdadelta/static_2/syntax/ceq_ext.ma [deleted file]
matita/matita/contribs/lambdadelta/static_2/syntax/ceq_ext_ceq_ext.ma [deleted file]
matita/matita/contribs/lambdadelta/static_2/syntax/lenv.ma
matita/matita/contribs/lambdadelta/static_2/syntax/teq.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/static_2/syntax/teq_ext.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/static_2/syntax/teq_ext_teq_ext.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/static_2/syntax/teq_teq.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/static_2/syntax/teqg.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/static_2/syntax/teqg_ext.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/static_2/syntax/teqg_teqg.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/static_2/syntax/teqo.ma
matita/matita/contribs/lambdadelta/static_2/syntax/teqo_simple.ma
matita/matita/contribs/lambdadelta/static_2/syntax/teqo_simple_vector.ma
matita/matita/contribs/lambdadelta/static_2/syntax/teqo_teqg.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/static_2/syntax/teqo_teqx.ma [deleted file]
matita/matita/contribs/lambdadelta/static_2/syntax/teqw.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/static_2/syntax/teqw_simple.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/static_2/syntax/teqw_teqg.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/static_2/syntax/teqw_teqw.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/static_2/syntax/teqx.ma
matita/matita/contribs/lambdadelta/static_2/syntax/teqx_ext.ma
matita/matita/contribs/lambdadelta/static_2/syntax/teqx_teqx.ma
matita/matita/contribs/lambdadelta/static_2/syntax/tweq.ma [deleted file]
matita/matita/contribs/lambdadelta/static_2/syntax/tweq_simple.ma [deleted file]
matita/matita/contribs/lambdadelta/static_2/syntax/tweq_teqx.ma [deleted file]
matita/matita/contribs/lambdadelta/static_2/syntax/tweq_tweq.ma [deleted file]
matita/matita/contribs/lambdadelta/static_2/web/static_2_src.tbl
matita/matita/contribs/lambdadelta/web/changes.tbl