--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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 *)
+(* *)
+(**************************************************************************)
+
+(* ********************************************************************** *)
+(* Progetto FreeScale *)
+(* *)
+(* Sviluppato da: *)
+(* Cosimo Oliboni, oliboni@cs.unibo.it *)
+(* *)
+(* Questo materiale fa parte della tesi: *)
+(* "Formalizzazione Interattiva dei Microcontroller a 8bit FreeScale" *)
+(* *)
+(* data ultima modifica 15/11/2007 *)
+(* ********************************************************************** *)
+
+include "freescale/bool.ma".
+include "freescale/nat.ma".
+
+(* ****** *)
+(* OTTALI *)
+(* ****** *)
+
+ninductive oct : Type ≝
+ o0: oct
+| o1: oct
+| o2: oct
+| o3: oct
+| o4: oct
+| o5: oct
+| o6: oct
+| o7: oct.
+
+ndefinition oct_ind :
+ ΠP:oct → Prop.P o0 → P o1 → P o2 → P o3 → P o4 → P o5 → P o6 → P o7 → Πn:oct.P n ≝
+λP:oct → Prop.
+λp:P o0.λp1:P o1.λp2:P o2.λp3:P o3.λp4:P o4.λp5:P o5.λp6:P o6.λp7:P o7.λn:oct.
+ match n with
+ [ o0 ⇒ p | o1 ⇒ p1 | o2 ⇒ p2 | o3 ⇒ p3 | o4 ⇒ p4 | o5 ⇒ p5 | o6 ⇒ p6 | o7 ⇒ p7 ].
+
+ndefinition oct_rec :
+ ΠP:oct → Set.P o0 → P o1 → P o2 → P o3 → P o4 → P o5 → P o6 → P o7 → Πn:oct.P n ≝
+λP:oct → Set.
+λp:P o0.λp1:P o1.λp2:P o2.λp3:P o3.λp4:P o4.λp5:P o5.λp6:P o6.λp7:P o7.λn:oct.
+ match n with
+ [ o0 ⇒ p | o1 ⇒ p1 | o2 ⇒ p2 | o3 ⇒ p3 | o4 ⇒ p4 | o5 ⇒ p5 | o6 ⇒ p6 | o7 ⇒ p7 ].
+
+ndefinition oct_rect :
+ ΠP:oct → Type.P o0 → P o1 → P o2 → P o3 → P o4 → P o5 → P o6 → P o7 → Πn:oct.P n ≝
+λP:oct → Type.
+λp:P o0.λp1:P o1.λp2:P o2.λp3:P o3.λp4:P o4.λp5:P o5.λp6:P o6.λp7:P o7.λn:oct.
+ match n with
+ [ o0 ⇒ p | o1 ⇒ p1 | o2 ⇒ p2 | o3 ⇒ p3 | o4 ⇒ p4 | o5 ⇒ p5 | o6 ⇒ p6 | o7 ⇒ p7 ].
+
+(* operatore = *)
+ndefinition eq_oct ≝
+λn1,n2:oct.
+ match n1 with
+ [ o0 ⇒ match n2 with
+ [ o0 ⇒ true | o1 ⇒ false | o2 ⇒ false | o3 ⇒ false
+ | o4 ⇒ false | o5 ⇒ false | o6 ⇒ false | o7 ⇒ false ]
+ | o1 ⇒ match n2 with
+ [ o0 ⇒ false | o1 ⇒ true | o2 ⇒ false | o3 ⇒ false
+ | o4 ⇒ false | o5 ⇒ false | o6 ⇒ false | o7 ⇒ false ]
+ | o2 ⇒ match n2 with
+ [ o0 ⇒ false | o1 ⇒ false | o2 ⇒ true | o3 ⇒ false
+ | o4 ⇒ false | o5 ⇒ false | o6 ⇒ false | o7 ⇒ false ]
+ | o3 ⇒ match n2 with
+ [ o0 ⇒ false | o1 ⇒ false | o2 ⇒ false | o3 ⇒ true
+ | o4 ⇒ false | o5 ⇒ false | o6 ⇒ false | o7 ⇒ false ]
+ | o4 ⇒ match n2 with
+ [ o0 ⇒ false | o1 ⇒ false | o2 ⇒ false | o3 ⇒ false
+ | o4 ⇒ true | o5 ⇒ false | o6 ⇒ false | o7 ⇒ false ]
+ | o5 ⇒ match n2 with
+ [ o0 ⇒ false | o1 ⇒ false | o2 ⇒ false | o3 ⇒ false
+ | o4 ⇒ false | o5 ⇒ true | o6 ⇒ false | o7 ⇒ false ]
+ | o6 ⇒ match n2 with
+ [ o0 ⇒ false | o1 ⇒ false | o2 ⇒ false | o3 ⇒ false
+ | o4 ⇒ false | o5 ⇒ false | o6 ⇒ true | o7 ⇒ false ]
+ | o7 ⇒ match n2 with
+ [ o0 ⇒ false | o1 ⇒ false | o2 ⇒ false | o3 ⇒ false
+ | o4 ⇒ false | o5 ⇒ false | o6 ⇒ false | o7 ⇒ true ]
+ ].
+
+(* ottali → naturali *)
+ndefinition nat_of_oct ≝
+λn:oct.
+ match n with
+ [ o0 ⇒ 0 | o1 ⇒ 1 | o2 ⇒ 2 | o3 ⇒ 3 | o4 ⇒ 4 | o5 ⇒ 5 | o6 ⇒ 6 | o7 ⇒ 7 ].
+
+(* iteratore sugli ottali *)
+ndefinition forall_oct ≝ λP.
+ P o0 ⊗ P o1 ⊗ P o2 ⊗ P o3 ⊗ P o4 ⊗ P o5 ⊗ P o6 ⊗ P o7.
+
+(* ************* *)
+(* BITRIGESIMALI *)
+(* ************* *)
+
+ninductive bitrigesim : Type ≝
+ t00: bitrigesim
+| t01: bitrigesim
+| t02: bitrigesim
+| t03: bitrigesim
+| t04: bitrigesim
+| t05: bitrigesim
+| t06: bitrigesim
+| t07: bitrigesim
+| t08: bitrigesim
+| t09: bitrigesim
+| t0A: bitrigesim
+| t0B: bitrigesim
+| t0C: bitrigesim
+| t0D: bitrigesim
+| t0E: bitrigesim
+| t0F: bitrigesim
+| t10: bitrigesim
+| t11: bitrigesim
+| t12: bitrigesim
+| t13: bitrigesim
+| t14: bitrigesim
+| t15: bitrigesim
+| t16: bitrigesim
+| t17: bitrigesim
+| t18: bitrigesim
+| t19: bitrigesim
+| t1A: bitrigesim
+| t1B: bitrigesim
+| t1C: bitrigesim
+| t1D: bitrigesim
+| t1E: bitrigesim
+| t1F: bitrigesim.
+
+ndefinition bitrigesim_ind :
+ ΠP:bitrigesim → Prop.P t00 → P t01 → P t02 → P t03 → P t04 → P t05 → P t06 → P t07 →
+ P t08 → P t09 → P t0A → P t0B → P t0C → P t0D → P t0E → P t0F →
+ P t10 → P t11 → P t12 → P t13 → P t14 → P t15 → P t16 → P t17 →
+ P t18 → P t19 → P t1A → P t1B → P t1C → P t1D → P t1E → P t1F → Πt:bitrigesim.P t ≝
+λP:bitrigesim → Prop.
+λp:P t00.λp1:P t01.λp2:P t02.λp3:P t03.λp4:P t04.λp5:P t05.λp6:P t06.λp7:P t07.
+λp8:P t08.λp9:P t09.λp10:P t0A.λp11:P t0B.λp12:P t0C.λp13:P t0D.λp14:P t0E.λp15:P t0F.
+λp16:P t10.λp17:P t11.λp18:P t12.λp19:P t13.λp20:P t14.λp21:P t15.λp22:P t16.λp23:P t17.
+λp24:P t18.λp25:P t19.λp26:P t1A.λp27:P t1B.λp28:P t1C.λp29:P t1D.λp30:P t1E.λp31:P t1F.λt:bitrigesim.
+ match t with
+ [ t00 ⇒ p | t01 ⇒ p1 | t02 ⇒ p2 | t03 ⇒ p3 | t04 ⇒ p4 | t05 ⇒ p5 | t06 ⇒ p6 | t07 ⇒ p7
+ | t08 ⇒ p8 | t09 ⇒ p9 | t0A ⇒ p10 | t0B ⇒ p11 | t0C ⇒ p12 | t0D ⇒ p13 | t0E ⇒ p14 | t0F ⇒ p15
+ | t10 ⇒ p16 | t11 ⇒ p17 | t12 ⇒ p18 | t13 ⇒ p19 | t14 ⇒ p20 | t15 ⇒ p21 | t16 ⇒ p22 | t17 ⇒ p23
+ | t18 ⇒ p24 | t19 ⇒ p25 | t1A ⇒ p26 | t1B ⇒ p27 | t1C ⇒ p28 | t1D ⇒ p29 | t1E ⇒ p30 | t1F ⇒ p31 ].
+
+ndefinition bitrigesim_rec :
+ ΠP:bitrigesim → Set.P t00 → P t01 → P t02 → P t03 → P t04 → P t05 → P t06 → P t07 →
+ P t08 → P t09 → P t0A → P t0B → P t0C → P t0D → P t0E → P t0F →
+ P t10 → P t11 → P t12 → P t13 → P t14 → P t15 → P t16 → P t17 →
+ P t18 → P t19 → P t1A → P t1B → P t1C → P t1D → P t1E → P t1F → Πt:bitrigesim.P t ≝
+λP:bitrigesim → Set.
+λp:P t00.λp1:P t01.λp2:P t02.λp3:P t03.λp4:P t04.λp5:P t05.λp6:P t06.λp7:P t07.
+λp8:P t08.λp9:P t09.λp10:P t0A.λp11:P t0B.λp12:P t0C.λp13:P t0D.λp14:P t0E.λp15:P t0F.
+λp16:P t10.λp17:P t11.λp18:P t12.λp19:P t13.λp20:P t14.λp21:P t15.λp22:P t16.λp23:P t17.
+λp24:P t18.λp25:P t19.λp26:P t1A.λp27:P t1B.λp28:P t1C.λp29:P t1D.λp30:P t1E.λp31:P t1F.λt:bitrigesim.
+ match t with
+ [ t00 ⇒ p | t01 ⇒ p1 | t02 ⇒ p2 | t03 ⇒ p3 | t04 ⇒ p4 | t05 ⇒ p5 | t06 ⇒ p6 | t07 ⇒ p7
+ | t08 ⇒ p8 | t09 ⇒ p9 | t0A ⇒ p10 | t0B ⇒ p11 | t0C ⇒ p12 | t0D ⇒ p13 | t0E ⇒ p14 | t0F ⇒ p15
+ | t10 ⇒ p16 | t11 ⇒ p17 | t12 ⇒ p18 | t13 ⇒ p19 | t14 ⇒ p20 | t15 ⇒ p21 | t16 ⇒ p22 | t17 ⇒ p23
+ | t18 ⇒ p24 | t19 ⇒ p25 | t1A ⇒ p26 | t1B ⇒ p27 | t1C ⇒ p28 | t1D ⇒ p29 | t1E ⇒ p30 | t1F ⇒ p31 ].
+
+ndefinition bitrigesim_rect :
+ ΠP:bitrigesim → Type.P t00 → P t01 → P t02 → P t03 → P t04 → P t05 → P t06 → P t07 →
+ P t08 → P t09 → P t0A → P t0B → P t0C → P t0D → P t0E → P t0F →
+ P t10 → P t11 → P t12 → P t13 → P t14 → P t15 → P t16 → P t17 →
+ P t18 → P t19 → P t1A → P t1B → P t1C → P t1D → P t1E → P t1F → Πt:bitrigesim.P t ≝
+λP:bitrigesim → Type.
+λp:P t00.λp1:P t01.λp2:P t02.λp3:P t03.λp4:P t04.λp5:P t05.λp6:P t06.λp7:P t07.
+λp8:P t08.λp9:P t09.λp10:P t0A.λp11:P t0B.λp12:P t0C.λp13:P t0D.λp14:P t0E.λp15:P t0F.
+λp16:P t10.λp17:P t11.λp18:P t12.λp19:P t13.λp20:P t14.λp21:P t15.λp22:P t16.λp23:P t17.
+λp24:P t18.λp25:P t19.λp26:P t1A.λp27:P t1B.λp28:P t1C.λp29:P t1D.λp30:P t1E.λp31:P t1F.λt:bitrigesim.
+ match t with
+ [ t00 ⇒ p | t01 ⇒ p1 | t02 ⇒ p2 | t03 ⇒ p3 | t04 ⇒ p4 | t05 ⇒ p5 | t06 ⇒ p6 | t07 ⇒ p7
+ | t08 ⇒ p8 | t09 ⇒ p9 | t0A ⇒ p10 | t0B ⇒ p11 | t0C ⇒ p12 | t0D ⇒ p13 | t0E ⇒ p14 | t0F ⇒ p15
+ | t10 ⇒ p16 | t11 ⇒ p17 | t12 ⇒ p18 | t13 ⇒ p19 | t14 ⇒ p20 | t15 ⇒ p21 | t16 ⇒ p22 | t17 ⇒ p23
+ | t18 ⇒ p24 | t19 ⇒ p25 | t1A ⇒ p26 | t1B ⇒ p27 | t1C ⇒ p28 | t1D ⇒ p29 | t1E ⇒ p30 | t1F ⇒ p31 ].
+
+(* operatore = *)
+ndefinition eq_bitrig ≝
+λt1,t2:bitrigesim.
+ match t1 with
+ [ t00 ⇒ match t2 with
+ [ t00 ⇒ true | t01 ⇒ false | t02 ⇒ false | t03 ⇒ false | t04 ⇒ false | t05 ⇒ false | t06 ⇒ false | t07 ⇒ false
+ | t08 ⇒ false | t09 ⇒ false | t0A ⇒ false | t0B ⇒ false | t0C ⇒ false | t0D ⇒ false | t0E ⇒ false | t0F ⇒ false
+ | t10 ⇒ false | t11 ⇒ false | t12 ⇒ false | t13 ⇒ false | t14 ⇒ false | t15 ⇒ false | t16 ⇒ false | t17 ⇒ false
+ | t18 ⇒ false | t19 ⇒ false | t1A ⇒ false | t1B ⇒ false | t1C ⇒ false | t1D ⇒ false | t1E ⇒ false | t1F ⇒ false ]
+ | t01 ⇒ match t2 with
+ [ t00 ⇒ false | t01 ⇒ true | t02 ⇒ false | t03 ⇒ false | t04 ⇒ false | t05 ⇒ false | t06 ⇒ false | t07 ⇒ false
+ | t08 ⇒ false | t09 ⇒ false | t0A ⇒ false | t0B ⇒ false | t0C ⇒ false | t0D ⇒ false | t0E ⇒ false | t0F ⇒ false
+ | t10 ⇒ false | t11 ⇒ false | t12 ⇒ false | t13 ⇒ false | t14 ⇒ false | t15 ⇒ false | t16 ⇒ false | t17 ⇒ false
+ | t18 ⇒ false | t19 ⇒ false | t1A ⇒ false | t1B ⇒ false | t1C ⇒ false | t1D ⇒ false | t1E ⇒ false | t1F ⇒ false ]
+ | t02 ⇒ match t2 with
+ [ t00 ⇒ false | t01 ⇒ false | t02 ⇒ true | t03 ⇒ false | t04 ⇒ false | t05 ⇒ false | t06 ⇒ false | t07 ⇒ false
+ | t08 ⇒ false | t09 ⇒ false | t0A ⇒ false | t0B ⇒ false | t0C ⇒ false | t0D ⇒ false | t0E ⇒ false | t0F ⇒ false
+ | t10 ⇒ false | t11 ⇒ false | t12 ⇒ false | t13 ⇒ false | t14 ⇒ false | t15 ⇒ false | t16 ⇒ false | t17 ⇒ false
+ | t18 ⇒ false | t19 ⇒ false | t1A ⇒ false | t1B ⇒ false | t1C ⇒ false | t1D ⇒ false | t1E ⇒ false | t1F ⇒ false ]
+ | t03 ⇒ match t2 with
+ [ t00 ⇒ false | t01 ⇒ false | t02 ⇒ false | t03 ⇒ true | t04 ⇒ false | t05 ⇒ false | t06 ⇒ false | t07 ⇒ false
+ | t08 ⇒ false | t09 ⇒ false | t0A ⇒ false | t0B ⇒ false | t0C ⇒ false | t0D ⇒ false | t0E ⇒ false | t0F ⇒ false
+ | t10 ⇒ false | t11 ⇒ false | t12 ⇒ false | t13 ⇒ false | t14 ⇒ false | t15 ⇒ false | t16 ⇒ false | t17 ⇒ false
+ | t18 ⇒ false | t19 ⇒ false | t1A ⇒ false | t1B ⇒ false | t1C ⇒ false | t1D ⇒ false | t1E ⇒ false | t1F ⇒ false ]
+ | t04 ⇒ match t2 with
+ [ t00 ⇒ false | t01 ⇒ false | t02 ⇒ false | t03 ⇒ false | t04 ⇒ true | t05 ⇒ false | t06 ⇒ false | t07 ⇒ false
+ | t08 ⇒ false | t09 ⇒ false | t0A ⇒ false | t0B ⇒ false | t0C ⇒ false | t0D ⇒ false | t0E ⇒ false | t0F ⇒ false
+ | t10 ⇒ false | t11 ⇒ false | t12 ⇒ false | t13 ⇒ false | t14 ⇒ false | t15 ⇒ false | t16 ⇒ false | t17 ⇒ false
+ | t18 ⇒ false | t19 ⇒ false | t1A ⇒ false | t1B ⇒ false | t1C ⇒ false | t1D ⇒ false | t1E ⇒ false | t1F ⇒ false ]
+ | t05 ⇒ match t2 with
+ [ t00 ⇒ false | t01 ⇒ false | t02 ⇒ false | t03 ⇒ false | t04 ⇒ false | t05 ⇒ true | t06 ⇒ false | t07 ⇒ false
+ | t08 ⇒ false | t09 ⇒ false | t0A ⇒ false | t0B ⇒ false | t0C ⇒ false | t0D ⇒ false | t0E ⇒ false | t0F ⇒ false
+ | t10 ⇒ false | t11 ⇒ false | t12 ⇒ false | t13 ⇒ false | t14 ⇒ false | t15 ⇒ false | t16 ⇒ false | t17 ⇒ false
+ | t18 ⇒ false | t19 ⇒ false | t1A ⇒ false | t1B ⇒ false | t1C ⇒ false | t1D ⇒ false | t1E ⇒ false | t1F ⇒ false ]
+ | t06 ⇒ match t2 with
+ [ t00 ⇒ false | t01 ⇒ false | t02 ⇒ false | t03 ⇒ false | t04 ⇒ false | t05 ⇒ false | t06 ⇒ true | t07 ⇒ false
+ | t08 ⇒ false | t09 ⇒ false | t0A ⇒ false | t0B ⇒ false | t0C ⇒ false | t0D ⇒ false | t0E ⇒ false | t0F ⇒ false
+ | t10 ⇒ false | t11 ⇒ false | t12 ⇒ false | t13 ⇒ false | t14 ⇒ false | t15 ⇒ false | t16 ⇒ false | t17 ⇒ false
+ | t18 ⇒ false | t19 ⇒ false | t1A ⇒ false | t1B ⇒ false | t1C ⇒ false | t1D ⇒ false | t1E ⇒ false | t1F ⇒ false ]
+ | t07 ⇒ match t2 with
+ [ t00 ⇒ false | t01 ⇒ false | t02 ⇒ false | t03 ⇒ false | t04 ⇒ false | t05 ⇒ false | t06 ⇒ false | t07 ⇒ true
+ | t08 ⇒ false | t09 ⇒ false | t0A ⇒ false | t0B ⇒ false | t0C ⇒ false | t0D ⇒ false | t0E ⇒ false | t0F ⇒ false
+ | t10 ⇒ false | t11 ⇒ false | t12 ⇒ false | t13 ⇒ false | t14 ⇒ false | t15 ⇒ false | t16 ⇒ false | t17 ⇒ false
+ | t18 ⇒ false | t19 ⇒ false | t1A ⇒ false | t1B ⇒ false | t1C ⇒ false | t1D ⇒ false | t1E ⇒ false | t1F ⇒ false ]
+ | t08 ⇒ match t2 with
+ [ t00 ⇒ false | t01 ⇒ false | t02 ⇒ false | t03 ⇒ false | t04 ⇒ false | t05 ⇒ false | t06 ⇒ false | t07 ⇒ false
+ | t08 ⇒ true | t09 ⇒ false | t0A ⇒ false | t0B ⇒ false | t0C ⇒ false | t0D ⇒ false | t0E ⇒ false | t0F ⇒ false
+ | t10 ⇒ false | t11 ⇒ false | t12 ⇒ false | t13 ⇒ false | t14 ⇒ false | t15 ⇒ false | t16 ⇒ false | t17 ⇒ false
+ | t18 ⇒ false | t19 ⇒ false | t1A ⇒ false | t1B ⇒ false | t1C ⇒ false | t1D ⇒ false | t1E ⇒ false | t1F ⇒ false ]
+ | t09 ⇒ match t2 with
+ [ t00 ⇒ false | t01 ⇒ false | t02 ⇒ false | t03 ⇒ false | t04 ⇒ false | t05 ⇒ false | t06 ⇒ false | t07 ⇒ false
+ | t08 ⇒ false | t09 ⇒ true | t0A ⇒ false | t0B ⇒ false | t0C ⇒ false | t0D ⇒ false | t0E ⇒ false | t0F ⇒ false
+ | t10 ⇒ false | t11 ⇒ false | t12 ⇒ false | t13 ⇒ false | t14 ⇒ false | t15 ⇒ false | t16 ⇒ false | t17 ⇒ false
+ | t18 ⇒ false | t19 ⇒ false | t1A ⇒ false | t1B ⇒ false | t1C ⇒ false | t1D ⇒ false | t1E ⇒ false | t1F ⇒ false ]
+ | t0A ⇒ match t2 with
+ [ t00 ⇒ false | t01 ⇒ false | t02 ⇒ false | t03 ⇒ false | t04 ⇒ false | t05 ⇒ false | t06 ⇒ false | t07 ⇒ false
+ | t08 ⇒ false | t09 ⇒ false | t0A ⇒ true | t0B ⇒ false | t0C ⇒ false | t0D ⇒ false | t0E ⇒ false | t0F ⇒ false
+ | t10 ⇒ false | t11 ⇒ false | t12 ⇒ false | t13 ⇒ false | t14 ⇒ false | t15 ⇒ false | t16 ⇒ false | t17 ⇒ false
+ | t18 ⇒ false | t19 ⇒ false | t1A ⇒ false | t1B ⇒ false | t1C ⇒ false | t1D ⇒ false | t1E ⇒ false | t1F ⇒ false ]
+ | t0B ⇒ match t2 with
+ [ t00 ⇒ false | t01 ⇒ false | t02 ⇒ false | t03 ⇒ false | t04 ⇒ false | t05 ⇒ false | t06 ⇒ false | t07 ⇒ false
+ | t08 ⇒ false | t09 ⇒ false | t0A ⇒ false | t0B ⇒ true | t0C ⇒ false | t0D ⇒ false | t0E ⇒ false | t0F ⇒ false
+ | t10 ⇒ false | t11 ⇒ false | t12 ⇒ false | t13 ⇒ false | t14 ⇒ false | t15 ⇒ false | t16 ⇒ false | t17 ⇒ false
+ | t18 ⇒ false | t19 ⇒ false | t1A ⇒ false | t1B ⇒ false | t1C ⇒ false | t1D ⇒ false | t1E ⇒ false | t1F ⇒ false ]
+ | t0C ⇒ match t2 with
+ [ t00 ⇒ false | t01 ⇒ false | t02 ⇒ false | t03 ⇒ false | t04 ⇒ false | t05 ⇒ false | t06 ⇒ false | t07 ⇒ false
+ | t08 ⇒ false | t09 ⇒ false | t0A ⇒ false | t0B ⇒ false | t0C ⇒ true | t0D ⇒ false | t0E ⇒ false | t0F ⇒ false
+ | t10 ⇒ false | t11 ⇒ false | t12 ⇒ false | t13 ⇒ false | t14 ⇒ false | t15 ⇒ false | t16 ⇒ false | t17 ⇒ false
+ | t18 ⇒ false | t19 ⇒ false | t1A ⇒ false | t1B ⇒ false | t1C ⇒ false | t1D ⇒ false | t1E ⇒ false | t1F ⇒ false ]
+ | t0D ⇒ match t2 with
+ [ t00 ⇒ false | t01 ⇒ false | t02 ⇒ false | t03 ⇒ false | t04 ⇒ false | t05 ⇒ false | t06 ⇒ false | t07 ⇒ false
+ | t08 ⇒ false | t09 ⇒ false | t0A ⇒ false | t0B ⇒ false | t0C ⇒ false | t0D ⇒ true | t0E ⇒ false | t0F ⇒ false
+ | t10 ⇒ false | t11 ⇒ false | t12 ⇒ false | t13 ⇒ false | t14 ⇒ false | t15 ⇒ false | t16 ⇒ false | t17 ⇒ false
+ | t18 ⇒ false | t19 ⇒ false | t1A ⇒ false | t1B ⇒ false | t1C ⇒ false | t1D ⇒ false | t1E ⇒ false | t1F ⇒ false ]
+ | t0E ⇒ match t2 with
+ [ t00 ⇒ false | t01 ⇒ false | t02 ⇒ false | t03 ⇒ false | t04 ⇒ false | t05 ⇒ false | t06 ⇒ false | t07 ⇒ false
+ | t08 ⇒ false | t09 ⇒ false | t0A ⇒ false | t0B ⇒ false | t0C ⇒ false | t0D ⇒ false | t0E ⇒ true | t0F ⇒ false
+ | t10 ⇒ false | t11 ⇒ false | t12 ⇒ false | t13 ⇒ false | t14 ⇒ false | t15 ⇒ false | t16 ⇒ false | t17 ⇒ false
+ | t18 ⇒ false | t19 ⇒ false | t1A ⇒ false | t1B ⇒ false | t1C ⇒ false | t1D ⇒ false | t1E ⇒ false | t1F ⇒ false ]
+ | t0F ⇒ match t2 with
+ [ t00 ⇒ false | t01 ⇒ false | t02 ⇒ false | t03 ⇒ false | t04 ⇒ false | t05 ⇒ false | t06 ⇒ false | t07 ⇒ false
+ | t08 ⇒ false | t09 ⇒ false | t0A ⇒ false | t0B ⇒ false | t0C ⇒ false | t0D ⇒ false | t0E ⇒ false | t0F ⇒ true
+ | t10 ⇒ false | t11 ⇒ false | t12 ⇒ false | t13 ⇒ false | t14 ⇒ false | t15 ⇒ false | t16 ⇒ false | t17 ⇒ false
+ | t18 ⇒ false | t19 ⇒ false | t1A ⇒ false | t1B ⇒ false | t1C ⇒ false | t1D ⇒ false | t1E ⇒ false | t1F ⇒ false ]
+ | t10 ⇒ match t2 with
+ [ t00 ⇒ false | t01 ⇒ false | t02 ⇒ false | t03 ⇒ false | t04 ⇒ false | t05 ⇒ false | t06 ⇒ false | t07 ⇒ false
+ | t08 ⇒ false | t09 ⇒ false | t0A ⇒ false | t0B ⇒ false | t0C ⇒ false | t0D ⇒ false | t0E ⇒ false | t0F ⇒ false
+ | t10 ⇒ true | t11 ⇒ false | t12 ⇒ false | t13 ⇒ false | t14 ⇒ false | t15 ⇒ false | t16 ⇒ false | t17 ⇒ false
+ | t18 ⇒ false | t19 ⇒ false | t1A ⇒ false | t1B ⇒ false | t1C ⇒ false | t1D ⇒ false | t1E ⇒ false | t1F ⇒ false ]
+ | t11 ⇒ match t2 with
+ [ t00 ⇒ false | t01 ⇒ false | t02 ⇒ false | t03 ⇒ false | t04 ⇒ false | t05 ⇒ false | t06 ⇒ false | t07 ⇒ false
+ | t08 ⇒ false | t09 ⇒ false | t0A ⇒ false | t0B ⇒ false | t0C ⇒ false | t0D ⇒ false | t0E ⇒ false | t0F ⇒ false
+ | t10 ⇒ false | t11 ⇒ true | t12 ⇒ false | t13 ⇒ false | t14 ⇒ false | t15 ⇒ false | t16 ⇒ false | t17 ⇒ false
+ | t18 ⇒ false | t19 ⇒ false | t1A ⇒ false | t1B ⇒ false | t1C ⇒ false | t1D ⇒ false | t1E ⇒ false | t1F ⇒ false ]
+ | t12 ⇒ match t2 with
+ [ t00 ⇒ false | t01 ⇒ false | t02 ⇒ false | t03 ⇒ false | t04 ⇒ false | t05 ⇒ false | t06 ⇒ false | t07 ⇒ false
+ | t08 ⇒ false | t09 ⇒ false | t0A ⇒ false | t0B ⇒ false | t0C ⇒ false | t0D ⇒ false | t0E ⇒ false | t0F ⇒ false
+ | t10 ⇒ false | t11 ⇒ false | t12 ⇒ true | t13 ⇒ false | t14 ⇒ false | t15 ⇒ false | t16 ⇒ false | t17 ⇒ false
+ | t18 ⇒ false | t19 ⇒ false | t1A ⇒ false | t1B ⇒ false | t1C ⇒ false | t1D ⇒ false | t1E ⇒ false | t1F ⇒ false ]
+ | t13 ⇒ match t2 with
+ [ t00 ⇒ false | t01 ⇒ false | t02 ⇒ false | t03 ⇒ false | t04 ⇒ false | t05 ⇒ false | t06 ⇒ false | t07 ⇒ false
+ | t08 ⇒ false | t09 ⇒ false | t0A ⇒ false | t0B ⇒ false | t0C ⇒ false | t0D ⇒ false | t0E ⇒ false | t0F ⇒ false
+ | t10 ⇒ false | t11 ⇒ false | t12 ⇒ false | t13 ⇒ true | t14 ⇒ false | t15 ⇒ false | t16 ⇒ false | t17 ⇒ false
+ | t18 ⇒ false | t19 ⇒ false | t1A ⇒ false | t1B ⇒ false | t1C ⇒ false | t1D ⇒ false | t1E ⇒ false | t1F ⇒ false ]
+ | t14 ⇒ match t2 with
+ [ t00 ⇒ false | t01 ⇒ false | t02 ⇒ false | t03 ⇒ false | t04 ⇒ false | t05 ⇒ false | t06 ⇒ false | t07 ⇒ false
+ | t08 ⇒ false | t09 ⇒ false | t0A ⇒ false | t0B ⇒ false | t0C ⇒ false | t0D ⇒ false | t0E ⇒ false | t0F ⇒ false
+ | t10 ⇒ false | t11 ⇒ false | t12 ⇒ false | t13 ⇒ false | t14 ⇒ true | t15 ⇒ false | t16 ⇒ false | t17 ⇒ false
+ | t18 ⇒ false | t19 ⇒ false | t1A ⇒ false | t1B ⇒ false | t1C ⇒ false | t1D ⇒ false | t1E ⇒ false | t1F ⇒ false ]
+ | t15 ⇒ match t2 with
+ [ t00 ⇒ false | t01 ⇒ false | t02 ⇒ false | t03 ⇒ false | t04 ⇒ false | t05 ⇒ false | t06 ⇒ false | t07 ⇒ false
+ | t08 ⇒ false | t09 ⇒ false | t0A ⇒ false | t0B ⇒ false | t0C ⇒ false | t0D ⇒ false | t0E ⇒ false | t0F ⇒ false
+ | t10 ⇒ false | t11 ⇒ false | t12 ⇒ false | t13 ⇒ false | t14 ⇒ false | t15 ⇒ true | t16 ⇒ false | t17 ⇒ false
+ | t18 ⇒ false | t19 ⇒ false | t1A ⇒ false | t1B ⇒ false | t1C ⇒ false | t1D ⇒ false | t1E ⇒ false | t1F ⇒ false ]
+ | t16 ⇒ match t2 with
+ [ t00 ⇒ false | t01 ⇒ false | t02 ⇒ false | t03 ⇒ false | t04 ⇒ false | t05 ⇒ false | t06 ⇒ false | t07 ⇒ false
+ | t08 ⇒ false | t09 ⇒ false | t0A ⇒ false | t0B ⇒ false | t0C ⇒ false | t0D ⇒ false | t0E ⇒ false | t0F ⇒ false
+ | t10 ⇒ false | t11 ⇒ false | t12 ⇒ false | t13 ⇒ false | t14 ⇒ false | t15 ⇒ false | t16 ⇒ true | t17 ⇒ false
+ | t18 ⇒ false | t19 ⇒ false | t1A ⇒ false | t1B ⇒ false | t1C ⇒ false | t1D ⇒ false | t1E ⇒ false | t1F ⇒ false ]
+ | t17 ⇒ match t2 with
+ [ t00 ⇒ false | t01 ⇒ false | t02 ⇒ false | t03 ⇒ false | t04 ⇒ false | t05 ⇒ false | t06 ⇒ false | t07 ⇒ false
+ | t08 ⇒ false | t09 ⇒ false | t0A ⇒ false | t0B ⇒ false | t0C ⇒ false | t0D ⇒ false | t0E ⇒ false | t0F ⇒ false
+ | t10 ⇒ false | t11 ⇒ false | t12 ⇒ false | t13 ⇒ false | t14 ⇒ false | t15 ⇒ false | t16 ⇒ false | t17 ⇒ true
+ | t18 ⇒ false | t19 ⇒ false | t1A ⇒ false | t1B ⇒ false | t1C ⇒ false | t1D ⇒ false | t1E ⇒ false | t1F ⇒ false ]
+ | t18 ⇒ match t2 with
+ [ t00 ⇒ false | t01 ⇒ false | t02 ⇒ false | t03 ⇒ false | t04 ⇒ false | t05 ⇒ false | t06 ⇒ false | t07 ⇒ false
+ | t08 ⇒ false | t09 ⇒ false | t0A ⇒ false | t0B ⇒ false | t0C ⇒ false | t0D ⇒ false | t0E ⇒ false | t0F ⇒ false
+ | t10 ⇒ false | t11 ⇒ false | t12 ⇒ false | t13 ⇒ false | t14 ⇒ false | t15 ⇒ false | t16 ⇒ false | t17 ⇒ false
+ | t18 ⇒ true | t19 ⇒ false | t1A ⇒ false | t1B ⇒ false | t1C ⇒ false | t1D ⇒ false | t1E ⇒ false | t1F ⇒ false ]
+ | t19 ⇒ match t2 with
+ [ t00 ⇒ false | t01 ⇒ false | t02 ⇒ false | t03 ⇒ false | t04 ⇒ false | t05 ⇒ false | t06 ⇒ false | t07 ⇒ false
+ | t08 ⇒ false | t09 ⇒ false | t0A ⇒ false | t0B ⇒ false | t0C ⇒ false | t0D ⇒ false | t0E ⇒ false | t0F ⇒ false
+ | t10 ⇒ false | t11 ⇒ false | t12 ⇒ false | t13 ⇒ false | t14 ⇒ false | t15 ⇒ false | t16 ⇒ false | t17 ⇒ false
+ | t18 ⇒ false | t19 ⇒ true | t1A ⇒ false | t1B ⇒ false | t1C ⇒ false | t1D ⇒ false | t1E ⇒ false | t1F ⇒ false ]
+ | t1A ⇒ match t2 with
+ [ t00 ⇒ false | t01 ⇒ false | t02 ⇒ false | t03 ⇒ false | t04 ⇒ false | t05 ⇒ false | t06 ⇒ false | t07 ⇒ false
+ | t08 ⇒ false | t09 ⇒ false | t0A ⇒ false | t0B ⇒ false | t0C ⇒ false | t0D ⇒ false | t0E ⇒ false | t0F ⇒ false
+ | t10 ⇒ false | t11 ⇒ false | t12 ⇒ false | t13 ⇒ false | t14 ⇒ false | t15 ⇒ false | t16 ⇒ false | t17 ⇒ false
+ | t18 ⇒ false | t19 ⇒ false | t1A ⇒ true | t1B ⇒ false | t1C ⇒ false | t1D ⇒ false | t1E ⇒ false | t1F ⇒ false ]
+ | t1B ⇒ match t2 with
+ [ t00 ⇒ false | t01 ⇒ false | t02 ⇒ false | t03 ⇒ false | t04 ⇒ false | t05 ⇒ false | t06 ⇒ false | t07 ⇒ false
+ | t08 ⇒ false | t09 ⇒ false | t0A ⇒ false | t0B ⇒ false | t0C ⇒ false | t0D ⇒ false | t0E ⇒ false | t0F ⇒ false
+ | t10 ⇒ false | t11 ⇒ false | t12 ⇒ false | t13 ⇒ false | t14 ⇒ false | t15 ⇒ false | t16 ⇒ false | t17 ⇒ false
+ | t18 ⇒ false | t19 ⇒ false | t1A ⇒ false | t1B ⇒ true | t1C ⇒ false | t1D ⇒ false | t1E ⇒ false | t1F ⇒ false ]
+ | t1C ⇒ match t2 with
+ [ t00 ⇒ false | t01 ⇒ false | t02 ⇒ false | t03 ⇒ false | t04 ⇒ false | t05 ⇒ false | t06 ⇒ false | t07 ⇒ false
+ | t08 ⇒ false | t09 ⇒ false | t0A ⇒ false | t0B ⇒ false | t0C ⇒ false | t0D ⇒ false | t0E ⇒ false | t0F ⇒ false
+ | t10 ⇒ false | t11 ⇒ false | t12 ⇒ false | t13 ⇒ false | t14 ⇒ false | t15 ⇒ false | t16 ⇒ false | t17 ⇒ false
+ | t18 ⇒ false | t19 ⇒ false | t1A ⇒ false | t1B ⇒ false | t1C ⇒ true | t1D ⇒ false | t1E ⇒ false | t1F ⇒ false ]
+ | t1D ⇒ match t2 with
+ [ t00 ⇒ false | t01 ⇒ false | t02 ⇒ false | t03 ⇒ false | t04 ⇒ false | t05 ⇒ false | t06 ⇒ false | t07 ⇒ false
+ | t08 ⇒ false | t09 ⇒ false | t0A ⇒ false | t0B ⇒ false | t0C ⇒ false | t0D ⇒ false | t0E ⇒ false | t0F ⇒ false
+ | t10 ⇒ false | t11 ⇒ false | t12 ⇒ false | t13 ⇒ false | t14 ⇒ false | t15 ⇒ false | t16 ⇒ false | t17 ⇒ false
+ | t18 ⇒ false | t19 ⇒ false | t1A ⇒ false | t1B ⇒ false | t1C ⇒ false | t1D ⇒ true | t1E ⇒ false | t1F ⇒ false ]
+ | t1E ⇒ match t2 with
+ [ t00 ⇒ false | t01 ⇒ false | t02 ⇒ false | t03 ⇒ false | t04 ⇒ false | t05 ⇒ false | t06 ⇒ false | t07 ⇒ false
+ | t08 ⇒ false | t09 ⇒ false | t0A ⇒ false | t0B ⇒ false | t0C ⇒ false | t0D ⇒ false | t0E ⇒ false | t0F ⇒ false
+ | t10 ⇒ false | t11 ⇒ false | t12 ⇒ false | t13 ⇒ false | t14 ⇒ false | t15 ⇒ false | t16 ⇒ false | t17 ⇒ false
+ | t18 ⇒ false | t19 ⇒ false | t1A ⇒ false | t1B ⇒ false | t1C ⇒ false | t1D ⇒ false | t1E ⇒ true | t1F ⇒ false ]
+ | t1F ⇒ match t2 with
+ [ t00 ⇒ false | t01 ⇒ false | t02 ⇒ false | t03 ⇒ false | t04 ⇒ false | t05 ⇒ false | t06 ⇒ false | t07 ⇒ false
+ | t08 ⇒ false | t09 ⇒ false | t0A ⇒ false | t0B ⇒ false | t0C ⇒ false | t0D ⇒ false | t0E ⇒ false | t0F ⇒ false
+ | t10 ⇒ false | t11 ⇒ false | t12 ⇒ false | t13 ⇒ false | t14 ⇒ false | t15 ⇒ false | t16 ⇒ false | t17 ⇒ false
+ | t18 ⇒ false | t19 ⇒ false | t1A ⇒ false | t1B ⇒ false | t1C ⇒ false | t1D ⇒ false | t1E ⇒ false | t1F ⇒ true ]
+ ].
+
+(* bitrigesimali → naturali *)
+ndefinition nat_of_bitrigesim ≝
+λt:bitrigesim.
+ match t with
+ [ t00 ⇒ 0 | t01 ⇒ 1 | t02 ⇒ 2 | t03 ⇒ 3 | t04 ⇒ 4 | t05 ⇒ 5 | t06 ⇒ 6 | t07 ⇒ 7
+ | t08 ⇒ 8 | t09 ⇒ 9 | t0A ⇒ 10 | t0B ⇒ 11 | t0C ⇒ 12 | t0D ⇒ 13 | t0E ⇒ 14 | t0F ⇒ 15
+ | t10 ⇒ 16 | t11 ⇒ 17 | t12 ⇒ 18 | t13 ⇒ 19 | t14 ⇒ 20 | t15 ⇒ 21 | t16 ⇒ 22 | t17 ⇒ 23
+ | t18 ⇒ 24 | t19 ⇒ 25 | t1A ⇒ 26 | t1B ⇒ 27 | t1C ⇒ 28 | t1D ⇒ 29 | t1E ⇒ 30 | t1F ⇒ 31 ].
+
+(* iteratore sui bitrigesimali *)
+ndefinition forall_bitrigesim ≝ λP.
+ P t00 ⊗ P t01 ⊗ P t02 ⊗ P t03 ⊗ P t04 ⊗ P t05 ⊗ P t06 ⊗ P t07 ⊗
+ P t08 ⊗ P t09 ⊗ P t0A ⊗ P t0B ⊗ P t0C ⊗ P t0D ⊗ P t0E ⊗ P t0F ⊗
+ P t10 ⊗ P t11 ⊗ P t12 ⊗ P t13 ⊗ P t14 ⊗ P t15 ⊗ P t16 ⊗ P t17 ⊗
+ P t18 ⊗ P t19 ⊗ P t1A ⊗ P t1B ⊗ P t1C ⊗ P t1D ⊗ P t1E ⊗ P t1F.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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 *)
+(* *)
+(**************************************************************************)
+
+(* ********************************************************************** *)
+(* Progetto FreeScale *)
+(* *)
+(* Sviluppato da: *)
+(* Cosimo Oliboni, oliboni@cs.unibo.it *)
+(* *)
+(* Questo materiale fa parte della tesi: *)
+(* "Formalizzazione Interattiva dei Microcontroller a 8bit FreeScale" *)
+(* *)
+(* data ultima modifica 15/11/2007 *)
+(* ********************************************************************** *)
+
+include "freescale/bool_lemmas.ma".
+include "freescale/aux_bases.ma".
+
+(* ****** *)
+(* OTTALI *)
+(* ****** *)
+
+ndefinition oct_destruct :
+ Πn1,n2:oct.ΠP:Prop.n1 = n2 →
+ match n1 with
+ [ o0 ⇒ match n2 with [ o0 ⇒ P → P | _ ⇒ P ]
+ | o1 ⇒ match n2 with [ o1 ⇒ P → P | _ ⇒ P ]
+ | o2 ⇒ match n2 with [ o2 ⇒ P → P | _ ⇒ P ]
+ | o3 ⇒ match n2 with [ o3 ⇒ P → P | _ ⇒ P ]
+ | o4 ⇒ match n2 with [ o4 ⇒ P → P | _ ⇒ P ]
+ | o5 ⇒ match n2 with [ o5 ⇒ P → P | _ ⇒ P ]
+ | o6 ⇒ match n2 with [ o6 ⇒ P → P | _ ⇒ P ]
+ | o7 ⇒ match n2 with [ o7 ⇒ P → P | _ ⇒ P ]
+ ].
+ #n1; #n2; #P;
+ nelim n1;
+ ##[ ##1: nelim n2; nnormalize; #H;
+ ##[ ##1: napply (λx:P.x)
+ ##| ##*: napply (False_ind ??);
+ nchange with (match o0 with [ o0 ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+ ##| ##2: nelim n2; nnormalize; #H;
+ ##[ ##2: napply (λx:P.x)
+ ##| ##*: napply (False_ind ??);
+ nchange with (match o1 with [ o1 ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+ ##| ##3: nelim n2; nnormalize; #H;
+ ##[ ##3: napply (λx:P.x)
+ ##| ##*: napply (False_ind ??);
+ nchange with (match o2 with [ o2 ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+ ##| ##4: nelim n2; nnormalize; #H;
+ ##[ ##4: napply (λx:P.x)
+ ##| ##*: napply (False_ind ??);
+ nchange with (match o3 with [ o3 ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+ ##| ##5: nelim n2; nnormalize; #H;
+ ##[ ##5: napply (λx:P.x)
+ ##| ##*: napply (False_ind ??);
+ nchange with (match o4 with [ o4 ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+ ##| ##6: nelim n2; nnormalize; #H;
+ ##[ ##6: napply (λx:P.x)
+ ##| ##*: napply (False_ind ??);
+ nchange with (match o5 with [ o5 ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+ ##| ##7: nelim n2; nnormalize; #H;
+ ##[ ##7: napply (λx:P.x)
+ ##| ##*: napply (False_ind ??);
+ nchange with (match o6 with [ o6 ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+ ##| ##8: nelim n2; nnormalize; #H;
+ ##[ ##8: napply (λx:P.x)
+ ##| ##*: napply (False_ind ??);
+ nchange with (match o7 with [ o7 ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+ ##]
+nqed.
+
+nlemma symmetric_eqoct : symmetricT oct bool eq_oct.
+ #n1; #n2;
+ nelim n1;
+ nelim n2;
+ nnormalize;
+ napply (refl_eq ??).
+nqed.
+
+nlemma eqoct_to_eq : ∀o1,o2.eq_oct o1 o2 = true → o1 = o2.
+ #n1; #n2; #H;
+ nletin K ≝ (bool_destruct ?? (n1 = n2) H);
+ nelim n1 in K:(%) ⊢ %;
+ nelim n2;
+ nnormalize;
+ ##[ ##1,10,19,28,37,46,55,64: #H; napply (refl_eq ??)
+ ##| ##*: #H; napply H
+ ##]
+nqed.
+
+nlemma eq_to_eqoct : ∀n1,n2.n1 = n2 → eq_oct n1 n2 = true.
+ #n1; #n2; #H;
+ nletin K ≝ (oct_destruct ?? (eq_oct n1 n2 = true) H);
+ nelim n1 in K:(%) ⊢ %;
+ nelim n2;
+ nnormalize;
+ ##[ ##1,10,19,28,37,46,55,64: #H; napply (refl_eq ??)
+ ##| ##*: #H; napply H
+ ##]
+nqed.
+
+(* ************* *)
+(* BITRIGESIMALI *)
+(* ************* *)
+
+ndefinition bitrigesim_destruct :
+ Πt1,t2:bitrigesim.ΠP:Prop.t1 = t2 →
+ match t1 with
+ [ t00 ⇒ match t2 with [ t00 ⇒ P → P | _ ⇒ P ]
+ | t01 ⇒ match t2 with [ t01 ⇒ P → P | _ ⇒ P ]
+ | t02 ⇒ match t2 with [ t02 ⇒ P → P | _ ⇒ P ]
+ | t03 ⇒ match t2 with [ t03 ⇒ P → P | _ ⇒ P ]
+ | t04 ⇒ match t2 with [ t04 ⇒ P → P | _ ⇒ P ]
+ | t05 ⇒ match t2 with [ t05 ⇒ P → P | _ ⇒ P ]
+ | t06 ⇒ match t2 with [ t06 ⇒ P → P | _ ⇒ P ]
+ | t07 ⇒ match t2 with [ t07 ⇒ P → P | _ ⇒ P ]
+ | t08 ⇒ match t2 with [ t08 ⇒ P → P | _ ⇒ P ]
+ | t09 ⇒ match t2 with [ t09 ⇒ P → P | _ ⇒ P ]
+ | t0A ⇒ match t2 with [ t0A ⇒ P → P | _ ⇒ P ]
+ | t0B ⇒ match t2 with [ t0B ⇒ P → P | _ ⇒ P ]
+ | t0C ⇒ match t2 with [ t0C ⇒ P → P | _ ⇒ P ]
+ | t0D ⇒ match t2 with [ t0D ⇒ P → P | _ ⇒ P ]
+ | t0E ⇒ match t2 with [ t0E ⇒ P → P | _ ⇒ P ]
+ | t0F ⇒ match t2 with [ t0F ⇒ P → P | _ ⇒ P ]
+ | t10 ⇒ match t2 with [ t10 ⇒ P → P | _ ⇒ P ]
+ | t11 ⇒ match t2 with [ t11 ⇒ P → P | _ ⇒ P ]
+ | t12 ⇒ match t2 with [ t12 ⇒ P → P | _ ⇒ P ]
+ | t13 ⇒ match t2 with [ t13 ⇒ P → P | _ ⇒ P ]
+ | t14 ⇒ match t2 with [ t14 ⇒ P → P | _ ⇒ P ]
+ | t15 ⇒ match t2 with [ t15 ⇒ P → P | _ ⇒ P ]
+ | t16 ⇒ match t2 with [ t16 ⇒ P → P | _ ⇒ P ]
+ | t17 ⇒ match t2 with [ t17 ⇒ P → P | _ ⇒ P ]
+ | t18 ⇒ match t2 with [ t18 ⇒ P → P | _ ⇒ P ]
+ | t19 ⇒ match t2 with [ t19 ⇒ P → P | _ ⇒ P ]
+ | t1A ⇒ match t2 with [ t1A ⇒ P → P | _ ⇒ P ]
+ | t1B ⇒ match t2 with [ t1B ⇒ P → P | _ ⇒ P ]
+ | t1C ⇒ match t2 with [ t1C ⇒ P → P | _ ⇒ P ]
+ | t1D ⇒ match t2 with [ t1D ⇒ P → P | _ ⇒ P ]
+ | t1E ⇒ match t2 with [ t1E ⇒ P → P | _ ⇒ P ]
+ | t1F ⇒ match t2 with [ t1F ⇒ P → P | _ ⇒ P ]
+ ].
+ #t1; #t2; #P;
+ nelim t1;
+ ##[ ##1: nelim t2; nnormalize; #H;
+ ##[ ##1: napply (λx:P.x)
+ ##| ##*: napply (False_ind ??);
+ nchange with (match t00 with [ t00 ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+ ##| ##2: nelim t2; nnormalize; #H;
+ ##[ ##2: napply (λx:P.x)
+ ##| ##*: napply (False_ind ??);
+ nchange with (match t01 with [ t01 ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+ ##| ##3: nelim t2; nnormalize; #H;
+ ##[ ##3: napply (λx:P.x)
+ ##| ##*: napply (False_ind ??);
+ nchange with (match t02 with [ t02 ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+ ##| ##4: nelim t2; nnormalize; #H;
+ ##[ ##4: napply (λx:P.x)
+ ##| ##*: napply (False_ind ??);
+ nchange with (match t03 with [ t03 ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+ ##| ##5: nelim t2; nnormalize; #H;
+ ##[ ##5: napply (λx:P.x)
+ ##| ##*: napply (False_ind ??);
+ nchange with (match t04 with [ t04 ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+ ##| ##6: nelim t2; nnormalize; #H;
+ ##[ ##6: napply (λx:P.x)
+ ##| ##*: napply (False_ind ??);
+ nchange with (match t05 with [ t05 ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+ ##| ##7: nelim t2; nnormalize; #H;
+ ##[ ##7: napply (λx:P.x)
+ ##| ##*: napply (False_ind ??);
+ nchange with (match t06 with [ t06 ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+ ##| ##8: nelim t2; nnormalize; #H;
+ ##[ ##8: napply (λx:P.x)
+ ##| ##*: napply (False_ind ??);
+ nchange with (match t07 with [ t07 ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+ ##| ##9: nelim t2; nnormalize; #H;
+ ##[ ##9: napply (λx:P.x)
+ ##| ##*: napply (False_ind ??);
+ nchange with (match t08 with [ t08 ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+ ##| ##10: nelim t2; nnormalize; #H;
+ ##[ ##10: napply (λx:P.x)
+ ##| ##*: napply (False_ind ??);
+ nchange with (match t09 with [ t09 ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+ ##| ##11: nelim t2; nnormalize; #H;
+ ##[ ##11: napply (λx:P.x)
+ ##| ##*: napply (False_ind ??);
+ nchange with (match t0A with [ t0A ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+ ##| ##12: nelim t2; nnormalize; #H;
+ ##[ ##12: napply (λx:P.x)
+ ##| ##*: napply (False_ind ??);
+ nchange with (match t0B with [ t0B ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+ ##| ##13: nelim t2; nnormalize; #H;
+ ##[ ##13: napply (λx:P.x)
+ ##| ##*: napply (False_ind ??);
+ nchange with (match t0C with [ t0C ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+ ##| ##14: nelim t2; nnormalize; #H;
+ ##[ ##14: napply (λx:P.x)
+ ##| ##*: napply (False_ind ??);
+ nchange with (match t0D with [ t0D ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+ ##| ##15: nelim t2; nnormalize; #H;
+ ##[ ##15: napply (λx:P.x)
+ ##| ##*: napply (False_ind ??);
+ nchange with (match t0E with [ t0E ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+ ##| ##16: nelim t2; nnormalize; #H;
+ ##[ ##16: napply (λx:P.x)
+ ##| ##*: napply (False_ind ??);
+ nchange with (match t0F with [ t0F ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+ ##| ##17: nelim t2; nnormalize; #H;
+ ##[ ##17: napply (λx:P.x)
+ ##| ##*: napply (False_ind ??);
+ nchange with (match t10 with [ t10 ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+ ##| ##18: nelim t2; nnormalize; #H;
+ ##[ ##18: napply (λx:P.x)
+ ##| ##*: napply (False_ind ??);
+ nchange with (match t11 with [ t11 ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+ ##| ##19: nelim t2; nnormalize; #H;
+ ##[ ##19: napply (λx:P.x)
+ ##| ##*: napply (False_ind ??);
+ nchange with (match t12 with [ t12 ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+ ##| ##20: nelim t2; nnormalize; #H;
+ ##[ ##20: napply (λx:P.x)
+ ##| ##*: napply (False_ind ??);
+ nchange with (match t13 with [ t13 ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+ ##| ##21: nelim t2; nnormalize; #H;
+ ##[ ##21: napply (λx:P.x)
+ ##| ##*: napply (False_ind ??);
+ nchange with (match t14 with [ t14 ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+ ##| ##22: nelim t2; nnormalize; #H;
+ ##[ ##22: napply (λx:P.x)
+ ##| ##*: napply (False_ind ??);
+ nchange with (match t15 with [ t15 ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+ ##| ##23: nelim t2; nnormalize; #H;
+ ##[ ##23: napply (λx:P.x)
+ ##| ##*: napply (False_ind ??);
+ nchange with (match t16 with [ t16 ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+ ##| ##24: nelim t2; nnormalize; #H;
+ ##[ ##24: napply (λx:P.x)
+ ##| ##*: napply (False_ind ??);
+ nchange with (match t17 with [ t17 ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+ ##| ##25: nelim t2; nnormalize; #H;
+ ##[ ##25: napply (λx:P.x)
+ ##| ##*: napply (False_ind ??);
+ nchange with (match t18 with [ t18 ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+ ##| ##26: nelim t2; nnormalize; #H;
+ ##[ ##26: napply (λx:P.x)
+ ##| ##*: napply (False_ind ??);
+ nchange with (match t19 with [ t19 ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+ ##| ##27: nelim t2; nnormalize; #H;
+ ##[ ##27: napply (λx:P.x)
+ ##| ##*: napply (False_ind ??);
+ nchange with (match t1A with [ t1A ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+ ##| ##28: nelim t2; nnormalize; #H;
+ ##[ ##28: napply (λx:P.x)
+ ##| ##*: napply (False_ind ??);
+ nchange with (match t1B with [ t1B ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+ ##| ##29: nelim t2; nnormalize; #H;
+ ##[ ##29: napply (λx:P.x)
+ ##| ##*: napply (False_ind ??);
+ nchange with (match t1C with [ t1C ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+ ##| ##30: nelim t2; nnormalize; #H;
+ ##[ ##30: napply (λx:P.x)
+ ##| ##*: napply (False_ind ??);
+ nchange with (match t1D with [ t1D ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+ ##| ##31: nelim t2; nnormalize; #H;
+ ##[ ##31: napply (λx:P.x)
+ ##| ##*: napply (False_ind ??);
+ nchange with (match t1E with [ t1E ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+ ##| ##32: nelim t2; nnormalize; #H;
+ ##[ ##32: napply (λx:P.x)
+ ##| ##*: napply (False_ind ??);
+ nchange with (match t1F with [ t1F ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+ ##]
+nqed.
+
+nlemma symmetric_eqbitrig : symmetricT bitrigesim bool eq_bitrig.
+ #t1;
+ nelim t1;
+ ##[ ##1: #t2; nelim t2; nnormalize; napply (refl_eq ??)
+ ##| ##2: #t2; nelim t2; nnormalize; napply (refl_eq ??)
+ ##| ##3: #t2; nelim t2; nnormalize; napply (refl_eq ??)
+ ##| ##4: #t2; nelim t2; nnormalize; napply (refl_eq ??)
+ ##| ##5: #t2; nelim t2; nnormalize; napply (refl_eq ??)
+ ##| ##6: #t2; nelim t2; nnormalize; napply (refl_eq ??)
+ ##| ##7: #t2; nelim t2; nnormalize; napply (refl_eq ??)
+ ##| ##8: #t2; nelim t2; nnormalize; napply (refl_eq ??)
+ ##| ##9: #t2; nelim t2; nnormalize; napply (refl_eq ??)
+ ##| ##10: #t2; nelim t2; nnormalize; napply (refl_eq ??)
+ ##| ##11: #t2; nelim t2; nnormalize; napply (refl_eq ??)
+ ##| ##12: #t2; nelim t2; nnormalize; napply (refl_eq ??)
+ ##| ##13: #t2; nelim t2; nnormalize; napply (refl_eq ??)
+ ##| ##14: #t2; nelim t2; nnormalize; napply (refl_eq ??)
+ ##| ##15: #t2; nelim t2; nnormalize; napply (refl_eq ??)
+ ##| ##16: #t2; nelim t2; nnormalize; napply (refl_eq ??)
+ ##| ##17: #t2; nelim t2; nnormalize; napply (refl_eq ??)
+ ##| ##18: #t2; nelim t2; nnormalize; napply (refl_eq ??)
+ ##| ##19: #t2; nelim t2; nnormalize; napply (refl_eq ??)
+ ##| ##20: #t2; nelim t2; nnormalize; napply (refl_eq ??)
+ ##| ##21: #t2; nelim t2; nnormalize; napply (refl_eq ??)
+ ##| ##22: #t2; nelim t2; nnormalize; napply (refl_eq ??)
+ ##| ##23: #t2; nelim t2; nnormalize; napply (refl_eq ??)
+ ##| ##24: #t2; nelim t2; nnormalize; napply (refl_eq ??)
+ ##| ##25: #t2; nelim t2; nnormalize; napply (refl_eq ??)
+ ##| ##26: #t2; nelim t2; nnormalize; napply (refl_eq ??)
+ ##| ##27: #t2; nelim t2; nnormalize; napply (refl_eq ??)
+ ##| ##28: #t2; nelim t2; nnormalize; napply (refl_eq ??)
+ ##| ##29: #t2; nelim t2; nnormalize; napply (refl_eq ??)
+ ##| ##30: #t2; nelim t2; nnormalize; napply (refl_eq ??)
+ ##| ##31: #t2; nelim t2; nnormalize; napply (refl_eq ??)
+ ##| ##32: #t2; nelim t2; nnormalize; napply (refl_eq ??)
+ ##]
+nqed.
+
+nlemma eqbitrig_to_eq : ∀t1,t2.eq_bitrig t1 t2 = true → t1 = t2.
+ #t1; #t2; #H;
+ nletin K ≝ (bool_destruct ?? (t1 = t2) H);
+ nelim t1 in K:(%) ⊢ %;
+ ##[ ##1: nelim t2; nnormalize; #H;
+ ##[ ##1: napply (refl_eq ??)
+ ##| ##*: napply H
+ ##]
+ ##| ##2: nelim t2; nnormalize; #H;
+ ##[ ##2: napply (refl_eq ??)
+ ##| ##*: napply H
+ ##]
+ ##| ##3: nelim t2; nnormalize; #H;
+ ##[ ##3: napply (refl_eq ??)
+ ##| ##*: napply H
+ ##]
+ ##| ##4: nelim t2; nnormalize; #H;
+ ##[ ##4: napply (refl_eq ??)
+ ##| ##*: napply H
+ ##]
+ ##| ##5: nelim t2; nnormalize; #H;
+ ##[ ##5: napply (refl_eq ??)
+ ##| ##*: napply H
+ ##]
+ ##| ##6: nelim t2; nnormalize; #H;
+ ##[ ##6: napply (refl_eq ??)
+ ##| ##*: napply H
+ ##]
+ ##| ##7: nelim t2; nnormalize; #H;
+ ##[ ##7: napply (refl_eq ??)
+ ##| ##*: napply H
+ ##]
+ ##| ##8: nelim t2; nnormalize; #H;
+ ##[ ##8: napply (refl_eq ??)
+ ##| ##*: napply H
+ ##]
+ ##| ##9: nelim t2; nnormalize; #H;
+ ##[ ##9: napply (refl_eq ??)
+ ##| ##*: napply H
+ ##]
+ ##| ##10: nelim t2; nnormalize; #H;
+ ##[ ##10: napply (refl_eq ??)
+ ##| ##*: napply H
+ ##]
+ ##| ##11: nelim t2; nnormalize; #H;
+ ##[ ##11: napply (refl_eq ??)
+ ##| ##*: napply H
+ ##]
+ ##| ##12: nelim t2; nnormalize; #H;
+ ##[ ##12: napply (refl_eq ??)
+ ##| ##*: napply H
+ ##]
+ ##| ##13: nelim t2; nnormalize; #H;
+ ##[ ##13: napply (refl_eq ??)
+ ##| ##*: napply H
+ ##]
+ ##| ##14: nelim t2; nnormalize; #H;
+ ##[ ##14: napply (refl_eq ??)
+ ##| ##*: napply H
+ ##]
+ ##| ##15: nelim t2; nnormalize; #H;
+ ##[ ##15: napply (refl_eq ??)
+ ##| ##*: napply H
+ ##]
+ ##| ##16: nelim t2; nnormalize; #H;
+ ##[ ##16: napply (refl_eq ??)
+ ##| ##*: napply H
+ ##]
+ ##| ##17: nelim t2; nnormalize; #H;
+ ##[ ##17: napply (refl_eq ??)
+ ##| ##*: napply H
+ ##]
+ ##| ##18: nelim t2; nnormalize; #H;
+ ##[ ##18: napply (refl_eq ??)
+ ##| ##*: napply H
+ ##]
+ ##| ##19: nelim t2; nnormalize; #H;
+ ##[ ##19: napply (refl_eq ??)
+ ##| ##*: napply H
+ ##]
+ ##| ##20: nelim t2; nnormalize; #H;
+ ##[ ##20: napply (refl_eq ??)
+ ##| ##*: napply H
+ ##]
+ ##| ##21: nelim t2; nnormalize; #H;
+ ##[ ##21: napply (refl_eq ??)
+ ##| ##*: napply H
+ ##]
+ ##| ##22: nelim t2; nnormalize; #H;
+ ##[ ##22: napply (refl_eq ??)
+ ##| ##*: napply H
+ ##]
+ ##| ##23: nelim t2; nnormalize; #H;
+ ##[ ##23: napply (refl_eq ??)
+ ##| ##*: napply H
+ ##]
+ ##| ##24: nelim t2; nnormalize; #H;
+ ##[ ##24: napply (refl_eq ??)
+ ##| ##*: napply H
+ ##]
+ ##| ##25: nelim t2; nnormalize; #H;
+ ##[ ##25: napply (refl_eq ??)
+ ##| ##*: napply H
+ ##]
+ ##| ##26: nelim t2; nnormalize; #H;
+ ##[ ##26: napply (refl_eq ??)
+ ##| ##*: napply H
+ ##]
+ ##| ##27: nelim t2; nnormalize; #H;
+ ##[ ##27: napply (refl_eq ??)
+ ##| ##*: napply H
+ ##]
+ ##| ##28: nelim t2; nnormalize; #H;
+ ##[ ##28: napply (refl_eq ??)
+ ##| ##*: napply H
+ ##]
+ ##| ##29: nelim t2; nnormalize; #H;
+ ##[ ##29: napply (refl_eq ??)
+ ##| ##*: napply H
+ ##]
+ ##| ##30: nelim t2; nnormalize; #H;
+ ##[ ##30: napply (refl_eq ??)
+ ##| ##*: napply H
+ ##]
+ ##| ##31: nelim t2; nnormalize; #H;
+ ##[ ##31: napply (refl_eq ??)
+ ##| ##*: napply H
+ ##]
+ ##| ##32: nelim t2; nnormalize; #H;
+ ##[ ##32: napply (refl_eq ??)
+ ##| ##*: napply H
+ ##]
+ ##]
+nqed.
+
+nlemma eq_to_eqbitrig : ∀t1,t2.t1 = t2 → eq_bitrig t1 t2 = true.
+ #t1; #t2; #H;
+ nletin K ≝ (bitrigesim_destruct ?? (eq_bitrig t1 t2 = true) H);
+ nelim t1 in K:(%) ⊢ %;
+ ##[ ##1: nelim t2; nnormalize; #H;
+ ##[ ##1: napply (refl_eq ??)
+ ##| ##*: napply H
+ ##]
+ ##| ##2: nelim t2; nnormalize; #H;
+ ##[ ##2: napply (refl_eq ??)
+ ##| ##*: napply H
+ ##]
+ ##| ##3: nelim t2; nnormalize; #H;
+ ##[ ##3: napply (refl_eq ??)
+ ##| ##*: napply H
+ ##]
+ ##| ##4: nelim t2; nnormalize; #H;
+ ##[ ##4: napply (refl_eq ??)
+ ##| ##*: napply H
+ ##]
+ ##| ##5: nelim t2; nnormalize; #H;
+ ##[ ##5: napply (refl_eq ??)
+ ##| ##*: napply H
+ ##]
+ ##| ##6: nelim t2; nnormalize; #H;
+ ##[ ##6: napply (refl_eq ??)
+ ##| ##*: napply H
+ ##]
+ ##| ##7: nelim t2; nnormalize; #H;
+ ##[ ##7: napply (refl_eq ??)
+ ##| ##*: napply H
+ ##]
+ ##| ##8: nelim t2; nnormalize; #H;
+ ##[ ##8: napply (refl_eq ??)
+ ##| ##*: napply H
+ ##]
+ ##| ##9: nelim t2; nnormalize; #H;
+ ##[ ##9: napply (refl_eq ??)
+ ##| ##*: napply H
+ ##]
+ ##| ##10: nelim t2; nnormalize; #H;
+ ##[ ##10: napply (refl_eq ??)
+ ##| ##*: napply H
+ ##]
+ ##| ##11: nelim t2; nnormalize; #H;
+ ##[ ##11: napply (refl_eq ??)
+ ##| ##*: napply H
+ ##]
+ ##| ##12: nelim t2; nnormalize; #H;
+ ##[ ##12: napply (refl_eq ??)
+ ##| ##*: napply H
+ ##]
+ ##| ##13: nelim t2; nnormalize; #H;
+ ##[ ##13: napply (refl_eq ??)
+ ##| ##*: napply H
+ ##]
+ ##| ##14: nelim t2; nnormalize; #H;
+ ##[ ##14: napply (refl_eq ??)
+ ##| ##*: napply H
+ ##]
+ ##| ##15: nelim t2; nnormalize; #H;
+ ##[ ##15: napply (refl_eq ??)
+ ##| ##*: napply H
+ ##]
+ ##| ##16: nelim t2; nnormalize; #H;
+ ##[ ##16: napply (refl_eq ??)
+ ##| ##*: napply H
+ ##]
+ ##| ##17: nelim t2; nnormalize; #H;
+ ##[ ##17: napply (refl_eq ??)
+ ##| ##*: napply H
+ ##]
+ ##| ##18: nelim t2; nnormalize; #H;
+ ##[ ##18: napply (refl_eq ??)
+ ##| ##*: napply H
+ ##]
+ ##| ##19: nelim t2; nnormalize; #H;
+ ##[ ##19: napply (refl_eq ??)
+ ##| ##*: napply H
+ ##]
+ ##| ##20: nelim t2; nnormalize; #H;
+ ##[ ##20: napply (refl_eq ??)
+ ##| ##*: napply H
+ ##]
+ ##| ##21: nelim t2; nnormalize; #H;
+ ##[ ##21: napply (refl_eq ??)
+ ##| ##*: napply H
+ ##]
+ ##| ##22: nelim t2; nnormalize; #H;
+ ##[ ##22: napply (refl_eq ??)
+ ##| ##*: napply H
+ ##]
+ ##| ##23: nelim t2; nnormalize; #H;
+ ##[ ##23: napply (refl_eq ??)
+ ##| ##*: napply H
+ ##]
+ ##| ##24: nelim t2; nnormalize; #H;
+ ##[ ##24: napply (refl_eq ??)
+ ##| ##*: napply H
+ ##]
+ ##| ##25: nelim t2; nnormalize; #H;
+ ##[ ##25: napply (refl_eq ??)
+ ##| ##*: napply H
+ ##]
+ ##| ##26: nelim t2; nnormalize; #H;
+ ##[ ##26: napply (refl_eq ??)
+ ##| ##*: napply H
+ ##]
+ ##| ##27: nelim t2; nnormalize; #H;
+ ##[ ##27: napply (refl_eq ??)
+ ##| ##*: napply H
+ ##]
+ ##| ##28: nelim t2; nnormalize; #H;
+ ##[ ##28: napply (refl_eq ??)
+ ##| ##*: napply H
+ ##]
+ ##| ##29: nelim t2; nnormalize; #H;
+ ##[ ##29: napply (refl_eq ??)
+ ##| ##*: napply H
+ ##]
+ ##| ##30: nelim t2; nnormalize; #H;
+ ##[ ##30: napply (refl_eq ??)
+ ##| ##*: napply H
+ ##]
+ ##| ##31: nelim t2; nnormalize; #H;
+ ##[ ##31: napply (refl_eq ??)
+ ##| ##*: napply H
+ ##]
+ ##| ##32: nelim t2; nnormalize; #H;
+ ##[ ##32: napply (refl_eq ??)
+ ##| ##*: napply H
+ ##]
+ ##]
+nqed.
projects / helm.git / commitdiff