sfintfinlem1 - New Foundations Explorer

	New Foundations Explorer		< Previous Next > Nearby theorems
Mirrors > Home > NFE Home > Th. List > sfintfinlem1		Unicode version

Theorem sfintfinlem1 4531

Description: Lemma for sfintfin 4532. Set up induction stratification. (Contributed by SF, 31-Jan-2015.)

**Assertion**
Ref	Expression
sfintfinlem1	S_fin S_fin T_fin T_fin

Distinct variable group:

Proof of Theorem sfintfinlem1 Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		vex 2862	. . . . 5
2	1	eluni1 4173	. . . 4 ⋃₁ ∼ _k SI_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c_k₁ 1_c_k₁ 1_c_k1_c ∼ _k SI_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c_k₁ 1_c_k₁ 1_c_k1_c
3		snex 4111	. . . . . . . 8
4	3	elimak 4259	. . . . . . 7 _k SI_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c_k₁ 1_c_k₁ 1_c_k1_c 1_c _k SI_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c_k₁ 1_c_k₁ 1_c
5		el1c 4139	. . . . . . . . . . 11 1_c
6	5	anbi1i 676	. . . . . . . . . 10 1_c $/\$ _k SI_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c_k₁ 1_c_k₁ 1_c $/\$ _k SI_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c_k₁ 1_c_k₁ 1_c
7		19.41v 1901	. . . . . . . . . 10 $/\$ _k SI_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c_k₁ 1_c_k₁ 1_c $/\$ _k SI_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c_k₁ 1_c_k₁ 1_c
8	6, 7	bitr4i 243	. . . . . . . . 9 1_c $/\$ _k SI_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c_k₁ 1_c_k₁ 1_c $/\$ _k SI_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c_k₁ 1_c_k₁ 1_c
9	8	exbii 1582	. . . . . . . 8 1_c $/\$ _k SI_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c_k₁ 1_c_k₁ 1_c $/\$ _k SI_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c_k₁ 1_c_k₁ 1_c
10		df-rex 2620	. . . . . . . 8 1_c _k SI_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c_k₁ 1_c_k₁ 1_c 1_c $/\$ _k SI_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c_k₁ 1_c_k₁ 1_c
11		excom 1741	. . . . . . . 8 $/\$ _k SI_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c_k₁ 1_c_k₁ 1_c $/\$ _k SI_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c_k₁ 1_c_k₁ 1_c
12	9, 10, 11	3bitr4i 268	. . . . . . 7 1_c _k SI_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c_k₁ 1_c_k₁ 1_c $/\$ _k SI_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c_k₁ 1_c_k₁ 1_c
13		snex 4111	. . . . . . . . . 10
14		opkeq1 4059	. . . . . . . . . . 11
15	14	eleq1d 2419	. . . . . . . . . 10 _k SI_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c_k₁ 1_c_k₁ 1_c _k SI_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c_k₁ 1_c_k₁ 1_c
16	13, 15	ceqsexv 2894	. . . . . . . . 9 $/\$ _k SI_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c_k₁ 1_c_k₁ 1_c _k SI_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c_k₁ 1_c_k₁ 1_c
17	13, 3	opkelcnvk 4250	. . . . . . . . 9 _k SI_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c_k₁ 1_c_k₁ 1_c SI_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c_k₁ 1_c_k₁ 1_c
18		eldif 3221	. . . . . . . . . 10 SI_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c_k₁ 1_c_k₁ 1_c SI_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c $/\$ Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c_k₁ 1_c_k₁ 1_c
19		vex 2862	. . . . . . . . . . . . 13
20	1, 19	opksnelsik 4265	. . . . . . . . . . . 12 SI_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c
21	1, 19	srelk 4524	. . . . . . . . . . . 12 Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c S_fin
22	20, 21	bitri 240	. . . . . . . . . . 11 SI_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c S_fin
23		opkex 4113	. . . . . . . . . . . . . . 15
24	23	elimak 4259	. . . . . . . . . . . . . 14 Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c_k₁ 1_c_k₁ 1_c ₁ 1_c Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c_k₁ 1_c
25		df-rex 2620	. . . . . . . . . . . . . 14 ₁ 1_c Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c_k₁ 1_c ₁ 1_c $/\$ Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c_k₁ 1_c
26		elpw11c 4147	. . . . . . . . . . . . . . . . . 18 ₁ 1_c
27	26	anbi1i 676	. . . . . . . . . . . . . . . . 17 ₁ 1_c $/\$ Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c_k₁ 1_c $/\$ Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c_k₁ 1_c
28		19.41v 1901	. . . . . . . . . . . . . . . . 17 $/\$ Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c_k₁ 1_c $/\$ Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c_k₁ 1_c
29	27, 28	bitr4i 243	. . . . . . . . . . . . . . . 16 ₁ 1_c $/\$ Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c_k₁ 1_c $/\$ Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c_k₁ 1_c
30	29	exbii 1582	. . . . . . . . . . . . . . 15 ₁ 1_c $/\$ Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c_k₁ 1_c $/\$ Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c_k₁ 1_c
31		excom 1741	. . . . . . . . . . . . . . 15 $/\$ Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c_k₁ 1_c $/\$ Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c_k₁ 1_c
32	30, 31	bitr4i 243	. . . . . . . . . . . . . 14 ₁ 1_c $/\$ Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Ins2_k _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Ins3_k Nn _k Nn Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins3_k SI_k ∼ Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c_k₁ 1_c $/\$ Ins2_k _k _k