Proofgold Signed Transaction

Import Signature 9b853..
Param 7736c..^Inj1 : ι → ι
Param 7d54b..^Inj0 : ι → ι
Param aa7bb..^{combine_funcs} : ι → ι → (ι → ι) → (ι → ι) → ι → ι
Known a0730..^{combine_funcs_eq1} : ∀ x0 x1 . ∀ x2 x3 : ι → ι . ∀ x4 . combine_funcs x0 x1 x2 x3 (Inj0 x4) = x2 x4
Known 39338..^{combine_funcs_eq2} : ∀ x0 x1 . ∀ x2 x3 : ι → ι . ∀ x4 . combine_funcs x0 x1 x2 x3 (Inj1 x4) = x3 x4
Param 5b7e0..^setsum : ι → ι → ι
Known 246ac..^Inj0_setsum : ∀ x0 x1 x2 . x2 ∈ x0 ⟶ Inj0 x2 ∈ setsum x0 x1
Known 2b4f9..^Inj1_setsum : ∀ x0 x1 x2 . x2 ∈ x1 ⟶ Inj1 x2 ∈ setsum x0 x1
Known a3640..^{setsum_Inj_inv} : ∀ x0 x1 x2 . x2 ∈ setsum x0 x1 ⟶ or (∃ x3 . and (x3 ∈ x0) (x2 = Inj0 x3)) (∃ x3 . and (x3 ∈ x1) (x2 = Inj1 x3))
Param d64bc..^Sigma : ι → (ι → ι) → ι
Def 107b6..^setprod : ι → ι → ι := λ x0 x1 . lam x0 (λ x2 . x1)
Param a4d82..^ap : ι → ι → ι
Param a7b1b..^Pi : ι → (ι → ι) → ι
Def 021ae..^setexp : ι → ι → ι := λ x0 x1 . Pi x1 (λ x2 . x0)
Known 9bd10..^Pi_eta : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2 ∈ Pi x0 x1 ⟶ lam x0 (ap x2) = x2
Known de381..^{tuple_2_Sigma} : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x1 x2 ⟶ lam 2 (λ x4 . If_i (x4 = 0) x2 x3) ∈ lam x0 x1
Known 1f9d7..^{tuple_2_setprod} : ∀ x0 x1 x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x1 ⟶ lam 2 (λ x4 . If_i (x4 = 0) x2 x3) ∈ setprod x0 x1
Known d965e..^{tuple_Sigma_eta} : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2 ∈ lam x0 x1 ⟶ lam 2 (λ x4 . If_i (x4 = 0) (ap x2 0) (ap x2 1)) = x2
Known ad903..^tuple_2_0_eq : ∀ x0 x1 . ap (lam 2 (λ x3 . If_i (x3 = 0) x0 x1)) 0 = x0
Known 2c0ad..^tuple_2_1_eq : ∀ x0 x1 . ap (lam 2 (λ x3 . If_i (x3 = 0) x0 x1)) 1 = x1
Known 0a4f5..^tuple_3_0_eq : ∀ x0 x1 x2 . ap (lam 3 (λ x4 . If_i (x4 = 0) x0 (If_i (x4 = 1) x1 x2))) 0 = x0
Known 14ea6..^tuple_3_1_eq : ∀ x0 x1 x2 . ap (lam 3 (λ x4 . If_i (x4 = 0) x0 (If_i (x4 = 1) x1 x2))) 1 = x1
Known f69c0..^tuple_3_2_eq : ∀ x0 x1 x2 . ap (lam 3 (λ x4 . If_i (x4 = 0) x0 (If_i (x4 = 1) x1 x2))) 2 = x2
Known fe562..^tuple_4_0_eq : ∀ x0 x1 x2 x3 . ap (lam 4 (λ x5 . If_i (x5 = 0) x0 (If_i (x5 = 1) x1 (If_i (x5 = 2) x2 x3)))) 0 = x0
Known bf73b..^tuple_4_1_eq : ∀ x0 x1 x2 x3 . ap (lam 4 (λ x5 . If_i (x5 = 0) x0 (If_i (x5 = 1) x1 (If_i (x5 = 2) x2 x3)))) 1 = x1
Known 7d442..^tuple_4_2_eq : ∀ x0 x1 x2 x3 . ap (lam 4 (λ x5 . If_i (x5 = 0) x0 (If_i (x5 = 1) x1 (If_i (x5 = 2) x2 x3)))) 2 = x2
Known 1a82d..^tuple_4_3_eq : ∀ x0 x1 x2 x3 . ap (lam 4 (λ x5 . If_i (x5 = 0) x0 (If_i (x5 = 1) x1 (If_i (x5 = 2) x2 x3)))) 3 = x3
Known 2eb5d..^tuple_5_0_eq : ∀ x0 x1 x2 x3 x4 . ap (lam 5 (λ x6 . If_i (x6 = 0) x0 (If_i (x6 = 1) x1 (If_i (x6 = 2) x2 (If_i (x6 = 3) x3 x4))))) 0 = x0
Known 49b93..^tuple_5_1_eq : ∀ x0 x1 x2 x3 x4 . ap (lam 5 (λ x6 . If_i (x6 = 0) x0 (If_i (x6 = 1) x1 (If_i (x6 = 2) x2 (If_i (x6 = 3) x3 x4))))) 1 = x1
Known 3bb23..^tuple_5_2_eq : ∀ x0 x1 x2 x3 x4 . ap (lam 5 (λ x6 . If_i (x6 = 0) x0 (If_i (x6 = 1) x1 (If_i (x6 = 2) x2 (If_i (x6 = 3) x3 x4))))) 2 = x2
Known 52772..^tuple_5_3_eq : ∀ x0 x1 x2 x3 x4 . ap (lam 5 (λ x6 . If_i (x6 = 0) x0 (If_i (x6 = 1) x1 (If_i (x6 = 2) x2 (If_i (x6 = 3) x3 x4))))) 3 = x3
Known 39fb6..^tuple_5_4_eq : ∀ x0 x1 x2 x3 x4 . ap (lam 5 (λ x6 . If_i (x6 = 0) x0 (If_i (x6 = 1) x1 (If_i (x6 = 2) x2 (If_i (x6 = 3) x3 x4))))) 4 = x4
Known b5182..^beta : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2 ∈ x0 ⟶ ap (lam x0 x1) x2 = x1 x2
Known 15b71..^encode_u_ext : ∀ x0 . ∀ x1 x2 : ι → ι . (∀ x3 . x3 ∈ x0 ⟶ x1 x3 = x2 x3) ⟶ lam x0 x1 = lam x0 x2
Param 3c7a5..^pack_u : ι → (ι → ι) → ι
Param df064..^struct_u : ι → ο
Known 7eff9..^pack_u_0_eq2 : ∀ x0 . ∀ x1 : ι → ι . x0 = ap (pack_u x0 x1) 0
Known 9556d..^{pack_struct_u_I} : ∀ x0 . ∀ x1 : ι → ι . (∀ x2 . x2 ∈ x0 ⟶ x1 x2 ∈ x0) ⟶ struct_u (pack_u x0 x1)
Param 9b53a..^unpack_u_i : ι → (ι → (ι → ι) → ι) → ι
Known 133f4..^{unpack_u_i_eq} : ∀ x0 : ι → (ι → ι) → ι . ∀ x1 . ∀ x2 : ι → ι . (∀ x3 : ι → ι . (∀ x4 . x4 ∈ x1 ⟶ x2 x4 = x3 x4) ⟶ x0 x1 x3 = x0 x1 x2) ⟶ unpack_u_i (pack_u x1 x2) x0 = x0 x1 x2
Param 8b490..^unpack_u_o : ι → (ι → (ι → ι) → ο) → ο
Known 3daff..^{unpack_u_o_eq} : ∀ x0 : ι → (ι → ι) → ο . ∀ x1 . ∀ x2 : ι → ι . (∀ x3 : ι → ι . (∀ x4 . x4 ∈ x1 ⟶ x2 x4 = x3 x4) ⟶ x0 x1 x3 = x0 x1 x2) ⟶ unpack_u_o (pack_u x1 x2) x0 = x0 x1 x2