1 files changed, 45 insertions, 0 deletions
diff --git a/src/scenes/substitution.tsx b/src/scenes/substitution.tsx
new file mode 100644
index 0000000..1e7e48c
--- /dev/null
+++ b/src/scenes/substitution.tsx
@@ -0,0 +1,45 @@
+import { Layout, Txt, makeScene2D } from "@motion-canvas/2d";
+import {
+  Direction,
+  beginSlide,
+  createRef,
+  slideTransition,
+} from "@motion-canvas/core";
+import { theme } from "../theme";
+
+const substitution = [
+  "β-reduce [ (λ x . x) y ] => y\n\n",
+  "Formal definition:",
+  "1. x[x := N] = N",
+  "2. y[x := N] = y if y != x",
+  "3. (M N)[x := P] = (M[x := P]) (N[x := P])",
+  "4. (λ x . M)[x := N] = λ x . M",
+  "5. (λ y . M)[x := N] = λ y . (M[x := N]) if y != x and y is not _free_ in N",
+  " +=> A variable is _free_ in a lambda term if it is not bound by a λ abstraction.",
+];
+
+export default makeScene2D(function* (view) {
+  const rules = createRef<Txt>();
+
+  view.add(
+    <Layout layout direction="column" alignItems="center">
+      <Txt fontSize={40} fontFamily={theme.font} fill={theme.text.hex}>
+        The Lambda Calculus - Substitution Rules
+      </Txt>
+      <Txt
+        ref={rules}
+        fontSize={30}
+        fontFamily={theme.font}
+        fill={theme.text.hex}
+      ></Txt>
+    </Layout>
+  );
+
+  yield* slideTransition(Direction.Right);
+  yield* beginSlide("The Lambda Calculus - Substitutions");
+
+  for (const rule of substitution) {
+    yield* rules().text(rules().text() + "\n\n" + rule, 1);
+    yield* beginSlide("substitution - " + rule);
+  }
+});