X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fnames.txt;h=353fd787a2c91a82eb2c74a63269e86320a3bd3e;hb=57103fa96f504f9bffca859dd60317162396657f;hp=8b80babf92ea0bc2895d977e0c07a2c1784daade;hpb=ef49e0e7f5f298c299afdd3cbfdc2404ecb93879;p=helm.git diff --git a/matita/matita/contribs/lambdadelta/basic_2/names.txt b/matita/matita/contribs/lambdadelta/basic_2/names.txt index 8b80babf9..353fd787a 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/names.txt +++ b/matita/matita/contribs/lambdadelta/basic_2/names.txt @@ -61,14 +61,17 @@ t: context-free for terms i: irreducible form n: normal form -p: parallel transformation +p: reflexive parallel transformation +q: sequential transformation r: reducible form -s: sequential transformation +s: strongly normalizing form - third letter +b: "big tree" reduction c: conversion d: decomposed extended reduction +e: decomposed extended conversion q: restricted reduction r: reduction s: substitution @@ -76,6 +79,9 @@ x: extended reduction - forth letter (if present) -p: non-reflexive transitive closure (plus) -q: reflexive closure (question) -s: reflexive transitive closure (star) +c: proper single step (successor) +e: reflexive transitive closure to normal form (evaluation) +g: proper multiple step (greater) +p: non-reflexive transitive closure (plus) +q: reflexive closure (question) +s: reflexive transitive closure (star)