]> matita.cs.unibo.it Git - helm.git/commit
update in delayed_updating
authorFerruccio Guidi <ferruccio.guidi@unibo.it>
Sat, 21 May 2022 18:23:22 +0000 (20:23 +0200)
committerFerruccio Guidi <ferruccio.guidi@unibo.it>
Sat, 21 May 2022 18:23:22 +0000 (20:23 +0200)
commit97ff918432e878ab8314c72fe2b948a253b26e21
treeb679c4a875a658c6df3cb0ea53324971e489443f
parentef07f57f5fb5bc34897fdef44987e6a154206807
update in delayed_updating

+ unwind completed with an important result on lift
44 files changed:
matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind1/unwind.etc [new file with mode: 0644]
matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind1/unwind_constructors.etc [new file with mode: 0644]
matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind1/unwind_depth.etc [new file with mode: 0644]
matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind1/unwind_eq.etc [new file with mode: 0644]
matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind1/unwind_eq_etc.etc [new file with mode: 0644]
matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind1/unwind_fsubst.etc [new file with mode: 0644]
matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind1/unwind_preterm_eq.etc [new file with mode: 0644]
matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind1/unwind_prototerm.etc [new file with mode: 0644]
matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind1/unwind_prototerm_eq.etc [new file with mode: 0644]
matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind1/unwind_structure.etc [new file with mode: 0644]
matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind1/unwind_structure_depth.etc [new file with mode: 0644]
matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind1/unwind_update.etc [new file with mode: 0644]
matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_eq.ma
matita/matita/contribs/lambdadelta/delayed_updating/syntax/bdd_term.ma
matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_proper.ma
matita/matita/contribs/lambdadelta/delayed_updating/unwind/nap.ma
matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_constructors.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_path.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_path_eq.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_path_lift.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_path_structure.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_preterm_eq.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_preterm_fsubst.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_prototerm.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_prototerm_eq.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_prototerm_lift.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_head.ma
matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind_gen.ma
matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind_gen_after.ma
matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind_gen_eq.ma
matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind_gen_structure.ma
matita/matita/contribs/lambdadelta/delayed_updating/unwind/xap.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/delayed_updating/unwind1/unwind.ma [deleted file]
matita/matita/contribs/lambdadelta/delayed_updating/unwind1/unwind_constructors.ma [deleted file]
matita/matita/contribs/lambdadelta/delayed_updating/unwind1/unwind_depth.ma [deleted file]
matita/matita/contribs/lambdadelta/delayed_updating/unwind1/unwind_eq.ma [deleted file]
matita/matita/contribs/lambdadelta/delayed_updating/unwind1/unwind_eq_etc.ma [deleted file]
matita/matita/contribs/lambdadelta/delayed_updating/unwind1/unwind_fsubst.ma [deleted file]
matita/matita/contribs/lambdadelta/delayed_updating/unwind1/unwind_preterm_eq.ma [deleted file]
matita/matita/contribs/lambdadelta/delayed_updating/unwind1/unwind_prototerm.ma [deleted file]
matita/matita/contribs/lambdadelta/delayed_updating/unwind1/unwind_prototerm_eq.ma [deleted file]
matita/matita/contribs/lambdadelta/delayed_updating/unwind1/unwind_structure.ma [deleted file]
matita/matita/contribs/lambdadelta/delayed_updating/unwind1/unwind_structure_depth.ma [deleted file]
matita/matita/contribs/lambdadelta/delayed_updating/unwind1/unwind_update.ma [deleted file]