NF weak partition development: NominalWPPReplayChunk017Compact001Part090.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCfbfdwppcarrierimpndv (A R : SemanticCore.Class) (k : SemanticCore.Var) (X : SemanticCore.Class) (dv_A_R : Disjoint A.fv R.fv) (dv_A_X : Disjoint A.fv X.fv) (dv_A_k : k ∉ A.fv) (dv_R_X : Disjoint R.fv X.fv) (_dv_R_k : k ∉ R.fv) (dv_X_k : k ∉ X.fv) (hyp_cfbfdwppcarrierimpndv_1 : Nominal.NPrf (SemanticCore.Wff.classMem R Compiler.CompactSourceSyntax.synCvv)) (hyp_cfbfdwppcarrierimpndv_2 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) (hyp_cfbfdwppcarrierimpndv_3 : Nominal.NPrf (SemanticCore.Wff.classMem X Compiler.CompactSourceSyntax.synCvv)) (hyp_cfbfdwppcarrierimpndv_4 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synChncard (Compiler.CompactSourceSyntax.synCxp (Compiler.CompactSourceSyntax.synCxpk X X) Compiler.CompactSourceSyntax.synCnnc)) Compiler.CompactSourceSyntax.synClec (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synChncard X))))) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCwe A) (Compiler.CompactSourceSyntax.synWss A (Compiler.CompactSourceSyntax.synCpw X))).imp (Compiler.CompactSourceSyntax.synWwpp.imp (Compiler.CompactSourceSyntax.synWex k (Compiler.CompactSourceSyntax.synWf1 (SemanticCore.Class.cv k) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 A))) (Compiler.CompactSourceSyntax.synCpw (Compiler.CompactSourceSyntax.synCpw (Compiler.CompactSourceSyntax.synChnord X)))))))

Checked nominal proof certificate identified upstream as g_cfbfdwppcarrierimpndv.

Equations

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