Proofgold Address

Param unpack_p_i^unpack_p_i : ι → (ι → (ι → ο) → ι) → ι
Param pack_p^pack_p : ι → (ι → ο) → ι
Param Sep^Sep : ι → (ι → ο) → ι
Param ap^ap : ι → ι → ι
Definition 2d9d0.. := λ x0 x1 x2 x3 . unpack_p_i x0 (λ x4 . pack_p {x5 ∈ x4|ap x2 x5 = ap x3 x5})
Definition and^and := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x1 ⟶ x2) ⟶ x2
Definition iff^iff := λ x0 x1 : ο . and (x0 ⟶ x1) (x1 ⟶ x0)
Known unpack_p_i_eq^{unpack_p_i_eq} : ∀ x0 : ι → (ι → ο) → ι . ∀ x1 . ∀ x2 : ι → ο . (∀ x3 : ι → ο . (∀ x4 . x4 ∈ x1 ⟶ iff (x2 x4) (x3 x4)) ⟶ x0 x1 x3 = x0 x1 x2) ⟶ unpack_p_i (pack_p x1 x2) x0 = x0 x1 x2
Known pack_p_ext^pack_p_ext : ∀ x0 . ∀ x1 x2 : ι → ο . (∀ x3 . x3 ∈ x0 ⟶ iff (x1 x3) (x2 x3)) ⟶ pack_p x0 x1 = pack_p x0 x2
Known SepE1^SepE1 : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . x2 ∈ Sep x0 x1 ⟶ x2 ∈ x0
Known iffI^iffI : ∀ x0 x1 : ο . (x0 ⟶ x1) ⟶ (x1 ⟶ x0) ⟶ iff x0 x1
Theorem 49a9d.. : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 x3 x4 . 2d9d0.. (pack_p x0 x1) x2 x3 x4 = pack_p {x6 ∈ x0|ap x3 x6 = ap x4 x6} x1 (proof)
Definition struct_p^struct_p := λ x0 . ∀ x1 : ι → ο . (∀ x2 . ∀ x3 : ι → ο . x1 (pack_p x2 x3)) ⟶ x1 x0
Param UnaryPredHom^Hom_struct_p : ι → ι → ι → ο
Definition MetaCat_equalizer_p^equalizer_p := λ x0 : ι → ο . λ x1 : ι → ι → ι → ο . λ x2 : ι → ι . λ x3 : ι → ι → ι → ι → ι → ι . λ x4 x5 x6 x7 x8 x9 . λ x10 : ι → ι → ι . and (and (and (and (and (and (and (x0 x4) (x0 x5)) (x1 x4 x5 x6)) (x1 x4 x5 x7)) (x0 x8)) (x1 x8 x4 x9)) (x3 x8 x4 x5 x6 x9 = x3 x8 x4 x5 x7 x9)) (∀ x11 . x0 x11 ⟶ ∀ x12 . x1 x11 x4 x12 ⟶ x3 x11 x4 x5 x6 x12 = x3 x11 x4 x5 x7 x12 ⟶ and (and (x1 x11 x8 (x10 x11 x12)) (x3 x11 x8 x4 x9 (x10 x11 x12) = x12)) (∀ x13 . x1 x11 x8 x13 ⟶ x3 x11 x8 x4 x9 x13 = x12 ⟶ x13 = x10 x11 x12))
Definition MetaCat_equalizer_struct_p^{equalizer_constr_p} := λ x0 : ι → ο . λ x1 : ι → ι → ι → ο . λ x2 : ι → ι . λ x3 : ι → ι → ι → ι → ι → ι . λ x4 x5 : ι → ι → ι → ι → ι . λ x6 : ι → ι → ι → ι → ι → ι → ι . ∀ x7 x8 . x0 x7 ⟶ x0 x8 ⟶ ∀ x9 x10 . x1 x7 x8 x9 ⟶ x1 x7 x8 x10 ⟶ MetaCat_equalizer_p x0 x1 x2 x3 x7 x8 x9 x10 (x4 x7 x8 x9 x10) (x5 x7 x8 x9 x10) (x6 x7 x8 x9 x10)
Param struct_id^struct_id : ι → ι
Param lam^Sigma : ι → (ι → ι) → ι
Definition lam_comp^lam_comp := λ x0 x1 x2 . lam x0 (λ x3 . ap x1 (ap x2 x3))
Definition struct_comp^struct_comp := λ x0 x1 x2 . lam_comp (ap x0 0)
Known 41253..^and8I : ∀ x0 x1 x2 x3 x4 x5 x6 x7 : ο . x0 ⟶ x1 ⟶ x2 ⟶ x3 ⟶ x4 ⟶ x5 ⟶ x6 ⟶ x7 ⟶ and (and (and (and (and (and (and x0 x1) x2) x3) x4) x5) x6) x7
Param Pi^Pi : ι → (ι → ι) → ι
Definition setexp^setexp := λ x0 x1 . Pi x1 (λ x2 . x0)
Known 55fb5..^{Hom_struct_p_pack} : ∀ x0 x1 . ∀ x2 x3 : ι → ο . ∀ x4 . UnaryPredHom (pack_p x0 x2) (pack_p x1 x3) x4 = and (x4 ∈ setexp x1 x0) (∀ x6 . x6 ∈ x0 ⟶ x2 x6 ⟶ x3 (ap x4 x6))
Known pack_p_0_eq2^pack_p_0_eq2 : ∀ x0 . ∀ x1 : ι → ο . x0 = ap (pack_p x0 x1) 0
Known andI^andI : ∀ x0 x1 : ο . x0 ⟶ x1 ⟶ and x0 x1
Known lam_Pi^lam_Pi : ∀ x0 . ∀ x1 x2 : ι → ι . (∀ x3 . x3 ∈ x0 ⟶ x2 x3 ∈ x1 x3) ⟶ lam x0 x2 ∈ Pi x0 x1
Known beta^beta : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2 ∈ x0 ⟶ ap (lam x0 x1) x2 = x1 x2
Known encode_u_ext^encode_u_ext : ∀ x0 . ∀ x1 x2 : ι → ι . (∀ x3 . x3 ∈ x0 ⟶ x1 x3 = x2 x3) ⟶ lam x0 x1 = lam x0 x2
Known SepE2^SepE2 : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . x2 ∈ Sep x0 x1 ⟶ x1 x2
Known and3I^and3I : ∀ x0 x1 x2 : ο . x0 ⟶ x1 ⟶ x2 ⟶ and (and x0 x1) x2
Known Pi_eta^Pi_eta : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2 ∈ Pi x0 x1 ⟶ lam x0 (ap x2) = x2
Known ap_Pi^ap_Pi : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 x3 . x2 ∈ Pi x0 x1 ⟶ x3 ∈ x0 ⟶ ap x2 x3 ∈ x1 x3
Known SepI^SepI : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . x2 ∈ x0 ⟶ x1 x2 ⟶ x2 ∈ Sep x0 x1
Theorem 380d6.. : ∀ x0 : ι → ο . (∀ x1 . x0 x1 ⟶ struct_p x1) ⟶ (∀ x1 x2 x3 x4 . x0 x1 ⟶ x0 x2 ⟶ UnaryPredHom x1 x2 x3 ⟶ UnaryPredHom x1 x2 x4 ⟶ x0 (2d9d0.. x1 x2 x3 x4)) ⟶ ∀ x1 : ο . (∀ x2 : ι → ι → ι → ι → ι . (∀ x3 : ο . (∀ x4 : ι → ι → ι → ι → ι . (∀ x5 : ο . (∀ x6 : ι → ι → ι → ι → ι → ι → ι . MetaCat_equalizer_struct_p x0 UnaryPredHom struct_id struct_comp x2 x4 x6 ⟶ x5) ⟶ x5) ⟶ x3) ⟶ x3) ⟶ x1) ⟶ x1 (proof)
Known pack_struct_p_I^{pack_struct_p_I} : ∀ x0 . ∀ x1 : ι → ο . struct_p (pack_p x0 x1)
Theorem 56101..^{MetaCat_struct_p_equalizer_constr} : ∀ x0 : ο . (∀ x1 : ι → ι → ι → ι → ι . (∀ x2 : ο . (∀ x3 : ι → ι → ι → ι → ι . (∀ x4 : ο . (∀ x5 : ι → ι → ι → ι → ι → ι → ι . MetaCat_equalizer_struct_p struct_p UnaryPredHom struct_id struct_comp x1 x3 x5 ⟶ x4) ⟶ x4) ⟶ x2) ⟶ x2) ⟶ x0) ⟶ x0 (proof)
Param MetaCat^MetaCat : (ι → ο) → (ι → ι → ι → ο) → (ι → ι) → (ι → ι → ι → ι → ι → ι) → ο
Known caa5e..^{MetaCat_struct_p} : MetaCat struct_p UnaryPredHom struct_id struct_comp
Definition MetaCat_pullback_p^pullback_p := λ x0 : ι → ο . λ x1 : ι → ι → ι → ο . λ x2 : ι → ι . λ x3 : ι → ι → ι → ι → ι → ι . λ x4 x5 x6 x7 x8 x9 x10 x11 . λ x12 : ι → ι → ι → ι . and (and (and (and (and (and (and (and (and (x0 x4) (x0 x5)) (x0 x6)) (x1 x4 x6 x7)) (x1 x5 x6 x8)) (x0 x9)) (x1 x9 x4 x10)) (x1 x9 x5 x11)) (x3 x9 x4 x6 x7 x10 = x3 x9 x5 x6 x8 x11)) (∀ x13 . x0 x13 ⟶ ∀ x14 . x1 x13 x4 x14 ⟶ ∀ x15 . x1 x13 x5 x15 ⟶ x3 x13 x4 x6 x7 x14 = x3 x13 x5 x6 x8 x15 ⟶ and (and (and (x1 x13 x9 (x12 x13 x14 x15)) (x3 x13 x9 x4 x10 (x12 x13 x14 x15) = x14)) (x3 x13 x9 x5 x11 (x12 x13 x14 x15) = x15)) (∀ x16 . x1 x13 x9 x16 ⟶ x3 x13 x9 x4 x10 x16 = x14 ⟶ x3 x13 x9 x5 x11 x16 = x15 ⟶ x16 = x12 x13 x14 x15))
Definition MetaCat_pullback_struct_p^{pullback_constr_p} := λ x0 : ι → ο . λ x1 : ι → ι → ι → ο . λ x2 : ι → ι . λ x3 x4 x5 x6 : ι → ι → ι → ι → ι → ι . λ x7 : ι → ι → ι → ι → ι → ι → ι → ι → ι . ∀ x8 x9 x10 . x0 x8 ⟶ x0 x9 ⟶ x0 x10 ⟶ ∀ x11 x12 . x1 x8 x10 x11 ⟶ x1 x9 x10 x12 ⟶ MetaCat_pullback_p x0 x1 x2 x3 x8 x9 x10 x11 x12 (x4 x8 x9 x10 x11 x12) (x5 x8 x9 x10 x11 x12) (x6 x8 x9 x10 x11 x12) (x7 x8 x9 x10 x11 x12)
Param MetaCat_product_constr_p^{product_constr_p} : (ι → ο) → (ι → ι → ι → ο) → (ι → ι) → (ι → ι → ι → ι → ι → ι) → (ι → ι → ι) → (ι → ι → ι) → (ι → ι → ι) → (ι → ι → ι → ι → ι → ι) → ο
Known ed2b0..^{product_equalizer_pullback_constr_ex} : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι → ο . ∀ x2 : ι → ι . ∀ x3 : ι → ι → ι → ι → ι → ι . MetaCat x0 x1 x2 x3 ⟶ (∀ x4 : ο . (∀ x5 : ι → ι → ι → ι → ι . (∀ x6 : ο . (∀ x7 : ι → ι → ι → ι → ι . (∀ x8 : ο . (∀ x9 : ι → ι → ι → ι → ι → ι → ι . MetaCat_equalizer_struct_p x0 x1 x2 x3 x5 x7 x9 ⟶ x8) ⟶ x8) ⟶ x6) ⟶ x6) ⟶ x4) ⟶ x4) ⟶ (∀ x4 : ο . (∀ x5 : ι → ι → ι . (∀ x6 : ο . (∀ x7 : ι → ι → ι . (∀ x8 : ο . (∀ x9 : ι → ι → ι . (∀ x10 : ο . (∀ x11 : ι → ι → ι → ι → ι → ι . MetaCat_product_constr_p x0 x1 x2 x3 x5 x7 x9 x11 ⟶ x10) ⟶ x10) ⟶ x8) ⟶ x8) ⟶ x6) ⟶ x6) ⟶ x4) ⟶ x4) ⟶ ∀ x4 : ο . (∀ x5 : ι → ι → ι → ι → ι → ι . (∀ x6 : ο . (∀ x7 : ι → ι → ι → ι → ι → ι . (∀ x8 : ο . (∀ x9 : ι → ι → ι → ι → ι → ι . (∀ x10 : ο . (∀ x11 : ι → ι → ι → ι → ι → ι → ι → ι → ι . MetaCat_pullback_struct_p x0 x1 x2 x3 x5 x7 x9 x11 ⟶ x10) ⟶ x10) ⟶ x8) ⟶ x8) ⟶ x6) ⟶ x6) ⟶ x4) ⟶ x4
Known 4f9ac..^{MetaCat_struct_p_product_constr} : ∀ x0 : ο . (∀ x1 : ι → ι → ι . (∀ x2 : ο . (∀ x3 : ι → ι → ι . (∀ x4 : ο . (∀ x5 : ι → ι → ι . (∀ x6 : ο . (∀ x7 : ι → ι → ι → ι → ι → ι . MetaCat_product_constr_p struct_p UnaryPredHom struct_id struct_comp x1 x3 x5 x7 ⟶ x6) ⟶ x6) ⟶ x4) ⟶ x4) ⟶ x2) ⟶ x2) ⟶ x0) ⟶ x0
Theorem 8ba3f..^{MetaCat_struct_p_pullback_constr} : ∀ x0 : ο . (∀ x1 : ι → ι → ι → ι → ι → ι . (∀ x2 : ο . (∀ x3 : ι → ι → ι → ι → ι → ι . (∀ x4 : ο . (∀ x5 : ι → ι → ι → ι → ι → ι . (∀ x6 : ο . (∀ x7 : ι → ι → ι → ι → ι → ι → ι → ι → ι . MetaCat_pullback_struct_p struct_p UnaryPredHom struct_id struct_comp x1 x3 x5 x7 ⟶ x6) ⟶ x6) ⟶ x4) ⟶ x4) ⟶ x2) ⟶ x2) ⟶ x0) ⟶ x0 (proof)
Definition False^False := ∀ x0 : ο . x0
Definition not^not := λ x0 : ο . x0 ⟶ False
Param PtdPred^{struct_p_nonempty} : ι → ο
Param ordsucc^ordsucc : ι → ι
Definition True^True := ∀ x0 : ο . x0 ⟶ x0
Known FalseE^FalseE : False ⟶ ∀ x0 : ο . x0
Known d8d91.. : ∀ x0 . PtdPred x0 ⟶ ∀ x1 : ι → ο . (∀ x2 . ∀ x3 : ι → ο . ∀ x4 . x4 ∈ x2 ⟶ x3 x4 ⟶ x1 (pack_p x2 x3)) ⟶ x1 x0
Known neq_0_1^neq_0_1 : 0 = 1 ⟶ ∀ x0 : ο . x0
Known In_1_2^In_1_2 : 1 ∈ 2
Known In_0_2^In_0_2 : 0 ∈ 2
Known 93af6.. : ∀ x0 . ∀ x1 : ι → ο . (∀ x2 : ο . (∀ x3 . and (x3 ∈ x0) (x1 x3) ⟶ x2) ⟶ x2) ⟶ PtdPred (pack_p x0 x1)
Known TrueI^TrueI : True
Known In_0_1^In_0_1 : 0 ∈ 1
Theorem 6eec9.. : not (∀ x0 : ο . (∀ x1 : ι → ι → ι → ι → ι . (∀ x2 : ο . (∀ x3 : ι → ι → ι → ι → ι . (∀ x4 : ο . (∀ x5 : ι → ι → ι → ι → ι → ι → ι . MetaCat_equalizer_struct_p PtdPred UnaryPredHom struct_id struct_comp x1 x3 x5 ⟶ x4) ⟶ x4) ⟶ x2) ⟶ x2) ⟶ x0) ⟶ x0) (proof)
Theorem 4b38a.. : not (∀ x0 : ο . (∀ x1 : ι → ι → ι → ι → ι → ι . (∀ x2 : ο . (∀ x3 : ι → ι → ι → ι → ι → ι . (∀ x4 : ο . (∀ x5 : ι → ι → ι → ι → ι → ι . (∀ x6 : ο . (∀ x7 : ι → ι → ι → ι → ι → ι → ι → ι → ι . MetaCat_pullback_struct_p PtdPred UnaryPredHom struct_id struct_comp x1 x3 x5 x7 ⟶ x6) ⟶ x6) ⟶ x4) ⟶ x4) ⟶ x2) ⟶ x2) ⟶ x0) ⟶ x0) (proof)