Nominal proof certificates grouped in dependency order.
Certificates from NominalWPPReplayChunk017Compact001Part065.
noncomputable def
NFChoice.DirectNominalPrf.WPPReplay.gWppstopgammafixedhwdndv
(x y : SemanticCore.Var)
(C F : SemanticCore.Class)
(p : SemanticCore.Var)
(dv_C_p : p ∉ C.fv)
(dv_C_x : x ∉ C.fv)
(dv_C_y : y ∉ C.fv)
(dv_F_p : p ∉ F.fv)
(dv_F_x : x ∉ F.fv)
(dv_F_y : y ∉ F.fv)
(dv_p_x : p ≠ x)
(_dv_p_y : p ≠ y)
(_dv_x_y : x ≠ y)
(hyp_wppstopgammafixedhwdndv_1 : Nominal.NPrf (SemanticCore.Wff.classMem F Compiler.CompactSourceSyntax.synCfuns))
(hyp_wppstopgammafixedhwdndv_2 :
Nominal.NPrf
(Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCrn F)
(Compiler.CompactSourceSyntax.synChwcards Compiler.CompactSourceSyntax.synCvv)))
(hyp_wppstopgammafixedhwdndv_3 :
Nominal.NPrf
(SemanticCore.Wff.classMem C (Compiler.CompactSourceSyntax.synChwcards Compiler.CompactSourceSyntax.synCvv)))
(hyp_wppstopgammafixedhwdndv_4 :
Nominal.NPrf
(Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCtc C) Compiler.CompactSourceSyntax.synClec
C))
(hyp_wppstopgammafixedhwdndv_5 :
Nominal.NPrf
(Compiler.CompactSourceSyntax.synWral p
(Compiler.CompactSourceSyntax.synChwcards Compiler.CompactSourceSyntax.synCvv)
((Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv p) Compiler.CompactSourceSyntax.synClec C).imp
(SemanticCore.Wff.classMem (SemanticCore.Class.cv p) (Compiler.CompactSourceSyntax.synCdm F)))))
(hyp_wppstopgammafixedhwdndv_6 :
Nominal.NPrf
(Compiler.CompactSourceSyntax.synWral x
(Compiler.CompactSourceSyntax.synCdm (Compiler.CompactSourceSyntax.synCwppstopstep F C))
(SemanticCore.Wff.classEq
(Compiler.CompactSourceSyntax.synCtc
(Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCwppstopstep F C)
(SemanticCore.Class.cv x)))
(Compiler.CompactSourceSyntax.synCfv
(Compiler.CompactSourceSyntax.synCwppstopstep F (Compiler.CompactSourceSyntax.synCtc C))
(Compiler.CompactSourceSyntax.synCtc (SemanticCore.Class.cv x))))))
:
Nominal.NPrf
((Compiler.CompactSourceSyntax.synWral y
(Compiler.CompactSourceSyntax.synCdm (Compiler.CompactSourceSyntax.synCwppstopstep F C))
((Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCtc C)
Compiler.CompactSourceSyntax.synClec (SemanticCore.Class.cv y)).imp
(Compiler.CompactSourceSyntax.synWbr C Compiler.CompactSourceSyntax.synClec
(Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCwppstopstep F C)
(SemanticCore.Class.cv y))))).imp
(Compiler.CompactSourceSyntax.synWa
(SemanticCore.Wff.classMem
(Compiler.CompactSourceSyntax.synCwppgamma (Compiler.CompactSourceSyntax.synCwppstopstep F C) C)
(Compiler.CompactSourceSyntax.synChwcards Compiler.CompactSourceSyntax.synCvv))
(SemanticCore.Wff.classEq
(Compiler.CompactSourceSyntax.synCtc
(Compiler.CompactSourceSyntax.synCwppgamma (Compiler.CompactSourceSyntax.synCwppstopstep F C) C))
(Compiler.CompactSourceSyntax.synCwppgamma (Compiler.CompactSourceSyntax.synCwppstopstep F C) C))))
Checked nominal proof certificate identified upstream as g_wppstopgammafixedhwdndv.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Certificates from NominalWPPReplayChunk017Compact001Part066.
noncomputable def
NFChoice.DirectNominalPrf.WPPReplay.gWppstopgammahwndv
(C F : SemanticCore.Class)
(hyp_wppstopgammahwndv_1 : Nominal.NPrf (SemanticCore.Wff.classMem F Compiler.CompactSourceSyntax.synCfuns))
(hyp_wppstopgammahwndv_2 :
Nominal.NPrf
(Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCrn F)
(Compiler.CompactSourceSyntax.synChwcards Compiler.CompactSourceSyntax.synCvv)))
(hyp_wppstopgammahwndv_3 :
Nominal.NPrf
(SemanticCore.Wff.classMem C (Compiler.CompactSourceSyntax.synChwcards Compiler.CompactSourceSyntax.synCvv)))
:
Checked nominal proof certificate identified upstream as g_wppstopgammahwndv.
Equations
- One or more equations did not get rendered due to their size.