Proofgold Signed Transaction

Import Signature a04d9..
Param cfd8e..^nat_p : ι → ο
Known 457a7..^nat_0 : nat_p 0
Known 57e94..^nat_ordsucc : ∀ x0 . nat_p x0 ⟶ nat_p (ordsucc x0)
Known ecdce..^nat_ind : ∀ x0 : ι → ο . x0 0 ⟶ (∀ x1 . nat_p x1 ⟶ x0 x1 ⟶ x0 (ordsucc x1)) ⟶ ∀ x1 . nat_p x1 ⟶ x0 x1
Known 1e160..^{nat_complete_ind} : ∀ x0 : ι → ο . (∀ x1 . nat_p x1 ⟶ (∀ x2 . x2 ∈ x1 ⟶ x0 x2) ⟶ x0 x1) ⟶ ∀ x1 . nat_p x1 ⟶ x0 x1
Known 175e2..^{nat_inv_impred} : ∀ x0 : ι → ο . x0 0 ⟶ (∀ x1 . nat_p x1 ⟶ x0 (ordsucc x1)) ⟶ ∀ x1 . nat_p x1 ⟶ x0 x1
Known 4f416..^nat_inv : ∀ x0 . nat_p x0 ⟶ or (x0 = 0) (∀ x1 : ο . (∀ x2 . and (nat_p x2) (x0 = ordsucc x2) ⟶ x1) ⟶ x1)
Known 03b87..^nat_p_trans : ∀ x0 . nat_p x0 ⟶ ∀ x1 . x1 ∈ x0 ⟶ nat_p x1
Known 672d0..^nat_1 : nat_p 1
Known 9112e..^nat_2 : nat_p 2
Known e5542..^neq_1_2 : 1 = 2 ⟶ ∀ x0 : ο . x0
Known 2949c..^neq_2_1 : 2 = 1 ⟶ ∀ x0 : ο . x0
Known 133bb..^nat_3 : nat_p 3
Known 69ffc..^nat_4 : nat_p 4
Known b84b2..^nat_5 : nat_p 5
Known b4ec6..^nat_6 : nat_p 6
Known 86ad8..^nat_7 : nat_p 7
Known f9312..^nat_8 : nat_p 8
Known 356a4..^nat_9 : nat_p 9
Known cd262..^nat_10 : nat_p 10
Known 60602..^nat_11 : nat_p 11
Known a6dc0..^nat_12 : nat_p 12
Known 74108..^nat_13 : nat_p 13
Known a8824..^nat_16 : nat_p 16
Known a3720..^nat_17 : nat_p 17
Known 9f78a..^In_0_6 : 0 ∈ 6
Known a8f5a..^In_2_6 : 2 ∈ 6
Known 9f463..^In_3_6 : 3 ∈ 6
Known 5d38f..^In_4_6 : 4 ∈ 6
Known 6d1dd..^In_5_6 : 5 ∈ 6
Known 799b0..^neq_3_0 : 3 = 0 ⟶ ∀ x0 : ο . x0
Known 8e4c7..^neq_3_1 : 3 = 1 ⟶ ∀ x0 : ο . x0
Known 46727..^neq_3_2 : 3 = 2 ⟶ ∀ x0 : ο . x0
Known dbfe9..^neq_4_0 : 4 = 0 ⟶ ∀ x0 : ο . x0
Known bbd62..^neq_4_1 : 4 = 1 ⟶ ∀ x0 : ο . x0
Known 0a09e..^neq_4_2 : 4 = 2 ⟶ ∀ x0 : ο . x0
Known 2a569..^neq_4_3 : 4 = 3 ⟶ ∀ x0 : ο . x0
Known 29ce2..^neq_5_0 : 5 = 0 ⟶ ∀ x0 : ο . x0
Known cdb67..^neq_5_1 : 5 = 1 ⟶ ∀ x0 : ο . x0
Known 72066..^neq_5_2 : 5 = 2 ⟶ ∀ x0 : ο . x0
Known c26bb..^neq_5_3 : 5 = 3 ⟶ ∀ x0 : ο . x0
Known 20c3f..^neq_5_4 : 5 = 4 ⟶ ∀ x0 : ο . x0
Known ed34a..^cases_6 : ∀ x0 . x0 ∈ 6 ⟶ ∀ x1 : ι → ο . x1 0 ⟶ x1 1 ⟶ x1 2 ⟶ x1 3 ⟶ x1 4 ⟶ x1 5 ⟶ x1 x0
Param 76c4c..^If_i : ο → ι → ι → ι
Known a9abd..^If_i_0 : ∀ x0 : ο . ∀ x1 x2 . not x0 ⟶ If_i x0 x1 x2 = x2
Known a93c2..^If_i_1 : ∀ x0 : ο . ∀ x1 x2 . x0 ⟶ If_i x0 x1 x2 = x1
Param dc313..^UPair : ι → ι → ι
Known e67fc..^UPairE : ∀ x0 x1 x2 . x0 ∈ UPair x1 x2 ⟶ or (x0 = x1) (x0 = x2)
Known bf364..^UPairI1 : ∀ x0 x1 . x0 ∈ UPair x0 x1
Known a0a5b..^UPairI2 : ∀ x0 x1 . x1 ∈ UPair x0 x1
Param b7dfc..^Sing : ι → ι
Known 2f93b..^SingI : ∀ x0 . x0 ∈ Sing x0
Known 3b0dd..^SingE : ∀ x0 x1 . x1 ∈ Sing x0 ⟶ x1 = x0
Param e1498..^binunion : ι → ι → ι
Known e43c8..^binunionI1 : ∀ x0 x1 x2 . x2 ∈ x0 ⟶ x2 ∈ binunion x0 x1
Known 95953..^binunionI2 : ∀ x0 x1 x2 . x2 ∈ x1 ⟶ x2 ∈ binunion x0 x1
Known 1ceeb..^binunionE : ∀ x0 x1 x2 . x2 ∈ binunion x0 x1 ⟶ or (x2 ∈ x0) (x2 ∈ x1)
Def 5bdda..^SetAdjoin : ι → ι → ι := λ x0 x1 . binunion x0 (Sing x1)
Known bed33..^binunion_com : ∀ x0 x1 . binunion x0 x1 = binunion x1 x0
Known d64da..^{binunion_Subq_min} : ∀ x0 x1 x2 . x0 ⊆ x2 ⟶ x1 ⊆ x2 ⟶ binunion x0 x1 ⊆ x2
Param 24134..^famunion : ι → (ι → ι) → ι
Known e4f49..^famunionI : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 x3 . x2 ∈ x0 ⟶ x3 ∈ x1 x2 ⟶ x3 ∈ famunion x0 x1
Known ede6e..^famunionE : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2 ∈ famunion x0 x1 ⟶ ∀ x3 : ο . (∀ x4 . and (x4 ∈ x0) (x2 ∈ x1 x4) ⟶ x3) ⟶ x3
Known 56202..^{famunionE_impred} : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2 ∈ famunion x0 x1 ⟶ ∀ x3 : ο . (∀ x4 . x4 ∈ x0 ⟶ x2 ∈ x1 x4 ⟶ x3) ⟶ x3
Param 7008e..^Sep : ι → (ι → ο) → ι
Known 147a6..^SepI : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . x2 ∈ x0 ⟶ x1 x2 ⟶ x2 ∈ Sep x0 x1
Known 00899..^SepE : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . x2 ∈ Sep x0 x1 ⟶ and (x2 ∈ x0) (x1 x2)
Known 6399b..^SepE1 : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . x2 ∈ Sep x0 x1 ⟶ x2 ∈ x0
Known 10422..^SepE2 : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . x2 ∈ Sep x0 x1 ⟶ x1 x2
Known c17d4..^Sep_Subq : ∀ x0 . ∀ x1 : ι → ο . Sep x0 x1 ⊆ x0
Param 9bdb5..^ReplSep : ι → (ι → ο) → (ι → ι) → ι
Known aa7b2..^ReplSepI : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 : ι → ι . ∀ x3 . x3 ∈ x0 ⟶ x1 x3 ⟶ x2 x3 ∈ ReplSep x0 x1 x2
Known 063ce..^{ReplSepE_impred} : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 : ι → ι . ∀ x3 . x3 ∈ ReplSep x0 x1 x2 ⟶ ∀ x4 : ο . (∀ x5 . x5 ∈ x0 ⟶ x1 x5 ⟶ x3 = x2 x5 ⟶ x4) ⟶ x4
Param 2c68d..^binintersect : ι → ι → ι
Known 9081a..^{binintersectI} : ∀ x0 x1 x2 . x2 ∈ x0 ⟶ x2 ∈ x1 ⟶ x2 ∈ binintersect x0 x1
Known ca063..^{binintersectE} : ∀ x0 x1 x2 . x2 ∈ binintersect x0 x1 ⟶ and (x2 ∈ x0) (x2 ∈ x1)
Known 51005..^{binintersectE1} : ∀ x0 x1 x2 . x2 ∈ binintersect x0 x1 ⟶ x2 ∈ x0
Known 599de..^{binintersectE2} : ∀ x0 x1 x2 . x2 ∈ binintersect x0 x1 ⟶ x2 ∈ x1
Known ea8a1..^{binintersect_com} : ∀ x0 x1 . binintersect x0 x1 = binintersect x1 x0
Param 913da..^setminus : ι → ι → ι
Known 80db6..^setminusI : ∀ x0 x1 x2 . x2 ∈ x0 ⟶ nIn x2 x1 ⟶ x2 ∈ setminus x0 x1
Known 71763..^setminusE : ∀ x0 x1 x2 . x2 ∈ setminus x0 x1 ⟶ and (x2 ∈ x0) (nIn x2 x1)
Known d74ba..^setminusE1 : ∀ x0 x1 x2 . x2 ∈ setminus x0 x1 ⟶ x2 ∈ x0
Known 36b27..^setminusE2 : ∀ x0 x1 x2 . x2 ∈ setminus x0 x1 ⟶ nIn x2 x1
Known 66f98..^{setminus_Subq} : ∀ x0 x1 . setminus x0 x1 ⊆ x0
Known 7bfd4..^In_irref : ∀ x0 . nIn x0 x0
Known 344f3..^In_no2cycle : ∀ x0 x1 . x0 ∈ x1 ⟶ x1 ∈ x0 ⟶ False
Known 367d8..^ordsuccI1 : ∀ x0 . x0 ⊆ ordsucc x0
Known 2be6b..^ordsuccI2 : ∀ x0 . x0 ∈ ordsucc x0
Known 3849f..^ordsuccE : ∀ x0 x1 . x1 ∈ ordsucc x0 ⟶ or (x1 ∈ x0) (x1 = x0)
Known 346ee..^{neq_ordsucc_0} : ∀ x0 . ordsucc x0 = 0 ⟶ ∀ x1 : ο . x1
Known 4869a..^ordsucc_inj : ∀ x0 x1 . ordsucc x0 = ordsucc x1 ⟶ x0 = x1
Known 32724..^In_1_6 : 1 ∈ 6
Known 251f3..^{nat_0_in_ordsucc} : ∀ x0 . nat_p x0 ⟶ 0 ∈ ordsucc x0
Known 4c2c9..^{nat_ordsucc_in_ordsucc} : ∀ x0 . nat_p x0 ⟶ ∀ x1 . x1 ∈ x0 ⟶ ordsucc x1 ∈ ordsucc x0
Known f9480..^neq_6_0 : 6 = 0 ⟶ ∀ x0 : ο . x0
Known 799bd..^neq_6_1 : 6 = 1 ⟶ ∀ x0 : ο . x0
Known 2865c..^neq_6_2 : 6 = 2 ⟶ ∀ x0 : ο . x0
Known 1ffa2..^neq_6_3 : 6 = 3 ⟶ ∀ x0 : ο . x0
Known b3e48..^neq_6_4 : 6 = 4 ⟶ ∀ x0 : ο . x0
Known f4436..^neq_6_5 : 6 = 5 ⟶ ∀ x0 : ο . x0