]> matita.cs.unibo.it Git - helm.git/commit
- new component "s_transition" for the restored fqu and fquq
authorFerruccio Guidi <ferruccio.guidi@unibo.it>
Fri, 1 Apr 2016 21:26:20 +0000 (21:26 +0000)
committerFerruccio Guidi <ferruccio.guidi@unibo.it>
Fri, 1 Apr 2016 21:26:20 +0000 (21:26 +0000)
commit93bba1c94779e83184d111cd077d4167e42a74aa
treec33618ba7a98c15dce21800f7893ecfc2479b57e
parent9a023f554e56d6edbbb2eeaf17ce61e31857ef4a
- new component "s_transition" for the restored fqu and fquq
- minor additions
- notation update
- partial commit in the "static" component to park da and lsubd
123 files changed:
matita/matita/contribs/lambdadelta/basic_2/etc_new/da/da.etc [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/etc_new/da/da_aaa.etc [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/etc_new/da/da_da.etc [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/etc_new/da/da_lift.etc [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/etc_new/da/degree_6.etc [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/etc_new/drops/drops.etc
matita/matita/contribs/lambdadelta/basic_2/etc_new/drops/rdropstar_3.etc [deleted file]
matita/matita/contribs/lambdadelta/basic_2/etc_new/fqu/fqu.etc [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/etc_new/fqu/fquq.etc [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/etc_new/lsubd/lrsubeqd_5.etc [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/etc_new/lsubd/lsubd.etc [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/etc_new/lsubd/lsubd_da.etc [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/etc_new/lsubd/lsubd_lsubd.etc [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/grammar/append.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/grammar/append_length.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/grammar/lenv.ma
matita/matita/contribs/lambdadelta/basic_2/grammar/lenv_append.ma [deleted file]
matita/matita/contribs/lambdadelta/basic_2/names.txt
matita/matita/contribs/lambdadelta/basic_2/notation/notation.ma
matita/matita/contribs/lambdadelta/basic_2/notation/relations/btpred_8.ma
matita/matita/contribs/lambdadelta/basic_2/notation/relations/btpredalt_8.ma
matita/matita/contribs/lambdadelta/basic_2/notation/relations/btpredproper_8.ma
matita/matita/contribs/lambdadelta/basic_2/notation/relations/btpredstar_8.ma
matita/matita/contribs/lambdadelta/basic_2/notation/relations/btpredstaralt_8.ma
matita/matita/contribs/lambdadelta/basic_2/notation/relations/btsn_5.ma
matita/matita/contribs/lambdadelta/basic_2/notation/relations/btsnalt_5.ma
matita/matita/contribs/lambdadelta/basic_2/notation/relations/cosn_5.ma
matita/matita/contribs/lambdadelta/basic_2/notation/relations/degree_6.ma [deleted file]
matita/matita/contribs/lambdadelta/basic_2/notation/relations/dpconvstar_8.ma
matita/matita/contribs/lambdadelta/basic_2/notation/relations/dpredstar_7.ma
matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazybtpredstarproper_8.ma
matita/matita/contribs/lambdadelta/basic_2/notation/relations/lrsubeqd_5.ma [deleted file]
matita/matita/contribs/lambdadelta/basic_2/notation/relations/lrsubeqv_5.ma
matita/matita/contribs/lambdadelta/basic_2/notation/relations/nativevalid_5.ma
matita/matita/contribs/lambdadelta/basic_2/notation/relations/nativevalid_6.ma
matita/matita/contribs/lambdadelta/basic_2/notation/relations/pred_6.ma
matita/matita/contribs/lambdadelta/basic_2/notation/relations/predeval_6.ma
matita/matita/contribs/lambdadelta/basic_2/notation/relations/prednormal_5.ma
matita/matita/contribs/lambdadelta/basic_2/notation/relations/prednotreducible_5.ma
matita/matita/contribs/lambdadelta/basic_2/notation/relations/predreducible_5.ma
matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsn_5.ma
matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsnstar_5.ma
matita/matita/contribs/lambdadelta/basic_2/notation/relations/predstar_6.ma
matita/matita/contribs/lambdadelta/basic_2/notation/relations/rdropstar_3.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/notation/relations/sn_5.ma
matita/matita/contribs/lambdadelta/basic_2/notation/relations/sn_6.ma
matita/matita/contribs/lambdadelta/basic_2/notation/relations/snalt_5.ma
matita/matita/contribs/lambdadelta/basic_2/notation/relations/snalt_6.ma
matita/matita/contribs/lambdadelta/basic_2/notation/relations/statictypestar_6.ma
matita/matita/contribs/lambdadelta/basic_2/notation/relations/suptermoptalt_6.ma [deleted file]
matita/matita/contribs/lambdadelta/basic_2/reduction/cir.ma
matita/matita/contribs/lambdadelta/basic_2/reduction/cir_lift.ma
matita/matita/contribs/lambdadelta/basic_2/reduction/cix.ma
matita/matita/contribs/lambdadelta/basic_2/reduction/cix_lift.ma
matita/matita/contribs/lambdadelta/basic_2/reduction/cnr.ma
matita/matita/contribs/lambdadelta/basic_2/reduction/cnr_lift.ma
matita/matita/contribs/lambdadelta/basic_2/reduction/cnx.ma
matita/matita/contribs/lambdadelta/basic_2/reduction/cnx_cix.ma
matita/matita/contribs/lambdadelta/basic_2/reduction/cnx_crx.ma
matita/matita/contribs/lambdadelta/basic_2/reduction/cnx_lift.ma
matita/matita/contribs/lambdadelta/basic_2/reduction/cpr.ma
matita/matita/contribs/lambdadelta/basic_2/reduction/cpr_lift.ma
matita/matita/contribs/lambdadelta/basic_2/reduction/cpr_llpx_sn.ma
matita/matita/contribs/lambdadelta/basic_2/reduction/cpx.ma
matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_cix.ma
matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_lift.ma
matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_lleq.ma
matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_llpx_sn.ma
matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_lreq.ma
matita/matita/contribs/lambdadelta/basic_2/reduction/crr.ma
matita/matita/contribs/lambdadelta/basic_2/reduction/crr_lift.ma
matita/matita/contribs/lambdadelta/basic_2/reduction/crx.ma
matita/matita/contribs/lambdadelta/basic_2/reduction/crx_lift.ma
matita/matita/contribs/lambdadelta/basic_2/reduction/fpb.ma
matita/matita/contribs/lambdadelta/basic_2/reduction/fpb_fleq.ma
matita/matita/contribs/lambdadelta/basic_2/reduction/fpb_lift.ma
matita/matita/contribs/lambdadelta/basic_2/reduction/fpb_lleq.ma
matita/matita/contribs/lambdadelta/basic_2/reduction/fpbq.ma
matita/matita/contribs/lambdadelta/basic_2/reduction/fpbq_aaa.ma
matita/matita/contribs/lambdadelta/basic_2/reduction/fpbq_alt.ma
matita/matita/contribs/lambdadelta/basic_2/reduction/fpbq_lift.ma
matita/matita/contribs/lambdadelta/basic_2/reduction/fqu.ma [deleted file]
matita/matita/contribs/lambdadelta/basic_2/reduction/fquq.ma [deleted file]
matita/matita/contribs/lambdadelta/basic_2/reduction/fquq_alt.ma [deleted file]
matita/matita/contribs/lambdadelta/basic_2/reduction/lpr_drop.ma
matita/matita/contribs/lambdadelta/basic_2/reduction/lpx.ma
matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_aaa.ma
matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_drop.ma
matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_frees.ma
matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_lleq.ma
matita/matita/contribs/lambdadelta/basic_2/relocation/drops.ma
matita/matita/contribs/lambdadelta/basic_2/relocation/lifts.ma
matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_lifts_vector.ma
matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_vector.ma
matita/matita/contribs/lambdadelta/basic_2/s_transition/fqu.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/s_transition/fqu_length.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/s_transition/fqu_weight.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/s_transition/fquq.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/s_transition/fquq_length.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/s_transition/fquq_weight.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/static/aaa.ma
matita/matita/contribs/lambdadelta/basic_2/static/aaa_aaa.ma
matita/matita/contribs/lambdadelta/basic_2/static/aaa_drops.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/static/aaa_lift.ma [deleted file]
matita/matita/contribs/lambdadelta/basic_2/static/aaa_lifts.ma [deleted file]
matita/matita/contribs/lambdadelta/basic_2/static/da.ma [deleted file]
matita/matita/contribs/lambdadelta/basic_2/static/da_aaa.ma [deleted file]
matita/matita/contribs/lambdadelta/basic_2/static/da_da.ma [deleted file]
matita/matita/contribs/lambdadelta/basic_2/static/da_lift.ma [deleted file]
matita/matita/contribs/lambdadelta/basic_2/static/lsuba.ma
matita/matita/contribs/lambdadelta/basic_2/static/lsubd.ma [deleted file]
matita/matita/contribs/lambdadelta/basic_2/static/lsubd_da.ma [deleted file]
matita/matita/contribs/lambdadelta/basic_2/static/lsubd_lsubd.ma [deleted file]
matita/matita/contribs/lambdadelta/basic_2/static/lsubr.ma
matita/matita/contribs/lambdadelta/basic_2/static/lsubr_drops.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/static/lsubr_length.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/static/lsubr_lsubr.ma
matita/matita/contribs/lambdadelta/basic_2/static/sd.ma
matita/matita/contribs/lambdadelta/basic_2/static/sh.ma
matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl
matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma
matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_after.ma
matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_at.ma