Nominal proof certificates grouped in dependency order.

Certificates from NominalWPPReplayChunk017Compact001Part043.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHncodepredstrictdescentndv (x y z v u : SemanticCore.Var) (A : SemanticCore.Class) (dv_A_u : u ∉ A.fv) (dv_A_v : v ∉ A.fv) (dv_A_y : y ∉ A.fv) (dv_A_z : z ∉ A.fv) (dv_u_y : u ≠ y) (dv_u_z : u ≠ z) (dv_v_z : v ≠ z) (dv_x_z : x ≠ z) (dv_y_z : y ≠ z) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synChwcn A)) (SemanticCore.Wff.classMem (SemanticCore.Class.cv v) (Compiler.CompactSourceSyntax.synChwcn A))) (SemanticCore.Wff.classMem (SemanticCore.Class.cv y) (Compiler.CompactSourceSyntax.synChwcn A)))) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv 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)))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv y) (Compiler.CompactSourceSyntax.synCdif (Compiler.CompactSourceSyntax.synChncodecmpset A) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synChncodecmpset A))) (SemanticCore.Class.cv u)))).imp (Compiler.CompactSourceSyntax.synWrex z (Compiler.CompactSourceSyntax.synCin (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv v)) (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC1st (SemanticCore.Class.cv v)) Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv x)))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv y) (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 z)))))

Checked nominal proof certificate identified upstream as g_hncodepredstrictdescentndv.

Equations

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

Certificates from NominalWPPReplayChunk017Compact001Part044.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHncodepredrepminimalndv (x y z v u : SemanticCore.Var) (A X : SemanticCore.Class) (dv_A_u : u ∉ A.fv) (dv_A_v : v ∉ A.fv) (dv_A_y : y ∉ A.fv) (dv_A_z : z ∉ A.fv) (dv_X_y : y ∉ X.fv) (dv_X_z : z ∉ X.fv) (dv_u_y : u ≠ y) (_dv_u_z : u ≠ z) (dv_v_y : v ≠ y) (dv_v_z : v ≠ z) (dv_x_y : x ≠ y) (dv_x_z : x ≠ z) (dv_y_z : y ≠ z) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWss X (Compiler.CompactSourceSyntax.synChwcn A)) (SemanticCore.Wff.classMem (SemanticCore.Class.cv v) (Compiler.CompactSourceSyntax.synChwcn A)))) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) (Compiler.CompactSourceSyntax.synChncodepredends A X v)) (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv u) X) (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))))) (Compiler.CompactSourceSyntax.synWral z (Compiler.CompactSourceSyntax.synChncodepredends A X v) ((Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv z) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC1st (SemanticCore.Class.cv v)) (SemanticCore.Class.cv x)).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv z) (SemanticCore.Class.cv x)))))).imp (Compiler.CompactSourceSyntax.synWral y X ((Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv y) (Compiler.CompactSourceSyntax.synCdif (Compiler.CompactSourceSyntax.synChncodecmpset A) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synChncodecmpset A))) (SemanticCore.Class.cv u)).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv y) (SemanticCore.Class.cv u)))))

Checked nominal proof certificate identified upstream as g_hncodepredrepminimalndv.

Equations

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

Certificates from NominalWPPReplayChunk017Compact001Part045.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHncodepredemptyminimalndv (y v : SemanticCore.Var) (A X : SemanticCore.Class) (dv_A_v : v ∉ A.fv) (dv_A_y : y ∉ A.fv) (dv_X_y : y ∉ X.fv) (dv_v_y : v ≠ y) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWss X (Compiler.CompactSourceSyntax.synChwcn A)) (SemanticCore.Wff.classMem (SemanticCore.Class.cv v) X))) (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synChncodepredends A X v) Compiler.CompactSourceSyntax.synC0)).imp (Compiler.CompactSourceSyntax.synWral y X ((Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv y) (Compiler.CompactSourceSyntax.synCdif (Compiler.CompactSourceSyntax.synChncodecmpset A) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synChncodecmpset A))) (SemanticCore.Class.cv v)).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv y) (SemanticCore.Class.cv v)))))

Checked nominal proof certificate identified upstream as g_hncodepredemptyminimalndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWefrndv (D R : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCwe D).imp (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCfound D))

Checked nominal proof certificate identified upstream as g_wefrndv.

Equations

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

Certificates from NominalWPPReplayChunk017Compact001Part046.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHncodeprednonemptyminimalndv (z v u : SemanticCore.Var) (A X : SemanticCore.Class) (dv_A_u : u ∉ A.fv) (dv_A_v : v ∉ A.fv) (dv_A_z : z ∉ A.fv) (dv_X_u : u ∉ X.fv) (dv_X_z : z ∉ X.fv) (dv_u_v : u ≠ v) (dv_u_z : u ≠ z) (dv_v_z : v ≠ z) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv) (SemanticCore.Wff.classMem X Compiler.CompactSourceSyntax.synCvv)) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWss X (Compiler.CompactSourceSyntax.synChwcn A)) (SemanticCore.Wff.classMem (SemanticCore.Class.cv v) X))) (Compiler.CompactSourceSyntax.synWne (Compiler.CompactSourceSyntax.synChncodepredends A X v) Compiler.CompactSourceSyntax.synC0)).imp (Compiler.CompactSourceSyntax.synWrex u X (Compiler.CompactSourceSyntax.synWral z X ((Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv z) (Compiler.CompactSourceSyntax.synCdif (Compiler.CompactSourceSyntax.synChncodecmpset A) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synChncodecmpset A))) (SemanticCore.Class.cv u)).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv z) (SemanticCore.Class.cv u))))))

Checked nominal proof certificate identified upstream as g_hncodeprednonemptyminimalndv.

Equations

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