LeanPool.NFWeakPartition.Certificates.NominalWPPReplayChunk018Compact001Block001

source

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCfbhncardpowershiftndv (A : SemanticCore.Class) (hyp_cfbhncardpowershiftndv_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) :

Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synChncard (Compiler.CompactSourceSyntax.synCpw (Compiler.CompactSourceSyntax.synCpw1 A))) (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synChncard (Compiler.CompactSourceSyntax.synCpw A))))

Checked nominal proof certificate identified upstream as g_cfbhncardpowershiftndv.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCfbtceqi (A B : SemanticCore.Class) (hyp_cfbtceqi_1 : Nominal.NPrf (SemanticCore.Wff.classEq A B)) :

Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCtc A) (Compiler.CompactSourceSyntax.synCtc B))

Checked nominal proof certificate identified upstream as g_cfbtceqi.

Equations

NFChoice.DirectNominalPrf.WPPReplay.gCfbtceqi A B hyp_cfbtceqi_1 = NFChoice.DirectNominalPrf.Nominal.mp hyp_cfbtceqi_1 (NFChoice.DirectNominalPrf.WPPReplay.gTceq A B)

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCfbhncardpw1ceqndv :

Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synChncard (Compiler.CompactSourceSyntax.synCpw Compiler.CompactSourceSyntax.synC1c)) (Compiler.CompactSourceSyntax.synChncard Compiler.CompactSourceSyntax.synC1c))

Checked nominal proof certificate identified upstream as g_cfbhncardpw1ceqndv.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCfbhncardpwpw16stepndv :

Checked nominal proof certificate identified upstream as g_cfbhncardpwpw16stepndv.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCfbhncardpwpw15stepndv :

Checked nominal proof certificate identified upstream as g_cfbhncardpwpw15stepndv.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCfbhncardpwpw14stepndv :

Checked nominal proof certificate identified upstream as g_cfbhncardpwpw14stepndv.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCfbhncardpwpw13stepndv :

Checked nominal proof certificate identified upstream as g_cfbhncardpwpw13stepndv.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCfbhncardpwpw12stepndv :

Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synChncard (Compiler.CompactSourceSyntax.synCpw (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 Compiler.CompactSourceSyntax.synC1c)))) (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synChncard (Compiler.CompactSourceSyntax.synCpw (Compiler.CompactSourceSyntax.synCpw1 Compiler.CompactSourceSyntax.synC1c)))))

Checked nominal proof certificate identified upstream as g_cfbhncardpwpw12stepndv.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCfbhncardpwpw11stepndv :

Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synChncard (Compiler.CompactSourceSyntax.synCpw (Compiler.CompactSourceSyntax.synCpw1 Compiler.CompactSourceSyntax.synC1c))) (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synChncard (Compiler.CompactSourceSyntax.synCpw Compiler.CompactSourceSyntax.synC1c))))

Checked nominal proof certificate identified upstream as g_cfbhncardpwpw11stepndv.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCfbhncardpwpw16to4ndv :

Checked nominal proof certificate identified upstream as g_cfbhncardpwpw16to4ndv.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCfbhncardpwpw14step2tndv :

Checked nominal proof certificate identified upstream as g_cfbhncardpwpw14step2tndv.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCfbhncardpwpw13step3tndv :

Checked nominal proof certificate identified upstream as g_cfbhncardpwpw13step3tndv.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCfbhncardpwpw12step4tndv :

Checked nominal proof certificate identified upstream as g_cfbhncardpwpw12step4tndv.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCfbhncardpwpw11step5tndv :

Checked nominal proof certificate identified upstream as g_cfbhncardpwpw11step5tndv.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCfbhncardpwpw16to3ndv :

Checked nominal proof certificate identified upstream as g_cfbhncardpwpw16to3ndv.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCfbhncardpwpw16to2ndv :

Checked nominal proof certificate identified upstream as g_cfbhncardpwpw16to2ndv.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCfbhncardpwpw16to1ndv :

Checked nominal proof certificate identified upstream as g_cfbhncardpwpw16to1ndv.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCfbhncardpwpw16to0ndv :

Checked nominal proof certificate identified upstream as g_cfbhncardpwpw16to0ndv.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCfbhncardtc3forwardndv (A : SemanticCore.Class) (hyp_cfbhncardtc3forwardndv_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) :

Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synChncard A)))) (Compiler.CompactSourceSyntax.synCnc (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synChnord A))))))

Checked nominal proof certificate identified upstream as g_cfbhncardtc3forwardndv.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCfbhncardtc3ndv (A : SemanticCore.Class) (hyp_cfbhncardtc3ndv_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) :

Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCnc (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synChnord A))))) (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synChncard A)))))

Checked nominal proof certificate identified upstream as g_cfbhncardtc3ndv.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCfbhncardpw1ceq6tndv :

Checked nominal proof certificate identified upstream as g_cfbhncardpw1ceq6tndv.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCfbhncardpwpw16basendv :

Checked nominal proof certificate identified upstream as g_cfbhncardpwpw16basendv.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCfbsourceledgerndv :

Checked nominal proof certificate identified upstream as g_cfbsourceledgerndv.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCfbhncardpw2enpw1shiftndv (Y Z : SemanticCore.Class) (hyp_cfbhncardpw2enpw1shiftndv_1 : Nominal.NPrf (SemanticCore.Wff.classMem Z Compiler.CompactSourceSyntax.synCvv)) (hyp_cfbhncardpw2enpw1shiftndv_2 : Nominal.NPrf (SemanticCore.Wff.classMem Y Compiler.CompactSourceSyntax.synCvv)) (hyp_cfbhncardpw2enpw1shiftndv_3 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr Z Compiler.CompactSourceSyntax.synCen (Compiler.CompactSourceSyntax.synCpw1 Y))) :

Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synChncard (Compiler.CompactSourceSyntax.synCpw (Compiler.CompactSourceSyntax.synCpw Z))) (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synChncard (Compiler.CompactSourceSyntax.synCpw (Compiler.CompactSourceSyntax.synCpw Y)))))

Checked nominal proof certificate identified upstream as g_cfbhncardpw2enpw1shiftndv.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCfbtccli (A : SemanticCore.Class) (hyp_cfbtccli_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCncs)) :

Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCtc A) Compiler.CompactSourceSyntax.synCncs)

Checked nominal proof certificate identified upstream as g_cfbtccli.

Equations

NFChoice.DirectNominalPrf.WPPReplay.gCfbtccli A hyp_cfbtccli_1 = NFChoice.DirectNominalPrf.Nominal.mp hyp_cfbtccli_1 (NFChoice.DirectNominalPrf.WPPReplay.gTccl A)

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCfbtargetqbaseexndv :

Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCpw (Compiler.CompactSourceSyntax.synCpw (Compiler.CompactSourceSyntax.synChnord (Compiler.CompactSourceSyntax.synCpw1 Compiler.CompactSourceSyntax.synC1c)))) Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_cfbtargetqbaseexndv.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCfbtargetqncndv :

Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synChncard (Compiler.CompactSourceSyntax.synCpw (Compiler.CompactSourceSyntax.synCpw (Compiler.CompactSourceSyntax.synChnord (Compiler.CompactSourceSyntax.synCpw1 Compiler.CompactSourceSyntax.synC1c))))) Compiler.CompactSourceSyntax.synCncs)

Checked nominal proof certificate identified upstream as g_cfbtargetqncndv.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCfbt6hncard1ncndv :

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.synCncs)

Checked nominal proof certificate identified upstream as g_cfbt6hncard1ncndv.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCfbt2targetqncndv :

Nominal.NPrf (SemanticCore.Wff.classMem (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.synCncs)

Checked nominal proof certificate identified upstream as g_cfbt2targetqncndv.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCfbfixedblockcancel3ndv :

Checked nominal proof certificate identified upstream as g_cfbfixedblockcancel3ndv.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCfbfixedblockouterhartogsndv (R : SemanticCore.Class) (hyp_cfbfixedblockouterhartogsndv_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))))))) :

Checked nominal proof certificate identified upstream as g_cfbfixedblockouterhartogsndv.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCfbfixedblockpointimpndv (R : SemanticCore.Class) (hyp_cfbfixedblockpointimpndv_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))))))) :

Checked nominal proof certificate identified upstream as g_cfbfixedblockpointimpndv.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCfbhnordpw1shiftensymndv (A : SemanticCore.Class) (hyp_cfbhnordpw1shiftensymndv_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) :

Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synChnord (Compiler.CompactSourceSyntax.synCpw1 A)) Compiler.CompactSourceSyntax.synCen (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synChnord A)))

Checked nominal proof certificate identified upstream as g_cfbhnordpw1shiftensymndv.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCfbhncardpw2hnordpw1shiftndv (A : SemanticCore.Class) (hyp_cfbhncardpw2hnordpw1shiftndv_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) :

Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synChncard (Compiler.CompactSourceSyntax.synCpw (Compiler.CompactSourceSyntax.synCpw (Compiler.CompactSourceSyntax.synChnord (Compiler.CompactSourceSyntax.synCpw1 A))))) (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synChncard (Compiler.CompactSourceSyntax.synCpw (Compiler.CompactSourceSyntax.synCpw (Compiler.CompactSourceSyntax.synChnord A))))))

Checked nominal proof certificate identified upstream as g_cfbhncardpw2hnordpw1shiftndv.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCfbtarget6stepndv :

Checked nominal proof certificate identified upstream as g_cfbtarget6stepndv.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCfbtarget5stepndv :

Checked nominal proof certificate identified upstream as g_cfbtarget5stepndv.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCfbtarget4stepndv :

Checked nominal proof certificate identified upstream as g_cfbtarget4stepndv.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCfbtarget3stepndv :

Checked nominal proof certificate identified upstream as g_cfbtarget3stepndv.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCfbtarget2stepndv :

Checked nominal proof certificate identified upstream as g_cfbtarget2stepndv.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCfbtarget5step1tndv :

Checked nominal proof certificate identified upstream as g_cfbtarget5step1tndv.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCfbtarget4step2tndv :

Checked nominal proof certificate identified upstream as g_cfbtarget4step2tndv.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCfbtarget3step3tndv :

Checked nominal proof certificate identified upstream as g_cfbtarget3step3tndv.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCfbtarget2step4tndv :

Checked nominal proof certificate identified upstream as g_cfbtarget2step4tndv.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCfbtarget6to4ndv :

Checked nominal proof certificate identified upstream as g_cfbtarget6to4ndv.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCfbtarget6to3ndv :

Checked nominal proof certificate identified upstream as g_cfbtarget6to3ndv.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCfbtarget6to2ndv :

Checked nominal proof certificate identified upstream as g_cfbtarget6to2ndv.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCfbtargethncardledgerndv :

Checked nominal proof certificate identified upstream as g_cfbtargethncardledgerndv.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCfbtargetledgerndv :

Checked nominal proof certificate identified upstream as g_cfbtargetledgerndv.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCfbfixedblockledgercmpndv :

Checked nominal proof certificate identified upstream as g_cfbfixedblockledgercmpndv.

Equations

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

Instances For

source

Checked nominal proof certificate identified upstream as g_cfbfixedblockledgercmpdndv.

Equations

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

Instances For

source

Checked nominal proof certificate identified upstream as g_cfbfixedblockcancelleddndv.

Equations

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

Instances For

source

Checked nominal proof certificate identified upstream as g_cfbfixedblockf6pointfromnclendv.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCfbpw16oneexndv :

Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 Compiler.CompactSourceSyntax.synC1c)))))) Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_cfbpw16oneexndv.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCfbfixedblocksourceexndv :

Checked nominal proof certificate identified upstream as g_cfbfixedblocksourceexndv.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCfbfixedblocktargetexndv :

Checked nominal proof certificate identified upstream as g_cfbfixedblocktargetexndv.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCfbnclefrominjimpndv (A B : SemanticCore.Class) (f : SemanticCore.Var) (dv_A_f : f ∉ A.fv) (dv_B_f : f ∉ B.fv) (hyp_cfbnclefrominjimpndv_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) (hyp_cfbnclefrominjimpndv_2 : Nominal.NPrf (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCvv)) :

Nominal.NPrf ((Compiler.CompactSourceSyntax.synWex f (Compiler.CompactSourceSyntax.synWf1 (SemanticCore.Class.cv f) A B)).imp (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCnc A) Compiler.CompactSourceSyntax.synClec (Compiler.CompactSourceSyntax.synCnc B)))

Checked nominal proof certificate identified upstream as g_cfbnclefrominjimpndv.

Equations

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

Instances For

source

Checked nominal proof certificate identified upstream as g_cfbfixedblocknclefrominjndv.

Equations

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

Instances For

source

Checked nominal proof certificate identified upstream as g_cfbfixedblockf6pointfrominjndv.

Equations

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

Instances For

source

Checked nominal proof certificate identified upstream as g_cfbfixedblockf6pointfrominjnowendv.

Equations

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

Instances For

source

Nominal.NPrf Compiler.CompactSourceSyntax.synWwpp.neg

Checked nominal proof certificate identified upstream as g_cfbfixedblocknotwppfrominjndv.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCfbthresholdnn2lencndv (X : SemanticCore.Class) (hyp_cfbthresholdnn2lencndv_1 : Nominal.NPrf (SemanticCore.Wff.classMem X Compiler.CompactSourceSyntax.synCvv)) (hyp_cfbthresholdnn2lencndv_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCnc Compiler.CompactSourceSyntax.synCnnc) Compiler.CompactSourceSyntax.synClec (Compiler.CompactSourceSyntax.synCnc X))) :

Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCnc Compiler.CompactSourceSyntax.synCnnc) Compiler.CompactSourceSyntax.synClec (Compiler.CompactSourceSyntax.synCnc (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 X))))

Checked nominal proof certificate identified upstream as g_cfbthresholdnn2lencndv.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCfbliteralunivhncardboundndv :

Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synChncard (Compiler.CompactSourceSyntax.synCxp (Compiler.CompactSourceSyntax.synCxpk Compiler.CompactSourceSyntax.synCvv Compiler.CompactSourceSyntax.synCvv) Compiler.CompactSourceSyntax.synCnnc)) Compiler.CompactSourceSyntax.synClec (Compiler.CompactSourceSyntax.synChncard (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 Compiler.CompactSourceSyntax.synCvv))))

Checked nominal proof certificate identified upstream as g_cfbliteralunivhncardboundndv.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCfbliteralp17hncardboundndv :

Checked nominal proof certificate identified upstream as g_cfbliteralp17hncardboundndv.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCfbliteralp16onehncardboundndv :

Checked nominal proof certificate identified upstream as g_cfbliteralp16onehncardboundndv.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCfbfixedblockhnqgraphexndv (X : SemanticCore.Class) (hyp_cfbfixedblockhnqgraphexndv_1 : Nominal.NPrf (SemanticCore.Wff.classMem X Compiler.CompactSourceSyntax.synCvv)) :

Checked nominal proof certificate identified upstream as g_cfbfixedblockhnqgraphexndv.

Equations

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

Instances For

source

Checked nominal proof certificate identified upstream as g_cfbwppfixedblockhnqinjexndv.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWppfiniteblocknotwppndv :

Nominal.NPrf Compiler.CompactSourceSyntax.synWwpp.neg

Checked nominal proof certificate identified upstream as g_wppfiniteblocknotwppndv.

Equations

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

Instances For