Documentation

LeanPool.NFWeakPartition.Certificates.NAR4H5C093M3Part002Block001

Nominal proof certificates grouped in dependency order.

Certificates from AlphaSupport.NAR4H5C093M3Part002Stage1.

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb093_support_mem_0051 (r : SemanticCore.Var) :

r ∈ (SemanticCore.Class.cv r).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv r))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb093_support_mem_0056 (A : SemanticCore.Class) :

nb093AlphaDummy058 A ∈ (SemanticCore.Class.cv (nb093AlphaDummy058 A)).fv ∪ (SemanticCore.Class.cv (nb093AlphaDummy059 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb093_support_mem_0057 (A : SemanticCore.Class) :

nb093AlphaDummy058 A ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb093AlphaDummy064 A) (Compiler.CompactSourceSyntax.synWrex (nb093AlphaDummy065 A) (SemanticCore.Class.cv (nb093AlphaDummy058 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb093AlphaDummy064 A)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb093AlphaDummy065 A))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb093AlphaDummy064 A) (Compiler.CompactSourceSyntax.synWrex (nb093AlphaDummy065 A) (SemanticCore.Class.cv (nb093AlphaDummy059 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb093AlphaDummy064 A)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb093AlphaDummy065 A))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb093_support_mem_0058 (r : SemanticCore.Var) :

nb093AlphaDummy060 r ∈ (SemanticCore.Class.cv (nb093AlphaDummy060 r)).fv ∪ (SemanticCore.Class.cv (nb093AlphaDummy061 r)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb093_support_mem_0059 (r : SemanticCore.Var) :

nb093AlphaDummy060 r ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb093AlphaDummy066 r) (Compiler.CompactSourceSyntax.synWrex (nb093AlphaDummy067 r) (SemanticCore.Class.cv (nb093AlphaDummy060 r)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb093AlphaDummy066 r)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb093AlphaDummy067 r))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb093AlphaDummy066 r) (Compiler.CompactSourceSyntax.synWrex (nb093AlphaDummy067 r) (SemanticCore.Class.cv (nb093AlphaDummy061 r)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb093AlphaDummy066 r)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb093AlphaDummy067 r))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb093_support_mem_0060 (A : SemanticCore.Class) :

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb093_support_mem_0061 (r : SemanticCore.Var) :

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb093_support_mem_0062 (A : SemanticCore.Class) :

nb093AlphaDummy065 A ∈ (SemanticCore.Class.cv (nb093AlphaDummy065 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb093_support_mem_0063 (r : SemanticCore.Var) :

nb093AlphaDummy067 r ∈ (SemanticCore.Class.cv (nb093AlphaDummy067 r)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb093_support_mem_0066 (A : SemanticCore.Class) :

nb093AlphaDummy072 A ∈ (SemanticCore.Class.cv (nb093AlphaDummy072 A)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb093_support_mem_0067 (r : SemanticCore.Var) :

nb093AlphaDummy074 r ∈ (SemanticCore.Class.cv (nb093AlphaDummy074 r)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb093_support_mem_0068 (A : SemanticCore.Class) :

nb093AlphaDummy079 A ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb093AlphaDummy079 A)) (SemanticCore.Class.cv (nb093AlphaDummy080 A))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb093AlphaDummy079 A)) (SemanticCore.Class.cv (nb093AlphaDummy080 A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb093_support_mem_0069 (r : SemanticCore.Var) :

nb093AlphaDummy082 r ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb093AlphaDummy082 r)) (SemanticCore.Class.cv (nb093AlphaDummy083 r))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb093AlphaDummy082 r)) (SemanticCore.Class.cv (nb093AlphaDummy083 r))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb093_support_mem_0070 (A : SemanticCore.Class) :

nb093AlphaDummy079 A ∈ (SemanticCore.Class.cv (nb093AlphaDummy079 A)).fv ∪ (SemanticCore.Class.cv (nb093AlphaDummy080 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb093_support_mem_0071 (r : SemanticCore.Var) :

nb093AlphaDummy082 r ∈ (SemanticCore.Class.cv (nb093AlphaDummy082 r)).fv ∪ (SemanticCore.Class.cv (nb093AlphaDummy083 r)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb093_support_mem_0072 (A : SemanticCore.Class) :

nb093AlphaDummy080 A ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb093AlphaDummy079 A)) (SemanticCore.Class.cv (nb093AlphaDummy080 A))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb093AlphaDummy079 A)) (SemanticCore.Class.cv (nb093AlphaDummy080 A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb093_support_mem_0073 (r : SemanticCore.Var) :

nb093AlphaDummy083 r ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb093AlphaDummy082 r)) (SemanticCore.Class.cv (nb093AlphaDummy083 r))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb093AlphaDummy082 r)) (SemanticCore.Class.cv (nb093AlphaDummy083 r))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb093_support_mem_0074 (A : SemanticCore.Class) :

nb093AlphaDummy080 A ∈ (SemanticCore.Class.cv (nb093AlphaDummy079 A)).fv ∪ (SemanticCore.Class.cv (nb093AlphaDummy080 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb093_support_mem_0075 (r : SemanticCore.Var) :

nb093AlphaDummy083 r ∈ (SemanticCore.Class.cv (nb093AlphaDummy082 r)).fv ∪ (SemanticCore.Class.cv (nb093AlphaDummy083 r)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb093_support_mem_0076 (A : SemanticCore.Class) :

nb093AlphaDummy079 A ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb093AlphaDummy079 A))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb093AlphaDummy080 A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb093_support_mem_0077 (r : SemanticCore.Var) :

nb093AlphaDummy082 r ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb093AlphaDummy082 r))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb093AlphaDummy083 r))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb093_support_mem_0078 (A : SemanticCore.Class) :

nb093AlphaDummy079 A ∈ (SemanticCore.Class.cv (nb093AlphaDummy079 A)).fv ∪ (SemanticCore.Class.cv (nb093AlphaDummy079 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb093_support_mem_0079 (r : SemanticCore.Var) :

nb093AlphaDummy082 r ∈ (SemanticCore.Class.cv (nb093AlphaDummy082 r)).fv ∪ (SemanticCore.Class.cv (nb093AlphaDummy082 r)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb093_support_mem_0080 (A : SemanticCore.Class) :

nb093AlphaDummy080 A ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb093AlphaDummy079 A))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb093AlphaDummy080 A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb093_support_mem_0081 (r : SemanticCore.Var) :

nb093AlphaDummy083 r ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb093AlphaDummy082 r))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb093AlphaDummy083 r))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb093_support_mem_0082 (A : SemanticCore.Class) :

nb093AlphaDummy080 A ∈ (SemanticCore.Class.cv (nb093AlphaDummy080 A)).fv ∪ (SemanticCore.Class.cv (nb093AlphaDummy080 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb093_support_mem_0083 (r : SemanticCore.Var) :

nb093AlphaDummy083 r ∈ (SemanticCore.Class.cv (nb093AlphaDummy083 r)).fv ∪ (SemanticCore.Class.cv (nb093AlphaDummy083 r)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb093_support_mem_0084 (A : SemanticCore.Class) :

nb093AlphaDummy059 A ∈ (SemanticCore.Class.cv (nb093AlphaDummy058 A)).fv ∪ (SemanticCore.Class.cv (nb093AlphaDummy059 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb093_support_mem_0085 (A : SemanticCore.Class) :

nb093AlphaDummy059 A ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb093AlphaDummy064 A) (Compiler.CompactSourceSyntax.synWrex (nb093AlphaDummy065 A) (SemanticCore.Class.cv (nb093AlphaDummy058 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb093AlphaDummy064 A)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb093AlphaDummy065 A))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb093AlphaDummy064 A) (Compiler.CompactSourceSyntax.synWrex (nb093AlphaDummy065 A) (SemanticCore.Class.cv (nb093AlphaDummy059 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb093AlphaDummy064 A)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb093AlphaDummy065 A))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb093_support_mem_0086 (r : SemanticCore.Var) :

nb093AlphaDummy061 r ∈ (SemanticCore.Class.cv (nb093AlphaDummy060 r)).fv ∪ (SemanticCore.Class.cv (nb093AlphaDummy061 r)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb093_support_mem_0087 (r : SemanticCore.Var) :

nb093AlphaDummy061 r ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb093AlphaDummy066 r) (Compiler.CompactSourceSyntax.synWrex (nb093AlphaDummy067 r) (SemanticCore.Class.cv (nb093AlphaDummy060 r)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb093AlphaDummy066 r)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb093AlphaDummy067 r))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb093AlphaDummy066 r) (Compiler.CompactSourceSyntax.synWrex (nb093AlphaDummy067 r) (SemanticCore.Class.cv (nb093AlphaDummy061 r)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb093AlphaDummy066 r)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb093AlphaDummy067 r))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb093_support_mem_0088 (A : SemanticCore.Class) :

nb093AlphaDummy059 A ∈ (SemanticCore.Class.cab (nb093AlphaDummy064 A) (Compiler.CompactSourceSyntax.synWrex (nb093AlphaDummy065 A) (SemanticCore.Class.cv (nb093AlphaDummy059 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb093AlphaDummy064 A)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb093AlphaDummy065 A))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab (nb093AlphaDummy064 A) (Compiler.CompactSourceSyntax.synWrex (nb093AlphaDummy065 A) (SemanticCore.Class.cv (nb093AlphaDummy059 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb093AlphaDummy064 A)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb093AlphaDummy065 A))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb093_support_mem_0089 (r : SemanticCore.Var) :

nb093AlphaDummy061 r ∈ (SemanticCore.Class.cab (nb093AlphaDummy066 r) (Compiler.CompactSourceSyntax.synWrex (nb093AlphaDummy067 r) (SemanticCore.Class.cv (nb093AlphaDummy061 r)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb093AlphaDummy066 r)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb093AlphaDummy067 r))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab (nb093AlphaDummy066 r) (Compiler.CompactSourceSyntax.synWrex (nb093AlphaDummy067 r) (SemanticCore.Class.cv (nb093AlphaDummy061 r)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb093AlphaDummy066 r)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb093AlphaDummy067 r))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb093_support_mem_0090 (A : SemanticCore.Class) :

nb093AlphaDummy065 A ∈ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb093AlphaDummy065 A)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb093_support_mem_0091 (r : SemanticCore.Var) :

nb093AlphaDummy067 r ∈ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb093AlphaDummy067 r)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb093_support_mem_0092 (A : SemanticCore.Class) :

nb093AlphaDummy065 A ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb093AlphaDummy065 A))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb093AlphaDummy065 A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb093_support_mem_0093 (r : SemanticCore.Var) :

nb093AlphaDummy067 r ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb093AlphaDummy067 r))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb093AlphaDummy067 r))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb093_support_mem_0094 (A : SemanticCore.Class) :

nb093AlphaDummy059 A ∈ (SemanticCore.Class.cv (nb093AlphaDummy059 A)).fv ∪ (SemanticCore.Class.cv (nb093AlphaDummy058 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb093_support_mem_0095 (A : SemanticCore.Class) :

nb093AlphaDummy059 A ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb093AlphaDummy100 A) (Compiler.CompactSourceSyntax.synWrex (nb093AlphaDummy101 A) (SemanticCore.Class.cv (nb093AlphaDummy059 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb093AlphaDummy100 A)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb093AlphaDummy101 A))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb093AlphaDummy100 A) (Compiler.CompactSourceSyntax.synWrex (nb093AlphaDummy101 A) (SemanticCore.Class.cv (nb093AlphaDummy058 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb093AlphaDummy100 A)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb093AlphaDummy101 A))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb093_support_mem_0096 (r : SemanticCore.Var) :

nb093AlphaDummy061 r ∈ (SemanticCore.Class.cv (nb093AlphaDummy061 r)).fv ∪ (SemanticCore.Class.cv (nb093AlphaDummy060 r)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb093_support_mem_0097 (r : SemanticCore.Var) :

nb093AlphaDummy061 r ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb093AlphaDummy102 r) (Compiler.CompactSourceSyntax.synWrex (nb093AlphaDummy103 r) (SemanticCore.Class.cv (nb093AlphaDummy061 r)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb093AlphaDummy102 r)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb093AlphaDummy103 r))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb093AlphaDummy102 r) (Compiler.CompactSourceSyntax.synWrex (nb093AlphaDummy103 r) (SemanticCore.Class.cv (nb093AlphaDummy060 r)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb093AlphaDummy102 r)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb093AlphaDummy103 r))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb093_support_mem_0098 (A : SemanticCore.Class) :

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb093_support_mem_0099 (r : SemanticCore.Var) :

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb093_support_mem_0100 (A : SemanticCore.Class) :

nb093AlphaDummy101 A ∈ (SemanticCore.Class.cv (nb093AlphaDummy101 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb093_support_mem_0101 (r : SemanticCore.Var) :

nb093AlphaDummy103 r ∈ (SemanticCore.Class.cv (nb093AlphaDummy103 r)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb093_support_mem_0104 (A : SemanticCore.Class) :

nb093AlphaDummy108 A ∈ (SemanticCore.Class.cv (nb093AlphaDummy108 A)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb093_support_mem_0105 (r : SemanticCore.Var) :

nb093AlphaDummy110 r ∈ (SemanticCore.Class.cv (nb093AlphaDummy110 r)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb093_support_mem_0106 (A : SemanticCore.Class) :

nb093AlphaDummy115 A ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb093AlphaDummy115 A)) (SemanticCore.Class.cv (nb093AlphaDummy116 A))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb093AlphaDummy115 A)) (SemanticCore.Class.cv (nb093AlphaDummy116 A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb093_support_mem_0107 (r : SemanticCore.Var) :

nb093AlphaDummy118 r ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb093AlphaDummy118 r)) (SemanticCore.Class.cv (nb093AlphaDummy119 r))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb093AlphaDummy118 r)) (SemanticCore.Class.cv (nb093AlphaDummy119 r))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb093_support_mem_0108 (A : SemanticCore.Class) :

nb093AlphaDummy115 A ∈ (SemanticCore.Class.cv (nb093AlphaDummy115 A)).fv ∪ (SemanticCore.Class.cv (nb093AlphaDummy116 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb093_support_mem_0109 (r : SemanticCore.Var) :

nb093AlphaDummy118 r ∈ (SemanticCore.Class.cv (nb093AlphaDummy118 r)).fv ∪ (SemanticCore.Class.cv (nb093AlphaDummy119 r)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb093_support_mem_0110 (A : SemanticCore.Class) :

nb093AlphaDummy116 A ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb093AlphaDummy115 A)) (SemanticCore.Class.cv (nb093AlphaDummy116 A))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb093AlphaDummy115 A)) (SemanticCore.Class.cv (nb093AlphaDummy116 A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb093_support_mem_0111 (r : SemanticCore.Var) :

nb093AlphaDummy119 r ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb093AlphaDummy118 r)) (SemanticCore.Class.cv (nb093AlphaDummy119 r))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb093AlphaDummy118 r)) (SemanticCore.Class.cv (nb093AlphaDummy119 r))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb093_support_mem_0112 (A : SemanticCore.Class) :

nb093AlphaDummy116 A ∈ (SemanticCore.Class.cv (nb093AlphaDummy115 A)).fv ∪ (SemanticCore.Class.cv (nb093AlphaDummy116 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb093_support_mem_0113 (r : SemanticCore.Var) :

nb093AlphaDummy119 r ∈ (SemanticCore.Class.cv (nb093AlphaDummy118 r)).fv ∪ (SemanticCore.Class.cv (nb093AlphaDummy119 r)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb093_support_mem_0114 (A : SemanticCore.Class) :

nb093AlphaDummy115 A ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb093AlphaDummy115 A))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb093AlphaDummy116 A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb093_support_mem_0115 (r : SemanticCore.Var) :

nb093AlphaDummy118 r ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb093AlphaDummy118 r))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb093AlphaDummy119 r))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb093_support_mem_0116 (A : SemanticCore.Class) :

nb093AlphaDummy115 A ∈ (SemanticCore.Class.cv (nb093AlphaDummy115 A)).fv ∪ (SemanticCore.Class.cv (nb093AlphaDummy115 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb093_support_mem_0117 (r : SemanticCore.Var) :

nb093AlphaDummy118 r ∈ (SemanticCore.Class.cv (nb093AlphaDummy118 r)).fv ∪ (SemanticCore.Class.cv (nb093AlphaDummy118 r)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb093_support_mem_0118 (A : SemanticCore.Class) :

nb093AlphaDummy116 A ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb093AlphaDummy115 A))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb093AlphaDummy116 A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb093_support_mem_0119 (r : SemanticCore.Var) :

nb093AlphaDummy119 r ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb093AlphaDummy118 r))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb093AlphaDummy119 r))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb093_support_mem_0120 (A : SemanticCore.Class) :

nb093AlphaDummy116 A ∈ (SemanticCore.Class.cv (nb093AlphaDummy116 A)).fv ∪ (SemanticCore.Class.cv (nb093AlphaDummy116 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb093_support_mem_0121 (r : SemanticCore.Var) :

nb093AlphaDummy119 r ∈ (SemanticCore.Class.cv (nb093AlphaDummy119 r)).fv ∪ (SemanticCore.Class.cv (nb093AlphaDummy119 r)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb093_support_mem_0122 (A : SemanticCore.Class) :

nb093AlphaDummy058 A ∈ (SemanticCore.Class.cv (nb093AlphaDummy059 A)).fv ∪ (SemanticCore.Class.cv (nb093AlphaDummy058 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb093_support_mem_0123 (A : SemanticCore.Class) :

nb093AlphaDummy058 A ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb093AlphaDummy100 A) (Compiler.CompactSourceSyntax.synWrex (nb093AlphaDummy101 A) (SemanticCore.Class.cv (nb093AlphaDummy059 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb093AlphaDummy100 A)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb093AlphaDummy101 A))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb093AlphaDummy100 A) (Compiler.CompactSourceSyntax.synWrex (nb093AlphaDummy101 A) (SemanticCore.Class.cv (nb093AlphaDummy058 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb093AlphaDummy100 A)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb093AlphaDummy101 A))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb093_support_mem_0124 (r : SemanticCore.Var) :

nb093AlphaDummy060 r ∈ (SemanticCore.Class.cv (nb093AlphaDummy061 r)).fv ∪ (SemanticCore.Class.cv (nb093AlphaDummy060 r)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb093_support_mem_0125 (r : SemanticCore.Var) :

nb093AlphaDummy060 r ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb093AlphaDummy102 r) (Compiler.CompactSourceSyntax.synWrex (nb093AlphaDummy103 r) (SemanticCore.Class.cv (nb093AlphaDummy061 r)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb093AlphaDummy102 r)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb093AlphaDummy103 r))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb093AlphaDummy102 r) (Compiler.CompactSourceSyntax.synWrex (nb093AlphaDummy103 r) (SemanticCore.Class.cv (nb093AlphaDummy060 r)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb093AlphaDummy102 r)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb093AlphaDummy103 r))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb093_support_mem_0126 (A : SemanticCore.Class) :

nb093AlphaDummy058 A ∈ (SemanticCore.Class.cab (nb093AlphaDummy100 A) (Compiler.CompactSourceSyntax.synWrex (nb093AlphaDummy101 A) (SemanticCore.Class.cv (nb093AlphaDummy058 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb093AlphaDummy100 A)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb093AlphaDummy101 A))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab (nb093AlphaDummy100 A) (Compiler.CompactSourceSyntax.synWrex (nb093AlphaDummy101 A) (SemanticCore.Class.cv (nb093AlphaDummy058 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb093AlphaDummy100 A)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb093AlphaDummy101 A))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb093_support_mem_0127 (r : SemanticCore.Var) :

nb093AlphaDummy060 r ∈ (SemanticCore.Class.cab (nb093AlphaDummy102 r) (Compiler.CompactSourceSyntax.synWrex (nb093AlphaDummy103 r) (SemanticCore.Class.cv (nb093AlphaDummy060 r)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb093AlphaDummy102 r)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb093AlphaDummy103 r))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab (nb093AlphaDummy102 r) (Compiler.CompactSourceSyntax.synWrex (nb093AlphaDummy103 r) (SemanticCore.Class.cv (nb093AlphaDummy060 r)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb093AlphaDummy102 r)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb093AlphaDummy103 r))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb093_support_mem_0128 (A : SemanticCore.Class) :

nb093AlphaDummy101 A ∈ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb093AlphaDummy101 A)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb093_support_mem_0129 (r : SemanticCore.Var) :

nb093AlphaDummy103 r ∈ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb093AlphaDummy103 r)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb093_support_mem_0130 (A : SemanticCore.Class) :

nb093AlphaDummy101 A ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb093AlphaDummy101 A))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb093AlphaDummy101 A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb093_support_mem_0131 (r : SemanticCore.Var) :

nb093AlphaDummy103 r ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb093AlphaDummy103 r))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb093AlphaDummy103 r))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb093_support_mem_0132 (A : SemanticCore.Class) :

nb093AlphaDummy001 A ∈ (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv (nb093AlphaDummy001 A))).fv ∪ (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv (nb093AlphaDummy001 A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb093_support_mem_0133 (r : SemanticCore.Var) :

r ∈ (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv r)).fv ∪ (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv r)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb093_support_mem_0135 (r : SemanticCore.Var) :

r ∈ {nb093AlphaDummy060 r} ∪ {nb093AlphaDummy061 r} ∪ (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb093AlphaDummy061 r)) (SemanticCore.Class.cv r) (SemanticCore.Class.cv (nb093AlphaDummy060 r))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb093_support_mem_0136 (A : SemanticCore.Class) :

nb093AlphaDummy001 A ∈ (SemanticCore.Class.cv (nb093AlphaDummy001 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb093_support_mem_0137 (r : SemanticCore.Var) :

r ∈ (SemanticCore.Class.cv r).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb093_support_mem_0138 (A : SemanticCore.Class) :

nb093AlphaDummy045 A ∈ (SemanticCore.Class.cv (nb093AlphaDummy045 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb093_support_mem_0139 (r d : SemanticCore.Var) :

nb093AlphaDummy047 r d ∈ (SemanticCore.Class.cv (nb093AlphaDummy047 r d)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb093_support_mem_0142 (A : SemanticCore.Class) :

nb093AlphaDummy136 A ∈ (SemanticCore.Class.cv (nb093AlphaDummy136 A)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb093_support_mem_0143 (r d : SemanticCore.Var) :

nb093AlphaDummy138 r d ∈ (SemanticCore.Class.cv (nb093AlphaDummy138 r d)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb093_support_mem_0144 (A : SemanticCore.Class) :

nb093AlphaDummy143 A ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb093AlphaDummy143 A)) (SemanticCore.Class.cv (nb093AlphaDummy144 A))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb093AlphaDummy143 A)) (SemanticCore.Class.cv (nb093AlphaDummy144 A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb093_support_mem_0145 (r d : SemanticCore.Var) :

nb093AlphaDummy146 r d ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb093AlphaDummy146 r d)) (SemanticCore.Class.cv (nb093AlphaDummy147 r d))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb093AlphaDummy146 r d)) (SemanticCore.Class.cv (nb093AlphaDummy147 r d))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb093_support_mem_0146 (A : SemanticCore.Class) :

nb093AlphaDummy143 A ∈ (SemanticCore.Class.cv (nb093AlphaDummy143 A)).fv ∪ (SemanticCore.Class.cv (nb093AlphaDummy144 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb093_support_mem_0147 (r d : SemanticCore.Var) :

nb093AlphaDummy146 r d ∈ (SemanticCore.Class.cv (nb093AlphaDummy146 r d)).fv ∪ (SemanticCore.Class.cv (nb093AlphaDummy147 r d)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb093_support_mem_0148 (A : SemanticCore.Class) :

nb093AlphaDummy144 A ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb093AlphaDummy143 A)) (SemanticCore.Class.cv (nb093AlphaDummy144 A))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb093AlphaDummy143 A)) (SemanticCore.Class.cv (nb093AlphaDummy144 A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb093_support_mem_0149 (r d : SemanticCore.Var) :

nb093AlphaDummy147 r d ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb093AlphaDummy146 r d)) (SemanticCore.Class.cv (nb093AlphaDummy147 r d))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb093AlphaDummy146 r d)) (SemanticCore.Class.cv (nb093AlphaDummy147 r d))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb093_support_mem_0150 (A : SemanticCore.Class) :

nb093AlphaDummy144 A ∈ (SemanticCore.Class.cv (nb093AlphaDummy143 A)).fv ∪ (SemanticCore.Class.cv (nb093AlphaDummy144 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb093_support_mem_0151 (r d : SemanticCore.Var) :

nb093AlphaDummy147 r d ∈ (SemanticCore.Class.cv (nb093AlphaDummy146 r d)).fv ∪ (SemanticCore.Class.cv (nb093AlphaDummy147 r d)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb093_support_mem_0152 (A : SemanticCore.Class) :

nb093AlphaDummy143 A ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb093AlphaDummy143 A))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb093AlphaDummy144 A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb093_support_mem_0153 (r d : SemanticCore.Var) :

nb093AlphaDummy146 r d ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb093AlphaDummy146 r d))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb093AlphaDummy147 r d))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb093_support_mem_0154 (A : SemanticCore.Class) :

nb093AlphaDummy143 A ∈ (SemanticCore.Class.cv (nb093AlphaDummy143 A)).fv ∪ (SemanticCore.Class.cv (nb093AlphaDummy143 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb093_support_mem_0155 (r d : SemanticCore.Var) :

nb093AlphaDummy146 r d ∈ (SemanticCore.Class.cv (nb093AlphaDummy146 r d)).fv ∪ (SemanticCore.Class.cv (nb093AlphaDummy146 r d)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb093_support_mem_0156 (A : SemanticCore.Class) :

nb093AlphaDummy144 A ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb093AlphaDummy143 A))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb093AlphaDummy144 A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb093_support_mem_0157 (r d : SemanticCore.Var) :

nb093AlphaDummy147 r d ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb093AlphaDummy146 r d))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb093AlphaDummy147 r d))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb093_support_mem_0158 (A : SemanticCore.Class) :

nb093AlphaDummy144 A ∈ (SemanticCore.Class.cv (nb093AlphaDummy144 A)).fv ∪ (SemanticCore.Class.cv (nb093AlphaDummy144 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb093_support_mem_0159 (r d : SemanticCore.Var) :

nb093AlphaDummy147 r d ∈ (SemanticCore.Class.cv (nb093AlphaDummy147 r d)).fv ∪ (SemanticCore.Class.cv (nb093AlphaDummy147 r d)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb093_support_mem_0160 (A : SemanticCore.Class) :

nb093AlphaDummy000 A ∈ (Compiler.CompactSourceSyntax.synCdif (SemanticCore.Class.cv (nb093AlphaDummy001 A)) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv (nb093AlphaDummy001 A)))).fv ∪ (SemanticCore.Class.cv (nb093AlphaDummy000 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb093_support_mem_0161 (A : SemanticCore.Class) :

nb093AlphaDummy000 A ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb093AlphaDummy044 A) (Compiler.CompactSourceSyntax.synWrex (nb093AlphaDummy045 A) (Compiler.CompactSourceSyntax.synCdif (SemanticCore.Class.cv (nb093AlphaDummy001 A)) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv (nb093AlphaDummy001 A)))) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb093AlphaDummy044 A)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb093AlphaDummy045 A))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb093AlphaDummy044 A) (Compiler.CompactSourceSyntax.synWrex (nb093AlphaDummy045 A) (SemanticCore.Class.cv (nb093AlphaDummy000 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb093AlphaDummy044 A)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb093AlphaDummy045 A))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb093_support_mem_0162 (r d : SemanticCore.Var) :

d ∈ (Compiler.CompactSourceSyntax.synCdif (SemanticCore.Class.cv r) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv r))).fv ∪ (SemanticCore.Class.cv d).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb093_support_mem_0163 (r d : SemanticCore.Var) :

d ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb093AlphaDummy046 r d) (Compiler.CompactSourceSyntax.synWrex (nb093AlphaDummy047 r d) (Compiler.CompactSourceSyntax.synCdif (SemanticCore.Class.cv r) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv r))) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb093AlphaDummy046 r d)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb093AlphaDummy047 r d))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb093AlphaDummy046 r d) (Compiler.CompactSourceSyntax.synWrex (nb093AlphaDummy047 r d) (SemanticCore.Class.cv d) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb093AlphaDummy046 r d)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb093AlphaDummy047 r d))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb093_support_mem_0164 (A : SemanticCore.Class) :

nb093AlphaDummy000 A ∈ (SemanticCore.Class.cab (nb093AlphaDummy044 A) (Compiler.CompactSourceSyntax.synWrex (nb093AlphaDummy045 A) (SemanticCore.Class.cv (nb093AlphaDummy000 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb093AlphaDummy044 A)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb093AlphaDummy045 A))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab (nb093AlphaDummy044 A) (Compiler.CompactSourceSyntax.synWrex (nb093AlphaDummy045 A) (SemanticCore.Class.cv (nb093AlphaDummy000 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb093AlphaDummy044 A)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb093AlphaDummy045 A))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb093_support_mem_0165 (r d : SemanticCore.Var) :

d ∈ (SemanticCore.Class.cab (nb093AlphaDummy046 r d) (Compiler.CompactSourceSyntax.synWrex (nb093AlphaDummy047 r d) (SemanticCore.Class.cv d) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb093AlphaDummy046 r d)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb093AlphaDummy047 r d))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab (nb093AlphaDummy046 r d) (Compiler.CompactSourceSyntax.synWrex (nb093AlphaDummy047 r d) (SemanticCore.Class.cv d) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb093AlphaDummy046 r d)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb093AlphaDummy047 r d))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb093_support_mem_0166 (A : SemanticCore.Class) :

nb093AlphaDummy045 A ∈ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb093AlphaDummy045 A)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb093_support_mem_0167 (r d : SemanticCore.Var) :

nb093AlphaDummy047 r d ∈ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb093AlphaDummy047 r d)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb093_support_mem_0168 (A : SemanticCore.Class) :

nb093AlphaDummy045 A ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb093AlphaDummy045 A))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb093AlphaDummy045 A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb093_support_mem_0169 (r d : SemanticCore.Var) :

nb093AlphaDummy047 r d ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb093AlphaDummy047 r d))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb093AlphaDummy047 r d))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb093_focused_notmem_0000 (A : SemanticCore.Class) :

nb093AlphaDummy004 A ∉ A.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb093_wpp_notmem_0000 (A : SemanticCore.Class) :

nb093AlphaDummy004 A ∉ (Compiler.CompactSourceSyntax.synClntpc A).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb093_focused_notmem_0001 (A : SemanticCore.Class) (r d : SemanticCore.Var) :

nb093AlphaDummy005 A r d ∉ A.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb093_wpp_notmem_0001 (A : SemanticCore.Class) (r d : SemanticCore.Var) :

nb093AlphaDummy005 A r d ∉ (Compiler.CompactSourceSyntax.synClntpc A).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb093_focused_notmem_0002 (A : SemanticCore.Class) :

nb093AlphaDummy002 A ∉ A.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb093_wpp_notmem_0002 (A : SemanticCore.Class) :

nb093AlphaDummy002 A ∉ (Compiler.CompactSourceSyntax.synClntpc A).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb093_focused_notmem_0003 (A : SemanticCore.Class) (r d : SemanticCore.Var) :

nb093AlphaDummy003 A r d ∉ A.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb093_wpp_notmem_0003 (A : SemanticCore.Class) (r d : SemanticCore.Var) :

nb093AlphaDummy003 A r d ∉ (Compiler.CompactSourceSyntax.synClntpc A).fv

Certificates from AlphaSupport.NAR4H5C093M3Part002Stage2.

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb093WppRefl0000 (A : SemanticCore.Class) (r d : SemanticCore.Var) :

Nominal.TReflOn [(nb093AlphaDummy004 A, nb093AlphaDummy005 A r d), (nb093AlphaDummy002 A, nb093AlphaDummy003 A r d)] (Compiler.CompactSourceSyntax.synClntpc A).fv

Checked nominal proof certificate identified upstream as nb093_wpp_refl_0000.

Equations

NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb093WppRefl0000 A r d = ⋯.reflOn

Instances For

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb093_compact_fv_empty_0020 (A : SemanticCore.Class) :

nb093AlphaDummy000 A ∉ ∅

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb093_compact_fv_empty_0021 (d : SemanticCore.Var) :

d ∉ ∅

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb093_compact_fv_empty_0022 (A : SemanticCore.Class) :

nb093AlphaDummy001 A ∉ ∅

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb093_compact_fv_empty_0023 (r : SemanticCore.Var) :

r ∉ ∅

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb093_compact_fv_empty_0024 (A : SemanticCore.Class) :

nb093AlphaDummy006 A ∉ ∅

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb093_compact_fv_empty_0025 (r d : SemanticCore.Var) :

nb093AlphaDummy007 r d ∉ ∅

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb093_compact_fv_empty_0026 (A : SemanticCore.Class) :

nb093AlphaDummy004 A ∉ ∅

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb093_compact_fv_empty_0027 (A : SemanticCore.Class) (r d : SemanticCore.Var) :

nb093AlphaDummy005 A r d ∉ ∅

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb093_compact_fv_empty_0028 (A : SemanticCore.Class) :

nb093AlphaDummy002 A ∉ ∅

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb093_compact_fv_empty_0029 (A : SemanticCore.Class) (r d : SemanticCore.Var) :

nb093AlphaDummy003 A r d ∉ ∅