NF weak partition development: NominalWPPReplayChunk017Compact001Part083.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHninjraisedselfcutalldndv (x u : SemanticCore.Var) (A : SemanticCore.Class) (f s r : SemanticCore.Var) (_dv_A_f : f ∉ A.fv) (dv_A_r : r ∉ A.fv) (_dv_A_s : s ∉ A.fv) (dv_A_u : u ∉ A.fv) (dv_A_x : x ∉ A.fv) (_dv_f_r : f ≠ r) (_dv_f_s : f ≠ s) (dv_f_u : f ≠ u) (dv_f_x : f ≠ x) (_dv_r_s : r ≠ s) (dv_r_u : r ≠ u) (dv_r_x : r ≠ x) (dv_s_u : s ≠ u) (dv_s_x : s ≠ x) (dv_u_x : u ≠ x) (hyp_hninjraisedselfcutalldndv_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWf1 (SemanticCore.Class.cv f) (Compiler.CompactSourceSyntax.synChnord A) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 A))) (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classEq (SemanticCore.Class.cv r) (Compiler.CompactSourceSyntax.synChncodecmpset A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv s) (Compiler.CompactSourceSyntax.synClnqord (SemanticCore.Class.cv r) (Compiler.CompactSourceSyntax.synChwcn A))))).imp (Compiler.CompactSourceSyntax.synWrex u (Compiler.CompactSourceSyntax.synChwcn (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 A))) (Compiler.CompactSourceSyntax.synWrex x (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synChwniso (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 A))) (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_hninjraisedselfcutalldndv.

Equations

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