matita.cs.unibo.it Git - helm.git/commit - matita/matita/contribs/lambdadelta/static_2/syntax/theq

]> matita.cs.unibo.it Git - helm.git/commit - matita/matita/contribs/lambdadelta/static_2/syntax/theq_simple.ma

author	Ferruccio Guidi <fguidi@maelstrom.helm.cs.unibo.it>
	Mon, 25 Mar 2019 16:32:22 +0000 (17:32 +0100)
committer	Ferruccio Guidi <fguidi@maelstrom.helm.cs.unibo.it>
	Mon, 25 Mar 2019 16:32:22 +0000 (17:32 +0100)
commit	4173283e148199871d787c53c0301891deb90713
tree	17bffb54765395b633a4b746a8990321965c3d1a	tree \| snapshot
parent	a67fc50ccfda64377e2c94c18c3a0d9265f651db	commit \| diff

milestone in basic_2

preservation of validity for rt-computation does not need the sort degree parameter (i.e. no induction on the degree).

151 files changed:

matita/matita/contribs/lambdadelta/apps_2/examples/ex_fpbg_refl.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_conf.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_tdeq.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_tdeq_conf.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_tdeq_trans.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_trans.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpms_conf.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpms_tdeq.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpms_tdeq_conf.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_fsb.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_preserve.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_preserve_sub.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_fsb.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/notation/relations/lsubeqx_5.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/notation/relations/lsubeqx_6.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsubty_7.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsubty_8.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsubtyproper_7.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsubtyproper_8.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsubtystar_7.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsubtystar_8.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsubtystarproper_7.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsubtystarproper_8.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsubtystrong_4.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsubtystrong_5.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/notation/relations/predtynormal_4.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/notation/relations/predtynormal_5.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/notation/relations/predtysnstrong_4.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/notation/relations/predtysnstrong_5.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/notation/relations/predtystrong_4.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/notation/relations/predtystrong_5.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms_cwhx.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms_fpbg.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms_fpbs.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms_rdeq.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_cnx.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_fdeq.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_fqus.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_rdeq.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_tdeq.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_theq.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_theq_vector.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_aaa.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_cnx.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_cnx_vector.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_cpxs.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_csx.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_csx_vector.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_drops.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_fdeq.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_fpbq.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_fqus.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_gcp.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_gcr.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_lpx.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_lpxs.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_lsubr.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_rdeq.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_simple.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_simple_theq.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_vector.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg_cpxs.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg_fpbg.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg_fpbs.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg_fqup.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg_lpxs.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_aaa.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_cpx.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_cpxs.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_csx.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_fpb.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_fpbs.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_fqup.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_fqus.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_lpxs.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb_aaa.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb_csx.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb_fdeq.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb_fpbg.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs_fdeq.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs_rdeq.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/lsubsx.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/lsubsx_lsubsx.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/lsubsx_rdsx.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/rdsx.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/rdsx_csx.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/rdsx_drops.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/rdsx_fqup.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/rdsx_length.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/rdsx_lpxs.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/rdsx_rdsx.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnx.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnx_basic.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnx_cnx.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnx_drops.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnx_simple.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm_tdeq.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpr_tdeq.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_fdeq.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_fqus.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_rdeq.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_transition/cwhx_rdeq.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpb.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpb_fdeq.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpb_rdeq.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpbq.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpbq_aaa.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpbq_fpb.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_transition/lpx_rdeq.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_transition/rpx_rdeq.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/web/basic_2.ldw.xml		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl		diff \| blob \| history
matita/matita/contribs/lambdadelta/static_2/notation/relations/stareq_2.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/static_2/notation/relations/stareq_3.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/static_2/notation/relations/stareq_4.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/static_2/notation/relations/stareq_5.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/static_2/notation/relations/stareqsn_3.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/static_2/notation/relations/stareqsn_5.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/static_2/notation/relations/stareqsn_6.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/static_2/notation/relations/stareqsn_8.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/static_2/notation/relations/topiso_2.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/static_2/notation/relations/topiso_4.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/static_2/relocation/lifts_tdeq.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/static_2/s_transition/fqu_tdeq.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/static_2/static/aaa_fdeq.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/static_2/static/aaa_rdeq.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/static_2/static/fdeq.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/static_2/static/fdeq_fdeq.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/static_2/static/fdeq_fqup.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/static_2/static/fdeq_fqus.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/static_2/static/fdeq_req.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/static_2/static/rdeq.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/static_2/static/rdeq_drops.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/static_2/static/rdeq_fqup.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/static_2/static/rdeq_fqus.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/static_2/static/rdeq_length.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/static_2/static/rdeq_rdeq.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/static_2/static/rdeq_req.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/static_2/syntax/tdeq.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/static_2/syntax/tdeq_ext.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/static_2/syntax/tdeq_tdeq.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/static_2/syntax/theq.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/static_2/syntax/theq_simple.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/static_2/syntax/theq_simple_vector.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/static_2/syntax/theq_tdeq.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/static_2/syntax/theq_theq.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/static_2/web/static_2_src.tbl		diff \| blob \| history

Unnamed repository; edit this file 'description' to name the repository.

RSS Atom