00:02:06 right, I thought it may have been a natural pause in the drama, but clearly not. 00:02:35 Oh, that means oerjan can't read what we're saying. 00:02:42 `owrjan 00:02:43 Your omnidryad saddle principal ideal golfing toe-obsessed "Darth Ook" oerjan the shifty eldrazi grinch is a punctual expert in minor compaction. Also a Groadep who minces Roald Dahl. He could never remember the word "amortized" so he put it here for convenience. His arkup-nemesis is mediawiki's default diff. He twice punned without noticing it. 00:06:59 I'm mainly interested is there was any more info on the cryptic Proto IE quote from Orin. Anything else that happened around that time is probably better lost 00:07:23 s/is there/if there/ 00:08:35 fungot: do you like PIE? 00:08:35 salpynx: ' but he looks the spit and fnord' people makin' cracks about bananas.' they'll say: the least we can do for him?' 00:09:01 PIE is fine but dynamic linking is not so good. 00:12:20 PIE is overloaded (I had to look that one up). 00:12:39 pooch-independent executable 00:17:05 salpynx: *sokʷh₂yóteh₂ti *gʷíh₃womos : We live in a society in PIE 00:20:34 orin: nice, I got "we live". Couldn't find the roots of the first word, and was pretty sure my best guess of "Juice-thief" was incorrect (unless "society" = juice-sapping in PIE?) 00:26:30 -!- tromp has joined. 00:31:08 -!- tromp has quit (Ping timeout: 259 seconds). 00:34:02 -!- A_ has joined. 00:34:27 Found it: *sokʷ-yo- companion vs. *sokʷos juice/resin. I won't make that mistake again! 00:34:37 Hi 00:35:44 (I have nothing to say here, so I will quit now.) 00:35:47 -!- A_ has left. 00:36:57 -!- A_ has joined. 00:38:30 -!- A_ has quit (Client Quit). 00:44:15 -!- oerjan has joined. 00:45:57 is something wrong with the logs? 00:46:37 oerjan: yes, they have not been updating since the long page move msg 00:48:28 sheesh 00:53:49 * oerjan merges with tunes logs 00:55:39 curiously, tunes doesn't have the very last line in the other logs, i guess the bot logged it but crashed before actually saying it. 00:58:05 Oh, that means oerjan can't read what we're saying. <-- DON'T BET ON IT 01:08:31 -!- tromp has joined. 01:22:14 -!- arseniiv has quit (Ping timeout: 272 seconds). 01:43:36 -!- FreeFull has quit. 01:44:08 -!- mniip has quit (Quit: This page is intentionally left blank.). 01:44:24 -!- tromp has quit (Remote host closed the connection). 01:51:10 -!- mniip has joined. 01:53:56 -!- budonyc has joined. 02:03:13 -!- mniip has quit (Quit: This page is intentionally left blank.). 02:11:08 -!- mniip has joined. 02:20:26 -!- tromp has joined. 02:21:46 -!- mniip has quit (Ping timeout: 604 seconds). 02:25:34 -!- tromp has quit (Ping timeout: 272 seconds). 02:28:28 -!- budonyc has quit (Quit: Leaving). 02:32:21 oerjan: tunes? 02:32:29 like the operating system? 02:42:11 adu: yes, although just because it's on the same site, see topic 03:18:47 -!- Hooloovo0 has quit (Quit: Temporarily refracted into a free-standing prism.). 03:19:05 -!- Hooloovo0 has joined. 03:35:32 -!- MDude has quit (Quit: Going offline, see ya! (www.adiirc.com)). 03:49:54 -!- A__ has joined. 03:51:04 I have devised an idea of a sorting algorithm - I decided to call it "Got a match?", but there could be better names for this. 03:51:20 Here is a glance of the algorithm of that algorithm: 03:52:39 (in natural language) : While the modified state does not equal to the current state: \ 03:53:16 Put the leftmost element in the unsorted list of elements after the rightmost matching number 03:53:34 Delete the leftmost unborted element 03:53:59 If the end of the list of elements is less than the beginning of that list: 03:54:13 Reverse-cat the whole list of elements 03:55:10 And that is it. This algorithm has certain limitations (i.e. it does not support sorting a list of elements where all elements are unique.) 03:55:43 I will put a working demonstration of this algorithm here: 03:56:26 Task: Sort 123123 -> 231123 -> 311223 -> 112233 03:56:51 The end of the list is larger than the beginning of the list, so the algorithm ends. 03:58:01 (This algorithm is inspired by the desire to not comparing elements of the list every time and to not waste too much space for that algorithm.) 03:58:37 You may be confused of the last part of the algorithm: why do we need to reverse-cat the list of elements sometimes? 03:58:53 Well, an example clears up the confusion: 04:00:03 (This example is complex; please don't mind) 32321321321 -> 23213213321 -> 32132133221 -> 04:00:53 21321333221 -> 13213332221 -> 32133322211 -> 21333322211 -> 04:01:19 13333222211 -> 33332222111 04:01:53 13333222211 -> 33332222111 (And see, it is in reversed order. Then you would have to reverse cat that string in order to sort correctly.) 04:02:41 I am done; any questions? (And I apoligize for using up too much space for it.) 04:06:14 I have nothing to do here. fungot 04:06:14 A__: " the deacon is far away. i am a stranger in a familiar script: 04:06:26 Fungot 04:06:45 fungot: " the deacon is far away. i am a stranger in a familiar script: 04:06:46 A__: " just as you go along to the study of time so wholeheartedly that, for the appropriate moment to descend, and thought about cigar smoke and flowing drink and fnord voices never ever gave cushy numbers to the likes of us any more... it chokes us to death with her own umbrella. 04:07:00 fungot: " just as you go along to the study of time so wholeheartedly that, for the appropriate moment to descend, and thought about cigar smoke and flowing drink and fnord voices never ever gave cushy numbers to the likes of us any more... it chokes us to death with her own umbrella. 04:07:00 A__: " er. what's bodacious mean?" asked granny. " gytha meant well, i, fnord' the faces of many of the things that had been tossed aside on to the roof of the city's kings, all haughty stance and imperious haircut. in fact, since the pyramids took up so much, is... 04:07:15 fungot: " er. what's bodacious mean?" asked granny. " gytha meant well, i, fnord' the faces of many of the things that had been tossed aside on to the roof of the city's kings, all haughty stance and imperious haircut. in fact, since the pyramids took up so much, is... 04:07:15 A__: ' intended to be a blob of swallow's vomit?' said 04:07:26 fungot: ' intended to be a blob of swallow's vomit?' said 04:07:44 Hey, fungot: ' intended to be a blob of swallow's vomit?' said 04:08:27 -!- tromp has joined. 04:08:58 You need to stop doing the thing where you paste the text other people write. 04:09:40 Did you see what I just wrote(presenting an algorithm)? 04:10:21 I saw it but I didn't read it. 04:11:12 -!- A__ has left. 04:13:05 -!- tromp has quit (Ping timeout: 258 seconds). 04:17:35 -!- Hooloovo0 has quit (Ping timeout: 248 seconds). 04:21:20 -!- Hooloovo0 has joined. 04:36:48 -!- tswett[m] has quit (Read error: Connection reset by peer). 04:37:01 -!- wmww has quit (Read error: Connection reset by peer). 04:39:27 -!- john_metcalf has quit (Ping timeout: 248 seconds). 04:39:59 -!- economicsbat_ has quit (Ping timeout: 248 seconds). 04:42:05 -!- economicsbat has joined. 04:43:08 -!- tswett[m] has joined. 05:00:58 -!- wmww has joined. 05:01:52 -!- mniip has joined. 05:08:43 -!- quintopia has joined. 05:33:32 -!- salpynx has quit (Quit: *apóh₁eimi). 05:38:09 -!- sprocklem has quit (Quit: brb). 05:38:25 -!- sprocklem has joined. 05:52:27 -!- imode has quit (Ping timeout: 248 seconds). 05:57:47 -!- Frater_EST has joined. 06:10:56 -!- Sgeo__ has joined. 06:14:12 -!- Sgeo_ has quit (Ping timeout: 272 seconds). 06:35:31 -!- AnotherTest has joined. 07:02:58 -!- clog has quit (Ping timeout: 245 seconds). 07:03:05 -!- clog has joined. 07:07:52 -!- mniip has quit (Ping timeout: 624 seconds). 07:09:24 -!- Sgeo_ has joined. 07:10:20 -!- mniip has joined. 07:12:19 -!- Sgeo__ has quit (Ping timeout: 246 seconds). 07:24:28 -!- oerjan has quit (Quit: leaving). 07:35:40 -!- Frater_EST has left. 07:54:50 -!- adu has quit (Quit: adu). 08:16:31 -!- uplime has changed nick to telnet. 08:24:25 -!- Sgeo__ has joined. 08:27:33 -!- Sgeo_ has quit (Ping timeout: 258 seconds). 08:32:52 -!- tromp has joined. 08:34:11 -!- tromp has quit (Client Quit). 08:43:54 -!- Sgeo_ has joined. 08:47:28 -!- Sgeo__ has quit (Ping timeout: 272 seconds). 08:49:39 -!- izabera has changed nick to Veronica. 08:50:08 -!- Veronica has changed nick to Guest49041. 08:50:19 -!- Guest49041 has changed nick to izabera. 08:53:55 -!- Sgeo__ has joined. 08:54:57 -!- tromp has joined. 08:56:00 -!- tromp has quit (Remote host closed the connection). 08:57:39 -!- Sgeo_ has quit (Ping timeout: 268 seconds). 09:08:23 -!- Vorpal has quit (Ping timeout: 245 seconds). 09:10:14 -!- Vorpal has joined. 09:14:26 -!- Sgeo__ has quit (Read error: Connection reset by peer). 09:14:53 -!- Sgeo__ has joined. 09:15:11 -!- Vorpal has quit (Ping timeout: 248 seconds). 09:15:43 -!- Vorpal has joined. 09:15:43 -!- Vorpal has quit (Changing host). 09:15:43 -!- Vorpal has joined. 09:27:14 -!- tromp has joined. 09:34:39 -!- wob_jonas has joined. 09:39:23 @tell oerjan oh no, now things may be going horribly right in the long term 09:39:23 Consider it noted. 09:40:54 -!- Guest91 has joined. 09:41:08 `5 09:41:10 1/2:1178) kmc: madam president, i have taken on serious proportions. \ 787) and all this time I thought we were talking about postmodern analysis of junk mail delivery methods and simulations of elephant breeding patterns \ 558) Ngevd:. i'm so kind, even to assholes! anmaster no not markov anmaster no not markov anmaster no not markov anmaster no not markov anmaster no not markov \ 498) now that we've cleared that u 09:41:14 `n 09:41:15 2/2:p let us hug fungot = elliott_: let's not start that again." \ 608) ais523: I pronounce "xor" by punching myself in the face and then "or" 09:41:37 fungot: hug? 09:41:38 shachaf: ' he wath my only friend!' she snapped, " never mind about my son," said carrot doggedly, " i thought that's what we always used to say the verruca gnome. 09:41:50 ^style 09:41:50 Available: agora alice c64 ct darwin discworld* enron europarl ff7 fisher fungot homestuck ic irc iwcs jargon lovecraft nethack oots pa qwantz sms speeches ss wp ukparl youtube 09:42:00 ^style speeches 09:42:00 Selected style: speeches (misc. speeches from Project Gutenberg) 09:42:07 fungot is upon us 09:42:08 shachaf: " a refutation of his whole argument? paley says, indeed, will appear beneath their dignity. the temerity of adventurers was much justified by the ill order of every state, which is always very near to it in display of gaiety, splendour, and which the disastrous events of the war against jacobinism, louis the fourteenth brittany had its states; burgundy had its states; and yet there is no such criterion, it must be raw 09:42:18 `5 09:42:20 1/2:1087) I prefer goat memory. I feel it's more reliable, like a vinyl over a CD. \ 331) [after a long string of Lymia getting lambdabot to spit out huge, meaningless type signatures] I need to learn more Haskell... ..I need to get op privs. \ 1222) when i was a kid it used to snow on christmas eve. what is this "freezing rain", "sleet" crap? yeah seriously, who is evn in charge anymore? apparently 09:42:23 `n 09:42:23 2/2:not santa claus Santa Claus is dead by now. \ 695) elliott_: how usable is borges in the real world \ 722) is tswett Warrigal? 09:44:50 -!- ais523 has joined. 09:48:23 -!- Sgeo_ has joined. 09:52:30 Oh does that mean that we have our own global warming theory... namely, Santa Claus died? 09:52:42 -!- Sgeo__ has quit (Ping timeout: 272 seconds). 09:52:49 that's not really the same language, is it? 09:54:51 wob_jonas: are you talking about the obfuscated tiny C dialects? 09:55:15 I haven't looked at it in detail, but if it's a different language (and not an obvious derivative of the original) it should be discussed on a different page 10:01:18 -!- MDude has joined. 10:01:28 ais523: yes 10:01:58 they're two somewhat unrelated implementations 10:02:47 the older one is a bytecode interpreter that has some builtin functions; the newer one is bellard's compiler which "cheats" by linking symbols in from libc 10:03:24 The older one calls itself OC = obfuscated C. Not sure where I stand on this. 10:05:12 also the older one uses the trick where the interpreter is written in C, but the compiler from C to the bytecode that that interpreter understands is written in the bytecode, though not in a cheating way, because both are contained in the size limit 10:05:47 * int-e idly wonders about the copyright status of that BNF, and the licensing situation of IOCCC (especially early years). 10:06:12 ah no, I'm wrong 10:06:15 the compiler is written in C too 10:06:43 int-e: the licensing situation is quite clear: whoever submits the entry keeps all the rights 10:06:51 wob_jonas: it's written in C but the bytecode optimizer and compressor required to make everything fit isn't included 10:07:31 int-e: hmm,ok 10:11:40 I should probably make some kind of toy compiler, though not a tiny golfed one, at some point, just for the heck of learning 10:11:58 and potentially teaching, if I document it properly 10:13:23 -!- Lord_of_Life has quit (Ping timeout: 245 seconds). 10:14:57 -!- ais523 has quit (Quit: quit). 10:15:07 can you recommend a good text teaching how to make a register allocator for a compiler to a real-world ugly CISC architecture? 10:16:57 -!- Lord_of_Life has joined. 10:41:14 `? 299792458 10:41:15 299792458? ¯\(°​_o)/¯ 10:47:45 What's that, another C variant? 10:57:26 -!- Sgeo_ has quit (Read error: Connection reset by peer). 10:57:53 -!- Sgeo_ has joined. 11:08:56 -!- Guest91 has quit (Remote host closed the connection). 11:51:51 -!- sebbu3 has joined. 11:55:42 -!- sebbu has quit (Ping timeout: 258 seconds). 12:36:47 -!- zzo38 has quit (Ping timeout: 248 seconds). 13:09:38 -!- arseniiv has joined. 13:49:19 -!- Hooloovo0 has quit (Ping timeout: 248 seconds). 13:53:50 -!- Hooloovo0 has joined. 14:14:14 -!- moei has joined. 14:23:22 -!- sebbu3 has changed nick to sebbu. 15:17:58 -!- imode has joined. 15:22:39 -!- Hooloovo0 has quit (Ping timeout: 248 seconds). 15:27:48 -!- ais523 has joined. 15:28:00 -!- Hooloovo0 has joined. 15:34:59 -!- S_Gautam has joined. 15:35:32 -!- wob_jonas has quit (Remote host closed the connection). 15:50:35 -!- yaewa has joined. 15:51:46 -!- atslash has joined. 15:51:59 -!- moei has quit (Ping timeout: 248 seconds). 15:59:18 anyone have thoughts on this?: https://esolangs.org/wiki/Quadratic_sync_problem 15:59:58 it's one of the simplest problems I've found that isn't obviously Turing-incomplete (another example of a simple problem that isn't obviously Turing-incomplete is "does this recurrence relation ever reach 0?", but I think that one's less likely to be, not that either are particularly likely to be) 16:05:51 -!- Hooloovo0 has quit (Ping timeout: 248 seconds). 16:10:01 -!- Hooloovo0 has joined. 16:18:50 -!- ais523 has quit (Remote host closed the connection). 16:20:06 -!- ais523 has joined. 16:30:35 ais523: relevant keyword: https://en.wikipedia.org/wiki/Pell%27s_equation 16:31:10 hmm, that's not exactly the same, but it's pretty similar 16:32:31 even something simple like the negative Pell equation doesn't have a known solution technique 16:37:50 https://www.maths.ed.ac.uk/~v1ranick/papers/conwaysens.pdf 16:37:57 can this be applied in any way? I dont know 16:46:33 oh these are 2 single variable quadratic forms 16:46:40 but that is f or binary quadratic form 16:47:44 since the constants are non-negative I think you can bound x andy 16:47:48 and then check finitely many values 16:48:10 Pquadratic residuosity problem has no known efficient solutions 16:48:12 > 16:48:27 wel it's efficient to know if a solution exists (using legendre symbol), but not to find it? 17:31:47 -!- Phantom_Hoover has joined. 17:36:19 rain1: the symbol doesn't always tell you if a solution exists 17:36:55 it can tell you that it doesn't exist, but the legendre symbol's only defined for prime modulus, and the jacoby symbol is only a necessary condition, not a sufficient condition 17:37:33 oh shit i didn't know that 18:15:48 -!- FreeFull has joined. 18:31:59 -!- Hooloovo0 has quit (Ping timeout: 248 seconds). 18:32:49 `olist 1165 18:32:50 olist 1165: shachaf oerjan Sgeo FireFly boily nortti b_jonas 18:39:17 -!- MDude has quit (Quit: Going offline, see ya! (www.adiirc.com)). 18:42:52 -!- tromp_ has joined. 18:44:39 -!- Hooloovo0 has joined. 18:45:33 -!- tromp has quit (Ping timeout: 258 seconds). 19:20:05 -!- b_jonas has joined. 19:23:01 ais523: not a direct answer, but see https://cstheory.stackexchange.com/q/14124/8067 , especially the second paragraph of the question 19:25:18 "The problem can be equivalently stated as follows: given b,c∈N, determine whether the quadratic x²+by−c=0 has a solution x,y∈N." …but isn't that literally quadratic residuosity? 19:26:24 ais523: you asked for Turing-complete or at least possibly so, I don't think that gives any such problem 19:26:25 ah no: x²+by-c=0 <=> x²=-by+c, quadratic residuosity is x²=by+c 19:26:45 this question is about NP problems 19:26:47 and given that b and y are both constrained to be be non-negative the sign flip actually makes a difference 19:27:00 b_jonas: yes, but quadratic residuosity being NP-complete would be a major result 19:30:43 or, hmm, /does/ the sign flip make a difference? 19:31:27 if c>b² it doesn't 19:31:42 I won't help you thinking about this now, that's just a question I had come across earlier today 19:32:02 s/tion/tion post/ 19:32:19 if it's lower then it's a reduction of the "find the root" part of quadratic residuosity to a decision problem, but a different reduction from the normal one 19:36:09 if I'm not misunderstanding something, this seems like it might be major news for the crypto community (although possibly not; they care about average-case complexity, NP-completeness results normally focus on the worst case) 19:41:54 is factoring expected to be NP-complete? 19:41:56 i don't think it si 19:42:18 which makes this quadratic thing being NP-complete strange, because square roots mod N is usually seen as equivalent in difficulty to factoring N 19:42:20 it's expected to be NP-incomplete, although nobody actually knows what class it's in atm 19:42:55 rain1: decision-problem quadratic residuosity can be solved in P-time via a factoring oracle, yes 19:43:21 going the other way, a find-a-square-root algorithm can factor in P-time if you have a random number generator 19:43:40 err, randomized P-time, there's always a chance your RNG doesn't cooperate 19:45:39 https://blog.computationalcomplexity.org/2019/04/x-3-y-3-z-3-33-has-solution-in-z-and.html 19:45:45 this is unrelated but fun 19:52:02 https://math.stackexchange.com/questions/1396122/please-help-understand-how-ax2by-c-0-is-np-complete 19:52:12 subset sum encoded into 2 variable quadratic diophantine 19:53:49 the use of subset sum makes me think that the signs are significant 19:54:38 yeah 19:54:42 > the NP-complete SUBSET-SUM problem can be considered as a LINEAR DIOPHANTNE EQUATION, when you restrict your solution over positive integers. If you allow also negative solutions then it is solvable in polynomial time 19:54:44 :1:85: error: parse error on input ‘,’ 19:59:25 I think it's very likely that the problem you posted is NP-complete 19:59:37 maybe it's a superset of another problem already shown NP-complete 19:59:43 /only/ NP-complete? 19:59:54 oh... 19:59:58 I think it's likely to be NP-hard but am not convinced it's solvable in NP 20:00:48 it can express "sign-flipped quadratic residuosity", thus must by the discussion above be at least NP-hard 20:01:27 i see 20:04:30 I had no idea that such a simple diophantine equation was NP complete 20:04:41 i read about the hilbert 10 stuff and they need lots of variables 20:06:15 or, hmm, no, I'm not sure it /can/ express the sign flip 20:06:54 because now one side is increasing and the other decreasing, which prevents the simple implementation method I was hoping for working 20:25:14 -!- john_metcalf has joined. 20:42:33 -!- AnotherTest has quit (Ping timeout: 252 seconds). 20:46:18 -!- Frater_EST has joined. 20:46:31 -!- Frater_EST has quit (Remote host closed the connection). 20:47:27 -!- Hooloovo0 has quit (Ping timeout: 248 seconds). 20:51:48 -!- Hooloovo0 has joined. 20:53:38 -!- S_Gautam has quit (Quit: Connection closed for inactivity). 20:56:20 -!- budonyc has joined. 21:43:43 -!- b_jonas has quit (Quit: leaving). 22:02:28 -!- yaewa has quit (Quit: Leaving...). 22:04:47 -!- Hooloovo0 has quit (Ping timeout: 248 seconds). 22:05:27 -!- Hooloovo0 has joined. 22:09:20 -!- MDude has joined. 22:13:33 -!- Lord_of_Life_ has joined. 22:15:28 -!- Lord_of_Life has quit (Ping timeout: 245 seconds). 22:15:59 -!- Lord_of_Life_ has changed nick to Lord_of_Life. 22:20:17 -!- adu has joined. 22:53:26 -!- Phantom_Hoover has quit (Read error: Connection reset by peer). 22:55:32 @ask zzo38 Do you like GF2P8AFFINEQB? 22:55:32 Consider it noted. 22:56:23 is that an x86 instruction 22:57:08 AVX-512 22:58:12 I just came across this post. Is it written by zzo38? https://www.realworldtech.com/forum/?threadid=150494&curpostid=169010 23:01:00 it's a fused multiply and add, what's not to like ;-) 23:01:33 It's easy to like GF2P8AFFINEQB, but what about GF2P8AFFINEINVQB? 23:03:00 Hmm I guess what's not to like is that b is an immediate. 23:05:14 WTFISTHATQM 23:06:36 And for that other one, the hard-coded GF(2^8). 23:09:41 vbroadcastf128 [ds:esi+ecx*2+0x12345678] 23:10:41 -!- Hooloovo0 has quit (Remote host closed the connection). 23:12:28 -!- Hooloovo0 has joined. 23:12:42 median a b c = atMost (max a b) . atLeast (min a b) $ c 23:12:50 Do you like this? 23:25:14 -!- ais523 has quit (Quit: quit). 23:25:28 -!- MDude has quit (Ping timeout: 245 seconds). 23:30:30 AVX512 23:30:40 aka "let's make the decoder even more of a disaster" 23:32:19 i like the idea 23:32:25 but they extended the ISA a bit *too* much 23:33:35 I guess median of 5 is a sort of important function because you need it for the linear-time median algorithm. 23:33:50 But not actually important because that algorithm isn't actually useful? 23:34:06 Apparently you can do it with 6 comparisons. 23:35:00 i imagine that with the amount of transistors they put toward AVX512's sheer number of instructions, they probably could've, say, added more op-fusion possibilities instead 23:35:30 oplax monoidal fusion 23:36:21 Moony's wishlist: add each individual lane of SIMD registers to the scoreboard as it's own register 23:38:15 dont ask why 23:38:35 because my reasoning is on the "how the hell would that be viable" end of things 23:42:45 Also, the fact that a particular AVX2 only CPU (You know which one) completely plastered the i9-9920X lately, i think AVX512 may have been a bad move on intel's part 23:45:17 shachaf: wait what's the difference between atMost and min? 23:46:53 int-e: atMost = min 23:47:18 clamp lo hi = atLeast lo . atMost hi 23:48:03 synonyms are confusing 23:48:16 Are they? 23:48:21 I like the name atMost for min. 23:48:29 seems v. clear 23:48:52 they suggest that there's a difference 23:49:04 to me at least, in programming 23:49:18 atMost (atLeast a b) . atLeast (atMost a b) 23:49:26 That's confusing. 23:49:34 But so is min (max a b) . max (min a b) 23:49:45 nah, that one is just fine. 23:49:57 I think it's confusing that if you want to bound something below, you write max. 23:50:04 I always have to think about which way to do it. 23:50:10 ah but I'm used to that 23:50:12 Whereas with a name like atLeast it's obvious. 23:54:02 what's confusing is that (a \/ b) /\ ((a /\ b) \/ c) should be symmetric in a, b, c. 23:54:56 -!- TriMill has joined.