NF weak partition development: NominalWPPReplayChunk016Compact001Part051.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gPwpullwesetimpndvStage6 (x y f r : SemanticCore.Var) (p0000 : Nominal.NPrf Compiler.CompactSourceSyntax.synWtru) (p0115 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWtru.imp (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))) (p0440 : Nominal.NPrf ((SemanticCore.Wff.classEq (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 2)) (Compiler.CompactSourceSyntax.synCpwpull (SemanticCore.Class.cv f) (SemanticCore.Class.cv r))).imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 2)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 5))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}))) (Compiler.CompactSourceSyntax.synCpwpull (SemanticCore.Class.cv f) (SemanticCore.Class.cv r)) (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 5)))))) (p0607 : 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.synWbr (Compiler.CompactSourceSyntax.synCpwpull (SemanticCore.Class.cv f) (SemanticCore.Class.cv r)) Compiler.CompactSourceSyntax.synCantisym (SemanticCore.Class.cv x)))) (p0687 : 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.synWbr (Compiler.CompactSourceSyntax.synCpwpull (SemanticCore.Class.cv f) (SemanticCore.Class.cv r)) Compiler.CompactSourceSyntax.synCstrict (SemanticCore.Class.cv x)))) (p0690 : Nominal.NPrf ((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.synWne (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 8)) Compiler.CompactSourceSyntax.synC0))) (p0693 : Nominal.NPrf ((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.synWne (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 8)) Compiler.CompactSourceSyntax.synC0).imp (Compiler.CompactSourceSyntax.synWss (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 8)) (SemanticCore.Class.cv x))))) (p0694 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWne (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 8)) Compiler.CompactSourceSyntax.synC0) (Compiler.CompactSourceSyntax.synWss (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 8)) (SemanticCore.Class.cv x))) (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)))) (p0696 : Nominal.NPrf ((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 (SemanticCore.Wff.classMem (SemanticCore.Class.cv (ReplaySupport.freshVar ({x} ∪ {y} ∪ {f} ∪ {r}) 8)) Compiler.CompactSourceSyntax.synCvv))) (p0777 : Nominal.NPrf (SemanticCore.Wff.classEq Compiler.CompactSourceSyntax.synCwe (Compiler.CompactSourceSyntax.synCin Compiler.CompactSourceSyntax.synCstrict Compiler.CompactSourceSyntax.synCfound))) (p1293 : 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))))) (p1294 : 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)))) (p1299 : 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 : 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.synWbr (Compiler.CompactSourceSyntax.synCpwpull (SemanticCore.Class.cv f) (SemanticCore.Class.cv r)) Compiler.CompactSourceSyntax.synCwe (SemanticCore.Class.cv x))) → Result) : Result

Checked nominal proof certificate identified upstream as g_pwpullwesetimpndv_stage6.

Equations

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