| pf |
|---|
Claim L0: ∀ x0 . x0 ∈ 6 ⟶ (λ x1 . ap (lam 6 (λ x2 . If_i (x2 = 0) 1 (If_i (x2 = 1) 0 (If_i (x2 = 2) 0 (If_i (x2 = 3) 1 (If_i (x2 = 4) 0 1)))))) x1) x0 ∈ 2Let x0 of type ι be given.
Assume H0: x0 ∈ 6.
Apply cases_6 with x0, λ x1 . (λ x2 . ap (lam 6 (λ x3 . If_i (x3 = 0) 1 (If_i (x3 = 1) 0 (If_i (x3 = 2) 0 (If_i (x3 = 3) 1 (If_i (x3 = 4) 0 1)))))) x2) x1 ∈ 2 leaving 7 subgoals.
The subproof is completed by applying H0.
Apply tuple_6_0_eq with 1, 0, 0, 1, 0, 1, λ x1 x2 . x2 ∈ 2.
The subproof is completed by applying In_1_2.
Apply tuple_6_1_eq with 1, 0, 0, 1, 0, 1, λ x1 x2 . x2 ∈ 2.
The subproof is completed by applying In_0_2.
Apply tuple_6_2_eq with 1, 0, 0, 1, 0, 1, λ x1 x2 . x2 ∈ 2.
The subproof is completed by applying In_0_2.
Apply tuple_6_3_eq with 1, 0, 0, 1, 0, 1, λ x1 x2 . x2 ∈ 2.
The subproof is completed by applying In_1_2.
Apply tuple_6_4_eq with 1, 0, 0, 1, 0, 1, λ x1 x2 . x2 ∈ 2.
The subproof is completed by applying In_0_2.
Apply tuple_6_5_eq with 1, 0, 0, 1, 0, 1, λ x1 x2 . x2 ∈ 2.
The subproof is completed by applying In_1_2.
Apply nat_In_atleastp with exp_nat 2 6, 41 leaving 2 subgoals.
Apply unknownprop_1b73e01bc234ba0e318bc9baf16604d4f0fc12bea57885439d70438de4eb7174 with 2, 6 leaving 2 subgoals.
The subproof is completed by applying nat_2.
The subproof is completed by applying nat_6.
Apply unknownprop_1b79dfbb43b0cc3437aae6976d9ab14a8460c88de672bd4d288d42598976082b with λ x0 x1 . x0 ∈ exp_nat 2 6.
Apply unknownprop_c741761a4cfde6107df9be6f245ef1dfd65e8b515dba3ea0060e6a63b5817580 with 6, λ x0 . ap (lam 6 (λ x1 . If_i (x1 = 0) 1 (If_i (x1 = 1) 0 (If_i (x1 = 2) 0 (If_i (x1 = 3) 1 (If_i (x1 = 4) 0 1)))))) x0 leaving 2 subgoals.
The subproof is completed by applying nat_6.
The subproof is completed by applying L0.
■ |
|