Documentation

LeanPool.NFWeakPartition.Certificates.WellOrderPullbackBlock002

Nominal proof certificates grouped in dependency order.

Certificates from ReplaySupport.WellOrderPullback4.

source
noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gPwpullwesetimpndvStage4 (x y f r : SemanticCore.Var) (p0015 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv r) Compiler.CompactSourceSyntax.synCref (SemanticCore.Class.cv y)).imp (Compiler.CompactSourceSyntax.synWral (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1) (SemanticCore.Class.cv y) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1)) (SemanticCore.Class.cv r) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1)))))) (p0042 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWf1o (SemanticCore.Class.cv f) (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv r) Compiler.CompactSourceSyntax.synCwe (SemanticCore.Class.cv y))).imp (Compiler.CompactSourceSyntax.synWfun (SemanticCore.Class.cv f)))) (p0286 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv r) Compiler.CompactSourceSyntax.synCpartial (SemanticCore.Class.cv y)) (Compiler.CompactSourceSyntax.synW3a (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv r) Compiler.CompactSourceSyntax.synCref (SemanticCore.Class.cv y)) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv r) Compiler.CompactSourceSyntax.synCtrans (SemanticCore.Class.cv y)) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv r) Compiler.CompactSourceSyntax.synCantisym (SemanticCore.Class.cv y))))) (p0615 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv r) Compiler.CompactSourceSyntax.synCconnex (SemanticCore.Class.cv y)).imp (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv r) Compiler.CompactSourceSyntax.synCvv) (SemanticCore.Wff.classMem (SemanticCore.Class.cv y) Compiler.CompactSourceSyntax.synCvv)))) (p0766 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWf1o (SemanticCore.Class.cv f) (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv r) Compiler.CompactSourceSyntax.synCwe (SemanticCore.Class.cv y))).imp ((Compiler.CompactSourceSyntax.synWa Compiler.CompactSourceSyntax.synWtru (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWss (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))) (SemanticCore.Class.cv x)) (Compiler.CompactSourceSyntax.synWne (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))) Compiler.CompactSourceSyntax.synC0))).imp (Compiler.CompactSourceSyntax.synWne (SemanticCore.Class.cab (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 8) (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 8)) (SemanticCore.Class.cv y)) (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 8)) (Compiler.CompactSourceSyntax.synCima (SemanticCore.Class.cv f) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))))))) Compiler.CompactSourceSyntax.synC0)))) (p0769 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa Compiler.CompactSourceSyntax.synWtru (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWss (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))) (SemanticCore.Class.cv x)) (Compiler.CompactSourceSyntax.synWne (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))) Compiler.CompactSourceSyntax.synC0))).imp ((Compiler.CompactSourceSyntax.synWne (SemanticCore.Class.cab (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 8) (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 8)) (SemanticCore.Class.cv y)) (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 8)) (Compiler.CompactSourceSyntax.synCima (SemanticCore.Class.cv f) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))))))) Compiler.CompactSourceSyntax.synC0).imp (Compiler.CompactSourceSyntax.synWss (SemanticCore.Class.cab (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 8) (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 8)) (SemanticCore.Class.cv y)) (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 8)) (Compiler.CompactSourceSyntax.synCima (SemanticCore.Class.cv f) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))))))) (SemanticCore.Class.cv y))))) (p0770 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWne (SemanticCore.Class.cab (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 8) (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 8)) (SemanticCore.Class.cv y)) (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 8)) (Compiler.CompactSourceSyntax.synCima (SemanticCore.Class.cv f) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))))))) Compiler.CompactSourceSyntax.synC0) (Compiler.CompactSourceSyntax.synWss (SemanticCore.Class.cab (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 8) (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 8)) (SemanticCore.Class.cv y)) (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 8)) (Compiler.CompactSourceSyntax.synCima (SemanticCore.Class.cv f) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))))))) (SemanticCore.Class.cv y))) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWss (SemanticCore.Class.cab (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 8) (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 8)) (SemanticCore.Class.cv y)) (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 8)) (Compiler.CompactSourceSyntax.synCima (SemanticCore.Class.cv f) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))))))) (SemanticCore.Class.cv y)) (Compiler.CompactSourceSyntax.synWne (SemanticCore.Class.cab (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 8) (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 8)) (SemanticCore.Class.cv y)) (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 8)) (Compiler.CompactSourceSyntax.synCima (SemanticCore.Class.cv f) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))))))) Compiler.CompactSourceSyntax.synC0)))) (p0776 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWf1o (SemanticCore.Class.cv f) (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv r) Compiler.CompactSourceSyntax.synCwe (SemanticCore.Class.cv y))).imp ((Compiler.CompactSourceSyntax.synWa Compiler.CompactSourceSyntax.synWtru (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWss (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))) (SemanticCore.Class.cv x)) (Compiler.CompactSourceSyntax.synWne (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))) Compiler.CompactSourceSyntax.synC0))).imp (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv r) Compiler.CompactSourceSyntax.synCwe (SemanticCore.Class.cv y))))) (p0780 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv r) Compiler.CompactSourceSyntax.synCwe (SemanticCore.Class.cv y)) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv r) Compiler.CompactSourceSyntax.synCstrict (SemanticCore.Class.cv y)) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv r) Compiler.CompactSourceSyntax.synCfound (SemanticCore.Class.cv y))))) (p0782 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWf1o (SemanticCore.Class.cv f) (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv r) Compiler.CompactSourceSyntax.synCwe (SemanticCore.Class.cv y))).imp ((Compiler.CompactSourceSyntax.synWa Compiler.CompactSourceSyntax.synWtru (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWss (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))) (SemanticCore.Class.cv x)) (Compiler.CompactSourceSyntax.synWne (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))) Compiler.CompactSourceSyntax.synC0))).imp (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv r) Compiler.CompactSourceSyntax.synCfound (SemanticCore.Class.cv y))))) (p0801 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWf1o (SemanticCore.Class.cv f) (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv r) Compiler.CompactSourceSyntax.synCwe (SemanticCore.Class.cv y))).imp ((Compiler.CompactSourceSyntax.synWa Compiler.CompactSourceSyntax.synWtru (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWss (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))) (SemanticCore.Class.cv x)) (Compiler.CompactSourceSyntax.synWne (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))) Compiler.CompactSourceSyntax.synC0))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cab (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 8) (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 8)) (SemanticCore.Class.cv y)) (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 8)) (Compiler.CompactSourceSyntax.synCima (SemanticCore.Class.cv f) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))))))) Compiler.CompactSourceSyntax.synCvv)))) (p0802 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv r) Compiler.CompactSourceSyntax.synCfound (SemanticCore.Class.cv y)).imp (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv r) Compiler.CompactSourceSyntax.synCvv) (SemanticCore.Wff.classMem (SemanticCore.Class.cv y) Compiler.CompactSourceSyntax.synCvv)))) (p0807 : Nominal.NPrf ((SemanticCore.Wff.classEq (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 3)) (SemanticCore.Class.cv r)).imp (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.all (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1) ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWss (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 2))) (Compiler.CompactSourceSyntax.synWne (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1)) Compiler.CompactSourceSyntax.synC0)).imp (Compiler.CompactSourceSyntax.synWrex (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 9) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1)) (Compiler.CompactSourceSyntax.synWral (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 10) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1)) ((Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 10)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 3)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 9))).imp (SemanticCore.Wff.objEq (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 10) (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 9))))))) (SemanticCore.Wff.all (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1) ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWss (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 2))) (Compiler.CompactSourceSyntax.synWne (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1)) Compiler.CompactSourceSyntax.synC0)).imp (Compiler.CompactSourceSyntax.synWrex (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 9) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1)) (Compiler.CompactSourceSyntax.synWral (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 10) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1)) ((Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 10)) (SemanticCore.Class.cv r) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 9))).imp (SemanticCore.Wff.objEq (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 10) (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 9)))))))))) (p0811 : Nominal.NPrf ((SemanticCore.Wff.classEq (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 2)) (SemanticCore.Class.cv y)).imp (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.all (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1) ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWss (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 2))) (Compiler.CompactSourceSyntax.synWne (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1)) Compiler.CompactSourceSyntax.synC0)).imp (Compiler.CompactSourceSyntax.synWrex (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 9) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1)) (Compiler.CompactSourceSyntax.synWral (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 10) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1)) ((Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 10)) (SemanticCore.Class.cv r) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 9))).imp (SemanticCore.Wff.objEq (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 10) (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 9))))))) (SemanticCore.Wff.all (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1) ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWss (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1)) (SemanticCore.Class.cv y)) (Compiler.CompactSourceSyntax.synWne (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1)) Compiler.CompactSourceSyntax.synC0)).imp (Compiler.CompactSourceSyntax.synWrex (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 9) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1)) (Compiler.CompactSourceSyntax.synWral (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 10) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1)) ((Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 10)) (SemanticCore.Class.cv r) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 9))).imp (SemanticCore.Wff.objEq (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 10) (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 9)))))))))) (p0812 : Nominal.NPrf (SemanticCore.Wff.classEq Compiler.CompactSourceSyntax.synCfound (Compiler.CompactSourceSyntax.synCopab (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 3) (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 2) (SemanticCore.Wff.all (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1) ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWss (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 2))) (Compiler.CompactSourceSyntax.synWne (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1)) Compiler.CompactSourceSyntax.synC0)).imp (Compiler.CompactSourceSyntax.synWrex (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 9) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1)) (Compiler.CompactSourceSyntax.synWral (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 10) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1)) ((Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 10)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 3)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 9))).imp (SemanticCore.Wff.objEq (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 10) (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 9)))))))))) {Result : Type} (continuation : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa Compiler.CompactSourceSyntax.synWtru (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWss (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))) (SemanticCore.Class.cv x)) (Compiler.CompactSourceSyntax.synWne (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))) Compiler.CompactSourceSyntax.synC0))).imp (SemanticCore.Wff.all (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 9) (Compiler.CompactSourceSyntax.synWa Compiler.CompactSourceSyntax.synWtru (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWss (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))) (SemanticCore.Class.cv x)) (Compiler.CompactSourceSyntax.synWne (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))) Compiler.CompactSourceSyntax.synC0))))) → Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWf1o (SemanticCore.Class.cv f) (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv r) Compiler.CompactSourceSyntax.synCwe (SemanticCore.Class.cv y))).imp ((Compiler.CompactSourceSyntax.synWa Compiler.CompactSourceSyntax.synWtru (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWss (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))) (SemanticCore.Class.cv x)) (Compiler.CompactSourceSyntax.synWne (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))) Compiler.CompactSourceSyntax.synC0))).imp (Compiler.CompactSourceSyntax.synWrex (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 9) (SemanticCore.Class.cv y) (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 9)) (Compiler.CompactSourceSyntax.synCima (SemanticCore.Class.cv f) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))))) (Compiler.CompactSourceSyntax.synWral (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 10) (SemanticCore.Class.cv y) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 10)) (Compiler.CompactSourceSyntax.synCima (SemanticCore.Class.cv f) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))))).imp (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 9)) (SemanticCore.Class.cv r) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 10))))))))) → Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa Compiler.CompactSourceSyntax.synWtru (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWss (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))) (SemanticCore.Class.cv x)) (Compiler.CompactSourceSyntax.synWne (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))) Compiler.CompactSourceSyntax.synC0))) (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 9)) (SemanticCore.Class.cv y)) (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 9)) (Compiler.CompactSourceSyntax.synCima (SemanticCore.Class.cv f) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))))) (Compiler.CompactSourceSyntax.synWral (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 10) (SemanticCore.Class.cv y) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 10)) (Compiler.CompactSourceSyntax.synCima (SemanticCore.Class.cv f) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))))).imp (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 9)) (SemanticCore.Class.cv r) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 10)))))))).imp (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 9)) (Compiler.CompactSourceSyntax.synCima (SemanticCore.Class.cv f) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))))) (Compiler.CompactSourceSyntax.synWral (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 10) (SemanticCore.Class.cv y) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 10)) (Compiler.CompactSourceSyntax.synCima (SemanticCore.Class.cv f) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))))).imp (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 9)) (SemanticCore.Class.cv r) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 10))))))) → Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWf1o (SemanticCore.Class.cv f) (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv r) Compiler.CompactSourceSyntax.synCwe (SemanticCore.Class.cv y))).imp ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa Compiler.CompactSourceSyntax.synWtru (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWss (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))) (SemanticCore.Class.cv x)) (Compiler.CompactSourceSyntax.synWne (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))) Compiler.CompactSourceSyntax.synC0))) (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 9)) (SemanticCore.Class.cv y)) (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 9)) (Compiler.CompactSourceSyntax.synCima (SemanticCore.Class.cv f) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))))) (Compiler.CompactSourceSyntax.synWral (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 10) (SemanticCore.Class.cv y) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 10)) (Compiler.CompactSourceSyntax.synCima (SemanticCore.Class.cv f) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))))).imp (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 9)) (SemanticCore.Class.cv r) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 10)))))))).imp (Compiler.CompactSourceSyntax.synWrex (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 11) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))) (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv (SemanticCore.Class.cv f) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 11))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 9)))))) → Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa Compiler.CompactSourceSyntax.synWtru (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWss (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))) (SemanticCore.Class.cv x)) (Compiler.CompactSourceSyntax.synWne (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))) Compiler.CompactSourceSyntax.synC0))) (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 9)) (SemanticCore.Class.cv y)) (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 9)) (Compiler.CompactSourceSyntax.synCima (SemanticCore.Class.cv f) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))))) (Compiler.CompactSourceSyntax.synWral (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 10) (SemanticCore.Class.cv y) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 10)) (Compiler.CompactSourceSyntax.synCima (SemanticCore.Class.cv f) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))))).imp (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 9)) (SemanticCore.Class.cv r) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 10)))))))).imp (SemanticCore.Wff.all (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 11) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa Compiler.CompactSourceSyntax.synWtru (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWss (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))) (SemanticCore.Class.cv x)) (Compiler.CompactSourceSyntax.synWne (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))) Compiler.CompactSourceSyntax.synC0))) (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 9)) (SemanticCore.Class.cv y)) (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 9)) (Compiler.CompactSourceSyntax.synCima (SemanticCore.Class.cv f) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))))) (Compiler.CompactSourceSyntax.synWral (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 10) (SemanticCore.Class.cv y) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 10)) (Compiler.CompactSourceSyntax.synCima (SemanticCore.Class.cv f) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))))).imp (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 9)) (SemanticCore.Class.cv r) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 10)))))))))) → Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa Compiler.CompactSourceSyntax.synWtru (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWss (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))) (SemanticCore.Class.cv x)) (Compiler.CompactSourceSyntax.synWne (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))) Compiler.CompactSourceSyntax.synC0))) (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 9)) (SemanticCore.Class.cv y)) (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 9)) (Compiler.CompactSourceSyntax.synCima (SemanticCore.Class.cv f) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))))) (Compiler.CompactSourceSyntax.synWral (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 10) (SemanticCore.Class.cv y) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 10)) (Compiler.CompactSourceSyntax.synCima (SemanticCore.Class.cv f) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))))).imp (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 9)) (SemanticCore.Class.cv r) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 10)))))))) (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 11)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r})))) (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv (SemanticCore.Class.cv f) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 11))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 9))))).imp (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 11)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r})))) (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv (SemanticCore.Class.cv f) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 11))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 9))))) → Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa Compiler.CompactSourceSyntax.synWtru (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWss (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))) (SemanticCore.Class.cv x)) (Compiler.CompactSourceSyntax.synWne (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))) Compiler.CompactSourceSyntax.synC0))) (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 9)) (SemanticCore.Class.cv y)) (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 9)) (Compiler.CompactSourceSyntax.synCima (SemanticCore.Class.cv f) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))))) (Compiler.CompactSourceSyntax.synWral (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 10) (SemanticCore.Class.cv y) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 10)) (Compiler.CompactSourceSyntax.synCima (SemanticCore.Class.cv f) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))))).imp (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 9)) (SemanticCore.Class.cv r) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 10)))))))) (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 11)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r})))) (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv (SemanticCore.Class.cv f) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 11))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 9))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 11)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))))) → Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa Compiler.CompactSourceSyntax.synWtru (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWss (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))) (SemanticCore.Class.cv x)) (Compiler.CompactSourceSyntax.synWne (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))) Compiler.CompactSourceSyntax.synC0))) (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 9)) (SemanticCore.Class.cv y)) (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 9)) (Compiler.CompactSourceSyntax.synCima (SemanticCore.Class.cv f) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))))) (Compiler.CompactSourceSyntax.synWral (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 10) (SemanticCore.Class.cv y) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 10)) (Compiler.CompactSourceSyntax.synCima (SemanticCore.Class.cv f) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))))).imp (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 9)) (SemanticCore.Class.cv r) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 10)))))))) (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 11)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r})))) (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv (SemanticCore.Class.cv f) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 11))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 9))))) (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))))).imp ((Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1)) (Compiler.CompactSourceSyntax.synCdif (Compiler.CompactSourceSyntax.synCpwpull (SemanticCore.Class.cv f) (SemanticCore.Class.cv r)) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCpwpull (SemanticCore.Class.cv f) (SemanticCore.Class.cv r)))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 11))).neg.neg.imp (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1)) (Compiler.CompactSourceSyntax.synCdif (Compiler.CompactSourceSyntax.synCpwpull (SemanticCore.Class.cv f) (SemanticCore.Class.cv r)) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCpwpull (SemanticCore.Class.cv f) (SemanticCore.Class.cv r)))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 11))))) → Result) :
Result

Checked nominal proof certificate identified upstream as g_pwpullwesetimpndv_stage4.

Instances For

    Certificates from ReplaySupport.WellOrderPullback5.

    source
    noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gPwpullwesetimpndvStage5 (x y f r : SemanticCore.Var) (p0000 : Nominal.NPrf Compiler.CompactSourceSyntax.synWtru) (p0036 : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCpwpull (SemanticCore.Class.cv f) (SemanticCore.Class.cv r)) (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f)) (SemanticCore.Class.cv r)) (SemanticCore.Class.cv f)))) (p0038 : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f))) (SemanticCore.Class.cv f))) (p0039 : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f)) (SemanticCore.Class.cv r)) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f)))) (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f)) (SemanticCore.Class.cv r)) (SemanticCore.Class.cv f)))) (p0042 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWf1o (SemanticCore.Class.cv f) (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv r) Compiler.CompactSourceSyntax.synCwe (SemanticCore.Class.cv y))).imp (Compiler.CompactSourceSyntax.synWfun (SemanticCore.Class.cv f)))) (p0045 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWf1o (SemanticCore.Class.cv f) (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv r) Compiler.CompactSourceSyntax.synCwe (SemanticCore.Class.cv y))).imp (Compiler.CompactSourceSyntax.synWfun (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f)))))) (p0047 : Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f)) Compiler.CompactSourceSyntax.synCvv)) (p0049 : Nominal.NPrf ((SemanticCore.Wff.classEq (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 4)) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f))).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 4))) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f)))))) (p0050 : Nominal.NPrf ((SemanticCore.Wff.classEq (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 4)) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f))).imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWfun (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 4)))) (Compiler.CompactSourceSyntax.synWfun (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f))))))) (p0055 : Nominal.NPrf ((SemanticCore.Wff.classEq (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 4)) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f))).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synCcom (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 4)) (SemanticCore.Class.cv r)) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 4)))) (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f)) (SemanticCore.Class.cv r)) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f))))))) (p0058 : Nominal.NPrf ((SemanticCore.Wff.classEq (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 4)) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f))).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 4))) (Compiler.CompactSourceSyntax.synCrn (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f)))))) (p0081 : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCrn (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f))) (Compiler.CompactSourceSyntax.synCdm (SemanticCore.Class.cv f)))) (p0101 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWf1o (SemanticCore.Class.cv f) (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv r) Compiler.CompactSourceSyntax.synCwe (SemanticCore.Class.cv y))).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCdm (SemanticCore.Class.cv f)) (SemanticCore.Class.cv x)))) (p0114 : Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCpwpull (SemanticCore.Class.cv f) (SemanticCore.Class.cv r)) Compiler.CompactSourceSyntax.synCvv)) (p0117 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWtru.imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) Compiler.CompactSourceSyntax.synCvv))) (p0162 : Nominal.NPrf ((SemanticCore.Wff.classEq (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 4)) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f))).imp (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1)) (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 4)))) (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1)) (Compiler.CompactSourceSyntax.synCrn (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f))))))) (p0169 : Nominal.NPrf ((SemanticCore.Wff.classEq (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 4)) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f))).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 4))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1))) (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1)))))) (p0185 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1)) (Compiler.CompactSourceSyntax.synCrn (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f)))) (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1)) (Compiler.CompactSourceSyntax.synCdm (SemanticCore.Class.cv f))))) (p0193 : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1))) (Compiler.CompactSourceSyntax.synCfv (SemanticCore.Class.cv f) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1))))) (p0201 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWf1o (SemanticCore.Class.cv f) (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv r) Compiler.CompactSourceSyntax.synCwe (SemanticCore.Class.cv y))).imp (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1)) (Compiler.CompactSourceSyntax.synCdm (SemanticCore.Class.cv f))) (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1)) (SemanticCore.Class.cv x))))) (p0318 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWf1o (SemanticCore.Class.cv f) (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv r) Compiler.CompactSourceSyntax.synCwe (SemanticCore.Class.cv y))).imp ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1)) (SemanticCore.Class.cv x)).imp (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCfv (SemanticCore.Class.cv f) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1))) (SemanticCore.Class.cv y))))) (p0709 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa Compiler.CompactSourceSyntax.synWtru (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWss (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))) (SemanticCore.Class.cv x)) (Compiler.CompactSourceSyntax.synWne (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))) Compiler.CompactSourceSyntax.synC0))).imp (Compiler.CompactSourceSyntax.synWss (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))) (SemanticCore.Class.cv x)))) (p0854 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa Compiler.CompactSourceSyntax.synWtru (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWss (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))) (SemanticCore.Class.cv x)) (Compiler.CompactSourceSyntax.synWne (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))) Compiler.CompactSourceSyntax.synC0))).imp (SemanticCore.Wff.all (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 9) (Compiler.CompactSourceSyntax.synWa Compiler.CompactSourceSyntax.synWtru (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWss (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))) (SemanticCore.Class.cv x)) (Compiler.CompactSourceSyntax.synWne (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))) Compiler.CompactSourceSyntax.synC0)))))) (p0978 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWf1o (SemanticCore.Class.cv f) (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv r) Compiler.CompactSourceSyntax.synCwe (SemanticCore.Class.cv y))).imp ((Compiler.CompactSourceSyntax.synWa Compiler.CompactSourceSyntax.synWtru (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWss (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))) (SemanticCore.Class.cv x)) (Compiler.CompactSourceSyntax.synWne (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))) Compiler.CompactSourceSyntax.synC0))).imp (Compiler.CompactSourceSyntax.synWrex (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 9) (SemanticCore.Class.cv y) (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 9)) (Compiler.CompactSourceSyntax.synCima (SemanticCore.Class.cv f) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))))) (Compiler.CompactSourceSyntax.synWral (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 10) (SemanticCore.Class.cv y) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 10)) (Compiler.CompactSourceSyntax.synCima (SemanticCore.Class.cv f) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))))).imp (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 9)) (SemanticCore.Class.cv r) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 10)))))))))) (p0984 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa Compiler.CompactSourceSyntax.synWtru (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWss (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))) (SemanticCore.Class.cv x)) (Compiler.CompactSourceSyntax.synWne (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))) Compiler.CompactSourceSyntax.synC0))) (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 9)) (SemanticCore.Class.cv y)) (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 9)) (Compiler.CompactSourceSyntax.synCima (SemanticCore.Class.cv f) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))))) (Compiler.CompactSourceSyntax.synWral (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 10) (SemanticCore.Class.cv y) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 10)) (Compiler.CompactSourceSyntax.synCima (SemanticCore.Class.cv f) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))))).imp (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 9)) (SemanticCore.Class.cv r) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 10)))))))).imp (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 9)) (Compiler.CompactSourceSyntax.synCima (SemanticCore.Class.cv f) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))))) (Compiler.CompactSourceSyntax.synWral (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 10) (SemanticCore.Class.cv y) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 10)) (Compiler.CompactSourceSyntax.synCima (SemanticCore.Class.cv f) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))))).imp (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 9)) (SemanticCore.Class.cv r) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 10)))))))) (p0992 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWf1o (SemanticCore.Class.cv f) (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv r) Compiler.CompactSourceSyntax.synCwe (SemanticCore.Class.cv y))).imp ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa Compiler.CompactSourceSyntax.synWtru (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWss (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))) (SemanticCore.Class.cv x)) (Compiler.CompactSourceSyntax.synWne (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))) Compiler.CompactSourceSyntax.synC0))) (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 9)) (SemanticCore.Class.cv y)) (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 9)) (Compiler.CompactSourceSyntax.synCima (SemanticCore.Class.cv f) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))))) (Compiler.CompactSourceSyntax.synWral (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 10) (SemanticCore.Class.cv y) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 10)) (Compiler.CompactSourceSyntax.synCima (SemanticCore.Class.cv f) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))))).imp (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 9)) (SemanticCore.Class.cv r) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 10)))))))).imp (Compiler.CompactSourceSyntax.synWrex (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 11) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))) (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv (SemanticCore.Class.cv f) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 11))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 9))))))) (p0994 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa Compiler.CompactSourceSyntax.synWtru (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWss (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))) (SemanticCore.Class.cv x)) (Compiler.CompactSourceSyntax.synWne (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))) Compiler.CompactSourceSyntax.synC0))) (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 9)) (SemanticCore.Class.cv y)) (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 9)) (Compiler.CompactSourceSyntax.synCima (SemanticCore.Class.cv f) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))))) (Compiler.CompactSourceSyntax.synWral (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 10) (SemanticCore.Class.cv y) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 10)) (Compiler.CompactSourceSyntax.synCima (SemanticCore.Class.cv f) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))))).imp (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 9)) (SemanticCore.Class.cv r) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 10)))))))).imp (SemanticCore.Wff.all (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 11) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa Compiler.CompactSourceSyntax.synWtru (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWss (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))) (SemanticCore.Class.cv x)) (Compiler.CompactSourceSyntax.synWne (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))) Compiler.CompactSourceSyntax.synC0))) (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 9)) (SemanticCore.Class.cv y)) (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 9)) (Compiler.CompactSourceSyntax.synCima (SemanticCore.Class.cv f) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))))) (Compiler.CompactSourceSyntax.synWral (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 10) (SemanticCore.Class.cv y) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 10)) (Compiler.CompactSourceSyntax.synCima (SemanticCore.Class.cv f) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))))).imp (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 9)) (SemanticCore.Class.cv r) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 10))))))))))) (p0995 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa Compiler.CompactSourceSyntax.synWtru (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWss (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))) (SemanticCore.Class.cv x)) (Compiler.CompactSourceSyntax.synWne (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))) Compiler.CompactSourceSyntax.synC0))) (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 9)) (SemanticCore.Class.cv y)) (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 9)) (Compiler.CompactSourceSyntax.synCima (SemanticCore.Class.cv f) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))))) (Compiler.CompactSourceSyntax.synWral (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 10) (SemanticCore.Class.cv y) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 10)) (Compiler.CompactSourceSyntax.synCima (SemanticCore.Class.cv f) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))))).imp (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 9)) (SemanticCore.Class.cv r) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 10)))))))) (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 11)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r})))) (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv (SemanticCore.Class.cv f) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 11))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 9))))).imp (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 11)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r})))) (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv (SemanticCore.Class.cv f) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 11))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 9)))))) (p0997 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa Compiler.CompactSourceSyntax.synWtru (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWss (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))) (SemanticCore.Class.cv x)) (Compiler.CompactSourceSyntax.synWne (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))) Compiler.CompactSourceSyntax.synC0))) (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 9)) (SemanticCore.Class.cv y)) (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 9)) (Compiler.CompactSourceSyntax.synCima (SemanticCore.Class.cv f) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))))) (Compiler.CompactSourceSyntax.synWral (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 10) (SemanticCore.Class.cv y) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 10)) (Compiler.CompactSourceSyntax.synCima (SemanticCore.Class.cv f) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))))).imp (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 9)) (SemanticCore.Class.cv r) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 10)))))))) (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 11)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r})))) (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv (SemanticCore.Class.cv f) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 11))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 9))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 11)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r})))))) (p1000 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa Compiler.CompactSourceSyntax.synWtru (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWss (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))) (SemanticCore.Class.cv x)) (Compiler.CompactSourceSyntax.synWne (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))) Compiler.CompactSourceSyntax.synC0))) (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 9)) (SemanticCore.Class.cv y)) (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 9)) (Compiler.CompactSourceSyntax.synCima (SemanticCore.Class.cv f) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))))) (Compiler.CompactSourceSyntax.synWral (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 10) (SemanticCore.Class.cv y) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 10)) (Compiler.CompactSourceSyntax.synCima (SemanticCore.Class.cv f) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))))).imp (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 9)) (SemanticCore.Class.cv r) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 10)))))))) (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 11)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r})))) (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv (SemanticCore.Class.cv f) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 11))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 9))))) (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))))).imp ((Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1)) (Compiler.CompactSourceSyntax.synCdif (Compiler.CompactSourceSyntax.synCpwpull (SemanticCore.Class.cv f) (SemanticCore.Class.cv r)) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCpwpull (SemanticCore.Class.cv f) (SemanticCore.Class.cv r)))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 11))).neg.neg.imp (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1)) (Compiler.CompactSourceSyntax.synCdif (Compiler.CompactSourceSyntax.synCpwpull (SemanticCore.Class.cv f) (SemanticCore.Class.cv r)) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCpwpull (SemanticCore.Class.cv f) (SemanticCore.Class.cv r)))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 11)))))) {Result : Type} (continuation : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWf1o (SemanticCore.Class.cv f) (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv r) Compiler.CompactSourceSyntax.synCwe (SemanticCore.Class.cv y))).imp ((Compiler.CompactSourceSyntax.synWa Compiler.CompactSourceSyntax.synWtru (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWss (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 8)) (SemanticCore.Class.cv x)) (Compiler.CompactSourceSyntax.synWne (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 8)) Compiler.CompactSourceSyntax.synC0))).imp (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCdif (Compiler.CompactSourceSyntax.synCpwpull (SemanticCore.Class.cv f) (SemanticCore.Class.cv r)) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCpwpull (SemanticCore.Class.cv f) (SemanticCore.Class.cv r)))) Compiler.CompactSourceSyntax.synCfound (SemanticCore.Class.cv x)))) → Nominal.NPrf ((Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCdif (Compiler.CompactSourceSyntax.synCpwpull (SemanticCore.Class.cv f) (SemanticCore.Class.cv r)) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCpwpull (SemanticCore.Class.cv f) (SemanticCore.Class.cv r)))) Compiler.CompactSourceSyntax.synCfound (SemanticCore.Class.cv x)).imp (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCdif (Compiler.CompactSourceSyntax.synCpwpull (SemanticCore.Class.cv f) (SemanticCore.Class.cv r)) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCpwpull (SemanticCore.Class.cv f) (SemanticCore.Class.cv r)))) Compiler.CompactSourceSyntax.synCvv) (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) Compiler.CompactSourceSyntax.synCvv))) → Nominal.NPrf ((SemanticCore.Wff.classEq (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 2)) (Compiler.CompactSourceSyntax.synCdif (Compiler.CompactSourceSyntax.synCpwpull (SemanticCore.Class.cv f) (SemanticCore.Class.cv r)) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCpwpull (SemanticCore.Class.cv f) (SemanticCore.Class.cv r))))).imp (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.all (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r})) ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWss (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1))) (Compiler.CompactSourceSyntax.synWne (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))) Compiler.CompactSourceSyntax.synC0)).imp (Compiler.CompactSourceSyntax.synWrex (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 5) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))) (Compiler.CompactSourceSyntax.synWral (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 9) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))) ((Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 9)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 2)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 5))).imp (SemanticCore.Wff.objEq (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 9) (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 5))))))) (SemanticCore.Wff.all (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r})) ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWss (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 1))) (Compiler.CompactSourceSyntax.synWne (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))) Compiler.CompactSourceSyntax.synC0)).imp (Compiler.CompactSourceSyntax.synWrex (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 5) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))) (Compiler.CompactSourceSyntax.synWral (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 9) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))) ((Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 9)) (Compiler.CompactSourceSyntax.synCdif (Compiler.CompactSourceSyntax.synCpwpull (SemanticCore.Class.cv f) (SemanticCore.Class.cv r)) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCpwpull (SemanticCore.Class.cv f) (SemanticCore.Class.cv r)))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 5))).imp (SemanticCore.Wff.objEq (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 9) (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 5))))))))) → Result) :
    Result

    Checked nominal proof certificate identified upstream as g_pwpullwesetimpndv_stage5.

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