Nominal proof certificates grouped in dependency order.
Certificates from NominalWPPReplayChunk010Compact001Part010.
noncomputable def
NFChoice.DirectNominalPrf.WPPReplay.gNnpweq
(A B : SemanticCore.Class)
(n : SemanticCore.Var)
(M : SemanticCore.Class)
(dv_A_n : n ∉ A.fv)
(dv_B_n : n ∉ B.fv)
(_dv_M_n : n ∉ M.fv)
:
Nominal.NPrf
((Compiler.CompactSourceSyntax.synW3a (SemanticCore.Wff.classMem M Compiler.CompactSourceSyntax.synCnnc)
(SemanticCore.Wff.classMem A M) (SemanticCore.Wff.classMem B M)).imp
(Compiler.CompactSourceSyntax.synWrex n Compiler.CompactSourceSyntax.synCnnc
(Compiler.CompactSourceSyntax.synWa
(SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCpw A) (SemanticCore.Class.cv n))
(SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCpw B) (SemanticCore.Class.cv n)))))
Checked nominal proof certificate identified upstream as g_nnpweq.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Certificates from NominalWPPReplayChunk010Compact001Part011.
noncomputable def
NFChoice.DirectNominalPrf.WPPReplay.gSrelk
(A B : SemanticCore.Class)
(hyp_srelk_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv))
(hyp_srelk_2 : Nominal.NPrf (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCvv))
:
Nominal.NPrf
(Compiler.CompactSourceSyntax.synWb
(SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCopk A B)
(Compiler.CompactSourceSyntax.synCin
(Compiler.CompactSourceSyntax.synCxpk Compiler.CompactSourceSyntax.synCnnc Compiler.CompactSourceSyntax.synCnnc)
(Compiler.CompactSourceSyntax.synCimak
(Compiler.CompactSourceSyntax.synCin
(Compiler.CompactSourceSyntax.synCins3k
(Compiler.CompactSourceSyntax.synCimak
(Compiler.CompactSourceSyntax.synCin
(Compiler.CompactSourceSyntax.synCins3k
(Compiler.CompactSourceSyntax.synCsik
(Compiler.CompactSourceSyntax.synCdif
(Compiler.CompactSourceSyntax.synCxpk
(Compiler.CompactSourceSyntax.synCpw Compiler.CompactSourceSyntax.synC1c)
Compiler.CompactSourceSyntax.synCvv)
(Compiler.CompactSourceSyntax.synCimak
(Compiler.CompactSourceSyntax.synCsymdif
(Compiler.CompactSourceSyntax.synCins3k Compiler.CompactSourceSyntax.synCssetk)
(Compiler.CompactSourceSyntax.synCins2k
(Compiler.CompactSourceSyntax.synCsik Compiler.CompactSourceSyntax.synCssetk)))
(Compiler.CompactSourceSyntax.synCpw1
(Compiler.CompactSourceSyntax.synCpw1
(Compiler.CompactSourceSyntax.synCpw1 Compiler.CompactSourceSyntax.synC1c)))))))
(Compiler.CompactSourceSyntax.synCins2k Compiler.CompactSourceSyntax.synCssetk))
(Compiler.CompactSourceSyntax.synCpw1
(Compiler.CompactSourceSyntax.synCpw1 Compiler.CompactSourceSyntax.synC1c))))
(Compiler.CompactSourceSyntax.synCins2k
(Compiler.CompactSourceSyntax.synCimak
(Compiler.CompactSourceSyntax.synCin
(Compiler.CompactSourceSyntax.synCins3k
(Compiler.CompactSourceSyntax.synCsik
(Compiler.CompactSourceSyntax.synCcompl
(Compiler.CompactSourceSyntax.synCimak
(Compiler.CompactSourceSyntax.synCsymdif
(Compiler.CompactSourceSyntax.synCins3k Compiler.CompactSourceSyntax.synCssetk)
(Compiler.CompactSourceSyntax.synCins2k
(Compiler.CompactSourceSyntax.synCsik Compiler.CompactSourceSyntax.synCssetk)))
(Compiler.CompactSourceSyntax.synCpw1
(Compiler.CompactSourceSyntax.synCpw1 Compiler.CompactSourceSyntax.synC1c))))))
(Compiler.CompactSourceSyntax.synCins2k Compiler.CompactSourceSyntax.synCssetk))
(Compiler.CompactSourceSyntax.synCpw1
(Compiler.CompactSourceSyntax.synCpw1 Compiler.CompactSourceSyntax.synC1c)))))
(Compiler.CompactSourceSyntax.synCpw1
(Compiler.CompactSourceSyntax.synCpw1
(Compiler.CompactSourceSyntax.synCpw1 Compiler.CompactSourceSyntax.synC1c))))))
(Compiler.CompactSourceSyntax.synWsfin A B))
Checked nominal proof certificate identified upstream as g_srelk.
Equations
- One or more equations did not get rendered due to their size.