Point out a special interpretation of df-ral (#3265)

* Point out a special interpretation of df-ral

* rm more OLD theorems

* minor style improvement

* provide an example for the exotic interpretation of a restricted quantifier

* style

* rewrap

---------

Co-authored-by: Wolf Lammen <[email protected]>

Author: wlammen

discouraged

@@ -13293,34 +13293,20 @@ New usage of "2uasban" is discouraged (0 uses).
 New usage of "2uasbanh" is discouraged (1 uses).
 New usage of "2uasbanhVD" is discouraged (0 uses).
 New usage of "2zrngALT" is discouraged (0 uses).
-New usage of "3adant1OLD" is discouraged (0 uses).
-New usage of "3adant1lOLD" is discouraged (0 uses).
-New usage of "3adant1rOLD" is discouraged (0 uses).
-New usage of "3adant2OLD" is discouraged (0 uses).
 New usage of "3adant2lOLD" is discouraged (0 uses).
 New usage of "3adant2rOLD" is discouraged (0 uses).
-New usage of "3adant3OLD" is discouraged (0 uses).
 New usage of "3adant3lOLD" is discouraged (0 uses).
 New usage of "3adant3rOLD" is discouraged (0 uses).
 New usage of "3anidm12p1" is discouraged (0 uses).
 New usage of "3anidm12p2" is discouraged (0 uses).
 New usage of "3atnelvolN" is discouraged (2 uses).
 New usage of "3cnOLD" is discouraged (0 uses).
-New usage of "3com12OLD" is discouraged (0 uses).
-New usage of "3com13OLD" is discouraged (0 uses).
 New usage of "3dimlem3OLDN" is discouraged (0 uses).
 New usage of "3dimlem4OLDN" is discouraged (0 uses).
-New usage of "3expOLD" is discouraged (0 uses).
-New usage of "3expaOLD" is discouraged (0 uses).
-New usage of "3expiaOLD" is discouraged (0 uses).
-New usage of "3imp21OLD" is discouraged (0 uses).
-New usage of "3impOLD" is discouraged (0 uses).
-New usage of "3impaOLD" is discouraged (0 uses).
 New usage of "3impdirp1" is discouraged (0 uses).
 New usage of "3impexpVD" is discouraged (0 uses).
 New usage of "3impexpbicomVD" is discouraged (0 uses).
 New usage of "3impexpbicomiVD" is discouraged (0 uses).
-New usage of "3impiaOLD" is discouraged (0 uses).
 New usage of "3jaoOLD" is discouraged (0 uses).
 New usage of "3lcm2e6woprm" is discouraged (1 uses).
 New usage of "3noncolr1N" is discouraged (1 uses).
@@ -13336,9 +13322,6 @@ New usage of "3orbi123VD" is discouraged (0 uses).
 New usage of "3ornot23" is discouraged (2 uses).
 New usage of "3ornot23VD" is discouraged (0 uses).
 New usage of "3polN" is discouraged (4 uses).
-New usage of "3simpaOLD" is discouraged (0 uses).
-New usage of "3simpbOLD" is discouraged (0 uses).
-New usage of "3simpcOLD" is discouraged (0 uses).
 New usage of "4atex2-0aOLDN" is discouraged (1 uses).
 New usage of "4atex2-0bOLDN" is discouraged (0 uses).
 New usage of "4atex2-0cOLDN" is discouraged (0 uses).
@@ -13380,12 +13363,6 @@ New usage of "abscncfALT" is discouraged (0 uses).
 New usage of "abshicom" is discouraged (1 uses).
 New usage of "ac2" is discouraged (1 uses).
 New usage of "ac3" is discouraged (1 uses).
-New usage of "ad5ant123OLD" is discouraged (0 uses).
-New usage of "ad5ant124OLD" is discouraged (0 uses).
-New usage of "ad5ant125OLD" is discouraged (0 uses).
-New usage of "ad5ant134OLD" is discouraged (0 uses).
-New usage of "ad5ant135OLD" is discouraged (0 uses).
-New usage of "ad5ant145OLD" is discouraged (0 uses).
 New usage of "addassnq" is discouraged (4 uses).
 New usage of "addasspi" is discouraged (1 uses).
 New usage of "addasspr" is discouraged (17 uses).
@@ -17208,7 +17185,6 @@ New usage of "pm13.18OLD" is discouraged (0 uses).
 New usage of "pm2.21ddALT" is discouraged (0 uses).
 New usage of "pm2.43bgbi" is discouraged (0 uses).
 New usage of "pm2.43cbi" is discouraged (2 uses).
-New usage of "pm3.2an3OLD" is discouraged (0 uses).
 New usage of "pmap1N" is discouraged (2 uses).
 New usage of "pmapglb2N" is discouraged (0 uses).
 New usage of "pmapglb2xN" is discouraged (1 uses).
@@ -17595,59 +17571,8 @@ New usage of "sii" is discouraged (2 uses).
 New usage of "siii" is discouraged (2 uses).
 New usage of "siilem1" is discouraged (1 uses).
 New usage of "siilem2" is discouraged (1 uses).
-New usage of "simp1OLD" is discouraged (0 uses).
-New usage of "simp2OLD" is discouraged (0 uses).
-New usage of "simp3OLD" is discouraged (0 uses).
-New usage of "simpl11OLD" is discouraged (0 uses).
-New usage of "simpl12OLD" is discouraged (0 uses).
-New usage of "simpl13OLD" is discouraged (0 uses).
-New usage of "simpl1OLD" is discouraged (0 uses).
-New usage of "simpl1lOLD" is discouraged (0 uses).
-New usage of "simpl1rOLD" is discouraged (0 uses).
-New usage of "simpl21OLD" is discouraged (0 uses).
-New usage of "simpl22OLD" is discouraged (0 uses).
-New usage of "simpl23OLD" is discouraged (0 uses).
-New usage of "simpl2OLD" is discouraged (0 uses).
-New usage of "simpl2lOLD" is discouraged (0 uses).
-New usage of "simpl2rOLD" is discouraged (0 uses).
-New usage of "simpl31OLD" is discouraged (0 uses).
-New usage of "simpl32OLD" is discouraged (0 uses).
-New usage of "simpl33OLD" is discouraged (0 uses).
-New usage of "simpl3OLD" is discouraged (0 uses).
-New usage of "simpl3lOLD" is discouraged (0 uses).
-New usage of "simpl3rOLD" is discouraged (0 uses).
 New usage of "simplbi2VD" is discouraged (0 uses).
 New usage of "simplbi2comtVD" is discouraged (0 uses).
-New usage of "simpll1OLD" is discouraged (0 uses).
-New usage of "simpll2OLD" is discouraged (0 uses).
-New usage of "simpll3OLD" is discouraged (0 uses).
-New usage of "simplr1OLD" is discouraged (0 uses).
-New usage of "simplr2OLD" is discouraged (0 uses).
-New usage of "simplr3OLD" is discouraged (0 uses).
-New usage of "simpr11OLD" is discouraged (0 uses).
-New usage of "simpr12OLD" is discouraged (0 uses).
-New usage of "simpr13OLD" is discouraged (0 uses).
-New usage of "simpr1OLD" is discouraged (0 uses).
-New usage of "simpr1lOLD" is discouraged (0 uses).
-New usage of "simpr1rOLD" is discouraged (0 uses).
-New usage of "simpr21OLD" is discouraged (0 uses).
-New usage of "simpr22OLD" is discouraged (0 uses).
-New usage of "simpr23OLD" is discouraged (0 uses).
-New usage of "simpr2OLD" is discouraged (0 uses).
-New usage of "simpr2lOLD" is discouraged (0 uses).
-New usage of "simpr2rOLD" is discouraged (0 uses).
-New usage of "simpr31OLD" is discouraged (0 uses).
-New usage of "simpr32OLD" is discouraged (0 uses).
-New usage of "simpr33OLD" is discouraged (0 uses).
-New usage of "simpr3OLD" is discouraged (0 uses).
-New usage of "simpr3lOLD" is discouraged (0 uses).
-New usage of "simpr3rOLD" is discouraged (0 uses).
-New usage of "simprl1OLD" is discouraged (0 uses).
-New usage of "simprl2OLD" is discouraged (0 uses).
-New usage of "simprl3OLD" is discouraged (0 uses).
-New usage of "simprr1OLD" is discouraged (0 uses).
-New usage of "simprr2OLD" is discouraged (0 uses).
-New usage of "simprr3OLD" is discouraged (0 uses).
 New usage of "sineq0ALT" is discouraged (0 uses).
 New usage of "smcn" is discouraged (3 uses).
 New usage of "smcnlem" is discouraged (1 uses).
@@ -18175,42 +18100,25 @@ Proof modification of "2uasbanh" is discouraged (214 steps).
 Proof modification of "2uasbanhVD" is discouraged (313 steps).
 Proof modification of "2zrngALT" is discouraged (207 steps).
 Proof modification of "31prm" is discouraged (541 steps).
-Proof modification of "3adant1OLD" is discouraged (14 steps).
-Proof modification of "3adant1lOLD" is discouraged (20 steps).
-Proof modification of "3adant1rOLD" is discouraged (20 steps).
-Proof modification of "3adant2OLD" is discouraged (14 steps).
 Proof modification of "3adant2lOLD" is discouraged (19 steps).
 Proof modification of "3adant2rOLD" is discouraged (19 steps).
-Proof modification of "3adant3OLD" is discouraged (14 steps).
 Proof modification of "3adant3lOLD" is discouraged (19 steps).
 Proof modification of "3adant3rOLD" is discouraged (19 steps).
 Proof modification of "3anidm12p1" is discouraged (5 steps).
 Proof modification of "3anidm12p2" is discouraged (19 steps).
 Proof modification of "3cnOLD" is discouraged (3 steps).
-Proof modification of "3com12OLD" is discouraged (15 steps).
-Proof modification of "3com13OLD" is discouraged (15 steps).
 Proof modification of "3dimlem3OLDN" is discouraged (335 steps).
 Proof modification of "3dimlem4OLDN" is discouraged (338 steps).
-Proof modification of "3expOLD" is discouraged (14 steps).
-Proof modification of "3expaOLD" is discouraged (11 steps).
-Proof modification of "3expiaOLD" is discouraged (12 steps).
-Proof modification of "3imp21OLD" is discouraged (11 steps).
-Proof modification of "3impOLD" is discouraged (21 steps).
-Proof modification of "3impaOLD" is discouraged (11 steps).
 Proof modification of "3impdirp1" is discouraged (21 steps).
 Proof modification of "3impexpVD" is discouraged (104 steps).
 Proof modification of "3impexpbicomVD" is discouraged (89 steps).
 Proof modification of "3impexpbicomiVD" is discouraged (28 steps).
-Proof modification of "3impiaOLD" is discouraged (12 steps).
 Proof modification of "3jaoOLD" is discouraged (49 steps).
 Proof modification of "3lcm2e6woprm" is discouraged (285 steps).
 Proof modification of "3orbi123" is discouraged (29 steps).
 Proof modification of "3orbi123VD" is discouraged (134 steps).
 Proof modification of "3ornot23" is discouraged (28 steps).
 Proof modification of "3ornot23VD" is discouraged (74 steps).
-Proof modification of "3simpaOLD" is discouraged (13 steps).
-Proof modification of "3simpbOLD" is discouraged (20 steps).
-Proof modification of "3simpcOLD" is discouraged (20 steps).
 Proof modification of "4cnOLD" is discouraged (3 steps).
 Proof modification of "5cnOLD" is discouraged (3 steps).
 Proof modification of "6cnOLD" is discouraged (3 steps).
@@ -18227,12 +18135,6 @@ Proof modification of "abbiiOLDOLD" is discouraged (17 steps).
 Proof modification of "abeq2fOLD" is discouraged (46 steps).
 Proof modification of "abscncfALT" is discouraged (71 steps).
 Proof modification of "ackm" is discouraged (71 steps).
-Proof modification of "ad5ant123OLD" is discouraged (45 steps).
-Proof modification of "ad5ant124OLD" is discouraged (51 steps).
-Proof modification of "ad5ant125OLD" is discouraged (30 steps).
-Proof modification of "ad5ant134OLD" is discouraged (56 steps).
-Proof modification of "ad5ant135OLD" is discouraged (67 steps).
-Proof modification of "ad5ant145OLD" is discouraged (29 steps).
 Proof modification of "addlenrevswrdOLD" is discouraged (91 steps).
 Proof modification of "addlenswrdOLD" is discouraged (89 steps).
 Proof modification of "addltmulALT" is discouraged (497 steps).
@@ -19514,7 +19416,6 @@ Proof modification of "pm13.18OLD" is discouraged (28 steps).
 Proof modification of "pm2.21ddALT" is discouraged (10 steps).
 Proof modification of "pm2.43bgbi" is discouraged (16 steps).
 Proof modification of "pm2.43cbi" is discouraged (34 steps).
-Proof modification of "pm3.2an3OLD" is discouraged (19 steps).
 Proof modification of "pncan3OLD" is discouraged (49 steps).
 Proof modification of "pnfexOLD" is discouraged (4 steps).
 Proof modification of "preleqALT" is discouraged (115 steps).
@@ -19665,59 +19566,8 @@ Proof modification of "scmateALT" is discouraged (236 steps).
 Proof modification of "sgrpplusgaopALT" is discouraged (82 steps).
 Proof modification of "signstfveq0OLD" is discouraged (737 steps).
 Proof modification of "signsvtn0OLD" is discouraged (802 steps).
-Proof modification of "simp1OLD" is discouraged (11 steps).
-Proof modification of "simp2OLD" is discouraged (11 steps).
-Proof modification of "simp3OLD" is discouraged (11 steps).
-Proof modification of "simpl11OLD" is discouraged (16 steps).
-Proof modification of "simpl12OLD" is discouraged (16 steps).
-Proof modification of "simpl13OLD" is discouraged (16 steps).
-Proof modification of "simpl1OLD" is discouraged (11 steps).
-Proof modification of "simpl1lOLD" is discouraged (14 steps).
-Proof modification of "simpl1rOLD" is discouraged (14 steps).
-Proof modification of "simpl21OLD" is discouraged (16 steps).
-Proof modification of "simpl22OLD" is discouraged (16 steps).
-Proof modification of "simpl23OLD" is discouraged (16 steps).
-Proof modification of "simpl2OLD" is discouraged (11 steps).
-Proof modification of "simpl2lOLD" is discouraged (14 steps).
-Proof modification of "simpl2rOLD" is discouraged (14 steps).
-Proof modification of "simpl31OLD" is discouraged (16 steps).
-Proof modification of "simpl32OLD" is discouraged (16 steps).
-Proof modification of "simpl33OLD" is discouraged (16 steps).
-Proof modification of "simpl3OLD" is discouraged (11 steps).
-Proof modification of "simpl3lOLD" is discouraged (14 steps).
-Proof modification of "simpl3rOLD" is discouraged (14 steps).
 Proof modification of "simplbi2VD" is discouraged (24 steps).
 Proof modification of "simplbi2comtVD" is discouraged (42 steps).
-Proof modification of "simpll1OLD" is discouraged (14 steps).
-Proof modification of "simpll2OLD" is discouraged (14 steps).
-Proof modification of "simpll3OLD" is discouraged (14 steps).
-Proof modification of "simplr1OLD" is discouraged (14 steps).
-Proof modification of "simplr2OLD" is discouraged (14 steps).
-Proof modification of "simplr3OLD" is discouraged (14 steps).
-Proof modification of "simpr11OLD" is discouraged (16 steps).
-Proof modification of "simpr12OLD" is discouraged (16 steps).
-Proof modification of "simpr13OLD" is discouraged (16 steps).
-Proof modification of "simpr1OLD" is discouraged (11 steps).
-Proof modification of "simpr1lOLD" is discouraged (14 steps).
-Proof modification of "simpr1rOLD" is discouraged (14 steps).
-Proof modification of "simpr21OLD" is discouraged (16 steps).
-Proof modification of "simpr22OLD" is discouraged (16 steps).
-Proof modification of "simpr23OLD" is discouraged (16 steps).
-Proof modification of "simpr2OLD" is discouraged (11 steps).
-Proof modification of "simpr2lOLD" is discouraged (14 steps).
-Proof modification of "simpr2rOLD" is discouraged (14 steps).
-Proof modification of "simpr31OLD" is discouraged (16 steps).
-Proof modification of "simpr32OLD" is discouraged (16 steps).
-Proof modification of "simpr33OLD" is discouraged (16 steps).
-Proof modification of "simpr3OLD" is discouraged (11 steps).
-Proof modification of "simpr3lOLD" is discouraged (14 steps).
-Proof modification of "simpr3rOLD" is discouraged (14 steps).
-Proof modification of "simprl1OLD" is discouraged (14 steps).
-Proof modification of "simprl2OLD" is discouraged (14 steps).
-Proof modification of "simprl3OLD" is discouraged (14 steps).
-Proof modification of "simprr1OLD" is discouraged (14 steps).
-Proof modification of "simprr2OLD" is discouraged (14 steps).
-Proof modification of "simprr3OLD" is discouraged (14 steps).
 Proof modification of "sineq0ALT" is discouraged (986 steps).
 Proof modification of "smgrpassOLD" is discouraged (54 steps).
 Proof modification of "smgrpismgmOLD" is discouraged (22 steps).