Documentation

LeanPool.NFWeakPartition.NominalAlphaRepairedBase001037OpabOpaqueCertificate004

NF weak partition development: NominalAlphaRepairedBase001037OpabOpaqueCertificate004.

source
noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb037OpabAlphaCertificateOpaque004 (ph : SemanticCore.Wff) (x y z : SemanticCore.Var) (dv_ph_z : z ∉ ph.fv) (dv_x_z : x ≠ z) (dv_y_z : y ≠ z) :
Nominal.TAlphaClass [] (Compiler.CompactSourceSyntax.synCopab x y ph) (SemanticCore.Class.cab z (Compiler.CompactSourceSyntax.synWex x (Compiler.CompactSourceSyntax.synWex y (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classEq (SemanticCore.Class.cv z) (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv x) (SemanticCore.Class.cv y))) ph))))

Checked nominal proof certificate identified upstream as nb037_opab_alpha_certificate_opaque004.

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