]> matita.cs.unibo.it Git - helm.git/commit
- fpbg can be reflexive (example given)
authorFerruccio Guidi <ferruccio.guidi@unibo.it>
Thu, 2 Oct 2014 15:36:10 +0000 (15:36 +0000)
committerFerruccio Guidi <ferruccio.guidi@unibo.it>
Thu, 2 Oct 2014 15:36:10 +0000 (15:36 +0000)
commit106b25f0206beedc4e416d223accb1308ca7161b
tree510237386f3abfe3bf25a7c359d8f8da1a9a7646
parent12fd764a3ab9df02fcea5403bdc50387bb648887
- fpbg can be reflexive (example given)
- so fpbu may use short steps rather than long steps
- some refactoring
40 files changed:
matita/matita/contribs/lambdadelta/basic_2/computation/fpbc.ma [deleted file]
matita/matita/contribs/lambdadelta/basic_2/computation/fpbc_fleq.ma [deleted file]
matita/matita/contribs/lambdadelta/basic_2/computation/fpbc_fpbs.ma [deleted file]
matita/matita/contribs/lambdadelta/basic_2/computation/fpbg.ma
matita/matita/contribs/lambdadelta/basic_2/computation/fpbg_fleq.ma
matita/matita/contribs/lambdadelta/basic_2/computation/fpbg_fpbg.ma
matita/matita/contribs/lambdadelta/basic_2/computation/fpbg_lift.ma
matita/matita/contribs/lambdadelta/basic_2/computation/fpbs.ma
matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_aaa.ma
matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_alt.ma
matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_ext.ma [deleted file]
matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_fleq.ma
matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_fpbc.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_fpbs.ma
matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_fpbu.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_lift.ma
matita/matita/contribs/lambdadelta/basic_2/computation/fpbu.ma [deleted file]
matita/matita/contribs/lambdadelta/basic_2/computation/fpbu_fleq.ma [deleted file]
matita/matita/contribs/lambdadelta/basic_2/computation/fpbu_lift.ma [deleted file]
matita/matita/contribs/lambdadelta/basic_2/computation/fpbu_lleq.ma [deleted file]
matita/matita/contribs/lambdadelta/basic_2/computation/fsb.ma
matita/matita/contribs/lambdadelta/basic_2/computation/fsb_aaa.ma
matita/matita/contribs/lambdadelta/basic_2/computation/fsb_alt.ma
matita/matita/contribs/lambdadelta/basic_2/computation/fsb_csx.ma
matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_lleq.ma
matita/matita/contribs/lambdadelta/basic_2/computation/lsx_alt.ma
matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_scpes.ma
matita/matita/contribs/lambdadelta/basic_2/examples/ex_cpr_omega.ma
matita/matita/contribs/lambdadelta/basic_2/examples/ex_sta_ldec.ma
matita/matita/contribs/lambdadelta/basic_2/multiple/lleq_lleq.ma
matita/matita/contribs/lambdadelta/basic_2/reduction/fpb.ma
matita/matita/contribs/lambdadelta/basic_2/reduction/fpb_aaa.ma
matita/matita/contribs/lambdadelta/basic_2/reduction/fpb_lift.ma
matita/matita/contribs/lambdadelta/basic_2/reduction/fpbc.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/reduction/fpbc_fleq.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/reduction/fpbu.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/reduction/fpbu_fleq.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/reduction/fpbu_lift.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/reduction/fpbu_lleq.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl