X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbin%2Frecomm%2FrecommGcbGroundRelocation.ml;h=466386a8d17ebc0f1a20b3a228de855f1ed5fab1;hp=70e95bb4e98edd4d63324bc49f3d77ee3fc2d41f;hb=f8b4eb67c2437f7b5174d7dca46e102e0ac0d19d;hpb=8bbe582d87984526f40182c4409cbfd43108cb79 diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/recommGcbGroundRelocation.ml b/matita/matita/contribs/lambdadelta/bin/recomm/recommGcbGroundRelocation.ml index 70e95bb4e..466386a8d 100644 --- a/matita/matita/contribs/lambdadelta/bin/recomm/recommGcbGroundRelocation.ml +++ b/matita/matita/contribs/lambdadelta/bin/recomm/recommGcbGroundRelocation.ml @@ -4,64 +4,64 @@ module R = RecommPcsAnd let step k st outs ins = if st <> T.OO then k st outs ins else match ins with - | "gr_sor" :: tl -> k T.OK ("gr_sor" :: outs) tl - | "sor" :: tl -> k T.OK ("gr_sor" :: outs) tl - | "gr_sand" :: tl -> k T.OK ("gr_sand" :: outs) tl - | "sand" :: tl -> k T.OK ("gr_sand" :: outs) tl - | "gr_sdj" :: tl -> k T.OK ("gr_sdj" :: outs) tl - | "sdj" :: tl -> k T.OK ("gr_sdj" :: outs) tl - | "gr_sle" :: tl -> k T.OK ("gr_sle" :: outs) tl - | "sle" :: tl -> k T.OK ("gr_sle" :: outs) tl - | "inclusion" :: tl -> k T.OK ("gr_sle" :: outs) tl - | "gr_coafter" :: tl -> k T.OK ("gr_coafter" :: outs) tl - | "coafter" :: tl -> k T.OK ("gr_coafter" :: outs) tl - | "gr_after" :: tl -> k T.OK ("gr_after" :: outs) tl - | "after" :: tl -> k T.OK ("gr_after" :: outs) tl - | "gr_isd" :: tl -> k T.OK ("gr_isd" :: outs) tl - | "isdiv" :: tl -> k T.OK ("gr_isd" :: outs) tl - | "gr_ist" :: tl -> k T.OK ("gr_ist" :: outs) tl - | "ist" :: tl -> k T.OK ("gr_ist" :: outs) tl - | "istot" :: tl -> k T.OK ("gr_ist" :: outs) tl - | "gr_isf" :: tl -> k T.OK ("gr_isf" :: outs) tl - | "isf" :: tl -> k T.OK ("gr_isf" :: outs) tl - | "isfin" :: tl -> k T.OK ("gr_isf" :: outs) tl - | "test" :: "for" :: "finite" :: "colength" :: tl -> k T.OK ("gr_isf" :: outs) tl - | "gr_fcla" :: tl -> k T.OK ("gr_fcla" :: outs) tl - | "fcla" :: tl -> k T.OK ("gr_fcla" :: outs) tl - | "finite" :: "colength" :: "assignment" :: tl -> k T.OK ("gr_fcla" :: outs) tl - | "finite" :: "colength" :: tl -> k T.OK ("gr_fcla" :: outs) tl - | "gr_isu" :: tl -> k T.OK ("gr_isu" :: outs) tl - | "isuni" :: tl -> k T.OK ("gr_isu" :: outs) tl - | "test" :: "for" :: "uniform" :: "relocations" :: tl -> k T.OK ("gr_isu" :: outs) tl - | "gr_isi" :: tl -> k T.OK ("gr_isi" :: outs) tl - | "isi" :: tl -> k T.OK ("gr_isi" :: outs) tl - | "isid" :: tl -> k T.OK ("gr_isi" :: outs) tl - | "test" :: "for" :: "identity" :: tl -> k T.OK ("gr_isi" :: outs) tl - | "gr_nat" :: tl -> k T.OK ("gr_nat" :: outs) tl - | "nat" :: tl -> k T.OK ("gr_nat" :: outs) tl - | "gr_pat" :: tl -> k T.OK ("gr_pat" :: outs) tl - | "pat" :: tl -> k T.OK ("gr_pat" :: outs) tl - | "at" :: tl -> k T.OK ("gr_pat" :: outs) tl - | "gr_basic" :: tl -> k T.OK ("gr_basic" :: outs) tl - | "basic" :: "relocation" :: tl -> k T.OK ("gr_basic" :: outs) tl - | "gr_uni" :: tl -> k T.OK ("gr_uni" :: outs) tl - | "uni" :: tl -> k T.OK ("gr_uni" :: outs) tl - | "uniform" :: "relocations" :: tl -> k T.OK ("gr_uni" :: outs) tl - | "gr_id" :: tl -> k T.OK ("gr_id" :: outs) tl - | "id" :: tl -> k T.OK ("gr_id" :: outs) tl - | "gr_tls" :: tl -> k T.OK ("gr_tls" :: outs) tl - | "tls" :: tl -> k T.OK ("gr_tls" :: outs) tl - | "iterated" :: "tail" :: tl -> k T.OK ("gr_tls" :: outs) tl - | "gr_nexts" :: tl -> k T.OK ("gr_nexts" :: outs) tl - | "nexts" :: tl -> k T.OK ("gr_nexts" :: outs) tl - | "iterated" :: "next" :: tl -> k T.OK ("gr_nexts" :: outs) tl - | "gr_pushs" :: tl -> k T.OK ("gr_pushs" :: outs) tl - | "pushs" :: tl -> k T.OK ("gr_pushs" :: outs) tl - | "iterated" :: "push" :: tl -> k T.OK ("gr_pushs" :: outs) tl - | "gr_tl" :: tl -> k T.OK ("gr_tl" :: outs) tl - | "tl" :: tl -> k T.OK ("gr_tl" :: outs) tl - | "tail" :: tl -> k T.OK ("gr_tl" :: outs) tl - | "gr_eq" :: tl -> k T.OK ("gr_eq" :: outs) tl + | "pr_sor" :: tl -> k T.OK ("pr_sor" :: outs) tl + | "sor" :: tl -> k T.OK ("pr_sor" :: outs) tl + | "pr_sand" :: tl -> k T.OK ("pr_sand" :: outs) tl + | "sand" :: tl -> k T.OK ("pr_sand" :: outs) tl + | "pr_sdj" :: tl -> k T.OK ("pr_sdj" :: outs) tl + | "sdj" :: tl -> k T.OK ("pr_sdj" :: outs) tl + | "pr_sle" :: tl -> k T.OK ("pr_sle" :: outs) tl + | "sle" :: tl -> k T.OK ("pr_sle" :: outs) tl + | "inclusion" :: tl -> k T.OK ("pr_sle" :: outs) tl + | "pr_coafter" :: tl -> k T.OK ("pr_coafter" :: outs) tl + | "coafter" :: tl -> k T.OK ("pr_coafter" :: outs) tl + | "pr_after" :: tl -> k T.OK ("pr_after" :: outs) tl + | "after" :: tl -> k T.OK ("pr_after" :: outs) tl + | "pr_isd" :: tl -> k T.OK ("pr_isd" :: outs) tl + | "isdiv" :: tl -> k T.OK ("pr_isd" :: outs) tl + | "pr_ist" :: tl -> k T.OK ("pr_ist" :: outs) tl + | "ist" :: tl -> k T.OK ("pr_ist" :: outs) tl + | "istot" :: tl -> k T.OK ("pr_ist" :: outs) tl + | "pr_isf" :: tl -> k T.OK ("pr_isf" :: outs) tl + | "isf" :: tl -> k T.OK ("pr_isf" :: outs) tl + | "isfin" :: tl -> k T.OK ("pr_isf" :: outs) tl + | "test" :: "for" :: "finite" :: "colength" :: tl -> k T.OK ("pr_isf" :: outs) tl + | "pr_fcla" :: tl -> k T.OK ("pr_fcla" :: outs) tl + | "fcla" :: tl -> k T.OK ("pr_fcla" :: outs) tl + | "finite" :: "colength" :: "assignment" :: tl -> k T.OK ("pr_fcla" :: outs) tl + | "finite" :: "colength" :: tl -> k T.OK ("pr_fcla" :: outs) tl + | "pr_isu" :: tl -> k T.OK ("pr_isu" :: outs) tl + | "isuni" :: tl -> k T.OK ("pr_isu" :: outs) tl + | "test" :: "for" :: "uniform" :: "relocations" :: tl -> k T.OK ("pr_isu" :: outs) tl + | "pr_isi" :: tl -> k T.OK ("pr_isi" :: outs) tl + | "isi" :: tl -> k T.OK ("pr_isi" :: outs) tl + | "isid" :: tl -> k T.OK ("pr_isi" :: outs) tl + | "test" :: "for" :: "identity" :: tl -> k T.OK ("pr_isi" :: outs) tl + | "pr_nat" :: tl -> k T.OK ("pr_nat" :: outs) tl + | "nat" :: tl -> k T.OK ("pr_nat" :: outs) tl + | "pr_pat" :: tl -> k T.OK ("pr_pat" :: outs) tl + | "pat" :: tl -> k T.OK ("pr_pat" :: outs) tl + | "at" :: tl -> k T.OK ("pr_pat" :: outs) tl + | "pr_basic" :: tl -> k T.OK ("pr_basic" :: outs) tl + | "basic" :: "relocation" :: tl -> k T.OK ("pr_basic" :: outs) tl + | "pr_uni" :: tl -> k T.OK ("pr_uni" :: outs) tl + | "uni" :: tl -> k T.OK ("pr_uni" :: outs) tl + | "uniform" :: "relocations" :: tl -> k T.OK ("pr_uni" :: outs) tl + | "pr_id" :: tl -> k T.OK ("pr_id" :: outs) tl + | "id" :: tl -> k T.OK ("pr_id" :: outs) tl + | "pr_tls" :: tl -> k T.OK ("pr_tls" :: outs) tl + | "tls" :: tl -> k T.OK ("pr_tls" :: outs) tl + | "iterated" :: "tail" :: tl -> k T.OK ("pr_tls" :: outs) tl + | "pr_nexts" :: tl -> k T.OK ("pr_nexts" :: outs) tl + | "nexts" :: tl -> k T.OK ("pr_nexts" :: outs) tl + | "iterated" :: "next" :: tl -> k T.OK ("pr_nexts" :: outs) tl + | "pr_pushs" :: tl -> k T.OK ("pr_pushs" :: outs) tl + | "pushs" :: tl -> k T.OK ("pr_pushs" :: outs) tl + | "iterated" :: "push" :: tl -> k T.OK ("pr_pushs" :: outs) tl + | "pr_tl" :: tl -> k T.OK ("pr_tl" :: outs) tl + | "tl" :: tl -> k T.OK ("pr_tl" :: outs) tl + | "tail" :: tl -> k T.OK ("pr_tl" :: outs) tl + | "pr_eq" :: tl -> k T.OK ("pr_eq" :: outs) tl | _ -> k T.OO outs ins let main =