Search for blocks/addresses/...
Proofgold Proof
pf
Apply ordinal_ind with
λ x0 .
∀ x1 .
prim1
x1
(
56ded..
x0
)
⟶
Subq
(
e4431..
(
f4dc0..
x1
)
)
(
e4431..
x1
)
.
Let x0 of type
ι
be given.
Assume H0:
ordinal
x0
.
Apply H0 with
(
∀ x1 .
prim1
x1
x0
⟶
∀ x2 .
prim1
x2
(
56ded..
x1
)
⟶
Subq
(
e4431..
(
f4dc0..
x2
)
)
(
e4431..
x2
)
)
⟶
∀ x1 .
prim1
x1
(
56ded..
x0
)
⟶
Subq
(
e4431..
(
f4dc0..
x1
)
)
(
e4431..
x1
)
.
Assume H1:
TransSet
x0
.
Assume H2:
∀ x1 .
prim1
x1
x0
⟶
TransSet
x1
.
Assume H3:
∀ x1 .
prim1
x1
x0
⟶
∀ x2 .
prim1
x2
(
56ded..
x1
)
⟶
Subq
(
e4431..
(
f4dc0..
x2
)
)
(
e4431..
x2
)
.
Let x1 of type
ι
be given.
Assume H4:
prim1
x1
(
56ded..
x0
)
.
Apply unknownprop_cd21c13b2c3f5b1a3b98367fcb2ef0b03b319d8c325362ea48d721c1e2e4842f with
x0
,
x1
,
Subq
(
e4431..
(
f4dc0..
x1
)
)
(
e4431..
x1
)
leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H4.
Assume H5:
prim1
(
e4431..
x1
)
x0
.
Assume H6:
ordinal
(
e4431..
x1
)
.
Assume H7:
80242..
x1
.
Assume H8:
1beb9..
(
e4431..
x1
)
x1
.
Claim L9:
...
...
Apply unknownprop_cb0c4ac573f21d515ac1c4f8e66909b50826695f34b524950ade1bb9cca6aa7b with
x1
,
λ x2 x3 .
Subq
(
e4431..
x3
)
(
e4431..
x1
)
leaving 2 subgoals.
The subproof is completed by applying H7.
Apply unknownprop_b01da77c5200afb1f524e6033a58358c3303b7f4989ae9962b195b5bb398525b with
94f9e..
(
5246e..
x1
)
(
λ x2 .
f4dc0..
x2
)
,
94f9e..
(
23e07..
x1
)
(
λ x2 .
f4dc0..
x2
)
,
Subq
(
e4431..
(
02a50..
(
94f9e..
(
5246e..
x1
)
(
λ x2 .
f4dc0..
x2
)
)
(
94f9e..
(
23e07..
x1
)
(
λ x2 .
f4dc0..
x2
)
)
)
)
(
e4431..
x1
)
leaving 2 subgoals.
The subproof is completed by applying L9.
Assume H10:
80242..
(
02a50..
(
94f9e..
(
5246e..
x1
)
(
λ x2 .
f4dc0..
x2
)
)
(
94f9e..
(
23e07..
x1
)
(
λ x2 .
f4dc0..
x2
)
)
)
.
Assume H11:
prim1
(
e4431..
(
02a50..
(
94f9e..
(
5246e..
x1
)
(
λ x2 .
f4dc0..
x2
)
)
(
94f9e..
(
23e07..
x1
)
(
λ x2 .
f4dc0..
x2
)
)
)
)
(
4ae4a..
(
0ac37..
(
a842e..
(
94f9e..
(
5246e..
x1
)
(
λ x2 .
f4dc0..
x2
)
)
(
λ x2 .
4ae4a..
(
e4431..
x2
)
)
)
(
a842e..
(
94f9e..
(
23e07..
x1
)
(
λ x2 .
f4dc0..
x2
)
)
(
λ x2 .
4ae4a..
(
e4431..
x2
)
)
)
)
)
.
Assume H12:
∀ x2 .
prim1
x2
(
94f9e..
(
5246e..
x1
)
f4dc0..
)
⟶
099f3..
x2
(
02a50..
(
94f9e..
(
5246e..
x1
)
f4dc0..
)
(
94f9e..
(
23e07..
x1
)
f4dc0..
)
)
.
Assume H13:
∀ x2 .
prim1
x2
(
94f9e..
(
23e07..
x1
)
f4dc0..
)
⟶
099f3..
(
02a50..
(
94f9e..
(
5246e..
x1
)
f4dc0..
)
(
94f9e..
(
23e07..
x1
)
f4dc0..
)
)
x2
.
Assume H14:
∀ x2 .
...
⟶
...
⟶
...
⟶
and
(
Subq
(
e4431..
(
02a50..
(
94f9e..
(
5246e..
x1
)
f4dc0..
)
(
94f9e..
(
23e07..
x1
)
f4dc0..
)
)
)
(
e4431..
x2
)
)
(
SNoEq_
(
e4431..
(
02a50..
(
94f9e..
(
5246e..
x1
)
f4dc0..
)
(
94f9e..
(
23e07..
x1
)
f4dc0..
)
)
)
(
02a50..
(
94f9e..
(
5246e..
x1
)
...
)
...
)
...
)
.
...
■