Nominal proof certificates grouped in dependency order.

Certificates from NominalWPPReplayChunk017Compact001Part012.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWppfdpivrangencdlitraw (A B R : SemanticCore.Class) (dv_A_B : Disjoint A.fv B.fv) (dv_A_R : Disjoint A.fv R.fv) (dv_B_R : Disjoint B.fv R.fv) (hyp_wppfdpivrangencdlitraw_1 : Nominal.NPrf (SemanticCore.Wff.classMem R Compiler.CompactSourceSyntax.synCvv)) (hyp_wppfdpivrangencdlitraw_2 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) (hyp_wppfdpivrangencdlitraw_3 : Nominal.NPrf (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWwpp.imp (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCnc (Compiler.CompactSourceSyntax.synCfdpivrange2 R A B)) Compiler.CompactSourceSyntax.synClec (Compiler.CompactSourceSyntax.synCnc (Compiler.CompactSourceSyntax.synCxp (Compiler.CompactSourceSyntax.synCxpk B B) Compiler.CompactSourceSyntax.synCnnc))))

Checked nominal proof certificate identified upstream as g_wppfdpivrangencdlitraw.

Equations

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

Certificates from NominalWPPReplayChunk017Compact001Part013.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHncardsuccshiftedndv (R : SemanticCore.Class) (hyp_hncardsuccshiftedndv_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCwe (Compiler.CompactSourceSyntax.synChnord (Compiler.CompactSourceSyntax.synCpw (Compiler.CompactSourceSyntax.synCpw (Compiler.CompactSourceSyntax.synChnord (Compiler.CompactSourceSyntax.synCpw1 Compiler.CompactSourceSyntax.synC1c))))))) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synChncard (Compiler.CompactSourceSyntax.synCpw (Compiler.CompactSourceSyntax.synCpw (Compiler.CompactSourceSyntax.synChnord (Compiler.CompactSourceSyntax.synCpw1 Compiler.CompactSourceSyntax.synC1c))))))) Compiler.CompactSourceSyntax.synClec (Compiler.CompactSourceSyntax.synChncard (Compiler.CompactSourceSyntax.synChnord (Compiler.CompactSourceSyntax.synCpw (Compiler.CompactSourceSyntax.synCpw (Compiler.CompactSourceSyntax.synChnord (Compiler.CompactSourceSyntax.synCpw1 Compiler.CompactSourceSyntax.synC1c)))))))

Checked nominal proof certificate identified upstream as g_hncardsuccshiftedndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gKqrelimakndv (A B : SemanticCore.Class) (_dv_A_B : Disjoint A.fv B.fv) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCkqrel A) B) (Compiler.CompactSourceSyntax.synCimak A B))

Checked nominal proof certificate identified upstream as g_kqrelimakndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWppqkrelresrangevalndv (A : SemanticCore.Class) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCrn (Compiler.CompactSourceSyntax.synCres (Compiler.CompactSourceSyntax.synCkqrel Compiler.CompactSourceSyntax.synCwppqkrelkernel) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 A)))) (Compiler.CompactSourceSyntax.synCqkrel A))

Checked nominal proof certificate identified upstream as g_wppqkrelresrangevalndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWppqkrelkernelpointbrndv (A B C : SemanticCore.Class) (hyp_wppqkrelkernelpointbrndv_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) (hyp_wppqkrelkernelpointbrndv_2 : Nominal.NPrf (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCvv)) (hyp_wppqkrelkernelpointbrndv_3 : Nominal.NPrf (SemanticCore.Wff.classMem C Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCop (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCsn A)) (Compiler.CompactSourceSyntax.synCopk B C)) (Compiler.CompactSourceSyntax.synCkqrel Compiler.CompactSourceSyntax.synCwppqkrelkernel)) (SemanticCore.Wff.classEq A (Compiler.CompactSourceSyntax.synCop B C)))

Checked nominal proof certificate identified upstream as g_wppqkrelkernelpointbrndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWppqkrelkernelrangeformndv (A D : SemanticCore.Class) (_hyp_wppqkrelkernelrangeformndv_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) (hyp_wppqkrelkernelrangeformndv_2 : Nominal.NPrf (SemanticCore.Wff.classMem D Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf ((SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCop (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCsn A)) D) (Compiler.CompactSourceSyntax.synCkqrel Compiler.CompactSourceSyntax.synCwppqkrelkernel)).imp (SemanticCore.Wff.classMem D (Compiler.CompactSourceSyntax.synCxpk Compiler.CompactSourceSyntax.synCvv Compiler.CompactSourceSyntax.synCvv)))

Checked nominal proof certificate identified upstream as g_wppqkrelkernelrangeformndv.

Equations

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

Certificates from NominalWPPReplayChunk017Compact001Part014.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWppqkrelcanonicalfiberndv (A B D : SemanticCore.Class) (hyp_wppqkrelcanonicalfiberndv_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) (hyp_wppqkrelcanonicalfiberndv_2 : Nominal.NPrf (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCvv)) (hyp_wppqkrelcanonicalfiberndv_3 : Nominal.NPrf (SemanticCore.Wff.classMem D Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCop (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCop A B))) D) (Compiler.CompactSourceSyntax.synCkqrel Compiler.CompactSourceSyntax.synCwppqkrelkernel)) (SemanticCore.Wff.classEq D (Compiler.CompactSourceSyntax.synCopk A B)))

Checked nominal proof certificate identified upstream as g_wppqkrelcanonicalfiberndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWppqkrelcanonicaleu (A B : SemanticCore.Class) (d : SemanticCore.Var) (dv_A_d : d ∉ A.fv) (dv_B_d : d ∉ B.fv) (hyp_wppqkrelcanonicaleu_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) (hyp_wppqkrelcanonicaleu_2 : Nominal.NPrf (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWeu d (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCop (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCop A B))) (SemanticCore.Class.cv d)) (Compiler.CompactSourceSyntax.synCkqrel Compiler.CompactSourceSyntax.synCwppqkrelkernel)))

Checked nominal proof certificate identified upstream as g_wppqkrelcanonicaleu.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWppqkrelresfnndv (A B : SemanticCore.Class) (_hyp_wppqkrelresfnndv_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) (_hyp_wppqkrelresfnndv_2 : Nominal.NPrf (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWfn (Compiler.CompactSourceSyntax.synCres (Compiler.CompactSourceSyntax.synCkqrel Compiler.CompactSourceSyntax.synCwppqkrelkernel) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCxp A B)))) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCxp A B))))

Checked nominal proof certificate identified upstream as g_wppqkrelresfnndv.

Equations

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