From 42b3a801fb00150635a03ece6077fb320cb411ae Mon Sep 17 00:00:00 2001
From: metakunt <zugvzuzuguih@eclipso.me>
Date: Mon, 7 Oct 2024 01:19:04 +0200
Subject: [PATCH] Add counting for sticks and stones

---
 set.mm | 53 +++++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 53 insertions(+)

diff --git a/set.mm b/set.mm
index fae5a02962..aa7d7ceb9b 100644
--- a/set.mm
+++ b/set.mm
@@ -646481,6 +646481,59 @@ fixed reference functional determined by this vector (corresponding to
       AMUJUHZVAVBUOSVDVBVAVDVBVAUOMUPUQURUSUT $.
   $}
 
+  ${
+    $d A a i k l $.  $d A b i k l $.  $d A a j k l x y $.  $d B a f j l $.
+    $d B b f j l $.  $d B a i k l $.  $d F b i k $.  $d K a f j l x y $.
+    $d K b f j l x y $.  $d K a g i k $.  $d N a f j l x y $.
+    $d N b f j l x y $.  $d N a g i k $.  $d a f j l ph x y $.
+    $d b g i k ph $.
+    sticksstones14.1 $e |- ( ph -> N e. NN0 ) $.
+    sticksstones14.2 $e |- ( ph -> K e. NN0 ) $.
+    sticksstones14.3 $e |- F = ( a e. A |-> ( j e. ( 1 ... K ) |->
+    ( j + sum_ l e. ( 1 ... j ) ( a ` l ) ) ) ) $.
+    sticksstones14.4 $e |- G = ( b e. B |-> if ( K = 0
+     , { <. 1 , N >. } , ( k e. ( 1 ... ( K + 1 ) )
+        |-> if ( k = ( K + 1 ) , ( ( N + K ) - ( b ` K ) ) , if
+       ( k = 1 , ( ( b ` 1 ) - 1 )
+       , ( ( ( b ` k ) - ( b ` ( k - 1 ) ) ) - 1 ) ) ) ) ) ) $.
+    sticksstones14.5 $e |- A = { g | ( g : ( 1 ... ( K + 1 ) ) --> NN0 /\
+     sum_ i e. ( 1 ... ( K + 1 ) ) ( g ` i ) = N ) } $.
+    sticksstones14.6 $e |- B = { f | ( f : ( 1 ... K ) --> ( 1 ... ( N + K ) )
+    /\ A. x e. ( 1 ... K ) A. y e. ( 1 ... K ) ( x < y ->
+    ( f ` x ) < ( f ` y ) ) ) } $.
+    $( Sticks and stones with definitions as hypotheses.  (Contributed by
+       metakunt, 7-Oct-2024.) $)
+    sticksstones14 $p |- ( ph -> ( # ` A ) = ( ( N + K ) _C K ) ) $=
+      ( chash cfv caddc co cbc cvv c1 cfz cn0 cv wf csu wceq wa cab a1i wcel wi
+      wss simpl ss2abdv cfn fzfid nn0ex mapex syl2anc sticksstones13 hasheqf1od
+      ssexg eqeltrd nn0addcld sticksstones5 eqtrd ) ADUDUEEUDUENMUFUGZMUHUGADEU
+      IKADUJMUJUFUGZUKUGZULGUMZUNZVSHUMVTUEHUONUPZUQZGURZUIDWDUPAUBUSAWDWAGURZV
+      BWEUIUTZWDUIUTAWCWAGWCWAVAAWAWBVCUSVDAVSVEUTULUIUTZWFAUJVRVFWGAVGUSVSULVE
+      UIGVHVIWDWEUIVLVIVMABCDEFGHIJKLMNOPQRSTUAUBUCVJVKABCEFMVQANMRSVNSUCVOVP
+      $.
+  $}
+
+  ${
+    $d A i t u v w x y z $.  $d K f l t u v x y z $.  $d K g i u v w $.
+    $d N f l t u v x y z $.  $d N g i u v w $.  $d f ph t u v x y z $.
+    $d g i ph u v w $.  $d i l t u v w x y z $.
+    sticksstones15.1 $e |- ( ph -> N e. NN0 ) $.
+    sticksstones15.2 $e |- ( ph -> K e. NN0 ) $.
+    sticksstones15.3 $e |- A = { g | ( g : ( 1 ... ( K + 1 ) ) --> NN0 /\
+     sum_ i e. ( 1 ... ( K + 1 ) ) ( g ` i ) = N ) } $.
+    $( Sticks and stones with almost collapsed definitions for positive
+       integers.  (Contributed by metakunt, 7-Oct-2024.) $)
+    sticksstones15 $p |- ( ph -> ( # ` A ) = ( ( N + K ) _C K ) ) $=
+      ( vx vy c1 cfz co cv clt cfv wral cmpt cmin vl vf vz vw vv vt vu caddc wf
+      wbr wi wa cab csu cc0 wceq cop csn cif eqid fveq1 breq12d imbi2d 2ralbidv
+      feq1 anbi12d cbvabv sticksstones14 ) AJKBLEMNZLFEUHNZMNZUAOZUIZJOZKOZPUJZ
+      VNVLQZVOVLQZPUJZUKZKVIRJVIRZULZUAUMZUBCDUCUDUEBUCVIUCOZLWDMNUFOUEOQUFUNUH
+      NSSZUGWCEUOUPLFUQURUDLELUHNZMNUDOZWFUPVJEUGOZQTNWGLUPLWHQLTNWGWHQWGLTNWHQ
+      TNLTNUSUSSUSSZEFUEUGUFGHWEUTWIUTIWBVIVKUBOZUIZVPVNWJQZVOWJQZPUJZUKZKVIRJV
+      IRZULUAUBVLWJUPZVMWKWAWPVIVKVLWJVEWQVTWOJKVIVIWQVSWNVPWQVQWLVRWMPVNVLWJVA
+      VOVLWJVAVBVCVDVFVGVH $.
+  $}
+
 $(
 =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
   Permutation results