Search for blocks/addresses/...
Proofgold Address
address
PUJyxCSTrDP8x3mTntCa4rP24rk6gQzzb8U
total
0
mg
-
conjpub
-
current assets
a8fff..
/
369cb..
bday:
36396
doc published by
PrCmT..
Known
df_rmo__df_rab__df_v__df_cdeq__df_sbc__df_csb__df_dif__df_un__df_in__df_ss__df_pss__df_symdif__df_nul__df_if__df_pw__df_sn__df_pr__df_tp
:
∀ x0 : ο .
(
(
∀ x1 :
ι → ο
.
∀ x2 :
ι →
ι → ο
.
wb
(
wrmo
x1
x2
)
(
wmo
(
λ x3 .
wa
(
wcel
(
cv
x3
)
(
x2
x3
)
)
(
x1
x3
)
)
)
)
⟶
(
∀ x1 :
ι → ο
.
∀ x2 :
ι →
ι → ο
.
wceq
(
crab
x1
x2
)
(
cab
(
λ x3 .
wa
(
wcel
(
cv
x3
)
(
x2
x3
)
)
(
x1
x3
)
)
)
)
⟶
wceq
cvv
(
cab
(
λ x1 .
wceq
(
cv
x1
)
(
cv
x1
)
)
)
⟶
(
∀ x1 : ο .
∀ x2 x3 .
wb
(
wcdeq
x1
x2
x3
)
(
wceq
(
cv
x2
)
(
cv
x3
)
⟶
x1
)
)
⟶
(
∀ x1 :
ι → ο
.
∀ x2 :
ι →
ι → ο
.
∀ x3 .
wb
(
wsbc
x1
(
x2
x3
)
)
(
wcel
(
x2
x3
)
(
cab
x1
)
)
)
⟶
(
∀ x1 x2 :
ι →
ι → ο
.
∀ x3 .
wceq
(
csb
(
x1
x3
)
x2
)
(
cab
(
λ x4 .
wsbc
(
λ x5 .
wcel
(
cv
x4
)
(
x2
x5
)
)
(
x1
x3
)
)
)
)
⟶
(
∀ x1 x2 :
ι → ο
.
wceq
(
cdif
x1
x2
)
(
cab
(
λ x3 .
wa
(
wcel
(
cv
x3
)
x1
)
(
wn
(
wcel
(
cv
x3
)
x2
)
)
)
)
)
⟶
(
∀ x1 x2 :
ι → ο
.
wceq
(
cun
x1
x2
)
(
cab
(
λ x3 .
wo
(
wcel
(
cv
x3
)
x1
)
(
wcel
(
cv
x3
)
x2
)
)
)
)
⟶
(
∀ x1 x2 :
ι → ο
.
wceq
(
cin
x1
x2
)
(
cab
(
λ x3 .
wa
(
wcel
(
cv
x3
)
x1
)
(
wcel
(
cv
x3
)
x2
)
)
)
)
⟶
(
∀ x1 x2 :
ι → ο
.
wb
(
wss
x1
x2
)
(
wceq
(
cin
x1
x2
)
x1
)
)
⟶
(
∀ x1 x2 :
ι → ο
.
wb
(
wpss
x1
x2
)
(
wa
(
wss
x1
x2
)
(
wne
x1
x2
)
)
)
⟶
(
∀ x1 x2 :
ι → ο
.
wceq
(
csymdif
x1
x2
)
(
cun
(
cdif
x1
x2
)
(
cdif
x2
x1
)
)
)
⟶
wceq
c0
(
cdif
cvv
cvv
)
⟶
(
∀ x1 : ο .
∀ x2 x3 :
ι → ο
.
wceq
(
cif
x1
x2
x3
)
(
cab
(
λ x4 .
wo
(
wa
(
wcel
(
cv
x4
)
x2
)
x1
)
(
wa
(
wcel
(
cv
x4
)
x3
)
(
wn
x1
)
)
)
)
)
⟶
(
∀ x1 :
ι → ο
.
wceq
(
cpw
x1
)
(
cab
(
λ x2 .
wss
(
cv
x2
)
x1
)
)
)
⟶
(
∀ x1 :
ι → ο
.
wceq
(
csn
x1
)
(
cab
(
λ x2 .
wceq
(
cv
x2
)
x1
)
)
)
⟶
(
∀ x1 x2 :
ι → ο
.
wceq
(
cpr
x1
x2
)
(
cun
(
csn
x1
)
(
csn
x2
)
)
)
⟶
(
∀ x1 x2 x3 :
ι → ο
.
wceq
(
ctp
x1
x2
x3
)
(
cun
(
cpr
x1
x2
)
(
csn
x3
)
)
)
⟶
x0
)
⟶
x0
Theorem
df_rmo
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ο
.
wb
(
wrmo
x0
x1
)
(
wmo
(
λ x2 .
wa
(
wcel
(
cv
x2
)
(
x1
x2
)
)
(
x0
x2
)
)
)
(proof)
Theorem
df_rab
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ο
.
wceq
(
crab
x0
x1
)
(
cab
(
λ x2 .
wa
(
wcel
(
cv
x2
)
(
x1
x2
)
)
(
x0
x2
)
)
)
(proof)
Theorem
df_v
:
wceq
cvv
(
cab
(
λ x0 .
wceq
(
cv
x0
)
(
cv
x0
)
)
)
(proof)
Theorem
df_cdeq
:
∀ x0 : ο .
∀ x1 x2 .
wb
(
wcdeq
x0
x1
x2
)
(
wceq
(
cv
x1
)
(
cv
x2
)
⟶
x0
)
(proof)
Theorem
df_sbc
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ο
.
∀ x2 .
wb
(
wsbc
x0
(
x1
x2
)
)
(
wcel
(
x1
x2
)
(
cab
x0
)
)
(proof)
Theorem
df_csb
:
∀ x0 x1 :
ι →
ι → ο
.
∀ x2 .
wceq
(
csb
(
x0
x2
)
x1
)
(
cab
(
λ x3 .
wsbc
(
λ x4 .
wcel
(
cv
x3
)
(
x1
x4
)
)
(
x0
x2
)
)
)
(proof)
Theorem
df_dif
:
∀ x0 x1 :
ι → ο
.
wceq
(
cdif
x0
x1
)
(
cab
(
λ x2 .
wa
(
wcel
(
cv
x2
)
x0
)
(
wn
(
wcel
(
cv
x2
)
x1
)
)
)
)
(proof)
Theorem
df_un
:
∀ x0 x1 :
ι → ο
.
wceq
(
cun
x0
x1
)
(
cab
(
λ x2 .
wo
(
wcel
(
cv
x2
)
x0
)
(
wcel
(
cv
x2
)
x1
)
)
)
(proof)
Theorem
df_in
:
∀ x0 x1 :
ι → ο
.
wceq
(
cin
x0
x1
)
(
cab
(
λ x2 .
wa
(
wcel
(
cv
x2
)
x0
)
(
wcel
(
cv
x2
)
x1
)
)
)
(proof)
Theorem
df_ss
:
∀ x0 x1 :
ι → ο
.
wb
(
wss
x0
x1
)
(
wceq
(
cin
x0
x1
)
x0
)
(proof)
Theorem
df_pss
:
∀ x0 x1 :
ι → ο
.
wb
(
wpss
x0
x1
)
(
wa
(
wss
x0
x1
)
(
wne
x0
x1
)
)
(proof)
Theorem
df_symdif
:
∀ x0 x1 :
ι → ο
.
wceq
(
csymdif
x0
x1
)
(
cun
(
cdif
x0
x1
)
(
cdif
x1
x0
)
)
(proof)
Theorem
df_nul
:
wceq
c0
(
cdif
cvv
cvv
)
(proof)
Theorem
df_if
:
∀ x0 : ο .
∀ x1 x2 :
ι → ο
.
wceq
(
cif
x0
x1
x2
)
(
cab
(
λ x3 .
wo
(
wa
(
wcel
(
cv
x3
)
x1
)
x0
)
(
wa
(
wcel
(
cv
x3
)
x2
)
(
wn
x0
)
)
)
)
(proof)
Theorem
df_pw
:
∀ x0 :
ι → ο
.
wceq
(
cpw
x0
)
(
cab
(
λ x1 .
wss
(
cv
x1
)
x0
)
)
(proof)
Theorem
df_sn
:
∀ x0 :
ι → ο
.
wceq
(
csn
x0
)
(
cab
(
λ x1 .
wceq
(
cv
x1
)
x0
)
)
(proof)
Theorem
df_pr
:
∀ x0 x1 :
ι → ο
.
wceq
(
cpr
x0
x1
)
(
cun
(
csn
x0
)
(
csn
x1
)
)
(proof)
Theorem
df_tp
:
∀ x0 x1 x2 :
ι → ο
.
wceq
(
ctp
x0
x1
x2
)
(
cun
(
cpr
x0
x1
)
(
csn
x2
)
)
(proof)
previous assets