Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι(ιιι) → ιι be given.
Assume H0: ∀ x1 . 80242.. x1∀ x2 x3 : ι → ι → ι . (∀ x4 . prim1 x4 (56ded.. (e4431.. x1))x2 x4 = x3 x4)x0 x1 x2 = x0 x1 x3.
Let x1 of type ι be given.
Assume H1: 80242.. x1.
Claim L2: ∀ x2 . ∀ x3 x4 : ι → ι → ι → ι . ...(λ x5 . λ x6 : ι → ι → ι → ι . If_iii (ordinal x5) (λ x7 . If_ii (prim1 x7 (56ded.. (4ae4a.. x5))) (x0 x7 (λ x8 . x6 (e4431.. x8) x8)) ...) ...) ... ... = ...
...
Apply In_rec_iii_eq with λ x2 . λ x3 : ι → ι → ι → ι . If_iii (ordinal x2) (λ x4 . If_ii (prim1 x4 (56ded.. (4ae4a.. x2))) (x0 x4 (λ x5 . x3 (e4431.. x5) x5)) (Descr_ii (λ x5 : ι → ι . True))) (λ x4 . Descr_ii (λ x5 : ι → ι . True)), e4431.. x1, λ x2 x3 : ι → ι → ι . x3 x1 = x0 x1 (λ x4 . In_rec_iii (λ x5 . λ x6 : ι → ι → ι → ι . If_iii (ordinal x5) (λ x7 . If_ii (prim1 x7 (56ded.. (4ae4a.. x5))) (x0 x7 (λ x8 . x6 (e4431.. x8) x8)) (Descr_ii (λ x8 : ι → ι . True))) (λ x7 . Descr_ii (λ x8 : ι → ι . True))) (e4431.. x4) x4) leaving 2 subgoals.
The subproof is completed by applying L2.
Claim L3: ordinal (e4431.. x1)
Apply unknownprop_afbf697e4489c80654ae2bc4c6605f6f1d2a8b7dcfe3f07863a96592ab5c88f5 with x1.
The subproof is completed by applying H1.
Apply If_iii_1 with ordinal (e4431.. x1), λ x2 . If_ii (prim1 x2 (56ded.. (4ae4a.. (e4431.. x1)))) (x0 x2 (λ x3 . In_rec_iii (λ x4 . λ x5 : ι → ι → ι → ι . If_iii (ordinal x4) (λ x6 . If_ii (prim1 x6 (56ded.. (4ae4a.. x4))) (x0 x6 (λ x7 . x5 (e4431.. x7) x7)) (Descr_ii (λ x7 : ι → ι . True))) (λ x6 . Descr_ii (λ x7 : ι → ι . True))) (e4431.. x3) x3)) (Descr_ii (λ x3 : ι → ι . True)), λ x2 . Descr_ii (λ x3 : ι → ι . True), λ x2 x3 : ι → ι → ι . x3 x1 = x0 x1 (λ x4 . In_rec_iii (λ x5 . λ x6 : ι → ι → ι → ι . If_iii (ordinal x5) (λ x7 . If_ii (prim1 x7 (56ded.. (4ae4a.. x5))) (x0 x7 (λ x8 . x6 (e4431.. x8) x8)) (Descr_ii (λ x8 : ι → ι . True))) (λ x7 . Descr_ii (λ x8 : ι → ι . True))) (e4431.. x4) x4) leaving 2 subgoals.
The subproof is completed by applying L3.
Claim L4: prim1 x1 (56ded.. (4ae4a.. (e4431.. x1)))
Apply unknownprop_55be23921c8e687561ab6e9faf36ed3618fa021f01ef196ba95aa8fcda0b83ee with x1.
The subproof is completed by applying H1.
Apply If_ii_1 with prim1 x1 (56ded.. (4ae4a.. (e4431.. x1))), x0 x1 (λ x2 . In_rec_iii (λ x3 . λ x4 : ι → ι → ι → ι . If_iii (ordinal x3) (λ x5 . If_ii (prim1 x5 (56ded.. (4ae4a.. x3))) (x0 x5 (λ x6 . x4 (e4431.. x6) x6)) (Descr_ii (λ x6 : ι → ι . True))) (λ x5 . Descr_ii (λ x6 : ι → ι . True))) (e4431.. x2) x2), Descr_ii (λ x2 : ι → ι . True).
The subproof is completed by applying L4.