misc.

* new theorem ~1strstr1
* use of ~1strstr discouraged
* proof of ~1strbas shortened
* ~baseltedgf  renamed ~basendxltedgfndx

Author: avekens

changes-set.txt

@@ -94,6 +94,7 @@ make a github issue.)
 
 DONE:
 Date      Old       New         Notes
+15-Nov-24 baseltedgf basendxltedgfndx 
 12-Nov-24 sseldi    sselid      compare to sselii or sseldd
  9-Nov-24 eqsb3     eqsb1
  9-Nov-24 eqsbc3    eqsbc1

discouraged

@@ -189,6 +189,7 @@
 "1sr" is used by "axi2m1".
 "1sr" is used by "axicn".
 "1sr" is used by "supsr".
+"1strstr" is used by "1strbasOLD".
 "1t1e1ALT" is used by "nnmul1com".
 "1t1e1ALT" is used by "remulinvcom".
 "1t1e1ALT" is used by "sn-0tie0".
@@ -1672,8 +1673,8 @@
 "basendx" is used by "1strstr".
 "basendx" is used by "2strstr".
 "basendx" is used by "2strstr1OLD".
-"basendx" is used by "baseltedgf".
 "basendx" is used by "basendxltdsndx".
+"basendx" is used by "basendxltedgfndx".
 "basendx" is used by "basendxltplendx".
 "basendx" is used by "basendxltplusgndx".
 "basendx" is used by "basendxlttsetndx".
@@ -5975,7 +5976,7 @@
 "e333" is used by "e33".
 "e3bi" is used by "en3lplem2VD".
 "e3bir" is used by "en3lplem2VD".
-"edgfndx" is used by "baseltedgf".
+"edgfndx" is used by "basendxltedgfndx".
 "edgfndx" is used by "edgfndxnn".
 "ee03" is used by "ee03an".
 "ee03" is used by "suctrALT2".
@@ -14254,6 +14255,8 @@ New usage of "1pi" is discouraged (11 uses).
 New usage of "1pr" is discouraged (16 uses).
 New usage of "1psubclN" is discouraged (0 uses).
 New usage of "1sr" is discouraged (8 uses).
+New usage of "1strbasOLD" is discouraged (0 uses).
+New usage of "1strstr" is discouraged (1 uses).
 New usage of "1strwunOLD" is discouraged (0 uses).
 New usage of "1t1e1ALT" is discouraged (3 uses).
 New usage of "235t711" is discouraged (0 uses).
@@ -19469,6 +19472,7 @@ Proof modification of "1div0apr" is discouraged (77 steps).
 Proof modification of "1oexOLD" is discouraged (4 steps).
 Proof modification of "1p1e2apr1" is discouraged (7 steps).
 Proof modification of "1p2e3ALT" is discouraged (7 steps).
+Proof modification of "1strbasOLD" is discouraged (22 steps).
 Proof modification of "1strwunOLD" is discouraged (20 steps).
 Proof modification of "1t1e1ALT" is discouraged (13 steps).
 Proof modification of "2bornot2b" is discouraged (26 steps).

set.mm

@@ -200407,14 +200407,28 @@ C_ dom ( S sSet <. I , E >. ) ) $=
 
   ${
     1str.g $e |- G = { <. ( Base ` ndx ) , B >. } $.
-    $( A constructed one-slot structure.  (Contributed by AV, 27-Mar-2020.) $)
+    $( A constructed one-slot structure.  Depending on hard-coded index.  Use
+       ~ 1strstr1 instead.  (Contributed by AV, 27-Mar-2020.)
+       (New usage is discouraged.) $)
     1strstr $p |- G Struct <. 1 , 1 >. $=
       ( cnx cbs cfv cop csn c1 cstr 1nn basendx strle1 eqbrtri ) BDEFZAGHIIGJCO
       IAKLMN $.
 
+    $( A constructed one-slot structure.  (Contributed by AV, 15-Nov-2024.) $)
+    1strstr1 $p |- G Struct <. ( Base ` ndx ) , ( Base ` ndx ) >. $=
+      ( cnx cbs cfv cop csn cstr basendxnn eqid strle1 eqbrtri ) BDEFZAGHNNGICN
+      NAJNKLM $.
+
     $( The base set of a constructed one-slot structure.  (Contributed by AV,
-       27-Mar-2020.) $)
+       27-Mar-2020.)  (Proof shortened by AV, 15-Nov-2024.) $)
     1strbas $p |- ( B e. V -> B = ( Base ` G ) ) $=
+      ( cbs cnx cfv cop 1strstr1 baseid csn eqimss2i strfv ) ABECFEGZNHABDIJBNA
+      HKDLM $.
+
+    $( Obsolete proof of ~ 1strbas as of 15-Nov-2024.  The base set of a
+       constructed one-slot structure.  (Contributed by AV, 27-Mar-2020.)
+       (Proof modification is discouraged.)  (New usage is discouraged.) $)
+    1strbasOLD $p |- ( B e. V -> B = ( Base ` G ) ) $=
       ( cbs c1 cop 1strstr baseid cnx cfv csn eqimss2i strfv ) ABECFFGABDHIBJEK
       AGLDMN $.
 
@@ -409551,12 +409565,12 @@ otherwise it could not be used in an extensible structure (slots must be
   $( The index value of the ` Base ` slot is less than the index value of the
      ` .ef ` slot.  (Contributed by AV, 21-Sep-2020.)  (Proof shortened by AV,
      30-Oct-2024.) $)
-  baseltedgf $p |- ( Base ` ndx ) < ( .ef ` ndx ) $=
+  basendxltedgfndx $p |- ( Base ` ndx ) < ( .ef ` ndx ) $=
     ( c1 cdc cnx cbs cfv cedgf clt 1nn 8nn0 1nn0 declti basendx edgfndx 3brtr4i
     c8 1lt10 ) AAOBCDECFEGAOAHIJPKLMN $.
 
-  $( Obsolete proof of ~ baseltedgf as of 30-Oct-2024.  The index value of the
-     ` Base ` slot is less than the index value of the ` .ef ` slot.
+  $( Obsolete proof of ~ basendxltedgfndx as of 30-Oct-2024.  The index value
+     of the ` Base ` slot is less than the index value of the ` .ef ` slot.
      (Contributed by AV, 21-Sep-2020.)  (Proof modification is discouraged.)
      (New usage is discouraged.) $)
   baseltedgfOLD $p |- ( Base ` ndx ) < ( .ef ` ndx ) $=
@@ -409566,7 +409580,8 @@ otherwise it could not be used in an extensible structure (slots must be
   $( The slots ` Base ` and ` .ef ` are different.  (Contributed by AV,
      21-Sep-2020.) $)
   basendxnedgfndx $p |- ( Base ` ndx ) =/= ( .ef ` ndx ) $=
-    ( cnx cbs cfv cedgf basendxnn nnrei baseltedgf ltneii ) ABCZADCIEFGH $.
+    ( cnx cbs cfv cedgf basendxnn nnrei basendxltedgfndx ltneii ) ABCZADCIEFGH
+    $.
 
 
 $(
@@ -409980,13 +409995,13 @@ class is an extensible structure (containing a slot for "edge functions")
        and indexed edges is actually an extensible structure.  (Contributed by
        AV, 23-Nov-2020.) $)
     struct2grstr $p |- G Struct <. ( Base ` ndx ) , ( .ef ` ndx ) >. $=
-      ( cnx cedgf cfv baseltedgf edgfndxnn 2strstr1 ) CABEFGDHIJ $.
+      ( cnx cedgf cfv basendxltedgfndx edgfndxnn 2strstr1 ) CABEFGDHIJ $.
 
     $( The set of vertices of a graph represented as an extensible structure
        with vertices as base set and indexed edges.  (Contributed by AV,
        23-Sep-2020.) $)
     struct2grvtx $p |- ( ( V e. X /\ E e. Y ) -> ( Vtx ` G ) = V ) $=
-      ( cnx cedgf cfv edgfndxnn baseltedgf structvtxval ) GHIABCDEJKFL $.
+      ( cnx cedgf cfv edgfndxnn basendxltedgfndx structvtxval ) GHIABCDEJKFL $.
 
     $( The set of indexed edges of a graph represented as an extensible
        structure with vertices as base set and indexed edges.  (Contributed by