From 25edeaa5ce9b6268d8db0428c3c4770673e0eb88 Mon Sep 17 00:00:00 2001 From: sneeker Date: Tue, 22 Sep 2026 13:49:00 +0200 Subject: [PATCH] add(subsystem): occurrence count per explicit substitution and the absence of a critical overlap between R and Gc (M3 infrastructure) --- theory/Subsystem.v | 24 ++++++++++++++++++++++++ 1 file changed, 24 insertions(+) diff --git a/theory/Subsystem.v b/theory/Subsystem.v index 69385bf..4ca9c43 100644 --- a/theory/Subsystem.v +++ b/theory/Subsystem.v @@ -38,3 +38,27 @@ 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. + +Lemma occurs_zfill : forall C k, occurs k (zfill C k) = true. +Proof. + induction C; intros k; simpl. + - rewrite Nat.eqb_refl. reflexivity. + - rewrite IHC. reflexivity. + - rewrite IHC. rewrite orb_true_r. reflexivity. + - rewrite (IHC (S k)). reflexivity. + - rewrite (IHC (S k)). reflexivity. + - rewrite IHC. rewrite orb_true_r. reflexivity. +Qed. + +Lemma zfill_occurs0 : forall C body, zfill C 0 = body -> occurs0 body = true. +Proof. intros C body H. rewrite <- H. apply occurs_zfill. Qed. + +Lemma R_Gc_disjoint : forall body, occurs0 body = false -> ~ (exists C, zfill C 0 = body). +Proof. + intros body Hf [C HC]. apply zfill_occurs0 in HC. + rewrite Hf in HC. discriminate HC. +Qed. + +Print Assumptions occurs_zfill. +Print Assumptions zfill_occurs0. +Print Assumptions R_Gc_disjoint.