@[simp]

instance SK.reduced_K : Reduced Expr.K

@[simp]

instance SK.reduced_S : Reduced Expr.S

@[simp]

theorem SK.reduces_reduced_iff {a b : Expr} [ha : Reduced a] : Reduces a b ↔ a = b

theorem SK.reduced_iff {a : Expr} : Reduced a ↔ ∀ {b : Expr}, Reduces a b → a = b

theorem SK.reduces_comb1_iff {c a b : Expr} (hc : c = Expr.K ∨ c = Expr.S) : Reduces (c %% a) b ↔ ∃ (a' : Expr), Reduces a a' ∧ c %% a' = b

theorem SK.K1_reduces_iff {a b : Expr} : Reduces (Expr.K %% a) b ↔ ∃ (a' : Expr), Reduces a a' ∧ Expr.K %% a' = b

theorem SK.S1_reduces_iff {a b : Expr} : Reduces (Expr.S %% a) b ↔ ∃ (a' : Expr), Reduces a a' ∧ Expr.S %% a' = b

theorem SK.S2_reduces_iff {a b c : Expr} : Reduces (Expr.S %% a %% b) c ↔ ∃ (a' : Expr) (b' : Expr), Reduces a a' ∧ Reduces b b' ∧ Expr.S %% a' %% b' = c

@[simp]

instance SK.reduced_K1 {a : Expr} [ha : Reduced a] : Reduced (Expr.K %% a)

@[simp]

instance SK.reduced_S1 {a : Expr} [ha : Reduced a] : Reduced (Expr.S %% a)

@[simp]

instance SK.reduced_S2 {a b : Expr} [ha : Reduced a] [hb : Reduced b] : Reduced (Expr.S %% a %% b)

@[simp]

instance SK.reduced_I : Reduced I

@[simp]

theorem SK.not_exprEq_iff {a b : Expr} : ¬ExprEq a b ↔ ExprNe a b

@[simp]

theorem SK.not_exprNe_iff {a b : Expr} : ¬ExprNe a b ↔ ExprEq a b

@[simp]

theorem SK.I_reduces {a : Expr} : Reduces (I %% a) a

@[simp]

instance SK.reduced_KI : Reduced KI

@[simp]

theorem SK.KI_reduces {a : Expr} : Reduces (KI %% a) I

@[simp]

theorem SK.KI_reduces' {a b : Expr} : Reduces (KI %% a %% b) b

@[simp]

instance SK.reduced_KK : Reduced KK

@[simp]

theorem SK.KK_reduces {a : Expr} : Reduces (KK %% a) Expr.K

@[simp]

theorem SK.exprNe_KK_I : ExprNe KK I

@[simp]

theorem SK.exprNe_I_KI : ExprNe I KI

@[simp]

theorem SK.exprNe_KI_SKIK : ExprNe KI (Expr.S %% KI %% Expr.K)

@[simp]

theorem SK.exprNe_KKI_SKI : ExprNe (Expr.K %% KI) (Expr.S %% KI)

@[simp]

theorem SK.exprNe_K_KI : ExprNe Expr.K KI

@[simp]

theorem SK.exprNe_KI_K : ExprNe KI Expr.K

theorem SK.exprEq_of_ext {f g : Expr} (h : ∀ ⦃x : Expr⦄, ExprEq (f %% x) (g %% x)) : ExprEq f g

@[simp]

theorem SK.exprNe_S_K : ExprNe Expr.S Expr.K

theorem SK.ExprNe.symm {a b : Expr} (h : ExprNe a b) : ExprNe b a

theorem SK.ExprEq.symm {a b : Expr} (h : ExprEq a b) : ExprEq b a

theorem SK.ExprNe.comm {a b : Expr} : ExprNe a b ↔ ExprNe b a

theorem SK.ExprEq.comm {a b : Expr} : ExprEq a b ↔ ExprEq b a

theorem SK.exprEq_of_reduces' {a b a' b' : Expr} (h₁ : Reduces a a') (h₂ : Reduces b b') (h₃ : ExprEq a b) : ExprEq a' b'