kendfrey

(;GM[1]FF[4]CA[UTF-8]AP[Sabaki:0.52.2]SZ[19]DT[2025-07-01]AB[bq][bo][fq][fp][fo][ir][iq][ip][jp][ko][lp][lq][mo][mn][nn][oo][op][pq][qr][ll][lk][kk][kj][jj][ij][hk][gm][lh][lg][mg][nh][pk][qb][eb][df][fh][jg][ke][kc][jb][ia][lb][ma]AW[cp][dq][kp][kq][jq][jr][js][ks][mp][mq][nq][ms][nr][or][os][sr][po][sm][om][ol][lo][jn][ho][an][dl][dj][gj][ii][ih][hh][ki][li][mh][pi][dg][ag][ac][ab][da][ea][fb][sc][sb][ra][qa][pb][ib][jc][lc][mb][pe][kg]GN[Snakebite]AN[Kendall Frey]GC[Can black kill the white group on the lower side?];B[lr]LB[lr:1])

kendfrey

Congratulations to Bill Lin 1p!

---

Rules, Players, & Schedule

https://nagofed.org/docs/2024-pro-qualification-rules.pdf

About the players

kendfrey

use indexmap::IndexMap;
use rand::{rngs::ThreadRng, seq::SliceRandom, thread_rng};

/// Represented as a number from 0 to 2
type Var = u8;

/// A choose function Var -> Var -> Var is represented by a 3x3 lookup table
type Func = [[Var; 3]; 3];

fn main()

kendfrey

import tactic

inductive the_rel {X Y : Type} (R : X → Y → Prop) : X ⊕ Y → X ⊕ Y → Prop
| fwd {x y} : R x y → the_rel (sum.inl x) (sum.inr y)

def mkl {X Y : Type} (R : X → Y → Prop) (x : X) : quot (the_rel R) := quot.mk _ (sum.inl x)
def mkr {X Y : Type} (R : X → Y → Prop) (y : Y) : quot (the_rel R) := quot.mk _ (sum.inr y)

example {X Y : Type} {R : X → Y → Prop} : 
  (∀ x₁ x₂ y₁ y₂, R x₁ y₁ → R x₂ y₁ → R x₂ y₂ → R x₁ y₂) ↔

kendfrey

import tactic

def transform : ℚ × ℚ × ℚ × ℚ × ℚ × ℚ × ℚ × ℚ × ℚ → ℚ × ℚ → ℚ × ℚ
| (a, b, c, d, e, f, g, h, i) (x, y) := ((a * x + b * y + c) / (g * x + h * y + i), (d * x + e * y + f) / (g * x + h * y + i))

def xy : ℚ × ℚ := (1, 1)
def xy' : ℚ × ℚ := (1, -1)
def x'y' : ℚ × ℚ := (-1, -1)
def x'y : ℚ × ℚ := (-1, 1)

kendfrey

import tactic

/-
I define ℤ⁺ to use for denominators, so that no proofs are required to construct rationals.
-/

/-- Strictly positive integers -/
inductive posint : Type
  | one : posint
  | succ : posint → posint

kendfrey

Require Setoid.

Declare Scope peano_scope.
Delimit Scope peano_scope with peano.
Open Scope peano_scope.

Axiom peano : Type -> Prop.

Axiom O : Type.
Axiom o_peano : peano O.

kendfrey

"use strict";

const words = require("./words.json");
const faces = [":grin:", ":smile:", ":grinning:", ":slight_smile:", ":neutral_face:", ":slight_frown:", ":worried:", ":persevere:", ":tired_face:", ":dizzy_face:", ":skull:"];

module.exports = class Hangman
{
	constructor()
	{
		this.guesses = new Set();

kendfrey

#NoEnv  ; Recommended for performance and compatibility with future AutoHotkey releases.
; #Warn  ; Enable warnings to assist with detecting common errors.
SendMode Input  ; Recommended for new scripts due to its superior speed and reliability.
SetWorkingDir %A_ScriptDir%  ; Ensures a consistent starting directory.
SetCapsLockState, AlwaysOff

#If GetKeyState("CapsLock","P")
{
	; Superscript & subscript
	1::Send {U+00B9} ; ¹ 1 superscript

kendfrey

using System;

namespace System
{
	internal static class LOGIC
	{
		internal static bool IMPLIES(bool p, bool q)
		{
			return !p || q;
		}