From: Ferruccio Guidi Date: Mon, 13 Mar 2017 17:04:14 +0000 (+0000) Subject: - tdeq must imply tsts X-Git-Tag: make_still_working~483 X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=1de84a809c842fbc8a4e0d92b9bc61763c0e6fae - tdeq must imply tsts - notational change for tsts - refactoring --- diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazyeq_4.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazyeq_4.ma index 9e302cf79..ab30a9936 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazyeq_4.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazyeq_4.ma @@ -14,6 +14,6 @@ (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) -notation "hvbox( T1 ≡ [ break term 46 h , term 46 o ] break term 46 T2 )" +notation "hvbox( T1 ≡ [ break term 46 h , break term 46 o ] break term 46 T2 )" non associative with precedence 45 for @{ 'LazyEq $h $o $T1 $T2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/topiso_2.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/topiso_2.ma deleted file mode 100644 index 059b4372b..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/topiso_2.ma +++ /dev/null @@ -1,19 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) - -notation "hvbox( T1 ≂ break term 46 T2 )" - non associative with precedence 45 - for @{ 'TopIso $T1 $T2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/topiso_4.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/topiso_4.ma new file mode 100644 index 000000000..bcb7fa345 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/topiso_4.ma @@ -0,0 +1,19 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) + +notation "hvbox( T1 ⩳ [ break term 46 h , break term 46 o ] break term 46 T2 )" + non associative with precedence 45 + for @{ 'TopIso $h $o $T1 $T2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/syntax/tdeq.ma b/matita/matita/contribs/lambdadelta/basic_2/syntax/tdeq.ma index 6e08f7446..52784b53f 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/syntax/tdeq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/syntax/tdeq.ma @@ -131,7 +131,7 @@ lemma tdeq_sym: ∀h,o. symmetric … (tdeq h o). /2 width=3 by tdeq_sort, tdeq_lref, tdeq_gref, tdeq_pair/ qed-. -lemma tdeq_dec: ∀h,o,T1,T2. Decidable (tdeq h o T1 T2). +lemma tdeq_dec: ∀h,o,T1,T2. Decidable (T1 ≡[h, o] T2). #h #o #T1 elim T1 -T1 [ * #s1 | #I1 #V1 #T1 #IHV #IHT ] * [1,3,5,7: * #s2 |*: #I2 #V2 #T2 ] [ elim (deg_total h o s1) #d1 #H1 elim (deg_total h o s2) #d2 #H2 diff --git a/matita/matita/contribs/lambdadelta/basic_2/syntax/tdeq_tdeq.ma b/matita/matita/contribs/lambdadelta/basic_2/syntax/tdeq_tdeq.ma index af82e7cd7..bdb48def6 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/syntax/tdeq_tdeq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/syntax/tdeq_tdeq.ma @@ -24,7 +24,7 @@ theorem tdeq_trans: ∀h,o. Transitive … (tdeq h o). elim (tdeq_inv_sort1_deg … H … Hs) -s /2 width=3 by tdeq_sort/ | #i1 #i #H <(tdeq_inv_lref1 … H) -H // | #l1 #l #H <(tdeq_inv_gref1 … H) -H // -| #I #V1 #V #T1 #T #_ #_ #IHV #IHT #X #H destruct +| #I #V1 #V #T1 #T #_ #_ #IHV #IHT #X #H elim (tdeq_inv_pair1 … H) -H /3 width=1 by tdeq_pair/ ] qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/syntax/term_simple.ma b/matita/matita/contribs/lambdadelta/basic_2/syntax/term_simple.ma index 50e259544..e6cfdb3c0 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/syntax/term_simple.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/syntax/term_simple.ma @@ -19,7 +19,7 @@ include "basic_2/syntax/term.ma". inductive simple: predicate term ≝ | simple_atom: ∀I. simple (⓪{I}) - | simple_flat: ∀I,V,T. simple (ⓕ{I} V. T) + | simple_flat: ∀I,V,T. simple (ⓕ{I}V.T) . interpretation "simple (term)" 'Simple T = (simple T). @@ -36,7 +36,7 @@ qed-. lemma simple_inv_bind: ∀p,I,V,T. 𝐒⦃ⓑ{p,I} V. T⦄ → ⊥. /2 width=7 by simple_inv_bind_aux/ qed-. -lemma simple_inv_pair: ∀I,V,T. 𝐒⦃②{I}V.T⦄ → ∃J. I = Flat2 J. +lemma simple_inv_pair: ∀I,V,T. 𝐒⦃②{I}V.T⦄ → ∃J. I = Flat2 J. * /2 width=2 by ex_intro/ #p #I #V #T #H elim (simple_inv_bind … H) qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/syntax/tsts.ma b/matita/matita/contribs/lambdadelta/basic_2/syntax/tsts.ma index 281f7fc81..d489fca88 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/syntax/tsts.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/syntax/tsts.ma @@ -12,97 +12,146 @@ (* *) (**************************************************************************) -include "basic_2/notation/relations/topiso_2.ma". -include "basic_2/syntax/term_simple.ma". +include "basic_2/notation/relations/topiso_4.ma". +include "basic_2/syntax/item_sd.ma". +include "basic_2/syntax/term.ma". (* SAME TOP TERM STRUCTURE **************************************************) -inductive tsts: relation term ≝ - | tsts_atom: ∀I. tsts (⓪{I}) (⓪{I}) - | tsts_pair: ∀I,V1,V2,T1,T2. tsts (②{I}V1.T1) (②{I}V2.T2) +(* Basic_2A1: includes: tsts_atom *) +inductive tsts (h) (o): relation term ≝ +| tsts_sort: ∀s1,s2,d. deg h o s1 d → deg h o s2 d → tsts h o (⋆s1) (⋆s2) +| tsts_lref: ∀i. tsts h o (#i) (#i) +| tsts_gref: ∀l. tsts h o (§l) (§l) +| tsts_pair: ∀I,V1,V2,T1,T2. tsts h o (②{I}V1.T1) (②{I}V2.T2) . -interpretation "same top structure (term)" 'TopIso T1 T2 = (tsts T1 T2). +interpretation "same top structure (term)" 'TopIso h o T1 T2 = (tsts h o T1 T2). (* Basic inversion lemmas ***************************************************) -fact tsts_inv_atom1_aux: ∀T1,T2. T1 ≂ T2 → ∀I. T1 = ⓪{I} → T2 = ⓪{I}. -#T1 #T2 * -T1 -T2 // -#J #V1 #V2 #T1 #T2 #I #H destruct +fact tsts_inv_sort1_aux: ∀h,o,X,Y. X ⩳[h, o] Y → ∀s1. X = ⋆s1 → + ∃∃s2,d. deg h o s1 d & deg h o s2 d & Y = ⋆s2. +#h #o #X #Y * -X -Y +[ #s1 #s2 #d #Hs1 #Hs2 #s #H destruct /2 width=5 by ex3_2_intro/ +| #i #s #H destruct +| #l #s #H destruct +| #I #V1 #V2 #T1 #T2 #s #H destruct +] qed-. -(* Basic_1: was: iso_gen_sort iso_gen_lref *) -lemma tsts_inv_atom1: ∀I,T2. ⓪{I} ≂ T2 → T2 = ⓪{I}. -/2 width=3 by tsts_inv_atom1_aux/ qed-. +(* Basic_1: was just: iso_gen_sort *) +lemma tsts_inv_sort1: ∀h,o,Y,s1. ⋆s1 ⩳[h, o] Y → + ∃∃s2,d. deg h o s1 d & deg h o s2 d & Y = ⋆s2. +/2 width=3 by tsts_inv_sort1_aux/ qed-. -fact tsts_inv_pair1_aux: ∀T1,T2. T1 ≂ T2 → ∀I,W1,U1. T1 = ②{I}W1.U1 → - ∃∃W2,U2. T2 = ②{I}W2. U2. -#T1 #T2 * -T1 -T2 -[ #J #I #W1 #U1 #H destruct -| #J #V1 #V2 #T1 #T2 #I #W1 #U1 #H destruct /2 width=3 by ex1_2_intro/ +fact tsts_inv_lref1_aux: ∀h,o,X,Y. X ⩳[h, o] Y → ∀i. X = #i → Y = #i. +#h #o #X #Y * -X -Y // +[ #s1 #s2 #d #_ #_ #j #H destruct +| #I #V1 #V2 #T1 #T2 #j #H destruct ] qed-. -(* Basic_1: was: iso_gen_head *) -lemma tsts_inv_pair1: ∀I,W1,U1,T2. ②{I}W1.U1 ≂ T2 → - ∃∃W2,U2. T2 = ②{I}W2. U2. -/2 width=5 by tsts_inv_pair1_aux/ qed-. +(* Basic_1: was: iso_gen_lref *) +lemma tsts_inv_lref1: ∀h,o,Y,i. #i ⩳[h, o] Y → Y = #i. +/2 width=5 by tsts_inv_lref1_aux/ qed-. -fact tsts_inv_atom2_aux: ∀T1,T2. T1 ≂ T2 → ∀I. T2 = ⓪{I} → T1 = ⓪{I}. -#T1 #T2 * -T1 -T2 // -#J #V1 #V2 #T1 #T2 #I #H destruct +fact tsts_inv_gref1_aux: ∀h,o,X,Y. X ⩳[h, o] Y → ∀l. X = §l → Y = §l. +#h #o #X #Y * -X -Y // +[ #s1 #s2 #d #_ #_ #k #H destruct +| #I #V1 #V2 #T1 #T2 #k #H destruct +] qed-. -lemma tsts_inv_atom2: ∀I,T1. T1 ≂ ⓪{I} → T1 = ⓪{I}. -/2 width=3 by tsts_inv_atom2_aux/ qed-. - -fact tsts_inv_pair2_aux: ∀T1,T2. T1 ≂ T2 → ∀I,W2,U2. T2 = ②{I}W2.U2 → - ∃∃W1,U1. T1 = ②{I}W1.U1. -#T1 #T2 * -T1 -T2 -[ #J #I #W2 #U2 #H destruct -| #J #V1 #V2 #T1 #T2 #I #W2 #U2 #H destruct /2 width=3 by ex1_2_intro/ +lemma tsts_inv_gref1: ∀h,o,Y,l. §l ⩳[h, o] Y → Y = §l. +/2 width=5 by tsts_inv_gref1_aux/ qed-. + +fact tsts_inv_pair1_aux: ∀h,o,T1,T2. T1 ⩳[h, o] T2 → + ∀I,W1,U1. T1 = ②{I}W1.U1 → + ∃∃W2,U2. T2 = ②{I}W2.U2. +#h #o #T1 #T2 * -T1 -T2 +[ #s1 #s2 #d #_ #_ #J #W1 #U1 #H destruct +| #i #J #W1 #U1 #H destruct +| #l #J #W1 #U1 #H destruct +| #I #V1 #V2 #T1 #T2 #J #W1 #U1 #H destruct /2 width=3 by ex1_2_intro/ ] qed-. -lemma tsts_inv_pair2: ∀I,T1,W2,U2. T1 ≂ ②{I}W2.U2 → - ∃∃W1,U1. T1 = ②{I}W1.U1. -/2 width=5 by tsts_inv_pair2_aux/ qed-. +(* Basic_1: was: iso_gen_head *) +lemma tsts_inv_pair1: ∀h,o,J,W1,U1,T2. ②{J}W1.U1 ⩳[h, o] T2 → + ∃∃W2,U2. T2 = ②{J}W2. U2. +/2 width=7 by tsts_inv_pair1_aux/ qed-. + +(* Advanced inversion lemmas ************************************************) + +lemma tsts_inv_sort1_deg: ∀h,o,Y,s1. ⋆s1 ⩳[h, o] Y → ∀d. deg h o s1 d → + ∃∃s2. deg h o s2 d & Y = ⋆s2. +#h #o #Y #s1 #H #d #Hs1 elim (tsts_inv_sort1 … H) -H +#s2 #x #Hx <(deg_mono h o … Hx … Hs1) -s1 -d /2 width=3 by ex2_intro/ +qed-. + +lemma tsts_inv_sort_deg: ∀h,o,s1,s2. ⋆s1 ⩳[h, o] ⋆s2 → + ∀d1,d2. deg h o s1 d1 → deg h o s2 d2 → + d1 = d2. +#h #o #s1 #y #H #d1 #d2 #Hs1 #Hy +elim (tsts_inv_sort1_deg … H … Hs1) -s1 #s2 #Hs2 #H destruct +<(deg_mono h o … Hy … Hs2) -s2 -d1 // +qed-. + +lemma tsts_inv_pair: ∀h,o,I1,I2,V1,V2,T1,T2. ②{I1}V1.T1 ⩳[h, o] ②{I2}V2.T2 → + I1 = I2. +#h #o #I1 #I2 #V1 #V2 #T1 #T2 #H elim (tsts_inv_pair1 … H) -H +#V0 #T0 #H destruct // +qed-. (* Basic properties *********************************************************) (* Basic_1: was: iso_refl *) -lemma tsts_refl: reflexive … tsts. -#T elim T -T // +lemma tsts_refl: ∀h,o. reflexive … (tsts h o). +#h #o * // +* /2 width=1 by tsts_lref, tsts_gref/ +#s elim (deg_total h o s) /2 width=3 by tsts_sort/ qed. -lemma tsts_sym: symmetric … tsts. -#T1 #T2 #H elim H -T1 -T2 // +lemma tsts_sym: ∀h,o. symmetric … (tsts h o). +#h #o #T1 #T2 * -T1 -T2 /2 width=3 by tsts_sort/ qed-. -lemma tsts_dec: ∀T1,T2. Decidable (T1 ≂ T2). -* #I1 [2: #V1 #T1 ] * #I2 [2,4: #V2 #T2 ] -[ elim (eq_item2_dec I1 I2) #HI12 - [ destruct /2 width=1 by tsts_pair, or_introl/ - | @or_intror #H - elim (tsts_inv_pair1 … H) -H #V #T #H destruct /2 width=1 by/ - ] -| @or_intror #H - lapply (tsts_inv_atom1 … H) -H #H destruct -| @or_intror #H - lapply (tsts_inv_atom2 … H) -H #H destruct -| elim (eq_item0_dec I1 I2) #HI12 - [ destruct /2 width=1 by or_introl/ - | @or_intror #H - lapply (tsts_inv_atom2 … H) -H #H destruct /2 width=1 by/ - ] +lemma tsts_dec: ∀h,o,T1,T2. Decidable (T1 ⩳[h, o] T2). +#h #o * [ * #s1 | #I1 #V1 #T1 ] * [1,3,5,7: * #s2 |*: #I2 #V2 #T2 ] +[ elim (deg_total h o s1) #d1 #H1 + elim (deg_total h o s2) #d2 #H2 + elim (eq_nat_dec d1 d2) #Hd12 destruct /3 width=3 by tsts_sort, or_introl/ + @or_intror #H + lapply (tsts_inv_sort_deg … H … H1 H2) -H -H1 -H2 /2 width=1 by/ +|2,3,13: + @or_intror #H + elim (tsts_inv_sort1 … H) -H #x1 #x2 #_ #_ #H destruct +|4,6,14: + @or_intror #H + lapply (tsts_inv_lref1 … H) -H #H destruct +|5: + elim (eq_nat_dec s1 s2) #Hs12 destruct /2 width=1 by or_introl/ + @or_intror #H + lapply (tsts_inv_lref1 … H) -H #H destruct /2 width=1 by/ +|7,8,15: + @or_intror #H + lapply (tsts_inv_gref1 … H) -H #H destruct +|9: + elim (eq_nat_dec s1 s2) #Hs12 destruct /2 width=1 by or_introl/ + @or_intror #H + lapply (tsts_inv_gref1 … H) -H #H destruct /2 width=1 by/ +|10,11,12: + @or_intror #H + elim (tsts_inv_pair1 … H) -H #X1 #X2 #H destruct +|16: + elim (eq_item2_dec I1 I2) #HI12 destruct + [ /3 width=1 by tsts_pair, or_introl/ ] + @or_intror #H + lapply (tsts_inv_pair … H) -H /2 width=1 by/ ] -qed. - -lemma simple_tsts_repl_dx: ∀T1,T2. T1 ≂ T2 → 𝐒⦃T1⦄ → 𝐒⦃T2⦄. -#T1 #T2 * -T1 -T2 // -#I #V1 #V2 #T1 #T2 #H -elim (simple_inv_pair … H) -H #J #H destruct // qed-. -lemma simple_tsts_repl_sn: ∀T1,T2. T1 ≂ T2 → 𝐒⦃T2⦄ → 𝐒⦃T1⦄. -/3 width=3 by simple_tsts_repl_dx, tsts_sym/ qed-. +(* Basic_2A1: removed theorems 4: + tsts_inv_atom1 tsts_inv_atom2 +*) diff --git a/matita/matita/contribs/lambdadelta/basic_2/syntax/tsts_simple.ma b/matita/matita/contribs/lambdadelta/basic_2/syntax/tsts_simple.ma new file mode 100644 index 000000000..fe3613e8d --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/syntax/tsts_simple.ma @@ -0,0 +1,29 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/syntax/term_simple.ma". +include "basic_2/syntax/tsts.ma". + +(* SAME TOP TERM STRUCTURE **************************************************) + +(* Properies with simple (neutral) terms ************************************) + +lemma simple_tsts_repl_dx: ∀h,o,T1,T2. T1 ⩳[h, o] T2 → 𝐒⦃T1⦄ → 𝐒⦃T2⦄. +#h #o #T1 #T2 * -T1 -T2 // +#I #V1 #V2 #T1 #T2 #H +elim (simple_inv_pair … H) -H #J #H destruct // +qed-. + +lemma simple_tsts_repl_sn: ∀h,o,T1,T2. T1 ⩳[h, o] T2 → 𝐒⦃T2⦄ → 𝐒⦃T1⦄. +/3 width=5 by simple_tsts_repl_dx, tsts_sym/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/syntax/tsts_tdeq.ma b/matita/matita/contribs/lambdadelta/basic_2/syntax/tsts_tdeq.ma new file mode 100644 index 000000000..08e358784 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/syntax/tsts_tdeq.ma @@ -0,0 +1,24 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/syntax/tdeq.ma". +include "basic_2/syntax/tsts.ma". + +(* SAME TOP TERM STRUCTURE **************************************************) + +(* Properties with degree-based equivalence for terms ***********************) + +lemma tdeq_tsts: ∀h,o,T1,T2. T1 ≡[h, o] T2 → T1 ⩳[h, o] T2. +#h #o #T1 #T2 * -T1 -T2 /2 width=3 by tsts_sort, tsts_pair/ +qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/syntax/tsts_tsts.ma b/matita/matita/contribs/lambdadelta/basic_2/syntax/tsts_tsts.ma index 59dfd02e4..b3c790e53 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/syntax/tsts_tsts.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/syntax/tsts_tsts.ma @@ -19,14 +19,19 @@ include "basic_2/syntax/tsts.ma". (* Main properties **********************************************************) (* Basic_1: was: iso_trans *) -theorem tsts_trans: Transitive … tsts. -#T1 #T * -T1 -T // -#I #V1 #V #T1 #T #X #H -elim (tsts_inv_pair1 … H) -H #V2 #T2 #H destruct // +theorem tsts_trans: ∀h,o. Transitive … (tsts h o). +#h #o #T1 #T * -T1 -T +[ #s1 #s #d #Hs1 #Hs #X #H + elim (tsts_inv_sort1_deg … H … Hs) -s /2 width=3 by tsts_sort/ +| #i1 #i #H <(tsts_inv_lref1 … H) -H // +| #l1 #l #H <(tsts_inv_gref1 … H) -H // +| #I #V1 #V #T1 #T #X #H + elim (tsts_inv_pair1 … H) -H #V2 #T2 #H destruct // +] qed-. -theorem tsts_canc_sn: ∀T,T1. T ≂ T1 → ∀T2. T ≂ T2 → T1 ≂ T2. +theorem tsts_canc_sn: ∀h,o. left_cancellable … (tsts h o). /3 width=3 by tsts_trans, tsts_sym/ qed-. -theorem tsts_canc_dx: ∀T1,T. T1 ≂ T → ∀T2. T2 ≂ T → T1 ≂ T2. +theorem tsts_canc_dx: ∀h,o. right_cancellable … (tsts h o). /3 width=3 by tsts_trans, tsts_sym/ qed-. diff --git a/matita/matita/predefined_virtuals.ml b/matita/matita/predefined_virtuals.ml index 6b259a253..12a7c9442 100644 --- a/matita/matita/predefined_virtuals.ml +++ b/matita/matita/predefined_virtuals.ml @@ -1512,7 +1512,7 @@ let predefined_classes = [ ["#"; "♯"; "⋕"; "⧣"; "⧤"; "⌘"; ]; ["+"; "⊞"; ]; ["-"; "÷"; "⊢"; "⊩"; "⊟"; ]; - ["="; "≝"; "≡"; "⩬"; "≂"; "≃"; "≈"; "≅"; "≗"; "≐"; "≑"; "≚"; "≙"; "⌆"; "⊜"; ]; + ["="; "≝"; "≡"; "≗"; "≐"; "≑"; "≚"; "≙"; "⌆"; "⊜"; "⩳"; "≅"; "⩬"; "≂"; "≃"; "≈"; ]; ["→"; "↦"; "⇝"; "⤞"; "⇾"; "⤍"; "⤏"; "⤳"; ] ; ["⇒"; "⤇"; "➾"; "⇨"; "➡"; "⬈"; "➤"; "➸"; "⇉"; "⥰"; ] ; ["^"; "↑"; ] ;