Documentation

LeanPool.NFWeakPartition.Certificates.CodeCoverBlock003

Nominal proof certificates grouped in dependency order.

Certificates from ReplaySupport.CodeCover7.

source
noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCfbhnqinjcodecoverddndvStage7 (u : SemanticCore.Var) (P : SemanticCore.Class) (k : SemanticCore.Var) (Y : SemanticCore.Class) (p0628 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7))) Compiler.CompactSourceSyntax.synCvv) (Compiler.CompactSourceSyntax.synWex (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 1) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 1)) (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7))))))) (p0630 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6))) Compiler.CompactSourceSyntax.synCvv) (Compiler.CompactSourceSyntax.synWex (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2)) (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6))))))) (p0639 : Nominal.NPrf ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2)) (Compiler.CompactSourceSyntax.synChwcn (Compiler.CompactSourceSyntax.synCun P Y))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2)) (Compiler.CompactSourceSyntax.synChwcodes (Compiler.CompactSourceSyntax.synCun P Y))))) (p0641 : Nominal.NPrf ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 1)) (Compiler.CompactSourceSyntax.synChwcn (Compiler.CompactSourceSyntax.synCun P Y))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 1)) (Compiler.CompactSourceSyntax.synChwcodes (Compiler.CompactSourceSyntax.synCun P Y))))) (p0653 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2)) (Compiler.CompactSourceSyntax.synChwcodes (Compiler.CompactSourceSyntax.synCun P Y))) (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 1)) (Compiler.CompactSourceSyntax.synChwcodes (Compiler.CompactSourceSyntax.synCun P Y)))).imp ((Compiler.CompactSourceSyntax.synWex (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 8) (Compiler.CompactSourceSyntax.synWiso (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 8)) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC1st (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2))) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC1st (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 1))) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2))) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 1))))).imp (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2)) (Compiler.CompactSourceSyntax.synChwcodes (Compiler.CompactSourceSyntax.synCun P Y))) (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 1)) (Compiler.CompactSourceSyntax.synChwcodes (Compiler.CompactSourceSyntax.synCun P Y)))) (Compiler.CompactSourceSyntax.synWex (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 8) (Compiler.CompactSourceSyntax.synWiso (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 8)) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC1st (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2))) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC1st (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 1))) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2))) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 1))))))))) (p0657 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2)) (Compiler.CompactSourceSyntax.synChwiso (Compiler.CompactSourceSyntax.synCun P Y)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 1))) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2)) (Compiler.CompactSourceSyntax.synChwcodes (Compiler.CompactSourceSyntax.synCun P Y))) (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 1)) (Compiler.CompactSourceSyntax.synChwcodes (Compiler.CompactSourceSyntax.synCun P Y)))) (Compiler.CompactSourceSyntax.synWex (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 8) (Compiler.CompactSourceSyntax.synWiso (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 8)) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC1st (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2))) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC1st (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 1))) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2))) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 1)))))))) (p0660 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2)) (Compiler.CompactSourceSyntax.synChwniso (Compiler.CompactSourceSyntax.synCun P Y)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 1))) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2)) (Compiler.CompactSourceSyntax.synChwcn (Compiler.CompactSourceSyntax.synCun P Y))) (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 1)) (Compiler.CompactSourceSyntax.synChwcn (Compiler.CompactSourceSyntax.synCun P Y)))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2)) (Compiler.CompactSourceSyntax.synChwiso (Compiler.CompactSourceSyntax.synCun P Y)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 1)))))) (p0668 : Nominal.NPrf ((SemanticCore.Wff.classEq (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2)) (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6)))).imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2)) (Compiler.CompactSourceSyntax.synChwniso (Compiler.CompactSourceSyntax.synCun P Y)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 1))) (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6))) (Compiler.CompactSourceSyntax.synChwniso (Compiler.CompactSourceSyntax.synCun P Y)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 1)))))) (p0677 : Nominal.NPrf ((SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6))) Compiler.CompactSourceSyntax.synCvv).imp (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6))) Compiler.CompactSourceSyntax.synCvv))) (p0684 : Nominal.NPrf ((SemanticCore.Wff.classEq (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 1)) (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7)))).imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6))) (Compiler.CompactSourceSyntax.synChwniso (Compiler.CompactSourceSyntax.synCun P Y)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 1))) (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6))) (Compiler.CompactSourceSyntax.synChwniso (Compiler.CompactSourceSyntax.synCun P Y)) (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7))))))) (p0691 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 1) (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6))) Compiler.CompactSourceSyntax.synCvv))) (p0697 : Nominal.NPrf ((SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7))) Compiler.CompactSourceSyntax.synCvv).imp (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7))) Compiler.CompactSourceSyntax.synCvv))) (p0715 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6))) (Compiler.CompactSourceSyntax.synChwcn (Compiler.CompactSourceSyntax.synCun P Y))) (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7))) (Compiler.CompactSourceSyntax.synChwcn (Compiler.CompactSourceSyntax.synCun P Y)))).imp (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCec (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6))) (Compiler.CompactSourceSyntax.synChwniso (Compiler.CompactSourceSyntax.synCun P Y))) (Compiler.CompactSourceSyntax.synCec (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7))) (Compiler.CompactSourceSyntax.synChwniso (Compiler.CompactSourceSyntax.synCun P Y)))) (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6))) (Compiler.CompactSourceSyntax.synChwniso (Compiler.CompactSourceSyntax.synCun P Y)) (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7))))))) (p0717 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCec (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6))) (Compiler.CompactSourceSyntax.synChwniso (Compiler.CompactSourceSyntax.synCun P Y))) (Compiler.CompactSourceSyntax.synCec (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7))) (Compiler.CompactSourceSyntax.synChwniso (Compiler.CompactSourceSyntax.synCun P Y)))) (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6))) (Compiler.CompactSourceSyntax.synChwniso (Compiler.CompactSourceSyntax.synCun P Y)) (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7))))) (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6))) (Compiler.CompactSourceSyntax.synChwniso (Compiler.CompactSourceSyntax.synCun P Y)) (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7)))) (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCec (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6))) (Compiler.CompactSourceSyntax.synChwniso (Compiler.CompactSourceSyntax.synCun P Y))) (Compiler.CompactSourceSyntax.synCec (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7))) (Compiler.CompactSourceSyntax.synChwniso (Compiler.CompactSourceSyntax.synCun P Y))))))) (p0719 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6))) (Compiler.CompactSourceSyntax.synChwniso (Compiler.CompactSourceSyntax.synCun P Y)) (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7)))) (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCec (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6))) (Compiler.CompactSourceSyntax.synChwniso (Compiler.CompactSourceSyntax.synCun P Y))) (Compiler.CompactSourceSyntax.synCec (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7))) (Compiler.CompactSourceSyntax.synChwniso (Compiler.CompactSourceSyntax.synCun P Y))))).imp ((Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6))) (Compiler.CompactSourceSyntax.synChwniso (Compiler.CompactSourceSyntax.synCun P Y)) (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7)))).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCec (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6))) (Compiler.CompactSourceSyntax.synChwniso (Compiler.CompactSourceSyntax.synCun P Y))) (Compiler.CompactSourceSyntax.synCec (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7))) (Compiler.CompactSourceSyntax.synChwniso (Compiler.CompactSourceSyntax.synCun P Y))))))) (p0721 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6))) (Compiler.CompactSourceSyntax.synChwniso (Compiler.CompactSourceSyntax.synCun P Y)) (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7)))).imp (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6))) (Compiler.CompactSourceSyntax.synChwniso (Compiler.CompactSourceSyntax.synCun P Y)) (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7)))))) (p0724 : Nominal.NPrf ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCec (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6))) (Compiler.CompactSourceSyntax.synChwniso (Compiler.CompactSourceSyntax.synCun P Y))) (Compiler.CompactSourceSyntax.synCec (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7))) (Compiler.CompactSourceSyntax.synChwniso (Compiler.CompactSourceSyntax.synCun P Y)))).imp (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6))) (Compiler.CompactSourceSyntax.synCec (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6))) (Compiler.CompactSourceSyntax.synChwniso (Compiler.CompactSourceSyntax.synCun P Y)))) (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6))) (Compiler.CompactSourceSyntax.synCec (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7))) (Compiler.CompactSourceSyntax.synChwniso (Compiler.CompactSourceSyntax.synCun P Y))))))) (p0726 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6))) (Compiler.CompactSourceSyntax.synCec (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6))) (Compiler.CompactSourceSyntax.synChwniso (Compiler.CompactSourceSyntax.synCun P Y)))) (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6))) (Compiler.CompactSourceSyntax.synCec (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7))) (Compiler.CompactSourceSyntax.synChwniso (Compiler.CompactSourceSyntax.synCun P Y))))).imp ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6))) (Compiler.CompactSourceSyntax.synCec (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6))) (Compiler.CompactSourceSyntax.synChwniso (Compiler.CompactSourceSyntax.synCun P Y)))).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6))) (Compiler.CompactSourceSyntax.synCec (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7))) (Compiler.CompactSourceSyntax.synChwniso (Compiler.CompactSourceSyntax.synCun P Y))))))) (p0734 : Nominal.NPrf ((SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7))) (Compiler.CompactSourceSyntax.synChwcn (Compiler.CompactSourceSyntax.synCun P Y))).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7))))) (Compiler.CompactSourceSyntax.synCec (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7))) (Compiler.CompactSourceSyntax.synChwniso (Compiler.CompactSourceSyntax.synCun P Y)))))) (p0736 : Nominal.NPrf ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7))))) (Compiler.CompactSourceSyntax.synCec (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7))) (Compiler.CompactSourceSyntax.synChwniso (Compiler.CompactSourceSyntax.synCun P Y)))).imp (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7))) (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7)))))) (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7))) (Compiler.CompactSourceSyntax.synCec (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7))) (Compiler.CompactSourceSyntax.synChwniso (Compiler.CompactSourceSyntax.synCun P Y))))))) (p0738 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7))) (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7)))))) (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7))) (Compiler.CompactSourceSyntax.synCec (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7))) (Compiler.CompactSourceSyntax.synChwniso (Compiler.CompactSourceSyntax.synCun P Y))))).imp ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7))) (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7)))))).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7))) (Compiler.CompactSourceSyntax.synCec (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7))) (Compiler.CompactSourceSyntax.synChwniso (Compiler.CompactSourceSyntax.synCun P Y))))))) (p0742 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7))) (Compiler.CompactSourceSyntax.synCec (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7))) (Compiler.CompactSourceSyntax.synChwniso (Compiler.CompactSourceSyntax.synCun P Y)))) (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCec (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7))) (Compiler.CompactSourceSyntax.synChwniso (Compiler.CompactSourceSyntax.synCun P Y))) (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7)))))) (p0744 : Nominal.NPrf ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCec (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7))) (Compiler.CompactSourceSyntax.synChwniso (Compiler.CompactSourceSyntax.synCun P Y))) (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7)))).imp (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6))) (Compiler.CompactSourceSyntax.synCec (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7))) (Compiler.CompactSourceSyntax.synChwniso (Compiler.CompactSourceSyntax.synCun P Y)))) (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6))) (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7))))))) (p0746 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6))) (Compiler.CompactSourceSyntax.synCec (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7))) (Compiler.CompactSourceSyntax.synChwniso (Compiler.CompactSourceSyntax.synCun P Y)))) (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6))) (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7))))).imp ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6))) (Compiler.CompactSourceSyntax.synCec (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7))) (Compiler.CompactSourceSyntax.synChwniso (Compiler.CompactSourceSyntax.synCun P Y)))).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6))) (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7))))))) (p0752 : Nominal.NPrf ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6))) (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7)))).imp (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classEq (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 1)) (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6)))) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 1)) (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7))))))) (p0754 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classEq (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 1)) (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6)))) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 1)) (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7))))).imp ((SemanticCore.Wff.classEq (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 1)) (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6)))).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 1)) (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7))))))) (p0764 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7)) (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 5))).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 5))))) (p0773 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWex (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 1)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 5)))).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 1)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 5))))) (p0781 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWex (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 1)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 5)))).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 1)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 5))))) (p0805 : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCdm (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y))) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synChwcn (Compiler.CompactSourceSyntax.synCun P Y))))) (p1121 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6))) Compiler.CompactSourceSyntax.synCvv) (Compiler.CompactSourceSyntax.synWex (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 4) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 4)) (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6))))))) (p1161 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7))) Compiler.CompactSourceSyntax.synCvv) (Compiler.CompactSourceSyntax.synWex (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 4) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 4)) (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7))))))) (p1163 : Nominal.NPrf ((SemanticCore.Wff.classEq (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 4)) (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7)))).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 4))) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7))))))) (p1208 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7))) Compiler.CompactSourceSyntax.synCvv) (Compiler.CompactSourceSyntax.synWex (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 11) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 11)) (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7))))))) (p1248 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 11) (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6))) Compiler.CompactSourceSyntax.synCvv))) (p1618 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWf1 (SemanticCore.Class.cv k) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)) Y).imp (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synChwcn (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv k))) (Compiler.CompactSourceSyntax.synChwcn (Compiler.CompactSourceSyntax.synCun P Y))))) (p1662 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWf1 (SemanticCore.Class.cv k) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)) Y).imp (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv k)) Compiler.CompactSourceSyntax.synCvv))) (p1664 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWf1 (SemanticCore.Class.cv k) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)) Y).imp (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synChwniso (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv k))) Compiler.CompactSourceSyntax.synCvv))) (p1789 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWf1 (SemanticCore.Class.cv k) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)) Y).imp ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 4)) (Compiler.CompactSourceSyntax.synChwcn (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv k)))).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv k))) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 4)))) (Compiler.CompactSourceSyntax.synCec (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 4)) (Compiler.CompactSourceSyntax.synChwniso (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv k)))))))) (p1853 : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synChnqinc (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv k)) (Compiler.CompactSourceSyntax.synCun P Y)) (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv k))))))) (p1858 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2)) (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv k))))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 1))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2)) (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv k))))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 5)))).imp (Compiler.CompactSourceSyntax.synWex (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2)) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv k)))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6)) (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 1))))))) (p1859 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2)) (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv k))))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 1))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2)) (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv k))))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 5)))).imp (SemanticCore.Wff.all (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2)) (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv k))))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 1))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2)) (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv k))))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 5))))))) (p1864 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2)) (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv k))))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 1))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2)) (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv k))))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 5)))) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2)) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv k)))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6)) (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 1))))).imp (Compiler.CompactSourceSyntax.synWex (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2)) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv k)))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7)) (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 5))))))) (p1865 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2)) (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv k))))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 1))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2)) (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv k))))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 5)))) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2)) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv k)))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6)) (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 1))))).imp (SemanticCore.Wff.all (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2)) (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv k))))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 1))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2)) (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv k))))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 5)))) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2)) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv k)))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6)) (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 1)))))))) (p1877 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2)) (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv k))))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 1))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2)) (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv k))))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 5)))) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2)) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv k)))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6)) (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 1))))) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2)) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv k)))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7)) (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 5))))).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 1)) (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6)))))) (p1890 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2)) (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv k))))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 1))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2)) (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv k))))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 5)))) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2)) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv k)))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 6)) (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 1))))) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2)) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv k)))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7)) (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 5))))).imp (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2)) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv k)))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7)) (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 5)))))) (p1904 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWf1 (SemanticCore.Class.cv k) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)) Y).imp ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2)) (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv k))))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 1))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2)) (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv k))))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 5)))) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ ⋯.fv ∪ ⋯ ∪ ⋯) ⋯)) ⋯ ⋯) ⋯)) ⋯).imp ⋯))) (p1915 : ⋯) (p1934 : ⋯) (p1943 : ⋯) (p1945 : ⋯) (p1953 : ⋯) (p1958 : ⋯) (p1963 : ⋯) (p1966 : ⋯) (p1968 : ⋯) {Result : ⋯} (continuation : ⋯) :
⋯

Checked nominal proof certificate identified upstream as g_cfbhnqinjcodecoverddndv_stage7.

Instances For

    Certificates from ReplaySupport.CodeCover8.

    source
    noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCfbhnqinjcodecoverddndvStage8 (u : SemanticCore.Var) (P : SemanticCore.Class) (k : SemanticCore.Var) (Y : SemanticCore.Class) (hyp_cfbhnqinjcodecoverddndv_2 : Nominal.NPrf (SemanticCore.Wff.classMem Y Compiler.CompactSourceSyntax.synCvv)) (p0286 : 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.synChncodetrnfn (SemanticCore.Class.cv k)) (SemanticCore.Class.cv u)) (Compiler.CompactSourceSyntax.synChwcn (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv k))))))) (p0340 : 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.synChncodetrnfn (SemanticCore.Class.cv k)) (SemanticCore.Class.cv u)) (Compiler.CompactSourceSyntax.synChwcn Y))))) (p0346 : 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 (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWfn (Compiler.CompactSourceSyntax.synChnqinc Y (Compiler.CompactSourceSyntax.synCun P Y)) (Compiler.CompactSourceSyntax.synChnord Y)) (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCec (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChncodetrnfn (SemanticCore.Class.cv k)) (SemanticCore.Class.cv u)) (Compiler.CompactSourceSyntax.synChwniso Y)) (Compiler.CompactSourceSyntax.synChnord Y)))))) (p0348 : 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 Y (Compiler.CompactSourceSyntax.synCun P Y)) (Compiler.CompactSourceSyntax.synCec (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChncodetrnfn (SemanticCore.Class.cv k)) (SemanticCore.Class.cv u)) (Compiler.CompactSourceSyntax.synChwniso Y))) (Compiler.CompactSourceSyntax.synCrn (Compiler.CompactSourceSyntax.synChnqinc Y (Compiler.CompactSourceSyntax.synCun P Y))))))) (p0824 : 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.classEq (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.synCfv (Compiler.CompactSourceSyntax.synChnqinc (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)) (Compiler.CompactSourceSyntax.synCun P Y)) (Compiler.CompactSourceSyntax.synCec (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synChwniso (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u))))))))) (p1642 : 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.classEq (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChnqinc (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)) (Compiler.CompactSourceSyntax.synCun P Y)) (Compiler.CompactSourceSyntax.synCec (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synChwniso (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u))))) (Compiler.CompactSourceSyntax.synCec (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChncodetrnfn (SemanticCore.Class.cv k)) (SemanticCore.Class.cv u)) (Compiler.CompactSourceSyntax.synChwniso (Compiler.CompactSourceSyntax.synCun P Y))))))) (p1643 : Nominal.NPrf ((SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChncodetrnfn (SemanticCore.Class.cv k)) (SemanticCore.Class.cv u)) (Compiler.CompactSourceSyntax.synChwcn (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv k)))).imp (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChncodetrnfn (SemanticCore.Class.cv k)) (SemanticCore.Class.cv u)) Compiler.CompactSourceSyntax.synCvv))) (p1645 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChncodetrnfn (SemanticCore.Class.cv k)) (SemanticCore.Class.cv u)) Compiler.CompactSourceSyntax.synCvv) (Compiler.CompactSourceSyntax.synWex (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 4) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 4)) (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChncodetrnfn (SemanticCore.Class.cv k)) (SemanticCore.Class.cv u)))))) (p1649 : Nominal.NPrf ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 4)) (Compiler.CompactSourceSyntax.synChwcn (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv k)))).imp (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 4))) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synChwcn (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv k))))))) (p1789 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWf1 (SemanticCore.Class.cv k) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)) Y).imp ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 4)) (Compiler.CompactSourceSyntax.synChwcn (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv k)))).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv k))) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 4)))) (Compiler.CompactSourceSyntax.synCec (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 4)) (Compiler.CompactSourceSyntax.synChwniso (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv k)))))))) (p1790 : Nominal.NPrf ((SemanticCore.Wff.classEq (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 4)) (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChncodetrnfn (SemanticCore.Class.cv k)) (SemanticCore.Class.cv u))).imp (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 4)) (Compiler.CompactSourceSyntax.synChwcn (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv k)))) (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChncodetrnfn (SemanticCore.Class.cv k)) (SemanticCore.Class.cv u)) (Compiler.CompactSourceSyntax.synChwcn (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv k))))))) (p1793 : Nominal.NPrf ((SemanticCore.Wff.classEq (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 4)) (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChncodetrnfn (SemanticCore.Class.cv k)) (SemanticCore.Class.cv u))).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCec (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 4)) (Compiler.CompactSourceSyntax.synChwniso (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv k)))) (Compiler.CompactSourceSyntax.synCec (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChncodetrnfn (SemanticCore.Class.cv k)) (SemanticCore.Class.cv u)) (Compiler.CompactSourceSyntax.synChwniso (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv k))))))) (p1802 : Nominal.NPrf ((SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChncodetrnfn (SemanticCore.Class.cv k)) (SemanticCore.Class.cv u)) Compiler.CompactSourceSyntax.synCvv).imp (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChncodetrnfn (SemanticCore.Class.cv k)) (SemanticCore.Class.cv u)) Compiler.CompactSourceSyntax.synCvv))) (p1813 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWf1 (SemanticCore.Class.cv k) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)) Y).imp (Compiler.CompactSourceSyntax.synWfn (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv k))) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synChwcn (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv k))))))) (p1841 : 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 (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChncodetrnfn (SemanticCore.Class.cv k)) (SemanticCore.Class.cv u))) (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (Compiler.CompactSourceSyntax.synCec (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChncodetrnfn (SemanticCore.Class.cv k)) (SemanticCore.Class.cv u)) (Compiler.CompactSourceSyntax.synChwniso (Compiler.CompactSourceSyntax.synCun P Y))))))) (p1843 : Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChncodetrnfn (SemanticCore.Class.cv k)) (SemanticCore.Class.cv u))) Compiler.CompactSourceSyntax.synCvv)) (p1844 : Nominal.NPrf ((SemanticCore.Wff.classEq (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2)) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChncodetrnfn (SemanticCore.Class.cv k)) (SemanticCore.Class.cv u)))).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2)) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChncodetrnfn (SemanticCore.Class.cv k)) (SemanticCore.Class.cv u)))))) (p1847 : Nominal.NPrf ((SemanticCore.Wff.classEq (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2)) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChncodetrnfn (SemanticCore.Class.cv k)) (SemanticCore.Class.cv u)))).imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 2)) (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (Compiler.CompactSourceSyntax.synCec (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChncodetrnfn (SemanticCore.Class.cv k)) (SemanticCore.Class.cv u)) (Compiler.CompactSourceSyntax.synChwniso (Compiler.CompactSourceSyntax.synCun P Y)))) (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChncodetrnfn (SemanticCore.Class.cv k)) (SemanticCore.Class.cv u))) (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (Compiler.CompactSourceSyntax.synCec (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChncodetrnfn (SemanticCore.Class.cv k)) (SemanticCore.Class.cv u)) (Compiler.CompactSourceSyntax.synChwniso (Compiler.CompactSourceSyntax.synCun P Y))))))) (p1855 : 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 (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCec (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChncodetrnfn (SemanticCore.Class.cv k)) (SemanticCore.Class.cv u)) (Compiler.CompactSourceSyntax.synChwniso (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv k)))) (Compiler.CompactSourceSyntax.synChnqinc (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv k)) (Compiler.CompactSourceSyntax.synCun P Y)) (Compiler.CompactSourceSyntax.synCec (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChncodetrnfn (SemanticCore.Class.cv k)) (SemanticCore.Class.cv u)) (Compiler.CompactSourceSyntax.synChwniso (Compiler.CompactSourceSyntax.synCun P Y))))))) (p2292 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWf1 (SemanticCore.Class.cv k) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)) Y).imp (Compiler.CompactSourceSyntax.synWfun (Compiler.CompactSourceSyntax.synChnqinc (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv k)) (Compiler.CompactSourceSyntax.synCun P Y))))) (p2294 : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCdm (Compiler.CompactSourceSyntax.synChnqinc (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv k)) (Compiler.CompactSourceSyntax.synCun P Y))) (Compiler.CompactSourceSyntax.synCdm (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv k)))))))) (p2309 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWf1 (SemanticCore.Class.cv k) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)) Y).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCdm (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCun P Y)) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv k)))))) (Compiler.CompactSourceSyntax.synCrn (Compiler.CompactSourceSyntax.synChnqmap1 (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv k))))))) (p2310 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7)) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synChwcn (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv k))))) (Compiler.CompactSourceSyntax.synWrex (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 4) (Compiler.CompactSourceSyntax.synChwcn (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv k))) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 7)) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 4))))))) (p2311 : Nominal.NPrf ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 4)) (Compiler.CompactSourceSyntax.synChwcn (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv k)))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 4)) (Compiler.CompactSourceSyntax.synChwcn (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv k)))))) (p2312 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWf1 (SemanticCore.Class.cv k) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)) Y).imp ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 4)) (Compiler.CompactSourceSyntax.synChwcn (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv k)))).imp (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synChwniso (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv k))) Compiler.CompactSourceSyntax.synCvv)))) (p2314 : Nominal.NPrf ((SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synChwniso (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv k))) Compiler.CompactSourceSyntax.synCvv).imp ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 4)) (Compiler.CompactSourceSyntax.synChwcn (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv k)))).imp (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCec (SemanticCore.Class.cv (ReplaySupport.freshVar ({u} ∪ P.fv ∪ {k} ∪ Y.fv) 4)) (Compiler.CompactSourceSyntax.synChwniso (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv k)))) (Compiler.CompactSourceSyntax.synCqs (Compiler.CompactSourceSyntax.synChwcn (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv k))) (Compiler.CompactSourceSyntax.synChwniso (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv k)))))))) {Result : Type} (continuation : 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)))))) → Result) :
    Result

    Checked nominal proof certificate identified upstream as g_cfbhnqinjcodecoverddndv_stage8.

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