Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: ordinal x0.
Let x1 of type ι be given.
Assume H1: 80242.. x1.
Assume H2: prim1 (e4431.. x1) (4ae4a.. x0).
Claim L3: 80242.. (f4dc0.. x1)
Apply unknownprop_8fbd0c2b48e78882e15936a0ad5f4a3c5af2cb37d9320d8cb210a91462e202ca with x1.
The subproof is completed by applying H1.
Claim L4: prim1 (e4431.. (f4dc0.. x1)) (4ae4a.. x0)
Apply unknownprop_9cdeca2a60d0177233427129e29ed2aec16e770191654a999da75532b00612a1 with x1, λ x2 x3 . prim1 x3 (4ae4a.. x0) leaving 2 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
Apply unknownprop_3a727fa768d5525d8195bdc93993ff4ea68fc9d53a8aef656546df8c698dedd5 with x1, λ x2 x3 . fe4bb.. (f4dc0.. x0) x2 leaving 2 subgoals.
The subproof is completed by applying H1.
Apply unknownprop_c83790dfcfb4e8ffee3425d347e76400181b6c85318c783704314a7d55693d45 with f4dc0.. x1, x0 leaving 3 subgoals.
The subproof is completed by applying L3.
Apply unknownprop_30912f2cca40a10142321c491284d8399f9fb6058ea49ef0a3ac5fa1be4efa52 with x0.
The subproof is completed by applying H0.
Apply unknownprop_a01a97b657898ff9d288e2af990470253bea0ca012cb491bf0a3063b2cc95ddb with x0, f4dc0.. x1 leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying L3.
The subproof is completed by applying L4.