From 28b7faac052f4ed135f3f06a5e16c8f4867492c4 Mon Sep 17 00:00:00 2001 From: Mysaa Date: Wed, 31 May 2023 13:59:33 +0200 Subject: [PATCH] Added a generalized version of the Normalization proof --- ListUtil.agda | 65 +++++++++++-- Prop.agda | 46 ---------- PropUtil.agda | 6 ++ PropositionalKripke.agda | 46 +++++++--- PropositionalKripkeGeneral.agda | 157 ++++++++++++++++++++++++++++++++ Readme.agda | 44 +++++++-- 6 files changed, 286 insertions(+), 78 deletions(-) delete mode 100644 Prop.agda create mode 100644 PropositionalKripkeGeneral.agda diff --git a/ListUtil.agda b/ListUtil.agda index a7dbad0..d54c224 100644 --- a/ListUtil.agda +++ b/ListUtil.agda @@ -9,6 +9,7 @@ module ListUtil where T : Set₀ L : List T L' : List T + L'' : List T A : T B : T @@ -38,12 +39,33 @@ module ListUtil where retro⊆ {L' = B ∷ L'} zero⊆ = next⊆ zero⊆ retro⊆ {L' = B ∷ L'} (next⊆ h) = next⊆ (retro⊆ h) + refl⊆ : L ⊆ L + refl⊆ = zero⊆ + + tran⊆ : L ⊆ L' → L' ⊆ L'' → L ⊆ L'' + tran⊆ zero⊆ h2 = h2 + tran⊆ (next⊆ h1) h2 = tran⊆ h1 (retro⊆ h2) + {- ⊂ : We can remove elements anywhere on the list, no duplicates, no reordering -} data _⊂_ : List T → List T → Prop where zero⊂ : [] ⊂ L both⊂ : L ⊂ L' → (A ∷ L) ⊂ (A ∷ L') next⊂ : L ⊂ L' → L ⊂ (A ∷ L') - + + ⊆→⊂ : L ⊆ L' → L ⊂ L' + refl⊂ : L ⊂ L + ⊆→⊂ {L = []} h = zero⊂ + ⊆→⊂ {L = x ∷ L} zero⊆ = both⊂ (refl⊂) + ⊆→⊂ {L = x ∷ L} (next⊆ h) = next⊂ (⊆→⊂ h) + refl⊂ = ⊆→⊂ refl⊆ + + tran⊂ : L ⊂ L' → L' ⊂ L'' → L ⊂ L'' + tran⊂ zero⊂ h2 = zero⊂ + tran⊂ (both⊂ h1) (both⊂ h2) = both⊂ (tran⊂ h1 h2) + tran⊂ (both⊂ h1) (next⊂ h2) = next⊂ (tran⊂ (both⊂ h1) h2) + tran⊂ (next⊂ h1) (both⊂ h2) = next⊂ (tran⊂ h1 h2) + tran⊂ (next⊂ h1) (next⊂ h2) = next⊂ (tran⊂ (next⊂ h1) h2) + {- ⊂⁰ : We can remove elements and reorder the list, as long as we don't duplicate the elements -} -----> We do not have unicity of derivation ([A,A] ⊂⁰ [A,A] can be prove by identity or by swapping its two elements --> We could do with some counting function, but ... it would not be nice, would it ? @@ -58,7 +80,27 @@ module ListUtil where data _⊂⁺_ : List T → List T → Prop where zero⊂⁺ : _⊂⁺_ {T} [] [] next⊂⁺ : L ⊂⁺ L' → L ⊂⁺ A ∷ L' - dup⊂⁺ : A ∷ L ⊂⁺ L' → A ∷ L ⊂⁺ A ∷ L' + dup⊂⁺ : L ⊂⁺ A ∷ L' → A ∷ L ⊂⁺ A ∷ L' + + ⊂→⊂⁺ : L ⊂ L' → L ⊂⁺ L' + ⊂→⊂⁺ {L' = []} zero⊂ = zero⊂⁺ + ⊂→⊂⁺ {L' = x ∷ L'} zero⊂ = next⊂⁺ (⊂→⊂⁺ zero⊂) + ⊂→⊂⁺ (both⊂ h) = dup⊂⁺ (next⊂⁺ (⊂→⊂⁺ h)) + ⊂→⊂⁺ (next⊂ h) = next⊂⁺ (⊂→⊂⁺ h) + refl⊂⁺ : L ⊂⁺ L + refl⊂⁺ = ⊂→⊂⁺ refl⊂ + tran⊂⁺ : L ⊂⁺ L' → L' ⊂⁺ L'' → L ⊂⁺ L'' + tran⊂⁺ zero⊂⁺ zero⊂⁺ = zero⊂⁺ + tran⊂⁺ zero⊂⁺ (next⊂⁺ h2) = next⊂⁺ h2 + tran⊂⁺ (next⊂⁺ h1) (next⊂⁺ h2) = next⊂⁺ (tran⊂⁺ (next⊂⁺ h1) h2) + tran⊂⁺ (next⊂⁺ h1) (dup⊂⁺ h2) = tran⊂⁺ h1 h2 + tran⊂⁺ (dup⊂⁺ h1) (next⊂⁺ h2) = next⊂⁺ (tran⊂⁺ (dup⊂⁺ h1) h2) + tran⊂⁺ (dup⊂⁺ h1) (dup⊂⁺ h2) = dup⊂⁺ (tran⊂⁺ h1 (dup⊂⁺ h2)) + + retro⊂⁺ : A ∷ L ⊂⁺ L' → L ⊂⁺ L' + retro⊂⁺ (next⊂⁺ h) = next⊂⁺ (retro⊂⁺ h) + retro⊂⁺ (dup⊂⁺ h) = h + {- ∈* : We can remove or duplicate elements and we can change their order -} -- The weakest of all relations on lists -- L ∈* L' if all elements of L exists in L' (no consideration for order nor duplication) @@ -73,19 +115,26 @@ module ListUtil where -- We show that the relation is reflexive and is implied by ⊆ refl∈* : L ∈* L - ⊆→∈* : L ⊆ L' → L ∈* L' + ⊂⁺→∈* : L ⊂⁺ L' → L ∈* L' refl∈* {L = []} = zero∈* - refl∈* {L = x ∷ L} = next∈* zero∈ (⊆→∈* (next⊆ zero⊆)) - ⊆→∈* zero⊆ = refl∈* - ⊆→∈* {L = []} (next⊆ h) = zero∈* - ⊆→∈* {L = x ∷ L} (next⊆ h) = next∈* (next∈ (mon∈∈* zero∈ (⊆→∈* h))) (⊆→∈* (retro⊆ (next⊆ h))) + refl∈* {L = x ∷ L} = next∈* zero∈ (⊂⁺→∈* (next⊂⁺ refl⊂⁺)) + ⊂⁺→∈* zero⊂⁺ = refl∈* + ⊂⁺→∈* {L = []} (next⊂⁺ h) = zero∈* + ⊂⁺→∈* {L = x ∷ L} (next⊂⁺ h) = next∈* (next∈ (mon∈∈* zero∈ (⊂⁺→∈* h))) (⊂⁺→∈* (retro⊂⁺ (next⊂⁺ h))) + ⊂⁺→∈* (dup⊂⁺ h) = next∈* zero∈ (⊂⁺→∈* h) -- Allows to grow ∈* to the right right∈* : L ∈* L' → L ∈* (A ∷ L') right∈* zero∈* = zero∈* right∈* (next∈* x h) = next∈* (next∈ x) (right∈* h) - -- Allows to grow ∈* from both sides both∈* : L ∈* L' → (A ∷ L) ∈* (A ∷ L') both∈* zero∈* = next∈* zero∈ zero∈* both∈* (next∈* x h) = next∈* zero∈ (next∈* (next∈ x) (right∈* h)) + + tran∈* : L ∈* L' → L' ∈* L'' → L ∈* L'' + tran∈* {L = []} = λ x x₁ → zero∈* + tran∈* {L = x ∷ L} (next∈* x₁ h1) h2 = next∈* (mon∈∈* x₁ h2) (tran∈* h1 h2) + + ⊆→∈* : L ⊆ L' → L ∈* L' + ⊆→∈* h = ⊂⁺→∈* (⊂→⊂⁺ (⊆→⊂ h)) diff --git a/Prop.agda b/Prop.agda deleted file mode 100644 index ab70ae5..0000000 --- a/Prop.agda +++ /dev/null @@ -1,46 +0,0 @@ -{-# OPTIONS --prop #-} - -module Prop where - - -- ⊥ is a data with no constructor - -- ⊤ is a record with one always-available constructor - data ⊥ : Prop where - record ⊤ : Prop where - constructor tt - - - data _∨_ : Prop → Prop → Prop where - inj₁ : {P Q : Prop} → P → P ∨ Q - inj₂ : {P Q : Prop} → Q → P ∨ Q - record _∧_ (P Q : Prop) : Prop where - constructor ⟨_,_⟩ - field - p : P - q : Q - - infixr 10 _∧_ - infixr 11 _∨_ - - -- ∧ elimination - proj₁ : {P Q : Prop} → P ∧ Q → P - proj₁ pq = _∧_.p pq - proj₂ : {P Q : Prop} → P ∧ Q → Q - proj₂ pq = _∧_.q pq - - -- ¬ is a shorthand for « → ⊥ » - ¬ : Prop → Prop - ¬ P = P → ⊥ - - -- ⊥ elimination - case⊥ : {P : Prop} → ⊥ → P - case⊥ () - - -- ∨ elimination - dis : {P Q S : Prop} → (P ∨ Q) → (P → S) → (Q → S) → S - dis (inj₁ p) ps qs = ps p - dis (inj₂ q) ps qs = qs q - - - -- ⇔ shorthand - _⇔_ : Prop → Prop → Prop - P ⇔ Q = (P → Q) ∧ (Q → P) diff --git a/PropUtil.agda b/PropUtil.agda index 69d105c..99b77d2 100644 --- a/PropUtil.agda +++ b/PropUtil.agda @@ -44,3 +44,9 @@ module PropUtil where -- ⇔ shorthand _⇔_ : Prop → Prop → Prop P ⇔ Q = (P → Q) ∧ (Q → P) + + + -- Syntactic sugar for writing applications + infixr 200 _$_ + _$_ : {T U : Prop} → (T → U) → T → U + h $ t = h t diff --git a/PropositionalKripke.agda b/PropositionalKripke.agda index 574f2c8..32a4639 100644 --- a/PropositionalKripke.agda +++ b/PropositionalKripke.agda @@ -58,8 +58,8 @@ module PropositionalKripke (PV : Set) where {- Soundness -} ⟦_⟧ : Γ ⊢ F → Γ ⊫ F - ⟦ zero ⟧ = proj₁ - ⟦ next p ⟧ = λ x → ⟦ p ⟧ (proj₂ x) + ⟦ zero zero∈ ⟧ wΓ = proj₁ wΓ + ⟦ zero (next∈ h) ⟧ wΓ = ⟦ zero h ⟧ (proj₂ wΓ) ⟦ lam p ⟧ = λ wΓ w≤ w'A → ⟦ p ⟧ ⟨ w'A , mon⊩ᶜ w≤ wΓ ⟩ ⟦ app p p₁ ⟧ wΓ = ⟦ p ⟧ wΓ refl≤ (⟦ p₁ ⟧ wΓ) @@ -81,21 +81,21 @@ module PropositionalKripke (PV : Set) where mon⊩ = λ ba bx → halftran⊢⁺ ba bx } open Kripke UK - + -- Now we can prove that ⊩ᶠ and ⊢ act in the same way ⊩ᶠ→⊢ : {F : Form} → {Γ : Con} → Γ ⊩ᶠ F → Γ ⊢ F ⊢→⊩ᶠ : {F : Form} → {Γ : Con} → Γ ⊢ F → Γ ⊩ᶠ F ⊢→⊩ᶠ {Var x} h = h - ⊢→⊩ᶠ {F ⇒ F₁} h {Γ'} iq hF = ⊢→⊩ᶠ {F₁} (app {Γ'} {F} {F₁} (lam (app (halftran⊢⁺ (addhyp⊢⁺ iq) h) zero)) (⊩ᶠ→⊢ hF)) + ⊢→⊩ᶠ {F ⇒ F₁} h {Γ'} iq hF = ⊢→⊩ᶠ {F₁} (app {Γ'} {F} {F₁} (lam (app (halftran⊢⁺ (addhyp⊢⁺ (right∈* refl∈*) iq) h) (zero zero∈))) (⊩ᶠ→⊢ hF)) ⊩ᶠ→⊢ {Var x} h = h - ⊩ᶠ→⊢ {F ⇒ F₁} {Γ} h = lam (⊩ᶠ→⊢ (h (addhyp⊢⁺ refl⊢⁺) (⊢→⊩ᶠ {F} {F ∷ Γ} zero))) + ⊩ᶠ→⊢ {F ⇒ F₁} {Γ} h = lam (⊩ᶠ→⊢ (h (addhyp⊢⁺ (right∈* refl∈*) refl⊢⁺) (⊢→⊩ᶠ {F} {F ∷ Γ} (zero zero∈)))) -- Finally, we can deduce completeness of the Kripke model completeness : {F : Form} → [] ⊫ F → [] ⊢ F completeness {F} ⊫F = ⊩ᶠ→⊢ (⊫F tt) module NormalizationProof where - + -- First we define the Universal model with (⊢⁰⁺)⁻¹ as world order -- It is slightly different from the last Model, but proofs are the same UK⁰ : Kripke @@ -119,7 +119,7 @@ module PropositionalKripke (PV : Set) where ⊢→⊩ᶠ {Var x} h = h ⊢→⊩ᶠ {F ⇒ F₁} h {Γ'} iq hF = ⊢→⊩ᶠ {F₁} (app {Γ'} {F} {F₁} (halftran⊢⁰⁺⁰ iq h) (⊩ᶠ→⊢ hF)) ⊩ᶠ→⊢ {Var x} h = neu⁰ h - ⊩ᶠ→⊢ {F ⇒ F₁} {Γ} h = lam (⊩ᶠ→⊢ (h (addhyp⊢⁰⁺ refl⊢⁰⁺) (⊢→⊩ᶠ {F} {F ∷ Γ} zero))) + ⊩ᶠ→⊢ {F ⇒ F₁} {Γ} h = lam (⊩ᶠ→⊢ (h (addhyp⊢⁰⁺ (right∈* refl∈*) refl⊢⁰⁺) (⊢→⊩ᶠ {F} {F ∷ Γ} (zero zero∈)))) module OtherProofs where @@ -132,16 +132,34 @@ module PropositionalKripke (PV : Set) where -- We can also use the relation ⊢⁰⁺, which is compatible with ⊢⁰ and ⊢* -- -> See module NormalizationProof - + - {- Renamings -} - - {- Weakening anywhere, order preserving, duplication authorized -} - - {- Weakening anywhere, no duplication, order preserving -} + {- Renamings : ∈* -} + UK∈* : Kripke + UK∈* = record { + Worlds = Con; + _≤_ = _∈*_; + refl≤ = refl∈*; + tran≤ = tran∈*; + _⊩_ = λ Γ x → Γ ⊢ Var x; + mon⊩ = λ x x₁ → addhyp⊢ x x₁ + } + {- + {- Weakening anywhere, order preserving, duplication authorized : ⊂⁺ -} + UK⊂⁺ : Kripke + UK⊂⁺ = record { + Worlds = Con; + _≤_ = _⊂⁺_; + refl≤ = refl⊂⁺; + tran≤ = tran⊂⁺; + _⊩_ = λ Γ x → Γ ⊢ Var x; + mon⊩ = λ x x₁ → addhyp⊢ x x₁ + } + -} + {- Weakening anywhere, no duplication, order preserving : ⊂ -} - {- Weakening at the end -} + {- Weakening at the end : ⊆-} -- This is exactly our relation ⊆ diff --git a/PropositionalKripkeGeneral.agda b/PropositionalKripkeGeneral.agda new file mode 100644 index 0000000..3796b1e --- /dev/null +++ b/PropositionalKripkeGeneral.agda @@ -0,0 +1,157 @@ +{-# OPTIONS --prop #-} + +module PropositionalKripkeGeneral (PV : Set) where + + open import ListUtil + open import PropUtil + open import PropositionalLogic PV using (Form; Var; _⇒_; Con) + + open import PropositionalKripke PV using (Kripke) + + record Preorder (T : Set₀) : Set₁ where + constructor order + field + _≤_ : T → T → Prop + refl≤ : {a : T} → a ≤ a + tran≤ : {a b c : T} → a ≤ b → b ≤ c → a ≤ c + + [_]ᵒᵖ : {T : Set₀} → Preorder T → Preorder T + [_]ᵒᵖ o = order (λ a b → (Preorder._≤_ o) b a) (Preorder.refl≤ o) (λ h₁ h₂ → (Preorder.tran≤ o) h₂ h₁) + + record NormalAndNeutral : Set₁ where + field + _⊢⁰_ : Con → Form → Prop + _⊢*_ : Con → Form → Prop + zero : {Γ : Con} → {F : Form} → (F ∷ Γ) ⊢⁰ F + app : {Γ : Con} → {F G : Form} → Γ ⊢⁰ (F ⇒ G) → Γ ⊢* F → Γ ⊢⁰ G + neu⁰ : {Γ : Con} → {x : PV} → Γ ⊢⁰ Var x → Γ ⊢* Var x + lam : {Γ : Con} → {F G : Form} → (F ∷ Γ) ⊢* G → Γ ⊢* (F ⇒ G) + + record NormalizationFrame : Set₁ where + field + o : Preorder Con + nn : NormalAndNeutral + retro : {Γ Δ : Con} → {F : Form} → (Preorder._≤_ o) Γ Δ → (Preorder._≤_ o) Γ (F ∷ Δ) + ⊢tran : {Γ Δ : Con} → {F : Form} → (Preorder._≤_ o) Γ Δ → (NormalAndNeutral._⊢⁰_ nn) Γ F → (NormalAndNeutral._⊢⁰_ nn) Δ F + + open Preorder o + open NormalAndNeutral nn + + all : Con → PV → Prop + all Γ x = ⊤ + + UK : Kripke + UK = record { + Worlds = Con; + _≤_ = _≤_; + refl≤ = refl≤; + tran≤ = tran≤; + _⊩_ = λ Γ x → Γ ⊢⁰ Var x; + mon⊩ = λ Γ h → ⊢tran Γ h + } + + open Kripke UK + + -- q is quote, u is unquote + q : {F : Form} → {Γ : Con} → Γ ⊩ᶠ F → Γ ⊢* F + u : {F : Form} → {Γ : Con} → Γ ⊢⁰ F → Γ ⊩ᶠ F + + u {Var x} h = h + u {F ⇒ F₁} h {Γ'} iq hF = u {F₁} (app {Γ'} {F} {F₁} (⊢tran iq h) (q hF)) + q {Var x} h = neu⁰ h + q {F ⇒ F₁} {Γ} h = lam (q (h (retro (Preorder.refl≤ o)) (u {F} {F ∷ Γ} zero))) + + + + + module NormalizationTests where + + {- Now using our records -} + open import PropositionalLogic PV hiding (Form; Var; _⇒_; Con) + + + ClassicNN : NormalAndNeutral + ClassicNN = record + { + _⊢⁰_ = _⊢⁰_ ; + _⊢*_ = _⊢*_ ; + zero = zero zero∈ ; + app = app ; + neu⁰ = neu⁰ ; + lam = lam + } + + BiggestNN : NormalAndNeutral + BiggestNN = record + { + _⊢⁰_ = _⊢_ ; + _⊢*_ = _⊢_ ; + zero = zero zero∈ ; + app = app ; + neu⁰ = λ x → x ; + lam = lam + } + + PO⊢⁺ = [ order {Con} _⊢⁺_ refl⊢⁺ tran⊢⁺ ]ᵒᵖ + PO⊢⁰⁺ = [ order {Con} _⊢⁰⁺_ refl⊢⁰⁺ tran⊢⁰⁺ ]ᵒᵖ + PO∈* = order {Con} _∈*_ refl∈* tran∈* + PO⊂⁺ = order {Con} _⊂⁺_ refl⊂⁺ tran⊂⁺ + PO⊂ = order {Con} _⊂_ refl⊂ tran⊂ + PO⊆ = order {Con} _⊆_ refl⊆ tran⊆ + + -- Completeness Proofs + Frame⊢ : NormalizationFrame + Frame⊢ = record + { + o = PO⊢⁺ ; + nn = BiggestNN ; + retro = λ s → addhyp⊢⁺ (right∈* refl∈*) s ; + ⊢tran = halftran⊢⁺ + } + + Frame⊢⁰ : NormalizationFrame + Frame⊢⁰ = record + { + o = PO⊢⁰⁺ ; + nn = ClassicNN ; + retro = λ s → addhyp⊢⁰⁺ (right∈* refl∈*) s ; + ⊢tran = halftran⊢⁰⁺⁰ + } + + Frame∈* : NormalizationFrame + Frame∈* = record + { + o = PO∈* ; + nn = ClassicNN ; + retro = right∈* ; + ⊢tran = λ s h → halftran⊢⁰⁺⁰ (mon∈*⊢⁰⁺ s) h + } + + Frame⊂⁺ : NormalizationFrame + Frame⊂⁺ = record + { + o = PO⊂⁺ ; + nn = ClassicNN ; + retro = next⊂⁺ ; + ⊢tran = λ s h → halftran⊢⁰⁺⁰ (mon∈*⊢⁰⁺ $ ⊂⁺→∈* s) h + } + + Frame⊂ : NormalizationFrame + Frame⊂ = record + { + o = PO⊂ ; + nn = ClassicNN ; + retro = next⊂ ; + ⊢tran = λ s h → halftran⊢⁰⁺⁰ (mon∈*⊢⁰⁺ $ ⊂⁺→∈* $ ⊂→⊂⁺ s) h + } + + Frame⊆ : NormalizationFrame + Frame⊆ = record + { + o = PO⊆ ; + nn = ClassicNN ; + retro = next⊆ ; + ⊢tran = λ s h → halftran⊢⁰⁺⁰ (mon∈*⊢⁰⁺ $ ⊂⁺→∈* $ ⊂→⊂⁺ $ ⊆→⊂ s) h + } + + diff --git a/Readme.agda b/Readme.agda index ca1e730..6af3a4e 100644 --- a/Readme.agda +++ b/Readme.agda @@ -12,7 +12,7 @@ open import PropositionalLogic String -- Here is an example of a propositional formula and its proof -- The formula is (Q → R) → (P → Q) → P → R d-C : [] ⊢ ((Var "Q") ⇒ (Var "R")) ⇒ ((Var "P") ⇒ (Var "Q")) ⇒ (Var "P") ⇒ (Var "R") -d-C = lam (lam (lam (app (next (next zero)) (app (next zero) zero)))) +d-C = lam (lam (lam (app (zero $ next∈ $ next∈ zero∈) (app (zero $ next∈ zero∈) (zero zero∈))))) -- We can with the basic interpretation ⟦_⟧ prove that some formulæ are not provable -- For example, we can disprove (P → Q) → P 's provability as we can construct an @@ -115,15 +115,39 @@ module PierceDisproof where PierceNotProvable h = Pierce⊥w₁ (⟦ h ⟧ {w₁} tt) - - - - - - - - - +module CompletenessAndNormalization where + -- With Kripke models, we can even prove completeness + -- Using the Universal Kripke Model + + completenessQuote = CompletenessProof.⊩ᶠ→⊢ + completenessUnquote = CompletenessProof.⊢→⊩ᶠ + + -- With a slightly different universal model (using normal and neutral forms), + -- we can make a normalization proof + normalizationQuote = NormalizationProof.⊩ᶠ→⊢ + normalizationUnquote = NormalizationProof.⊢→⊩ᶠ + + -- This normalization proof has been made in the biggest Kripke model possible + -- that is, the one using the relation ⊢⁰⁺ + -- But we can also prove it with tighter relations: ∈*, ⊂⁺, ⊂, ⊆ + + -- As all those proofs are really similar, we created a NormalizationFrame structure + -- that computes most of the proof with only a few lemmas + open import PropositionalKripkeGeneral String + + -- We now have access to quote and unquote functions with this + u1 = NormalizationFrame.u NormalizationTests.Frame⊢ + q1 = NormalizationFrame.q NormalizationTests.Frame⊢ + u2 = NormalizationFrame.u NormalizationTests.Frame⊢⁰ + q2 = NormalizationFrame.q NormalizationTests.Frame⊢⁰ + u3 = NormalizationFrame.u NormalizationTests.Frame∈* + q3 = NormalizationFrame.q NormalizationTests.Frame∈* + u4 = NormalizationFrame.u NormalizationTests.Frame⊂⁺ + q4 = NormalizationFrame.q NormalizationTests.Frame⊂⁺ + u5 = NormalizationFrame.u NormalizationTests.Frame⊂ + q5 = NormalizationFrame.q NormalizationTests.Frame⊂ + u6 = NormalizationFrame.u NormalizationTests.Frame⊆ + q6 = NormalizationFrame.q NormalizationTests.Frame⊆