Search for blocks/addresses/...
Proofgold Asset
asset id
369cb9bdae96103555c04c2b5fce2aefe96834c487b234cdbd0903549d922553
asset hash
a8fff31c211267cc0dd733de13e82bc1ab853e53f017269620cfa4b03ed7aaff
bday / block
36396
tx
575bc..
preasset
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)