Search for blocks/addresses/...

Proofgold Address

address
PUStC47yrCBB3tWbbAUm3NFH128CSVGzJ2x
total
0
mg
-
conjpub
-
current assets
68592../89eea.. bday: 35044 doc published by PrHS6..
Param nat_primrecnat_primrec : ι(ιιι) → ιι
Definition 1319b.. := λ x0 . λ x1 : ι → ι . λ x2 . nat_primrec x2 (λ x3 . x1) x0
Known nat_primrec_0nat_primrec_0 : ∀ x0 . ∀ x1 : ι → ι → ι . nat_primrec x0 x1 0 = x0
Theorem 76108.. : ∀ x0 : ι → ι . ∀ x1 . 1319b.. 0 x0 x1 = x1 (proof)
Param omegaomega : ι
Param ordsuccordsucc : ιι
Param nat_pnat_p : ιο
Known nat_primrec_Snat_primrec_S : ∀ x0 . ∀ x1 : ι → ι → ι . ∀ x2 . nat_p x2nat_primrec x0 x1 (ordsucc x2) = x1 x2 (nat_primrec x0 x1 x2)
Known omega_nat_pomega_nat_p : ∀ x0 . x0omeganat_p x0
Theorem 99a2b.. : ∀ x0 . x0omega∀ x1 : ι → ι . ∀ x2 . 1319b.. (ordsucc x0) x1 x2 = x1 (1319b.. x0 x1 x2) (proof)
Known nat_indnat_ind : ∀ x0 : ι → ο . x0 0(∀ x1 . nat_p x1x0 x1x0 (ordsucc x1))∀ x1 . nat_p x1x0 x1
Known nat_p_omeganat_p_omega : ∀ x0 . nat_p x0x0omega
Theorem acd4e.. : ∀ x0 x1 . x1x0∀ x2 : ι → ι . (∀ x3 . x3x0x2 x3x0)∀ x3 . nat_p x31319b.. x3 x2 x1x0 (proof)
Theorem c6fca.. : ∀ x0 x1 . x1x0∀ x2 x3 : ι → ι . (∀ x4 . x4x0x2 x4x0)(∀ x4 . x4x0x2 x4 = x3 x4)∀ x4 . nat_p x41319b.. x4 x2 x1 = 1319b.. x4 x3 x1 (proof)
Theorem 9bb87.. : ∀ x0 x1 . x1x0∀ x2 x3 : ι → ι . (∀ x4 . x4x0x2 x4x0)∀ x4 : ι → ι . (∀ x5 . x5x0x4 (x2 x5) = x3 (x4 x5))∀ x5 . nat_p x5x4 (1319b.. x5 x2 x1) = 1319b.. x5 x3 (x4 x1) (proof)
Param lamSigma : ι(ιι) → ι
Param If_iIf_i : οιιι
Param apap : ιιι
Known tuple_2_0_eqtuple_2_0_eq : ∀ x0 x1 . ap (lam 2 (λ x3 . If_i (x3 = 0) x0 x1)) 0 = x0
Known tuple_2_1_eqtuple_2_1_eq : ∀ x0 x1 . ap (lam 2 (λ x3 . If_i (x3 = 0) x0 x1)) 1 = x1
Theorem 60ada.. : ∀ x0 x1 . nat_p x11319b.. x1 (λ x3 . lam 2 (λ x4 . If_i (x4 = 0) (ordsucc (ap x3 0)) (ap x3 1))) (lam 2 (λ x3 . If_i (x3 = 0) 0 x0)) = lam 2 (λ x3 . If_i (x3 = 0) x1 x0) (proof)
Param add_SNoadd_SNo : ιιι
Param minus_SNominus_SNo : ιι
Known minus_SNo_0minus_SNo_0 : minus_SNo 0 = 0
Param ordinalordinal : ιο
Known ordinal_ordsucc_SNo_eqordinal_ordsucc_SNo_eq : ∀ x0 . ordinal x0ordsucc x0 = add_SNo 1 x0
Known nat_p_ordinalnat_p_ordinal : ∀ x0 . nat_p x0ordinal x0
Param SNoSNo : ιο
Known add_SNo_comadd_SNo_com : ∀ x0 x1 . SNo x0SNo x1add_SNo x0 x1 = add_SNo x1 x0
Known SNo_1SNo_1 : SNo 1
Known minus_add_SNo_distrminus_add_SNo_distr : ∀ x0 x1 . SNo x0SNo x1minus_SNo (add_SNo x0 x1) = add_SNo (minus_SNo x0) (minus_SNo x1)
Known omega_SNoomega_SNo : ∀ x0 . x0omegaSNo x0
Theorem 7c549.. : ∀ x0 x1 . nat_p x11319b.. x1 (λ x3 . lam 2 (λ x4 . If_i (x4 = 0) (add_SNo (ap x3 0) (minus_SNo 1)) (ap x3 1))) (lam 2 (λ x3 . If_i (x3 = 0) 0 x0)) = lam 2 (λ x3 . If_i (x3 = 0) (minus_SNo x1) x0) (proof)
Param pack_upack_u : ι(ιι) → ι
Definition setprodsetprod := λ x0 x1 . lam x0 (λ x2 . x1)
Definition 340cb.. := λ x0 . pack_u (setprod omega x0) (λ x1 . lam 2 (λ x2 . If_i (x2 = 0) (ordsucc (ap x1 0)) (ap x1 1)))
Definition 9132f.. := λ x0 x1 x2 . lam (setprod omega x0) (λ x3 . lam 2 (λ x4 . If_i (x4 = 0) (ap x3 0) (ap x2 (ap x3 1))))
Definition 139e8.. := λ x0 . lam x0 (λ x1 . lam 2 (λ x2 . If_i (x2 = 0) 0 x1))
Param unpack_u_iunpack_u_i : ι(ι(ιι) → ι) → ι
Definition 82409.. := λ x0 . unpack_u_i x0 (λ x1 . λ x2 : ι → ι . lam (setprod omega x1) (λ x3 . 1319b.. (ap x3 0) x2 (ap x3 1)))
Param MetaAdjunction_strictMetaAdjunction_strict : (ιο) → (ιιιο) → (ιι) → (ιιιιιι) → (ιο) → (ιιιο) → (ιι) → (ιιιιιι) → (ιι) → (ιιιι) → (ιι) → (ιιιι) → (ιι) → (ιι) → ο
Param TrueTrue : ο
Param PiPi : ι(ιι) → ι
Definition setexpsetexp := λ x0 x1 . Pi x1 (λ x2 . x0)
Definition HomSetSetHom := λ x0 x1 x2 . x2setexp x1 x0
Definition lam_idlam_id := λ x0 . lam x0 (λ x1 . x1)
Definition lam_complam_comp := λ x0 x1 x2 . lam x0 (λ x3 . ap x1 (ap x2 x3))
Definition struct_ustruct_u := λ x0 . ∀ x1 : ι → ο . (∀ x2 . ∀ x3 : ι → ι . (∀ x4 . x4x2x3 x4x2)x1 (pack_u x2 x3))x1 x0
Param UnaryFuncHomHom_struct_u : ιιιο
Definition struct_idstruct_id := λ x0 . lam_id (ap x0 0)
Definition struct_compstruct_comp := λ x0 x1 x2 . lam_comp (ap x0 0)
Param MetaFunctor_strictMetaFunctor_strict : (ιο) → (ιιιο) → (ιι) → (ιιιιιι) → (ιο) → (ιιιο) → (ιι) → (ιιιιιι) → (ιι) → (ιιιι) → ο
Param MetaFunctorMetaFunctor : (ιο) → (ιιιο) → (ιι) → (ιιιιιι) → (ιο) → (ιιιο) → (ιι) → (ιιιιιι) → (ιι) → (ιιιι) → ο
Param MetaNatTransMetaNatTrans : (ιο) → (ιιιο) → (ιι) → (ιιιιιι) → (ιο) → (ιιιο) → (ιι) → (ιιιιιι) → (ιι) → (ιιιι) → (ιι) → (ιιιι) → (ιι) → ο
Param MetaAdjunctionMetaAdjunction : (ιο) → (ιιιο) → (ιι) → (ιιιιιι) → (ιο) → (ιιιο) → (ιι) → (ιιιιιι) → (ιι) → (ιιιι) → (ιι) → (ιιιι) → (ιι) → (ιι) → ο
Known d6aa5..MetaAdjunction_strict_I : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι → ο . ∀ x2 : ι → ι . ∀ x3 : ι → ι → ι → ι → ι → ι . ∀ x4 : ι → ο . ∀ x5 : ι → ι → ι → ο . ∀ x6 : ι → ι . ∀ x7 : ι → ι → ι → ι → ι → ι . ∀ x8 : ι → ι . ∀ x9 : ι → ι → ι → ι . ∀ x10 : ι → ι . ∀ x11 : ι → ι → ι → ι . ∀ x12 x13 : ι → ι . MetaFunctor_strict x0 x1 x2 x3 x4 x5 x6 x7 x8 x9MetaFunctor x4 x5 x6 x7 x0 x1 x2 x3 x10 x11MetaNatTrans x0 x1 x2 x3 x0 x1 x2 x3 (λ x14 . x14) (λ x14 x15 x16 . x16) (λ x14 . x10 (x8 x14)) (λ x14 x15 x16 . x11 (x8 x14) (x8 x15) (x9 x14 x15 x16)) x12MetaNatTrans x4 x5 x6 x7 x4 x5 x6 x7 (λ x14 . x8 (x10 x14)) (λ x14 x15 x16 . x9 (x10 x14) (x10 x15) (x11 x14 x15 x16)) (λ x14 . x14) (λ x14 x15 x16 . x16) x13MetaAdjunction x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13MetaAdjunction_strict x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13
Param MetaCatMetaCat : (ιο) → (ιιιο) → (ιι) → (ιιιιιι) → ο
Known 5cbb4..MetaFunctor_strict_I : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι → ο . ∀ x2 : ι → ι . ∀ x3 : ι → ι → ι → ι → ι → ι . ∀ x4 : ι → ο . ∀ x5 : ι → ι → ι → ο . ∀ x6 : ι → ι . ∀ x7 : ι → ι → ι → ι → ι → ι . ∀ x8 : ι → ι . ∀ x9 : ι → ι → ι → ι . MetaCat x0 x1 x2 x3MetaCat x4 x5 x6 x7MetaFunctor x0 x1 x2 x3 x4 x5 x6 x7 x8 x9MetaFunctor_strict x0 x1 x2 x3 x4 x5 x6 x7 x8 x9
Known e4125..MetaCatSet : MetaCat (λ x0 . True) HomSet lam_id (λ x0 x1 x2 . lam_comp x0)
Known 73eab..MetaCat_struct_u : MetaCat struct_u UnaryFuncHom struct_id struct_comp
Known 2cb62..MetaFunctorI : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι → ο . ∀ x2 : ι → ι . ∀ x3 : ι → ι → ι → ι → ι → ι . ∀ x4 : ι → ο . ∀ x5 : ι → ι → ι → ο . ∀ x6 : ι → ι . ∀ x7 : ι → ι → ι → ι → ι → ι . ∀ x8 : ι → ι . ∀ x9 : ι → ι → ι → ι . (∀ x10 . x0 x10x4 (x8 x10))(∀ x10 x11 x12 . x0 x10x0 x11x1 x10 x11 x12x5 (x8 x10) (x8 x11) (x9 x10 x11 x12))(∀ x10 . x0 x10x9 x10 x10 (x2 x10) = x6 (x8 x10))(∀ x10 x11 x12 x13 x14 . x0 x10x0 x11x0 x12x1 x10 x11 x13x1 x11 x12 x14x9 x10 x12 (x3 x10 x11 x12 x14 x13) = x7 (x8 x10) (x8 x11) (x8 x12) (x9 x11 x12 x14) (x9 x10 x11 x13))MetaFunctor x0 x1 x2 x3 x4 x5 x6 x7 x8 x9
Known pack_struct_u_Ipack_struct_u_I : ∀ x0 . ∀ x1 : ι → ι . (∀ x2 . x2x0x1 x2x0)struct_u (pack_u x0 x1)
Definition andand := λ x0 x1 : ο . ∀ x2 : ο . (x0x1x2)x2
Known 66c4c..Hom_struct_u_pack : ∀ x0 x1 . ∀ x2 x3 : ι → ι . ∀ x4 . UnaryFuncHom (pack_u x0 x2) (pack_u x1 x3) x4 = and (x4setexp x1 x0) (∀ x6 . x6x0ap x4 (x2 x6) = x3 (ap x4 x6))
Known andIandI : ∀ x0 x1 : ο . x0x1and x0 x1
Known lam_Pilam_Pi : ∀ x0 . ∀ x1 x2 : ι → ι . (∀ x3 . x3x0x2 x3x1 x3)lam x0 x2Pi x0 x1
Known tuple_2_setprodtuple_2_setprod : ∀ x0 x1 x2 . x2x0∀ x3 . x3x1lam 2 (λ x4 . If_i (x4 = 0) x2 x3)setprod x0 x1
Known ap0_Sigmaap0_Sigma : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2lam x0 x1ap x2 0x0
Known ap_Piap_Pi : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 x3 . x2Pi x0 x1x3x0ap x2 x3x1 x3
Known ap1_Sigmaap1_Sigma : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2lam x0 x1ap x2 1x1 (ap x2 0)
Known betabeta : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2x0ap (lam x0 x1) x2 = x1 x2
Known pack_u_0_eq2pack_u_0_eq2 : ∀ x0 . ∀ x1 : ι → ι . x0 = ap (pack_u x0 x1) 0
Known encode_u_extencode_u_ext : ∀ x0 . ∀ x1 x2 : ι → ι . (∀ x3 . x3x0x1 x3 = x2 x3)lam x0 x1 = lam x0 x2
Known tuple_Sigma_etatuple_Sigma_eta : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2lam x0 x1lam 2 (λ x4 . If_i (x4 = 0) (ap x2 0) (ap x2 1)) = x2
Known 0032d..MetaCat_struct_u_Forgetful : MetaFunctor struct_u UnaryFuncHom struct_id struct_comp (λ x0 . True) HomSet lam_id (λ x0 x1 x2 . lam_comp x0) (λ x0 . ap x0 0) (λ x0 x1 x2 . x2)
Known c1d68..MetaNatTransI : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι → ο . ∀ x2 : ι → ι . ∀ x3 : ι → ι → ι → ι → ι → ι . ∀ x4 : ι → ο . ∀ x5 : ι → ι → ι → ο . ∀ x6 : ι → ι . ∀ x7 : ι → ι → ι → ι → ι → ι . ∀ x8 : ι → ι . ∀ x9 : ι → ι → ι → ι . ∀ x10 : ι → ι . ∀ x11 : ι → ι → ι → ι . ∀ x12 : ι → ι . (∀ x13 . x0 x13x5 (x8 x13) (x10 x13) (x12 x13))(∀ x13 x14 x15 . x0 x13x0 x14x1 x13 x14 x15x7 (x8 x13) (x10 x13) (x10 x14) (x11 x13 x14 x15) (x12 x13) = x7 (x8 x13) (x8 x14) (x10 x14) (x12 x14) (x9 x13 x14 x15))MetaNatTrans x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12
Known nat_0nat_0 : nat_p 0
Known omega_ordsuccomega_ordsucc : ∀ x0 . x0omegaordsucc x0omega
Known fd494..MetaAdjunctionI : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι → ο . ∀ x2 : ι → ι . ∀ x3 : ι → ι → ι → ι → ι → ι . ∀ x4 : ι → ο . ∀ x5 : ι → ι → ι → ο . ∀ x6 : ι → ι . ∀ x7 : ι → ι → ι → ι → ι → ι . ∀ x8 : ι → ι . ∀ x9 : ι → ι → ι → ι . ∀ x10 : ι → ι . ∀ x11 : ι → ι → ι → ι . ∀ x12 x13 : ι → ι . (∀ x14 . x0 x14x7 (x8 x14) (x8 (x10 (x8 x14))) (x8 x14) (x13 (x8 x14)) (x9 x14 (x10 (x8 x14)) (x12 x14)) = x6 (x8 x14))(∀ x14 . x4 x14x3 (x10 x14) (x10 (x8 (x10 x14))) (x10 x14) (x11 (x8 (x10 x14)) x14 (x13 x14)) (x12 (x10 x14)) = x2 (x10 x14))MetaAdjunction x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13
Known unpack_u_i_equnpack_u_i_eq : ∀ x0 : ι → (ι → ι) → ι . ∀ x1 . ∀ x2 : ι → ι . (∀ x3 : ι → ι . (∀ x4 . x4x1x2 x4 = x3 x4)x0 x1 x3 = x0 x1 x2)unpack_u_i (pack_u x1 x2) x0 = x0 x1 x2
Theorem 6722a.. : MetaAdjunction_strict (λ x0 . True) HomSet lam_id (λ x0 x1 x2 . lam_comp x0) struct_u UnaryFuncHom struct_id struct_comp 340cb.. 9132f.. (λ x0 . ap x0 0) (λ x0 x1 x2 . x2) 139e8.. 82409.. (proof)
Theorem ed3d2..MetaCat_struct_u_left_adjoint_forgetful : ∀ x0 : ο . (∀ x1 : ι → ι . (∀ x2 : ο . (∀ x3 : ι → ι → ι → ι . (∀ x4 : ο . (∀ x5 : ι → ι . (∀ x6 : ο . (∀ x7 : ι → ι . MetaAdjunction_strict (λ x8 . True) HomSet lam_id (λ x8 x9 x10 . lam_comp x8) struct_u UnaryFuncHom struct_id struct_comp x1 x3 (λ x8 . ap x8 0) (λ x8 x9 x10 . x10) x5 x7x6)x6)x4)x4)x2)x2)x0)x0 (proof)
Param unpack_u_ounpack_u_o : ι(ι(ιι) → ο) → ο
Definition injinj := λ x0 x1 . λ x2 : ι → ι . and (∀ x3 . x3x0x2 x3x1) (∀ x3 . x3x0∀ x4 . x4x0x2 x3 = x2 x4x3 = x4)
Definition SelfInjectionstruct_u_inj := λ x0 . and (struct_u x0) (unpack_u_o x0 (λ x1 . inj x1 x1))
Known 6bcb5..MetaCat_struct_u_inj : MetaCat SelfInjection UnaryFuncHom struct_id struct_comp
Known unpack_u_o_equnpack_u_o_eq : ∀ x0 : ι → (ι → ι) → ο . ∀ x1 . ∀ x2 : ι → ι . (∀ x3 : ι → ι . (∀ x4 . x4x1x2 x4 = x3 x4)x0 x1 x3 = x0 x1 x2)unpack_u_o (pack_u x1 x2) x0 = x0 x1 x2
Known tuple_2_injtuple_2_inj : ∀ x0 x1 x2 x3 . lam 2 (λ x5 . If_i (x5 = 0) x0 x1) = lam 2 (λ x5 . If_i (x5 = 0) x2 x3)and (x0 = x2) (x1 = x3)
Known ordsucc_injordsucc_inj : ∀ x0 x1 . ordsucc x0 = ordsucc x1x0 = x1
Known 1687d..MetaCat_struct_u_inj_Forgetful : MetaFunctor SelfInjection UnaryFuncHom struct_id struct_comp (λ x0 . True) HomSet lam_id (λ x0 x1 x2 . lam_comp x0) (λ x0 . ap x0 0) (λ x0 x1 x2 . x2)
Known prop_ext_2prop_ext_2 : ∀ x0 x1 : ο . (x0x1)(x1x0)x0 = x1
Theorem 68f23.. : MetaAdjunction_strict (λ x0 . True) HomSet lam_id (λ x0 x1 x2 . lam_comp x0) SelfInjection UnaryFuncHom struct_id struct_comp 340cb.. 9132f.. (λ x0 . ap x0 0) (λ x0 x1 x2 . x2) 139e8.. 82409.. (proof)
Theorem 8822b..MetaCat_struct_u_inj_left_adjoint_forgetful : ∀ x0 : ο . (∀ x1 : ι → ι . (∀ x2 : ο . (∀ x3 : ι → ι → ι → ι . (∀ x4 : ο . (∀ x5 : ι → ι . (∀ x6 : ο . (∀ x7 : ι → ι . MetaAdjunction_strict (λ x8 . True) HomSet lam_id (λ x8 x9 x10 . lam_comp x8) SelfInjection UnaryFuncHom struct_id struct_comp x1 x3 (λ x8 . ap x8 0) (λ x8 x9 x10 . x10) x5 x7x6)x6)x4)x4)x2)x2)x0)x0 (proof)

previous assets