Friedman’s A-translation
1992
-- Mechanised by Miëtek Bak -- thanks to András, Ambrus, ames, drvink, Jesper, ncf, and roconnor -- first-order predicate logic with one sort (naturals) and one predicate (equality) -- variant with first-order structures for renaming and substitution {-# OPTIONS --rewriting #-} module mi.Selinger1992 where open import mi.FOL public ---------------------------------------------------------------------------------------------------- -- TODO: statement of theorem 1 ---------------------------------------------------------------------------------------------------- -- lemma 2 lem2 : ∀ {Þ k} {Γ : Fm§ k} {A} → Þ / Γ ⊢ A → PA / Γ ⊢ A lem2 (‵var i) = ‵var i lem2 (‵lam d) = ‵lam (lem2 d) lem2 (d ‵$ e) = lem2 d ‵$ lem2 e lem2 (‵pair d e) = ‵pair (lem2 d) (lem2 e) lem2 (‵fst d) = ‵fst (lem2 d) lem2 (‵snd d) = ‵snd (lem2 d) lem2 (‵left d) = ‵left (lem2 d) lem2 (‵right d) = ‵right (lem2 d) lem2 (‵either c d e) = ‵either (lem2 c) (lem2 d) (lem2 e) lem2 (‵all refl d) = ‵all refl (lem2 d) lem2 (‵unall t refl d) = ‵unall t refl (lem2 d) lem2 (‵ex t refl d) = ‵ex t refl (lem2 d) lem2 (‵letex refl refl d e) = ‵letex refl refl (lem2 d) (lem2 e) lem2 (‵abortHA d) = ‵abort (lem2 d) lem2 (‵magicPA d) = ‵magicPA (lem2 d) lem2 ‵refl = ‵refl lem2 (‵sym d) = ‵sym (lem2 d) lem2 (‵trans d e) = ‵trans (lem2 d) (lem2 e) lem2 (‵cong f i refl refl d) = ‵cong f i refl refl (lem2 d) lem2 ‵dis = ‵dis lem2 (‵inj d) = ‵inj (lem2 d) lem2 (‵ind refl refl d e) = ‵ind refl refl (lem2 d) (lem2 e) lem2 (‵proj i refl) = ‵proj i refl lem2 (‵comp g φ refl) = ‵comp g φ refl lem2 (‵rec f g) = ‵rec f g ---------------------------------------------------------------------------------------------------- -- quantifier-free formulas data IsQFree {k} : Fm k → Set where _‵⊃_ : ∀ {A B} (p : IsQFree A) (q : IsQFree B) → IsQFree (A ‵⊃ B) _‵∧_ : ∀ {A B} (p : IsQFree A) (q : IsQFree B) → IsQFree (A ‵∧ B) _‵∨_ : ∀ {A B} (p : IsQFree A) (q : IsQFree B) → IsQFree (A ‵∨ B) ‵⊥ : IsQFree ‵⊥ _‵=_ : ∀ {t u} → IsQFree (t ‵= u) -- TODO: lemma 3 -- module _ where -- open =-Reasoning -- -- lem3 : ∀ {Þ k} {Γ : Fm§ k} (A : Fm k) {{_ : IsQFree A}} → Σ (Prim k) λ f → -- Þ / Γ ⊢ A ‵⫗ ‵fun f (tab ‵var) ‵= 𝟘 -- lem3 (A ‵⊃ B) = {!!} -- lem3 (A ‵∧ B) = {!!} -- lem3 (A ‵∨ B) = {!!} -- lem3 ‵⊥ = sig -- (ƒconst 1) -- (‵pair -- (‵lam (abort 0)) -- (‵lam (‵dis ‵$ (‵lam goal) ‵$ 0))) -- where -- goal : ∀ {Þ k} {Γ : Fm§ k} → -- Þ / Γ , ‵fun (ƒconst 1) (tab ‵var) ‵= 𝟘 ⊢ 𝕊 𝟘 ‵= 𝟘 -- goal = begin -- 𝕊 𝟘 -- =⟨⟩ -- ‵fun suc (∙ , ‵fun zero ∙) -- =⟨ ‵cong suc zero refl refl -- (begin -- ‵fun zero ∙ -- =˘⟨ ‵comp zero ∙ refl ⟩ -- ‵fun (comp zero ∙) (tab ‵var) -- ∎) -- ⟩ -- ‵fun suc (∙ , ‵fun (comp zero ∙) (tab ‵var)) -- =˘⟨ ‵comp suc ((∙ , comp zero ∙)) refl ⟩ -- ‵fun (comp suc (∙ , comp zero ∙)) (tab ‵var) -- =⟨⟩ -- ‵fun (ƒconst 1) (tab ‵var) -- =⟨ 0 ⟩ -- 𝟘 -- ∎ -- lem3 (t ‵= u) = {!!} ---------------------------------------------------------------------------------------------------- -- Π⁰₂ class of formulas -- TODO: definition of Π⁰₂ -- TODO: lemma 4 ---------------------------------------------------------------------------------------------------- -- double negation translation _° : ∀ {k} → Fm k → Fm k (A ‵⊃ B) ° = A ° ‵⊃ B ° (A ‵∧ B) ° = A ° ‵∧ B ° (A ‵∨ B) ° = ‵¬ ‵¬ (A ° ‵∨ B °) (‵∀ A) ° = ‵∀ A ° (‵∃ A) ° = ‵¬ ‵¬ (‵∃ A °) ‵⊥ ° = ‵⊥ (t ‵= u) ° = ‵¬ ‵¬ (t ‵= u) _°§ : ∀ {k} → Fm§ k → Fm§ k ∙ °§ = ∙ (Γ , A) °§ = Γ °§ , A ° -- TODO: interactions between DNT and renaming/substitution module _ where postulate TODO1 : ∀ {k} {A : Fm (suc k)} {t} → A ° [ t /0]Fm ≡ A [ t /0]Fm ° -- TODO1 = {!!} postulate TODO2 : ∀ {Þ k} {Γ : Fm§ k} {A} → Þ / wkFm§ Γ °§ ⊢ A → Þ / wkFm§ (Γ °§) ⊢ A -- TODO2 = {!!} postulate TODO3 : ∀ {Þ k} {Γ : Fm§ k} {A t} → Þ / Γ ⊢ A [ t /0]Fm ° → Þ / Γ ⊢ A ° [ t /0]Fm -- TODO3 = {!!} postulate TODO4 : ∀ {Þ k} {Γ : Fm§ k} {A t} → Þ / Γ ⊢ ‵∀ (A ° ‵⊃ wkFm A [ t /1]Fm °) → Þ / Γ ⊢ ‵∀ (A ° ‵⊃ wkFm (A °) [ t /1]Fm) -- TODO4 = {!!} postulate TODO5 : ∀ {Þ k} {Γ : Fm§ k} {A C} → Þ / wkFm§ Γ °§ , A ° ⊢ wkFm C ° → Þ / wkFm§ (Γ °§) , A ° ⊢ wkFm (C °) -- TODO5 = {!!} -- TODO: lemma 5 module _ where open ⫗-Reasoning lem5-1 : ∀ {k} {Γ : Fm§ k} {A} → PA / Γ ⊢ A ° ‵⫗ A lem5-1 {A = A ‵⊃ B} = ‵cong⊃ lem5-1 lem5-1 lem5-1 {A = A ‵∧ B} = ‵cong∧ lem5-1 lem5-1 lem5-1 {A = A ‵∨ B} = begin (A ‵∨ B) ° ⫗⟨ ‵dn ⟩ A ° ‵∨ B ° ⫗⟨ ‵cong∨ lem5-1 lem5-1 ⟩ A ‵∨ B ∎ lem5-1 {A = ‵∀ A} = ‵cong∀ lem5-1 lem5-1 {A = ‵∃ A} = begin (‵∃ A) ° ⫗⟨ ‵dn ⟩ ‵∃ A ° ⫗⟨ ‵cong∃ lem5-1 ⟩ ‵∃ A ∎ lem5-1 {A = ‵⊥} = ⫗refl lem5-1 {A = t ‵= u} = ‵dn lem5-2 : ∀ {Þ k} {Γ : Fm§ k} {A} → Þ / Γ ⊢ ‵¬ ‵¬ (A °) ‵⊃ A ° lem5-2 {A = A ‵⊃ B} = ‵lam (‵lam (lem5-2 ‵$ ‵lam (2 ‵$ ‵lam (1 ‵$ 0 ‵$ 2)))) lem5-2 {A = A ‵∧ B} = ‵lam (‵pair (lem5-2 ‵$ ‵lam (1 ‵$ ‵lam (1 ‵$ ‵fst 0))) (lem5-2 ‵$ ‵lam (1 ‵$ ‵lam (1 ‵$ ‵snd 0)))) lem5-2 {A = A ‵∨ B} = ‵lam (‵join 0) lem5-2 {A = ‵∀ A} = ‵lam (‵all refl (lem5-2 ‵$ ‵lam (1 ‵$ ‵lam (1 ‵$ ‵unall (‵tvar 0) (idcutFm (A °)) 0)))) lem5-2 {A = ‵∃ A} = ‵lam (‵join 0) lem5-2 {A = ‵⊥} = ‵lam (0 ‵$ ⊃id) lem5-2 {A = t ‵= u} = ‵lam (‵join 0) lem5-3∋ : ∀ {k} {Γ : Fm§ k} {A} → Γ ∋ A → Γ °§ ∋ A ° lem5-3∋ zero = zero lem5-3∋ (suc i) = suc (lem5-3∋ i) -- TODO: why does rewriting blow up constraint solver here? module _ where lem5-3 : ∀ {Þ k} {Γ : Fm§ k} {A} → PA / Γ ⊢ A → Þ / Γ °§ ⊢ A ° lem5-3 (‵var i) = ‵var (lem5-3∋ i) lem5-3 (‵lam d) = ‵lam (lem5-3 d) lem5-3 (d ‵$ e) = lem5-3 d ‵$ lem5-3 e lem5-3 (‵pair d e) = ‵pair (lem5-3 d) (lem5-3 e) lem5-3 (‵fst d) = ‵fst (lem5-3 d) lem5-3 (‵snd d) = ‵snd (lem5-3 d) lem5-3 (‵left d) = ‵return (‵left (lem5-3 d)) lem5-3 (‵right d) = ‵return (‵right (lem5-3 d)) lem5-3 (‵either c d e) = lem5-2 ‵$ (lem5-3 c ‵>>= ‵lam (‵either 0 (‵return (‵exch (wk (lem5-3 d)))) (‵return (‵exch (wk (lem5-3 e)))))) lem5-3 {Γ = Γ} (‵all refl d) = ‵all refl (TODO2 {Γ = Γ} (lem5-3 d)) lem5-3 (‵unall t refl d) = ‵unall t TODO1 (lem5-3 d) lem5-3 (‵ex t refl d) = ‵return (‵ex t TODO1 (lem5-3 d)) lem5-3 {Γ = Γ} (‵letex {C = C} refl refl d e) = lem5-2 ‵$ (lem5-3 d ‵>>= ‵lam (‵letex refl refl 0 (‵return (‵exch (wk (TODO5 {Γ = Γ} {C = C} (lem5-3 e))))))) lem5-3 (‵magicPA d) = lem5-2 ‵$ ‵lam (lem5-3 d) lem5-3 ‵refl = ‵return ‵refl lem5-3 (‵sym d) = lem5-3 d ‵>>= ‵lam (‵return (‵sym 0)) lem5-3 (‵trans d e) = lem5-3 d ‵>>= ‵lam (wk (lem5-3 e) ‵>>= ‵lam (‵return (‵trans 1 0))) lem5-3 (‵cong f i refl refl d) = lem5-3 d ‵>>= ‵lam (‵return (‵cong f i refl refl 0)) lem5-3 ‵dis = ‵return ‵dis lem5-3 (‵inj d) = lem5-3 d ‵>>= ‵lam (‵return (‵inj 0)) lem5-3 (‵ind refl refl d e) = ‵ind refl refl (TODO3 (lem5-3 d)) (TODO4 (lem5-3 e)) lem5-3 (‵proj i refl) = ‵return (‵proj i refl) lem5-3 (‵comp g φ refl) = ‵return (‵comp g φ refl) lem5-3 (‵rec {t = t} f g) = ‵pair (‵return (‵fst (‵rec {t = t} f g))) (‵return (‵snd (‵rec f g))) -- "Note that the converse of 3 trivially holds wih 1." lem5-3⁻¹ : ∀ {Þ k} {Γ : Fm§ k} {A} → Þ / Γ °§ ⊢ A ° → PA / Γ ⊢ A lem5-3⁻¹ d = aux (‵fst lem5-1 ‵$ lem2 d) where aux : ∀ {k} {Γ : Fm§ k} {A} → PA / Γ °§ ⊢ A → PA / Γ ⊢ A aux {Γ = ∙} d = d aux {Γ = Γ , C} d = wk (aux (‵lam d)) ‵$ (‵snd lem5-1 ‵$ 0) -- TODO: "A counterexample for 4 is ¬∀y.A[y/x₀]." -- lem5-4 : ∀ {k} {Γ : Fm§ k} → ¬ (∀ {A} → HA / Γ , ‵¬ (‵∀ A) ⊢ (‵¬ (‵∀ A)) °) -- lem5-4 = {!!} ---------------------------------------------------------------------------------------------------- -- A-translation _ᴬ⟨_⟩ : ∀ {k} → Fm k → Fm k → Fm k (A ‵⊃ B) ᴬ⟨ T ⟩ = A ᴬ⟨ T ⟩ ‵⊃ B ᴬ⟨ T ⟩ (A ‵∧ B) ᴬ⟨ T ⟩ = A ᴬ⟨ T ⟩ ‵∧ B ᴬ⟨ T ⟩ (A ‵∨ B) ᴬ⟨ T ⟩ = A ᴬ⟨ T ⟩ ‵∨ B ᴬ⟨ T ⟩ (‵∀ A) ᴬ⟨ T ⟩ = ‵∀ A ᴬ⟨ wkFm T ⟩ (‵∃ A) ᴬ⟨ T ⟩ = ‵∃ A ᴬ⟨ wkFm T ⟩ ‵⊥ ᴬ⟨ T ⟩ = T (t ‵= u) ᴬ⟨ T ⟩ = (t ‵= u) ‵∨ T _ᴬ⟨_⟩§ : ∀ {k} → Fm§ k → Fm k → Fm§ k ∙ ᴬ⟨ T ⟩§ = ∙ (Γ , A) ᴬ⟨ T ⟩§ = Γ ᴬ⟨ T ⟩§ , A ᴬ⟨ T ⟩ -- TODO: interactions between A-translation and renaming/substitution module _ where postulate TODO6 : ∀ {k} {A : Fm (suc k)} {T t} → (A ᴬ⟨ wkFm T ⟩) [ t /0]Fm ≡ (A [ t /0]Fm) ᴬ⟨ T ⟩ -- TODO6 = ? -- TODO: lemma 6 module _ where open ≡ -- non-constructive lemma aux1 : ∀ {k} {Γ : Fm§ k} {A B C} → PA / Γ ⊢ (A ‵∨ C) ‵⊃ (B ‵∨ C) ‵⫗ (A ‵⊃ B) ‵∨ C aux1 = ‵pair (‵lam (‵either ‵em (‵right 0) (‵left (‵lam (‵either (2 ‵$ (‵left 0)) 0 (‵abort (2 ‵$ 0))))))) (‵lam (‵lam (‵either 0 (‵either 2 (‵left (0 ‵$ 1)) (‵right 0)) (‵right 0)))) aux2 : ∀ {Þ k} {Γ : Fm§ k} {A B C} → Þ / Γ ⊢ (A ‵∨ C) ‵∧ (B ‵∨ C) ‵⫗ (A ‵∧ B) ‵∨ C aux2 = ‵pair (‵lam (‵either (‵fst 0) (‵either (‵snd 1) (‵left (‵pair 1 0)) (‵right 0)) (‵right 0))) (‵lam (‵either 0 (‵pair (‵left (‵fst 0)) (‵left (‵snd 0))) (‵pair (‵right 0) (‵right 0)))) aux3 : ∀ {Þ k} {Γ : Fm§ k} {A B C} → Þ / Γ ⊢ (A ‵∨ C) ‵∨ (B ‵∨ C) ‵⫗ (A ‵∨ B) ‵∨ C aux3 = ‵pair (‵lam (‵either 0 (‵either 0 (‵left (‵left 0)) (‵right 0)) (‵either 0 (‵left (‵right 0)) (‵right 0)))) (‵lam (‵either 0 (‵either 0 (‵left (‵left 0)) (‵right (‵left 0))) (‵left (‵right 0)))) -- could also be ‵right -- non-constructive lemma aux4 : ∀ {k} {Γ : Fm§ k} {A C} → PA / Γ ⊢ ‵∀ (A ‵∨ wkFm C) ‵⫗ ‵∀ A ‵∨ C aux4 {A = A} {C} = ‵pair (‵lam (‵either ‵em (‵right 0) (‵left (‵all refl (‵either (‵unall (‵tvar 0) (idcutFm (A ‵∨ wkFm C)) 1) 0 (‵abort (1 ‵$ 0))))))) (‵lam (‵either 0 (‵all refl (‵left (‵unall (‵tvar 0) (idcutFm A) 0))) (‵all refl (‵right 0)))) aux5 : ∀ {Þ k} {Γ : Fm§ k} {A C} → Þ / Γ ⊢ ‵∃ (A ‵∨ wkFm C) ‵⫗ ‵∃ A ‵∨ C aux5 {A = A} {C} = ‵pair (‵lam (‵letex refl refl 0 (‵either 0 (‵left (‵ex (‵tvar 0) (idcutFm A) 0)) (‵right 0)))) (‵lam (‵either 0 (‵letex refl refl 0 (‵ex (‵tvar 0) (_‵∨_ & idcutFm A ⊗ idcutFm (wkFm C)) (‵left 0))) (‵ex 𝟘 -- could also be any other natural ( (subFm (idTm§ , 𝟘) A ‵∨_) & ( eqsubFm idTm§ 𝟘 C ⋮ idsubFm C ) ) (‵right 0)))) aux6 : ∀ {Þ k} {Γ : Fm§ k} {C} → Þ / Γ ⊢ C ‵⫗ ‵⊥ ‵∨ C aux6 = ‵pair (‵lam (‵right 0)) (‵lam (‵either 0 (‵abort 0) 0)) module _ where open ⫗-Reasoning lem6-1 : ∀ {k} {Γ : Fm§ k} {A T} → PA / Γ ⊢ A ᴬ⟨ T ⟩ ‵⫗ A ‵∨ T lem6-1 {A = A ‵⊃ B} {T} = begin A ᴬ⟨ T ⟩ ‵⊃ B ᴬ⟨ T ⟩ ⫗⟨ ‵cong⊃ lem6-1 lem6-1 ⟩ (A ‵∨ T) ‵⊃ (B ‵∨ T) ⫗⟨ aux1 ⟩ (A ‵⊃ B) ‵∨ T ∎ lem6-1 {A = A ‵∧ B} {T} = begin A ᴬ⟨ T ⟩ ‵∧ B ᴬ⟨ T ⟩ ⫗⟨ ‵cong∧ lem6-1 lem6-1 ⟩ (A ‵∨ T) ‵∧ (B ‵∨ T) ⫗⟨ aux2 ⟩ (A ‵∧ B) ‵∨ T ∎ lem6-1 {A = A ‵∨ B} {T} = begin A ᴬ⟨ T ⟩ ‵∨ B ᴬ⟨ T ⟩ ⫗⟨ ‵cong∨ lem6-1 lem6-1 ⟩ (A ‵∨ T) ‵∨ (B ‵∨ T) ⫗⟨ aux3 ⟩ (A ‵∨ B) ‵∨ T ∎ lem6-1 {A = ‵∀ A} {T} = begin ‵∀ (A ᴬ⟨ wkFm T ⟩) ⫗⟨ ‵cong∀ lem6-1 ⟩ ‵∀ (A ‵∨ wkFm T) ⫗⟨ aux4 ⟩ ‵∀ A ‵∨ T ∎ lem6-1 {A = ‵∃ A} {T} = begin ‵∃ (A ᴬ⟨ wkFm T ⟩) ⫗⟨ ‵cong∃ lem6-1 ⟩ ‵∃ (A ‵∨ wkFm T) ⫗⟨ aux5 ⟩ ‵∃ A ‵∨ T ∎ lem6-1 {A = ‵⊥} {T} = aux6 lem6-1 {A = t ‵= u} {T} = ⫗refl -- lem6-2 : ∀ {Þ k} {Γ : Fm§ k} {A T} → Þ / Γ ⊢ T ‵⊃ A ᴬ⟨ T ⟩ -- lem6-2 {A = A ‵⊃ B} = ‵lam (‵lam (lem6-2 ‵$ 1)) -- function argument ignored -- lem6-2 {A = A ‵∧ B} = ‵lam (‵pair (lem6-2 ‵$ 0) (lem6-2 ‵$ 0)) -- lem6-2 {A = A ‵∨ B} = ‵lam (‵left (lem6-2 ‵$ 0)) -- could also be ‵right -- lem6-2 {A = ‵∀ A} = ‵lam (‵all refl (lem6-2 ‵$ 0)) -- lem6-2 {A = ‵∃ A} {T} = {!!} -- -- ‵lam (‵ex 𝟘 (TODO6 {A = A} {T}) (lem6-2 {A = A [ 𝟘 /0]Fm} ‵$ 0)) -- TODO: termination failure -- lem6-2 {A = ‵⊥} = ⊃id -- lem6-2 {A = t ‵= u} = ‵lam (‵right 0) -- -- lem6-3∋ : ∀ {k} {Γ : Fm§ k} {A T} → Γ ∋ A → Γ ᴬ⟨ T ⟩§ ∋ A ᴬ⟨ T ⟩ -- lem6-3∋ zero = zero -- lem6-3∋ (suc i) = suc (lem6-3∋ i) -- TODO: "The proof of 3 is a bit tricky where eigenvariable conditions are involved." -- lem6-3 : ∀ {Þ k} {Γ : Fm§ k} {A T} → Þ / Γ ⊢ A → Þ / Γ ᴬ⟨ T ⟩§ ⊢ A ᴬ⟨ T ⟩ -- lem6-3 (‵var i) = ‵var (lem6-3∋ i) -- lem6-3 (‵lam d) = ‵lam (lem6-3 d) -- lem6-3 (d ‵$ e) = lem6-3 d ‵$ lem6-3 e -- lem6-3 (‵pair d e) = ‵pair (lem6-3 d) (lem6-3 e) -- lem6-3 (‵fst d) = ‵fst (lem6-3 d) -- lem6-3 (‵snd d) = ‵snd (lem6-3 d) -- lem6-3 (‵left d) = ‵left (lem6-3 d) -- lem6-3 (‵right d) = ‵right (lem6-3 d) -- lem6-3 (‵either c d e) = ‵either (lem6-3 c) (lem6-3 d) (lem6-3 e) -- lem6-3 (‵all refl d) = {!!} -- lem6-3 (‵unall t refl d) = {!!} -- lem6-3 (‵ex t refl d) = {!!} -- lem6-3 (‵letex refl refl d e) = {!!} -- lem6-3 (‵abort d) = {!!} -- lem6-3 (‵magic d) = {!!} -- lem6-3 ‵refl = ‵left ‵refl -- lem6-3 (‵sym d) = ‵either (lem6-3 d) -- (‵left (‵sym 0)) -- (‵right 0) -- lem6-3 (‵trans d e) = ‵either (lem6-3 d) -- (‵either (wk (lem6-3 e)) -- (‵left (‵trans 1 0)) -- (‵right 0)) -- (‵right 0) -- lem6-3 (‵cong f i refl refl d) = {!!} -- lem6-3 ‵dis = {!!} -- lem6-3 (‵inj d) = {!!} -- lem6-3 (‵ind refl refl d e) = {!!} -- lem6-3 (‵proj i refl) = {!!} -- lem6-3 (‵comp g φ refl) = {!!} -- lem6-3 (‵rec f g) = {!!} -- TODO: "A counterexample for 4 is A = ¬¬T." -- lem6-4 : ∀ {k} {Γ : Fm§ k} → ¬ (∀ {T} → HA / Γ , ‵¬ ‵¬ T ⊢ (‵¬ ‵¬ T) ᴬ⟨ T ⟩) -- lem6-4 = {!!} ---------------------------------------------------------------------------------------------------- -- proof of theorem 1 -- TODO: lemma 7 -- TODO: corollary 8 -- TODO: theorem 1 ----------------------------------------------------------------------------------------------------
Lorem ipsum dolor sit amet, consectetur adipisicing elit, sed do eiusmod tempor incididunt ut labore et dolore magna aliqua. Ut enim ad minim veniam, quis nostrud exercitation ullamco laboris nisi ut aliquip ex ea commodo consequat. Duis aute irure dolor in reprehenderit in voluptate velit esse cillum dolore eu fugiat nulla pariatur. Excepteur sint occaecat cupidatat non proident, sunt in culpa qui officia deserunt mollit anim id est laborum.