Nominal proof certificates grouped in dependency order.

Certificates from NominalWPPReplayChunk017Compact001Part021.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHncodecutreledgedecode (x v u : SemanticCore.Var) (A C : SemanticCore.Class) (_dv_A_C : Disjoint A.fv C.fv) (dv_A_u : u ∉ A.fv) (_dv_A_v : v ∉ A.fv) (dv_A_x : x ∉ A.fv) (dv_C_u : u ∉ C.fv) (_dv_C_v : v ∉ C.fv) (dv_C_x : x ∉ C.fv) (dv_u_v : u ≠ v) (dv_u_x : u ≠ x) (dv_v_x : v ≠ x) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWbr C (Compiler.CompactSourceSyntax.synChncodecutrel A) (SemanticCore.Class.cv v)).imp (Compiler.CompactSourceSyntax.synWrex u (Compiler.CompactSourceSyntax.synChwcn A) (Compiler.CompactSourceSyntax.synWrex x (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)) (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classEq C (Compiler.CompactSourceSyntax.synChnwcutcode (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC1st (SemanticCore.Class.cv u)) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)) (SemanticCore.Class.cv x))) (SemanticCore.Wff.classEq (SemanticCore.Class.cv v) (SemanticCore.Class.cv u))))))

Checked nominal proof certificate identified upstream as g_hncodecutreledgedecode.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHncodecutfnvalhwcn (x u : SemanticCore.Var) (A : SemanticCore.Class) (_dv_A_u : u ∉ A.fv) : Nominal.NPrf ((SemanticCore.Wff.classMem (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synChwcn A)).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synChncodecutfn (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv x)))) (Compiler.CompactSourceSyntax.synChnwcutcode (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC1st (SemanticCore.Class.cv u)) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)) (SemanticCore.Class.cv x))))

Checked nominal proof certificate identified upstream as g_hncodecutfnvalhwcn.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHncodecutreledgedecodetarget (x v : SemanticCore.Var) (A C : SemanticCore.Class) (dv_A_C : Disjoint A.fv C.fv) (dv_A_v : v ∉ A.fv) (_dv_A_x : x ∉ A.fv) (dv_C_v : v ∉ C.fv) (dv_C_x : x ∉ C.fv) (dv_v_x : v ≠ x) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWbr C (Compiler.CompactSourceSyntax.synChncodecutrel A) (SemanticCore.Class.cv v)).imp (Compiler.CompactSourceSyntax.synWrex x (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv v)) (SemanticCore.Wff.classEq C (Compiler.CompactSourceSyntax.synChnwcutcode (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC1st (SemanticCore.Class.cv v)) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv v)) (SemanticCore.Class.cv x)))))

Checked nominal proof certificate identified upstream as g_hncodecutreledgedecodetarget.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHncodecutreledgeihwcn (x v : SemanticCore.Var) (A : SemanticCore.Class) (dv_A_v : v ∉ A.fv) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv v) (Compiler.CompactSourceSyntax.synChwcn A)) (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv v)))).imp (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synChnwcutcode (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC1st (SemanticCore.Class.cv v)) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv v)) (SemanticCore.Class.cv x)) (Compiler.CompactSourceSyntax.synChncodecutrel A) (SemanticCore.Class.cv v)))

Checked nominal proof certificate identified upstream as g_hncodecutreledgeihwcn.

Equations

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

Certificates from NominalWPPReplayChunk017Compact001Part022.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHncodecmpsetstrictcutsemdv (x v u : SemanticCore.Var) (A : SemanticCore.Class) (_dv_A_u : u ∉ A.fv) (dv_A_v : v ∉ A.fv) (dv_A_x : x ∉ A.fv) (dv_u_x : u ≠ x) (dv_v_x : v ≠ x) : Nominal.NPrf ((SemanticCore.Wff.classMem (SemanticCore.Class.cv v) (Compiler.CompactSourceSyntax.synChwcn A)).imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synChncodecmpset A) (SemanticCore.Class.cv v)) (Compiler.CompactSourceSyntax.synWo (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synChwniso A) (SemanticCore.Class.cv v)) (Compiler.CompactSourceSyntax.synWrex x (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv v)) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synChwniso A) (Compiler.CompactSourceSyntax.synChnwcutcode (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC1st (SemanticCore.Class.cv v)) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv v)) (SemanticCore.Class.cv x)))))))

Checked nominal proof certificate identified upstream as g_hncodecmpsetstrictcutsemdv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHncodecmpsetrefndv (A : SemanticCore.Class) : Nominal.NPrf ((SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv).imp (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synChncodecmpset A) Compiler.CompactSourceSyntax.synCref (Compiler.CompactSourceSyntax.synChwcn A)))

Checked nominal proof certificate identified upstream as g_hncodecmpsetrefndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHncodecutreltargetclndv (v : SemanticCore.Var) (A C : SemanticCore.Class) (dv_A_C : Disjoint A.fv C.fv) (dv_A_v : v ∉ A.fv) (dv_C_v : v ∉ C.fv) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWbr C (Compiler.CompactSourceSyntax.synChncodecutrel A) (SemanticCore.Class.cv v)).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv v) (Compiler.CompactSourceSyntax.synChwcn A)))

Checked nominal proof certificate identified upstream as g_hncodecutreltargetclndv.

Equations

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

Certificates from NominalWPPReplayChunk017Compact001Part023.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHncodecmpsetssxpndv (A : SemanticCore.Class) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synChncodecmpset A) (Compiler.CompactSourceSyntax.synCxp (Compiler.CompactSourceSyntax.synChwcn A) (Compiler.CompactSourceSyntax.synChwcn A)))

Checked nominal proof certificate identified upstream as g_hncodecmpsetssxpndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHncodecmpdefaultcnndv (A : SemanticCore.Class) : Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCop (Compiler.CompactSourceSyntax.synCin (Compiler.CompactSourceSyntax.synCkqrel Compiler.CompactSourceSyntax.synClefin) (Compiler.CompactSourceSyntax.synCxp Compiler.CompactSourceSyntax.synC0 Compiler.CompactSourceSyntax.synC0)) Compiler.CompactSourceSyntax.synC0) (Compiler.CompactSourceSyntax.synChwcn A))

Checked nominal proof certificate identified upstream as g_hncodecmpdefaultcnndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHwcnweclndv (A B : SemanticCore.Class) : Nominal.NPrf ((SemanticCore.Wff.classMem B (Compiler.CompactSourceSyntax.synChwcn A)).imp (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC1st B) Compiler.CompactSourceSyntax.synCwe (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd B)))

Checked nominal proof certificate identified upstream as g_hwcnweclndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHwcnbaseclndv (A B : SemanticCore.Class) : Nominal.NPrf ((SemanticCore.Wff.classMem B (Compiler.CompactSourceSyntax.synChwcn A)).imp (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd B) A))

Checked nominal proof certificate identified upstream as g_hwcnbaseclndv.

Equations

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

Certificates from NominalWPPReplayChunk017Compact001Part024.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHncodecmpsetstrictcutsemclndv (x : SemanticCore.Var) (A B C : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_B_x : x ∉ B.fv) (dv_C_x : x ∉ C.fv) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem B (Compiler.CompactSourceSyntax.synChwcn A)) (SemanticCore.Wff.classMem C (Compiler.CompactSourceSyntax.synChwcn A))).imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWbr B (Compiler.CompactSourceSyntax.synChncodecmpset A) C) (Compiler.CompactSourceSyntax.synWo (Compiler.CompactSourceSyntax.synWbr B (Compiler.CompactSourceSyntax.synChwniso A) C) (Compiler.CompactSourceSyntax.synWrex x (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd C) (Compiler.CompactSourceSyntax.synWbr B (Compiler.CompactSourceSyntax.synChwniso A) (Compiler.CompactSourceSyntax.synChnwcutcode (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC1st C) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd C) (SemanticCore.Class.cv x)))))))

Checked nominal proof certificate identified upstream as g_hncodecmpsetstrictcutsemclndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHncodetotalleftmemndv (u : SemanticCore.Var) (A : SemanticCore.Class) (_dv_A_u : u ∉ A.fv) : Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCif (SemanticCore.Wff.classMem (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synChwcn A)) (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synCop (Compiler.CompactSourceSyntax.synCin (Compiler.CompactSourceSyntax.synCkqrel Compiler.CompactSourceSyntax.synClefin) (Compiler.CompactSourceSyntax.synCxp Compiler.CompactSourceSyntax.synC0 Compiler.CompactSourceSyntax.synC0)) Compiler.CompactSourceSyntax.synC0)) (Compiler.CompactSourceSyntax.synChwcn A))

Checked nominal proof certificate identified upstream as g_hncodetotalleftmemndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHncodetotalrightmemndv (v : SemanticCore.Var) (A : SemanticCore.Class) (_dv_A_v : v ∉ A.fv) : Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCif (SemanticCore.Wff.classMem (SemanticCore.Class.cv v) (Compiler.CompactSourceSyntax.synChwcn A)) (SemanticCore.Class.cv v) (Compiler.CompactSourceSyntax.synCop (Compiler.CompactSourceSyntax.synCin (Compiler.CompactSourceSyntax.synCkqrel Compiler.CompactSourceSyntax.synClefin) (Compiler.CompactSourceSyntax.synCxp Compiler.CompactSourceSyntax.synC0 Compiler.CompactSourceSyntax.synC0)) Compiler.CompactSourceSyntax.synC0)) (Compiler.CompactSourceSyntax.synChwcn A))

Checked nominal proof certificate identified upstream as g_hncodetotalrightmemndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHncodecomparisontotalndv (x v u : SemanticCore.Var) (A : SemanticCore.Class) (h : SemanticCore.Var) (dv_A_h : h ∉ A.fv) (_dv_A_u : u ∉ A.fv) (_dv_A_v : v ∉ A.fv) (dv_A_x : x ∉ A.fv) (dv_h_u : h ≠ u) (dv_h_v : h ≠ v) (dv_h_x : h ≠ x) (dv_u_x : u ≠ x) (dv_v_x : v ≠ x) : Nominal.NPrf (Compiler.CompactSourceSyntax.synW3o (Compiler.CompactSourceSyntax.synWex h (Compiler.CompactSourceSyntax.synWiso (SemanticCore.Class.cv h) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC1st (Compiler.CompactSourceSyntax.synCif (SemanticCore.Wff.classMem (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synChwcn A)) (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synCop (Compiler.CompactSourceSyntax.synCin (Compiler.CompactSourceSyntax.synCkqrel Compiler.CompactSourceSyntax.synClefin) (Compiler.CompactSourceSyntax.synCxp Compiler.CompactSourceSyntax.synC0 Compiler.CompactSourceSyntax.synC0)) Compiler.CompactSourceSyntax.synC0))) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC1st (Compiler.CompactSourceSyntax.synCif (SemanticCore.Wff.classMem (SemanticCore.Class.cv v) (Compiler.CompactSourceSyntax.synChwcn A)) (SemanticCore.Class.cv v) (Compiler.CompactSourceSyntax.synCop (Compiler.CompactSourceSyntax.synCin (Compiler.CompactSourceSyntax.synCkqrel Compiler.CompactSourceSyntax.synClefin) (Compiler.CompactSourceSyntax.synCxp Compiler.CompactSourceSyntax.synC0 Compiler.CompactSourceSyntax.synC0)) Compiler.CompactSourceSyntax.synC0))) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (Compiler.CompactSourceSyntax.synCif (SemanticCore.Wff.classMem (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synChwcn A)) (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synCop (Compiler.CompactSourceSyntax.synCin (Compiler.CompactSourceSyntax.synCkqrel Compiler.CompactSourceSyntax.synClefin) (Compiler.CompactSourceSyntax.synCxp Compiler.CompactSourceSyntax.synC0 Compiler.CompactSourceSyntax.synC0)) Compiler.CompactSourceSyntax.synC0))) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (Compiler.CompactSourceSyntax.synCif (SemanticCore.Wff.classMem (SemanticCore.Class.cv v) (Compiler.CompactSourceSyntax.synChwcn A)) (SemanticCore.Class.cv v) (Compiler.CompactSourceSyntax.synCop (Compiler.CompactSourceSyntax.synCin (Compiler.CompactSourceSyntax.synCkqrel Compiler.CompactSourceSyntax.synClefin) (Compiler.CompactSourceSyntax.synCxp Compiler.CompactSourceSyntax.synC0 Compiler.CompactSourceSyntax.synC0)) Compiler.CompactSourceSyntax.synC0))))) (Compiler.CompactSourceSyntax.synWrex x (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (Compiler.CompactSourceSyntax.synCif (SemanticCore.Wff.classMem (SemanticCore.Class.cv v) (Compiler.CompactSourceSyntax.synChwcn A)) (SemanticCore.Class.cv v) (Compiler.CompactSourceSyntax.synCop (Compiler.CompactSourceSyntax.synCin (Compiler.CompactSourceSyntax.synCkqrel Compiler.CompactSourceSyntax.synClefin) (Compiler.CompactSourceSyntax.synCxp Compiler.CompactSourceSyntax.synC0 Compiler.CompactSourceSyntax.synC0)) Compiler.CompactSourceSyntax.synC0))) (Compiler.CompactSourceSyntax.synWex h (Compiler.CompactSourceSyntax.synWiso (SemanticCore.Class.cv h) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC1st (Compiler.CompactSourceSyntax.synCif (SemanticCore.Wff.classMem (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synChwcn A)) (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synCop (Compiler.CompactSourceSyntax.synCin (Compiler.CompactSourceSyntax.synCkqrel Compiler.CompactSourceSyntax.synClefin) (Compiler.CompactSourceSyntax.synCxp Compiler.CompactSourceSyntax.synC0 Compiler.CompactSourceSyntax.synC0)) Compiler.CompactSourceSyntax.synC0))) (Compiler.CompactSourceSyntax.synCin (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC1st (Compiler.CompactSourceSyntax.synCif (SemanticCore.Wff.classMem (SemanticCore.Class.cv v) (Compiler.CompactSourceSyntax.synChwcn A)) (SemanticCore.Class.cv v) (Compiler.CompactSourceSyntax.synCop (Compiler.CompactSourceSyntax.synCin (Compiler.CompactSourceSyntax.synCkqrel Compiler.CompactSourceSyntax.synClefin) (Compiler.CompactSourceSyntax.synCxp Compiler.CompactSourceSyntax.synC0 Compiler.CompactSourceSyntax.synC0)) Compiler.CompactSourceSyntax.synC0))) (Compiler.CompactSourceSyntax.synCxp (Compiler.CompactSourceSyntax.synCin (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (Compiler.CompactSourceSyntax.synCif (SemanticCore.Wff.classMem (SemanticCore.Class.cv v) (Compiler.CompactSourceSyntax.synChwcn A)) (SemanticCore.Class.cv v) (Compiler.CompactSourceSyntax.synCop (Compiler.CompactSourceSyntax.synCin (Compiler.CompactSourceSyntax.synCkqrel Compiler.CompactSourceSyntax.synClefin) (Compiler.CompactSourceSyntax.synCxp Compiler.CompactSourceSyntax.synC0 Compiler.CompactSourceSyntax.synC0)) Compiler.CompactSourceSyntax.synC0))) (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC1st (Compiler.CompactSourceSyntax.synCif (SemanticCore.Wff.classMem (SemanticCore.Class.cv v) (Compiler.CompactSourceSyntax.synChwcn A)) (SemanticCore.Class.cv v) (Compiler.CompactSourceSyntax.synCop (Compiler.CompactSourceSyntax.synCin (Compiler.CompactSourceSyntax.synCkqrel Compiler.CompactSourceSyntax.synClefin) (Compiler.CompactSourceSyntax.synCxp Compiler.CompactSourceSyntax.synC0 Compiler.CompactSourceSyntax.synC0)) Compiler.CompactSourceSyntax.synC0))) Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv x)))) (Compiler.CompactSourceSyntax.synCin (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (Compiler.CompactSourceSyntax.synCif (SemanticCore.Wff.classMem (SemanticCore.Class.cv v) (Compiler.CompactSourceSyntax.synChwcn A)) (SemanticCore.Class.cv v) (Compiler.CompactSourceSyntax.synCop (Compiler.CompactSourceSyntax.synCin (Compiler.CompactSourceSyntax.synCkqrel Compiler.CompactSourceSyntax.synClefin) (Compiler.CompactSourceSyntax.synCxp Compiler.CompactSourceSyntax.synC0 Compiler.CompactSourceSyntax.synC0)) Compiler.CompactSourceSyntax.synC0))) (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC1st (Compiler.CompactSourceSyntax.synCif (SemanticCore.Wff.classMem (SemanticCore.Class.cv v) (Compiler.CompactSourceSyntax.synChwcn A)) (SemanticCore.Class.cv v) (Compiler.CompactSourceSyntax.synCop (Compiler.CompactSourceSyntax.synCin (Compiler.CompactSourceSyntax.synCkqrel Compiler.CompactSourceSyntax.synClefin) (Compiler.CompactSourceSyntax.synCxp Compiler.CompactSourceSyntax.synC0 Compiler.CompactSourceSyntax.synC0)) Compiler.CompactSourceSyntax.synC0))) Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv x)))))) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (Compiler.CompactSourceSyntax.synCif (SemanticCore.Wff.classMem (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synChwcn A)) (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synCop (Compiler.CompactSourceSyntax.synCin (Compiler.CompactSourceSyntax.synCkqrel Compiler.CompactSourceSyntax.synClefin) (Compiler.CompactSourceSyntax.synCxp Compiler.CompactSourceSyntax.synC0 Compiler.CompactSourceSyntax.synC0)) Compiler.CompactSourceSyntax.synC0))) (Compiler.CompactSourceSyntax.synCin (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (Compiler.CompactSourceSyntax.synCif (SemanticCore.Wff.classMem (SemanticCore.Class.cv v) (Compiler.CompactSourceSyntax.synChwcn A)) (SemanticCore.Class.cv v) (Compiler.CompactSourceSyntax.synCop (Compiler.CompactSourceSyntax.synCin (Compiler.CompactSourceSyntax.synCkqrel Compiler.CompactSourceSyntax.synClefin) (Compiler.CompactSourceSyntax.synCxp Compiler.CompactSourceSyntax.synC0 Compiler.CompactSourceSyntax.synC0)) Compiler.CompactSourceSyntax.synC0))) (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC1st (Compiler.CompactSourceSyntax.synCif (SemanticCore.Wff.classMem (SemanticCore.Class.cv v) (Compiler.CompactSourceSyntax.synChwcn A)) (SemanticCore.Class.cv v) (Compiler.CompactSourceSyntax.synCop (Compiler.CompactSourceSyntax.synCin (Compiler.CompactSourceSyntax.synCkqrel Compiler.CompactSourceSyntax.synClefin) (Compiler.CompactSourceSyntax.synCxp Compiler.CompactSourceSyntax.synC0 Compiler.CompactSourceSyntax.synC0)) Compiler.CompactSourceSyntax.synC0))) Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv x))))))) (Compiler.CompactSourceSyntax.synWrex x (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (Compiler.CompactSourceSyntax.synCif (SemanticCore.Wff.classMem (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synChwcn A)) (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synCop (Compiler.CompactSourceSyntax.synCin (Compiler.CompactSourceSyntax.synCkqrel Compiler.CompactSourceSyntax.synClefin) (Compiler.CompactSourceSyntax.synCxp Compiler.CompactSourceSyntax.synC0 Compiler.CompactSourceSyntax.synC0)) Compiler.CompactSourceSyntax.synC0))) (Compiler.CompactSourceSyntax.synWex h (Compiler.CompactSourceSyntax.synWiso (SemanticCore.Class.cv h) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC1st (Compiler.CompactSourceSyntax.synCif (SemanticCore.Wff.classMem (SemanticCore.Class.cv v) (Compiler.CompactSourceSyntax.synChwcn A)) (SemanticCore.Class.cv v) (Compiler.CompactSourceSyntax.synCop (Compiler.CompactSourceSyntax.synCin (Compiler.CompactSourceSyntax.synCkqrel Compiler.CompactSourceSyntax.synClefin) (Compiler.CompactSourceSyntax.synCxp Compiler.CompactSourceSyntax.synC0 Compiler.CompactSourceSyntax.synC0)) Compiler.CompactSourceSyntax.synC0))) (Compiler.CompactSourceSyntax.synCin (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC1st (Compiler.CompactSourceSyntax.synCif (SemanticCore.Wff.classMem (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synChwcn A)) (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synCop (Compiler.CompactSourceSyntax.synCin (Compiler.CompactSourceSyntax.synCkqrel Compiler.CompactSourceSyntax.synClefin) (Compiler.CompactSourceSyntax.synCxp Compiler.CompactSourceSyntax.synC0 Compiler.CompactSourceSyntax.synC0)) Compiler.CompactSourceSyntax.synC0))) (Compiler.CompactSourceSyntax.synCxp (Compiler.CompactSourceSyntax.synCin (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (Compiler.CompactSourceSyntax.synCif (SemanticCore.Wff.classMem (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synChwcn A)) (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synCop (Compiler.CompactSourceSyntax.synCin (Compiler.CompactSourceSyntax.synCkqrel Compiler.CompactSourceSyntax.synClefin) (Compiler.CompactSourceSyntax.synCxp Compiler.CompactSourceSyntax.synC0 Compiler.CompactSourceSyntax.synC0)) Compiler.CompactSourceSyntax.synC0))) (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC1st (Compiler.CompactSourceSyntax.synCif (SemanticCore.Wff.classMem (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synChwcn A)) (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synCop (Compiler.CompactSourceSyntax.synCin (Compiler.CompactSourceSyntax.synCkqrel Compiler.CompactSourceSyntax.synClefin) (Compiler.CompactSourceSyntax.synCxp Compiler.CompactSourceSyntax.synC0 Compiler.CompactSourceSyntax.synC0)) Compiler.CompactSourceSyntax.synC0))) Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv x)))) (Compiler.CompactSourceSyntax.synCin (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (Compiler.CompactSourceSyntax.synCif (SemanticCore.Wff.classMem (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synChwcn A)) (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synCop (Compiler.CompactSourceSyntax.synCin (Compiler.CompactSourceSyntax.synCkqrel Compiler.CompactSourceSyntax.synClefin) (Compiler.CompactSourceSyntax.synCxp Compiler.CompactSourceSyntax.synC0 Compiler.CompactSourceSyntax.synC0)) Compiler.CompactSourceSyntax.synC0))) (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC1st (Compiler.CompactSourceSyntax.synCif (SemanticCore.Wff.classMem (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synChwcn A)) (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synCop (Compiler.CompactSourceSyntax.synCin (Compiler.CompactSourceSyntax.synCkqrel Compiler.CompactSourceSyntax.synClefin) (Compiler.CompactSourceSyntax.synCxp Compiler.CompactSourceSyntax.synC0 Compiler.CompactSourceSyntax.synC0)) Compiler.CompactSourceSyntax.synC0))) Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv x)))))) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (Compiler.CompactSourceSyntax.synCif (SemanticCore.Wff.classMem (SemanticCore.Class.cv v) (Compiler.CompactSourceSyntax.synChwcn A)) (SemanticCore.Class.cv v) (Compiler.CompactSourceSyntax.synCop (Compiler.CompactSourceSyntax.synCin (Compiler.CompactSourceSyntax.synCkqrel Compiler.CompactSourceSyntax.synClefin) (Compiler.CompactSourceSyntax.synCxp Compiler.CompactSourceSyntax.synC0 Compiler.CompactSourceSyntax.synC0)) Compiler.CompactSourceSyntax.synC0))) (Compiler.CompactSourceSyntax.synCin (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (Compiler.CompactSourceSyntax.synCif (SemanticCore.Wff.classMem (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synChwcn A)) (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synCop (Compiler.CompactSourceSyntax.synCin (Compiler.CompactSourceSyntax.synCkqrel Compiler.CompactSourceSyntax.synClefin) (Compiler.CompactSourceSyntax.synCxp Compiler.CompactSourceSyntax.synC0 Compiler.CompactSourceSyntax.synC0)) Compiler.CompactSourceSyntax.synC0))) (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC1st (Compiler.CompactSourceSyntax.synCif (SemanticCore.Wff.classMem (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synChwcn A)) (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synCop (Compiler.CompactSourceSyntax.synCin (Compiler.CompactSourceSyntax.synCkqrel Compiler.CompactSourceSyntax.synClefin) (Compiler.CompactSourceSyntax.synCxp Compiler.CompactSourceSyntax.synC0 Compiler.CompactSourceSyntax.synC0)) Compiler.CompactSourceSyntax.synC0))) Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv x))))))))

Checked nominal proof certificate identified upstream as g_hncodecomparisontotalndv.

Equations

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