Filters of lists of CrAnFieldOp

def FieldSpecification.createFilter {𝓕 : FieldSpecification} (φs : List 𝓕.CrAnFieldOp) : List 𝓕.CrAnFieldOp

Given a list of creation and annihilation states, the filtered list only containing the creation states. As a schematic example, for the list:

• [φ1c, φ1a, φ2c, φ2a] this will return [φ1c, φ2c].

Equations

• FieldSpecification.createFilter φs = List.filter (fun (φ : 𝓕.CrAnFieldOp) => decide (𝓕.crAnFieldOpToCreateAnnihilate φ = CreateAnnihilate.create)) φs

theorem FieldSpecification.createFilter_cons_create {𝓕 : FieldSpecification} {φ : 𝓕.CrAnFieldOp} (hφ : 𝓕.crAnFieldOpToCreateAnnihilate φ = CreateAnnihilate.create) (φs : List 𝓕.CrAnFieldOp) : createFilter (φ :: φs) = φ :: createFilter φs

theorem FieldSpecification.createFilter_cons_annihilate {𝓕 : FieldSpecification} {φ : 𝓕.CrAnFieldOp} (hφ : 𝓕.crAnFieldOpToCreateAnnihilate φ = CreateAnnihilate.annihilate) (φs : List 𝓕.CrAnFieldOp) : createFilter (φ :: φs) = createFilter φs

theorem FieldSpecification.createFilter_append {𝓕 : FieldSpecification} (φs φs' : List 𝓕.CrAnFieldOp) : createFilter (φs ++ φs') = createFilter φs ++ createFilter φs'

theorem FieldSpecification.createFilter_singleton_create {𝓕 : FieldSpecification} (φ : 𝓕.CrAnFieldOp) (hφ : 𝓕.crAnFieldOpToCreateAnnihilate φ = CreateAnnihilate.create) : createFilter [φ] = [φ]

theorem FieldSpecification.createFilter_singleton_annihilate {𝓕 : FieldSpecification} (φ : 𝓕.CrAnFieldOp) (hφ : 𝓕.crAnFieldOpToCreateAnnihilate φ = CreateAnnihilate.annihilate) : createFilter [φ] = []

def FieldSpecification.annihilateFilter {𝓕 : FieldSpecification} (φs : List 𝓕.CrAnFieldOp) : List 𝓕.CrAnFieldOp

Given a list of creation and annihilation states, the filtered list only containing the annihilation states. As a schematic example, for the list:

• [φ1c, φ1a, φ2c, φ2a] this will return [φ1a, φ2a].

Equations

• FieldSpecification.annihilateFilter φs = List.filter (fun (φ : 𝓕.CrAnFieldOp) => decide (𝓕.crAnFieldOpToCreateAnnihilate φ = CreateAnnihilate.annihilate)) φs

theorem FieldSpecification.annihilateFilter_cons_create {𝓕 : FieldSpecification} {φ : 𝓕.CrAnFieldOp} (hφ : 𝓕.crAnFieldOpToCreateAnnihilate φ = CreateAnnihilate.create) (φs : List 𝓕.CrAnFieldOp) : annihilateFilter (φ :: φs) = annihilateFilter φs

theorem FieldSpecification.annihilateFilter_cons_annihilate {𝓕 : FieldSpecification} {φ : 𝓕.CrAnFieldOp} (hφ : 𝓕.crAnFieldOpToCreateAnnihilate φ = CreateAnnihilate.annihilate) (φs : List 𝓕.CrAnFieldOp) : annihilateFilter (φ :: φs) = φ :: annihilateFilter φs

theorem FieldSpecification.annihilateFilter_append {𝓕 : FieldSpecification} (φs φs' : List 𝓕.CrAnFieldOp) : annihilateFilter (φs ++ φs') = annihilateFilter φs ++ annihilateFilter φs'

theorem FieldSpecification.annihilateFilter_singleton_create {𝓕 : FieldSpecification} (φ : 𝓕.CrAnFieldOp) (hφ : 𝓕.crAnFieldOpToCreateAnnihilate φ = CreateAnnihilate.create) : annihilateFilter [φ] = []

theorem FieldSpecification.annihilateFilter_singleton_annihilate {𝓕 : FieldSpecification} (φ : 𝓕.CrAnFieldOp) (hφ : 𝓕.crAnFieldOpToCreateAnnihilate φ = CreateAnnihilate.annihilate) : annihilateFilter [φ] = [φ]