From f34c8aa6d055b234fff7c9543893bec02517567d Mon Sep 17 00:00:00 2001
From: GinoGiotto <73717712+GinoGiotto@users.noreply.github.com>
Date: Sun, 14 Jan 2024 15:38:00 +0100
Subject: [PATCH] moved cbv2w in main (#3764)

---
 discouraged |  2 ++
 set.mm      | 63 +++++++++++++++++++++++------------------------------
 2 files changed, 29 insertions(+), 36 deletions(-)

diff --git a/discouraged b/discouraged
index 2e7a163b09..f2c7f41e59 100755
--- a/discouraged
+++ b/discouraged
@@ -14058,6 +14058,7 @@ New usage of "cbncms" is discouraged (5 uses).
 New usage of "cbv2OLD" is discouraged (0 uses).
 New usage of "cbvabvOLD" is discouraged (0 uses).
 New usage of "cbval2OLD" is discouraged (0 uses).
+New usage of "cbval2vOLD" is discouraged (0 uses).
 New usage of "cbvalvOLD" is discouraged (0 uses).
 New usage of "cbveuALT" is discouraged (0 uses).
 New usage of "cbvexsv" is discouraged (2 uses).
@@ -18208,6 +18209,7 @@ Proof modification of "cayleyhamiltonALT" is discouraged (657 steps).
 Proof modification of "cbv2OLD" is discouraged (40 steps).
 Proof modification of "cbvabvOLD" is discouraged (12 steps).
 Proof modification of "cbval2OLD" is discouraged (85 steps).
+Proof modification of "cbval2vOLD" is discouraged (85 steps).
 Proof modification of "cbvalvOLD" is discouraged (53 steps).
 Proof modification of "cbveuALT" is discouraged (48 steps).
 Proof modification of "cbvexsv" is discouraged (29 steps).
diff --git a/set.mm b/set.mm
index 70f468237f..810ed64a54 100644
--- a/set.mm
+++ b/set.mm
@@ -19990,6 +19990,20 @@ Corresponds to the dual of Axiom (B) of modal logic.  (Contributed by NM,
       KACLZEKAUALAUBLUCUDDEABEGHMACDFIMDENZABCAUEBCLJOPQABDFRACEGRST $.
   $}
 
+  ${
+    $d x y $.
+    cbv2w.1 $e |- F/ x ph $.
+    cbv2w.2 $e |- F/ y ph $.
+    cbv2w.3 $e |- ( ph -> F/ y ps ) $.
+    cbv2w.4 $e |- ( ph -> F/ x ch ) $.
+    cbv2w.5 $e |- ( ph -> ( x = y -> ( ps <-> ch ) ) ) $.
+    $( Version of ~ cbv2 with a disjoint variable condition, which does not
+       require ~ ax-13 .  (Contributed by Gino Giotto, 10-Jan-2024.) $)
+    cbv2w $p |- ( ph -> ( A. x ps <-> A. y ch ) ) $=
+      ( wal weq wb wi biimp syl6 cbv1v equcomi biimpr syl56 impbid ) ABDKCEKABC
+      DEFGHIADELZBCMZBCNJBCOPQACBEDGFIHEDLUBAUCCBNEDRJBCSTQUA $.
+  $}
+
   ${
     $d x y $.
     cbv3hv.nf1 $e |- ( ph -> A. y ph ) $.
@@ -20034,8 +20048,16 @@ Corresponds to the dual of Axiom (B) of modal logic.  (Contributed by NM,
     cbval2v.4 $e |- F/ y ps $.
     cbval2v.5 $e |- ( ( x = z /\ y = w ) -> ( ph <-> ps ) ) $.
     $( Version of ~ cbval2 with a disjoint variable condition, which does not
-       require ~ ax-13 .  (Contributed by BJ, 16-Jun-2019.) $)
+       require ~ ax-13 .  (Contributed by BJ, 16-Jun-2019.)  (Proof shortened
+       by Gino Giotto, 10-Jan-2024.) $)
     cbval2v $p |- ( A. x A. y ph <-> A. z A. w ps ) $=
+      ( wal nfal weq nfv wnf a1i wb ex cbv2w cbvalv1 ) ADLBFLCEAEDGMBCFIMCENZAB
+      DFUBDOUBFOAFPUBHQBDPUBJQUBDFNABRKSTUA $.
+
+    $( Obsolete version of ~ cbval2v as of 14-Jan-2024.  (Contributed by BJ,
+       16-Jan-2019.)  (Proof modification is discouraged.)
+       (New usage is discouraged.) $)
+    cbval2vOLD $p |- ( A. x A. y ph <-> A. z A. w ps ) $=
       ( wal nfal weq wi nfv nfim wb cbvalv1 19.21v pm5.74d 3bitr3i pm5.74ri
       expcom ) ADLZBFLZCEAEDGMBCFIMCENZUEUFUGAOZDLUGBOZFLUGUEOUGUFOUHUIDFUGAFUG
       FPHQUGBDUGDPJQDFNZUGABUGUJABRKUDUASUGADTUGBFTUBUCS $.
@@ -538728,10 +538750,10 @@ coordinates of a barycenter of two points in one dimension (complex
        quantifier, using implicit substitution.  (Contributed by ML,
        27-Mar-2021.) $)
     cbveud $p |- ( ph -> ( E! x ps <-> E! y ch ) ) $=
-      ( vz cv wceq wb wal wex weu nfvd nfbid eu6 wa simpr equequ1 adantr sylcom
-      bibi12d ex cbv2 exbidv 3bitr4g ) ABDLZKLZMZNZDOZKPCELZULMZNZEOZKPBDQCEQAU
-      OUSKAUNURDEFGABUMEHAUMERSACUQDIAUQDRSAUKUPMZBCNZUNURNZJUTVAVBUTVAUABCUMUQ
-      UTVAUBUTUMUQNVADEKUCUDUFUGUEUHUIBDKTCEKTUJ $.
+      ( vz weq wb wal wex weu nfvd nfbid wa eu6 simpr equequ1 adantr bibi12d ex
+      sylcom cbv2w exbidv 3bitr4g ) ABDKLZMZDNZKOCEKLZMZENZKOBDPCEPAULUOKAUKUND
+      EFGABUJEHAUJEQRACUMDIAUMDQRADELZBCMZUKUNMZJUPUQURUPUQSBCUJUMUPUQUAUPUJUMM
+      UQDEKUBUCUDUEUFUGUHBDKTCEKTUI $.
   $}
 
   ${
@@ -629441,8 +629463,6 @@ standardize vectors to a length (norm) of one, but such definitions require
   - ~ moexexv -> ~ moexexvw
   - ~ rgen2a -> ~ rgen2
 
-  Note: ~ cbval2w is identical to ~ cbval2v , but has shorter proof.
-
   If everything goes well, at the end of the process, we should observe a
   reduction of ~ ax-13 usage from more than 30,000 theorems, as shown in
   https://github.com/GinoGiotto/set.mm/tree/ax-13-complete.
@@ -629566,20 +629586,6 @@ standardize vectors to a length (norm) of one, but such definitions require
       ( wnf wal wsb alrimi nfsb4tw syl ) ABEHZCIBCDJEHANCFGKBCDELM $.
   $}
 
-  ${
-    $d x y $.
-    cbv2w.1 $e |- F/ x ph $.
-    cbv2w.2 $e |- F/ y ph $.
-    cbv2w.3 $e |- ( ph -> F/ y ps ) $.
-    cbv2w.4 $e |- ( ph -> F/ x ch ) $.
-    cbv2w.5 $e |- ( ph -> ( x = y -> ( ps <-> ch ) ) ) $.
-    $( Version of ~ cbv2 with a disjoint variable condition, which does not
-       require ~ ax-13 .  (Contributed by Gino Giotto, 10-Jan-2024.) $)
-    cbv2w $p |- ( ph -> ( A. x ps <-> A. y ch ) ) $=
-      ( wal weq wb wi biimp syl6 cbv1v equcomi biimpr syl56 impbid ) ABDKCEKABC
-      DEFGHIADELZBCMZBCNJBCOPQACBEDGFIHEDLUBAUCCBNEDRJBCSTQUA $.
-  $}
-
   ${
     $d x ph $.  $d x ch $.  $d x y $.
     cbvaldw.1 $e |- F/ y ph $.
@@ -629645,21 +629651,6 @@ standardize vectors to a length (norm) of one, but such definitions require
       HNUAUBDEHIDHOEIOPABFGLQRUBUCHIBCFGJKMRST $.
   $}
 
-  ${
-    $d x y z w $.
-    cbval2w.1 $e |- F/ z ph $.
-    cbval2w.2 $e |- F/ w ph $.
-    cbval2w.3 $e |- F/ x ps $.
-    cbval2w.4 $e |- F/ y ps $.
-    cbval2w.5 $e |- ( ( x = z /\ y = w ) -> ( ph <-> ps ) ) $.
-    $( Version of ~ cbval2 with additional disjoint variable conditions, which
-       does not require ~ ax-13 .  (Contributed by Gino Giotto,
-       10-Jan-2024.) $)
-    cbval2w $p |- ( A. x A. y ph <-> A. z A. w ps ) $=
-      ( wal nfal weq nfv wnf a1i wb ex cbv2w cbvalv1 ) ADLBFLCEAEDGMBCFIMCENZAB
-      DFUBDOUBFOAFPUBHQBDPUBJQUBDFNABRKSTUA $.
-  $}
-
   ${
     $d x y $.
     exdistrfw.1 $e |- ( -. A. x x = y -> F/ y ph ) $.