Documentation

LeanPool.NFWeakPartition.NAR4H5C095M3Part046

NF weak partition development: NAR4H5C095M3Part046.

source
noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095SplitAlpha0102 (x u : SemanticCore.Var) (D R S_cls : SemanticCore.Class) (f : SemanticCore.Var) (E : SemanticCore.Class) (dv_D_f : f ∉ D.fv) (dv_D_u : u ∉ D.fv) (dv_D_x : x ∉ D.fv) (dv_E_f : f ∉ E.fv) (dv_E_u : u ∉ E.fv) (dv_E_x : x ∉ E.fv) (dv_R_f : f ∉ R.fv) (dv_R_u : u ∉ R.fv) (dv_R_x : x ∉ R.fv) (dv_S_f : f ∉ S_cls.fv) (dv_S_u : u ∉ S_cls.fv) (dv_S_x : x ∉ S_cls.fv) (dv_f_u : f ≠ u) (dv_f_x : f ≠ x) (dv_u_x : u ≠ x) :
Nominal.TAlphaWff [(nb095AlphaDummy004 D R S_cls E, nb095AlphaDummy006 x u D R S_cls f E), (nb095AlphaDummy003 D R S_cls E, nb095AlphaDummy005 x u D R S_cls f E), (nb095AlphaDummy001 D R S_cls E, u), (nb095AlphaDummy002 D R S_cls E, x), (nb095AlphaDummy000 D R S_cls E, f)] ((Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCfv (SemanticCore.Class.cv (nb095AlphaDummy000 D R S_cls E)) (SemanticCore.Class.cv (nb095AlphaDummy003 D R S_cls E))) (Compiler.CompactSourceSyntax.synCin S_cls (Compiler.CompactSourceSyntax.synCxp (Compiler.CompactSourceSyntax.synCin E (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif S_cls Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv (nb095AlphaDummy001 D R S_cls E))))) (Compiler.CompactSourceSyntax.synCin E (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif S_cls Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv (nb095AlphaDummy001 D R S_cls E))))))) (Compiler.CompactSourceSyntax.synCfv (SemanticCore.Class.cv (nb095AlphaDummy000 D R S_cls E)) (SemanticCore.Class.cv (nb095AlphaDummy004 D R S_cls E)))).imp (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb095AlphaDummy003 D R S_cls E)) (Compiler.CompactSourceSyntax.synCin R (Compiler.CompactSourceSyntax.synCxp (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv (nb095AlphaDummy002 D R S_cls E))))) (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv (nb095AlphaDummy002 D R S_cls E))))))) (SemanticCore.Class.cv (nb095AlphaDummy004 D R S_cls E)))) ((Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCfv (SemanticCore.Class.cv f) (SemanticCore.Class.cv (nb095AlphaDummy005 x u D R S_cls f E))) (Compiler.CompactSourceSyntax.synCin S_cls (Compiler.CompactSourceSyntax.synCxp (Compiler.CompactSourceSyntax.synCin E (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif S_cls Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv u)))) (Compiler.CompactSourceSyntax.synCin E (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif S_cls Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv u)))))) (Compiler.CompactSourceSyntax.synCfv (SemanticCore.Class.cv f) (SemanticCore.Class.cv (nb095AlphaDummy006 x u D R S_cls f E)))).imp (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb095AlphaDummy005 x u D R S_cls f E)) (Compiler.CompactSourceSyntax.synCin R (Compiler.CompactSourceSyntax.synCxp (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv x)))) (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv x)))))) (SemanticCore.Class.cv (nb095AlphaDummy006 x u D R S_cls f E))))

Checked nominal proof certificate identified upstream as nb095_split_alpha_0102.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095SplitAlpha0103 (x u : SemanticCore.Var) (D R S_cls : SemanticCore.Class) (f : SemanticCore.Var) (E : SemanticCore.Class) (dv_D_f : f ∉ D.fv) (dv_D_u : u ∉ D.fv) (dv_D_x : x ∉ D.fv) (dv_E_f : f ∉ E.fv) (dv_E_u : u ∉ E.fv) (dv_E_x : x ∉ E.fv) (dv_R_f : f ∉ R.fv) (dv_R_u : u ∉ R.fv) (dv_R_x : x ∉ R.fv) (dv_S_f : f ∉ S_cls.fv) (dv_S_u : u ∉ S_cls.fv) (dv_S_x : x ∉ S_cls.fv) (dv_f_u : f ≠ u) (dv_f_x : f ≠ x) (dv_u_x : u ≠ x) :
    Nominal.TAlphaWff [(nb095AlphaDummy003 D R S_cls E, nb095AlphaDummy005 x u D R S_cls f E), (nb095AlphaDummy001 D R S_cls E, u), (nb095AlphaDummy002 D R S_cls E, x), (nb095AlphaDummy000 D R S_cls E, f)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb095AlphaDummy003 D R S_cls E)) (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv (nb095AlphaDummy002 D R S_cls E)))))).imp (Compiler.CompactSourceSyntax.synWral (nb095AlphaDummy004 D R S_cls E) (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv (nb095AlphaDummy002 D R S_cls E))))) (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb095AlphaDummy003 D R S_cls E)) (Compiler.CompactSourceSyntax.synCin R (Compiler.CompactSourceSyntax.synCxp (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv (nb095AlphaDummy002 D R S_cls E))))) (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv (nb095AlphaDummy002 D R S_cls E))))))) (SemanticCore.Class.cv (nb095AlphaDummy004 D R S_cls E))) (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCfv (SemanticCore.Class.cv (nb095AlphaDummy000 D R S_cls E)) (SemanticCore.Class.cv (nb095AlphaDummy003 D R S_cls E))) (Compiler.CompactSourceSyntax.synCin S_cls (Compiler.CompactSourceSyntax.synCxp (Compiler.CompactSourceSyntax.synCin E (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif S_cls Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv (nb095AlphaDummy001 D R S_cls E))))) (Compiler.CompactSourceSyntax.synCin E (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif S_cls Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv (nb095AlphaDummy001 D R S_cls E))))))) (Compiler.CompactSourceSyntax.synCfv (SemanticCore.Class.cv (nb095AlphaDummy000 D R S_cls E)) (SemanticCore.Class.cv (nb095AlphaDummy004 D R S_cls E))))))) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb095AlphaDummy005 x u D R S_cls f E)) (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv x))))).imp (Compiler.CompactSourceSyntax.synWral (nb095AlphaDummy006 x u D R S_cls f E) (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv x)))) (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb095AlphaDummy005 x u D R S_cls f E)) (Compiler.CompactSourceSyntax.synCin R (Compiler.CompactSourceSyntax.synCxp (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv x)))) (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv x)))))) (SemanticCore.Class.cv (nb095AlphaDummy006 x u D R S_cls f E))) (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCfv (SemanticCore.Class.cv f) (SemanticCore.Class.cv (nb095AlphaDummy005 x u D R S_cls f E))) (Compiler.CompactSourceSyntax.synCin S_cls (Compiler.CompactSourceSyntax.synCxp (Compiler.CompactSourceSyntax.synCin E (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif S_cls Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv u)))) (Compiler.CompactSourceSyntax.synCin E (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif S_cls Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv u)))))) (Compiler.CompactSourceSyntax.synCfv (SemanticCore.Class.cv f) (SemanticCore.Class.cv (nb095AlphaDummy006 x u D R S_cls f E)))))))

    Checked nominal proof certificate identified upstream as nb095_split_alpha_0103.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nominalDfWecutiso (x u : SemanticCore.Var) (D R S_cls : SemanticCore.Class) (f : SemanticCore.Var) (E : SemanticCore.Class) (dv_D_f : f ∉ D.fv) (dv_D_u : u ∉ D.fv) (dv_D_x : x ∉ D.fv) (dv_E_f : f ∉ E.fv) (dv_E_u : u ∉ E.fv) (dv_E_x : x ∉ E.fv) (dv_R_f : f ∉ R.fv) (dv_R_u : u ∉ R.fv) (dv_R_x : x ∉ R.fv) (dv_S_f : f ∉ S_cls.fv) (dv_S_u : u ∉ S_cls.fv) (dv_S_x : x ∉ S_cls.fv) (dv_f_u : f ≠ u) (dv_f_x : f ≠ x) (dv_u_x : u ≠ x) :
      Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCwecutiso R D S_cls E) (SemanticCore.Class.cab f (Compiler.CompactSourceSyntax.synWrex x D (Compiler.CompactSourceSyntax.synWrex u E (Compiler.CompactSourceSyntax.synWiso (SemanticCore.Class.cv f) (Compiler.CompactSourceSyntax.synCin R (Compiler.CompactSourceSyntax.synCxp (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv x)))) (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv x)))))) (Compiler.CompactSourceSyntax.synCin S_cls (Compiler.CompactSourceSyntax.synCxp (Compiler.CompactSourceSyntax.synCin E (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif S_cls Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv u)))) (Compiler.CompactSourceSyntax.synCin E (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif S_cls Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv u)))))) (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv x)))) (Compiler.CompactSourceSyntax.synCin E (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif S_cls Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv u)))))))))

      Checked nominal proof certificate identified upstream as nominal_df_wecutiso.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For