Nominal proof certificates grouped in dependency order.

Certificates from NominalWPPReplayChunk017Compact001Part059.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWpphitprefixtransferpackdndv (k : SemanticCore.Var) (F G I L : SemanticCore.Class) (q : SemanticCore.Var) (dv_F_q : q ∉ F.fv) (dv_G_q : q ∉ G.fv) (dv_I_q : q ∉ I.fv) (dv_L_q : q ∉ L.fv) (dv_k_q : k ≠ q) (hyp_wpphitprefixtransferpackdndv_1 : Nominal.NPrf (SemanticCore.Wff.classMem F Compiler.CompactSourceSyntax.synCfuns)) (hyp_wpphitprefixtransferpackdndv_2 : Nominal.NPrf (SemanticCore.Wff.classMem I (Compiler.CompactSourceSyntax.synCdm F))) (hyp_wpphitprefixtransferpackdndv_3 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCrn F) (Compiler.CompactSourceSyntax.synCdm F))) (hyp_wpphitprefixtransferpackdndv_4 : Nominal.NPrf (SemanticCore.Wff.classMem G Compiler.CompactSourceSyntax.synCfuns)) (hyp_wpphitprefixtransferpackdndv_5 : Nominal.NPrf (SemanticCore.Wff.classMem I (Compiler.CompactSourceSyntax.synCdm G))) (hyp_wpphitprefixtransferpackdndv_6 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCrn G) (Compiler.CompactSourceSyntax.synCdm G))) (hyp_wpphitprefixtransferpackdndv_7 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWral q Compiler.CompactSourceSyntax.synCnnc ((Compiler.CompactSourceSyntax.synWbr L Compiler.CompactSourceSyntax.synClec (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCfrec G I) (SemanticCore.Class.cv q))).neg.imp (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCfrec G I) (SemanticCore.Class.cv q)) Compiler.CompactSourceSyntax.synClec L)))) (hyp_wpphitprefixtransferpackdndv_8 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWral q Compiler.CompactSourceSyntax.synCnnc ((Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCfrec G I) (SemanticCore.Class.cv q)) Compiler.CompactSourceSyntax.synClec L).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv F (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCfrec G I) (SemanticCore.Class.cv q))) (Compiler.CompactSourceSyntax.synCfv G (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCfrec G I) (SemanticCore.Class.cv q))))))) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv k) Compiler.CompactSourceSyntax.synCnnc) (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv k) (Compiler.CompactSourceSyntax.synCwpphit G I L)) (Compiler.CompactSourceSyntax.synWral q Compiler.CompactSourceSyntax.synCnnc ((SemanticCore.Wff.classMem (SemanticCore.Class.cv q) (Compiler.CompactSourceSyntax.synCwpphit G I L)).imp (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv k) (Compiler.CompactSourceSyntax.synCkqrel Compiler.CompactSourceSyntax.synClefin) (SemanticCore.Class.cv q)))))).imp (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv k) (Compiler.CompactSourceSyntax.synCwpphit F I L)) (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCfrec G I) (SemanticCore.Class.cv k)) (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCfrec F I) (SemanticCore.Class.cv k)))))

Checked nominal proof certificate identified upstream as g_wpphitprefixtransferpackdndv.

Equations

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

Certificates from NominalWPPReplayChunk017Compact001Part060.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWppreachprefixbidv (D F G L : SemanticCore.Class) (q : SemanticCore.Var) (dv_D_q : q ∉ D.fv) (dv_F_q : q ∉ F.fv) (dv_G_q : q ∉ G.fv) (dv_L_q : q ∉ L.fv) (hyp_wppreachprefixbidv_1 : Nominal.NPrf (SemanticCore.Wff.classMem F Compiler.CompactSourceSyntax.synCfuns)) (hyp_wppreachprefixbidv_2 : Nominal.NPrf (SemanticCore.Wff.classMem D (Compiler.CompactSourceSyntax.synCdm F))) (hyp_wppreachprefixbidv_3 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCrn F) (Compiler.CompactSourceSyntax.synCdm F))) (hyp_wppreachprefixbidv_4 : Nominal.NPrf (SemanticCore.Wff.classMem G Compiler.CompactSourceSyntax.synCfuns)) (hyp_wppreachprefixbidv_5 : Nominal.NPrf (SemanticCore.Wff.classMem D (Compiler.CompactSourceSyntax.synCdm G))) (hyp_wppreachprefixbidv_6 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCrn G) (Compiler.CompactSourceSyntax.synCdm G))) (hyp_wppreachprefixbidv_7 : Nominal.NPrf (SemanticCore.Wff.classMem L Compiler.CompactSourceSyntax.synCvv)) (hyp_wppreachprefixbidv_8 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWral q Compiler.CompactSourceSyntax.synCnnc ((Compiler.CompactSourceSyntax.synWbr L Compiler.CompactSourceSyntax.synClec (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCfrec F D) (SemanticCore.Class.cv q))).neg.imp (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCfrec F D) (SemanticCore.Class.cv q)) Compiler.CompactSourceSyntax.synClec L)))) (hyp_wppreachprefixbidv_9 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWral q Compiler.CompactSourceSyntax.synCnnc ((Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCfrec F D) (SemanticCore.Class.cv q)) Compiler.CompactSourceSyntax.synClec L).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv G (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCfrec F D) (SemanticCore.Class.cv q))) (Compiler.CompactSourceSyntax.synCfv F (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCfrec F D) (SemanticCore.Class.cv q))))))) (hyp_wppreachprefixbidv_10 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWral q Compiler.CompactSourceSyntax.synCnnc ((Compiler.CompactSourceSyntax.synWbr L Compiler.CompactSourceSyntax.synClec (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCfrec G D) (SemanticCore.Class.cv q))).neg.imp (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCfrec G D) (SemanticCore.Class.cv q)) Compiler.CompactSourceSyntax.synClec L)))) (hyp_wppreachprefixbidv_11 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWral q Compiler.CompactSourceSyntax.synCnnc ((Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCfrec G D) (SemanticCore.Class.cv q)) Compiler.CompactSourceSyntax.synClec L).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv F (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCfrec G D) (SemanticCore.Class.cv q))) (Compiler.CompactSourceSyntax.synCfv G (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCfrec G D) (SemanticCore.Class.cv q))))))) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem D (Compiler.CompactSourceSyntax.synCwppreach F L)) (SemanticCore.Wff.classMem D (Compiler.CompactSourceSyntax.synCwppreach G L)))

Checked nominal proof certificate identified upstream as g_wppreachprefixbidv.

Equations

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

Certificates from NominalWPPReplayChunk017Compact001Part061.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWppcandprefixpointbidv (D F G L : SemanticCore.Class) (q : SemanticCore.Var) (dv_D_q : q ∉ D.fv) (dv_F_q : q ∉ F.fv) (dv_G_q : q ∉ G.fv) (dv_L_q : q ∉ L.fv) (hyp_wppcandprefixpointbidv_1 : Nominal.NPrf (SemanticCore.Wff.classMem F Compiler.CompactSourceSyntax.synCfuns)) (hyp_wppcandprefixpointbidv_2 : Nominal.NPrf (SemanticCore.Wff.classMem D (Compiler.CompactSourceSyntax.synCdm F))) (hyp_wppcandprefixpointbidv_3 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCrn F) (Compiler.CompactSourceSyntax.synCdm F))) (hyp_wppcandprefixpointbidv_4 : Nominal.NPrf (SemanticCore.Wff.classMem G Compiler.CompactSourceSyntax.synCfuns)) (hyp_wppcandprefixpointbidv_5 : Nominal.NPrf (SemanticCore.Wff.classMem D (Compiler.CompactSourceSyntax.synCdm G))) (hyp_wppcandprefixpointbidv_6 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCrn G) (Compiler.CompactSourceSyntax.synCdm G))) (hyp_wppcandprefixpointbidv_7 : Nominal.NPrf (SemanticCore.Wff.classMem L Compiler.CompactSourceSyntax.synCvv)) (hyp_wppcandprefixpointbidv_8 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWral q Compiler.CompactSourceSyntax.synCnnc ((Compiler.CompactSourceSyntax.synWbr L Compiler.CompactSourceSyntax.synClec (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCfrec F D) (SemanticCore.Class.cv q))).neg.imp (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCfrec F D) (SemanticCore.Class.cv q)) Compiler.CompactSourceSyntax.synClec L)))) (hyp_wppcandprefixpointbidv_9 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWral q Compiler.CompactSourceSyntax.synCnnc ((Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCfrec F D) (SemanticCore.Class.cv q)) Compiler.CompactSourceSyntax.synClec L).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv G (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCfrec F D) (SemanticCore.Class.cv q))) (Compiler.CompactSourceSyntax.synCfv F (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCfrec F D) (SemanticCore.Class.cv q))))))) (hyp_wppcandprefixpointbidv_10 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWral q Compiler.CompactSourceSyntax.synCnnc ((Compiler.CompactSourceSyntax.synWbr L Compiler.CompactSourceSyntax.synClec (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCfrec G D) (SemanticCore.Class.cv q))).neg.imp (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCfrec G D) (SemanticCore.Class.cv q)) Compiler.CompactSourceSyntax.synClec L)))) (hyp_wppcandprefixpointbidv_11 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWral q Compiler.CompactSourceSyntax.synCnnc ((Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCfrec G D) (SemanticCore.Class.cv q)) Compiler.CompactSourceSyntax.synClec L).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv F (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCfrec G D) (SemanticCore.Class.cv q))) (Compiler.CompactSourceSyntax.synCfv G (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCfrec G D) (SemanticCore.Class.cv q))))))) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem D (Compiler.CompactSourceSyntax.synCwppcand F L)) (SemanticCore.Wff.classMem D (Compiler.CompactSourceSyntax.synCwppcand G L)))

Checked nominal proof certificate identified upstream as g_wppcandprefixpointbidv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWppgammaprefixeqpointndv (F G L : SemanticCore.Class) (q : SemanticCore.Var) (dv_F_q : q ∉ F.fv) (dv_G_q : q ∉ G.fv) (dv_L_q : q ∉ L.fv) (hyp_wppgammaprefixeqpointndv_1 : Nominal.NPrf (SemanticCore.Wff.classMem F Compiler.CompactSourceSyntax.synCfuns)) (hyp_wppgammaprefixeqpointndv_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCrn F) (Compiler.CompactSourceSyntax.synCdm F))) (hyp_wppgammaprefixeqpointndv_3 : Nominal.NPrf (SemanticCore.Wff.classMem G Compiler.CompactSourceSyntax.synCfuns)) (hyp_wppgammaprefixeqpointndv_4 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCrn G) (Compiler.CompactSourceSyntax.synCdm G))) (hyp_wppgammaprefixeqpointndv_5 : Nominal.NPrf (SemanticCore.Wff.classMem L (Compiler.CompactSourceSyntax.synChwcards Compiler.CompactSourceSyntax.synCvv))) (hyp_wppgammaprefixeqpointndv_6 : Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCwppgamma F L) (Compiler.CompactSourceSyntax.synCdm F))) (hyp_wppgammaprefixeqpointndv_7 : Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCwppgamma F L) (Compiler.CompactSourceSyntax.synCdm G))) (hyp_wppgammaprefixeqpointndv_8 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWral q Compiler.CompactSourceSyntax.synCnnc ((Compiler.CompactSourceSyntax.synWbr L Compiler.CompactSourceSyntax.synClec (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCfrec F (Compiler.CompactSourceSyntax.synCwppgamma F L)) (SemanticCore.Class.cv q))).neg.imp (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCfrec F (Compiler.CompactSourceSyntax.synCwppgamma F L)) (SemanticCore.Class.cv q)) Compiler.CompactSourceSyntax.synClec L)))) (hyp_wppgammaprefixeqpointndv_9 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWral q Compiler.CompactSourceSyntax.synCnnc ((Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCfrec F (Compiler.CompactSourceSyntax.synCwppgamma F L)) (SemanticCore.Class.cv q)) Compiler.CompactSourceSyntax.synClec L).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv G (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCfrec F (Compiler.CompactSourceSyntax.synCwppgamma F L)) (SemanticCore.Class.cv q))) (Compiler.CompactSourceSyntax.synCfv F (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCfrec F (Compiler.CompactSourceSyntax.synCwppgamma F L)) (SemanticCore.Class.cv q))))))) (hyp_wppgammaprefixeqpointndv_10 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWral q Compiler.CompactSourceSyntax.synCnnc ((Compiler.CompactSourceSyntax.synWbr L Compiler.CompactSourceSyntax.synClec (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCfrec G (Compiler.CompactSourceSyntax.synCwppgamma F L)) (SemanticCore.Class.cv q))).neg.imp (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCfrec G (Compiler.CompactSourceSyntax.synCwppgamma F L)) (SemanticCore.Class.cv q)) Compiler.CompactSourceSyntax.synClec L)))) (hyp_wppgammaprefixeqpointndv_11 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWral q Compiler.CompactSourceSyntax.synCnnc ((Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCfrec G (Compiler.CompactSourceSyntax.synCwppgamma F L)) (SemanticCore.Class.cv q)) Compiler.CompactSourceSyntax.synClec L).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv F (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCfrec G (Compiler.CompactSourceSyntax.synCwppgamma F L)) (SemanticCore.Class.cv q))) (Compiler.CompactSourceSyntax.synCfv G (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCfrec G (Compiler.CompactSourceSyntax.synCwppgamma F L)) (SemanticCore.Class.cv q))))))) (hyp_wppgammaprefixeqpointndv_12 : Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCwppgamma G L) (Compiler.CompactSourceSyntax.synCdm F))) (hyp_wppgammaprefixeqpointndv_13 : Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCwppgamma G L) (Compiler.CompactSourceSyntax.synCdm G))) (hyp_wppgammaprefixeqpointndv_14 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWral q Compiler.CompactSourceSyntax.synCnnc ((Compiler.CompactSourceSyntax.synWbr L Compiler.CompactSourceSyntax.synClec (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCfrec F (Compiler.CompactSourceSyntax.synCwppgamma G L)) (SemanticCore.Class.cv q))).neg.imp (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCfrec F (Compiler.CompactSourceSyntax.synCwppgamma G L)) (SemanticCore.Class.cv q)) Compiler.CompactSourceSyntax.synClec L)))) (hyp_wppgammaprefixeqpointndv_15 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWral q Compiler.CompactSourceSyntax.synCnnc ((Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCfrec F (Compiler.CompactSourceSyntax.synCwppgamma G L)) (SemanticCore.Class.cv q)) Compiler.CompactSourceSyntax.synClec L).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv G (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCfrec F (Compiler.CompactSourceSyntax.synCwppgamma G L)) (SemanticCore.Class.cv q))) (Compiler.CompactSourceSyntax.synCfv F (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCfrec F (Compiler.CompactSourceSyntax.synCwppgamma G L)) (SemanticCore.Class.cv q))))))) (hyp_wppgammaprefixeqpointndv_16 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWral q Compiler.CompactSourceSyntax.synCnnc ((Compiler.CompactSourceSyntax.synWbr L Compiler.CompactSourceSyntax.synClec (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCfrec G (Compiler.CompactSourceSyntax.synCwppgamma G L)) (SemanticCore.Class.cv q))).neg.imp (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCfrec G (Compiler.CompactSourceSyntax.synCwppgamma G L)) (SemanticCore.Class.cv q)) Compiler.CompactSourceSyntax.synClec L)))) (hyp_wppgammaprefixeqpointndv_17 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWral q Compiler.CompactSourceSyntax.synCnnc ((Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCfrec G (Compiler.CompactSourceSyntax.synCwppgamma G L)) (SemanticCore.Class.cv q)) Compiler.CompactSourceSyntax.synClec L).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv F (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCfrec G (Compiler.CompactSourceSyntax.synCwppgamma G L)) (SemanticCore.Class.cv q))) (Compiler.CompactSourceSyntax.synCfv G (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCfrec G (Compiler.CompactSourceSyntax.synCwppgamma G L)) (SemanticCore.Class.cv q))))))) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCwppgamma F L) (Compiler.CompactSourceSyntax.synCwppgamma G L))

Checked nominal proof certificate identified upstream as g_wppgammaprefixeqpointndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWecomparisonnclecclndv (D R S E : SemanticCore.Class) (hyp_wecomparisonnclecclndv_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCwe D)) (hyp_wecomparisonnclecclndv_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr S Compiler.CompactSourceSyntax.synCwe E)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWo (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCnc D) Compiler.CompactSourceSyntax.synClec (Compiler.CompactSourceSyntax.synCnc E)) (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCnc E) Compiler.CompactSourceSyntax.synClec (Compiler.CompactSourceSyntax.synCnc D)))

Checked nominal proof certificate identified upstream as g_wecomparisonnclecclndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWecomparisonnclecandndv (e s r d : SemanticCore.Var) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv r) Compiler.CompactSourceSyntax.synCwe (SemanticCore.Class.cv d)) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv s) Compiler.CompactSourceSyntax.synCwe (SemanticCore.Class.cv e))).imp (Compiler.CompactSourceSyntax.synWo (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCnc (SemanticCore.Class.cv d)) Compiler.CompactSourceSyntax.synClec (Compiler.CompactSourceSyntax.synCnc (SemanticCore.Class.cv e))) (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCnc (SemanticCore.Class.cv e)) Compiler.CompactSourceSyntax.synClec (Compiler.CompactSourceSyntax.synCnc (SemanticCore.Class.cv d)))))

Checked nominal proof certificate identified upstream as g_wecomparisonnclecandndv.

Equations

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