[Imprint][Data Privacy Statement][E-Mail]

Back to main index. View the specification. View theorem base summary, View theorem base listing, the used properties by spec, the dependency list, the symbol table,

Used simplifier rules/spec theorems by specification

Used from specification nat

nat/eq is used by RG2-Strong-Total-Corr, RG2-Sound+DF+Term,
nat/l-num-01 is used by rg2-sound-main, rg2-lem2-term-strnger, rg2-lem1-term-strnger,
nat/lels is used by RG2-Strong-Total-Corr, RG2-Sound+DF+Term,

Used from specification nat-basic2

Used from specification nat-basic1

nat-basic1/ref-1 is used by rg2-sound-main, rg2-not-pre2-term-strnger, rg2-not-pre2, rg2-not-pre1-term-strnger, rg2-not-pre1, rg2-lem2-term-strnger, rg2-lem1-term-strnger, rg-blocked2-not-r2-term, rg-blocked2-not-r2, rg-blocked1-not-r1-term, rg-blocked1-not-r1,