Documentation

LeanPool.NFWeakPartition.Certificates.NominalWPPReplayChunk017Compact001Block021

Nominal proof certificates grouped in dependency order.

Certificates from NominalWPPReplayChunk017Compact001Part088.

source
noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCfbhnqinjcodecoverddndv (u : SemanticCore.Var) (P : SemanticCore.Class) (k : SemanticCore.Var) (Y : SemanticCore.Class) (_dv_P_k : k ∉ P.fv) (dv_P_u : u ∉ P.fv) (_dv_Y_k : k ∉ Y.fv) (_dv_Y_u : u ∉ Y.fv) (_dv_k_u : k ≠ u) (hyp_cfbhnqinjcodecoverddndv_1 : Nominal.NPrf (SemanticCore.Wff.classMem P Compiler.CompactSourceSyntax.synCvv)) (hyp_cfbhnqinjcodecoverddndv_2 : Nominal.NPrf (SemanticCore.Wff.classMem Y Compiler.CompactSourceSyntax.synCvv)) :
Nominal.NPrf ((SemanticCore.Wff.classMem (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synChwcn P)).imp ((Compiler.CompactSourceSyntax.synWf1 (SemanticCore.Class.cv k) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)) Y).imp (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChnqinc P (Compiler.CompactSourceSyntax.synCun P Y)) (Compiler.CompactSourceSyntax.synCec (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synChwniso P))) (Compiler.CompactSourceSyntax.synCrn (Compiler.CompactSourceSyntax.synChnqinc Y (Compiler.CompactSourceSyntax.synCun P Y))))))

Checked nominal proof certificate identified upstream as g_cfbhnqinjcodecoverddndv.

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

    Certificates from NominalWPPReplayChunk017Compact001Part089.

    source
    noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCfbhnqinjcodecoverdclndv (C P : SemanticCore.Class) (k : SemanticCore.Var) (Y : SemanticCore.Class) (dv_P_k : k ∉ P.fv) (dv_Y_k : k ∉ Y.fv) (hyp_cfbhnqinjcodecoverdclndv_1 : Nominal.NPrf (SemanticCore.Wff.classMem P Compiler.CompactSourceSyntax.synCvv)) (hyp_cfbhnqinjcodecoverdclndv_2 : Nominal.NPrf (SemanticCore.Wff.classMem Y Compiler.CompactSourceSyntax.synCvv)) (hyp_cfbhnqinjcodecoverdclndv_3 : Nominal.NPrf (SemanticCore.Wff.classMem C (Compiler.CompactSourceSyntax.synChwcn P))) :
    Nominal.NPrf ((Compiler.CompactSourceSyntax.synWf1 (SemanticCore.Class.cv k) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd C) Y).imp (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChnqinc P (Compiler.CompactSourceSyntax.synCun P Y)) (Compiler.CompactSourceSyntax.synCec C (Compiler.CompactSourceSyntax.synChwniso P))) (Compiler.CompactSourceSyntax.synCrn (Compiler.CompactSourceSyntax.synChnqinc Y (Compiler.CompactSourceSyntax.synCun P Y)))))

    Checked nominal proof certificate identified upstream as g_cfbhnqinjcodecoverdclndv.

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