Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: CRing_with_id x0.
Claim L1: ∀ x1 . nat_p x1 ⟶ ∀ x2 . (∀ x3 . x3 ∈ x1 ⟶ ap x2 x3 ∈ K_field_0 x0 x0) ⟶ ∀ x3 . x3 ∈ K_field_0 x0 x0 ⟶ 47209.. x0 x1 x2 x3 ∈ K_field_0 x0 x0
Apply nat_ind with λ x1 . ∀ x2 . (∀ x3 . x3 ∈ x1 ⟶ ap x2 x3 ∈ K_field_0 x0 x0) ⟶ ∀ x3 . x3 ∈ K_field_0 x0 x0 ⟶ 47209.. x0 x1 x2 x3 ∈ K_field_0 x0 x0 leaving 2 subgoals.
Let x1 of type ι be given.
Assume H1: ∀ x2 . x2 ∈ 0 ⟶ ap x1 x2 ∈ K_field_0 x0 x0.
Let x2 of type ι be given.
Assume H2: x2 ∈ K_field_0 x0 x0.
Apply nat_primrec_0 with K_field_3 x0 x0, λ x3 x4 . K_field_1_b x0 x0 (K_field_2_b x0 x0 (ap x1 x3) (4a41c.. x0 x2 x3)) x4, λ x3 x4 . x4 ∈ K_field_0 x0 x0.
Apply unknownprop_367a75c6b8bf5f61e0a46f6b598edb93a655b70e4732923ac22f94c52d814ea1 with x0.
The subproof is completed by applying H0.
Let x1 of type ι be given.
Assume H1: nat_p x1.
Assume H2: ∀ x2 . (∀ x3 . x3 ∈ x1 ⟶ ap x2 x3 ∈ K_field_0 x0 x0) ⟶ ∀ x3 . x3 ∈ K_field_0 x0 x0 ⟶ 47209.. x0 x1 x2 x3 ∈ K_field_0 x0 x0.
Let x2 of type ι be given.
Assume H3: ∀ x3 . x3 ∈ ordsucc x1 ⟶ ap x2 x3 ∈ K_field_0 x0 x0.
Let x3 of type ι be given.
Assume H4: x3 ∈ K_field_0 x0 x0.
Apply nat_primrec_S with K_field_3 x0 x0, λ x4 x5 . K_field_1_b x0 x0 (K_field_2_b x0 x0 (ap x2 x4) (4a41c.. x0 x3 x4)) x5, x1, λ x4 x5 . x5 ∈ K_field_0 x0 x0 leaving 2 subgoals.
The subproof is completed by applying H1.
Apply unknownprop_fd8780fbed61ca272b11706395da54d2d31e56a004ea175904da8ec787a7de9a with x0, K_field_2_b x0 x0 (ap x2 x1) (4a41c.. x0 x3 x1), nat_primrec (K_field_3 x0 x0) (λ x4 x5 . K_field_1_b x0 x0 (K_field_2_b x0 x0 (ap x2 x4) (4a41c.. x0 x3 x4)) x5) x1 leaving 3 subgoals.
The subproof is completed by applying H0.
Apply unknownprop_83ca4313fe8b0637c2e8068a8b92f4bb986f1989193702cbeb0baf134d146d34 with x0, ap x2 x1, 4a41c.. x0 x3 x1 leaving 3 subgoals.
The subproof is completed by applying H0.
Apply H3 with x1.
The subproof is completed by applying ordsuccI2 with x1.
Apply unknownprop_b75e15b7618f186de797a9c3b946547093a25c925a7003e20116b4ad0756b295 with x0, x3, x1 leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H4.
Apply nat_p_omega with x1.
The subproof is completed by applying H1.
Claim L5: ∀ x4 . ... ⟶ ap x2 x4 ∈ K_field_0 x0 ...
...
Apply H2 with x2, x3 leaving 2 subgoals.
The subproof is completed by applying L5.
The subproof is completed by applying H4.
Let x1 of type ι be given.
Assume H2: x1 ∈ omega.
Let x2 of type ι be given.
Assume H3: x2 ∈ setexp (K_field_0 x0 x0) x1.
Apply L1 with x1, x2 leaving 2 subgoals.
Apply omega_nat_p with x1.
The subproof is completed by applying H2.
Let x3 of type ι be given.
Assume H4: x3 ∈ x1.
Apply ap_Pi with x1, λ x4 . K_field_0 x0 x0, x2, x3 leaving 2 subgoals.
The subproof is completed by applying H3.
The subproof is completed by applying H4.
■