From 0cc5707ce0fbcc100804350f59fb6c5b4e599ce8 Mon Sep 17 00:00:00 2001
From: milner <m@cpl0.zip>
Date: Tue, 22 Sep 2026 12:59:00 +0200
Subject: [PATCH] add(subsystem): define the relation generated by R and Gc and
 prove its embedding into red1 (M3 infrastructure)

---
 scripts/audit.sh   |  2 +-
 theory/Subsystem.v | 40 ++++++++++++++++++++++++++++++++++++++++
 2 files changed, 41 insertions(+), 1 deletion(-)
 create mode 100644 theory/Subsystem.v

diff --git a/scripts/audit.sh b/scripts/audit.sh
index 7a4166a..49d0cb9 100755
--- a/scripts/audit.sh
+++ b/scripts/audit.sh
@@ -35,7 +35,7 @@ done < <(find theory -name '*.v' -print0 2>/dev/null)
 echo "== Print Assumptions =="
 WORK="$(mktemp -d ./.audit-work.XXXXXX)"
 cp theory/*.v "$WORK"/
-for f in ExecReducer Binding Reduction Metatheory Tests; do
+for f in ExecReducer Binding Reduction Metatheory Subsystem Tests; do
   echo "-- $f"
   out="$(rocq compile -Q "$WORK" LambdaSub "$WORK/$f.v" 2>&1 || true)"
   echo "$out"
diff --git a/theory/Subsystem.v b/theory/Subsystem.v
new file mode 100644
index 0000000..69385bf
--- /dev/null
+++ b/theory/Subsystem.v
@@ -0,0 +1,40 @@
+From Stdlib Require Import List Bool Arith Lia PeanoNat.
+Import ListNotations.
+From LambdaSub Require Import ExecReducer Binding Reduction.
+
+Inductive red_sub_root : trm -> trm -> Prop :=
+| rs_gc : forall body u, occurs0 body = false -> red_sub_root (ESub body u) body
+| rs_r : forall C body u, zfill C 0 = body ->
+    red_sub_root (ESub body u) (ESub (zplug_lift C 0 u) u).
+
+Inductive red_sub : trm -> trm -> Prop :=
+| red_sub_base : forall t t', red_sub_root t t' -> red_sub t t'
+| red_sub_ctx : forall C t t', red_sub t t' -> red_sub (plug C t) (plug C t').
+
+Lemma red_sub_root_to_red1 : forall t t', red_sub_root t t' -> red1 t t'.
+Proof.
+  intros t t' H. destruct H.
+  - exists RGc. apply red1r_root. apply rGc. exact H.
+  - exists RR. apply red1r_root. apply rR. exact H.
+Qed.
+
+Lemma red_sub_to_red1 : forall t t', red_sub t t' -> red1 t t'.
+Proof.
+  intros t t' H. induction H.
+  - apply red_sub_root_to_red1. exact H.
+  - destruct IHred_sub as [r Hr]. exists r. apply rctx. exact Hr.
+Qed.
+
+Lemma red_sub_context : forall C t t', red_sub t t' -> red_sub (plug C t) (plug C t').
+Proof. intros. apply red_sub_ctx. exact H. Qed.
+
+Lemma red_sub_gc : forall body u, occurs0 body = false -> red_sub (ESub body u) body.
+Proof. intros. apply red_sub_base. apply rs_gc. exact H. Qed.
+
+Lemma red_sub_r : forall C body u, zfill C 0 = body ->
+  red_sub (ESub body u) (ESub (zplug_lift C 0 u) u).
+Proof. intros. apply red_sub_base. apply rs_r. exact H. Qed.
+
+Print Assumptions red_sub_root_to_red1.
+Print Assumptions red_sub_to_red1.
+Print Assumptions red_sub_context.