LeanPool.NFWeakPartition.Certificates.NominalWPPReplayChunk017Compact001Block009

source

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHncodecmpstrictnoreversendv (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) :

Checked nominal proof certificate identified upstream as g_hncodecmpstrictnoreversendv.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHncodecmpkerptndv (v u : SemanticCore.Var) (A : SemanticCore.Class) (dv_A_u : u ∉ A.fv) (dv_A_v : v ∉ A.fv) (dv_u_v : u ≠ v) :

Checked nominal proof certificate identified upstream as g_hncodecmpkerptndv.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHncodecmplnkerndv (A : SemanticCore.Class) :

Nominal.NPrf ((SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synClnker (Compiler.CompactSourceSyntax.synChncodecmpset A)) (Compiler.CompactSourceSyntax.synChwniso A)))

Checked nominal proof certificate identified upstream as g_hncodecmplnkerndv.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHncodecmpstrictbrndv (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_v : u ≠ v) (dv_u_x : u ≠ x) (dv_v_x : v ≠ x) :

Checked nominal proof certificate identified upstream as g_hncodecmpstrictbrndv.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHncodecutfnex :

Nominal.NPrf (SemanticCore.Wff.classMem Compiler.CompactSourceSyntax.synChncodecutfn Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_hncodecutfnex.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHncodepredinputsexg (v : SemanticCore.Var) (A X : SemanticCore.Class) (_dv_A_v : v ∉ A.fv) :

Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv) (SemanticCore.Wff.classMem X Compiler.CompactSourceSyntax.synCvv)).imp (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synChncodepredinputs A X v) Compiler.CompactSourceSyntax.synCvv))

Checked nominal proof certificate identified upstream as g_hncodepredinputsexg.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHncodepredinputsssndv (v : SemanticCore.Var) (A X : SemanticCore.Class) (_dv_A_v : v ∉ A.fv) :

Nominal.NPrf (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synChncodepredinputs A X v) (Compiler.CompactSourceSyntax.synCxp (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv v)) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv v)))))

Checked nominal proof certificate identified upstream as g_hncodepredinputsssndv.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHncodepredinputmemndv (x v u : SemanticCore.Var) (A X : SemanticCore.Class) (dv_A_u : u ∉ A.fv) (dv_A_v : v ∉ A.fv) (dv_X_u : u ∉ X.fv) (dv_u_v : u ≠ v) (dv_u_x : u ≠ x) :

Checked nominal proof certificate identified upstream as g_hncodepredinputmemndv.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHncodepredendsexg (v : SemanticCore.Var) (A X : SemanticCore.Class) (dv_A_v : v ∉ A.fv) :

Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv) (SemanticCore.Wff.classMem X Compiler.CompactSourceSyntax.synCvv)).imp (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synChncodepredends A X v) Compiler.CompactSourceSyntax.synCvv))

Checked nominal proof certificate identified upstream as g_hncodepredendsexg.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHncodepredendsmemndv (x v u : SemanticCore.Var) (A X : SemanticCore.Class) (dv_A_u : u ∉ A.fv) (dv_A_v : v ∉ A.fv) (dv_X_u : u ∉ X.fv) (dv_u_v : u ≠ v) (dv_u_x : u ≠ x) :

Checked nominal proof certificate identified upstream as g_hncodepredendsmemndv.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHncodepredendsssndv (v : SemanticCore.Var) (A X : SemanticCore.Class) (dv_A_v : v ∉ A.fv) :

Nominal.NPrf ((SemanticCore.Wff.classMem (SemanticCore.Class.cv v) (Compiler.CompactSourceSyntax.synChwcn A)).imp (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synChncodepredends A X v) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv v))))

Checked nominal proof certificate identified upstream as g_hncodepredendsssndv.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHnwcutcodetransportintocutsegndv (x y z v u : SemanticCore.Var) (A : SemanticCore.Class) (dv_A_u : u ∉ A.fv) (dv_A_v : v ∉ A.fv) (dv_A_z : z ∉ A.fv) (dv_u_z : u ≠ z) (dv_v_z : v ≠ z) (dv_x_z : x ≠ z) (dv_y_z : y ≠ z) :

Checked nominal proof certificate identified upstream as g_hnwcutcodetransportintocutsegndv.

Equations

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

Instances For