diff --git a/Cslib/Foundations/Semantics/Realizes.lean b/Cslib/Foundations/Semantics/Realizes.lean
new file mode 100644
index 000000000..51335ccd5
--- /dev/null
+++ b/Cslib/Foundations/Semantics/Realizes.lean
@@ -0,0 +1,56 @@
+/-
+Copyright (c) 2025 Thomas Waring. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Thomas Waring
+-/
+
+module
+
+public import Cslib.Foundations.Data.Relation
+
+@[expose] public section
+
+namespace Cslib
+
+open Relation
+
+/-- A type `α` has "realisers" in some calculus `β`. -/
+class HasRealizer (α β : Type*) where
+  /-- A term represents (realizes) a element. -/
+  Realizes : β → α → Prop
+
+def Realizes {α β : Type*} [HasRealizer α β] : β → α → Prop := HasRealizer.Realizes
+
+scoped notation x " ⊩ " a => Realizes x a
+
+/-- Types for which the realisability relation is invariant by anti-reduction. -/
+class HasRealizerLift (α : Type*) {β : Type*} (r : β → β → Prop) extends HasRealizer α β where
+  /-- Realisers lift along reductions. -/
+  realizes_left_of_red : {a : α} → {x y : β} → (y ⊩ a) → r x y → x ⊩ a
+
+/-- Types for which the realisability relation is invariant by reduction. -/
+class HasRealizerDesc (α : Type*) {β : Type*} (r : β → β → Prop) extends HasRealizer α β where
+  /-- Realisers descend along reductions. -/
+  realizes_right_of_red : {a : α} → {x y : β} → (x ⊩ a) → r x y → y ⊩ a
+
+variable {α β : Type*} {r : β → β → Prop}
+
+lemma Realizes.left_of_red [HasRealizerLift α r] {a : α} {x y : β} (ha : y ⊩ a) (h : r x y) :
+    x ⊩ a := HasRealizerLift.realizes_left_of_red ha h
+
+lemma Realizes.left_of_mRed [HasRealizerLift α r] {a : α} {x y : β} (ha : y ⊩ a)
+    (h : (ReflTransGen r) x y) : x ⊩ a := by
+  induction h with
+  | refl => assumption
+  | tail h h' ih => exact ih <| ha.left_of_red h'
+
+lemma Realizes.right_of_red [HasRealizerDesc α r] {a : α} {x y : β} (ha : x ⊩ a) (h : r x y) :
+    y ⊩ a := HasRealizerDesc.realizes_right_of_red ha h
+
+lemma Realizes.right_of_mRed [HasRealizerDesc α r] {a : α} {x y : β} (ha : x ⊩ a)
+    (h : (ReflTransGen r) x y) : y ⊩ a := by
+  induction h with
+  | refl => assumption
+  | tail h h' ih => exact ih.right_of_red h'
+
+end Cslib
diff --git a/Cslib/Languages/CombinatoryLogic/Basic.lean b/Cslib/Languages/CombinatoryLogic/Basic.lean
index e8743062a..df32b8676 100644
--- a/Cslib/Languages/CombinatoryLogic/Basic.lean
+++ b/Cslib/Languages/CombinatoryLogic/Basic.lean
@@ -187,6 +187,13 @@ theorem C_def (f x y : SKI) : (C ⬝ f ⬝ x ⬝ y) ↠ f ⬝ y ⬝ x :=
 lemma C_head_mred (f x y z : SKI) (h : (f ⬝ y) ↠ z) : (C ⬝ f ⬝ x ⬝ y) ↠ z ⬝ x :=
   Trans.trans (C_def f x y) (MRed.head x h)
 
+/-- W := λ f x. f x x -/
+def WPoly : SKI.Polynomial 2 := &0 ⬝' &1 ⬝' &1
+/-- A SKI term representing W -/
+def W : SKI := WPoly.toSKI
+theorem W_def (f x : SKI) : (W ⬝ f ⬝ x) ↠ f ⬝ x ⬝ x :=
+  WPoly.toSKI_correct [f, x] (by simp)
+
 /-- Rotate right: RotR := λ x y z. z x y -/
 def RotRPoly : SKI.Polynomial 3 := &2 ⬝' &0 ⬝' &1
 /-- A SKI term representing RotR -/
@@ -250,134 +257,6 @@ def Th : SKI := ThAux ⬝ ThAux
 /-- A SKI term representing Θ -/
 theorem Th_correct (f : SKI) : (Th ⬝ f) ↠ f ⬝ (Th ⬝ f) := ThAux_def ThAux f
 
-/-! ### Church Booleans -/
-
-/-- A term a represents the boolean value u if it is βη-equivalent to a standard Church boolean. -/
-def IsBool (u : Bool) (a : SKI) : Prop :=
-  ∀ x y : SKI, (a ⬝ x ⬝ y) ↠ (if u then x else y)
-
-theorem isBool_trans (u : Bool) (a a' : SKI) (h : a ↠ a') (ha' : IsBool u a') :
-    IsBool u a := by
-  intro x y
-  trans a' ⬝ x ⬝ y
-  · apply MRed.head
-    apply MRed.head
-    exact h
-  · exact ha' x y
-
-/-- Standard true: TT := λ x y. x -/
-def TT : SKI := K
-@[scoped grind .]
-theorem TT_correct : IsBool true TT := fun x y ↦ MRed.K x y
-
-/-- Standard false: FF := λ x y. y -/
-def FF : SKI := K ⬝ I
-@[scoped grind .]
-theorem FF_correct : IsBool false FF :=
-  fun x y ↦ calc
-    (FF ⬝ x ⬝ y) ↠ I ⬝ y := by apply Relation.ReflTransGen.single; apply red_head; exact red_K I x
-    _         ⭢ y := red_I y
-
-/-- Conditional: Cond x y b := if b then x else y -/
-protected def Cond : SKI := RotR
-theorem cond_correct (a x y : SKI) (u : Bool) (h : IsBool u a) :
-    (SKI.Cond ⬝ x ⬝ y ⬝ a) ↠ if u then x else y := by
-  trans a ⬝ x ⬝ y
-  · exact rotR_def x y a
-  · exact h x y
-
-/-- Neg := λ a. Cond FF TT a -/
-protected def Neg : SKI := SKI.Cond ⬝ FF ⬝ TT
-theorem neg_correct (a : SKI) (ua : Bool) (h : IsBool ua a) : IsBool (¬ ua) (SKI.Neg ⬝ a) := by
-  apply isBool_trans (a' := if ua then FF else TT)
-  · apply cond_correct (h := h)
-  · cases ua
-    · simp [TT_correct]
-    · simp [FF_correct]
-
-/-- And := λ a b. Cond (Cond TT FF b) FF a -/
-def AndPoly : SKI.Polynomial 2 := SKI.Cond ⬝' (SKI.Cond ⬝ TT ⬝ FF ⬝' &1) ⬝' FF ⬝' &0
-/-- A SKI term representing And -/
-protected def And : SKI := AndPoly.toSKI
-theorem and_def (a b : SKI) : (SKI.And ⬝ a ⬝ b) ↠ SKI.Cond ⬝ (SKI.Cond ⬝ TT ⬝ FF ⬝ b) ⬝ FF ⬝ a :=
-  AndPoly.toSKI_correct [a, b] (by simp)
-
-theorem and_correct (a b : SKI) (ua ub : Bool) (ha : IsBool ua a) (hb : IsBool ub b) :
-    IsBool (ua && ub) (SKI.And ⬝ a ⬝ b) := by
-  apply isBool_trans (a' := SKI.Cond ⬝ (SKI.Cond ⬝ TT ⬝ FF ⬝ b) ⬝ FF ⬝ a) (h := and_def _ _)
-  cases ua
-  · simp_rw [Bool.false_and] at ⊢
-    apply isBool_trans (a' := FF) (ha' := FF_correct) (h := cond_correct a _ _ false ha)
-  · simp_rw [Bool.true_and] at ⊢
-    apply isBool_trans (a' := SKI.Cond ⬝ TT ⬝ FF ⬝ b) (h := cond_correct a _ _ true ha)
-    apply isBool_trans (a' := if ub = true then TT else FF) (h := cond_correct b _ _ ub hb)
-    cases ub
-    · simp [FF_correct]
-    · simp [TT_correct]
-
-/-- Or := λ a b. Cond TT (Cond TT FF b) b -/
-def OrPoly : SKI.Polynomial 2 := SKI.Cond ⬝' TT ⬝' (SKI.Cond ⬝ TT ⬝ FF ⬝' &1) ⬝' &0
-/-- A SKI term representing Or -/
-protected def Or : SKI := OrPoly.toSKI
-theorem or_def (a b : SKI) : (SKI.Or ⬝ a ⬝ b) ↠ SKI.Cond ⬝ TT ⬝ (SKI.Cond ⬝ TT ⬝ FF ⬝ b) ⬝ a :=
-  OrPoly.toSKI_correct [a, b] (by simp)
-
-theorem or_correct (a b : SKI) (ua ub : Bool) (ha : IsBool ua a) (hb : IsBool ub b) :
-  IsBool (ua || ub) (SKI.Or ⬝ a ⬝ b) := by
-  apply isBool_trans (a' := SKI.Cond ⬝ TT ⬝ (SKI.Cond ⬝ TT ⬝ FF ⬝ b) ⬝ a) (h := or_def _ _)
-  cases ua
-  · simp_rw [Bool.false_or]
-    apply isBool_trans (a' := SKI.Cond ⬝ TT ⬝ FF ⬝ b) (h := cond_correct a _ _ false ha)
-    apply isBool_trans (a' := if ub = true then TT else FF) (h := cond_correct b _ _ ub hb)
-    cases ub
-    · simp [FF_correct]
-    · simp [TT_correct]
-  · apply isBool_trans (a' := TT) (h := cond_correct a _ _ true ha)
-    simp [TT_correct]
-
-/- TODO?: other boolean connectives -/
-
-/-! ### Pairs -/
-
-/-- MkPair := λ a b. ⟨a,b⟩ -/
-def MkPair : SKI := SKI.Cond
-/-- First projection -/
-def Fst : SKI := R ⬝ TT
-/-- Second projection -/
-def Snd : SKI := R ⬝ FF
-
-@[scoped grind .]
-theorem fst_correct (a b : SKI) : (Fst ⬝ (MkPair ⬝ a ⬝ b)) ↠ a := by calc
-  _ ↠ SKI.Cond ⬝ a ⬝ b ⬝ TT := R_def _ _
-  _ ↠ a := cond_correct TT a b true TT_correct
-
-@[scoped grind .]
-theorem snd_correct (a b : SKI) : (Snd ⬝ (MkPair ⬝ a ⬝ b)) ↠ b := by calc
-  _ ↠ SKI.Cond ⬝ a ⬝ b ⬝ FF := R_def _ _
-  _ ↠ b := cond_correct FF a b false FF_correct
-
-/-- Unpaired f ⟨x, y⟩ := f x y, cf `Nat.unparied`. -/
-def UnpairedPoly : SKI.Polynomial 2 := &0 ⬝' (Fst ⬝' &1) ⬝' (Snd ⬝' &1)
-/-- A term representing Unpaired -/
-protected def Unpaired : SKI := UnpairedPoly.toSKI
-theorem unpaired_def (f p : SKI) : (SKI.Unpaired ⬝ f ⬝ p) ↠ f ⬝ (Fst ⬝ p) ⬝ (Snd ⬝ p) :=
-  UnpairedPoly.toSKI_correct [f, p] (by simp)
-
-theorem unpaired_correct (f x y : SKI) : (SKI.Unpaired ⬝ f ⬝ (MkPair ⬝ x ⬝ y)) ↠ f ⬝ x ⬝ y := by
-  trans f ⬝ (Fst ⬝ (MkPair ⬝ x ⬝ y)) ⬝ (Snd ⬝ (MkPair ⬝ x ⬝ y))
-  · exact unpaired_def f _
-  · apply parallel_mRed
-    · apply MRed.tail
-      exact fst_correct _ _
-    · exact snd_correct _ _
-
-/-- Pair f g x := ⟨f x, g x⟩, cf `Primrec.Pair`. -/
-def PairPoly : SKI.Polynomial 3 := MkPair ⬝' (&0 ⬝' &2) ⬝' (&1 ⬝' &2)
-/-- A SKI term representing Pair -/
-protected def Pair : SKI := PairPoly.toSKI
-theorem pair_def (f g x : SKI) : (SKI.Pair ⬝ f ⬝ g ⬝ x) ↠ MkPair ⬝ (f ⬝ x) ⬝ (g ⬝ x) :=
-  PairPoly.toSKI_correct [f, g, x] (by simp)
-
 end SKI
 
 end Cslib
diff --git a/Cslib/Languages/CombinatoryLogic/Evaluation.lean b/Cslib/Languages/CombinatoryLogic/Evaluation.lean
index 299c748d4..7647d1b80 100644
--- a/Cslib/Languages/CombinatoryLogic/Evaluation.lean
+++ b/Cslib/Languages/CombinatoryLogic/Evaluation.lean
@@ -209,7 +209,7 @@ lemma sk_nequiv : ¬ MJoin Red S K := by
   cases (redexFree_iff_mred_eq.1 hK _).1 hkz
 
 /-- Injectivity for booleans. -/
-theorem isBool_injective (x y : SKI) (u v : Bool) (hx : IsBool u x) (hy : IsBool v y)
+theorem realizes_bool_injective (x y : SKI) (u v : Bool) (hx : x ⊩ u) (hy : y ⊩ v)
     (hxy : MJoin Red x y) : u = v := by
   have h : MJoin Red (if u then S else K) (if v then S else K) := by
     apply mJoin_red_equivalence.trans (y := x ⬝ S ⬝ K)
@@ -223,7 +223,8 @@ theorem isBool_injective (x y : SKI) (u v : Bool) (hx : IsBool u x) (hy : IsBool
   grind [sk_nequiv, mJoin_red_equivalence.symm h]
 
 lemma TF_nequiv : ¬ MJoin Red TT FF := fun h =>
-  (Bool.eq_not_self true).mp <| isBool_injective TT FF true false TT_correct FF_correct h
+  (Bool.eq_not_self true).mp <|
+    realizes_bool_injective TT FF true false realizes_true realizes_false h
 
 /-- A specialisation of `Church : Nat → SKI`. -/
 def churchK : Nat → SKI
@@ -247,7 +248,7 @@ lemma churchK_injective : Function.Injective churchK :=
   fun n m h => by simpa using congrArg SKI.size h
 
 /-- Injectivity for Church numerals -/
-theorem isChurch_injective (x y : SKI) (n m : Nat) (hx : IsChurch n x) (hy : IsChurch m y)
+theorem realizes_nat_injective (x y : SKI) (n m : Nat) (hx : x ⊩ n) (hy : y ⊩ m)
     (hxy : MJoin Red x y) : n = m := by
   suffices MJoin Red (churchK n) (churchK m) by
     apply churchK_injective
@@ -283,7 +284,7 @@ theorem rice {P : SKI} (hP : ∀ x : SKI, ((P ⬝ x) ↠ TT) ∨ (P ⬝ x) ↠ F
       _ ↠ P ⬝ (Neg ⬝ Abs) := by apply MRed.tail; apply fixedPoint_correct
       _ ↠ P ⬝ (P ⬝ Abs ⬝ b ⬝ a) := by apply MRed.tail; apply Neg_app
       _ ↠ P ⬝ (TT ⬝ b ⬝ a) := by apply MRed.tail; apply MRed.head; apply MRed.head; exact h
-      _ ↠ P ⬝ b := by apply MRed.tail; apply TT_correct
+      _ ↠ P ⬝ b := by apply MRed.tail; apply realizes_true
       _ ↠ FF := hb
     exact TF_nequiv <| MRed.diamond h this
   case inr h =>
@@ -291,7 +292,7 @@ theorem rice {P : SKI} (hP : ∀ x : SKI, ((P ⬝ x) ↠ TT) ∨ (P ⬝ x) ↠ F
       _ ↠ P ⬝ (Neg ⬝ Abs) := by apply MRed.tail; apply fixedPoint_correct
       _ ↠ P ⬝ (P ⬝ Abs ⬝ b ⬝ a) := by apply MRed.tail; apply Neg_app
       _ ↠ P ⬝ (FF ⬝ b ⬝ a) := by apply MRed.tail; apply MRed.head; apply MRed.head; exact h
-      _ ↠ P ⬝ a := by apply MRed.tail; apply FF_correct
+      _ ↠ P ⬝ a := by apply MRed.tail; apply realizes_false
       _ ↠ TT := ha
     exact TF_nequiv <| MRed.diamond this h
 
diff --git a/Cslib/Languages/CombinatoryLogic/List.lean b/Cslib/Languages/CombinatoryLogic/List.lean
index c71721da9..c63c37dec 100644
--- a/Cslib/Languages/CombinatoryLogic/List.lean
+++ b/Cslib/Languages/CombinatoryLogic/List.lean
@@ -13,8 +13,8 @@ public import Cslib.Languages.CombinatoryLogic.Recursion
 /-!
 # Church-Encoded Lists in SKI Combinatory Logic
 
-Church-encoded lists for proving SKI ≃ TM equivalence. A list is encoded as
-`λ c n. c a₀ (c a₁ (... (c aₖ n)...))` where each `aᵢ` is a Church numeral.
+Church-encoded lists for proving SKI ≃ TM equivalence. A list `[a₀, ... aₖ]` is encoded as
+`λ c n. c xa₀ (c xa₁ (... (c xaₖ n)...))` where each `xaᵢ` represents `aᵢ`.
 -/
 
 namespace Cslib
@@ -23,41 +23,34 @@ namespace SKI
 
 open Red MRed
 
+variable {α β : Type*} [HasRealizer α SKI] [HasRealizer β SKI]
+
 /-! ### Church List Representation -/
 
-/-- A term correctly Church-encodes a list of natural numbers. -/
-def IsChurchList : List ℕ → SKI → Prop
-  | [], cns => ∀ c n : SKI, (cns ⬝ c ⬝ n) ↠ n
-  | x :: xs, cns => ∀ c n : SKI,
-      ∃ cx cxs : SKI, IsChurch x cx ∧ IsChurchList xs cxs ∧
+/-- A term correctly Church-encodes a list. -/
+def RealizesList (cns : SKI) : List α → Prop
+  | [] => ∀ c n : SKI, (cns ⬝ c ⬝ n) ↠ n
+  | a :: as => ∀ c n : SKI,
+      ∃ cx cxs : SKI, Realizes cx a ∧ RealizesList cxs as ∧
         (cns ⬝ c ⬝ n) ↠ c ⬝ cx ⬝ (cxs ⬝ c ⬝ n)
 
-/-- `IsChurchList` is preserved under multi-step reduction of the term. -/
-theorem isChurchList_trans {ns : List ℕ} {cns cns' : SKI} (h : cns ↠ cns')
-    (hcns' : IsChurchList ns cns') : IsChurchList ns cns := by
-  match ns with
-  | [] =>
-    intro c n
-    exact Trans.trans (parallel_mRed (MRed.head c h) .refl) (hcns' c n)
-  | x :: xs =>
-    intro c n
-    obtain ⟨cx, cxs, hcx, hcxs, hred⟩ := hcns' c n
-    exact ⟨cx, cxs, hcx, hcxs, Trans.trans (parallel_mRed (MRed.head c h) .refl) hred⟩
-
-/-- Both components of a pair are Church lists. -/
-structure IsChurchListPair (prev curr : List ℕ) (p : SKI) : Prop where
-  fst : IsChurchList prev (Fst ⬝ p)
-  snd : IsChurchList curr (Snd ⬝ p)
-
-/-- IsChurchListPair is preserved under reduction. -/
-@[scoped grind →]
-theorem isChurchListPair_trans {prev curr : List ℕ} {p p' : SKI} (hp : p ↠ p')
-    (hp' : IsChurchListPair prev curr p') : IsChurchListPair prev curr p := by
-  constructor
-  · apply isChurchList_trans (MRed.tail Fst hp)
-    exact hp'.1
-  · apply isChurchList_trans (MRed.tail Snd hp)
-    exact hp'.2
+instance instEncodedList : HasRealizer (List α) SKI where
+  Realizes := RealizesList
+
+instance instHasRealizerLiftList [HasRealizerLift α Red] : HasRealizerLift (List α) Red where
+  realizes_left_of_red := by
+    intro as cns cns' has h
+    induction as generalizing cns cns' with
+    | nil =>
+      intro c n
+      refine Relation.ReflTransGen.head ?_ (has c n)
+      exact red_head _ _ _ <| red_head _ _ _ h
+    | cons a as ih =>
+      intro c n
+      obtain ⟨cx', cxs', hcx, hcxs, hred⟩ := has c n
+      use cx', cxs', hcx, hcxs
+      refine Relation.ReflTransGen.head ?_ hred
+      exact red_head _ _ _ <| red_head _ _ _ h
 
 namespace List
 
@@ -74,7 +67,7 @@ theorem nil_def (c n : SKI) : (Nil ⬝ c ⬝ n) ↠ n :=
   NilPoly.toSKI_correct [c, n] (by simp)
 
 /-- The empty list term correctly represents `[]`. -/
-theorem nil_correct : IsChurchList [] Nil := nil_def
+theorem realizes_nil : Nil ⊩ ([] : List α) := nil_def
 
 /-! ### Cons: Consing an element onto a list -/
 
@@ -90,37 +83,88 @@ theorem cons_def (x xs c n : SKI) :
   ConsPoly.toSKI_correct [x, xs, c, n] (by simp)
 
 /-- Cons preserves Church list representation. -/
-theorem cons_correct {x : ℕ} {xs : List ℕ} {cx cxs : SKI}
-    (hcx : IsChurch x cx) (hcxs : IsChurchList xs cxs) :
-    IsChurchList (x :: xs) (Cons ⬝ cx ⬝ cxs) := by
-  intro c n
-  use cx, cxs, hcx, hcxs
+theorem realizes_cons : Cons ⊩ (List.cons : α → List α → List α) := by
+  intro c cx hx xs cxs hxs c n
+  use cx, cxs, hx, hxs
   exact cons_def cx cxs c n
 
 /-- Singleton list correctness. -/
-theorem singleton_correct {x : ℕ} {cx : SKI} (hcx : IsChurch x cx) :
-    IsChurchList [x] (Cons ⬝ cx ⬝ Nil) :=
-  cons_correct hcx nil_correct
-
-/-- The canonical SKI term for a Church-encoded list. -/
-def toChurch : List ℕ → SKI
-  | [] => Nil
-  | x :: xs => Cons ⬝ (SKI.toChurch x) ⬝ (toChurch xs)
-
-/-- `toChurch [] = Nil`. -/
-@[simp]
-lemma toChurch_nil : toChurch [] = Nil := rfl
-
-/-- `toChurch (x :: xs) = Cons ⬝ SKI.toChurch x ⬝ toChurch xs`. -/
-@[simp]
-lemma toChurch_cons (x : ℕ) (xs : List ℕ) :
-    toChurch (x :: xs) = Cons ⬝ (SKI.toChurch x) ⬝ (toChurch xs) := rfl
-
-/-- `toChurch ns` correctly represents `ns`. -/
-theorem toChurch_correct (ns : List ℕ) : IsChurchList ns (toChurch ns) := by
-  induction ns with
-  | nil => exact nil_correct
-  | cons x xs ih => exact cons_correct (SKI.toChurch_correct x) ih
+theorem realizes_singleton {x : α} {cx : SKI} (hcx : cx ⊩ x) :
+    (Cons ⬝ cx ⬝ Nil) ⊩ [x] :=
+  realizes_cons hcx realizes_nil
+
+/-! ### Basic recursion on lists -/
+
+def FoldR := RotR
+
+lemma realizes_list_foldr {α β : Type*} [HasRealizer α SKI] [HasRealizerLift β Red] :
+    FoldR ⊩ (List.foldr : (α → β → β) → β → List α → β) := by
+  intro f xf hf b xb hb l xl hl
+  suffices (xl ⬝ xf ⬝ xb) ⊩ (l.foldr f b) by apply this.left_of_mRed <| rotR_def ..
+  induction l generalizing xl with
+  | nil => exact hb.left_of_mRed <| hl ..
+  | cons a l ih =>
+    obtain ⟨xa, xl', ha, hl', hred⟩ := hl xf xb
+    have : Realizes (xf ⬝ xa ⬝ (xl' ⬝ xf ⬝ xb)) (f a (List.foldr f b l)) :=
+      hf ha (ih hl')
+    exact this.left_of_mRed hred
+
+def recPairStep (f : α → List α → β → β) : α → (β × List α) → (β × List α)
+  | a, ⟨y, as⟩ => ⟨f a as y, a :: as⟩
+
+lemma recPairStep_foldr {α' β' : Type*} (b : β') (f : α' → List α' → β' → β') (as : List α') :
+    List.foldr (β := β' × List α') (List.recPairStep f) ⟨b, []⟩ as = ⟨List.rec b f as, as⟩ := by
+  induction as <;> simp_all [recPairStep]
+
+def listRecAuxPoly : SKI.Polynomial 3 :=
+  SKI.MkPair ⬝' (&0 ⬝' &1 ⬝' (Snd ⬝' &2) ⬝' (Fst ⬝' &2)) ⬝' (Cons ⬝' &1 ⬝' (Snd ⬝' &2))
+def listRecAux : SKI := listRecAuxPoly.toSKI
+lemma listRecAux_def (xf xa xp : SKI) :
+    (listRecAux ⬝ xf ⬝ xa ⬝ xp) ↠
+      SKI.MkPair ⬝ (xf ⬝ xa ⬝ (Snd ⬝ xp) ⬝ (Fst ⬝ xp)) ⬝ (Cons ⬝ xa ⬝ (Snd ⬝ xp)) :=
+  listRecAuxPoly.toSKI_correct [xf, xa, xp] (by simp)
+
+lemma realizes_listRecAux {α β : Type*} [HasRealizerLift α Red] [HasRealizerLift β Red]
+    {f : α → List α → β → β} {xf : SKI} (hf : xf ⊩ f) :
+    (listRecAux ⬝ xf) ⊩ (List.recPairStep f) := by
+  intro a xa ha p xp hp
+  refine Realizes.left_of_mRed (α := β × List α) ?_ (listRecAux_def xf xa xp)
+  apply realizes_mkPair
+  · exact hf ha hp.2 hp.1
+  · exact realizes_cons ha hp.2
+
+lemma realizes_recPairStep_foldr {α β : Type*} [HasRealizerLift α Red] [HasRealizerLift β Red]
+    {b : β} {xb : SKI} (hb : xb ⊩ b)
+    {f : α → List α → β → β} {xf : SKI} (hf : xf ⊩ f) {as : List α} {xas : SKI} (has : xas ⊩ as) :
+    (SKI.RotR ⬝ (listRecAux ⬝ xf) ⬝ (MkPair ⬝ xb ⬝ Nil) ⬝ xas) ⊩
+      (⟨List.rec b f as, as⟩ : β × List α) := by
+  rw [←List.recPairStep_foldr]
+  refine realizes_list_foldr (realizes_listRecAux hf) ?_ has
+  exact realizes_mkPair hb realizes_nil
+
+def listRecPoly : SKI.Polynomial 3 :=
+  Fst ⬝' (SKI.RotR ⬝' (listRecAux ⬝' &1) ⬝' (MkPair ⬝' &0 ⬝' Nil) ⬝' &2)
+def listRec := listRecPoly.toSKI
+lemma listRec_def (xb xf xas : SKI) :
+    (listRec ⬝ xb ⬝ xf ⬝ xas) ↠ Fst ⬝ (SKI.RotR ⬝ (listRecAux ⬝ xf) ⬝ (MkPair ⬝ xb ⬝ Nil) ⬝ xas) :=
+  listRecPoly.toSKI_correct [xb, xf, xas] (by simp)
+
+theorem realizes_list_rec {α β : Type*} [HasRealizerLift α Red] [HasRealizerLift β Red] :
+    listRec ⊩ (List.rec : β → (α → List α → β → β) → List α → β) := by
+  intro b xb hb f xf hf as xas has
+  have := realizes_recPairStep_foldr hb hf has
+  exact this.1.left_of_mRed <| listRec_def ..
+
+def Tail := (listRec ⬝ Nil ⬝ (&1 : SKI.Polynomial 3).toSKI)
+
+lemma realizes_tail {α β : Type*} [HasRealizerLift α Red] [HasRealizerLift β Red] :
+    Tail ⊩ (List.tail : List α → List α) := by
+  intro as xas has
+  have : (as.tail = as.rec [] (fun _ t _ => t)) := by cases as <;> rfl
+  rw [this]
+  refine realizes_list_rec realizes_nil ?_ has
+  intro _ xs _ t xt ht _ xu _
+  apply ht.left_of_mRed <| (&1 : SKI.Polynomial 3).toSKI_correct [xs, xt, xu] (by simp)
 
 /-! ### Head: Extract the head of a list -/
 
@@ -135,20 +179,21 @@ theorem headD_def (d xs : SKI) : (HeadD ⬝ d ⬝ xs) ↠ xs ⬝ K ⬝ d :=
   HeadDPoly.toSKI_correct [d, xs] (by simp)
 
 /-- General head-with-default correctness. -/
-theorem headD_correct {d : ℕ} {cd : SKI} (hcd : IsChurch d cd)
-    {ns : List ℕ} {cns : SKI} (hcns : IsChurchList ns cns) :
-    IsChurch (ns.headD d) (HeadD ⬝ cd ⬝ cns) := by
-  match ns with
+theorem realizes_headD {α : Type*} [HasRealizerLift α Red] :
+    HeadD ⊩ (fun a (as : List α) => as.headD a) := by
+  intro a xa ha as xas has
+  match as with
   | [] =>
     simp only [List.headD_nil]
-    apply isChurch_trans d (headD_def cd cns)
-    apply isChurch_trans d (hcns K cd)
-    exact hcd
+    refine Realizes.left_of_mRed ?_ (headD_def xa xas)
+    apply ha.left_of_mRed
+    exact has K xa
   | x :: xs =>
     simp only [List.headD_cons]
-    apply isChurch_trans x (headD_def cd cns)
-    obtain ⟨cx, cxs, hcx, _, hred⟩ := hcns K cd
-    exact isChurch_trans x hred (isChurch_trans x (MRed.K cx _) hcx)
+    refine Realizes.left_of_mRed ?_ (headD_def xa xas)
+    obtain ⟨cx, cxs, hcx, _, hred⟩ := has K xa
+    apply hcx.left_of_mRed
+    exact hred.trans <| MRed.K ..
 
 /-- The SKI term for list head (default 0). -/
 def Head : SKI := HeadD ⬝ SKI.Zero
@@ -158,88 +203,9 @@ theorem head_def (xs : SKI) : (Head ⬝ xs) ↠ xs ⬝ K ⬝ SKI.Zero :=
   headD_def SKI.Zero xs
 
 /-- Head correctness (default 0). -/
-theorem head_correct (ns : List ℕ) (cns : SKI) (hcns : IsChurchList ns cns) :
-    IsChurch (ns.headD 0) (Head ⬝ cns) :=
-  headD_correct zero_correct hcns
-
-/-! ### Tail: Extract the tail of a list -/
-
-/-- Step function for tail: (prev, curr) → (curr, cons h curr) -/
-def TailStepPoly : SKI.Polynomial 2 :=
-  MkPair ⬝' (Snd ⬝' &1) ⬝' (Cons ⬝' &0 ⬝' (Snd ⬝' &1))
-
-/-- The step function for computing list tail. -/
-def TailStep : SKI := TailStepPoly.toSKI
-
-/-- Reduction of the tail step function. -/
-theorem tailStep_def (h p : SKI) :
-    (TailStep ⬝ h ⬝ p) ↠ MkPair ⬝ (Snd ⬝ p) ⬝ (Cons ⬝ h ⬝ (Snd ⬝ p)) :=
-  TailStepPoly.toSKI_correct [h, p] (by simp)
-
-/-- tail xs = Fst (xs TailStep (MkPair Nil Nil)) -/
-def TailPoly : SKI.Polynomial 1 :=
-  Fst ⬝' (&0 ⬝' TailStep ⬝' (MkPair ⬝ Nil ⬝ Nil))
-
-/-- The tail of a Church-encoded list. -/
-def Tail : SKI := TailPoly.toSKI
-
-/-- Reduction: `Tail ⬝ xs ↠ Fst ⬝ (xs ⬝ TailStep ⬝ (MkPair ⬝ Nil ⬝ Nil))`. -/
-theorem tail_def (xs : SKI) :
-    (Tail ⬝ xs) ↠ Fst ⬝ (xs ⬝ TailStep ⬝ (MkPair ⬝ Nil ⬝ Nil)) :=
-  TailPoly.toSKI_correct [xs] (by simp)
-
-/-- The initial pair (nil, nil) satisfies the invariant. -/
-@[simp]
-theorem tail_init : IsChurchListPair [] [] (MkPair ⬝ Nil ⬝ Nil) := by
-  constructor
-  · apply isChurchList_trans (fst_correct _ _); exact nil_correct
-  · apply isChurchList_trans (snd_correct _ _); exact nil_correct
-
-/-- The step function preserves the tail-computing invariant. -/
-theorem tailStep_correct {x : ℕ} {xs : List ℕ} {cx p : SKI}
-    (hcx : IsChurch x cx) (hp : IsChurchListPair xs.tail xs p) :
-    IsChurchListPair xs (x :: xs) (TailStep ⬝ cx ⬝ p) := by
-  apply isChurchListPair_trans (tailStep_def cx p)
-  exact ⟨isChurchList_trans (fst_correct _ _) hp.2,
-         isChurchList_trans (snd_correct _ _) (cons_correct hcx hp.2)⟩
-
-theorem tailFold_correct (ns : List ℕ) (cns : SKI) (hcns : IsChurchList ns cns) :
-    ∃ p, (cns ⬝ TailStep ⬝ (MkPair ⬝ Nil ⬝ Nil)) ↠ p ∧
-         IsChurchListPair ns.tail ns p := by
-  induction ns generalizing cns with
-  | nil =>
-    -- For empty list, the fold returns the initial pair
-    use MkPair ⬝ Nil ⬝ Nil
-    constructor
-    · exact hcns TailStep (MkPair ⬝ Nil ⬝ Nil)
-    · exact tail_init
-  | cons x xs ih =>
-    -- For x :: xs, first fold xs, then apply step
-    -- cns ⬝ TailStep ⬝ init ↠ TailStep ⬝ cx ⬝ (cxs ⬝ TailStep ⬝ init)
-    -- Get the Church representations for x and xs
-    obtain ⟨cx, cxs, hcx, hcxs, hred⟩ := hcns TailStep (MkPair ⬝ Nil ⬝ Nil)
-    -- By IH, folding xs gives a pair representing (xs.tail, xs)
-    obtain ⟨p_xs, hp_xs_red, hp_xs_pair⟩ := ih cxs hcxs
-    -- After step, we get a pair representing (xs, x :: xs)
-    have hstep := tailStep_correct hcx hp_xs_pair
-    -- The full fold: cns ⬝ TailStep ⬝ init ↠ TailStep ⬝ cx ⬝ (cxs ⬝ TailStep ⬝ init)
-    --                                         ↠ TailStep ⬝ cx ⬝ p_xs
-    use TailStep ⬝ cx ⬝ p_xs
-    constructor
-    · exact Trans.trans hred (MRed.tail _ hp_xs_red)
-    · exact hstep
-
-/-- Tail correctness. -/
-theorem tail_correct (ns : List ℕ) (cns : SKI) (hcns : IsChurchList ns cns) :
-    IsChurchList ns.tail (Tail ⬝ cns) := by
-  -- Tail ⬝ cns ↠ Fst ⬝ (cns ⬝ TailStep ⬝ (MkPair ⬝ Nil ⬝ Nil))
-  apply isChurchList_trans (tail_def cns)
-  -- Get the fold result
-  obtain ⟨p, hp_red, hp_pair⟩ := tailFold_correct ns cns hcns
-  -- Fst ⬝ (cns ⬝ TailStep ⬝ init) ↠ Fst ⬝ p
-  apply isChurchList_trans (MRed.tail Fst hp_red)
-  -- Fst ⬝ p represents ns.tail (from hp_pair)
-  exact hp_pair.1
+theorem realizes_head : Head ⊩ (fun (xs : List Nat) => xs.headD 0) := by
+  intro ns xns hns
+  exact realizes_headD realizes_zero hns
 
 /-! ### Prepending zero to a list (for Code.zero') -/
 
@@ -254,10 +220,10 @@ theorem prependZero_def (xs : SKI) : (PrependZero ⬝ xs) ↠ Cons ⬝ SKI.Zero
   PrependZeroPoly.toSKI_correct [xs] (by simp)
 
 /-- Prepending zero preserves Church list representation. -/
-theorem prependZero_correct {ns : List ℕ} {cns : SKI} (hcns : IsChurchList ns cns) :
-    IsChurchList (0 :: ns) (PrependZero ⬝ cns) := by
-  apply isChurchList_trans (prependZero_def cns)
-  exact cons_correct zero_correct hcns
+theorem realizes_prependZero : PrependZero ⊩ (fun ns => 0 :: ns) := by
+  intro ns cns hns
+  refine Realizes.left_of_mRed ?_ (prependZero_def cns)
+  exact realizes_cons realizes_zero hns
 
 /-! ### Successor on list head (for Code.succ) -/
 
@@ -265,12 +231,13 @@ theorem prependZero_correct {ns : List ℕ} {cns : SKI} (hcns : IsChurchList ns
 def SuccHead : SKI := B ⬝ (C ⬝ Cons ⬝ Nil) ⬝ (B ⬝ SKI.Succ ⬝ Head)
 
 /-- `SuccHead` correctly computes a singleton containing `succ(head ns)`. -/
-theorem succHead_correct (ns : List ℕ) (cns : SKI) (hcns : IsChurchList ns cns) :
-    IsChurchList [ns.headD 0 + 1] (SuccHead ⬝ cns) := by
-  have hhead := head_correct ns cns hcns
-  have hsucc := succ_correct (ns.headD 0) (Head ⬝ cns) hhead
-  apply isChurchList_trans (.trans (B_tail_mred _ _ _ _ (B_def .Succ Head cns)) (C_def Cons Nil _))
-  exact cons_correct hsucc nil_correct
+theorem realizes_prependSucc : SuccHead ⊩ (fun (ns : List Nat) => [ns.headD 0 + 1]) := by
+  intro ns cns hcns
+  have hhead := realizes_head hcns
+  have hsucc := realizes_succ hhead
+  refine Realizes.left_of_mRed ?_
+    (.trans (B_tail_mred _ _ _ _ (B_def .Succ Head cns)) (C_def Cons Nil _))
+  exact realizes_cons hsucc realizes_nil
 
 end List
 
diff --git a/Cslib/Languages/CombinatoryLogic/Realizes.lean b/Cslib/Languages/CombinatoryLogic/Realizes.lean
new file mode 100644
index 000000000..163cb2459
--- /dev/null
+++ b/Cslib/Languages/CombinatoryLogic/Realizes.lean
@@ -0,0 +1,325 @@
+/-
+Copyright (c) 2025 Thomas Waring. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Thomas Waring
+-/
+
+module
+
+public import Cslib.Languages.CombinatoryLogic.Basic
+public import Cslib.Foundations.Semantics.Realizes
+public import Mathlib.Data.PFun
+
+@[expose] public section
+
+namespace Cslib.SKI
+
+open Red MRed Relation HasRealizer Realizes
+
+/-! ### Function types
+
+Realizers for a function type `α → β` are defined by a logical relation: `xf ⊩ f` if for every
+`xa ⊩ a`, `xf ⬝ xa ⊩ f a`. We provide realizer interpretations for the primitive combinators
+`S`,`K` and `I` as well as those from the `BCKW` basis.
+-/
+
+/-- A term `xf` encodes a function `f : α → β` if for every `xa ⊩ a : α`, `xf ⬝ a ⊩ f a`. -/
+instance instHasRealizerPi (α β : Type*) [hα : HasRealizer α SKI] [hβ : HasRealizer β SKI] :
+    HasRealizer (α → β) SKI where
+  Realizes z f := ∀ {a : α} {x : SKI}, (x ⊩ a) → (z ⬝ x) ⊩ (f a)
+
+instance instHasRealizerLiftPi (α β : Type*) [hα : HasRealizer α SKI] [hβ : HasRealizerLift β Red] :
+    HasRealizerLift (α → β) Red where
+  realizes_left_of_red := by
+    intro f x y hy h a z hz
+    apply HasRealizerLift.realizes_left_of_red (hy hz)
+    exact red_head _ _ _ h
+
+instance instHasRealizerDescPi (α β : Type*) [hα : HasRealizer α SKI] [hβ : HasRealizerDesc β Red] :
+    HasRealizerDesc (α → β) Red where
+  realizes_right_of_red := by
+    intro f x y hy h a z hz
+    apply HasRealizerDesc.realizes_right_of_red (hy hz)
+    exact red_head _ _ _ h
+
+lemma realizes_id {α : Type*} [HasRealizerLift α Red] : I ⊩ (id : α → α) :=
+  fun ha => ha.left_of_red <| red_I _
+
+lemma realizes_const {α β : Type*} [HasRealizerLift α Red] [HasRealizer β SKI] :
+    K ⊩ (Function.const β : α → β → α) := fun ha _ _ _ => ha.left_of_red <| red_K ..
+
+lemma realizes_S {α β γ : Type*} [HasRealizer α SKI] [HasRealizer β SKI]
+    [HasRealizerLift γ Red] : S ⊩ (fun (f : α → β → γ) (g : α → β) (a : α) => f a (g a)) :=
+  fun hf _ _ hg _ _ ha => (hf ha (hg ha)).left_of_red <| red_S ..
+
+lemma realizes_comp {α β γ : Type*} [HasRealizer α SKI] [HasRealizer β SKI]
+    [HasRealizerLift γ Red] : B ⊩ (Function.comp : (β → γ) → (α → β) → α → γ) :=
+  fun hf _ _ hg _ _ ha => (hf <| hg ha).left_of_mRed <| B_def ..
+
+lemma realizes_swap {α β γ : Type*} [HasRealizer α SKI] [HasRealizer β SKI]
+    [HasRealizerLift γ Red] : C ⊩ (Function.swap : (α → β → γ) → β → α → γ) :=
+  fun hf _ _ hb _ _ ha => (hf ha hb).left_of_mRed <| C_def ..
+
+lemma realizes_diagonal_app {α β : Type*} [HasRealizer α SKI] [HasRealizerLift β Red] :
+    W ⊩ (fun (f : α → α → β) (a : α) => f a a) :=
+  fun hf _ _ ha => (hf ha ha).left_of_mRed <| W_def ..
+
+/-!
+### Booleans
+
+`xu ⊩ u` if `xu` is βη-equivalent to the standard Church boolean.
+-/
+
+instance instHasRealizerLiftBool : HasRealizerLift Bool Red where
+  Realizes z u := ∀ x y : SKI, (z ⬝ x ⬝ y) ↠ (if u then x else y)
+  realizes_left_of_red := by
+    intro u x y hu h a b
+    trans y ⬝ a ⬝ b
+    · apply MRed.head; apply MRed.head; exact ReflTransGen.single h
+    · exact hu a b
+
+
+/-- Standard true: TT := λ x y. x -/
+def TT : SKI := K
+
+@[scoped grind .]
+theorem realizes_true : TT ⊩ true := fun x y ↦ MRed.K x y
+
+/-- Standard false: FF := λ x y. y -/
+def FF : SKI := K ⬝ I
+
+@[scoped grind .]
+theorem realizes_false : FF ⊩ false :=
+  fun x y ↦ calc
+    (FF ⬝ x ⬝ y) ↠ I ⬝ y := by apply ReflTransGen.single; apply red_head; exact red_K I x
+    _ ⭢ y := red_I y
+
+/-- Conditional: Cond x y b := if b then x else y -/
+protected def Cond : SKI := RotR
+
+lemma cond_def {xu y z} {u : Bool} (hu : xu ⊩ u) :
+    (SKI.Cond ⬝ y ⬝ z ⬝ xu) ↠ if u then y else z := by
+  cases u
+  all_goals {
+    trans xu ⬝ y ⬝ z
+    · exact rotR_def ..
+    · exact hu ..
+    }
+
+lemma realizes_cond {α : Type*} [HasRealizerLift α Red] :
+    SKI.Cond ⊩ (fun (a b : α) (u : Bool) => if u then a else b) := by
+  intro a xa ha b xb hb u xu hu
+  cases u
+  case false =>
+    exact hb.left_of_mRed <| cond_def hu
+  case true =>
+    exact ha.left_of_mRed <| cond_def hu
+
+/-!
+### Pairs
+
+`xp ⊩ ⟨a, b⟩` if `Fst ⬝ xp ⊩ a` and `Snd ⬝ xp ⊩ b`, where `Fst` and `Snd` are the canonical
+projections. We note that this breaks the "Church encoding" pattern, which would define encodings
+of a product by its recursor, ie `xp ⊩ ⟨a, b⟩` if for every `f`, `xp ⬝ f ↠ f ⬝ xa ⬝ xb` for some
+`xa ⊩ a` and `xb ⊩ b`.
+-/
+
+/-- MkPair := λ a b. ⟨a,b⟩ -/
+def MkPair : SKI := SKI.Cond
+/-- First projection -/
+def Fst : SKI := R ⬝ TT
+/-- Second projection -/
+def Snd : SKI := R ⬝ FF
+
+@[scoped grind .]
+theorem fst_correct (a b : SKI) : (Fst ⬝ (MkPair ⬝ a ⬝ b)) ↠ a := calc
+  _ ↠ SKI.Cond ⬝ a ⬝ b ⬝ TT := R_def _ _
+  _ ↠ TT ⬝ a ⬝ b := rotR_def ..
+  _ ⭢ a := red_K ..
+
+@[scoped grind .]
+theorem snd_correct (a b : SKI) : (Snd ⬝ (MkPair ⬝ a ⬝ b)) ↠ b := by calc
+  _ ↠ SKI.Cond ⬝ a ⬝ b ⬝ FF := R_def _ _
+  _ ↠ FF ⬝ a ⬝ b := rotR_def ..
+  _ ⭢ I ⬝ b := red_head _ _ b <| red_K ..
+  _ ⭢ b := red_I b
+
+instance instHasRealizerProd {α β : Type*} [HasRealizer α SKI] [HasRealizer β SKI] :
+    HasRealizer (α × β) SKI where
+  Realizes x p := ((Fst ⬝ x) ⊩ p.1)  ∧ (Snd ⬝ x) ⊩ p.2
+
+instance instHasRealizerLiftProd {α β : Type*} [HasRealizerLift α Red] [HasRealizerLift β Red] :
+    HasRealizerLift (α × β) Red where
+  realizes_left_of_red := by
+    intro p x y ⟨hp₁, hp₂⟩ h
+    constructor
+    · apply hp₁.left_of_mRed
+      exact ReflTransGen.single <| red_tail Fst _ _ h
+    · apply hp₂.left_of_mRed
+      exact ReflTransGen.single <| red_tail Snd _ _ h
+
+instance instHasRealizerDescProd {α β : Type*} [HasRealizerDesc α Red] [HasRealizerDesc β Red] :
+    HasRealizerDesc (α × β) Red where
+  realizes_right_of_red := by
+    intro p x y ⟨hp₁, hp₂⟩ h
+    constructor
+    · apply hp₁.right_of_mRed
+      exact ReflTransGen.single <| red_tail Fst _ _ h
+    · apply hp₂.right_of_mRed
+      exact ReflTransGen.single <| red_tail Snd _ _ h
+
+/-- The pairing term `SKI.MkPair` indeed encodes `Prod.Mk`. -/
+lemma realizes_mkPair {α β : Type*} [HasRealizerLift α Red] [HasRealizerLift β Red] :
+    SKI.MkPair ⊩ (Prod.mk : α → β → α × β) := by
+  intro a xa ha b xb hb
+  constructor
+  · exact ha.left_of_mRed <| fst_correct ..
+  · exact hb.left_of_mRed <| snd_correct ..
+
+lemma realizes_fst {α β : Type*} [HasRealizer α SKI] [HasRealizer β SKI] :
+    SKI.Fst ⊩ (Prod.fst : α × β → α) := by
+  intro _ _ h
+  exact h.1
+
+lemma realizes_snd {α β : Type*} [HasRealizer α SKI] [HasRealizer β SKI] :
+    SKI.Snd ⊩ (Prod.snd : α × β → β) := by
+  intro _ _ h
+  exact h.2
+
+def prodRecPoly : SKI.Polynomial 2 := &0 ⬝' (Fst ⬝' &1) ⬝' (Snd ⬝' &1)
+/-- The term which will encode `Prod.rec`. -/
+def prodRec := prodRecPoly.toSKI
+lemma prodRec_def (xf xp : SKI) : (prodRec ⬝ xf ⬝ xp) ↠ xf ⬝ (Fst ⬝ xp) ⬝ (Snd ⬝ xp) :=
+  prodRecPoly.toSKI_correct [xf, xp] (by simp)
+
+theorem realizes_prod_rec {α β γ : Type*} [HasRealizer α SKI] [HasRealizer β SKI]
+    [HasRealizerLift γ Red] : prodRec ⊩ (Prod.rec : (α → β → γ) → α × β → γ) := by
+  intro f xf hf p xp hp
+  exact (hf hp.1 hp.2).left_of_mRed <| prodRec_def ..
+
+/-!
+### Sums
+
+`xab ⊩ s : α ⊕ β` if for every `f, g`, `xab ⬝ f ⬝ g` reduces to `f ⬝ xa`, for `s = .inl a` and
+`xa ⊩ a`, or `g ⬝ xb`, for `s = .inr b` and `xb ⊩  b`.
+-/
+
+def realizesSum {α β : Type*} [HasRealizer α SKI] [HasRealizer β SKI] (x : SKI) : α ⊕ β → Prop
+  | .inl a => ∀ f g : SKI, ∃ xa : SKI, (xa ⊩ a) ∧ (x ⬝ f ⬝ g) ↠ f ⬝ xa
+  | .inr b => ∀ f g : SKI, ∃ xb : SKI, (xb ⊩ b) ∧ (x ⬝ f ⬝ g) ↠ g ⬝ xb
+
+instance instHasRealizerSum {α β : Type*} [HasRealizer α SKI] [HasRealizer β SKI] :
+    HasRealizer (α ⊕ β) SKI where
+  Realizes := realizesSum
+
+instance instHasRealizerLiftSum {α β : Type*} [HasRealizerLift α Red] [HasRealizerLift β Red] :
+    HasRealizerLift (α ⊕ β) Red where
+  realizes_left_of_red := by
+    intro ab x y hy h
+    cases ab
+    case inl a =>
+      intro f g
+      obtain ⟨xa, ha, hred⟩ := hy f g
+      use xa, ha
+      exact ReflTransGen.head (red_head _ _ g <| red_head _ _ f h) hred
+    case inr b =>
+      intro f g
+      obtain ⟨xb, hb, hred⟩ := hy f g
+      use xb, hb
+      exact ReflTransGen.head (red_head _ _ g <| red_head _ _ f h) hred
+
+def inlPoly : SKI.Polynomial 3 := &1 ⬝' &0
+protected def Inl : SKI := inlPoly.toSKI
+lemma inl_def (a f g : SKI) : (SKI.Inl ⬝ a ⬝ f ⬝ g) ↠ f ⬝ a :=
+  inlPoly.toSKI_correct [a, f, g] (by simp)
+
+lemma realizes_sum_inl {α β : Type*} [HasRealizer α SKI] [HasRealizer β SKI] :
+    SKI.Inl ⊩ (Sum.inl : α → α ⊕ β) := by
+  intro a xa ha f g
+  use xa, ha, inl_def ..
+
+def inrPoly : SKI.Polynomial 3 := &2 ⬝' &0
+protected def Inr : SKI := inrPoly.toSKI
+lemma inr_def (a f g : SKI) : (SKI.Inr ⬝ a ⬝ f ⬝ g) ↠ g ⬝ a :=
+  inrPoly.toSKI_correct [a, f, g] (by simp)
+
+lemma realizes_sum_inr {α β : Type*} [HasRealizer α SKI] [HasRealizer β SKI] :
+    SKI.Inr ⊩ (Sum.inr : β → α ⊕ β) := by
+  intro b xb hb f g
+  use xb, hb, inr_def ..
+
+def sumRec : SKI := RotR
+
+theorem realizes_sum_rec {α β γ : Type*} [HasRealizer α SKI] [HasRealizer β SKI]
+    [HasRealizerLift γ Red] : sumRec ⊩ (Sum.rec : (α → γ) → (β → γ) → α ⊕ β → γ) := by
+  intro f xf hf g xg hg ab xab hab
+  cases ab with
+  | inl a =>
+    obtain ⟨xa, ha, hred⟩ := hab xf xg
+    exact (hf ha).left_of_mRed <| (rotR_def ..).trans hred
+  | inr b =>
+    obtain ⟨xb, hb, hred⟩ := hab xf xg
+    exact (hg hb).left_of_mRed <| (rotR_def ..).trans hred
+
+/-!
+### Partial values
+
+A term `x` encodes a partial value `o` if `o = Part.none`, or `o = Part.some a` and `x ⊩ a`. We
+specialize the definition of realizers for function types to partial functions `a →. β`.
+-/
+
+instance instHasRealizerPart {α : Type*} [HasRealizer α SKI] : HasRealizer (Part α) SKI where
+  Realizes x o := (h : o.Dom) → x ⊩ (o.get h)
+
+lemma realizes_of_mem {α : Type*} [HasRealizer α SKI] {o : Part α} {x : SKI} (h : x ⊩ o)
+    {a : α} (ha : a ∈ o) : x ⊩ a := by
+  obtain ⟨hao, ha⟩ := ha
+  exact ha ▸ h hao
+
+lemma realizes_some_iff {α : Type*} [HasRealizer α SKI] {a : α} {x : SKI} :
+    (x ⊩ Part.some a) ↔ x ⊩ a := by
+  refine ⟨?_, ?_⟩
+  · intro h; exact h (Part.some_dom a)
+  · intro h; exact fun _ => h
+
+lemma realizes_none {α : Type*} [HasRealizer α SKI] (x : SKI) : x ⊩ (Part.none : Part α) :=
+  fun h => False.elim (Part.not_none_dom h)
+
+lemma realizes_some {α : Type*} [HasRealizerLift α Red] : I ⊩ (Part.some : α → Part α) := by
+  intro a xa ha
+  rw [realizes_some_iff]
+  exact ha.left_of_red (red_I xa)
+
+instance instHasRealizerLiftPart {α : Type*} [HasRealizerLift α Red] :
+    HasRealizerLift (Part α) Red where
+  realizes_left_of_red := by
+    intro o x y ho h hdom
+    exact (ho hdom).left_of_red h
+
+instance instHasRealizerDescPart {α : Type*} [HasRealizerDesc α Red] :
+    HasRealizerDesc (Part α) Red where
+  realizes_right_of_red := by
+    intro o x y ho h hdom
+    exact (ho hdom).right_of_red h
+
+instance instHasRealizerPFun (α β : Type*) [HasRealizer α SKI] [HasRealizer β SKI] :
+  HasRealizer (α →. β) SKI := inferInstanceAs <| HasRealizer (α → Part β) SKI
+
+instance instHasRealizerLiftPFun (α β : Type*) [hα : HasRealizer α SKI]
+    [hβ : HasRealizerLift β Red] : HasRealizerLift (α →. β) Red :=
+    inferInstanceAs <| HasRealizerLift (α → Part β) Red
+
+instance instHasRealizerDescPFun (α β : Type*) [hα : HasRealizer α SKI]
+    [hβ : HasRealizerDesc β Red] : HasRealizerDesc (α →. β) Red :=
+    inferInstanceAs <| HasRealizerDesc (α → Part β) Red
+
+lemma realizes_pfun_iff {α β : Type*} [HasRealizer α SKI] [HasRealizer β SKI] (xf : SKI)
+    (f : α →. β) :
+    (xf ⊩ f) ↔ ∀ {a : α} (ha : a ∈ f.Dom) {xa : SKI}, (xa ⊩ a) → (xf ⬝ xa) ⊩ f.fn a ha := by
+  constructor
+  · intro h a ha xa hxa
+    exact h hxa ha
+  · intro h a xa ha hdom
+    exact h hdom ha
+
+end Cslib.SKI
diff --git a/Cslib/Languages/CombinatoryLogic/Recursion.lean b/Cslib/Languages/CombinatoryLogic/Recursion.lean
index b9128f09f..3d39a3f73 100644
--- a/Cslib/Languages/CombinatoryLogic/Recursion.lean
+++ b/Cslib/Languages/CombinatoryLogic/Recursion.lean
@@ -6,7 +6,7 @@ Authors: Thomas Waring
 
 module
 
-public import Cslib.Languages.CombinatoryLogic.Basic
+public import Cslib.Languages.CombinatoryLogic.Realizes
 
 @[expose] public section
 
@@ -73,27 +73,24 @@ lemma church_red (n : Nat) (f f' x x' : SKI) (hf : f ↠ f') (hx : x ↠ x') :
   | zero => exact hx
   | succ n ih => exact parallel_mRed hf ih
 
-/-- The term `a` is βη-equivalent to a standard church numeral. -/
-def IsChurch (n : Nat) (a : SKI) : Prop :=
-    ∀ f x :SKI, (a ⬝ f ⬝ x) ↠ (Church n f x)
-
-/-- To show `IsChurch n a` it suffices to show the same for a reduct of `a`. -/
-theorem isChurch_trans (n : Nat) {a a' : SKI} (h : a ↠ a') :
-    IsChurch n a' → IsChurch n a := by
-  simp_rw [IsChurch]
-  intro ha' f x
-  calc
-  _ ↠ a' ⬝ f ⬝ x := by apply MRed.head; apply MRed.head; exact h
-  _ ↠ Church n f x := by apply ha'
+instance instHasRealizerLiftNat : HasRealizerLift Nat Red where
+  Realizes a n := ∀ f x : SKI, (a ⬝ f ⬝ x) ↠ (Church n f x)
+  realizes_left_of_red := by
+    intro n a a' ha' h f x
+    calc
+    (a ⬝ f ⬝ x) ⭢ a' ⬝ f ⬝ x := red_head _ _ x <| red_head _ _ f <| h
+    _ ↠ Church n f x := by apply ha'
 
+/-! ### Church numeral basics
 
-/-! ### Church numeral basics -/
+Canonical constructors, iteration and primitive recursion.
+-/
 
 /-- Church zero := λ f x. x -/
 protected def Zero : SKI := K ⬝ I
+
 @[scoped grind .]
-theorem zero_correct : IsChurch 0 SKI.Zero := by
-  unfold IsChurch SKI.Zero Church
+theorem realizes_zero : SKI.Zero ⊩ 0 := by
   intro f x
   calc
   _ ↠ I ⬝ x := by apply Relation.ReflTransGen.single; apply red_head; apply red_K
@@ -101,22 +98,22 @@ theorem zero_correct : IsChurch 0 SKI.Zero := by
 
 /-- Church one := λ f x. f x -/
 protected def One : SKI := I
+
 @[scoped grind .]
-theorem one_correct : IsChurch 1 SKI.One := by
+theorem realizes_one : SKI.One ⊩ 1 := by
   intro f x
   apply head
   exact .single (red_I f)
 
 /-- Church succ := λ a f x. f (a f x) ~ λ a f. B f (a f) ~ λ a. S B a ~ S B -/
 protected def Succ : SKI := S ⬝ B
-@[scoped grind →]
-theorem succ_correct (n : Nat) (a : SKI) (h : IsChurch n a) :
-    IsChurch (n+1) (SKI.Succ ⬝ a) := by
-  intro f x
+
+theorem realizes_succ : SKI.Succ ⊩ Nat.succ := by
+  intro n xn hn f x
   calc
-  _ ⭢ B ⬝ f ⬝ (a ⬝ f) ⬝ x := by apply red_head; apply red_S
-  _ ↠ f ⬝ (a ⬝ f ⬝ x) := by apply B_def
-  _ ↠ f ⬝ (Church n  f x) := by apply MRed.tail; exact h f x
+  _ ⭢ B ⬝ f ⬝ (xn ⬝ f) ⬝ x := by apply red_head; apply red_S
+  _ ↠ f ⬝ (xn ⬝ f ⬝ x) := by apply B_def
+  _ ↠ f ⬝ (Church n  f x) := by apply MRed.tail; exact hn f x
 
 /-- Build the canonical SKI Church numeral for `n`. -/
 def toChurch : ℕ → SKI
@@ -125,81 +122,94 @@ def toChurch : ℕ → SKI
 
 /-- `toChurch 0 = Zero`. -/
 @[simp] lemma toChurch_zero : toChurch 0 = SKI.Zero := rfl
+
 /-- `toChurch (n + 1) = Succ ⬝ toChurch n`. -/
 @[simp] lemma toChurch_succ (n : ℕ) : toChurch (n + 1) = SKI.Succ ⬝ (toChurch n) := rfl
 
 /-- `toChurch n` correctly represents `n`. -/
 @[scoped grind .]
-theorem toChurch_correct (n : ℕ) : IsChurch n (toChurch n) := by
+theorem realizes_toChurch (n : ℕ) : (toChurch n) ⊩ n := by
   induction n with
-  | zero => exact zero_correct
-  | succ n ih => exact succ_correct n (toChurch n) ih
+  | zero => exact realizes_zero
+  | succ n ih => exact realizes_succ ih
 
-/--
-To define the predecessor, iterate the function `PredAux` ⟨i, j⟩ ↦ ⟨j, j+1⟩ on ⟨0,0⟩, then take
-the  first component.
--/
-def PredAuxPoly : SKI.Polynomial 1 := MkPair ⬝' (Snd ⬝' &0) ⬝' (SKI.Succ ⬝' (Snd ⬝' &0))
-/-- A term representing PredAux -/
-def PredAux : SKI := PredAuxPoly.toSKI
-theorem predAux_def (p : SKI) :  (PredAux ⬝ p) ↠ MkPair ⬝ (Snd ⬝ p) ⬝ (SKI.Succ ⬝ (Snd ⬝ p)) :=
-  PredAuxPoly.toSKI_correct [p] (by simp)
-
-/-- Useful auxiliary definition expressing that `p` represents ns ∈ Nat × Nat. -/
-def IsChurchPair (ns : Nat × Nat) (x : SKI) : Prop :=
-  IsChurch ns.1 (Fst ⬝ x) ∧ IsChurch ns.2 (Snd ⬝ x)
-
-theorem isChurchPair_trans (ns : Nat × Nat) (a a' : SKI) (h : a ↠ a') :
-    IsChurchPair ns a' → IsChurchPair ns a := by
-  simp_rw [IsChurchPair]
-  intro ⟨ha₁,ha₂⟩
-  constructor
-  · apply isChurch_trans (a' := Fst ⬝ a')
-    · apply MRed.tail; exact h
-    · exact ha₁
-  · apply isChurch_trans (a' := Snd ⬝ a')
-    · apply MRed.tail; exact h
-    · exact ha₂
-
-theorem predAux_correct (p : SKI) (ns : Nat × Nat) (h : IsChurchPair ns p) :
-    IsChurchPair ⟨ns.2, ns.2+1⟩ (PredAux ⬝ p) := by
-  refine isChurchPair_trans _ _ (MkPair ⬝ (Snd ⬝ p) ⬝ (SKI.Succ ⬝ (Snd ⬝ p))) (predAux_def p) ?_
-  constructor
-  · exact isChurch_trans ns.2 (fst_correct _ _) h.2
-  · refine isChurch_trans (ns.2+1) (snd_correct _ _) ?_
-    exact succ_correct ns.2 (Snd ⬝ p) h.2
-
-/-- The stronger induction hypothesis necessary for the proof of `pred_correct`. -/
-theorem predAux_correct' (n : Nat) :
-    IsChurchPair (n.pred, n) <| Church n PredAux  (MkPair ⬝ SKI.Zero ⬝ SKI.Zero) := by
+variable {α : Type*} [HasRealizerLift α Red]
+
+def Iter := R
+
+lemma realizes_iter : Iter ⊩ (Nat.iterate (α := α)) := by
+  intro f xf hf n xn hn a xa ha
+  suffices (Church n xf xa) ⊩ f^[n] a by
+    apply this.left_of_mRed
+    calc
+      _ ↠ xn ⬝ xf ⬝ xa := MRed.head _ <| R_def ..
+      _ ↠ Church n xf xa := hn ..
+  clear hn
   induction n with
-    | zero =>
-      apply isChurchPair_trans ⟨0,0⟩ _ (MkPair ⬝ SKI.Zero ⬝ SKI.Zero)
-        (by rfl)
-      constructor <;> apply isChurch_trans 0 ?_ zero_correct
-      · exact fst_correct _ _
-      · exact snd_correct _ _
-    | succ n ih =>
-      simp_rw [Church_succ]
-      apply predAux_correct (ns := ⟨n.pred, n⟩) (h := ih)
-
-/-- Predecessor := λ n. Fst ⬝ (n ⬝ PredAux ⬝ (MkPair ⬝ Zero ⬝ Zero)) -/
-def PredPoly : SKI.Polynomial 1 := Fst ⬝' (&0 ⬝' PredAux ⬝' (MkPair ⬝ SKI.Zero ⬝ SKI.Zero))
-/-- A term representing Pred -/
-def Pred : SKI := PredPoly.toSKI
-theorem pred_def (a : SKI) : (Pred ⬝ a) ↠ Fst ⬝ (a ⬝ PredAux ⬝ (MkPair ⬝ SKI.Zero ⬝ SKI.Zero)) :=
-  PredPoly.toSKI_correct [a] (by simp)
-
-theorem pred_correct (n : Nat) (a : SKI) (h : IsChurch n a) : IsChurch n.pred (Pred ⬝ a) := by
-  refine isChurch_trans n.pred
-    (pred_def a) ?_
-  refine isChurch_trans _ (a' := Fst ⬝ (Church n PredAux (MkPair ⬝ SKI.Zero ⬝ SKI.Zero))) ?_ ?_
-  · apply MRed.tail
-    exact h _ _
-  · exact predAux_correct' n |>.1
-
-
-/-! ### Primitive recursion -/
+  | zero => simpa
+  | succ n ih =>
+      rw [Function.iterate_succ']
+      exact hf ih
+
+def Nat.recPairStep (f : Nat → α → α) : α × Nat → α × Nat
+  | ⟨y, m⟩ => ⟨f m y, m + 1⟩
+
+lemma Nat.realizes_recPairStep {α' : Type*} (a : α') (f : Nat → α' → α') (n : Nat) :
+    (Nat.recPairStep f)^[n] ⟨a, 0⟩ = ⟨Nat.rec a f n, n⟩ := by
+  induction n with
+  | zero => simp
+  | succ n ih =>
+    rw [Function.iterate_succ', Function.comp_apply, ih, recPairStep]
+
+/-- We encode primitive recursion on `Nat` by the usual Kleene dentist trick. -/
+def natRecAuxPoly : SKI.Polynomial 2 :=
+  SKI.MkPair ⬝' (&0 ⬝' (Snd ⬝' &1) ⬝' (Fst ⬝' &1)) ⬝' (SKI.Succ ⬝' (Snd ⬝' &1))
+def natRecAux := natRecAuxPoly.toSKI
+lemma natRecAux_def (f p : SKI) :
+    (natRecAux ⬝ f ⬝ p) ↠ SKI.MkPair ⬝ (f ⬝ (Snd ⬝ p) ⬝ (Fst ⬝ p)) ⬝ (SKI.Succ ⬝ (Snd ⬝ p)) :=
+  natRecAuxPoly.toSKI_correct [f, p] (by simp)
+
+lemma natRecAux_realizes {f : Nat → α → α} {xf : SKI} (hf : xf ⊩ f) :
+    (natRecAux ⬝ xf) ⊩ (Nat.recPairStep f) := by
+  intro p xp hp
+  suffices (SKI.MkPair ⬝ (xf ⬝ (Snd ⬝ xp) ⬝ (Fst ⬝ xp)) ⬝ (SKI.Succ ⬝ (Snd ⬝ xp))) ⊩
+      (Nat.recPairStep f p) by
+    exact this.left_of_mRed <| natRecAux_def ..
+  apply realizes_mkPair
+  · exact hf hp.2 hp.1
+  · exact SKI.realizes_succ hp.2
+
+lemma realizes_recPairStep_iter {a : α} {xa : SKI} (ha : xa ⊩ a)
+    {f : Nat → α → α} {xf : SKI} (hf : xf ⊩ f) {n : Nat} {xn : SKI} (hn : xn ⊩ n) :
+    (R ⬝ (natRecAux ⬝ xf) ⬝ xn ⬝ (MkPair ⬝ xa ⬝ SKI.Zero)) ⊩ (⟨Nat.rec a f n, n⟩ : α × Nat) := by
+  rw [←Nat.realizes_recPairStep]
+  refine realizes_iter (natRecAux_realizes hf) hn ?_
+  apply realizes_mkPair
+  · exact ha
+  · exact realizes_zero
+
+def natRecPoly : SKI.Polynomial 3 :=
+  Fst ⬝' (R ⬝' (natRecAux ⬝' &1) ⬝' &2 ⬝' (MkPair ⬝' &0 ⬝' SKI.Zero))
+def natRec := natRecPoly.toSKI
+lemma natRec_def (xa xf xn : SKI) :
+    (natRec ⬝ xa ⬝ xf ⬝ xn) ↠ Fst ⬝ (R ⬝ (natRecAux ⬝ xf) ⬝ xn ⬝ (MkPair ⬝ xa ⬝ SKI.Zero)) :=
+  natRecPoly.toSKI_correct [xa, xf, xn] (by simp)
+
+/-- Primitive recursion on `Nat`. -/
+theorem realizes_nat_rec :
+    natRec ⊩ (Nat.rec : α → (Nat → α → α) → Nat → α) := by
+  intro a xa ha f xf hf n xn hn
+  exact Realizes.left_of_mRed (realizes_recPairStep_iter ha hf hn).1 (natRec_def xa xf xn)
+
+def Pred : SKI := natRec ⬝ SKI.Zero ⬝ K
+
+theorem realizes_pred : Pred ⊩ Nat.pred := by
+  intro n xn hn
+  have : n.pred = n.rec 0 (fun a _ => a) := by induction n <;> simp
+  rw [this]
+  refine realizes_nat_rec realizes_zero ?_ hn
+  intro _ _ h _ _ _
+  exact h.left_of_red <| red_K ..
 
 /-- IsZero := λ n. n (K FF) TT -/
 def IsZeroPoly : SKI.Polynomial 1 := &0 ⬝' (K ⬝ FF) ⬝' TT
@@ -207,65 +217,22 @@ def IsZeroPoly : SKI.Polynomial 1 := &0 ⬝' (K ⬝ FF) ⬝' TT
 def IsZero : SKI := IsZeroPoly.toSKI
 theorem isZero_def (a : SKI) : (IsZero ⬝ a) ↠ a ⬝ (K ⬝ FF) ⬝ TT :=
   IsZeroPoly.toSKI_correct [a] (by simp)
-theorem isZero_correct (n : Nat) (a : SKI) (h : IsChurch n a) :
-    IsBool (n = 0) (IsZero ⬝ a) := by
-  apply isBool_trans (a' := a ⬝ (K ⬝ FF) ⬝ TT) (h := isZero_def a)
-  by_cases n=0
+
+theorem realizes_isZero : IsZero ⊩ (· == 0) := by
+  intro n xn hn
+  refine Realizes.left_of_mRed ?_ (isZero_def _)
+  by_cases n = 0
   case pos h0 =>
-    simp_rw [h0]
-    rw [h0] at h
-    apply isBool_trans (ha' := TT_correct)
-    exact h _ _
+    simp_rw [h0] at hn ⊢
+    exact realizes_true.left_of_mRed <| hn ..
   case neg h0 =>
-    simp_rw [h0]
-    let ⟨k,hk⟩ := Nat.exists_eq_succ_of_ne_zero h0
-    rw [hk] at h
-    apply isBool_trans (ha' := FF_correct)
+    simp_rw [beq_false_of_ne h0]
+    let ⟨k, hk⟩ := Nat.exists_eq_succ_of_ne_zero h0
+    rw [hk] at hn
+    apply realizes_false.left_of_mRed
     calc
-    _ ↠ (K ⬝ FF) ⬝ Church k (K ⬝ FF) TT := h _ _
-    _ ⭢ FF := red_K _ _
-
-
-/--
-To define `Rec x g n := if n==0 then x else (Rec x g (Pred n))`, we obtain a fixed point of
-R ↦ λ x g n. Cond ⬝ (IsZero ⬝ n) ⬝ x ⬝ (g ⬝ a ⬝ (R ⬝ x ⬝ g ⬝ (Pred ⬝ n)))
--/
-def RecAuxPoly : SKI.Polynomial 4 :=
-  SKI.Cond ⬝' &1 ⬝' (&2 ⬝' &3 ⬝' (&0 ⬝' &1 ⬝' &2 ⬝' (Pred ⬝' &3))) ⬝' (IsZero ⬝' &3)
-/-- A term representing RecAux -/
-def RecAux : SKI := RecAuxPoly.toSKI
-theorem recAux_def (R₀ x g a : SKI) :
-    (RecAux ⬝ R₀ ⬝ x ⬝ g ⬝ a) ↠
-      SKI.Cond ⬝ x ⬝ (g ⬝ a ⬝ (R₀ ⬝ x ⬝ g ⬝ (Pred ⬝ a))) ⬝ (IsZero ⬝ a)  :=
-  RecAuxPoly.toSKI_correct [R₀, x, g, a] (by simp)
-
-/--
-We define Rec so that
-`Rec ⬝ x ⬝ g ⬝ a ↠ SKI.Cond ⬝ x ⬝ (g ⬝ a ⬝ (Rec ⬝ x ⬝ g ⬝ (Pred ⬝ a))) ⬝ (IsZero ⬝ a)`
--/
-def Rec : SKI := fixedPoint RecAux
-theorem rec_def (x g a : SKI) :
-  (Rec ⬝ x ⬝ g ⬝ a) ↠ SKI.Cond ⬝ x ⬝ (g ⬝ a ⬝ (Rec ⬝ x ⬝ g ⬝ (Pred ⬝ a))) ⬝ (IsZero ⬝ a) := calc
-  _ ↠ RecAux ⬝ Rec ⬝ x ⬝ g ⬝ a := by
-      apply MRed.head; apply MRed.head; apply MRed.head
-      apply fixedPoint_correct
-  _ ↠ SKI.Cond ⬝ x ⬝ (g ⬝ a ⬝ (Rec ⬝ x ⬝ g ⬝ (Pred ⬝ a))) ⬝ (IsZero ⬝ a) := recAux_def Rec x g a
-
-theorem rec_zero (x g a : SKI) (ha : IsChurch 0 a) : (Rec ⬝ x ⬝ g ⬝ a) ↠ x := by
-  calc
-  _ ↠ SKI.Cond ⬝ x ⬝ (g ⬝ a ⬝ (Rec ⬝ x ⬝ g ⬝ (Pred ⬝ a))) ⬝ (IsZero ⬝ a) := rec_def _ _ _
-  _ ↠ if (Nat.beq 0 0) then x else (g ⬝ a ⬝ (Rec ⬝ x ⬝ g ⬝ (Pred ⬝ a))) := by
-      apply cond_correct
-      exact isZero_correct 0 a ha
-
-theorem rec_succ (n : Nat) (x g a : SKI) (ha : IsChurch (n + 1) a) :
-    (Rec ⬝ x ⬝ g ⬝ a) ↠ g ⬝ a ⬝ (Rec ⬝ x ⬝ g ⬝ (Pred ⬝ a)) := by
-  calc
-  _ ↠ SKI.Cond ⬝ x ⬝ (g ⬝ a ⬝ (Rec ⬝ x ⬝ g ⬝ (Pred ⬝ a))) ⬝ (IsZero ⬝ a) := rec_def _ _ _
-  _ ↠ if (Nat.beq (n+1) 0) then x else (g ⬝ a ⬝ (Rec ⬝ x ⬝ g ⬝ (Pred ⬝ a))) := by
-      apply cond_correct
-      exact isZero_correct (n+1) a ha
-
+    _ ↠ (K ⬝ FF) ⬝ Church k (K ⬝ FF) TT := hn ..
+    _ ⭢ FF := red_K ..
 
 /-! ### Root-finding (μ-recursion) -/
 
@@ -282,55 +249,47 @@ lemma rfindAboveAux_def (R₀ f a : SKI) :
     (RFindAboveAux ⬝ R₀ ⬝ a ⬝ f) ↠ SKI.Cond ⬝ a ⬝ (R₀ ⬝ (SKI.Succ ⬝ a) ⬝ f) ⬝ (IsZero ⬝ (f ⬝ a)) :=
   RFindAboveAuxPoly.toSKI_correct [R₀, a, f] (by trivial)
 
-theorem rfindAboveAux_base (R₀ f a : SKI) (hfa : IsChurch 0 (f ⬝ a)) :
+theorem rfindAboveAux_base (R₀ f a : SKI) (hfa : (f ⬝ a) ⊩ 0) :
     (RFindAboveAux ⬝ R₀ ⬝ a ⬝ f) ↠ a := calc
   _ ↠ SKI.Cond ⬝ a ⬝ (R₀ ⬝ (SKI.Succ ⬝ a) ⬝ f) ⬝ (IsZero ⬝ (f ⬝ a)) := rfindAboveAux_def _ _ _
   _ ↠ if (Nat.beq 0 0) then a else (R₀ ⬝ (SKI.Succ ⬝ a) ⬝ f) := by
-      apply cond_correct
-      apply isZero_correct _ _ hfa
-theorem rfindAboveAux_step (R₀ f a : SKI) {m : Nat} (hfa : IsChurch (m + 1) (f ⬝ a)) :
+      exact cond_def <| realizes_isZero hfa
+
+theorem rfindAboveAux_step (R₀ f a : SKI) {m : Nat} (hfa : (f ⬝ a) ⊩ m + 1) :
     (RFindAboveAux ⬝ R₀ ⬝ a ⬝ f) ↠ R₀ ⬝ (SKI.Succ ⬝ a) ⬝ f := calc
   _ ↠ SKI.Cond ⬝ a ⬝ (R₀ ⬝ (SKI.Succ ⬝ a) ⬝ f) ⬝ (IsZero ⬝ (f ⬝ a)) := rfindAboveAux_def _ _ _
-  _ ↠ if (Nat.beq (m+1) 0) then a else (R₀ ⬝ (SKI.Succ ⬝ a) ⬝ f) := by
-      apply cond_correct
-      apply isZero_correct _ _ hfa
+  _ ↠ if (Nat.beq (m + 1) 0) then a else (R₀ ⬝ (SKI.Succ ⬝ a) ⬝ f) := by
+      exact cond_def <| realizes_isZero hfa
 
 /-- Find the minimal root of `fNat` above a number n -/
 def RFindAbove : SKI := RFindAboveAux.fixedPoint
-theorem RFindAbove_correct (fNat : Nat → Nat) (f x : SKI)
-    (hf : ∀ i : Nat, ∀ y : SKI, IsChurch i y →  IsChurch (fNat i) (f ⬝ y))
-    (n m : Nat) (hx : IsChurch m x) (hroot : fNat (m+n) = 0) (hpos : ∀ i < n, fNat (m+i) ≠ 0) :
-    IsChurch (m+n) (RFindAbove ⬝ x ⬝ f) := by
+
+theorem RFindAbove_correct (f : Nat → Nat) (xf x : SKI) (hf : xf ⊩ f) (n m : Nat) (hx : x ⊩ m)
+    (hroot : f (m + n) = 0) (hpos : ∀ i < n, f (m + i) ≠ 0) :
+    (RFindAbove ⬝ x ⬝ xf) ⊩ (m + n) := by
   induction n generalizing m x
-  all_goals apply isChurch_trans (a' := RFindAboveAux ⬝ RFindAbove ⬝ x ⬝ f)
-  case zero.a =>
-    apply isChurch_trans (a' := x) <;>
-      grind [rfindAboveAux_base]
-  case succ.a n ih =>
-    apply isChurch_trans (a' := RFindAbove ⬝ (SKI.Succ ⬝ x) ⬝ f)
-    · let y := (fNat m).pred
-      have : IsChurch (y + 1) (f ⬝ x) := by
-        subst y
-        exact Nat.succ_pred_eq_of_ne_zero (hpos 0 (by simp)) ▸ hf m x hx
-      apply rfindAboveAux_step
-      assumption
-    · replace ih := ih (SKI.Succ ⬝ x) (m + 1) (succ_correct _ x hx)
+  all_goals apply Realizes.left_of_mRed (y := RFindAboveAux ⬝ RFindAbove ⬝ x ⬝ xf)
+  case zero.ha =>
+    apply hx.left_of_mRed
+    apply rfindAboveAux_base
+    exact hroot ▸ hf hx
+  case succ.ha n ih =>
+    apply Realizes.left_of_mRed (y := RFindAbove ⬝ (SKI.Succ ⬝ x) ⬝ xf)
+    · replace ih := ih (SKI.Succ ⬝ x) (m + 1) (realizes_succ hx)
       grind
+    · have : (xf ⬝ x) ⊩ ((f m).pred + 1) := Nat.succ_pred_eq_of_ne_zero (hpos 0 (by simp)) ▸ hf hx
+      exact rfindAboveAux_step _ _ _ this
   -- close the `h` goals of the above `apply isChurch_trans`
   all_goals {apply MRed.head; apply MRed.head; exact fixedPoint_correct _}
 
-
 /-- Ordinary root finding is root finding above zero -/
 def RFind := RFindAbove ⬝ SKI.Zero
-theorem RFind_correct (fNat : Nat → Nat) (f : SKI)
-    (hf : ∀ (i : Nat) (y : SKI), IsChurch i y → IsChurch (fNat i) (f ⬝ y))
-    (n : Nat) (hroot : fNat n = 0) (hpos : ∀ i < n, fNat i ≠ 0) : IsChurch n (RFind ⬝ f) := by
-  have :_ := RFindAbove_correct (n := n) (fNat := fNat) (hf := hf) (hx := zero_correct)
+theorem RFind_correct (f : Nat → Nat) (xf : SKI) (hf : xf ⊩ f)
+    (n : Nat) (hroot : f n = 0) (hpos : ∀ i < n, f i ≠ 0) : (RFind ⬝ xf) ⊩ n := by
+  have :_ := RFindAbove_correct (n := n) (f := f) (hf := hf) (hx := realizes_zero)
   simp_rw [Nat.zero_add] at this
   exact this hroot hpos
 
-
-
 /-! ### Further numeric operations -/
 
 /-- Addition: λ n m. n Succ m -/
@@ -340,18 +299,17 @@ protected def Add : SKI := AddPoly.toSKI
 theorem add_def (a b : SKI) : (SKI.Add ⬝ a ⬝ b) ↠ a ⬝ SKI.Succ ⬝ b :=
   AddPoly.toSKI_correct [a, b] (by simp)
 
-theorem add_correct (n m : Nat) (a b : SKI) (ha : IsChurch n a) (hb : IsChurch m b) :
-    IsChurch (n + m) (SKI.Add ⬝ a ⬝ b) := by
-  refine isChurch_trans (n + m) (a' := Church n SKI.Succ b) ?_ ?_
-  · calc
-    _ ↠ a ⬝ SKI.Succ ⬝ b := add_def a b
-    _ ↠ Church n SKI.Succ b := ha SKI.Succ b
-  · clear ha
+theorem realizes_add : SKI.Add ⊩ Nat.add:= by
+  intro n xn hn m xm hm
+  refine Realizes.left_of_mRed (y := Church n SKI.Succ xm) ?_ ?_
+  · clear hn
     induction n with
-      | zero => simp_rw [Nat.zero_add, Church]; exact hb
+      | zero => simpa
       | succ n ih =>
-        simp_rw [Nat.add_right_comm, Church]
-        exact succ_correct _ _ ih
+        simpa [Nat.add_right_comm] using realizes_succ ih
+  · calc
+    _ ↠ xn ⬝ SKI.Succ ⬝ xm := add_def ..
+    _ ↠ Church n SKI.Succ xm := hn ..
 
 /-- Multiplication: λ n m. n (Add m) Zero -/
 def MulPoly : SKI.Polynomial 2 := &0 ⬝' (SKI.Add ⬝' &1) ⬝' SKI.Zero
@@ -360,16 +318,15 @@ protected def Mul : SKI := MulPoly.toSKI
 theorem mul_def (a b : SKI) : (SKI.Mul ⬝ a ⬝ b) ↠ a ⬝ (SKI.Add ⬝ b) ⬝ SKI.Zero :=
   MulPoly.toSKI_correct [a, b] (by simp)
 
-theorem mul_correct {n m : Nat} {a b : SKI} (ha : IsChurch n a) (hb : IsChurch m b) :
-    IsChurch (n * m) (SKI.Mul ⬝ a ⬝ b) := by
-  refine isChurch_trans (n * m) (a' := Church n (SKI.Add ⬝ b) SKI.Zero) ?_ ?_
-  · exact Trans.trans (mul_def a b) (ha (SKI.Add ⬝ b) SKI.Zero)
-  · clear ha
+theorem realizes_mul : SKI.Mul ⊩ Nat.mul := by
+  intro n xn hn m xm hm
+  refine Realizes.left_of_mRed (y := Church n (SKI.Add ⬝ xm) SKI.Zero) ?_ ?_
+  · clear hn
     induction n with
-      | zero => simp_rw [Nat.zero_mul, Church]; exact zero_correct
+      | zero => simpa using realizes_zero
       | succ n ih =>
-        simp_rw [Nat.add_mul, Nat.one_mul, Nat.add_comm, Church]
-        exact add_correct m (n * m) b (Church n (SKI.Add ⬝ b) SKI.Zero) hb ih
+        simpa [Nat.add_mul, Nat.one_mul, Nat.add_comm, Church] using realizes_add hm ih
+  · exact Trans.trans (mul_def xn xm) (hn (SKI.Add ⬝ xm) SKI.Zero)
 
 /-- Subtraction: λ n m. n Pred m -/
 def SubPoly : SKI.Polynomial 2 := &1 ⬝' Pred ⬝' &0
@@ -378,18 +335,17 @@ protected def Sub : SKI := SubPoly.toSKI
 theorem sub_def (a b : SKI) : (SKI.Sub ⬝ a ⬝ b) ↠ b ⬝ Pred ⬝ a :=
   SubPoly.toSKI_correct [a, b] (by simp)
 
-theorem sub_correct (n m : Nat) (a b : SKI) (ha : IsChurch n a) (hb : IsChurch m b) :
-    IsChurch (n - m) (SKI.Sub ⬝ a ⬝ b) := by
-  refine isChurch_trans (n - m) (a' := Church m Pred a) ?_ ?_
-  · calc
-    _ ↠ b ⬝ Pred ⬝ a := sub_def a b
-    _ ↠ Church m Pred a := hb Pred a
-  · clear hb
+theorem realizes_sub : SKI.Sub ⊩ Nat.sub := by
+  intro n xn hn m xm hm
+  refine Realizes.left_of_mRed (y := Church m Pred xn) ?_ ?_
+  · clear hm
     induction m with
-      | zero => simp_rw [Nat.sub_zero, Church]; exact ha
+      | zero => simpa using hn
       | succ m ih =>
-        simp_rw [←Nat.sub_sub, Church]
-        exact pred_correct _ _ ih
+        simpa using realizes_pred ih
+  · calc
+    _ ↠ xm ⬝ Pred ⬝ xn := sub_def ..
+    _ ↠ Church m Pred xn := hm Pred xn
 
 /-- Comparison: (. ≤ .) := λ n m. IsZero ⬝ (Sub ⬝ n ⬝ m) -/
 def LEPoly : SKI.Polynomial 2 := IsZero ⬝' (SKI.Sub ⬝' &0 ⬝' &1)
@@ -398,12 +354,12 @@ protected def LE : SKI := LEPoly.toSKI
 theorem le_def (a b : SKI) : (SKI.LE ⬝ a ⬝ b) ↠ IsZero ⬝ (SKI.Sub ⬝ a ⬝ b) :=
   LEPoly.toSKI_correct [a, b] (by simp)
 
-theorem le_correct (n m : Nat) (a b : SKI) (ha : IsChurch n a) (hb : IsChurch m b) :
-    IsBool (n ≤ m) (SKI.LE ⬝ a ⬝ b) := by
-  simp only [← decide_eq_decide.mpr <| Nat.sub_eq_zero_iff_le]
-  apply isBool_trans (a' := IsZero ⬝ (SKI.Sub ⬝ a ⬝ b)) (h := le_def _ _)
-  apply isZero_correct
-  apply sub_correct <;> assumption
+theorem realizes_le : SKI.LE ⊩ (· ≤ · : Nat → Nat → Bool) := by
+  intro n xn hn m xm hm
+  simp_rw [← decide_eq_decide.mpr <| Nat.sub_eq_zero_iff_le]
+  apply Realizes.left_of_mRed (y := IsZero ⬝ (SKI.Sub ⬝ xn ⬝ xm)) (h := le_def _ _)
+  apply realizes_isZero
+  apply realizes_sub <;> assumption
 
 end SKI