Nominal proof certificates grouped in dependency order.

Certificates from NominalWPPReplayChunk017Compact001Part053.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWppconcrete6tchomdmndv (x : SemanticCore.Var) : Nominal.NPrf ((SemanticCore.Wff.classMem (SemanticCore.Class.cv x) (Compiler.CompactSourceSyntax.synCdm Compiler.CompactSourceSyntax.synCwppconcrete6fn)).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synCwppconcrete6fn (SemanticCore.Class.cv x))) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synCwppconcrete6fn (Compiler.CompactSourceSyntax.synCtc (SemanticCore.Class.cv x)))))

Checked nominal proof certificate identified upstream as g_wppconcrete6tchomdmndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWppstopstepexndv (C F : SemanticCore.Class) (hyp_wppstopstepexndv_1 : Nominal.NPrf (SemanticCore.Wff.classMem F Compiler.CompactSourceSyntax.synCfuns)) : Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCwppstopstep F C) Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_wppstopstepexndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWppstopstepmapndv (C F : SemanticCore.Class) (hyp_wppstopstepmapndv_1 : Nominal.NPrf (SemanticCore.Wff.classMem F Compiler.CompactSourceSyntax.synCfuns)) (hyp_wppstopstepmapndv_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCrn F) (Compiler.CompactSourceSyntax.synChwcards Compiler.CompactSourceSyntax.synCvv))) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWf (Compiler.CompactSourceSyntax.synCwppstopstep F C) (Compiler.CompactSourceSyntax.synChwcards Compiler.CompactSourceSyntax.synCvv) (Compiler.CompactSourceSyntax.synChwcards Compiler.CompactSourceSyntax.synCvv))

Checked nominal proof certificate identified upstream as g_wppstopstepmapndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWppstopstepfunsndv (C F : SemanticCore.Class) (hyp_wppstopstepfunsndv_1 : Nominal.NPrf (SemanticCore.Wff.classMem F Compiler.CompactSourceSyntax.synCfuns)) (hyp_wppstopstepfunsndv_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCrn F) (Compiler.CompactSourceSyntax.synChwcards Compiler.CompactSourceSyntax.synCvv))) : Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCwppstopstep F C) Compiler.CompactSourceSyntax.synCfuns)

Checked nominal proof certificate identified upstream as g_wppstopstepfunsndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWppstopstepdmndv (C F : SemanticCore.Class) (hyp_wppstopstepdmndv_1 : Nominal.NPrf (SemanticCore.Wff.classMem F Compiler.CompactSourceSyntax.synCfuns)) (hyp_wppstopstepdmndv_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCrn F) (Compiler.CompactSourceSyntax.synChwcards Compiler.CompactSourceSyntax.synCvv))) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCdm (Compiler.CompactSourceSyntax.synCwppstopstep F C)) (Compiler.CompactSourceSyntax.synChwcards Compiler.CompactSourceSyntax.synCvv))

Checked nominal proof certificate identified upstream as g_wppstopstepdmndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWppstopsteprndmndv (C F : SemanticCore.Class) (hyp_wppstopstepdmndv_1 : Nominal.NPrf (SemanticCore.Wff.classMem F Compiler.CompactSourceSyntax.synCfuns)) (hyp_wppstopstepdmndv_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCrn F) (Compiler.CompactSourceSyntax.synChwcards Compiler.CompactSourceSyntax.synCvv))) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCrn (Compiler.CompactSourceSyntax.synCwppstopstep F C)) (Compiler.CompactSourceSyntax.synCdm (Compiler.CompactSourceSyntax.synCwppstopstep F C)))

Checked nominal proof certificate identified upstream as g_wppstopsteprndmndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWppstopstepfvactclndv (A C F : SemanticCore.Class) (hyp_wppstopstepfvactclndv_1 : Nominal.NPrf (SemanticCore.Wff.classMem F Compiler.CompactSourceSyntax.synCfuns)) (hyp_wppstopstepfvactclndv_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCrn F) (Compiler.CompactSourceSyntax.synChwcards Compiler.CompactSourceSyntax.synCvv))) : Nominal.NPrf ((SemanticCore.Wff.classMem A (Compiler.CompactSourceSyntax.synCwppstopact F C)).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCwppstopstep F C) A) (Compiler.CompactSourceSyntax.synCfv F A)))

Checked nominal proof certificate identified upstream as g_wppstopstepfvactclndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWppstopstepfvidleclndv (A C F : SemanticCore.Class) (hyp_wppstopstepfvidleclndv_1 : Nominal.NPrf (SemanticCore.Wff.classMem F Compiler.CompactSourceSyntax.synCfuns)) (hyp_wppstopstepfvidleclndv_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCrn F) (Compiler.CompactSourceSyntax.synChwcards Compiler.CompactSourceSyntax.synCvv))) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem A (Compiler.CompactSourceSyntax.synChwcards Compiler.CompactSourceSyntax.synCvv)) (SemanticCore.Wff.classMem A (Compiler.CompactSourceSyntax.synCwppstopact F C)).neg).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCwppstopstep F C) A) A))

Checked nominal proof certificate identified upstream as g_wppstopstepfvidleclndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWppstopactlecbindv (A C F : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem A (Compiler.CompactSourceSyntax.synChwcards Compiler.CompactSourceSyntax.synCvv)) ((Compiler.CompactSourceSyntax.synWbr A Compiler.CompactSourceSyntax.synClec C).imp (SemanticCore.Wff.classMem A (Compiler.CompactSourceSyntax.synCdm F)))).imp (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem A (Compiler.CompactSourceSyntax.synCwppstopact F C)) (Compiler.CompactSourceSyntax.synWbr A Compiler.CompactSourceSyntax.synClec C)))

Checked nominal proof certificate identified upstream as g_wppstopactlecbindv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWppstopstepfvlecdndv (A C F : SemanticCore.Class) (hyp_wppstopstepfvlecdndv_1 : Nominal.NPrf (SemanticCore.Wff.classMem F Compiler.CompactSourceSyntax.synCfuns)) (hyp_wppstopstepfvlecdndv_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCrn F) (Compiler.CompactSourceSyntax.synChwcards Compiler.CompactSourceSyntax.synCvv))) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem A (Compiler.CompactSourceSyntax.synChwcards Compiler.CompactSourceSyntax.synCvv)) ((Compiler.CompactSourceSyntax.synWbr A Compiler.CompactSourceSyntax.synClec C).imp (SemanticCore.Wff.classMem A (Compiler.CompactSourceSyntax.synCdm F)))).imp ((Compiler.CompactSourceSyntax.synWbr A Compiler.CompactSourceSyntax.synClec C).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCwppstopstep F C) A) (Compiler.CompactSourceSyntax.synCfv F A))))

Checked nominal proof certificate identified upstream as g_wppstopstepfvlecdndv.

Equations

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

Certificates from NominalWPPReplayChunk017Compact001Part054.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWppstopstepfvnlecdndv (A C F : SemanticCore.Class) (hyp_wppstopstepfvnlecdndv_1 : Nominal.NPrf (SemanticCore.Wff.classMem F Compiler.CompactSourceSyntax.synCfuns)) (hyp_wppstopstepfvnlecdndv_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCrn F) (Compiler.CompactSourceSyntax.synChwcards Compiler.CompactSourceSyntax.synCvv))) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem A (Compiler.CompactSourceSyntax.synChwcards Compiler.CompactSourceSyntax.synCvv)) ((Compiler.CompactSourceSyntax.synWbr A Compiler.CompactSourceSyntax.synClec C).imp (SemanticCore.Wff.classMem A (Compiler.CompactSourceSyntax.synCdm F)))).imp ((Compiler.CompactSourceSyntax.synWbr A Compiler.CompactSourceSyntax.synClec C).neg.imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCwppstopstep F C) A) A)))

Checked nominal proof certificate identified upstream as g_wppstopstepfvnlecdndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWppstopsteptchomdndv (x : SemanticCore.Var) (C F : SemanticCore.Class) (hyp_wppstopsteptchomdndv_1 : Nominal.NPrf (SemanticCore.Wff.classMem F Compiler.CompactSourceSyntax.synCfuns)) (hyp_wppstopsteptchomdndv_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCrn F) (Compiler.CompactSourceSyntax.synChwcards Compiler.CompactSourceSyntax.synCvv))) (hyp_wppstopsteptchomdndv_3 : Nominal.NPrf (SemanticCore.Wff.classMem C (Compiler.CompactSourceSyntax.synChwcards Compiler.CompactSourceSyntax.synCvv))) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synW3a (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) (Compiler.CompactSourceSyntax.synChwcards Compiler.CompactSourceSyntax.synCvv)) ((Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv x) Compiler.CompactSourceSyntax.synClec C).imp (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) (Compiler.CompactSourceSyntax.synCdm F)) (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCtc (SemanticCore.Class.cv x)) (Compiler.CompactSourceSyntax.synCdm F)))) ((Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv x) Compiler.CompactSourceSyntax.synClec C).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCfv F (SemanticCore.Class.cv x))) (Compiler.CompactSourceSyntax.synCfv F (Compiler.CompactSourceSyntax.synCtc (SemanticCore.Class.cv x)))))).imp (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)))))

Checked nominal proof certificate identified upstream as g_wppstopsteptchomdndv.

Equations

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

Certificates from NominalWPPReplayChunk017Compact001Part055.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWppconcrete6stoppedtchomndv (x : SemanticCore.Var) (hyp_wppconcrete6stoppedtchomndv_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCrn Compiler.CompactSourceSyntax.synCwppconcrete6fn) (Compiler.CompactSourceSyntax.synChwcards Compiler.CompactSourceSyntax.synCvv))) (hyp_wppconcrete6stoppedtchomndv_2 : Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synChncard Compiler.CompactSourceSyntax.synC1c))))))) (Compiler.CompactSourceSyntax.synChwcards Compiler.CompactSourceSyntax.synCvv))) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWral x (Compiler.CompactSourceSyntax.synCdm (Compiler.CompactSourceSyntax.synCwppstopstep Compiler.CompactSourceSyntax.synCwppconcrete6fn (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synChncard Compiler.CompactSourceSyntax.synC1c))))))))) (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCwppstopstep Compiler.CompactSourceSyntax.synCwppconcrete6fn (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synChncard Compiler.CompactSourceSyntax.synC1c)))))))) (SemanticCore.Class.cv x))) (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCwppstopstep Compiler.CompactSourceSyntax.synCwppconcrete6fn (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synChncard Compiler.CompactSourceSyntax.synC1c))))))))) (Compiler.CompactSourceSyntax.synCtc (SemanticCore.Class.cv x)))))

Checked nominal proof certificate identified upstream as g_wppconcrete6stoppedtchomndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWppconcrete6rnhwcardsredndv (u : SemanticCore.Var) (hyp_wppconcrete6rnhwcardsredndv_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWral u Compiler.CompactSourceSyntax.synCvv (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synChncard (Compiler.CompactSourceSyntax.synChnord (Compiler.CompactSourceSyntax.synCpw (Compiler.CompactSourceSyntax.synCpw (SemanticCore.Class.cv u))))) (Compiler.CompactSourceSyntax.synChwcards Compiler.CompactSourceSyntax.synCvv)))) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCrn Compiler.CompactSourceSyntax.synCwppconcrete6fn) (Compiler.CompactSourceSyntax.synChwcards Compiler.CompactSourceSyntax.synCvv))

Checked nominal proof certificate identified upstream as g_wppconcrete6rnhwcardsredndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWppfreceqexndv (F G I : SemanticCore.Class) (hyp_wppfreceqexndv_1 : Nominal.NPrf (SemanticCore.Wff.classMem F Compiler.CompactSourceSyntax.synCfuns)) (hyp_wppfreceqexndv_2 : Nominal.NPrf (SemanticCore.Wff.classMem G Compiler.CompactSourceSyntax.synCfuns)) : Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCwppfreceq F G I) Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_wppfreceqexndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWppfreceqvalndv (n : SemanticCore.Var) (F G I : SemanticCore.Class) (hyp_wppfreceqvalndv_1 : Nominal.NPrf (SemanticCore.Wff.classMem F Compiler.CompactSourceSyntax.synCfuns)) (hyp_wppfreceqvalndv_2 : Nominal.NPrf (SemanticCore.Wff.classMem I (Compiler.CompactSourceSyntax.synCdm F))) (hyp_wppfreceqvalndv_3 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCrn F) (Compiler.CompactSourceSyntax.synCdm F))) (hyp_wppfreceqvalndv_4 : Nominal.NPrf (SemanticCore.Wff.classMem G Compiler.CompactSourceSyntax.synCfuns)) (hyp_wppfreceqvalndv_5 : Nominal.NPrf (SemanticCore.Wff.classMem I (Compiler.CompactSourceSyntax.synCdm G))) (hyp_wppfreceqvalndv_6 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCrn G) (Compiler.CompactSourceSyntax.synCdm G))) : Nominal.NPrf ((SemanticCore.Wff.classMem (SemanticCore.Class.cv n) Compiler.CompactSourceSyntax.synCnnc).imp (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (SemanticCore.Class.cv n) (Compiler.CompactSourceSyntax.synCwppfreceq F G I)) (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCfrec F I) (SemanticCore.Class.cv n)) (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCfrec G I) (SemanticCore.Class.cv n)))))

Checked nominal proof certificate identified upstream as g_wppfreceqvalndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWppfreceqvalclndv (B F G I : SemanticCore.Class) (hyp_wppfreceqvalclndv_1 : Nominal.NPrf (SemanticCore.Wff.classMem F Compiler.CompactSourceSyntax.synCfuns)) (hyp_wppfreceqvalclndv_2 : Nominal.NPrf (SemanticCore.Wff.classMem I (Compiler.CompactSourceSyntax.synCdm F))) (hyp_wppfreceqvalclndv_3 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCrn F) (Compiler.CompactSourceSyntax.synCdm F))) (hyp_wppfreceqvalclndv_4 : Nominal.NPrf (SemanticCore.Wff.classMem G Compiler.CompactSourceSyntax.synCfuns)) (hyp_wppfreceqvalclndv_5 : Nominal.NPrf (SemanticCore.Wff.classMem I (Compiler.CompactSourceSyntax.synCdm G))) (hyp_wppfreceqvalclndv_6 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCrn G) (Compiler.CompactSourceSyntax.synCdm G))) : Nominal.NPrf ((SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCnnc).imp (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem B (Compiler.CompactSourceSyntax.synCwppfreceq F G I)) (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCfrec F I) B) (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCfrec G I) B))))

Checked nominal proof certificate identified upstream as g_wppfreceqvalclndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWppfrecprefixeqexndv (k : SemanticCore.Var) (F G I : SemanticCore.Class) (hyp_wppfrecprefixeqexndv_1 : Nominal.NPrf (SemanticCore.Wff.classMem F Compiler.CompactSourceSyntax.synCfuns)) (hyp_wppfrecprefixeqexndv_2 : Nominal.NPrf (SemanticCore.Wff.classMem G Compiler.CompactSourceSyntax.synCfuns)) : Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCwppfrecprefixeq F G I k) Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_wppfrecprefixeqexndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWppfrecprefixeqvalndv (B : SemanticCore.Class) (k : SemanticCore.Var) (F G I : SemanticCore.Class) (hyp_wppfrecprefixeqvalndv_1 : Nominal.NPrf (SemanticCore.Wff.classMem F Compiler.CompactSourceSyntax.synCfuns)) (hyp_wppfrecprefixeqvalndv_2 : Nominal.NPrf (SemanticCore.Wff.classMem I (Compiler.CompactSourceSyntax.synCdm F))) (hyp_wppfrecprefixeqvalndv_3 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCrn F) (Compiler.CompactSourceSyntax.synCdm F))) (hyp_wppfrecprefixeqvalndv_4 : Nominal.NPrf (SemanticCore.Wff.classMem G Compiler.CompactSourceSyntax.synCfuns)) (hyp_wppfrecprefixeqvalndv_5 : Nominal.NPrf (SemanticCore.Wff.classMem I (Compiler.CompactSourceSyntax.synCdm G))) (hyp_wppfrecprefixeqvalndv_6 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCrn G) (Compiler.CompactSourceSyntax.synCdm G))) : Nominal.NPrf ((SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCnnc).imp (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem B (Compiler.CompactSourceSyntax.synCwppfrecprefixeq F G I k)) ((Compiler.CompactSourceSyntax.synWbr B (Compiler.CompactSourceSyntax.synCkqrel Compiler.CompactSourceSyntax.synClefin) (SemanticCore.Class.cv k)).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCfrec F I) B) (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCfrec G I) B)))))

Checked nominal proof certificate identified upstream as g_wppfrecprefixeqvalndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWppstopstepsamebelowdndv (y : SemanticCore.Var) (C F : SemanticCore.Class) (p : SemanticCore.Var) (dv_C_p : p ∉ C.fv) (dv_F_p : p ∉ F.fv) (dv_p_y : p ≠ y) (hyp_wppstopstepsamebelowdndv_1 : Nominal.NPrf (SemanticCore.Wff.classMem F Compiler.CompactSourceSyntax.synCfuns)) (hyp_wppstopstepsamebelowdndv_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCrn F) (Compiler.CompactSourceSyntax.synChwcards Compiler.CompactSourceSyntax.synCvv))) (hyp_wppstopstepsamebelowdndv_3 : Nominal.NPrf (SemanticCore.Wff.classMem C (Compiler.CompactSourceSyntax.synChwcards Compiler.CompactSourceSyntax.synCvv))) (hyp_wppstopstepsamebelowdndv_4 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCtc C) Compiler.CompactSourceSyntax.synClec C)) (hyp_wppstopstepsamebelowdndv_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))))) : Nominal.NPrf ((SemanticCore.Wff.classMem (SemanticCore.Class.cv y) (Compiler.CompactSourceSyntax.synChwcards Compiler.CompactSourceSyntax.synCvv)).imp ((Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv y) Compiler.CompactSourceSyntax.synClec (Compiler.CompactSourceSyntax.synCtc C)).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCwppstopstep F C) (SemanticCore.Class.cv y)) (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCwppstopstep F (Compiler.CompactSourceSyntax.synCtc C)) (SemanticCore.Class.cv y)))))

Checked nominal proof certificate identified upstream as g_wppstopstepsamebelowdndv.

Equations

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

Certificates from NominalWPPReplayChunk017Compact001Part056.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWppreachtchwboundedndv (x : SemanticCore.Var) (C F G : SemanticCore.Class) (r p d : SemanticCore.Var) (dv_C_p : p ∉ C.fv) (dv_C_r : r ∉ C.fv) (dv_C_x : x ∉ C.fv) (dv_F_p : p ∉ F.fv) (dv_F_r : r ∉ F.fv) (dv_F_x : x ∉ F.fv) (dv_G_p : p ∉ G.fv) (_dv_G_r : r ∉ G.fv) (dv_G_x : x ∉ G.fv) (dv_d_p : d ≠ p) (dv_d_r : d ≠ r) (dv_d_x : d ≠ x) (dv_p_r : p ≠ r) (_dv_p_x : p ≠ x) (_dv_r_x : r ≠ x) (hyp_wppreachtchwboundedndv_1 : Nominal.NPrf (SemanticCore.Wff.classMem F Compiler.CompactSourceSyntax.synCfuns)) (hyp_wppreachtchwboundedndv_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCrn F) (Compiler.CompactSourceSyntax.synCdm F))) (hyp_wppreachtchwboundedndv_3 : Nominal.NPrf (SemanticCore.Wff.classMem G Compiler.CompactSourceSyntax.synCfuns)) (hyp_wppreachtchwboundedndv_4 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCrn G) (Compiler.CompactSourceSyntax.synCdm G))) (hyp_wppreachtchwboundedndv_5 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWral x (Compiler.CompactSourceSyntax.synCdm F) (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCfv F (SemanticCore.Class.cv x))) (Compiler.CompactSourceSyntax.synCfv G (Compiler.CompactSourceSyntax.synCtc (SemanticCore.Class.cv x)))))) (hyp_wppreachtchwboundedndv_6 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWral p (Compiler.CompactSourceSyntax.synChwcards Compiler.CompactSourceSyntax.synCvv) ((Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv p) Compiler.CompactSourceSyntax.synClec C).imp (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv p) (Compiler.CompactSourceSyntax.synCdm F)) (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCtc (SemanticCore.Class.cv p)) (Compiler.CompactSourceSyntax.synCdm G)))))) (hyp_wppreachtchwboundedndv_7 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWral p (Compiler.CompactSourceSyntax.synChwcards Compiler.CompactSourceSyntax.synCvv) ((Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv p) Compiler.CompactSourceSyntax.synClec C).imp (Compiler.CompactSourceSyntax.synWral r Compiler.CompactSourceSyntax.synCnnc (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCfrec F (SemanticCore.Class.cv p)) (SemanticCore.Class.cv r)) Compiler.CompactSourceSyntax.synCncs))))) (hyp_wppreachtchwboundedndv_8 : Nominal.NPrf (SemanticCore.Wff.classMem C (Compiler.CompactSourceSyntax.synChwcards Compiler.CompactSourceSyntax.synCvv))) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv d) (Compiler.CompactSourceSyntax.synChwcards Compiler.CompactSourceSyntax.synCvv)) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv d) Compiler.CompactSourceSyntax.synClec C)).imp (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (SemanticCore.Class.cv d) (Compiler.CompactSourceSyntax.synCwppreach F C)) (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCtc (SemanticCore.Class.cv d)) (Compiler.CompactSourceSyntax.synCwppreach G (Compiler.CompactSourceSyntax.synCtc C)))))

Checked nominal proof certificate identified upstream as g_wppreachtchwboundedndv.

Equations

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

Certificates from NominalWPPReplayChunk017Compact001Part057.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWppcandtchwboundedimagebindv (x : SemanticCore.Var) (C : SemanticCore.Class) (k : SemanticCore.Var) (F G : SemanticCore.Class) (r p d : SemanticCore.Var) (dv_C_d : d ∉ C.fv) (dv_C_p : p ∉ C.fv) (dv_C_r : r ∉ C.fv) (dv_C_x : x ∉ C.fv) (dv_F_d : d ∉ F.fv) (dv_F_p : p ∉ F.fv) (dv_F_r : r ∉ F.fv) (dv_F_x : x ∉ F.fv) (dv_G_d : d ∉ G.fv) (dv_G_p : p ∉ G.fv) (dv_G_r : r ∉ G.fv) (dv_G_x : x ∉ G.fv) (dv_d_k : d ≠ k) (dv_d_p : d ≠ p) (dv_d_r : d ≠ r) (dv_d_x : d ≠ x) (_dv_k_p : k ≠ p) (_dv_k_r : k ≠ r) (_dv_k_x : k ≠ x) (dv_p_r : p ≠ r) (dv_p_x : p ≠ x) (dv_r_x : r ≠ x) (hyp_wppcandtchwboundedimagebindv_1 : Nominal.NPrf (SemanticCore.Wff.classMem F Compiler.CompactSourceSyntax.synCfuns)) (hyp_wppcandtchwboundedimagebindv_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCrn F) (Compiler.CompactSourceSyntax.synCdm F))) (hyp_wppcandtchwboundedimagebindv_3 : Nominal.NPrf (SemanticCore.Wff.classMem G Compiler.CompactSourceSyntax.synCfuns)) (hyp_wppcandtchwboundedimagebindv_4 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCrn G) (Compiler.CompactSourceSyntax.synCdm G))) (hyp_wppcandtchwboundedimagebindv_5 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWral x (Compiler.CompactSourceSyntax.synCdm F) (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCfv F (SemanticCore.Class.cv x))) (Compiler.CompactSourceSyntax.synCfv G (Compiler.CompactSourceSyntax.synCtc (SemanticCore.Class.cv x)))))) (hyp_wppcandtchwboundedimagebindv_6 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWral p (Compiler.CompactSourceSyntax.synChwcards Compiler.CompactSourceSyntax.synCvv) ((Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv p) Compiler.CompactSourceSyntax.synClec C).imp (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv p) (Compiler.CompactSourceSyntax.synCdm F)) (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCtc (SemanticCore.Class.cv p)) (Compiler.CompactSourceSyntax.synCdm G)))))) (hyp_wppcandtchwboundedimagebindv_7 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWral p (Compiler.CompactSourceSyntax.synChwcards Compiler.CompactSourceSyntax.synCvv) ((Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv p) Compiler.CompactSourceSyntax.synClec C).imp (Compiler.CompactSourceSyntax.synWral r Compiler.CompactSourceSyntax.synCnnc (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCfrec F (SemanticCore.Class.cv p)) (SemanticCore.Class.cv r)) Compiler.CompactSourceSyntax.synCncs))))) (hyp_wppcandtchwboundedimagebindv_8 : Nominal.NPrf (SemanticCore.Wff.classMem C (Compiler.CompactSourceSyntax.synChwcards Compiler.CompactSourceSyntax.synCvv))) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (SemanticCore.Class.cv k) (Compiler.CompactSourceSyntax.synCwppcand G (Compiler.CompactSourceSyntax.synCtc C))) (Compiler.CompactSourceSyntax.synWex d (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv d) (Compiler.CompactSourceSyntax.synCwppcand F C)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv k) (Compiler.CompactSourceSyntax.synCtc (SemanticCore.Class.cv d))))))

Checked nominal proof certificate identified upstream as g_wppcandtchwboundedimagebindv.

Equations

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

Certificates from NominalWPPReplayChunk017Compact001Part058.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWppgammatchwboundedeqndv (x : SemanticCore.Var) (C F G : SemanticCore.Class) (r p : SemanticCore.Var) (dv_C_p : p ∉ C.fv) (dv_C_r : r ∉ C.fv) (dv_C_x : x ∉ C.fv) (dv_F_p : p ∉ F.fv) (dv_F_r : r ∉ F.fv) (dv_F_x : x ∉ F.fv) (dv_G_p : p ∉ G.fv) (dv_G_r : r ∉ G.fv) (dv_G_x : x ∉ G.fv) (dv_p_r : p ≠ r) (dv_p_x : p ≠ x) (dv_r_x : r ≠ x) (hyp_wppgammatchwboundedeqndv_1 : Nominal.NPrf (SemanticCore.Wff.classMem F Compiler.CompactSourceSyntax.synCfuns)) (hyp_wppgammatchwboundedeqndv_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCrn F) (Compiler.CompactSourceSyntax.synCdm F))) (hyp_wppgammatchwboundedeqndv_3 : Nominal.NPrf (SemanticCore.Wff.classMem G Compiler.CompactSourceSyntax.synCfuns)) (hyp_wppgammatchwboundedeqndv_4 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCrn G) (Compiler.CompactSourceSyntax.synCdm G))) (hyp_wppgammatchwboundedeqndv_5 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWral x (Compiler.CompactSourceSyntax.synCdm F) (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCfv F (SemanticCore.Class.cv x))) (Compiler.CompactSourceSyntax.synCfv G (Compiler.CompactSourceSyntax.synCtc (SemanticCore.Class.cv x)))))) (hyp_wppgammatchwboundedeqndv_6 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWral p (Compiler.CompactSourceSyntax.synChwcards Compiler.CompactSourceSyntax.synCvv) ((Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv p) Compiler.CompactSourceSyntax.synClec C).imp (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv p) (Compiler.CompactSourceSyntax.synCdm F)) (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCtc (SemanticCore.Class.cv p)) (Compiler.CompactSourceSyntax.synCdm G)))))) (hyp_wppgammatchwboundedeqndv_7 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWral p (Compiler.CompactSourceSyntax.synChwcards Compiler.CompactSourceSyntax.synCvv) ((Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv p) Compiler.CompactSourceSyntax.synClec C).imp (Compiler.CompactSourceSyntax.synWral r Compiler.CompactSourceSyntax.synCnnc (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCfrec F (SemanticCore.Class.cv p)) (SemanticCore.Class.cv r)) Compiler.CompactSourceSyntax.synCncs))))) (hyp_wppgammatchwboundedeqndv_8 : Nominal.NPrf (SemanticCore.Wff.classMem C (Compiler.CompactSourceSyntax.synChwcards Compiler.CompactSourceSyntax.synCvv))) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCwppgamma F C)) (Compiler.CompactSourceSyntax.synCwppgamma G (Compiler.CompactSourceSyntax.synCtc C)))

Checked nominal proof certificate identified upstream as g_wppgammatchwboundedeqndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWppgammadomhwndv (C F : SemanticCore.Class) (p : SemanticCore.Var) (dv_C_p : p ∉ C.fv) (dv_F_p : p ∉ F.fv) (hyp_wppgammadomhwndv_1 : Nominal.NPrf (SemanticCore.Wff.classMem F Compiler.CompactSourceSyntax.synCvv)) (hyp_wppgammadomhwndv_2 : 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_wppgammadomhwndv_3 : Nominal.NPrf (SemanticCore.Wff.classMem C (Compiler.CompactSourceSyntax.synChwcards Compiler.CompactSourceSyntax.synCvv))) : Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCwppgamma F C) (Compiler.CompactSourceSyntax.synCdm F))

Checked nominal proof certificate identified upstream as g_wppgammadomhwndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWppgammareachexhwndv (C : SemanticCore.Class) (n : SemanticCore.Var) (F : SemanticCore.Class) (p : SemanticCore.Var) (dv_C_n : n ∉ C.fv) (dv_C_p : p ∉ C.fv) (dv_F_n : n ∉ F.fv) (dv_F_p : p ∉ F.fv) (_dv_n_p : n ≠ p) (hyp_wppgammareachexhwndv_1 : Nominal.NPrf (SemanticCore.Wff.classMem F Compiler.CompactSourceSyntax.synCfuns)) (hyp_wppgammareachexhwndv_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCrn F) (Compiler.CompactSourceSyntax.synCdm F))) (hyp_wppgammareachexhwndv_3 : 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_wppgammareachexhwndv_4 : Nominal.NPrf (SemanticCore.Wff.classMem C (Compiler.CompactSourceSyntax.synChwcards Compiler.CompactSourceSyntax.synCvv))) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWrex n Compiler.CompactSourceSyntax.synCnnc (Compiler.CompactSourceSyntax.synWbr C Compiler.CompactSourceSyntax.synClec (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCfrec F (Compiler.CompactSourceSyntax.synCwppgamma F C)) (SemanticCore.Class.cv n))))

Checked nominal proof certificate identified upstream as g_wppgammareachexhwndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWppgammaleasthithwndv (C : SemanticCore.Class) (m n : SemanticCore.Var) (F : SemanticCore.Class) (p : SemanticCore.Var) (dv_C_m : m ∉ C.fv) (dv_C_n : n ∉ C.fv) (dv_C_p : p ∉ C.fv) (dv_F_m : m ∉ F.fv) (dv_F_n : n ∉ F.fv) (dv_F_p : p ∉ F.fv) (dv_m_n : m ≠ n) (hyp_wppgammaleasthithwndv_1 : Nominal.NPrf (SemanticCore.Wff.classMem F Compiler.CompactSourceSyntax.synCfuns)) (hyp_wppgammaleasthithwndv_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCrn F) (Compiler.CompactSourceSyntax.synCdm F))) (hyp_wppgammaleasthithwndv_3 : 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_wppgammaleasthithwndv_4 : Nominal.NPrf (SemanticCore.Wff.classMem C (Compiler.CompactSourceSyntax.synChwcards Compiler.CompactSourceSyntax.synCvv))) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWrex m Compiler.CompactSourceSyntax.synCnnc (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv m) (Compiler.CompactSourceSyntax.synCwpphit F (Compiler.CompactSourceSyntax.synCwppgamma F C) C)) (Compiler.CompactSourceSyntax.synWral n Compiler.CompactSourceSyntax.synCnnc ((SemanticCore.Wff.classMem (SemanticCore.Class.cv n) (Compiler.CompactSourceSyntax.synCwpphit F (Compiler.CompactSourceSyntax.synCwppgamma F C) C)).imp (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv m) (Compiler.CompactSourceSyntax.synCkqrel Compiler.CompactSourceSyntax.synClefin) (SemanticCore.Class.cv n))))))

Checked nominal proof certificate identified upstream as g_wppgammaleasthithwndv.

Equations

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