Param nat_p^nat_p : ι → ο
Param ordsucc^ordsucc : ι → ι
Definition u1 := 1
Definition u2 := ordsucc u1
Definition u3 := ordsucc u2
Definition u4 := ordsucc u3
Definition u5 := ordsucc u4
Definition u6 := ordsucc u5
Definition u7 := ordsucc u6
Definition u8 := ordsucc u7
Definition u9 := ordsucc u8
Definition u10 := ordsucc u9
Definition u11 := ordsucc u10
Definition u12 := ordsucc u11
Definition u13 := ordsucc u12
Definition u14 := ordsucc u13
Definition u15 := ordsucc u14
Definition u16 := ordsucc u15
Definition u17 := ordsucc u16
Definition u18 := ordsucc u17
Definition u19 := ordsucc u18
Definition u20 := ordsucc u19
Definition u21 := ordsucc u20
Definition u22 := ordsucc u21
Definition u23 := ordsucc u22
Definition u24 := ordsucc u23
Definition u25 := ordsucc u24
Definition u26 := ordsucc u25
Definition u27 := ordsucc u26
Definition u28 := ordsucc u27
Definition u29 := ordsucc u28
Definition u30 := ordsucc u29
Definition u31 := ordsucc u30
Definition u32 := ordsucc u31
Definition u33 := ordsucc u32
Definition u34 := ordsucc u33
Definition u35 := ordsucc u34
Definition u36 := ordsucc u35
Definition u37 := ordsucc u36
Known nat_ordsucc^nat_ordsucc : ∀ x0 . nat_p x0 ⟶ nat_p (ordsucc x0)
Known 4aca7.. : nat_p u36
Theorem 36e82.. : nat_p u37 (proof)
Definition u38 := ordsucc u37
Theorem b010c.. : nat_p u38 (proof)
Definition u39 := ordsucc u38
Theorem 29daf.. : nat_p u39 (proof)
Definition u40 := ordsucc u39
Theorem 9c301.. : nat_p u40 (proof)
Definition u41 := ordsucc u40
Theorem 61d53.. : nat_p u41 (proof)
Definition u42 := ordsucc u41
Theorem aacd7.. : nat_p u42 (proof)
Definition u43 := ordsucc u42
Theorem c4565.. : nat_p u43 (proof)
Definition u44 := ordsucc u43
Theorem 28e92.. : nat_p u44 (proof)
Definition u45 := ordsucc u44
Theorem 3c299.. : nat_p u45 (proof)
Definition u46 := ordsucc u45
Theorem de546.. : nat_p u46 (proof)
Definition u47 := ordsucc u46
Theorem 470e1.. : nat_p u47 (proof)
Definition u48 := ordsucc u47
Theorem 12596.. : nat_p u48 (proof)
Definition u49 := ordsucc u48
Theorem ea244.. : nat_p u49 (proof)
Definition u50 := ordsucc u49
Theorem d7080.. : nat_p u50 (proof)
Definition u51 := ordsucc u50
Theorem 81538.. : nat_p u51 (proof)
Definition u52 := ordsucc u51
Theorem 95d3a.. : nat_p u52 (proof)
Definition u53 := ordsucc u52
Theorem 3c6e6.. : nat_p u53 (proof)
Definition u54 := ordsucc u53
Theorem b9629.. : nat_p u54 (proof)
Definition u55 := ordsucc u54
Theorem 008c1.. : nat_p u55 (proof)
Definition u56 := ordsucc u55
Theorem 59b49.. : nat_p u56 (proof)
Definition u57 := ordsucc u56
Theorem aa500.. : nat_p u57 (proof)
Definition u58 := ordsucc u57
Theorem 74d52.. : nat_p u58 (proof)
Definition u59 := ordsucc u58
Theorem 417f8.. : nat_p u59 (proof)
Definition u60 := ordsucc u59
Theorem 563e5.. : nat_p u60 (proof)
Definition u61 := ordsucc u60
Theorem 71f8e.. : nat_p u61 (proof)
Definition u62 := ordsucc u61
Theorem 15f7b.. : nat_p u62 (proof)
Definition u63 := ordsucc u62
Theorem afba1.. : nat_p u63 (proof)
Definition u64 := ordsucc u63
Theorem 5a366.. : nat_p u64 (proof)
Param add_nat^add_nat : ι → ι → ι
Known add_nat_SR^add_nat_SR : ∀ x0 x1 . nat_p x1 ⟶ add_nat x0 (ordsucc x1) = ordsucc (add_nat x0 x1)
Known nat_4^nat_4 : nat_p 4
Known nat_3^nat_3 : nat_p 3
Known nat_2^nat_2 : nat_p 2
Known nat_1^nat_1 : nat_p 1
Known nat_0^nat_0 : nat_p 0
Known add_nat_0R^add_nat_0R : ∀ x0 . add_nat x0 0 = x0
Theorem 35651.. : add_nat u13 u5 = u18 (proof)
Known nat_5^nat_5 : nat_p 5
Theorem 37308.. : add_nat u19 u6 = u25 (proof)
Known nat_6^nat_6 : nat_p 6
Theorem 4c9e0.. : add_nat u26 u7 = u33 (proof)
Known nat_7^nat_7 : nat_p 7
Theorem 7e9d6.. : add_nat u34 u8 = u42 (proof)
Known nat_12^nat_12 : nat_p 12
Known nat_11^nat_11 : nat_p 11
Known nat_10^nat_10 : nat_p 10
Known nat_9^nat_9 : nat_p 9
Known nat_8^nat_8 : nat_p 8
Theorem a2eda.. : add_nat u51 u13 = u64 (proof)
Definition Subq^Subq := λ x0 x1 . ∀ x2 . x2 ∈ x0 ⟶ x2 ∈ x1
Param exp_nat^exp_nat : ι → ι → ι
Param mul_nat^mul_nat : ι → ι → ι
Known caaf4..^exp_nat_S : ∀ x0 x1 . nat_p x1 ⟶ exp_nat x0 (ordsucc x1) = mul_nat x0 (exp_nat x0 x1)
Known 337ce.. : exp_nat u2 u6 = u64
Known 6cce6.. : ∀ x0 . nat_p x0 ⟶ mul_nat u2 x0 = add_nat x0 x0
Known Subq_tra^Subq_tra : ∀ x0 x1 x2 . x0 ⊆ x1 ⟶ x1 ⊆ x2 ⟶ x0 ⊆ x2
Known 4d87b.. : ∀ x0 x1 . nat_p x1 ⟶ x0 ⊆ add_nat x0 x1
Known nat_14^nat_14 : nat_p 14
Known nat_13^nat_13 : nat_p 13
Known add_nat_SL^add_nat_SL : ∀ x0 . nat_p x0 ⟶ ∀ x1 . nat_p x1 ⟶ add_nat (ordsucc x0) x1 = ordsucc (add_nat x0 x1)
Known add_nat_p^add_nat_p : ∀ x0 . nat_p x0 ⟶ ∀ x1 . nat_p x1 ⟶ nat_p (add_nat x0 x1)
Known add_nat_com^add_nat_com : ∀ x0 . nat_p x0 ⟶ ∀ x1 . nat_p x1 ⟶ add_nat x0 x1 = add_nat x1 x0
Known add_nat_asso^add_nat_asso : ∀ x0 . nat_p x0 ⟶ ∀ x1 . nat_p x1 ⟶ ∀ x2 . nat_p x2 ⟶ add_nat (add_nat x0 x1) x2 = add_nat x0 (add_nat x1 x2)
Known Subq_ref^Subq_ref : ∀ x0 . x0 ⊆ x0
Theorem 9db25.. : add_nat u51 u63 ⊆ exp_nat u2 u7 (proof)
Known nat_ind^nat_ind : ∀ x0 : ι → ο . x0 0 ⟶ (∀ x1 . nat_p x1 ⟶ x0 x1 ⟶ x0 (ordsucc x1)) ⟶ ∀ x1 . nat_p x1 ⟶ x0 x1
Definition and^and := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x1 ⟶ x2) ⟶ x2
Definition TransSet^TransSet := λ x0 . ∀ x1 . x1 ∈ x0 ⟶ x1 ⊆ x0
Definition ordinal^ordinal := λ x0 . and (TransSet x0) (∀ x1 . x1 ∈ x0 ⟶ TransSet x1)
Known nat_ordsucc_in_ordsucc^{nat_ordsucc_in_ordsucc} : ∀ x0 . nat_p x0 ⟶ ∀ x1 . x1 ∈ x0 ⟶ ordsucc x1 ∈ ordsucc x0
Known ordinal_ordsucc^{ordinal_ordsucc} : ∀ x0 . ordinal x0 ⟶ ordinal (ordsucc x0)
Known nat_p_ordinal^{nat_p_ordinal} : ∀ x0 . nat_p x0 ⟶ ordinal x0
Theorem 9cc32.. : ∀ x0 . nat_p x0 ⟶ ∀ x1 . nat_p x1 ⟶ ∀ x2 . nat_p x2 ⟶ x1 ∈ x2 ⟶ add_nat x1 x0 ∈ add_nat x2 x0 (proof)
Definition or^or := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x2) ⟶ (x1 ⟶ x2) ⟶ x2
Known ordinal_In_Or_Subq^{ordinal_In_Or_Subq} : ∀ x0 x1 . ordinal x0 ⟶ ordinal x1 ⟶ or (x0 ∈ x1) (x1 ⊆ x0)
Known set_ext^set_ext : ∀ x0 x1 . x0 ⊆ x1 ⟶ x1 ⊆ x0 ⟶ x0 = x1
Theorem 1fe5e.. : ∀ x0 x1 x2 . nat_p x0 ⟶ nat_p x1 ⟶ nat_p x2 ⟶ x0 ⊆ x1 ⟶ add_nat x0 x2 ⊆ add_nat x1 x2 (proof)
Theorem 66af2.. : ∀ x0 x1 x2 x3 . nat_p x0 ⟶ nat_p x1 ⟶ nat_p x2 ⟶ nat_p x3 ⟶ x0 ⊆ x2 ⟶ x1 ⊆ x3 ⟶ add_nat x0 x1 ⊆ add_nat x2 x3 (proof)
Param TwoRamseyProp^{TwoRamseyProp} : ι → ι → ι → ο
Param atleastp^atleastp : ι → ι → ο
Known 46dcf.. : ∀ x0 x1 x2 x3 . atleastp x2 x3 ⟶ TwoRamseyProp x0 x1 x2 ⟶ TwoRamseyProp x0 x1 x3
Known 24234.. : nat_p u26
Known e06fe.. : nat_p u27
Known 183e4.. : nat_p u34
Known ffdd1.. : nat_p u33
Known 1f846.. : nat_p u32
Known 74918.. : nat_p u31
Known bf663.. : add_nat u31 u27 = u58
Known atleastp_tra^atleastp_tra : ∀ x0 x1 x2 . atleastp x0 x1 ⟶ atleastp x1 x2 ⟶ atleastp x0 x2
Known Subq_atleastp^{Subq_atleastp} : ∀ x0 x1 . x0 ⊆ x1 ⟶ atleastp x0 x1
Param equip^equip : ι → ι → ο
Known equip_atleastp^{equip_atleastp} : ∀ x0 x1 . equip x0 x1 ⟶ atleastp x0 x1
Known equip_sym^equip_sym : ∀ x0 x1 . equip x0 x1 ⟶ equip x1 x0
Known 293d3.. : ∀ x0 . nat_p x0 ⟶ equip (prim4 x0) (exp_nat 2 x0)
Known 164da..^{TwoRamseyProp_bd} : ∀ x0 x1 x2 x3 . nat_p x2 ⟶ nat_p x3 ⟶ TwoRamseyProp (ordsucc x0) x1 (ordsucc x2) ⟶ TwoRamseyProp x0 (ordsucc x1) (ordsucc x3) ⟶ TwoRamseyProp (ordsucc x0) (ordsucc x1) (ordsucc (ordsucc (add_nat x2 x3)))
Known f0d6f..^{TwoRamseyProp_2} : ∀ x0 . TwoRamseyProp 2 x0 x0
Known d9e2e.. : nat_p u19
Known 20c1f.. : add_nat u31 u19 = u50
Known TwoRamseyProp_u4_u5_u32 : TwoRamseyProp u4 u5 u32
Known TwoRamseyProp_3_5_14^{TwoRamseyProp_3_5_14} : TwoRamseyProp 3 5 14
Theorem TwoRamseyProp_4_8_Power_7^{TwoRamseyProp_4_8_Power_7} : TwoRamseyProp 4 8 (prim4 7) (proof)
Known 4f402..^exp_nat_p : ∀ x0 . nat_p x0 ⟶ ∀ x1 . nat_p x1 ⟶ nat_p (exp_nat x0 x1)
Known ordsuccI1^ordsuccI1 : ∀ x0 . x0 ⊆ ordsucc x0
Known ordsuccI2^ordsuccI2 : ∀ x0 . x0 ∈ ordsucc x0
Known Subq_Empty^Subq_Empty : ∀ x0 . 0 ⊆ x0
Theorem TwoRamseyProp_4_9_Power_8^{TwoRamseyProp_4_9_Power_8} : TwoRamseyProp 4 9 (prim4 8) (proof)

Proofgold Address