[ . forall X1:Nat

. (op pre : Nat ->? Nat)((op suc : Nat -> Nat)((var X1 : Nat))) =

(var X1 : Nat) %(ga_selector_pre)%,

. forall X1:Nat; Y1:Nat

. (op suc : Nat -> Nat)((var X1 : Nat)) =

(op suc : Nat -> Nat)((var Y1 : Nat)) <=>

(var X1 : Nat) = (var Y1 : Nat) %(ga_injective_suc)%,

. forall Y1:Nat

. not (op 0 : Nat) =

(op suc : Nat -> Nat)((var Y1 : Nat)) %(ga_disjoint_0_suc)%,

. not def (op pre : Nat ->? Nat)((op 0 : Nat)) %(ga_selector_undef_pre_0)%,

generated{sort Nat; op 0 : Nat;

op suc : Nat -> Nat} %(ga_generated_Nat)%,

. forall m, n, r, s:Nat

. (pred __<=__ : Int * Int)((op inj : Nat -> Int)((op 0 : Nat)),

(op inj : Nat -> Int)((var n : Nat))) %(Nat_leq_def1)%,

. forall m, n, r, s:Nat

. not (pred __<=__ : Int *

Int)((op inj : Pos -> Int)((op suc : Nat -> Pos)((var n : Nat))),

(op inj : Nat -> Int)((op 0 : Nat))) %(Nat_leq_def2)%,

. forall m, n, r, s:Nat

. (pred __<=__ : Int *

Int)((op inj : Pos -> Int)((op suc : Nat -> Pos)((var m : Nat))),

(op inj : Pos -> Int)((op suc : Nat -> Pos)((var n : Nat)))) <=>

(pred __<=__ : Int * Int)((op inj : Nat -> Int)((var m : Nat)),

(op inj : Nat -> Int)((var n : Nat))) %(Nat_leq_def3)%,

. forall m, n, r, s:Nat

. (pred __>=__ : Int * Int)((op inj : Nat -> Int)((var m : Nat)),

(op inj : Nat -> Int)((var n : Nat))) <=>

(pred __<=__ : Int * Int)((op inj : Nat -> Int)((var n : Nat)),

(op inj : Nat -> Int)((var m : Nat))) %(Nat_geq_def)%,

. forall m, n, r, s:Nat

. (pred __<__ : Int * Int)((op inj : Nat -> Int)((var m : Nat)),

(op inj : Nat -> Int)((var n : Nat))) <=>

(pred __<=__ : Int * Int)((op inj : Nat -> Int)((var m : Nat)),

(op inj : Nat -> Int)((var n : Nat)))

/\ not (var m : Nat) = (var n : Nat) %(Nat_less_def)%,

. forall m, n, r, s:Nat

. (pred __>__ : Int * Int)((op inj : Nat -> Int)((var m : Nat)),

(op inj : Nat -> Int)((var n : Nat))) <=>

(pred __<__ : Int * Int)((op inj : Nat -> Int)((var m : Nat)),

(op inj : Nat -> Int)((var n : Nat))) %(Nat_greater_def)%,

. forall m, n, r, s:Nat

. (op __+__ : Nat * Nat -> Nat)((op 0 : Nat), (var m : Nat)) =

(var m : Nat) %(Nat_add_0)%,

. forall m, n, r, s:Nat

. (op __+__ : Pos *

Nat -> Pos)((op suc : Nat -> Pos)((var n : Nat)), (var m : Nat)) =

(op suc : Nat -> Pos)((op __+__ : Nat * Nat -> Nat)((var n : Nat),

(var m : Nat))) %(Nat_add_suc)%,

. forall m, n, r, s:Nat

. (op __*__ : Nat * Nat -> Nat)((op 0 : Nat), (var m : Nat)) =

(op 0 : Nat) %(Nat_mult_0)%,

. forall m, n, r, s:Nat

. (op __*__ : Nat *

Nat -> Nat)((op inj : Pos -> Nat)((op suc : Nat -> Pos)((var n : Nat))),

(var m : Nat)) =

(op __+__ : Nat * Nat -> Nat)((op __*__ : Nat *

Nat -> Nat)((var n : Nat), (var m : Nat)),

(var m : Nat)) %(Nat_mult_suc)%,

. forall m, n, r, s:Nat

. (op __^__ : Nat * Nat -> Nat)((var m : Nat), (op 0 : Nat)) =

(op inj : Pos -> Nat)((op 1 : Pos)) %(Nat_power_0)%,

. forall m, n, r, s:Nat

. (op __^__ : Nat * Nat -> Nat)((var m : Nat),

(op inj : Pos -> Nat)((op suc : Nat -> Pos)((var n : Nat)))) =

(op __*__ : Nat * Nat -> Nat)((var m : Nat),

(op __^__ : Nat * Nat -> Nat)((var m : Nat),

(var n : Nat))) %(Nat_power_suc)%,

. forall m, n, r, s:Nat

. (op min : Nat * Nat -> Nat)((var m : Nat), (var n : Nat)) =

(var m : Nat)

when (pred __<=__ : Int *

Int)((op inj : Nat -> Int)((var m : Nat)),

(op inj : Nat -> Int)((var n : Nat)))

else (var n : Nat) %(Nat_min_def)%,

. forall m, n, r, s:Nat

. (op max : Nat * Nat -> Nat)((var m : Nat), (var n : Nat)) =

(var n : Nat)

when (pred __<=__ : Int *

Int)((op inj : Nat -> Int)((var m : Nat)),

(op inj : Nat -> Int)((var n : Nat)))

else (var m : Nat) %(Nat_max_def)%,

. forall m, n, r, s:Nat

. (op +__ : Nat -> Nat)((var m : Nat)) =

(var m : Nat) %(plus_def)%,

. forall m, n, r, s:Nat

. (op abs : Int -> Nat)((op inj : Nat -> Int)((var n : Nat))) =

(var n : Nat) %(Nat_abs)%,

. forall m, n, r, s:Nat

. (pred odd : Int)((op inj : Nat -> Int)((var m : Nat))) <=>

not (pred even : Int)((op inj : Nat -> Int)((var m : Nat))) %(Nat_odd_def)%,

. forall m, n, r, s:Nat

. (pred even : Int)((op inj : Nat -> Int)((op 0 : Nat))) %(Nat_even_0)%,

. forall m, n, r, s:Nat

. (pred even : Int)((op inj : Pos -> Int)((op suc : Nat -> Pos)((var m : Nat)))) <=>

(pred odd : Int)((op inj : Nat -> Int)((var m : Nat))) %(Nat_even_suc)%,

. forall m, n, r, s:Nat

. (op __! : Nat -> Nat)((op 0 : Nat)) =

(op inj : Pos -> Nat)((op 1 : Pos)) %(Nat_factorial_0)%,

. forall m, n, r, s:Nat

. (op __! : Nat -> Nat)((op inj : Pos -> Nat)((op suc : Nat -> Pos)((var n : Nat)))) =

(op __*__ : Nat *

Nat -> Nat)((op inj : Pos -> Nat)((op suc : Nat -> Pos)((var n : Nat))),

(op __! : Nat -> Nat)((var n : Nat))) %(Nat_factorial_suc)%,

. forall m, n, r, s:Nat

. (op __-?__ : Nat * Nat ->? Nat)((var m : Nat), (var n : Nat)) =

(var r : Nat) <=>

(var m : Nat) =

(op __+__ : Nat * Nat -> Nat)((var r : Nat),

(var n : Nat)) %(Nat_sub_def)%,

. forall m, n, r, s:Nat

. not def (op __/?__ : Nat * Nat ->? Nat)((var m : Nat),

(op 0 : Nat)) %(Nat_divide_0)%,

. forall m, n, r, s:Nat

. ((op __/?__ : Nat * Nat ->? Nat)((var m : Nat), (var n : Nat)) =

(var r : Nat) <=>

(var m : Nat) =

(op __*__ : Nat * Nat -> Nat)((var r : Nat), (var n : Nat))) if

(pred __>__ : Int * Int)((op inj : Nat -> Int)((var n : Nat)),

(op inj : Nat -> Int)((op 0 : Nat))) %(Nat_divide_Pos)%,

. forall m, n, r, s:Nat

. (op __div__ : Nat * Nat ->? Nat)((var m : Nat), (var n : Nat)) =

(var r : Nat) <=>

(exists s:Nat

. (var m : Nat) =

(op __+__ : Nat * Nat -> Nat)((op __*__ : Nat *

Nat -> Nat)((var n : Nat),

(var r : Nat)),

(var s : Nat))

/\ (pred __<__ : Int * Int)((op inj : Nat -> Int)((var s : Nat)),

(op inj : Nat -> Int)((var n : Nat)))) %(Nat_div)%,

. forall m, n, r, s:Nat

. (op __mod__ : Int *

Int ->? Nat)((op inj : Nat -> Int)((var m : Nat)),

(op inj : Nat -> Int)((var n : Nat))) =

(var s : Nat) <=>

(exists r:Nat

. (var m : Nat) =

(op __+__ : Nat * Nat -> Nat)((op __*__ : Nat *

Nat -> Nat)((var n : Nat),

(var r : Nat)),

(var s : Nat))

/\ (pred __<__ : Int * Int)((op inj : Nat -> Int)((var s : Nat)),

(op inj : Nat -> Int)((var n : Nat)))) %(Nat_mod)%,

. forall m, n, r, s:Nat

. (op __quot__ : Nat * Nat ->? Nat)((var m : Nat), (var n : Nat)) =

(op __div__ : Nat * Nat ->? Nat)((var m : Nat),

(var n : Nat)) %(Nat_quot)%,

. forall m, n, r, s:Nat

. (op __rem__ : Nat * Nat ->? Nat)((var m : Nat), (var n : Nat)) =

(op __mod__ : Int *

Int ->? Nat)((op inj : Nat -> Int)((var m : Nat)),

(op inj : Nat -> Int)((var n : Nat))) %(Nat_rem)%,

. forall m, n, r, s:Nat

. (op 1 : Pos) = (op suc : Nat -> Pos)((op 0 : Nat)) %(Nat_1_def)%,

. forall m, n, r, s:Nat

. (op 2 : Nat) =

(op inj : Pos -> Nat)((op suc : Nat -> Pos)((op inj : Pos -> Nat)((op 1 : Pos)))) %(Nat_2_def)%,

. forall m, n, r, s:Nat

. (op 3 : Nat) =

(op inj : Pos -> Nat)((op suc : Nat -> Pos)((op 2 : Nat))) %(Nat_3_def)%,

. forall m, n, r, s:Nat

. (op 4 : Nat) =

(op inj : Pos -> Nat)((op suc : Nat -> Pos)((op 3 : Nat))) %(Nat_4_def)%,

. forall m, n, r, s:Nat

. (op 5 : Nat) =

(op inj : Pos -> Nat)((op suc : Nat -> Pos)((op 4 : Nat))) %(Nat_5_def)%,

. forall m, n, r, s:Nat

. (op 6 : Nat) =

(op inj : Pos -> Nat)((op suc : Nat -> Pos)((op 5 : Nat))) %(Nat_6_def)%,

. forall m, n, r, s:Nat

. (op 7 : Nat) =

(op inj : Pos -> Nat)((op suc : Nat -> Pos)((op 6 : Nat))) %(Nat_7_def)%,

. forall m, n, r, s:Nat

. (op 8 : Nat) =

(op inj : Pos -> Nat)((op suc : Nat -> Pos)((op 7 : Nat))) %(Nat_8_def)%,

. forall m, n, r, s:Nat

. (op 9 : Nat) =

(op inj : Pos -> Nat)((op suc : Nat -> Pos)((op 8 : Nat))) %(Nat_9_def)%,

. forall m, n, r, s:Nat

. (op __@@__ : Nat * Nat -> Nat)((var m : Nat), (var n : Nat)) =

(op __+__ : Nat * Nat -> Nat)((op __*__ : Nat *

Nat -> Nat)((var m : Nat),

(op inj : Pos -> Nat)((op suc : Nat -> Pos)((op 9 : Nat)))),

(var n : Nat)) %(Nat_decimal_def)%,

. forall p:Nat

. (var p : Nat) in Pos <=>

(pred __>__ : Int * Int)((op inj : Nat -> Int)((var p : Nat)),

(op inj : Nat -> Int)((op 0 : Nat))),

. (op 1 : Pos) =

(op suc : Nat -> Pos)((op 0 : Nat)) %(Nat_1_as_Pos_def)%,

. forall x:Nat; y:Nat

. (op min : Nat * Nat -> Nat)((var x : Nat), (var y : Nat)) =

(op min : Nat * Nat -> Nat)((var y : Nat),

(var x : Nat)) %(ga_comm_min)%,

. forall x:Nat; y:Nat

. (op max : Nat * Nat -> Nat)((var x : Nat), (var y : Nat)) =

(op max : Nat * Nat -> Nat)((var y : Nat),

(var x : Nat)) %(ga_comm_max)%,

. forall x:Nat; y:Nat; z:Nat

. (op min : Nat * Nat -> Nat)((var x : Nat),

(op min : Nat * Nat -> Nat)((var y : Nat), (var z : Nat))) =

(op min : Nat * Nat -> Nat)((op min : Nat *

Nat -> Nat)((var x : Nat), (var y : Nat)),

(var z : Nat)) %(ga_assoc_min)%,

. forall x:Nat; y:Nat; z:Nat

. (op max : Nat * Nat -> Nat)((var x : Nat),

(op max : Nat * Nat -> Nat)((var y : Nat), (var z : Nat))) =

(op max : Nat * Nat -> Nat)((op max : Nat *

Nat -> Nat)((var x : Nat), (var y : Nat)),

(var z : Nat)) %(ga_assoc_max)%,

. forall x, m, n, r, s, t:Nat; p:Pos

. def (op __-?__ : Nat * Nat ->? Nat)((var m : Nat),

(var n : Nat)) <=>

(pred __>=__ : Int * Int)((op inj : Nat -> Int)((var m : Nat)),

(op inj : Nat -> Int)((var n : Nat))) %(Nat_sub_dom)%,

. forall x, m, n, r, s, t:Nat; p:Pos

. def (op __/?__ : Nat * Nat ->? Nat)((var m : Nat),

(var n : Nat)) <=>

(op __mod__ : Int *

Int ->? Nat)((op inj : Nat -> Int)((var m : Nat)),

(op inj : Nat -> Int)((var n : Nat))) =

(op 0 : Nat) %(Nat_divide_dom)%,

. forall x, m, n, r, s, t:Nat; p:Pos

. def (op __div__ : Nat * Nat ->? Nat)((var m : Nat),

(var n : Nat)) <=>

not (var n : Nat) = (op 0 : Nat) %(Nat_div_dom)%,

. forall x, m, n, r, s, t:Nat; p:Pos

. def (op __mod__ : Int *

Int ->? Nat)((op inj : Nat -> Int)((var m : Nat)),

(op inj : Nat -> Int)((var n : Nat))) <=>

not (var n : Nat) = (op 0 : Nat) %(Nat_mod_dom)%,

. forall x, m, n, r, s, t:Nat; p:Pos

. def (op __quot__ : Nat * Nat ->? Nat)((var m : Nat),

(var n : Nat)) <=>

not (var n : Nat) = (op 0 : Nat) %(Nat_quot_dom)%,

. forall x, m, n, r, s, t:Nat; p:Pos

. def (op __rem__ : Nat * Nat ->? Nat)((var m : Nat),

(var n : Nat)) <=>

not (var n : Nat) = (op 0 : Nat) %(Nat_rem_dom)%,

. forall x, m, n, r, s, t:Nat; p:Pos

. (op __*__ : Nat * Nat -> Nat)((op __+__ : Nat *

Nat -> Nat)((var r : Nat), (var s : Nat)),

(var t : Nat)) =

(op __+__ : Nat * Nat -> Nat)((op __*__ : Nat *

Nat -> Nat)((var r : Nat), (var t : Nat)),

(op __*__ : Nat * Nat -> Nat)((var s : Nat),

(var t : Nat))) %(Nat_distr)%,

. forall x, m, n, r, s, t:Nat; p:Pos

. (op max : Nat * Nat -> Nat)((var m : Nat), (op 0 : Nat)) =

(var m : Nat) %(Nat_max_unit)%,

. forall x, m, n, r, s, t:Nat; p:Pos

. (op min : Nat * Nat -> Nat)((var m : Nat), (op 0 : Nat)) =

(op 0 : Nat) %(Nat_min_0)%,

generated{sort Int; op __-__ : Nat *

Nat -> Int} %(ga_generated_Int)%,

. forall a:Nat

. (op inj : Nat -> Int)((var a : Nat)) =

(op __-__ : Int * Int -> Int)((op inj : Nat -> Int)((var a : Nat)),

(op inj : Nat -> Int)((op 0 : Nat))) %(Int_Nat_embedding)%,

. forall m, n, r, s:Int; a, b, c, d:Nat

. (op __-__ : Int * Int -> Int)((var m : Int), (var n : Int)) =

(op __+__ : Int * Int -> Int)((var m : Int),

(op -__ : Int -> Int)((var n : Int))) %(Int_sub_def)%,

. forall m, n, r, s:Int; a, b, c, d:Nat

. (op +__ : Int -> Int)((var m : Int)) =

(var m : Int) %(Int_pos_def)%,

. forall m, n, r, s:Int; a, b, c, d:Nat

. (op -__ : Int -> Int)((op __-__ : Int *

Int -> Int)((op inj : Nat -> Int)((var a : Nat)),

(op inj : Nat -> Int)((var b : Nat)))) =

(op __-__ : Int * Int -> Int)((op inj : Nat -> Int)((var b : Nat)),

(op inj : Nat -> Int)((var a : Nat))) %(Int_neg_def)%,

. forall m, n, r, s:Int; a, b, c, d:Nat

. (op sign : Int -> Int)((var m : Int)) =

(op inj : Nat -> Int)((op 0 : Nat))

when (var m : Int) = (op inj : Nat -> Int)((op 0 : Nat))

else (op inj : Pos -> Int)((op 1 : Pos))

when (pred __>__ : Int * Int)((var m : Int),

(op inj : Nat -> Int)((op 0 : Nat)))

else (op -__ : Int -> Int)((op inj : Pos -> Int)((op 1 : Pos))) %(Int_sign_def)%,

. forall m, n, r, s:Int; a, b, c, d:Nat

. (pred __<=__ : Int * Int)((var m : Int), (var n : Int)) <=>

(op __-__ : Int * Int -> Int)((var n : Int),

(var m : Int)) in Nat %(Int_leq_def)%,

. forall m, n, r, s:Int; a, b, c, d:Nat

. (pred __>=__ : Int * Int)((var m : Int), (var n : Int)) <=>

(pred __<=__ : Int * Int)((var n : Int),

(var m : Int)) %(Int_geq_def)%,

. forall m, n, r, s:Int; a, b, c, d:Nat

. (pred __<__ : Int * Int)((var m : Int), (var n : Int)) <=>

(pred __<=__ : Int * Int)((var m : Int), (var n : Int))

/\ not (var m : Int) = (var n : Int) %(Int_less_def)%,

. forall m, n, r, s:Int; a, b, c, d:Nat

. (pred __>__ : Int * Int)((var m : Int), (var n : Int)) <=>

(pred __<__ : Int * Int)((var m : Int),

(var n : Int)) %(Int_greater_def)%,

. forall m, n, r, s:Int; a, b, c, d:Nat

. (op min : Int * Int -> Int)((var m : Int), (var n : Int)) =

(var m : Int)

when (pred __<=__ : Int * Int)((var m : Int), (var n : Int))

else (var n : Int) %(Int_min_def)%,

. forall m, n, r, s:Int; a, b, c, d:Nat

. (op max : Int * Int -> Int)((var m : Int), (var n : Int)) =

(var n : Int)

when (pred __<=__ : Int * Int)((var m : Int), (var n : Int))

else (var m : Int) %(Int_max_def)%,

. forall m, n, r, s:Int; a, b, c, d:Nat

. (op inj : Nat -> Int)((op abs : Int -> Nat)((var m : Int))) =

(op -__ : Int -> Int)((var m : Int)) if

(pred __<__ : Int * Int)((var m : Int),

(op inj : Nat -> Int)((op 0 : Nat))) %(Int_abs_def)%,

. forall m, n, r, s:Int; a, b, c, d:Nat

. (op __^__ : Int *

Nat -> Int)((op -__ : Int -> Int)((op inj : Pos -> Int)((op 1 : Pos))),

(var a : Nat)) =

(op inj : Pos -> Int)((op 1 : Pos))

when (pred even : Int)((op inj : Nat -> Int)((var a : Nat)))

else (op -__ : Int -> Int)((op inj : Pos -> Int)((op 1 : Pos))) %(Int_neg1_power_def)%,

. forall m, n, r, s:Int; a, b, c, d:Nat

. (op __^__ : Int * Nat -> Int)((var m : Int), (var a : Nat)) =

(op __*__ : Int * Int -> Int)((op __^__ : Int *

Nat -> Int)((op sign : Int -> Int)((var m : Int)),

(var a : Nat)),

(op inj : Nat -> Int)((op __^__ : Nat *

Nat -> Nat)((op abs : Int -> Nat)((var m : Int)),

(var a : Nat)))) %(Int_power_def)%,

. forall m, n, r, s:Int; a, b, c, d:Nat

. (pred even : Int)((var m : Int)) <=>

(pred even : Int)((op inj : Nat -> Int)((op abs : Int -> Nat)((var m : Int)))) %(Int_even_def)%,

. forall m, n, r, s:Int; a, b, c, d:Nat

. (pred odd : Int)((var m : Int)) <=>

not (pred even : Int)((var m : Int)) %(Int_odd_def)%,

. forall m, n, r, s:Int; a, b, c, d:Nat

. (op __/?__ : Int * Int ->? Int)((var m : Int), (var n : Int)) =

(op __*__ : Int * Int -> Int)((op __*__ : Int *

Int -> Int)((op sign : Int -> Int)((var m : Int)),

(op sign : Int -> Int)((var n : Int))),

(op inj : Nat -> Int)((op __/?__ : Nat *

Nat ->? Nat)((op abs : Int -> Nat)((var m : Int)),

(op abs : Int -> Nat)((var n : Int))))) %(Int_divide)%,

. forall m, n, r, s:Int; a, b, c, d:Nat

. (pred __<__ : Int *

Int)((op inj : Nat -> Int)((op __mod__ : Int *

Int ->? Nat)((var m : Int),

(var n : Int))),

(op inj : Nat -> Int)((op abs : Int -> Nat)((var n : Int)))) if

not (var n : Int) =

(op inj : Nat -> Int)((op 0 : Nat)) %(Int_mod_range)%,

. forall m, n, r, s:Int; a, b, c, d:Nat

. (var m : Int) =

(op __+__ : Int * Int -> Int)((op __*__ : Int *

Int -> Int)((op __div__ : Int *

Int ->? Int)((var m : Int),

(var n : Int)),

(var n : Int)),

(op inj : Nat -> Int)((op __mod__ : Int *

Int ->? Nat)((var m : Int),

(var n : Int)))) if

not (var n : Int) =

(op inj : Nat -> Int)((op 0 : Nat)) %(Int_mod__div_def)%,

. forall m, n, r, s:Int; a, b, c, d:Nat

. not def (op __mod__ : Int * Int ->? Nat)((var m : Int),

(op inj : Nat -> Int)((op 0 : Nat))) %(Int_mod_zero)%,

. forall m, n, r, s:Int; a, b, c, d:Nat

. not def (op __div__ : Int * Int ->? Int)((var m : Int),

(op inj : Nat -> Int)((op 0 : Nat))) %(Int_div_zero)%,

. forall m, n, r, s:Int; a, b, c, d:Nat

. (op __quot__ : Int * Int ->? Int)((var m : Int), (var n : Int)) =

(op __*__ : Int * Int -> Int)((op __*__ : Int *

Int -> Int)((op sign : Int -> Int)((var m : Int)),

(op sign : Int -> Int)((var n : Int))),

(op inj : Nat -> Int)((op __quot__ : Nat *

Nat ->? Nat)((op abs : Int -> Nat)((var m : Int)),

(op abs : Int -> Nat)((var n : Int))))) %(Int_quot_def)%,

. forall m, n, r, s:Int; a, b, c, d:Nat

. (op __rem__ : Int * Int ->? Int)((var m : Int), (var n : Int)) =

(op __*__ : Int * Int -> Int)((op __*__ : Int *

Int -> Int)((op sign : Int -> Int)((var m : Int)),

(op sign : Int -> Int)((var n : Int))),

(op inj : Nat -> Int)((op __rem__ : Nat *

Nat ->? Nat)((op abs : Int -> Nat)((var m : Int)),

(op abs : Int -> Nat)((var n : Int))))) %(Int_rem_def)%,

. forall m, n, r:Int; a, b:Nat

. def (op __-?__ : Nat * Nat ->? Nat)((var a : Nat),

(var b : Nat)) =>

(op inj : Nat -> Int)((op __-?__ : Nat *

Nat ->? Nat)((var a : Nat), (var b : Nat))) =

(op __-__ : Int * Int -> Int)((op inj : Nat -> Int)((var a : Nat)),

(op inj : Nat -> Int)((var b : Nat))) %(Int_Nat_sub_compat)%,

. forall m, n, r:Int; a, b:Nat

. (var m : Int) =

(op __*__ : Int *

Int -> Int)((op sign : Int -> Int)((var m : Int)),

(op inj : Nat -> Int)((op abs : Int -> Nat)((var m : Int)))) %(Int_abs_decomp)%,

. forall m, n, r:Int; a, b:Nat

. (pred odd : Int)((var m : Int)) <=>

(pred odd : Int)((op inj : Nat -> Int)((op abs : Int -> Nat)((var m : Int)))) %(Int_odd_alt)%,

. forall m, n, r:Int; a, b:Nat

. (op __/?__ : Int * Int ->? Int)((var m : Int), (var n : Int)) =

(var r : Int) <=>

not (var n : Int) = (op inj : Nat -> Int)((op 0 : Nat))

/\ (op __*__ : Int * Int -> Int)((var n : Int), (var r : Int)) =

(var n : Int) %(Int_divide_dom1)%,

. forall m, n, r:Int; a, b:Nat

. def (op __/?__ : Int * Int ->? Int)((var m : Int),

(var n : Int)) <=>

(op __mod__ : Int * Int ->? Nat)((var m : Int), (var n : Int)) =

(op 0 : Nat) %(Int_divide_dom2)%,

. forall m, n, r:Int; a, b:Nat

. def (op __mod__ : Int * Int ->? Nat)((var m : Int),

(var n : Int)) <=>

not (var n : Int) =

(op inj : Nat -> Int)((op 0 : Nat)) %(Int_mod_dom)%,

. forall m, n, r:Int; a, b:Nat

. (op __mod__ : Int * Int ->? Nat)((var m : Int), (var n : Int)) =

(op __mod__ : Int * Int ->? Nat)((var m : Int),

(op inj : Nat -> Int)((op abs : Int -> Nat)((var n : Int)))) %(Int_mod_abs)%,

. forall m, n, r:Int; a, b:Nat

. def (op __div__ : Int * Int ->? Int)((var m : Int),

(var n : Int)) <=>

not (var n : Int) =

(op inj : Nat -> Int)((op 0 : Nat)) %(Int_div_dom)%,

. forall m, n, r:Int; a, b:Nat

. def (op __quot__ : Int * Int ->? Int)((var m : Int),

(var n : Int)) <=>

not (var n : Int) =

(op inj : Nat -> Int)((op 0 : Nat)) %(Int_quot_dom)%,

. forall m, n, r:Int; a, b:Nat

. def (op __rem__ : Int * Int ->? Int)((var m : Int),

(var n : Int)) <=>

not (var n : Int) =

(op inj : Nat -> Int)((op 0 : Nat)) %(Int_rem_dom)%,

. forall m, n, r:Int; a, b:Nat

. (var m : Int) =

(op __+__ : Int * Int -> Int)((op __*__ : Int *

Int -> Int)((op __quot__ : Int *

Int ->? Int)((var m : Int),

(var n : Int)),

(var n : Int)),

(op __rem__ : Int * Int ->? Int)((var m : Int),

(var n : Int))) if

not (var n : Int) =

(op inj : Nat -> Int)((op 0 : Nat)) %(Int_quot_rem)%,

generated{sort Rat; op __/__ : Int *

Pos -> Rat} %(ga_generated_Rat)%,

. forall i, j:Int; p, q:Pos

. (op __/__ : Int * Pos -> Rat)((var i : Int), (var p : Pos)) =

(op __/__ : Int * Pos -> Rat)((var j : Int), (var q : Pos)) <=>

(op __*__ : Int * Int -> Int)((var i : Int),

(op inj : Pos -> Int)((var q : Pos))) =

(op __*__ : Int * Int -> Int)((var j : Int),

(op inj : Pos -> Int)((var p : Pos))) %(Rat_equality)%,

. forall i:Int

. (op __/__ : Int * Pos -> Rat)((var i : Int), (op 1 : Pos)) =

(op inj : Int -> Rat)((var i : Int)) %(embeddingIntToRat)%,

. forall p, q:Pos; n:Nat; i, j:Int; x, y, z:Rat

. (pred __<=__ : Rat * Rat)((op __/__ : Int *

Pos -> Rat)((var i : Int), (var p : Pos)),

(op __/__ : Int * Pos -> Rat)((var j : Int),

(var q : Pos))) <=>

(pred __<=__ : Int * Int)((op __*__ : Int *

Int -> Int)((var i : Int),

(op inj : Pos -> Int)((var q : Pos))),

(op __*__ : Int * Int -> Int)((var j : Int),

(op inj : Pos -> Int)((var p : Pos)))) %(Rat_leq_def)%,

. forall p, q:Pos; n:Nat; i, j:Int; x, y, z:Rat

. (pred __>=__ : Rat * Rat)((var x : Rat), (var y : Rat)) <=>

(pred __<=__ : Rat * Rat)((var y : Rat),

(var x : Rat)) %(Rat_geq_def)%,

. forall p, q:Pos; n:Nat; i, j:Int; x, y, z:Rat

. (pred __>__ : Rat * Rat)((var x : Rat), (var y : Rat)) <=>

(pred __<__ : Rat * Rat)((var y : Rat),

(var x : Rat)) %(Rat_greater_def)%,

. forall p, q:Pos; n:Nat; i, j:Int; x, y, z:Rat

. (op __+__ : Rat * Rat -> Rat)((op __/__ : Int *

Pos -> Rat)((var i : Int), (var p : Pos)),

(op __/__ : Int * Pos -> Rat)((var j : Int),

(var q : Pos))) =

(op __/__ : Int * Pos -> Rat)((op __+__ : Int *

Int -> Int)((op __*__ : Int *

Int -> Int)((var i : Int),

(op inj : Pos -> Int)((var q : Pos))),

(op __*__ : Int *

Int -> Int)((var j : Int),

(op inj : Pos -> Int)((var p : Pos)))),

(op __*__ : Pos * Pos -> Pos)((var p : Pos),

(var q : Pos))) %(Rat_add_def)%,

. forall p, q:Pos; n:Nat; i, j:Int; x, y, z:Rat

. (op __-__ : Rat * Rat -> Rat)((var x : Rat), (var y : Rat)) =

(op __+__ : Rat * Rat -> Rat)((var x : Rat),

(op -__ : Rat -> Rat)((var y : Rat))) %(Rat_sub_def)%,

. forall p, q:Pos; n:Nat; i, j:Int; x, y, z:Rat

. (op __*__ : Rat * Rat -> Rat)((op __/__ : Int *

Pos -> Rat)((var i : Int), (var p : Pos)),

(op __/__ : Int * Pos -> Rat)((var j : Int),

(var q : Pos))) =

(op __/__ : Int * Pos -> Rat)((op __*__ : Int *

Int -> Int)((var i : Int), (var j : Int)),

(op __*__ : Pos * Pos -> Pos)((var p : Pos),

(var q : Pos))) %(Rat_mult_def)%,

. forall p, q:Pos; n:Nat; i, j:Int; x, y, z:Rat

. not def (op __/__ : Rat * Rat ->? Rat)((var x : Rat),

(op inj : Nat -> Rat)((op 0 : Nat))) %(Rat_divide_def1)%,

. forall p, q:Pos; n:Nat; i, j:Int; x, y, z:Rat

. (op +__ : Rat -> Rat)((var x : Rat)) =

(var x : Rat) %(Rat_plus_def)%,

. forall p, q:Pos; n:Nat; i, j:Int; x, y, z:Rat

. (op -__ : Rat -> Rat)((op __/__ : Int *

Pos -> Rat)((var i : Int), (var p : Pos))) =

(op __/__ : Int * Pos -> Rat)((op -__ : Int -> Int)((var i : Int)),

(var p : Pos)) %(Rat_minus_def)%,

. forall p, q:Pos; n:Nat; i, j:Int; x, y, z:Rat

. (op abs : Rat -> Rat)((op __/__ : Int *

Pos -> Rat)((var i : Int), (var p : Pos))) =

(op __/__ : Int *

Pos -> Rat)((op inj : Nat -> Int)((op abs : Int -> Nat)((var i : Int))),

(var p : Pos)) %(Rat_abs_def)%,

. forall p, q:Pos; n:Nat; i, j:Int; x, y, z:Rat

. (op __^__ : Rat * Int -> Rat)((var x : Rat),

(op inj : Nat -> Int)((op 0 : Nat))) =

(op inj : Pos -> Rat)((op 1 : Pos)) %(Rat_power_0)%,

. forall p, q:Pos; n:Nat; i, j:Int; x, y, z:Rat

. (op __^__ : Rat * Int -> Rat)((var x : Rat),

(op inj : Pos -> Int)((op suc : Nat -> Pos)((var n : Nat)))) =

(op __*__ : Rat * Rat -> Rat)((var x : Rat),

(op __^__ : Rat * Int -> Rat)((var x : Rat),

(op inj : Nat -> Int)((var n : Nat)))) %(Rat_power_suc)%,

. forall p, q:Pos; n:Nat; i, j:Int; x, y, z:Rat

. (op __^__ : Rat * Int -> Rat)((var x : Rat),

(op -__ : Int -> Int)((op inj : Pos -> Int)((var p : Pos)))) =

(op __/__ : Rat * Rat ->? Rat)((op inj : Pos -> Rat)((op 1 : Pos)),

(op __^__ : Rat * Int -> Rat)((var x : Rat),

(op inj : Pos -> Int)((var p : Pos)))) %(Rat_power_neg)%,

. forall p, q:Pos; n:Nat; i, j:Int; x, y, z:Rat

. (op min : Rat * Rat -> Rat)((var x : Rat), (var y : Rat)) =

(var x : Rat)

when (pred __<=__ : Rat * Rat)((var x : Rat), (var y : Rat))

else (var y : Rat) %(Rat_min_def)%,

. forall p, q:Pos; n:Nat; i, j:Int; x, y, z:Rat

. (op max : Rat * Rat -> Rat)((var x : Rat), (var y : Rat)) =

(var y : Rat)

when (pred __<=__ : Rat * Rat)((var x : Rat), (var y : Rat))

else (var x : Rat) %(Rat_max_def)%,

. forall i, j:Int; p, q:Pos

. (op __/__ : Rat * Rat ->? Rat)((op __/__ : Int *

Pos -> Rat)((var i : Int), (var p : Pos)),

(op __/__ : Int * Pos -> Rat)((var j : Int),

(var q : Pos))) =

(op __*__ : Rat * Rat -> Rat)((op __/__ : Int *

Pos -> Rat)((var i : Int), (var p : Pos)),

(op __/__ : Rat *

Rat ->? Rat)((op inj : Pos -> Rat)((var q : Pos)),

(op inj : Int -> Rat)((var j : Int)))) if

not (var j : Int) =

(op inj : Nat -> Int)((op 0 : Nat)) %(Rat_divide_rule)%,

. forall X1:a; X2:t; X3:t; X4:t; X5:t

. (op a : s -> t)((op c : a * t * t * t * t -> s)((var X1 : a),

(var X2 : t), (var X3 : t), (var X4 : t),

(var X5 : t))) =

(var X2 : t) %(ga_selector_a)%,

. forall X1:a; X2:t; X3:t; X4:t; X5:t

. (op b : s -> t)((op c : a * t * t * t * t -> s)((var X1 : a),

(var X2 : t), (var X3 : t), (var X4 : t),

(var X5 : t))) =

(var X3 : t) %(ga_selector_b)%,

. forall X1:a; X2:t; X3:t; X4:t; X5:t

. (op a : s -> t)((op c : a * t * t * t * t -> s)((var X1 : a),

(var X2 : t), (var X3 : t), (var X4 : t),

(var X5 : t))) =

(var X4 : t) %(ga_selector_a)%,

. forall X1:a; X2:t; X3:t; X4:t; X5:t

. (op d : s -> t)((op c : a * t * t * t * t -> s)((var X1 : a),

(var X2 : t), (var X3 : t), (var X4 : t),

(var X5 : t))) =

(var X5 : t) %(ga_selector_d)%,

. forall X1:a; X2:t; X3:t; X4:t

. (op a : s -> t)((op c : a * t * t * t -> s)((var X1 : a),

(var X2 : t), (var X3 : t), (var X4 : t))) =

(var X2 : t) %(ga_selector_a)%,

. forall X1:a; X2:t; X3:t; X4:t

. (op b : s -> t)((op c : a * t * t * t -> s)((var X1 : a),

(var X2 : t), (var X3 : t), (var X4 : t))) =

(var X3 : t) %(ga_selector_b)%,

. forall X1:a; X2:t; X3:t; X4:t

. (op d : s -> t)((op c : a * t * t * t -> s)((var X1 : a),

(var X2 : t), (var X3 : t), (var X4 : t))) =

(var X4 : t) %(ga_selector_d)%,

. forall X1:a; X2:t; X3:t; X4:t; Y1:a; Y2:t; Y3:t; Y4:t

. (op c : a * t * t * t -> s)((var X1 : a), (var X2 : t),

(var X3 : t), (var X4 : t)) =

(op c : a * t * t * t -> s)((var Y1 : a), (var Y2 : t),

(var Y3 : t), (var Y4 : t)) <=>

(var X1 : a) = (var Y1 : a)

/\ (var X2 : t) = (var Y2 : t)

/\ (var X3 : t) = (var Y3 : t)

/\ (var X4 : t) = (var Y4 : t) %(ga_injective_c)%,

. forall X1:a; Y1:a

. (op c : a ->? s)((var X1 : a)) =

(op c : a ->? s)((var Y1 : a)) <=>

(var X1 : a) = (var Y1 : a) %(ga_injective_c)%,

. not (op c : s) in s2 %(ga_disjoint_c_sort_s2)%,

. not (op c : s) in s1 %(ga_disjoint_c_sort_s1)%,

. forall X1:a; X2:t; X3:t; X4:t

. not (op c : a * t * t * t -> s)((var X1 : a), (var X2 : t),

(var X3 : t),

(var X4 : t)) in s2 %(ga_disjoint_c_sort_s2)%,

. forall X1:a; X2:t; X3:t; X4:t

. not (op c : a * t * t * t -> s)((var X1 : a), (var X2 : t),

(var X3 : t),

(var X4 : t)) in s1 %(ga_disjoint_c_sort_s1)%,

. forall X1:a

. not (op c : a ->? s)((var X1 : a)) in s2 %(ga_disjoint_c_sort_s2)%,

. forall X1:a

. not (op c : a ->? s)((var X1 : a)) in s1 %(ga_disjoint_c_sort_s1)%,

. forall Y1:a; Y2:t; Y3:t; Y4:t

. not (op c : s) =

(op c : a * t * t * t -> s)((var Y1 : a), (var Y2 : t),

(var Y3 : t), (var Y4 : t)) %(ga_disjoint_c_c)%,

. forall Y1:a

. not (op c : s) =

(op c : a ->? s)((var Y1 : a)) %(ga_disjoint_c_c)%,

. forall X1:a; X2:t; X3:t; X4:t; Y1:a

. not (op c : a * t * t * t -> s)((var X1 : a), (var X2 : t),

(var X3 : t), (var X4 : t)) =

(op c : a ->? s)((var Y1 : a)) %(ga_disjoint_c_c)%,

. not def (op a : s -> t)((op c : s)) %(ga_selector_undef_a_c)%,

. forall X1:a

. not def (op a : s -> t)((op c : a ->? s)((var X1 : a))) %(ga_selector_undef_a_c)%,

. not def (op b : s -> t)((op c : s)) %(ga_selector_undef_b_c)%,

. forall X1:a

. not def (op b : s -> t)((op c : a ->? s)((var X1 : a))) %(ga_selector_undef_b_c)%,

. not def (op d : s -> t)((op c : s)) %(ga_selector_undef_d_c)%,

. forall X1:a

. not def (op d : s -> t)((op c : a ->? s)((var X1 : a))) %(ga_selector_undef_d_c)%,

generated{sort s; op c : s; op c : a ->? s;

op c : a * t * t * t -> s; op inj : s1 -> s;

op inj : s2 -> s} %(ga_generated_s)%,

. forall X1:a; X2:t; X3:t; X4:t

. (op a : s -> t)((op c : a * t * t * t -> s)((var X1 : a),

(var X2 : t), (var X3 : t), (var X4 : t))) =

(var X2 : t) %(ga_selector_a)%,

. forall X1:a; X2:t; X3:t; X4:t

. (op b : s -> t)((op c : a * t * t * t -> s)((var X1 : a),

(var X2 : t), (var X3 : t), (var X4 : t))) =

(var X3 : t) %(ga_selector_b)%,

. forall X1:a; X2:t; X3:t; X4:t

. (op d : s -> t)((op c : a * t * t * t -> s)((var X1 : a),

(var X2 : t), (var X3 : t), (var X4 : t))) =

(var X4 : t) %(ga_selector_d)%,

generated{sort s; op c : s; op c : a ->? s;

op c : a * t * t * t -> s; op inj : s1 -> s;

op inj : s2 -> s} %(ga_generated_s)%,

. forall X1:a; X2:t; X3:t; X4:t

. (op a : s -> t)((op c : a * t * t * t -> s)((var X1 : a),

(var X2 : t), (var X3 : t), (var X4 : t))) =

(var X2 : t) %(ga_selector_a)%,

. forall X1:a; X2:t; X3:t; X4:t

. (op b : s -> t)((op c : a * t * t * t -> s)((var X1 : a),

(var X2 : t), (var X3 : t), (var X4 : t))) =

(var X3 : t) %(ga_selector_b)%,

. forall X1:a; X2:t; X3:t; X4:t

. (op d : s -> t)((op c : a * t * t * t -> s)((var X1 : a),

(var X2 : t), (var X3 : t), (var X4 : t))) =

(var X4 : t) %(ga_selector_d)%,

generated{sort s, t; op c : s; op c : a ->? s;

op c : a * t * t * t -> s; op inj : s1 -> s;

op inj : s2 -> s} %(ga_generated_s_t)%,

. true %(The true formula)%, . true %(and this)%,

. forall x:b . (var x : b) in a <=> true,

. forall x:s; y:s; z:s

. (op c : s * s -> s)((var x : s),

(op c : s * s -> s)((var y : s), (var z : s))) =

(op c : s * s -> s)((op c : s * s -> s)((var x : s), (var y : s)),

(var z : s)) %(ga_assoc_c)%,

. forall x:s; y:s

. (op c : s * s -> s)((var x : s), (var y : s)) =

(op c : s * s -> s)((var y : s), (var x : s)) %(ga_comm_c)%,

. forall x:s

. (op c : s * s -> s)((var x : s), (var x : s)) =

(var x : s) %(ga_idem_c)%,

. forall x:s; y:s; z:s

. (op c : s * s ->? s)((var x : s),

(op c : s * s ->? s)((var y : s), (var z : s))) =

(op c : s * s ->? s)((op c : s * s ->? s)((var x : s),

(var y : s)),

(var z : s)) %(ga_assoc_c)%,

. forall x:s; y:s

. (op c : s * s ->? s)((var x : s), (var y : s)) =

(op c : s * s ->? s)((var y : s), (var x : s)) %(ga_comm_c)%,

. forall x:s

. (op c : s * s ->? s)((var x : s), (var x : s)) =

(var x : s) %(ga_idem_c)%,

. forall x, y:s; z:t

. (pred c : s * s * t)((var x : s), (var y : s), (var z : t)) <=>

false,

. forall X1:Data1; X2:Data2

. (op sel1 : Data3 ->? Data1)((op Cons31 : Data1 *

Data2 -> Data3)((var X1 : Data1),

(var X2 : Data2))) =

(var X1 : Data1) %(ga_selector_sel1)%,

. forall X1:Data1; X2:Data2

. (op sel2 : Data3 ->? Data2)((op Cons31 : Data1 *

Data2 -> Data3)((var X1 : Data1),

(var X2 : Data2))) =

(var X2 : Data2) %(ga_selector_sel2)%,

. forall X1:Data2; X2:Data1

. (op sel2 : Data3 ->? Data2)((op Cons32 : Data2 *

Data1 -> Data3)((var X1 : Data2),

(var X2 : Data1))) =

(var X1 : Data2) %(ga_selector_sel2)%,

. forall X1:Data2; X2:Data1

. (op sel1 : Data3 ->? Data1)((op Cons32 : Data2 *

Data1 -> Data3)((var X1 : Data2),

(var X2 : Data1))) =

(var X2 : Data1) %(ga_selector_sel1)%,

. forall X1:Data1; X2:Data2

. (op sel1 : Data4 ->? Data1)((op Cons41 : Data1 *

Data2 ->? Data4)((var X1 : Data1),

(var X2 : Data2))) =

(var X1 : Data1) %(ga_selector_sel1)%,

. forall X1:Data1; X2:Data2

. (op sel2 : Data4 ->? Data2)((op Cons41 : Data1 *

Data2 ->? Data4)((var X1 : Data1),

(var X2 : Data2))) =

(var X2 : Data2) %(ga_selector_sel2)%,

. forall X1:Data2; X2:Data1

. (op sel2 : Data4 ->? Data2)((op Cons42 : Data2 *

Data1 ->? Data4)((var X1 : Data2),

(var X2 : Data1))) =

(var X1 : Data2) %(ga_selector_sel2)%,

. forall X1:Data2; X2:Data1

. (op sel1 : Data4 ->? Data1)((op Cons42 : Data2 *

Data1 ->? Data4)((var X1 : Data2),

(var X2 : Data1))) =

(var X2 : Data1) %(ga_selector_sel1)%,

. forall X1:Data1; X2:List; Y1:Data1; Y2:List

. (op Cons : Data1 * List -> List)((var X1 : Data1),

(var X2 : List)) =

(op Cons : Data1 * List -> List)((var Y1 : Data1),

(var Y2 : List)) <=>

(var X1 : Data1) = (var Y1 : Data1)

/\ (var X2 : List) = (var Y2 : List) %(ga_injective_Cons)%,

. forall Y1:Data1; Y2:List

. not (op Nil : List) =

(op Cons : Data1 * List -> List)((var Y1 : Data1),

(var Y2 : List)) %(ga_disjoint_Nil_Cons)%,

generated{sort List; op Cons : Data1 * List -> List;

op Nil : List} %(ga_generated_List)%,

generated{sort Set; op Add : Data1 * Set -> Set;

op Mt : Set} %(ga_generated_Set)%,

generated{sort Set; op Add : Data1 * Set -> Set;

op Mt : Set} %(ga_generated_Set)%,

generated{sort nat; op 0 : nat;

op succ : nat -> nat} %(ga_generated_nat)%,

. false, . true,

. not (pred p : ())

/\ not (pred q : s)((var x : s))

/\ (pred q : s)((var x : s)),

. not (pred p : ())

\/ not (pred q : s)((var x : s))

\/ (pred q : s)((var x : s)),

. not (pred p : ())

/\ not (pred q : s)((var x : s))

/\ (pred q : s)((var x : s)) =>

not (pred p : ())

\/ not (pred q : s)((var x : s))

\/ (pred q : s)((var x : s)) =>

not (pred p : ())

/\ not (pred q : s)((var x : s))

/\ (pred q : s)((var x : s)),

. not (pred p : ())

/\ not (pred q : s)((var x : s))

/\ (pred q : s)((var x : s)) if

not (pred p : ())

\/ not (pred q : s)((var x : s))

\/ (pred q : s)((var x : s)) if

not (pred p : ())

/\ not (pred q : s)((var x : s))

/\ (pred q : s)((var x : s)),

. forall x:s

. not (pred p : ())

/\ not (pred q : s)((var x : s))

/\ (pred q : s)((var x : s)) <=>

(exists x:s

. not (pred p : ())

\/ not (pred q : s)((var x : s))

\/ (pred q : s)((var x : s)) <=>

(exists! x:s

. not (pred p : ())

/\ not (pred q : s)((var x : s))

/\ (pred q : s)((var x : s)))),

. forall x:s . def (op f : s ->? s)((var x : s)),

. forall x:s

. (op f : s ->? s)((var x : s)) =e=

(op inj : t -> s)((op g : s -> t)((var x : s))),

. forall x:s

. (op f : s ->? s)((var x : s)) =

(op inj : t -> s)((op g : s -> t)((var x : s))),

. forall x:s . (var r1 : t) in s,

. forall x:s . def (op g : s -> t)((var x : s)),

. forall x:s . def (op g : s -> t)((var x : s)) as s,

. forall x:s . def (op f : s ->? s)((var x : s)),

. forall x:s . def (op g : s -> t)((var x : s)),

. forall x:s . (pred p : ()),

. forall x:s . (pred q : s)((var x : s)),

. forall x:s

. def (op __+__ : s * s -> s)((op __*__ : s *

s -> s)((op __*__ : s * s -> s)((var x : s),

(var y : s)),

(var z : s)),

(op __*__ : s * s -> s)((op __*__ : s * s -> s)((var z : s),

(var y : s)),

(var x : s))),

. forall x:s . def (op {} : s),

. forall x:s . def (op {__} : s -> s)((var x : s)), . true,

. not (op True : Boolean) =

(op False : Boolean) %(ga_disjoint_True_False)%,

generated{sort Boolean; op False : Boolean;

op True : Boolean} %(ga_generated_Boolean)%,

. forall x, y, z:Boolean

. (op Not__ : Boolean -> Boolean)((op False : Boolean)) =

(op True : Boolean) %(Not_False)%,

. forall x, y, z:Boolean

. (op Not__ : Boolean -> Boolean)((op True : Boolean)) =

(op False : Boolean) %(Not_True)%,

. forall x, y, z:Boolean

. (op __And__ : Boolean * Boolean -> Boolean)((op False : Boolean),

(op False : Boolean)) =

(op False : Boolean) %(And_def1)%,

. forall x, y, z:Boolean

. (op __And__ : Boolean * Boolean -> Boolean)((op False : Boolean),

(op True : Boolean)) =

(op False : Boolean) %(And_def2)%,

. forall x, y, z:Boolean

. (op __And__ : Boolean * Boolean -> Boolean)((op True : Boolean),

(op False : Boolean)) =

(op False : Boolean) %(And_def3)%,

. forall x, y, z:Boolean

. (op __And__ : Boolean * Boolean -> Boolean)((op True : Boolean),

(op True : Boolean)) =

(op True : Boolean) %(And_def4)%,

. forall x, y, z:Boolean

. (op __Or__ : Boolean * Boolean -> Boolean)((var x : Boolean),

(var y : Boolean)) =

(op Not__ : Boolean -> Boolean)((op __And__ : Boolean *

Boolean -> Boolean)((op Not__ : Boolean -> Boolean)((var x : Boolean)),

(op Not__ : Boolean -> Boolean)((var y : Boolean)))) %(Or_def)%,

. forall n:Nat; c:Char

. def (op chr : Nat ->? Char)((var n : Nat)) <=>

(pred __<=__ : Int * Int)((op inj : Nat -> Int)((var n : Nat)),

(op inj : Nat -> Int)((op __@@__ : Nat *

Nat -> Nat)((op 2 : Nat),

(op __@@__ : Nat *

Nat -> Nat)((op 5 : Nat),

(op 5 : Nat))))) %(chr_dom)%,

. forall n:Nat; c:Char

. (op chr : Nat ->? Char)((op ord : Char -> Nat)((var c : Char))) =

(var c : Char) %(chr_def)%,

. forall n:Nat; c:Char

. (op ord : Char -> Nat)((op chr : Nat ->? Char)((var n : Nat))) =

(var n : Nat) if

(pred __<=__ : Int * Int)((op inj : Nat -> Int)((var n : Nat)),

(op inj : Nat -> Int)((op __@@__ : Nat *

Nat -> Nat)((op 2 : Nat),

(op __@@__ : Nat *

Nat -> Nat)((op 5 : Nat),

(op 5 : Nat))))) %(ord_def)%,

. (op '\000' : Char) =

(op chr : Nat ->? Char)((op 0 : Nat)) %(slash_000)%,

. (op '\001' : Char) =

(op chr : Nat ->? Char)((op inj : Pos -> Nat)((op 1 : Pos))) %(slash_001)%,

. (op '\002' : Char) =

(op chr : Nat ->? Char)((op 2 : Nat)) %(slash_002)%,

. (op '\003' : Char) =

(op chr : Nat ->? Char)((op 3 : Nat)) %(slash_003)%,

. (op '\004' : Char) =

(op chr : Nat ->? Char)((op 4 : Nat)) %(slash_004)%,

. (op '\005' : Char) =

(op chr : Nat ->? Char)((op 5 : Nat)) %(slash_005)%,

. (op '\006' : Char) =

(op chr : Nat ->? Char)((op 6 : Nat)) %(slash_006)%,

. (op '\007' : Char) =

(op chr : Nat ->? Char)((op 7 : Nat)) %(slash_007)%,

. (op '\008' : Char) =

(op chr : Nat ->? Char)((op 8 : Nat)) %(slash_008)%,

. (op '\009' : Char) =

(op chr : Nat ->? Char)((op 9 : Nat)) %(slash_009)%,

. (op '\010' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op inj : Pos -> Nat)((op 1 : Pos)),

(op 0 : Nat))) %(slash_010)%,

. (op '\011' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op inj : Pos -> Nat)((op 1 : Pos)),

(op inj : Pos -> Nat)((op 1 : Pos)))) %(slash_011)%,

. (op '\012' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op inj : Pos -> Nat)((op 1 : Pos)),

(op 2 : Nat))) %(slash_012)%,

. (op '\013' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op inj : Pos -> Nat)((op 1 : Pos)),

(op 3 : Nat))) %(slash_013)%,

. (op '\014' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op inj : Pos -> Nat)((op 1 : Pos)),

(op 4 : Nat))) %(slash_014)%,

. (op '\015' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op inj : Pos -> Nat)((op 1 : Pos)),

(op 5 : Nat))) %(slash_015)%,

. (op '\016' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op inj : Pos -> Nat)((op 1 : Pos)),

(op 6 : Nat))) %(slash_016)%,

. (op '\017' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op inj : Pos -> Nat)((op 1 : Pos)),

(op 7 : Nat))) %(slash_017)%,

. (op '\018' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op inj : Pos -> Nat)((op 1 : Pos)),

(op 8 : Nat))) %(slash_018)%,

. (op '\019' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op inj : Pos -> Nat)((op 1 : Pos)),

(op 9 : Nat))) %(slash_019)%,

. (op '\020' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op 2 : Nat),

(op 0 : Nat))) %(slash_020)%,

. (op '\021' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op 2 : Nat),

(op inj : Pos -> Nat)((op 1 : Pos)))) %(slash_021)%,

. (op '\022' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op 2 : Nat),

(op 2 : Nat))) %(slash_022)%,

. (op '\023' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op 2 : Nat),

(op 3 : Nat))) %(slash_023)%,

. (op '\024' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op 2 : Nat),

(op 4 : Nat))) %(slash_024)%,

. (op '\025' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op 2 : Nat),

(op 5 : Nat))) %(slash_025)%,

. (op '\026' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op 2 : Nat),

(op 6 : Nat))) %(slash_026)%,

. (op '\027' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op 2 : Nat),

(op 7 : Nat))) %(slash_027)%,

. (op '\028' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op 2 : Nat),

(op 8 : Nat))) %(slash_028)%,

. (op '\029' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op 2 : Nat),

(op 9 : Nat))) %(slash_029)%,

. (op '\030' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op 3 : Nat),

(op 0 : Nat))) %(slash_030)%,

. (op '\031' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op 3 : Nat),

(op inj : Pos -> Nat)((op 1 : Pos)))) %(slash_031)%,

. (op '\032' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op 3 : Nat),

(op 2 : Nat))) %(slash_032)%,

. (op '\033' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op 3 : Nat),

(op 3 : Nat))) %(slash_033)%,

. (op '\034' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op 3 : Nat),

(op 4 : Nat))) %(slash_034)%,

. (op '\035' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op 3 : Nat),

(op 5 : Nat))) %(slash_035)%,

. (op '\036' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op 3 : Nat),

(op 6 : Nat))) %(slash_036)%,

. (op '\037' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op 3 : Nat),

(op 7 : Nat))) %(slash_037)%,

. (op '\038' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op 3 : Nat),

(op 8 : Nat))) %(slash_038)%,

. (op '\039' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op 3 : Nat),

(op 9 : Nat))) %(slash_039)%,

. (op '\040' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op 4 : Nat),

(op 0 : Nat))) %(slash_040)%,

. (op '\041' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op 4 : Nat),

(op inj : Pos -> Nat)((op 1 : Pos)))) %(slash_041)%,

. (op '\042' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op 4 : Nat),

(op 2 : Nat))) %(slash_042)%,

. (op '\043' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op 4 : Nat),

(op 3 : Nat))) %(slash_043)%,

. (op '\044' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op 4 : Nat),

(op 4 : Nat))) %(slash_044)%,

. (op '\045' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op 4 : Nat),

(op 5 : Nat))) %(slash_045)%,

. (op '\046' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op 4 : Nat),

(op 6 : Nat))) %(slash_046)%,

. (op '\047' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op 4 : Nat),

(op 7 : Nat))) %(slash_047)%,

. (op '\048' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op 4 : Nat),

(op 8 : Nat))) %(slash_048)%,

. (op '\049' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op 4 : Nat),

(op 9 : Nat))) %(slash_049)%,

. (op '\050' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op 5 : Nat),

(op 0 : Nat))) %(slash_050)%,

. (op '\051' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op 5 : Nat),

(op inj : Pos -> Nat)((op 1 : Pos)))) %(slash_051)%,

. (op '\052' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op 5 : Nat),

(op 2 : Nat))) %(slash_052)%,

. (op '\053' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op 5 : Nat),

(op 3 : Nat))) %(slash_053)%,

. (op '\054' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op 5 : Nat),

(op 4 : Nat))) %(slash_054)%,

. (op '\055' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op 5 : Nat),

(op 5 : Nat))) %(slash_055)%,

. (op '\056' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op 5 : Nat),

(op 6 : Nat))) %(slash_056)%,

. (op '\057' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op 5 : Nat),

(op 7 : Nat))) %(slash_057)%,

. (op '\058' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op 5 : Nat),

(op 8 : Nat))) %(slash_058)%,

. (op '\059' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op 5 : Nat),

(op 9 : Nat))) %(slash_059)%,

. (op '\060' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op 6 : Nat),

(op 0 : Nat))) %(slash_060)%,

. (op '\061' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op 6 : Nat),

(op inj : Pos -> Nat)((op 1 : Pos)))) %(slash_061)%,

. (op '\062' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op 6 : Nat),

(op 2 : Nat))) %(slash_062)%,

. (op '\063' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op 6 : Nat),

(op 3 : Nat))) %(slash_063)%,

. (op '\064' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op 6 : Nat),

(op 4 : Nat))) %(slash_064)%,

. (op '\065' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op 6 : Nat),

(op 5 : Nat))) %(slash_065)%,

. (op '\066' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op 6 : Nat),

(op 6 : Nat))) %(slash_066)%,

. (op '\067' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op 6 : Nat),

(op 7 : Nat))) %(slash_067)%,

. (op '\068' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op 6 : Nat),

(op 8 : Nat))) %(slash_068)%,

. (op '\069' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op 6 : Nat),

(op 9 : Nat))) %(slash_069)%,

. (op '\070' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op 7 : Nat),

(op 0 : Nat))) %(slash_070)%,

. (op '\071' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op 7 : Nat),

(op inj : Pos -> Nat)((op 1 : Pos)))) %(slash_071)%,

. (op '\072' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op 7 : Nat),

(op 2 : Nat))) %(slash_072)%,

. (op '\073' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op 7 : Nat),

(op 3 : Nat))) %(slash_073)%,

. (op '\074' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op 7 : Nat),

(op 4 : Nat))) %(slash_074)%,

. (op '\075' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op 7 : Nat),

(op 5 : Nat))) %(slash_075)%,

. (op '\076' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op 7 : Nat),

(op 6 : Nat))) %(slash_076)%,

. (op '\077' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op 7 : Nat),

(op 7 : Nat))) %(slash_077)%,

. (op '\078' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op 7 : Nat),

(op 8 : Nat))) %(slash_078)%,

. (op '\079' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op 7 : Nat),

(op 9 : Nat))) %(slash_079)%,

. (op '\080' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op 8 : Nat),

(op 0 : Nat))) %(slash_080)%,

. (op '\081' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op 8 : Nat),

(op inj : Pos -> Nat)((op 1 : Pos)))) %(slash_081)%,

. (op '\082' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op 8 : Nat),

(op 2 : Nat))) %(slash_082)%,

. (op '\083' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op 8 : Nat),

(op 3 : Nat))) %(slash_083)%,

. (op '\084' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op 8 : Nat),

(op 4 : Nat))) %(slash_084)%,

. (op '\085' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op 8 : Nat),

(op 5 : Nat))) %(slash_085)%,

. (op '\086' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op 8 : Nat),

(op 6 : Nat))) %(slash_086)%,

. (op '\087' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op 8 : Nat),

(op 7 : Nat))) %(slash_087)%,

. (op '\088' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op 8 : Nat),

(op 8 : Nat))) %(slash_088)%,

. (op '\089' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op 8 : Nat),

(op 9 : Nat))) %(slash_089)%,

. (op '\090' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op 9 : Nat),

(op 0 : Nat))) %(slash_090)%,

. (op '\091' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op 9 : Nat),

(op inj : Pos -> Nat)((op 1 : Pos)))) %(slash_091)%,

. (op '\092' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op 9 : Nat),

(op 2 : Nat))) %(slash_092)%,

. (op '\093' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op 9 : Nat),

(op 3 : Nat))) %(slash_093)%,

. (op '\094' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op 9 : Nat),

(op 4 : Nat))) %(slash_094)%,

. (op '\095' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op 9 : Nat),

(op 5 : Nat))) %(slash_095)%,

. (op '\096' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op 9 : Nat),

(op 6 : Nat))) %(slash_096)%,

. (op '\097' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op 9 : Nat),

(op 7 : Nat))) %(slash_097)%,

. (op '\098' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op 9 : Nat),

(op 8 : Nat))) %(slash_098)%,

. (op '\099' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op 9 : Nat),

(op 9 : Nat))) %(slash_099)%,

. (op '\100' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op inj : Pos -> Nat)((op 1 : Pos)),

(op __@@__ : Nat *

Nat -> Nat)((op 0 : Nat),

(op 0 : Nat)))) %(slash_100)%,

. (op '\101' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op inj : Pos -> Nat)((op 1 : Pos)),

(op __@@__ : Nat *

Nat -> Nat)((op 0 : Nat),

(op inj : Pos -> Nat)((op 1 : Pos))))) %(slash_101)%,

. (op '\102' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op inj : Pos -> Nat)((op 1 : Pos)),

(op __@@__ : Nat *

Nat -> Nat)((op 0 : Nat),

(op 2 : Nat)))) %(slash_102)%,

. (op '\103' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op inj : Pos -> Nat)((op 1 : Pos)),

(op __@@__ : Nat *

Nat -> Nat)((op 0 : Nat),

(op 3 : Nat)))) %(slash_103)%,

. (op '\104' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op inj : Pos -> Nat)((op 1 : Pos)),

(op __@@__ : Nat *

Nat -> Nat)((op 0 : Nat),

(op 4 : Nat)))) %(slash_104)%,

. (op '\105' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op inj : Pos -> Nat)((op 1 : Pos)),

(op __@@__ : Nat *

Nat -> Nat)((op 0 : Nat),

(op 5 : Nat)))) %(slash_105)%,

. (op '\106' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op inj : Pos -> Nat)((op 1 : Pos)),

(op __@@__ : Nat *

Nat -> Nat)((op 0 : Nat),

(op 6 : Nat)))) %(slash_106)%,

. (op '\107' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op inj : Pos -> Nat)((op 1 : Pos)),

(op __@@__ : Nat *

Nat -> Nat)((op 0 : Nat),

(op 7 : Nat)))) %(slash_107)%,

. (op '\108' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op inj : Pos -> Nat)((op 1 : Pos)),

(op __@@__ : Nat *

Nat -> Nat)((op 0 : Nat),

(op 8 : Nat)))) %(slash_108)%,

. (op '\109' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op inj : Pos -> Nat)((op 1 : Pos)),

(op __@@__ : Nat *

Nat -> Nat)((op 0 : Nat),

(op 9 : Nat)))) %(slash_109)%,

. (op '\110' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op inj : Pos -> Nat)((op 1 : Pos)),

(op __@@__ : Nat *

Nat -> Nat)((op inj : Pos -> Nat)((op 1 : Pos)),

(op 0 : Nat)))) %(slash_110)%,

. (op '\111' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op inj : Pos -> Nat)((op 1 : Pos)),

(op __@@__ : Nat *

Nat -> Nat)((op inj : Pos -> Nat)((op 1 : Pos)),

(op inj : Pos -> Nat)((op 1 : Pos))))) %(slash_111)%,

. (op '\112' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op inj : Pos -> Nat)((op 1 : Pos)),

(op __@@__ : Nat *

Nat -> Nat)((op inj : Pos -> Nat)((op 1 : Pos)),

(op 2 : Nat)))) %(slash_112)%,

. (op '\113' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op inj : Pos -> Nat)((op 1 : Pos)),

(op __@@__ : Nat *

Nat -> Nat)((op inj : Pos -> Nat)((op 1 : Pos)),

(op 3 : Nat)))) %(slash_113)%,

. (op '\114' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op inj : Pos -> Nat)((op 1 : Pos)),

(op __@@__ : Nat *

Nat -> Nat)((op inj : Pos -> Nat)((op 1 : Pos)),

(op 4 : Nat)))) %(slash_114)%,

. (op '\115' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op inj : Pos -> Nat)((op 1 : Pos)),

(op __@@__ : Nat *

Nat -> Nat)((op inj : Pos -> Nat)((op 1 : Pos)),

(op 5 : Nat)))) %(slash_115)%,

. (op '\116' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op inj : Pos -> Nat)((op 1 : Pos)),

(op __@@__ : Nat *

Nat -> Nat)((op inj : Pos -> Nat)((op 1 : Pos)),

(op 6 : Nat)))) %(slash_116)%,

. (op '\117' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op inj : Pos -> Nat)((op 1 : Pos)),

(op __@@__ : Nat *

Nat -> Nat)((op inj : Pos -> Nat)((op 1 : Pos)),

(op 7 : Nat)))) %(slash_117)%,

. (op '\118' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op inj : Pos -> Nat)((op 1 : Pos)),

(op __@@__ : Nat *

Nat -> Nat)((op inj : Pos -> Nat)((op 1 : Pos)),

(op 8 : Nat)))) %(slash_118)%,

. (op '\119' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op inj : Pos -> Nat)((op 1 : Pos)),

(op __@@__ : Nat *

Nat -> Nat)((op inj : Pos -> Nat)((op 1 : Pos)),

(op 9 : Nat)))) %(slash_119)%,

. (op '\120' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op inj : Pos -> Nat)((op 1 : Pos)),

(op __@@__ : Nat *

Nat -> Nat)((op 2 : Nat),

(op 0 : Nat)))) %(slash_120)%,

. (op '\121' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op inj : Pos -> Nat)((op 1 : Pos)),

(op __@@__ : Nat *

Nat -> Nat)((op 2 : Nat),

(op inj : Pos -> Nat)((op 1 : Pos))))) %(slash_121)%,

. (op '\122' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op inj : Pos -> Nat)((op 1 : Pos)),

(op __@@__ : Nat *

Nat -> Nat)((op 2 : Nat),

(op 2 : Nat)))) %(slash_122)%,

. (op '\123' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op inj : Pos -> Nat)((op 1 : Pos)),

(op __@@__ : Nat *

Nat -> Nat)((op 2 : Nat),

(op 3 : Nat)))) %(slash_123)%,

. (op '\124' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op inj : Pos -> Nat)((op 1 : Pos)),

(op __@@__ : Nat *

Nat -> Nat)((op 2 : Nat),

(op 4 : Nat)))) %(slash_124)%,

. (op '\125' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op inj : Pos -> Nat)((op 1 : Pos)),

(op __@@__ : Nat *

Nat -> Nat)((op 2 : Nat),

(op 5 : Nat)))) %(slash_125)%,

. (op '\126' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op inj : Pos -> Nat)((op 1 : Pos)),

(op __@@__ : Nat *

Nat -> Nat)((op 2 : Nat),

(op 6 : Nat)))) %(slash_126)%,

. (op '\127' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op inj : Pos -> Nat)((op 1 : Pos)),

(op __@@__ : Nat *

Nat -> Nat)((op 2 : Nat),

(op 7 : Nat)))) %(slash_127)%,

. (op '\128' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op inj : Pos -> Nat)((op 1 : Pos)),

(op __@@__ : Nat *

Nat -> Nat)((op 2 : Nat),

(op 8 : Nat)))) %(slash_128)%,

. (op '\129' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op inj : Pos -> Nat)((op 1 : Pos)),

(op __@@__ : Nat *

Nat -> Nat)((op 2 : Nat),

(op 9 : Nat)))) %(slash_129)%,

. (op '\130' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op inj : Pos -> Nat)((op 1 : Pos)),

(op __@@__ : Nat *

Nat -> Nat)((op 3 : Nat),

(op 0 : Nat)))) %(slash_130)%,

. (op '\131' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op inj : Pos -> Nat)((op 1 : Pos)),

(op __@@__ : Nat *

Nat -> Nat)((op 3 : Nat),

(op inj : Pos -> Nat)((op 1 : Pos))))) %(slash_131)%,

. (op '\132' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op inj : Pos -> Nat)((op 1 : Pos)),

(op __@@__ : Nat *

Nat -> Nat)((op 3 : Nat),

(op 2 : Nat)))) %(slash_132)%,

. (op '\133' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op inj : Pos -> Nat)((op 1 : Pos)),

(op __@@__ : Nat *

Nat -> Nat)((op 3 : Nat),

(op 3 : Nat)))) %(slash_133)%,

. (op '\134' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op inj : Pos -> Nat)((op 1 : Pos)),

(op __@@__ : Nat *

Nat -> Nat)((op 3 : Nat),

(op 4 : Nat)))) %(slash_134)%,

. (op '\135' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op inj : Pos -> Nat)((op 1 : Pos)),

(op __@@__ : Nat *

Nat -> Nat)((op 3 : Nat),

(op 5 : Nat)))) %(slash_135)%,

. (op '\136' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op inj : Pos -> Nat)((op 1 : Pos)),

(op __@@__ : Nat *

Nat -> Nat)((op 3 : Nat),

(op 6 : Nat)))) %(slash_136)%,

. (op '\137' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op inj : Pos -> Nat)((op 1 : Pos)),

(op __@@__ : Nat *

Nat -> Nat)((op 3 : Nat),

(op 7 : Nat)))) %(slash_137)%,

. (op '\138' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op inj : Pos -> Nat)((op 1 : Pos)),

(op __@@__ : Nat *

Nat -> Nat)((op 3 : Nat),

(op 8 : Nat)))) %(slash_138)%,

. (op '\139' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op inj : Pos -> Nat)((op 1 : Pos)),

(op __@@__ : Nat *

Nat -> Nat)((op 3 : Nat),

(op 9 : Nat)))) %(slash_139)%,

. (op '\140' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op inj : Pos -> Nat)((op 1 : Pos)),

(op __@@__ : Nat *

Nat -> Nat)((op 4 : Nat),

(op 0 : Nat)))) %(slash_140)%,

. (op '\141' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op inj : Pos -> Nat)((op 1 : Pos)),

(op __@@__ : Nat *

Nat -> Nat)((op 4 : Nat),

(op inj : Pos -> Nat)((op 1 : Pos))))) %(slash_141)%,

. (op '\142' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op inj : Pos -> Nat)((op 1 : Pos)),

(op __@@__ : Nat *

Nat -> Nat)((op 4 : Nat),

(op 2 : Nat)))) %(slash_142)%,

. (op '\143' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op inj : Pos -> Nat)((op 1 : Pos)),

(op __@@__ : Nat *

Nat -> Nat)((op 4 : Nat),

(op 3 : Nat)))) %(slash_143)%,

. (op '\144' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op inj : Pos -> Nat)((op 1 : Pos)),

(op __@@__ : Nat *

Nat -> Nat)((op 4 : Nat),

(op 4 : Nat)))) %(slash_144)%,

. (op '\145' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op inj : Pos -> Nat)((op 1 : Pos)),

(op __@@__ : Nat *

Nat -> Nat)((op 4 : Nat),

(op 5 : Nat)))) %(slash_145)%,

. (op '\146' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op inj : Pos -> Nat)((op 1 : Pos)),

(op __@@__ : Nat *

Nat -> Nat)((op 4 : Nat),

(op 6 : Nat)))) %(slash_146)%,

. (op '\147' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op inj : Pos -> Nat)((op 1 : Pos)),

(op __@@__ : Nat *

Nat -> Nat)((op 4 : Nat),

(op 7 : Nat)))) %(slash_147)%,

. (op '\148' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op inj : Pos -> Nat)((op 1 : Pos)),

(op __@@__ : Nat *

Nat -> Nat)((op 4 : Nat),

(op 8 : Nat)))) %(slash_148)%,

. (op '\149' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op inj : Pos -> Nat)((op 1 : Pos)),

(op __@@__ : Nat *

Nat -> Nat)((op 4 : Nat),

(op 9 : Nat)))) %(slash_149)%,

. (op '\150' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op inj : Pos -> Nat)((op 1 : Pos)),

(op __@@__ : Nat *

Nat -> Nat)((op 5 : Nat),

(op 0 : Nat)))) %(slash_150)%,

. (op '\151' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op inj : Pos -> Nat)((op 1 : Pos)),

(op __@@__ : Nat *

Nat -> Nat)((op 5 : Nat),

(op inj : Pos -> Nat)((op 1 : Pos))))) %(slash_151)%,

. (op '\152' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op inj : Pos -> Nat)((op 1 : Pos)),

(op __@@__ : Nat *

Nat -> Nat)((op 5 : Nat),

(op 2 : Nat)))) %(slash_152)%,

. (op '\153' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op inj : Pos -> Nat)((op 1 : Pos)),

(op __@@__ : Nat *

Nat -> Nat)((op 5 : Nat),

(op 3 : Nat)))) %(slash_153)%,

. (op '\154' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op inj : Pos -> Nat)((op 1 : Pos)),

(op __@@__ : Nat *

Nat -> Nat)((op 5 : Nat),

(op 4 : Nat)))) %(slash_154)%,

. (op '\155' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op inj : Pos -> Nat)((op 1 : Pos)),

(op __@@__ : Nat *

Nat -> Nat)((op 5 : Nat),

(op 5 : Nat)))) %(slash_155)%,

. (op '\156' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op inj : Pos -> Nat)((op 1 : Pos)),

(op __@@__ : Nat *

Nat -> Nat)((op 5 : Nat),

(op 6 : Nat)))) %(slash_156)%,

. (op '\157' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op inj : Pos -> Nat)((op 1 : Pos)),

(op __@@__ : Nat *

Nat -> Nat)((op 5 : Nat),

(op 7 : Nat)))) %(slash_157)%,

. (op '\158' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op inj : Pos -> Nat)((op 1 : Pos)),

(op __@@__ : Nat *

Nat -> Nat)((op 5 : Nat),

(op 8 : Nat)))) %(slash_158)%,

. (op '\159' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op inj : Pos -> Nat)((op 1 : Pos)),

(op __@@__ : Nat *

Nat -> Nat)((op 5 : Nat),

(op 9 : Nat)))) %(slash_159)%,

. (op '\160' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op inj : Pos -> Nat)((op 1 : Pos)),

(op __@@__ : Nat *

Nat -> Nat)((op 6 : Nat),

(op 0 : Nat)))) %(slash_160)%,

. (op '\161' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op inj : Pos -> Nat)((op 1 : Pos)),

(op __@@__ : Nat *

Nat -> Nat)((op 6 : Nat),

(op inj : Pos -> Nat)((op 1 : Pos))))) %(slash_161)%,

. (op '\162' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op inj : Pos -> Nat)((op 1 : Pos)),

(op __@@__ : Nat *

Nat -> Nat)((op 6 : Nat),

(op 2 : Nat)))) %(slash_162)%,

. (op '\163' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op inj : Pos -> Nat)((op 1 : Pos)),

(op __@@__ : Nat *

Nat -> Nat)((op 6 : Nat),

(op 3 : Nat)))) %(slash_163)%,

. (op '\164' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op inj : Pos -> Nat)((op 1 : Pos)),

(op __@@__ : Nat *

Nat -> Nat)((op 6 : Nat),

(op 4 : Nat)))) %(slash_164)%,

. (op '\165' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op inj : Pos -> Nat)((op 1 : Pos)),

(op __@@__ : Nat *

Nat -> Nat)((op 6 : Nat),

(op 5 : Nat)))) %(slash_165)%,

. (op '\166' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op inj : Pos -> Nat)((op 1 : Pos)),

(op __@@__ : Nat *

Nat -> Nat)((op 6 : Nat),

(op 6 : Nat)))) %(slash_166)%,

. (op '\167' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op inj : Pos -> Nat)((op 1 : Pos)),

(op __@@__ : Nat *

Nat -> Nat)((op 6 : Nat),

(op 7 : Nat)))) %(slash_167)%,

. (op '\168' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op inj : Pos -> Nat)((op 1 : Pos)),

(op __@@__ : Nat *

Nat -> Nat)((op 6 : Nat),

(op 8 : Nat)))) %(slash_168)%,

. (op '\169' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op inj : Pos -> Nat)((op 1 : Pos)),

(op __@@__ : Nat *

Nat -> Nat)((op 6 : Nat),

(op 9 : Nat)))) %(slash_169)%,

. (op '\170' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op inj : Pos -> Nat)((op 1 : Pos)),

(op __@@__ : Nat *

Nat -> Nat)((op 7 : Nat),

(op 0 : Nat)))) %(slash_170)%,

. (op '\171' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op inj : Pos -> Nat)((op 1 : Pos)),

(op __@@__ : Nat *

Nat -> Nat)((op 7 : Nat),

(op inj : Pos -> Nat)((op 1 : Pos))))) %(slash_171)%,

. (op '\172' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op inj : Pos -> Nat)((op 1 : Pos)),

(op __@@__ : Nat *

Nat -> Nat)((op 7 : Nat),

(op 2 : Nat)))) %(slash_172)%,

. (op '\173' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op inj : Pos -> Nat)((op 1 : Pos)),

(op __@@__ : Nat *

Nat -> Nat)((op 7 : Nat),

(op 3 : Nat)))) %(slash_173)%,

. (op '\174' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op inj : Pos -> Nat)((op 1 : Pos)),

(op __@@__ : Nat *

Nat -> Nat)((op 7 : Nat),

(op 4 : Nat)))) %(slash_174)%,

. (op '\175' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op inj : Pos -> Nat)((op 1 : Pos)),

(op __@@__ : Nat *

Nat -> Nat)((op 7 : Nat),

(op 5 : Nat)))) %(slash_175)%,

. (op '\176' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op inj : Pos -> Nat)((op 1 : Pos)),

(op __@@__ : Nat *

Nat -> Nat)((op 7 : Nat),

(op 6 : Nat)))) %(slash_176)%,

. (op '\177' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op inj : Pos -> Nat)((op 1 : Pos)),

(op __@@__ : Nat *

Nat -> Nat)((op 7 : Nat),

(op 7 : Nat)))) %(slash_177)%,

. (op '\178' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op inj : Pos -> Nat)((op 1 : Pos)),

(op __@@__ : Nat *

Nat -> Nat)((op 7 : Nat),

(op 8 : Nat)))) %(slash_178)%,

. (op '\179' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op inj : Pos -> Nat)((op 1 : Pos)),

(op __@@__ : Nat *

Nat -> Nat)((op 7 : Nat),

(op 9 : Nat)))) %(slash_179)%,

. (op '\180' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op inj : Pos -> Nat)((op 1 : Pos)),

(op __@@__ : Nat *

Nat -> Nat)((op 8 : Nat),

(op 0 : Nat)))) %(slash_180)%,

. (op '\181' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op inj : Pos -> Nat)((op 1 : Pos)),

(op __@@__ : Nat *

Nat -> Nat)((op 8 : Nat),

(op inj : Pos -> Nat)((op 1 : Pos))))) %(slash_181)%,

. (op '\182' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op inj : Pos -> Nat)((op 1 : Pos)),

(op __@@__ : Nat *

Nat -> Nat)((op 8 : Nat),

(op 2 : Nat)))) %(slash_182)%,

. (op '\183' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op inj : Pos -> Nat)((op 1 : Pos)),

(op __@@__ : Nat *

Nat -> Nat)((op 8 : Nat),

(op 3 : Nat)))) %(slash_183)%,

. (op '\184' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op inj : Pos -> Nat)((op 1 : Pos)),

(op __@@__ : Nat *

Nat -> Nat)((op 8 : Nat),

(op 4 : Nat)))) %(slash_184)%,

. (op '\185' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op inj : Pos -> Nat)((op 1 : Pos)),

(op __@@__ : Nat *

Nat -> Nat)((op 8 : Nat),

(op 5 : Nat)))) %(slash_185)%,

. (op '\186' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op inj : Pos -> Nat)((op 1 : Pos)),

(op __@@__ : Nat *

Nat -> Nat)((op 8 : Nat),

(op 6 : Nat)))) %(slash_186)%,

. (op '\187' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op inj : Pos -> Nat)((op 1 : Pos)),

(op __@@__ : Nat *

Nat -> Nat)((op 8 : Nat),

(op 7 : Nat)))) %(slash_187)%,

. (op '\188' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op inj : Pos -> Nat)((op 1 : Pos)),

(op __@@__ : Nat *

Nat -> Nat)((op 8 : Nat),

(op 8 : Nat)))) %(slash_188)%,

. (op '\189' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op inj : Pos -> Nat)((op 1 : Pos)),

(op __@@__ : Nat *

Nat -> Nat)((op 8 : Nat),

(op 9 : Nat)))) %(slash_189)%,

. (op '\190' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op inj : Pos -> Nat)((op 1 : Pos)),

(op __@@__ : Nat *

Nat -> Nat)((op 9 : Nat),

(op 0 : Nat)))) %(slash_190)%,

. (op '\191' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op inj : Pos -> Nat)((op 1 : Pos)),

(op __@@__ : Nat *

Nat -> Nat)((op 9 : Nat),

(op inj : Pos -> Nat)((op 1 : Pos))))) %(slash_191)%,

. (op '\192' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op inj : Pos -> Nat)((op 1 : Pos)),

(op __@@__ : Nat *

Nat -> Nat)((op 9 : Nat),

(op 2 : Nat)))) %(slash_192)%,

. (op '\193' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op inj : Pos -> Nat)((op 1 : Pos)),

(op __@@__ : Nat *

Nat -> Nat)((op 9 : Nat),

(op 3 : Nat)))) %(slash_193)%,

. (op '\194' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op inj : Pos -> Nat)((op 1 : Pos)),

(op __@@__ : Nat *

Nat -> Nat)((op 9 : Nat),

(op 4 : Nat)))) %(slash_194)%,

. (op '\195' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op inj : Pos -> Nat)((op 1 : Pos)),

(op __@@__ : Nat *

Nat -> Nat)((op 9 : Nat),

(op 5 : Nat)))) %(slash_195)%,

. (op '\196' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op inj : Pos -> Nat)((op 1 : Pos)),

(op __@@__ : Nat *

Nat -> Nat)((op 9 : Nat),

(op 6 : Nat)))) %(slash_196)%,

. (op '\197' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op inj : Pos -> Nat)((op 1 : Pos)),

(op __@@__ : Nat *

Nat -> Nat)((op 9 : Nat),

(op 7 : Nat)))) %(slash_197)%,

. (op '\198' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op inj : Pos -> Nat)((op 1 : Pos)),

(op __@@__ : Nat *

Nat -> Nat)((op 9 : Nat),

(op 8 : Nat)))) %(slash_198)%,

. (op '\199' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op inj : Pos -> Nat)((op 1 : Pos)),

(op __@@__ : Nat *

Nat -> Nat)((op 9 : Nat),

(op 9 : Nat)))) %(slash_199)%,

. (op '\200' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op 2 : Nat),

(op __@@__ : Nat *

Nat -> Nat)((op 0 : Nat),

(op 0 : Nat)))) %(slash_200)%,

. (op '\201' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op 2 : Nat),

(op __@@__ : Nat *

Nat -> Nat)((op 0 : Nat),

(op inj : Pos -> Nat)((op 1 : Pos))))) %(slash_201)%,

. (op '\202' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op 2 : Nat),

(op __@@__ : Nat *

Nat -> Nat)((op 0 : Nat),

(op 2 : Nat)))) %(slash_202)%,

. (op '\203' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op 2 : Nat),

(op __@@__ : Nat *

Nat -> Nat)((op 0 : Nat),

(op 3 : Nat)))) %(slash_203)%,

. (op '\204' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op 2 : Nat),

(op __@@__ : Nat *

Nat -> Nat)((op 0 : Nat),

(op 4 : Nat)))) %(slash_204)%,

. (op '\205' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op 2 : Nat),

(op __@@__ : Nat *

Nat -> Nat)((op 0 : Nat),

(op 5 : Nat)))) %(slash_205)%,

. (op '\206' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op 2 : Nat),

(op __@@__ : Nat *

Nat -> Nat)((op 0 : Nat),

(op 6 : Nat)))) %(slash_206)%,

. (op '\207' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op 2 : Nat),

(op __@@__ : Nat *

Nat -> Nat)((op 0 : Nat),

(op 7 : Nat)))) %(slash_207)%,

. (op '\208' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op 2 : Nat),

(op __@@__ : Nat *

Nat -> Nat)((op 0 : Nat),

(op 8 : Nat)))) %(slash_208)%,

. (op '\209' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op 2 : Nat),

(op __@@__ : Nat *

Nat -> Nat)((op 0 : Nat),

(op 9 : Nat)))) %(slash_209)%,

. (op '\210' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op 2 : Nat),

(op __@@__ : Nat *

Nat -> Nat)((op inj : Pos -> Nat)((op 1 : Pos)),

(op 0 : Nat)))) %(slash_210)%,

. (op '\211' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op 2 : Nat),

(op __@@__ : Nat *

Nat -> Nat)((op inj : Pos -> Nat)((op 1 : Pos)),

(op inj : Pos -> Nat)((op 1 : Pos))))) %(slash_211)%,

. (op '\212' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op 2 : Nat),

(op __@@__ : Nat *

Nat -> Nat)((op inj : Pos -> Nat)((op 1 : Pos)),

(op 2 : Nat)))) %(slash_212)%,

. (op '\213' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op 2 : Nat),

(op __@@__ : Nat *

Nat -> Nat)((op inj : Pos -> Nat)((op 1 : Pos)),

(op 3 : Nat)))) %(slash_213)%,

. (op '\214' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op 2 : Nat),

(op __@@__ : Nat *

Nat -> Nat)((op inj : Pos -> Nat)((op 1 : Pos)),

(op 4 : Nat)))) %(slash_214)%,

. (op '\215' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op 2 : Nat),

(op __@@__ : Nat *

Nat -> Nat)((op inj : Pos -> Nat)((op 1 : Pos)),

(op 5 : Nat)))) %(slash_215)%,

. (op '\216' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op 2 : Nat),

(op __@@__ : Nat *

Nat -> Nat)((op inj : Pos -> Nat)((op 1 : Pos)),

(op 6 : Nat)))) %(slash_216)%,

. (op '\217' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op 2 : Nat),

(op __@@__ : Nat *

Nat -> Nat)((op inj : Pos -> Nat)((op 1 : Pos)),

(op 7 : Nat)))) %(slash_217)%,

. (op '\218' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op 2 : Nat),

(op __@@__ : Nat *

Nat -> Nat)((op inj : Pos -> Nat)((op 1 : Pos)),

(op 8 : Nat)))) %(slash_218)%,

. (op '\219' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op 2 : Nat),

(op __@@__ : Nat *

Nat -> Nat)((op inj : Pos -> Nat)((op 1 : Pos)),

(op 9 : Nat)))) %(slash_219)%,

. (op '\220' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op 2 : Nat),

(op __@@__ : Nat *

Nat -> Nat)((op 2 : Nat),

(op 0 : Nat)))) %(slash_220)%,

. (op '\221' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op 2 : Nat),

(op __@@__ : Nat *

Nat -> Nat)((op 2 : Nat),

(op inj : Pos -> Nat)((op 1 : Pos))))) %(slash_221)%,

. (op '\222' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op 2 : Nat),

(op __@@__ : Nat *

Nat -> Nat)((op 2 : Nat),

(op 2 : Nat)))) %(slash_222)%,

. (op '\223' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op 2 : Nat),

(op __@@__ : Nat *

Nat -> Nat)((op 2 : Nat),

(op 3 : Nat)))) %(slash_223)%,

. (op '\224' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op 2 : Nat),

(op __@@__ : Nat *

Nat -> Nat)((op 2 : Nat),

(op 4 : Nat)))) %(slash_224)%,

. (op '\225' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op 2 : Nat),

(op __@@__ : Nat *

Nat -> Nat)((op 2 : Nat),

(op 5 : Nat)))) %(slash_225)%,

. (op '\226' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op 2 : Nat),

(op __@@__ : Nat *

Nat -> Nat)((op 2 : Nat),

(op 6 : Nat)))) %(slash_226)%,

. (op '\227' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op 2 : Nat),

(op __@@__ : Nat *

Nat -> Nat)((op 2 : Nat),

(op 7 : Nat)))) %(slash_227)%,

. (op '\228' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op 2 : Nat),

(op __@@__ : Nat *

Nat -> Nat)((op 2 : Nat),

(op 8 : Nat)))) %(slash_228)%,

. (op '\229' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op 2 : Nat),

(op __@@__ : Nat *

Nat -> Nat)((op 2 : Nat),

(op 9 : Nat)))) %(slash_229)%,

. (op '\230' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op 2 : Nat),

(op __@@__ : Nat *

Nat -> Nat)((op 3 : Nat),

(op 0 : Nat)))) %(slash_230)%,

. (op '\231' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op 2 : Nat),

(op __@@__ : Nat *

Nat -> Nat)((op 3 : Nat),

(op inj : Pos -> Nat)((op 1 : Pos))))) %(slash_231)%,

. (op '\232' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op 2 : Nat),

(op __@@__ : Nat *

Nat -> Nat)((op 3 : Nat),

(op 2 : Nat)))) %(slash_232)%,

. (op '\233' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op 2 : Nat),

(op __@@__ : Nat *

Nat -> Nat)((op 3 : Nat),

(op 3 : Nat)))) %(slash_233)%,

. (op '\234' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op 2 : Nat),

(op __@@__ : Nat *

Nat -> Nat)((op 3 : Nat),

(op 4 : Nat)))) %(slash_234)%,

. (op '\235' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op 2 : Nat),

(op __@@__ : Nat *

Nat -> Nat)((op 3 : Nat),

(op 5 : Nat)))) %(slash_235)%,

. (op '\236' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op 2 : Nat),

(op __@@__ : Nat *

Nat -> Nat)((op 3 : Nat),

(op 6 : Nat)))) %(slash_236)%,

. (op '\237' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op 2 : Nat),

(op __@@__ : Nat *

Nat -> Nat)((op 3 : Nat),

(op 7 : Nat)))) %(slash_237)%,

. (op '\238' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op 2 : Nat),

(op __@@__ : Nat *

Nat -> Nat)((op 3 : Nat),

(op 8 : Nat)))) %(slash_238)%,

. (op '\239' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op 2 : Nat),

(op __@@__ : Nat *

Nat -> Nat)((op 3 : Nat),

(op 9 : Nat)))) %(slash_239)%,

. (op '\240' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op 2 : Nat),

(op __@@__ : Nat *

Nat -> Nat)((op 4 : Nat),

(op 0 : Nat)))) %(slash_240)%,

. (op '\241' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op 2 : Nat),

(op __@@__ : Nat *

Nat -> Nat)((op 4 : Nat),

(op inj : Pos -> Nat)((op 1 : Pos))))) %(slash_241)%,

. (op '\242' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op 2 : Nat),

(op __@@__ : Nat *

Nat -> Nat)((op 4 : Nat),

(op 2 : Nat)))) %(slash_242)%,

. (op '\243' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op 2 : Nat),

(op __@@__ : Nat *

Nat -> Nat)((op 4 : Nat),

(op 3 : Nat)))) %(slash_243)%,

. (op '\244' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op 2 : Nat),

(op __@@__ : Nat *

Nat -> Nat)((op 4 : Nat),

(op 4 : Nat)))) %(slash_244)%,

. (op '\245' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op 2 : Nat),

(op __@@__ : Nat *

Nat -> Nat)((op 4 : Nat),

(op 5 : Nat)))) %(slash_245)%,

. (op '\246' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op 2 : Nat),

(op __@@__ : Nat *

Nat -> Nat)((op 4 : Nat),

(op 6 : Nat)))) %(slash_246)%,

. (op '\247' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op 2 : Nat),

(op __@@__ : Nat *

Nat -> Nat)((op 4 : Nat),

(op 7 : Nat)))) %(slash_247)%,

. (op '\248' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op 2 : Nat),

(op __@@__ : Nat *

Nat -> Nat)((op 4 : Nat),

(op 8 : Nat)))) %(slash_248)%,

. (op '\249' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op 2 : Nat),

(op __@@__ : Nat *

Nat -> Nat)((op 4 : Nat),

(op 9 : Nat)))) %(slash_249)%,

. (op '\250' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op 2 : Nat),

(op __@@__ : Nat *

Nat -> Nat)((op 5 : Nat),

(op 0 : Nat)))) %(slash_250)%,

. (op '\251' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op 2 : Nat),

(op __@@__ : Nat *

Nat -> Nat)((op 5 : Nat),

(op inj : Pos -> Nat)((op 1 : Pos))))) %(slash_251)%,

. (op '\252' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op 2 : Nat),

(op __@@__ : Nat *

Nat -> Nat)((op 5 : Nat),

(op 2 : Nat)))) %(slash_252)%,

. (op '\253' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op 2 : Nat),

(op __@@__ : Nat *

Nat -> Nat)((op 5 : Nat),

(op 3 : Nat)))) %(slash_253)%,

. (op '\254' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op 2 : Nat),

(op __@@__ : Nat *

Nat -> Nat)((op 5 : Nat),

(op 4 : Nat)))) %(slash_254)%,

. (op '\255' : Char) =

(op chr : Nat ->? Char)((op __@@__ : Nat *

Nat -> Nat)((op 2 : Nat),

(op __@@__ : Nat *

Nat -> Nat)((op 5 : Nat),

(op 5 : Nat)))) %(slash_255)%,

. (op ' ' : Char) = (op '\032' : Char) %(printable_32)%,

. (op '!' : Char) = (op '\033' : Char) %(printable_33)%,

. (op '\"' : Char) = (op '\034' : Char) %(printable_34)%,

. (op '#' : Char) = (op '\035' : Char) %(printable_35)%,

. (op '$' : Char) = (op '\036' : Char) %(printable_36)%,

. (op '%' : Char) = (op '\037' : Char) %(printable_37)%,

. (op '&' : Char) = (op '\038' : Char) %(printable_38)%,

. (op '\'' : Char) = (op '\039' : Char) %(printable_39)%,

. (op '(' : Char) = (op '\040' : Char) %(printable_40)%,

. (op ')' : Char) = (op '\041' : Char) %(printable_41)%,

. (op '*' : Char) = (op '\042' : Char) %(printable_42)%,

. (op '+' : Char) = (op '\043' : Char) %(printable_43)%,

. (op ',' : Char) = (op '\044' : Char) %(printable_44)%,

. (op '-' : Char) = (op '\045' : Char) %(printable_45)%,

. (op '.' : Char) = (op '\046' : Char) %(printable_46)%,

. (op '/' : Char) = (op '\047' : Char) %(printable_47)%,

. (op '0' : Char) = (op '\048' : Char) %(printable_48)%,

. (op '1' : Char) = (op '\049' : Char) %(printable_49)%,

. (op '2' : Char) = (op '\050' : Char) %(printable_50)%,

. (op '3' : Char) = (op '\051' : Char) %(printable_51)%,

. (op '4' : Char) = (op '\052' : Char) %(printable_52)%,

. (op '5' : Char) = (op '\053' : Char) %(printable_53)%,

. (op '6' : Char) = (op '\054' : Char) %(printable_54)%,

. (op '7' : Char) = (op '\055' : Char) %(printable_55)%,

. (op '8' : Char) = (op '\056' : Char) %(printable_56)%,

. (op '9' : Char) = (op '\057' : Char) %(printable_57)%,

. (op ':' : Char) = (op '\058' : Char) %(printable_58)%,

. (op ';' : Char) = (op '\059' : Char) %(printable_59)%,

. (op '<' : Char) = (op '\060' : Char) %(printable_60)%,

. (op '=' : Char) = (op '\061' : Char) %(printable_61)%,

. (op '>' : Char) = (op '\062' : Char) %(printable_62)%,

. (op '?' : Char) = (op '\063' : Char) %(printable_63)%,

. (op '@' : Char) = (op '\064' : Char) %(printable_64)%,

. (op 'A' : Char) = (op '\065' : Char) %(printable_65)%,

. (op 'B' : Char) = (op '\066' : Char) %(printable_66)%,

. (op 'C' : Char) = (op '\067' : Char) %(printable_67)%,

. (op 'D' : Char) = (op '\068' : Char) %(printable_68)%,

. (op 'E' : Char) = (op '\069' : Char) %(printable_69)%,

. (op 'F' : Char) = (op '\070' : Char) %(printable_70)%,

. (op 'G' : Char) = (op '\071' : Char) %(printable_71)%,

. (op 'H' : Char) = (op '\072' : Char) %(printable_72)%,

. (op 'I' : Char) = (op '\073' : Char) %(printable_73)%,

. (op 'J' : Char) = (op '\074' : Char) %(printable_74)%,

. (op 'K' : Char) = (op '\075' : Char) %(printable_75)%,

. (op 'L' : Char) = (op '\076' : Char) %(printable_76)%,

. (op 'M' : Char) = (op '\077' : Char) %(printable_77)%,

. (op 'N' : Char) = (op '\078' : Char) %(printable_78)%,

. (op 'O' : Char) = (op '\079' : Char) %(printable_79)%,

. (op 'P' : Char) = (op '\080' : Char) %(printable_80)%,

. (op 'Q' : Char) = (op '\081' : Char) %(printable_81)%,

. (op 'R' : Char) = (op '\082' : Char) %(printable_82)%,

. (op 'S' : Char) = (op '\083' : Char) %(printable_83)%,

. (op 'T' : Char) = (op '\084' : Char) %(printable_84)%,

. (op 'U' : Char) = (op '\085' : Char) %(printable_85)%,

. (op 'V' : Char) = (op '\086' : Char) %(printable_86)%,

. (op 'W' : Char) = (op '\087' : Char) %(printable_87)%,

. (op 'X' : Char) = (op '\088' : Char) %(printable_88)%,

. (op 'Y' : Char) = (op '\089' : Char) %(printable_89)%,

. (op 'Z' : Char) = (op '\090' : Char) %(printable_90)%,

. (op '[' : Char) = (op '\091' : Char) %(printable_91)%,

. (op '\\' : Char) = (op '\092' : Char) %(printable_92)%,

. (op ']' : Char) = (op '\093' : Char) %(printable_93)%,

. (op '^' : Char) = (op '\094' : Char) %(printable_94)%,

. (op '_' : Char) = (op '\095' : Char) %(printable_95)%,

. (op '`' : Char) = (op '\096' : Char) %(printable_96)%,

. (op 'a' : Char) = (op '\097' : Char) %(printable_97)%,

. (op 'b' : Char) = (op '\098' : Char) %(printable_98)%,

. (op 'c' : Char) = (op '\099' : Char) %(printable_99)%,

. (op 'd' : Char) = (op '\100' : Char) %(printable_100)%,

. (op 'e' : Char) = (op '\101' : Char) %(printable_101)%,

. (op 'f' : Char) = (op '\102' : Char) %(printable_102)%,

. (op 'g' : Char) = (op '\103' : Char) %(printable_103)%,

. (op 'h' : Char) = (op '\104' : Char) %(printable_104)%,

. (op 'i' : Char) = (op '\105' : Char) %(printable_105)%,

. (op 'j' : Char) = (op '\106' : Char) %(printable_106)%,

. (op 'k' : Char) = (op '\107' : Char) %(printable_107)%,

. (op 'l' : Char) = (op '\108' : Char) %(printable_108)%,

. (op 'm' : Char) = (op '\109' : Char) %(printable_109)%,

. (op 'n' : Char) = (op '\110' : Char) %(printable_110)%,

. (op 'o' : Char) = (op '\111' : Char) %(printable_111)%,

. (op 'p' : Char) = (op '\112' : Char) %(printable_112)%,

. (op 'q' : Char) = (op '\113' : Char) %(printable_113)%,

. (op 'r' : Char) = (op '\114' : Char) %(printable_114)%,

. (op 's' : Char) = (op '\115' : Char) %(printable_115)%,

. (op 't' : Char) = (op '\116' : Char) %(printable_116)%,

. (op 'u' : Char) = (op '\117' : Char) %(printable_117)%,

. (op 'v' : Char) = (op '\118' : Char) %(printable_118)%,

. (op 'w' : Char) = (op '\119' : Char) %(printable_119)%,

. (op 'x' : Char) = (op '\120' : Char) %(printable_120)%,

. (op 'y' : Char) = (op '\121' : Char) %(printable_121)%,

. (op 'z' : Char) = (op '\122' : Char) %(printable_122)%,

. (op '{' : Char) = (op '\123' : Char) %(printable_123)%,

. (op '|' : Char) = (op '\124' : Char) %(printable_124)%,

. (op '}' : Char) = (op '\125' : Char) %(printable_125)%,

. (op '~' : Char) = (op '\126' : Char) %(printable_126)%,

. (op ' ' : Char) = (op '\160' : Char) %(printable_160)%,

. (op '�' : Char) = (op '\161' : Char) %(printable_161)%,

. (op '�' : Char) = (op '\162' : Char) %(printable_162)%,

. (op '�' : Char) = (op '\163' : Char) %(printable_163)%,

. (op '�' : Char) = (op '\164' : Char) %(printable_164)%,

. (op '�' : Char) = (op '\165' : Char) %(printable_165)%,

. (op '�' : Char) = (op '\166' : Char) %(printable_166)%,

. (op '�' : Char) = (op '\167' : Char) %(printable_167)%,

. (op '�' : Char) = (op '\168' : Char) %(printable_168)%,

. (op '�' : Char) = (op '\169' : Char) %(printable_169)%,

. (op '�' : Char) = (op '\170' : Char) %(printable_170)%,

. (op '�' : Char) = (op '\171' : Char) %(printable_171)%,

. (op '�' : Char) = (op '\172' : Char) %(printable_172)%,

. (op '�' : Char) = (op '\173' : Char) %(printable_173)%,

. (op '�' : Char) = (op '\174' : Char) %(printable_174)%,

. (op '�' : Char) = (op '\175' : Char) %(printable_175)%,

. (op '�' : Char) = (op '\176' : Char) %(printable_176)%,

. (op '�' : Char) = (op '\177' : Char) %(printable_177)%,

. (op '�' : Char) = (op '\178' : Char) %(printable_178)%,

. (op '�' : Char) = (op '\179' : Char) %(printable_179)%,

. (op '�' : Char) = (op '\180' : Char) %(printable_180)%,

. (op '�' : Char) = (op '\181' : Char) %(printable_181)%,

. (op '�' : Char) = (op '\182' : Char) %(printable_182)%,

. (op '�' : Char) = (op '\183' : Char) %(printable_183)%,

. (op '�' : Char) = (op '\184' : Char) %(printable_184)%,

. (op '�' : Char) = (op '\185' : Char) %(printable_185)%,

. (op '�' : Char) = (op '\186' : Char) %(printable_186)%,

. (op '�' : Char) = (op '\187' : Char) %(printable_187)%,

. (op '�' : Char) = (op '\188' : Char) %(printable_188)%,

. (op '�' : Char) = (op '\189' : Char) %(printable_189)%,

. (op '�' : Char) = (op '\190' : Char) %(printable_190)%,

. (op '�' : Char) = (op '\191' : Char) %(printable_191)%,

. (op '�' : Char) = (op '\192' : Char) %(printable_192)%,

. (op '�' : Char) = (op '\193' : Char) %(printable_193)%,

. (op '�' : Char) = (op '\194' : Char) %(printable_194)%,

. (op '�' : Char) = (op '\195' : Char) %(printable_195)%,

. (op '�' : Char) = (op '\196' : Char) %(printable_196)%,

. (op '�' : Char) = (op '\197' : Char) %(printable_197)%,

. (op '�' : Char) = (op '\198' : Char) %(printable_198)%,

. (op '�' : Char) = (op '\199' : Char) %(printable_199)%,

. (op '�' : Char) = (op '\200' : Char) %(printable_200)%,

. (op '�' : Char) = (op '\201' : Char) %(printable_201)%,

. (op '�' : Char) = (op '\202' : Char) %(printable_202)%,

. (op '�' : Char) = (op '\203' : Char) %(printable_203)%,

. (op '�' : Char) = (op '\204' : Char) %(printable_204)%,

. (op '�' : Char) = (op '\205' : Char) %(printable_205)%,

. (op '�' : Char) = (op '\206' : Char) %(printable_206)%,

. (op '�' : Char) = (op '\207' : Char) %(printable_207)%,

. (op '�' : Char) = (op '\208' : Char) %(printable_208)%,

. (op '�' : Char) = (op '\209' : Char) %(printable_209)%,

. (op '�' : Char) = (op '\210' : Char) %(printable_210)%,

. (op '�' : Char) = (op '\211' : Char) %(printable_211)%,

. (op '�' : Char) = (op '\212' : Char) %(printable_212)%,

. (op '�' : Char) = (op '\213' : Char) %(printable_213)%,

. (op '�' : Char) = (op '\214' : Char) %(printable_214)%,

. (op '�' : Char) = (op '\215' : Char) %(printable_215)%,

. (op '�' : Char) = (op '\216' : Char) %(printable_216)%,

. (op '�' : Char) = (op '\217' : Char) %(printable_217)%,

. (op '�' : Char) = (op '\218' : Char) %(printable_218)%,

. (op '�' : Char) = (op '\219' : Char) %(printable_219)%,

. (op '�' : Char) = (op '\220' : Char) %(printable_220)%,

. (op '�' : Char) = (op '\221' : Char) %(printable_221)%,

. (op '�' : Char) = (op '\222' : Char) %(printable_222)%,

. (op '�' : Char) = (op '\223' : Char) %(printable_223)%,

. (op '�' : Char) = (op '\224' : Char) %(printable_224)%,

. (op '�' : Char) = (op '\225' : Char) %(printable_225)%,

. (op '�' : Char) = (op '\226' : Char) %(printable_226)%,

. (op '�' : Char) = (op '\227' : Char) %(printable_227)%,

. (op '�' : Char) = (op '\228' : Char) %(printable_228)%,

. (op '�' : Char) = (op '\229' : Char) %(printable_229)%,

. (op '�' : Char) = (op '\230' : Char) %(printable_230)%,

. (op '�' : Char) = (op '\231' : Char) %(printable_231)%,

. (op '�' : Char) = (op '\232' : Char) %(printable_232)%,

. (op '�' : Char) = (op '\233' : Char) %(printable_233)%,

. (op '�' : Char) = (op '\234' : Char) %(printable_234)%,

. (op '�' : Char) = (op '\235' : Char) %(printable_235)%,

. (op '�' : Char) = (op '\236' : Char) %(printable_236)%,

. (op '�' : Char) = (op '\237' : Char) %(printable_237)%,

. (op '�' : Char) = (op '\238' : Char) %(printable_238)%,

. (op '�' : Char) = (op '\239' : Char) %(printable_239)%,

. (op '�' : Char) = (op '\240' : Char) %(printable_240)%,

. (op '�' : Char) = (op '\241' : Char) %(printable_241)%,

. (op '�' : Char) = (op '\242' : Char) %(printable_242)%,

. (op '�' : Char) = (op '\243' : Char) %(printable_243)%,

. (op '�' : Char) = (op '\244' : Char) %(printable_244)%,

. (op '�' : Char) = (op '\245' : Char) %(printable_245)%,

. (op '�' : Char) = (op '\246' : Char) %(printable_246)%,

. (op '�' : Char) = (op '\247' : Char) %(printable_247)%,

. (op '�' : Char) = (op '\248' : Char) %(printable_248)%,

. (op '�' : Char) = (op '\249' : Char) %(printable_249)%,

. (op '�' : Char) = (op '\250' : Char) %(printable_250)%,

. (op '�' : Char) = (op '\251' : Char) %(printable_251)%,

. (op '�' : Char) = (op '\252' : Char) %(printable_252)%,

. (op '�' : Char) = (op '\253' : Char) %(printable_253)%,

. (op '�' : Char) = (op '\254' : Char) %(printable_254)%,

. (op '�' : Char) = (op '\255' : Char) %(printable_255)%,

. forall c:Char

. (pred isLetter : Char)((var c : Char)) <=>

((pred __<=__ : Int *

Int)((op inj : Nat -> Int)((op ord : Char -> Nat)((op 'A' : Char))),

(op inj : Nat -> Int)((op ord : Char -> Nat)((var c : Char))))

/\ (pred __<=__ : Int *

Int)((op inj : Nat -> Int)((op ord : Char -> Nat)((var c : Char))),

(op inj : Nat -> Int)((op ord : Char -> Nat)((op 'Z' : Char)))))

\/ ((pred __<=__ : Int *

Int)((op inj : Nat -> Int)((op ord : Char -> Nat)((op 'a' : Char))),

(op inj : Nat -> Int)((op ord : Char -> Nat)((var c : Char))))

/\ (pred __<=__ : Int *

Int)((op inj : Nat -> Int)((op ord : Char -> Nat)((var c : Char))),

(op inj : Nat -> Int)((op ord : Char -> Nat)((op 'z' : Char))))) %(isLetter_def)%,

. forall c:Char

. (pred isDigit : Char)((var c : Char)) <=>

(pred __<=__ : Int *

Int)((op inj : Nat -> Int)((op ord : Char -> Nat)((op '0' : Char))),

(op inj : Nat -> Int)((op ord : Char -> Nat)((var c : Char))))

/\ (pred __<=__ : Int *

Int)((op inj : Nat -> Int)((op ord : Char -> Nat)((var c : Char))),

(op inj : Nat -> Int)((op ord : Char -> Nat)((op '9' : Char)))) %(isDigit_def)%,

. forall c:Char

. (pred isPrintable : Char)((var c : Char)) <=>

((pred __<=__ : Int *

Int)((op inj : Nat -> Int)((op ord : Char -> Nat)((op ' ' : Char))),

(op inj : Nat -> Int)((op ord : Char -> Nat)((var c : Char))))

/\ (pred __<=__ : Int *

Int)((op inj : Nat -> Int)((op ord : Char -> Nat)((var c : Char))),

(op inj : Nat -> Int)((op ord : Char -> Nat)((op '~' : Char)))))

\/ ((pred __<=__ : Int *

Int)((op inj : Nat -> Int)((op ord : Char -> Nat)((op ' ' : Char))),

(op inj : Nat -> Int)((op ord : Char -> Nat)((var c : Char))))

/\ (pred __<=__ : Int *

Int)((op inj : Nat -> Int)((op ord : Char -> Nat)((var c : Char))),

(op inj : Nat -> Int)((op ord : Char -> Nat)((op '�' : Char))))) %(isPrintable_def)%,

. (op '\o000' : Char) = (op '\000' : Char) %(slash_o000)%,

. (op '\o001' : Char) = (op '\001' : Char) %(slash_o001)%,

. (op '\o002' : Char) = (op '\002' : Char) %(slash_o002)%,

. (op '\o003' : Char) = (op '\003' : Char) %(slash_o003)%,

. (op '\o004' : Char) = (op '\004' : Char) %(slash_o004)%,

. (op '\o005' : Char) = (op '\005' : Char) %(slash_o005)%,

. (op '\o006' : Char) = (op '\006' : Char) %(slash_o006)%,

. (op '\o007' : Char) = (op '\007' : Char) %(slash_o007)%,

. (op '\o010' : Char) = (op '\008' : Char) %(slash_o010)%,

. (op '\o011' : Char) = (op '\009' : Char) %(slash_o011)%,

. (op '\o012' : Char) = (op '\010' : Char) %(slash_o012)%,

. (op '\o013' : Char) = (op '\011' : Char) %(slash_o013)%,

. (op '\o014' : Char) = (op '\012' : Char) %(slash_o014)%,

. (op '\o015' : Char) = (op '\013' : Char) %(slash_o015)%,

. (op '\o016' : Char) = (op '\014' : Char) %(slash_o016)%,

. (op '\o017' : Char) = (op '\015' : Char) %(slash_o017)%,

. (op '\o020' : Char) = (op '\016' : Char) %(slash_o020)%,

. (op '\o021' : Char) = (op '\017' : Char) %(slash_o021)%,

. (op '\o022' : Char) = (op '\018' : Char) %(slash_o022)%,

. (op '\o023' : Char) = (op '\019' : Char) %(slash_o023)%,

. (op '\o024' : Char) = (op '\020' : Char) %(slash_o024)%,

. (op '\o025' : Char) = (op '\021' : Char) %(slash_o025)%,

. (op '\o026' : Char) = (op '\022' : Char) %(slash_o026)%,

. (op '\o027' : Char) = (op '\023' : Char) %(slash_o027)%,

. (op '\o030' : Char) = (op '\024' : Char) %(slash_o030)%,

. (op '\o031' : Char) = (op '\025' : Char) %(slash_o031)%,

. (op '\o032' : Char) = (op '\026' : Char) %(slash_o032)%,

. (op '\o033' : Char) = (op '\027' : Char) %(slash_o033)%,

. (op '\o034' : Char) = (op '\028' : Char) %(slash_o034)%,

. (op '\o035' : Char) = (op '\029' : Char) %(slash_o035)%,

. (op '\o036' : Char) = (op '\030' : Char) %(slash_o036)%,

. (op '\o037' : Char) = (op '\031' : Char) %(slash_o037)%,

. (op '\o040' : Char) = (op '\032' : Char) %(slash_o040)%,

. (op '\o041' : Char) = (op '\033' : Char) %(slash_o041)%,

. (op '\o042' : Char) = (op '\034' : Char) %(slash_o042)%,

. (op '\o043' : Char) = (op '\035' : Char) %(slash_o043)%,

. (op '\o044' : Char) = (op '\036' : Char) %(slash_o044)%,

. (op '\o045' : Char) = (op '\037' : Char) %(slash_o045)%,

. (op '\o046' : Char) = (op '\038' : Char) %(slash_o046)%,

. (op '\o047' : Char) = (op '\039' : Char) %(slash_o047)%,

. (op '\o050' : Char) = (op '\040' : Char) %(slash_o050)%,

. (op '\o051' : Char) = (op '\041' : Char) %(slash_o051)%,

. (op '\o052' : Char) = (op '\042' : Char) %(slash_o052)%,

. (op '\o053' : Char) = (op '\043' : Char) %(slash_o053)%,

. (op '\o054' : Char) = (op '\044' : Char) %(slash_o054)%,

. (op '\o055' : Char) = (op '\045' : Char) %(slash_o055)%,

. (op '\o056' : Char) = (op '\046' : Char) %(slash_o056)%,

. (op '\o057' : Char) = (op '\047' : Char) %(slash_o057)%,

. (op '\o060' : Char) = (op '\048' : Char) %(slash_o060)%,

. (op '\o061' : Char) = (op '\049' : Char) %(slash_o061)%,

. (op '\o062' : Char) = (op '\050' : Char) %(slash_o062)%,

. (op '\o063' : Char) = (op '\051' : Char) %(slash_o063)%,

. (op '\o064' : Char) = (op '\052' : Char) %(slash_o064)%,

. (op '\o065' : Char) = (op '\053' : Char) %(slash_o065)%,

. (op '\o066' : Char) = (op '\054' : Char) %(slash_o066)%,

. (op '\o067' : Char) = (op '\055' : Char) %(slash_o067)%,

. (op '\o070' : Char) = (op '\056' : Char) %(slash_o070)%,

. (op '\o071' : Char) = (op '\057' : Char) %(slash_o071)%,

. (op '\o072' : Char) = (op '\058' : Char) %(slash_o072)%,

. (op '\o073' : Char) = (op '\059' : Char) %(slash_o073)%,

. (op '\o074' : Char) = (op '\060' : Char) %(slash_o074)%,

. (op '\o075' : Char) = (op '\061' : Char) %(slash_o075)%,

. (op '\o076' : Char) = (op '\062' : Char) %(slash_o076)%,

. (op '\o077' : Char) = (op '\063' : Char) %(slash_o077)%,

. (op '\o100' : Char) = (op '\064' : Char) %(slash_o100)%,

. (op '\o101' : Char) = (op '\065' : Char) %(slash_o101)%,

. (op '\o102' : Char) = (op '\066' : Char) %(slash_o102)%,

. (op '\o103' : Char) = (op '\067' : Char) %(slash_o103)%,

. (op '\o104' : Char) = (op '\068' : Char) %(slash_o104)%,

. (op '\o105' : Char) = (op '\069' : Char) %(slash_o105)%,

. (op '\o106' : Char) = (op '\070' : Char) %(slash_o106)%,

. (op '\o107' : Char) = (op '\071' : Char) %(slash_o107)%,

. (op '\o110' : Char) = (op '\072' : Char) %(slash_o110)%,

. (op '\o111' : Char) = (op '\073' : Char) %(slash_o111)%,

. (op '\o112' : Char) = (op '\074' : Char) %(slash_o112)%,

. (op '\o113' : Char) = (op '\075' : Char) %(slash_o113)%,

. (op '\o114' : Char) = (op '\076' : Char) %(slash_o114)%,

. (op '\o115' : Char) = (op '\077' : Char) %(slash_o115)%,

. (op '\o116' : Char) = (op '\078' : Char) %(slash_o116)%,

. (op '\o117' : Char) = (op '\079' : Char) %(slash_o117)%,

. (op '\o120' : Char) = (op '\080' : Char) %(slash_o120)%,

. (op '\o121' : Char) = (op '\081' : Char) %(slash_o121)%,

. (op '\o122' : Char) = (op '\082' : Char) %(slash_o122)%,

. (op '\o123' : Char) = (op '\083' : Char) %(slash_o123)%,

. (op '\o124' : Char) = (op '\084' : Char) %(slash_o124)%,

. (op '\o125' : Char) = (op '\085' : Char) %(slash_o125)%,

. (op '\o126' : Char) = (op '\086' : Char) %(slash_o126)%,

. (op '\o127' : Char) = (op '\087' : Char) %(slash_o127)%,

. (op '\o130' : Char) = (op '\088' : Char) %(slash_o130)%,

. (op '\o131' : Char) = (op '\089' : Char) %(slash_o131)%,

. (op '\o132' : Char) = (op '\090' : Char) %(slash_o132)%,

. (op '\o133' : Char) = (op '\091' : Char) %(slash_o133)%,

. (op '\o134' : Char) = (op '\092' : Char) %(slash_o134)%,

. (op '\o135' : Char) = (op '\093' : Char) %(slash_o135)%,

. (op '\o136' : Char) = (op '\094' : Char) %(slash_o136)%,

. (op '\o137' : Char) = (op '\095' : Char) %(slash_o137)%,

. (op '\o140' : Char) = (op '\096' : Char) %(slash_o140)%,

. (op '\o141' : Char) = (op '\097' : Char) %(slash_o141)%,

. (op '\o142' : Char) = (op '\098' : Char) %(slash_o142)%,

. (op '\o143' : Char) = (op '\099' : Char) %(slash_o143)%,

. (op '\o144' : Char) = (op '\100' : Char) %(slash_o144)%,

. (op '\o145' : Char) = (op '\101' : Char) %(slash_o145)%,

. (op '\o146' : Char) = (op '\102' : Char) %(slash_o146)%,

. (op '\o147' : Char) = (op '\103' : Char) %(slash_o147)%,

. (op '\o150' : Char) = (op '\104' : Char) %(slash_o150)%,

. (op '\o151' : Char) = (op '\105' : Char) %(slash_o151)%,

. (op '\o152' : Char) = (op '\106' : Char) %(slash_o152)%,

. (op '\o153' : Char) = (op '\107' : Char) %(slash_o153)%,

. (op '\o154' : Char) = (op '\108' : Char) %(slash_o154)%,

. (op '\o155' : Char) = (op '\109' : Char) %(slash_o155)%,

. (op '\o156' : Char) = (op '\110' : Char) %(slash_o156)%,

. (op '\o157' : Char) = (op '\111' : Char) %(slash_o157)%,

. (op '\o160' : Char) = (op '\112' : Char) %(slash_o160)%,

. (op '\o161' : Char) = (op '\113' : Char) %(slash_o161)%,

. (op '\o162' : Char) = (op '\114' : Char) %(slash_o162)%,

. (op '\o163' : Char) = (op '\115' : Char) %(slash_o163)%,

. (op '\o164' : Char) = (op '\116' : Char) %(slash_o164)%,

. (op '\o165' : Char) = (op '\117' : Char) %(slash_o165)%,

. (op '\o166' : Char) = (op '\118' : Char) %(slash_o166)%,

. (op '\o167' : Char) = (op '\119' : Char) %(slash_o167)%,

. (op '\o170' : Char) = (op '\120' : Char) %(slash_o170)%,

. (op '\o171' : Char) = (op '\121' : Char) %(slash_o171)%,

. (op '\o172' : Char) = (op '\122' : Char) %(slash_o172)%,

. (op '\o173' : Char) = (op '\123' : Char) %(slash_o173)%,

. (op '\o174' : Char) = (op '\124' : Char) %(slash_o174)%,

. (op '\o175' : Char) = (op '\125' : Char) %(slash_o175)%,

. (op '\o176' : Char) = (op '\126' : Char) %(slash_o176)%,

. (op '\o177' : Char) = (op '\127' : Char) %(slash_o177)%,

. (op '\o200' : Char) = (op '\128' : Char) %(slash_o200)%,

. (op '\o201' : Char) = (op '\129' : Char) %(slash_o201)%,

. (op '\o202' : Char) = (op '\130' : Char) %(slash_o202)%,

. (op '\o203' : Char) = (op '\131' : Char) %(slash_o203)%,

. (op '\o204' : Char) = (op '\132' : Char) %(slash_o204)%,

. (op '\o205' : Char) = (op '\133' : Char) %(slash_o205)%,

. (op '\o206' : Char) = (op '\134' : Char) %(slash_o206)%,

. (op '\o207' : Char) = (op '\135' : Char) %(slash_o207)%,

. (op '\o210' : Char) = (op '\136' : Char) %(slash_o210)%,

. (op '\o211' : Char) = (op '\137' : Char) %(slash_o211)%,

. (op '\o212' : Char) = (op '\138' : Char) %(slash_o212)%,

. (op '\o213' : Char) = (op '\139' : Char) %(slash_o213)%,

. (op '\o214' : Char) = (op '\140' : Char) %(slash_o214)%,

. (op '\o215' : Char) = (op '\141' : Char) %(slash_o215)%,

. (op '\o216' : Char) = (op '\142' : Char) %(slash_o216)%,

. (op '\o217' : Char) = (op '\143' : Char) %(slash_o217)%,

. (op '\o220' : Char) = (op '\144' : Char) %(slash_o220)%,

. (op '\o221' : Char) = (op '\145' : Char) %(slash_o221)%,

. (op '\o222' : Char) = (op '\146' : Char) %(slash_o222)%,

. (op '\o223' : Char) = (op '\147' : Char) %(slash_o223)%,

. (op '\o224' : Char) = (op '\148' : Char) %(slash_o224)%,

. (op '\o225' : Char) = (op '\149' : Char) %(slash_o225)%,

. (op '\o226' : Char) = (op '\150' : Char) %(slash_o226)%,

. (op '\o227' : Char) = (op '\151' : Char) %(slash_o227)%,

. (op '\o230' : Char) = (op '\152' : Char) %(slash_o230)%,

. (op '\o231' : Char) = (op '\153' : Char) %(slash_o231)%,

. (op '\o232' : Char) = (op '\154' : Char) %(slash_o232)%,

. (op '\o233' : Char) = (op '\155' : Char) %(slash_o233)%,

. (op '\o234' : Char) = (op '\156' : Char) %(slash_o234)%,

. (op '\o235' : Char) = (op '\157' : Char) %(slash_o235)%,

. (op '\o236' : Char) = (op '\158' : Char) %(slash_o236)%,

. (op '\o237' : Char) = (op '\159' : Char) %(slash_o237)%,

. (op '\o240' : Char) = (op '\160' : Char) %(slash_o240)%,

. (op '\o241' : Char) = (op '\161' : Char) %(slash_o241)%,

. (op '\o242' : Char) = (op '\162' : Char) %(slash_o242)%,

. (op '\o243' : Char) = (op '\163' : Char) %(slash_o243)%,

. (op '\o244' : Char) = (op '\164' : Char) %(slash_o244)%,

. (op '\o245' : Char) = (op '\165' : Char) %(slash_o245)%,

. (op '\o246' : Char) = (op '\166' : Char) %(slash_o246)%,

. (op '\o247' : Char) = (op '\167' : Char) %(slash_o247)%,

. (op '\o250' : Char) = (op '\168' : Char) %(slash_o250)%,

. (op '\o251' : Char) = (op '\169' : Char) %(slash_o251)%,

. (op '\o252' : Char) = (op '\170' : Char) %(slash_o252)%,

. (op '\o253' : Char) = (op '\171' : Char) %(slash_o253)%,

. (op '\o254' : Char) = (op '\172' : Char) %(slash_o254)%,

. (op '\o255' : Char) = (op '\173' : Char) %(slash_o255)%,

. (op '\o256' : Char) = (op '\174' : Char) %(slash_o256)%,

. (op '\o257' : Char) = (op '\175' : Char) %(slash_o257)%,

. (op '\o260' : Char) = (op '\176' : Char) %(slash_o260)%,

. (op '\o261' : Char) = (op '\177' : Char) %(slash_o261)%,

. (op '\o262' : Char) = (op '\178' : Char) %(slash_o262)%,

. (op '\o263' : Char) = (op '\179' : Char) %(slash_o263)%,

. (op '\o264' : Char) = (op '\180' : Char) %(slash_o264)%,

. (op '\o265' : Char) = (op '\181' : Char) %(slash_o265)%,

. (op '\o266' : Char) = (op '\182' : Char) %(slash_o266)%,

. (op '\o267' : Char) = (op '\183' : Char) %(slash_o267)%,

. (op '\o270' : Char) = (op '\184' : Char) %(slash_o270)%,

. (op '\o271' : Char) = (op '\185' : Char) %(slash_o271)%,

. (op '\o272' : Char) = (op '\186' : Char) %(slash_o272)%,

. (op '\o273' : Char) = (op '\187' : Char) %(slash_o273)%,

. (op '\o274' : Char) = (op '\188' : Char) %(slash_o274)%,

. (op '\o275' : Char) = (op '\189' : Char) %(slash_o275)%,

. (op '\o276' : Char) = (op '\190' : Char) %(slash_o276)%,

. (op '\o277' : Char) = (op '\191' : Char) %(slash_o277)%,

. (op '\o300' : Char) = (op '\192' : Char) %(slash_o300)%,

. (op '\o301' : Char) = (op '\193' : Char) %(slash_o301)%,

. (op '\o302' : Char) = (op '\194' : Char) %(slash_o302)%,

. (op '\o303' : Char) = (op '\195' : Char) %(slash_o303)%,

. (op '\o304' : Char) = (op '\196' : Char) %(slash_o304)%,

. (op '\o305' : Char) = (op '\197' : Char) %(slash_o305)%,

. (op '\o306' : Char) = (op '\198' : Char) %(slash_o306)%,

. (op '\o307' : Char) = (op '\199' : Char) %(slash_o307)%,

. (op '\o310' : Char) = (op '\200' : Char) %(slash_o310)%,

. (op '\o311' : Char) = (op '\201' : Char) %(slash_o311)%,

. (op '\o312' : Char) = (op '\202' : Char) %(slash_o312)%,

. (op '\o313' : Char) = (op '\203' : Char) %(slash_o313)%,

. (op '\o314' : Char) = (op '\204' : Char) %(slash_o314)%,

. (op '\o315' : Char) = (op '\205' : Char) %(slash_o315)%,

. (op '\o316' : Char) = (op '\206' : Char) %(slash_o316)%,

. (op '\o317' : Char) = (op '\207' : Char) %(slash_o317)%,

. (op '\o320' : Char) = (op '\208' : Char) %(slash_o320)%,

. (op '\o321' : Char) = (op '\209' : Char) %(slash_o321)%,

. (op '\o322' : Char) = (op '\210' : Char) %(slash_o322)%,

. (op '\o323' : Char) = (op '\211' : Char) %(slash_o323)%,

. (op '\o324' : Char) = (op '\212' : Char) %(slash_o324)%,

. (op '\o325' : Char) = (op '\213' : Char) %(slash_o325)%,

. (op '\o326' : Char) = (op '\214' : Char) %(slash_o326)%,

. (op '\o327' : Char) = (op '\215' : Char) %(slash_o327)%,

. (op '\o330' : Char) = (op '\216' : Char) %(slash_o330)%,

. (op '\o331' : Char) = (op '\217' : Char) %(slash_o331)%,

. (op '\o332' : Char) = (op '\218' : Char) %(slash_o332)%,

. (op '\o333' : Char) = (op '\219' : Char) %(slash_o333)%,

. (op '\o334' : Char) = (op '\220' : Char) %(slash_o334)%,

. (op '\o335' : Char) = (op '\221' : Char) %(slash_o335)%,

. (op '\o336' : Char) = (op '\222' : Char) %(slash_o336)%,

. (op '\o337' : Char) = (op '\223' : Char) %(slash_o337)%,

. (op '\o340' : Char) = (op '\224' : Char) %(slash_o340)%,

. (op '\o341' : Char) = (op '\225' : Char) %(slash_o341)%,

. (op '\o342' : Char) = (op '\226' : Char) %(slash_o342)%,

. (op '\o343' : Char) = (op '\227' : Char) %(slash_o343)%,

. (op '\o344' : Char) = (op '\228' : Char) %(slash_o344)%,

. (op '\o345' : Char) = (op '\229' : Char) %(slash_o345)%,

. (op '\o346' : Char) = (op '\230' : Char) %(slash_o346)%,

. (op '\o347' : Char) = (op '\231' : Char) %(slash_o347)%,

. (op '\o350' : Char) = (op '\232' : Char) %(slash_o350)%,

. (op '\o351' : Char) = (op '\233' : Char) %(slash_o351)%,

. (op '\o352' : Char) = (op '\234' : Char) %(slash_o352)%,

. (op '\o353' : Char) = (op '\235' : Char) %(slash_o353)%,

. (op '\o354' : Char) = (op '\236' : Char) %(slash_o354)%,

. (op '\o355' : Char) = (op '\237' : Char) %(slash_o355)%,

. (op '\o356' : Char) = (op '\238' : Char) %(slash_o356)%,

. (op '\o357' : Char) = (op '\239' : Char) %(slash_o357)%,

. (op '\o360' : Char) = (op '\240' : Char) %(slash_o360)%,

. (op '\o361' : Char) = (op '\241' : Char) %(slash_o361)%,

. (op '\o362' : Char) = (op '\242' : Char) %(slash_o362)%,

. (op '\o363' : Char) = (op '\243' : Char) %(slash_o363)%,

. (op '\o364' : Char) = (op '\244' : Char) %(slash_o364)%,

. (op '\o365' : Char) = (op '\245' : Char) %(slash_o365)%,

. (op '\o366' : Char) = (op '\246' : Char) %(slash_o366)%,

. (op '\o367' : Char) = (op '\247' : Char) %(slash_o367)%,

. (op '\o370' : Char) = (op '\248' : Char) %(slash_o370)%,

. (op '\o371' : Char) = (op '\249' : Char) %(slash_o371)%,

. (op '\o372' : Char) = (op '\250' : Char) %(slash_o372)%,

. (op '\o373' : Char) = (op '\251' : Char) %(slash_o373)%,

. (op '\o374' : Char) = (op '\252' : Char) %(slash_o374)%,

. (op '\o375' : Char) = (op '\253' : Char) %(slash_o375)%,

. (op '\o376' : Char) = (op '\254' : Char) %(slash_o376)%,

. (op '\o377' : Char) = (op '\255' : Char) %(slash_o377)%,

. (op '\x00' : Char) = (op '\000' : Char) %(slash_x00)%,

. (op '\x01' : Char) = (op '\001' : Char) %(slash_x01)%,

. (op '\x02' : Char) = (op '\002' : Char) %(slash_x02)%,

. (op '\x03' : Char) = (op '\003' : Char) %(slash_x03)%,

. (op '\x04' : Char) = (op '\004' : Char) %(slash_x04)%,

. (op '\x05' : Char) = (op '\005' : Char) %(slash_x05)%,

. (op '\x06' : Char) = (op '\006' : Char) %(slash_x06)%,

. (op '\x07' : Char) = (op '\007' : Char) %(slash_x07)%,

. (op '\x08' : Char) = (op '\008' : Char) %(slash_x08)%,

. (op '\x09' : Char) = (op '\009' : Char) %(slash_x09)%,

. (op '\x0A' : Char) = (op '\010' : Char) %(slash_x0A)%,

. (op '\x0B' : Char) = (op '\011' : Char) %(slash_x0B)%,

. (op '\x0C' : Char) = (op '\012' : Char) %(slash_x0C)%,

. (op '\x0D' : Char) = (op '\013' : Char) %(slash_x0D)%,

. (op '\x0E' : Char) = (op '\014' : Char) %(slash_x0E)%,

. (op '\x0F' : Char) = (op '\015' : Char) %(slash_x0F)%,

. (op '\x10' : Char) = (op '\016' : Char) %(slash_x10)%,

. (op '\x11' : Char) = (op '\017' : Char) %(slash_x11)%,

. (op '\x12' : Char) = (op '\018' : Char) %(slash_x12)%,

. (op '\x13' : Char) = (op '\019' : Char) %(slash_x13)%,

. (op '\x14' : Char) = (op '\020' : Char) %(slash_x14)%,

. (op '\x15' : Char) = (op '\021' : Char) %(slash_x15)%,

. (op '\x16' : Char) = (op '\022' : Char) %(slash_x16)%,

. (op '\x17' : Char) = (op '\023' : Char) %(slash_x17)%,

. (op '\x18' : Char) = (op '\024' : Char) %(slash_x18)%,

. (op '\x19' : Char) = (op '\025' : Char) %(slash_x19)%,

. (op '\x1A' : Char) = (op '\026' : Char) %(slash_x1A)%,

. (op '\x1B' : Char) = (op '\027' : Char) %(slash_x1B)%,

. (op '\x1C' : Char) = (op '\028' : Char) %(slash_x1C)%,

. (op '\x1D' : Char) = (op '\029' : Char) %(slash_x1D)%,

. (op '\x1E' : Char) = (op '\030' : Char) %(slash_x1E)%,

. (op '\x1F' : Char) = (op '\031' : Char) %(slash_x1F)%,

. (op '\x20' : Char) = (op '\032' : Char) %(slash_x20)%,

. (op '\x21' : Char) = (op '\033' : Char) %(slash_x21)%,

. (op '\x22' : Char) = (op '\034' : Char) %(slash_x22)%,

. (op '\x23' : Char) = (op '\035' : Char) %(slash_x23)%,

. (op '\x24' : Char) = (op '\036' : Char) %(slash_x24)%,

. (op '\x25' : Char) = (op '\037' : Char) %(slash_x25)%,

. (op '\x26' : Char) = (op '\038' : Char) %(slash_x26)%,

. (op '\x27' : Char) = (op '\039' : Char) %(slash_x27)%,

. (op '\x28' : Char) = (op '\040' : Char) %(slash_x28)%,

. (op '\x29' : Char) = (op '\041' : Char) %(slash_x29)%,

. (op '\x2A' : Char) = (op '\042' : Char) %(slash_x2A)%,

. (op '\x2B' : Char) = (op '\043' : Char) %(slash_x2B)%,

. (op '\x2C' : Char) = (op '\044' : Char) %(slash_x2C)%,

. (op '\x2D' : Char) = (op '\045' : Char) %(slash_x2D)%,

. (op '\x2E' : Char) = (op '\046' : Char) %(slash_x2E)%,

. (op '\x2F' : Char) = (op '\047' : Char) %(slash_x2F)%,

. (op '\x30' : Char) = (op '\048' : Char) %(slash_x30)%,

. (op '\x31' : Char) = (op '\049' : Char) %(slash_x31)%,

. (op '\x32' : Char) = (op '\050' : Char) %(slash_x32)%,

. (op '\x33' : Char) = (op '\051' : Char) %(slash_x33)%,

. (op '\x34' : Char) = (op '\052' : Char) %(slash_x34)%,

. (op '\x35' : Char) = (op '\053' : Char) %(slash_x35)%,

. (op '\x36' : Char) = (op '\054' : Char) %(slash_x36)%,

. (op '\x37' : Char) = (op '\055' : Char) %(slash_x37)%,

. (op '\x38' : Char) = (op '\056' : Char) %(slash_x38)%,

. (op '\x39' : Char) = (op '\057' : Char) %(slash_x39)%,

. (op '\x3A' : Char) = (op '\058' : Char) %(slash_x3A)%,

. (op '\x3B' : Char) = (op '\059' : Char) %(slash_x3B)%,

. (op '\x3C' : Char) = (op '\060' : Char) %(slash_x3C)%,

. (op '\x3D' : Char) = (op '\061' : Char) %(slash_x3D)%,

. (op '\x3E' : Char) = (op '\062' : Char) %(slash_x3E)%,

. (op '\x3F' : Char) = (op '\063' : Char) %(slash_x3F)%,

. (op '\x40' : Char) = (op '\064' : Char) %(slash_x40)%,

. (op '\x41' : Char) = (op '\065' : Char) %(slash_x41)%,

. (op '\x42' : Char) = (op '\066' : Char) %(slash_x42)%,

. (op '\x43' : Char) = (op '\067' : Char) %(slash_x43)%,

. (op '\x44' : Char) = (op '\068' : Char) %(slash_x44)%,

. (op '\x45' : Char) = (op '\069' : Char) %(slash_x45)%,

. (op '\x46' : Char) = (op '\070' : Char) %(slash_x46)%,

. (op '\x47' : Char) = (op '\071' : Char) %(slash_x47)%,

. (op '\x48' : Char) = (op '\072' : Char) %(slash_x48)%,

. (op '\x49' : Char) = (op '\073' : Char) %(slash_x49)%,

. (op '\x4A' : Char) = (op '\074' : Char) %(slash_x4A)%,

. (op '\x4B' : Char) = (op '\075' : Char) %(slash_x4B)%,

. (op '\x4C' : Char) = (op '\076' : Char) %(slash_x4C)%,

. (op '\x4D' : Char) = (op '\077' : Char) %(slash_x4D)%,

. (op '\x4E' : Char) = (op '\078' : Char) %(slash_x4E)%,

. (op '\x4F' : Char) = (op '\079' : Char) %(slash_x4F)%,

. (op '\x50' : Char) = (op '\080' : Char) %(slash_x50)%,

. (op '\x51' : Char) = (op '\081' : Char) %(slash_x51)%,

. (op '\x52' : Char) = (op '\082' : Char) %(slash_x52)%,

. (op '\x53' : Char) = (op '\083' : Char) %(slash_x53)%,

. (op '\x54' : Char) = (op '\084' : Char) %(slash_x54)%,

. (op '\x55' : Char) = (op '\085' : Char) %(slash_x55)%,

. (op '\x56' : Char) = (op '\086' : Char) %(slash_x56)%,

. (op '\x57' : Char) = (op '\087' : Char) %(slash_x57)%,

. (op '\x58' : Char) = (op '\088' : Char) %(slash_x58)%,

. (op '\x59' : Char) = (op '\089' : Char) %(slash_x59)%,

. (op '\x5A' : Char) = (op '\090' : Char) %(slash_x5A)%,

. (op '\x5B' : Char) = (op '\091' : Char) %(slash_x5B)%,

. (op '\x5C' : Char) = (op '\092' : Char) %(slash_x5C)%,

. (op '\x5D' : Char) = (op '\093' : Char) %(slash_x5D)%,

. (op '\x5E' : Char) = (op '\094' : Char) %(slash_x5E)%,

. (op '\x5F' : Char) = (op '\095' : Char) %(slash_x5F)%,

. (op '\x60' : Char) = (op '\096' : Char) %(slash_x60)%,

. (op '\x61' : Char) = (op '\097' : Char) %(slash_x61)%,

. (op '\x62' : Char) = (op '\098' : Char) %(slash_x62)%,

. (op '\x63' : Char) = (op '\099' : Char) %(slash_x63)%,

. (op '\x64' : Char) = (op '\100' : Char) %(slash_x64)%,

. (op '\x65' : Char) = (op '\101' : Char) %(slash_x65)%,

. (op '\x66' : Char) = (op '\102' : Char) %(slash_x66)%,

. (op '\x67' : Char) = (op '\103' : Char) %(slash_x67)%,

. (op '\x68' : Char) = (op '\104' : Char) %(slash_x68)%,

. (op '\x69' : Char) = (op '\105' : Char) %(slash_x69)%,

. (op '\x6A' : Char) = (op '\106' : Char) %(slash_x6A)%,

. (op '\x6B' : Char) = (op '\107' : Char) %(slash_x6B)%,

. (op '\x6C' : Char) = (op '\108' : Char) %(slash_x6C)%,

. (op '\x6D' : Char) = (op '\109' : Char) %(slash_x6D)%,

. (op '\x6E' : Char) = (op '\110' : Char) %(slash_x6E)%,

. (op '\x6F' : Char) = (op '\111' : Char) %(slash_x6F)%,

. (op '\x70' : Char) = (op '\112' : Char) %(slash_x70)%,

. (op '\x71' : Char) = (op '\113' : Char) %(slash_x71)%,

. (op '\x72' : Char) = (op '\114' : Char) %(slash_x72)%,

. (op '\x73' : Char) = (op '\115' : Char) %(slash_x73)%,

. (op '\x74' : Char) = (op '\116' : Char) %(slash_x74)%,

. (op '\x75' : Char) = (op '\117' : Char) %(slash_x75)%,

. (op '\x76' : Char) = (op '\118' : Char) %(slash_x76)%,

. (op '\x77' : Char) = (op '\119' : Char) %(slash_x77)%,

. (op '\x78' : Char) = (op '\120' : Char) %(slash_x78)%,

. (op '\x79' : Char) = (op '\121' : Char) %(slash_x79)%,

. (op '\x7A' : Char) = (op '\122' : Char) %(slash_x7A)%,

. (op '\x7B' : Char) = (op '\123' : Char) %(slash_x7B)%,

. (op '\x7C' : Char) = (op '\124' : Char) %(slash_x7C)%,

. (op '\x7D' : Char) = (op '\125' : Char) %(slash_x7D)%,

. (op '\x7E' : Char) = (op '\126' : Char) %(slash_x7E)%,

. (op '\x7F' : Char) = (op '\127' : Char) %(slash_x7F)%,

. (op '\x80' : Char) = (op '\128' : Char) %(slash_x80)%,

. (op '\x81' : Char) = (op '\129' : Char) %(slash_x81)%,

. (op '\x82' : Char) = (op '\130' : Char) %(slash_x82)%,

. (op '\x83' : Char) = (op '\131' : Char) %(slash_x83)%,

. (op '\x84' : Char) = (op '\132' : Char) %(slash_x84)%,

. (op '\x85' : Char) = (op '\133' : Char) %(slash_x85)%,

. (op '\x86' : Char) = (op '\134' : Char) %(slash_x86)%,

. (op '\x87' : Char) = (op '\135' : Char) %(slash_x87)%,

. (op '\x88' : Char) = (op '\136' : Char) %(slash_x88)%,

. (op '\x89' : Char) = (op '\137' : Char) %(slash_x89)%,

. (op '\x8A' : Char) = (op '\138' : Char) %(slash_x8A)%,

. (op '\x8B' : Char) = (op '\139' : Char) %(slash_x8B)%,

. (op '\x8C' : Char) = (op '\140' : Char) %(slash_x8C)%,

. (op '\x8D' : Char) = (op '\141' : Char) %(slash_x8D)%,

. (op '\x8E' : Char) = (op '\142' : Char) %(slash_x8E)%,

. (op '\x8F' : Char) = (op '\143' : Char) %(slash_x8F)%,

. (op '\x90' : Char) = (op '\144' : Char) %(slash_x90)%,

. (op '\x91' : Char) = (op '\145' : Char) %(slash_x91)%,

. (op '\x92' : Char) = (op '\146' : Char) %(slash_x92)%,

. (op '\x93' : Char) = (op '\147' : Char) %(slash_x93)%,

. (op '\x94' : Char) = (op '\148' : Char) %(slash_x94)%,

. (op '\x95' : Char) = (op '\149' : Char) %(slash_x95)%,

. (op '\x96' : Char) = (op '\150' : Char) %(slash_x96)%,

. (op '\x97' : Char) = (op '\151' : Char) %(slash_x97)%,

. (op '\x98' : Char) = (op '\152' : Char) %(slash_x98)%,

. (op '\x99' : Char) = (op '\153' : Char) %(slash_x99)%,

. (op '\x9A' : Char) = (op '\154' : Char) %(slash_x9A)%,

. (op '\x9B' : Char) = (op '\155' : Char) %(slash_x9B)%,

. (op '\x9C' : Char) = (op '\156' : Char) %(slash_x9C)%,

. (op '\x9D' : Char) = (op '\157' : Char) %(slash_x9D)%,

. (op '\x9E' : Char) = (op '\158' : Char) %(slash_x9E)%,

. (op '\x9F' : Char) = (op '\159' : Char) %(slash_x9F)%,

. (op '\xA0' : Char) = (op '\160' : Char) %(slash_xA0)%,

. (op '\xA1' : Char) = (op '\161' : Char) %(slash_xA1)%,

. (op '\xA2' : Char) = (op '\162' : Char) %(slash_xA2)%,

. (op '\xA3' : Char) = (op '\163' : Char) %(slash_xA3)%,

. (op '\xA4' : Char) = (op '\164' : Char) %(slash_xA4)%,

. (op '\xA5' : Char) = (op '\165' : Char) %(slash_xA5)%,

. (op '\xA6' : Char) = (op '\166' : Char) %(slash_xA6)%,

. (op '\xA7' : Char) = (op '\167' : Char) %(slash_xA7)%,

. (op '\xA8' : Char) = (op '\168' : Char) %(slash_xA8)%,

. (op '\xA9' : Char) = (op '\169' : Char) %(slash_xA9)%,

. (op '\xAA' : Char) = (op '\170' : Char) %(slash_xAA)%,

. (op '\xAB' : Char) = (op '\171' : Char) %(slash_xAB)%,

. (op '\xAC' : Char) = (op '\172' : Char) %(slash_xAC)%,

. (op '\xAD' : Char) = (op '\173' : Char) %(slash_xAD)%,

. (op '\xAE' : Char) = (op '\174' : Char) %(slash_xAE)%,

. (op '\xAF' : Char) = (op '\175' : Char) %(slash_xAF)%,

. (op '\xB0' : Char) = (op '\176' : Char) %(slash_xB0)%,

. (op '\xB1' : Char) = (op '\177' : Char) %(slash_xB1)%,

. (op '\xB2' : Char) = (op '\178' : Char) %(slash_xB2)%,

. (op '\xB3' : Char) = (op '\179' : Char) %(slash_xB3)%,

. (op '\xB4' : Char) = (op '\180' : Char) %(slash_xB4)%,

. (op '\xB5' : Char) = (op '\181' : Char) %(slash_xB5)%,

. (op '\xB6' : Char) = (op '\182' : Char) %(slash_xB6)%,

. (op '\xB7' : Char) = (op '\183' : Char) %(slash_xB7)%,

. (op '\xB8' : Char) = (op '\184' : Char) %(slash_xB8)%,

. (op '\xB9' : Char) = (op '\185' : Char) %(slash_xB9)%,

. (op '\xBA' : Char) = (op '\186' : Char) %(slash_xBA)%,

. (op '\xBB' : Char) = (op '\187' : Char) %(slash_xBB)%,

. (op '\xBC' : Char) = (op '\188' : Char) %(slash_xBC)%,

. (op '\xBD' : Char) = (op '\189' : Char) %(slash_xBD)%,

. (op '\xBE' : Char) = (op '\190' : Char) %(slash_xBE)%,

. (op '\xBF' : Char) = (op '\191' : Char) %(slash_xBF)%,

. (op '\xC0' : Char) = (op '\192' : Char) %(slash_xC0)%,

. (op '\xC1' : Char) = (op '\193' : Char) %(slash_xC1)%,

. (op '\xC2' : Char) = (op '\194' : Char) %(slash_xC2)%,

. (op '\xC3' : Char) = (op '\195' : Char) %(slash_xC3)%,

. (op '\xC4' : Char) = (op '\196' : Char) %(slash_xC4)%,

. (op '\xC5' : Char) = (op '\197' : Char) %(slash_xC5)%,

. (op '\xC6' : Char) = (op '\198' : Char) %(slash_xC6)%,

. (op '\xC7' : Char) = (op '\199' : Char) %(slash_xC7)%,

. (op '\xC8' : Char) = (op '\200' : Char) %(slash_xC8)%,

. (op '\xC9' : Char) = (op '\201' : Char) %(slash_xC9)%,

. (op '\xCA' : Char) = (op '\202' : Char) %(slash_xCA)%,

. (op '\xCB' : Char) = (op '\203' : Char) %(slash_xCB)%,

. (op '\xCC' : Char) = (op '\204' : Char) %(slash_xCC)%,

. (op '\xCD' : Char) = (op '\205' : Char) %(slash_xCD)%,

. (op '\xCE' : Char) = (op '\206' : Char) %(slash_xCE)%,

. (op '\xCF' : Char) = (op '\207' : Char) %(slash_xCF)%,

. (op '\xD0' : Char) = (op '\208' : Char) %(slash_xD0)%,

. (op '\xD1' : Char) = (op '\209' : Char) %(slash_xD1)%,

. (op '\xD2' : Char) = (op '\210' : Char) %(slash_xD2)%,

. (op '\xD3' : Char) = (op '\211' : Char) %(slash_xD3)%,

. (op '\xD4' : Char) = (op '\212' : Char) %(slash_xD4)%,

. (op '\xD5' : Char) = (op '\213' : Char) %(slash_xD5)%,

. (op '\xD6' : Char) = (op '\214' : Char) %(slash_xD6)%,

. (op '\xD7' : Char) = (op '\215' : Char) %(slash_xD7)%,

. (op '\xD8' : Char) = (op '\216' : Char) %(slash_xD8)%,

. (op '\xD9' : Char) = (op '\217' : Char) %(slash_xD9)%,

. (op '\xDA' : Char) = (op '\218' : Char) %(slash_xDA)%,

. (op '\xDB' : Char) = (op '\219' : Char) %(slash_xDB)%,

. (op '\xDC' : Char) = (op '\220' : Char) %(slash_xDC)%,

. (op '\xDD' : Char) = (op '\221' : Char) %(slash_xDD)%,

. (op '\xDE' : Char) = (op '\222' : Char) %(slash_xDE)%,

. (op '\xDF' : Char) = (op '\223' : Char) %(slash_xDF)%,

. (op '\xE0' : Char) = (op '\224' : Char) %(slash_xE0)%,

. (op '\xE1' : Char) = (op '\225' : Char) %(slash_xE1)%,

. (op '\xE2' : Char) = (op '\226' : Char) %(slash_xE2)%,

. (op '\xE3' : Char) = (op '\227' : Char) %(slash_xE3)%,

. (op '\xE4' : Char) = (op '\228' : Char) %(slash_xE4)%,

. (op '\xE5' : Char) = (op '\229' : Char) %(slash_xE5)%,

. (op '\xE6' : Char) = (op '\230' : Char) %(slash_xE6)%,

. (op '\xE7' : Char) = (op '\231' : Char) %(slash_xE7)%,

. (op '\xE8' : Char) = (op '\232' : Char) %(slash_xE8)%,

. (op '\xE9' : Char) = (op '\233' : Char) %(slash_xE9)%,

. (op '\xEA' : Char) = (op '\234' : Char) %(slash_xEA)%,

. (op '\xEB' : Char) = (op '\235' : Char) %(slash_xEB)%,

. (op '\xEC' : Char) = (op '\236' : Char) %(slash_xEC)%,

. (op '\xED' : Char) = (op '\237' : Char) %(slash_xED)%,

. (op '\xEE' : Char) = (op '\238' : Char) %(slash_xEE)%,

. (op '\xEF' : Char) = (op '\239' : Char) %(slash_xEF)%,

. (op '\xF0' : Char) = (op '\240' : Char) %(slash_xF0)%,

. (op '\xF1' : Char) = (op '\241' : Char) %(slash_xF1)%,

. (op '\xF2' : Char) = (op '\242' : Char) %(slash_xF2)%,

. (op '\xF3' : Char) = (op '\243' : Char) %(slash_xF3)%,

. (op '\xF4' : Char) = (op '\244' : Char) %(slash_xF4)%,

. (op '\xF5' : Char) = (op '\245' : Char) %(slash_xF5)%,

. (op '\xF6' : Char) = (op '\246' : Char) %(slash_xF6)%,

. (op '\xF7' : Char) = (op '\247' : Char) %(slash_xF7)%,

. (op '\xF8' : Char) = (op '\248' : Char) %(slash_xF8)%,

. (op '\xF9' : Char) = (op '\249' : Char) %(slash_xF9)%,

. (op '\xFA' : Char) = (op '\250' : Char) %(slash_xFA)%,

. (op '\xFB' : Char) = (op '\251' : Char) %(slash_xFB)%,

. (op '\xFC' : Char) = (op '\252' : Char) %(slash_xFC)%,

. (op '\xFD' : Char) = (op '\253' : Char) %(slash_xFD)%,

. (op '\xFE' : Char) = (op '\254' : Char) %(slash_xFE)%,

. (op '\xFF' : Char) = (op '\255' : Char) %(slash_xFF)%,

. (op NUL : Char) = (op '\000' : Char) %(NUL_def)%,

. (op SOH : Char) = (op '\001' : Char) %(SOH_def)%,

. (op SYX : Char) = (op '\002' : Char) %(SYX_def)%,

. (op ETX : Char) = (op '\003' : Char) %(ETX_def)%,

. (op EOT : Char) = (op '\004' : Char) %(EOT_def)%,

. (op ENQ : Char) = (op '\005' : Char) %(ENQ_def)%,

. (op ACK : Char) = (op '\006' : Char) %(ACK_def)%,

. (op BEL : Char) = (op '\007' : Char) %(BEL_def)%,

. (op BS : Char) = (op '\008' : Char) %(BS_def)%,

. (op HT : Char) = (op '\009' : Char) %(HT_def)%,

. (op LF : Char) = (op '\010' : Char) %(LF_def)%,

. (op VT : Char) = (op '\011' : Char) %(VT_def)%,

. (op FF : Char) = (op '\012' : Char) %(FF_def)%,

. (op CR : Char) = (op '\013' : Char) %(CR_def)%,

. (op SO : Char) = (op '\014' : Char) %(SO_def)%,

. (op SI : Char) = (op '\015' : Char) %(SI_def)%,

. (op DLE : Char) = (op '\016' : Char) %(DLE_def)%,

. (op DC1 : Char) = (op '\017' : Char) %(DC1_def)%,

. (op DC2 : Char) = (op '\018' : Char) %(DC2_def)%,

. (op DC3 : Char) = (op '\019' : Char) %(DC3_def)%,

. (op DC4 : Char) = (op '\020' : Char) %(DC4_def)%,

. (op NAK : Char) = (op '\021' : Char) %(NAK_def)%,

. (op SYN : Char) = (op '\022' : Char) %(SYN_def)%,

. (op ETB : Char) = (op '\023' : Char) %(ETB_def)%,

. (op CAN : Char) = (op '\024' : Char) %(CAN_def)%,

. (op EM : Char) = (op '\025' : Char) %(EM_def)%,

. (op SUB : Char) = (op '\026' : Char) %(SUB_def)%,

. (op ESC : Char) = (op '\027' : Char) %(ESC_def)%,

. (op FS : Char) = (op '\028' : Char) %(FS_def)%,

. (op GS : Char) = (op '\029' : Char) %(GS_def)%,

. (op RS : Char) = (op '\030' : Char) %(RS_def)%,

. (op US : Char) = (op '\031' : Char) %(US_def)%,

. (op SP : Char) = (op '\032' : Char) %(SP_def)%,

. (op DEL : Char) = (op '\127' : Char) %(DEL_def)%,

. (op NL : Char) = (op LF : Char) %(NL_def)%,

. (op NP : Char) = (op FF : Char) %(NP_def)%,

. (op '\n' : Char) = (op NL : Char) %(slash_n)%,

. (op '\t' : Char) = (op HT : Char) %(slash_t)%,

. (op '\v' : Char) = (op VT : Char) %(slash_v)%,

. (op '\b' : Char) = (op BS : Char) %(slash_b)%,

. (op '\r' : Char) = (op CR : Char) %(slash_r)%,

. (op '\f' : Char) = (op FF : Char) %(slash_f)%,

. (op '\a' : Char) = (op BEL : Char) %(slash_a)%,

. (op '\?' : Char) = (op '?' : Char) %(slash_quest)%,

. forall x:a; y:a; z:a

. (op __||__ : a * a -> a)((var x : a),

(op __||__ : a * a -> a)((var y : a), (var z : a))) =

(op __||__ : a * a -> a)((op __||__ : a * a -> a)((var x : a),

(var y : a)),

(var z : a)) %(ga_assoc___||__)%,

. (op __||__ : a * a -> a)((op __||__ : a * a -> a)((op b : a),

(op b : a)),

(op b : a)) =

(op b : a) ]

*** Error 261.9, ambiguous mixfix term

__*__(i, __-__(q, __*__(j, p)))

__-__(__*__(i, q), __*__(j, p))

__*__(__*__(i, __-__(q, j)), p)

*** Error 266.16, unknown sort 'a'

*** Error 266.20, unknown sort 'a'

*** Error 268.9, unknown sort 'b'

*** Error 268.6, wrong number of places '__a'

*** Error 268.15, unknown sort 'b'

*** Error 270.3, unexpected mixfix token: a

*** Error 285.17, unknown sort 's2'

*** Error 285.20, unknown sort 's1'

*** Error 285.31, unknown sort 'a'

*** Error 285.34, duplicates at '(285,41)' for 'a : s -> t'

*** Error 285.52, unknown sort 'a'

*** Error 285.25, total selectors 'a : s -> t,b : s -> t,d : s -> t'

must appear in alternative 'c : s'

*** Error 285.50, total selectors 'a : s -> t,b : s -> t,d : s -> t'

must appear in alternative 'c : a ->? s'

*** Error 286.22, unknown sort 's2'

*** Error 286.25, unknown sort 's1'

*** Error 286.36, unknown sort 'a'

*** Error 286.55, unknown sort 'a'

*** Error 286.30, total selectors 'a : s -> t,b : s -> t,d : s -> t'

must appear in alternative 'c : s'

*** Error 286.53, total selectors 'a : s -> t,b : s -> t,d : s -> t'

must appear in alternative 'c : a ->? s'

*** Error 287.27, unknown sort 's2'

*** Error 287.30, unknown sort 's1'

*** Error 287.41, unknown sort 'a'

*** Error 287.60, unknown sort 'a'

*** Error 287.35, total selectors 'a : s -> t,b : s -> t,d : s -> t'

must appear in alternative 'c : s'

*** Error 287.58, total selectors 'a : s -> t,b : s -> t,d : s -> t'

must appear in alternative 'c : a ->? s'

*** Error 290.16, unknown sort 'a'

*** Error 290.20, unknown sort 'a'

*** Error 292.7, unknown sort 'b'

*** Error 292.13, unknown sort 'b'

*** Error 294.17, unknown sort 's2'

*** Error 294.20, unknown sort 's1'

*** Error 294.31, unknown sort 'a'

*** Error 294.38, unknown sort 'a'

*** Error 294.57, unknown sort 'a'

*** Error 294.29, duplicates at '(294,55)' for 'c : a -> s'

*** Error 294.25, total selectors 'a : s -> t,b : s -> t,d : s -> t'

must appear in alternative 'c : s'

*** Error 294.29, total selectors 'a : s -> t,b : s -> t,d : s -> t'

must appear in alternative 'c : a -> s'

*** Error 294.55, total selectors 'a : s -> t,b : s -> t,d : s -> t'

must appear in alternative 'c : a ->? s'

*** Error 304.6, unknown sort 'b'

*** Error 305.6, unknown sort 'd'

*** Error 351.11, wrong number of places '__and'__'

*** Error 118.15, ambiguous term

. (op __-__ : s * s -> s)((op a : s), (var b : s)) =

(op __-__ : s * s -> s)((op c : s), (op d : t))

. (op __-__ : Int * Int -> Int)((var a : Nat), (var b : Nat)) =

(op __-__ : Int * Int -> Int)((var c : Nat), (var d : Nat))

. (op __-__ : s * s -> s)((var a : s), (var b : s)) =

(op __-__ : s * s -> s)((op c : s), (op d : t))

*** Error 141.26, ambiguous term

. (op __+__ : s * s -> s)((op __-__ : s * s -> s)((op a : s),

(var b : s)),

(op __-__ : s * s -> s)((op c : s), (op d : t))) =

(op __-__ : s * s -> s)((op __+__ : s * s -> s)((op a : s),

(op c : s)),

(op __+__ : s * s -> s)((var b : s), (op d : t)))

. (op __+__ : s * s -> s)((op __-__ : s * s -> s)((op a : s),

(var b : s)),

(op __-__ : s * s -> s)((op c : s), (op d : t))) =

(op __-__ : s * s -> s)((op __+__ : s * s -> s)((var a : s),

(op c : s)),

(op __+__ : s * s -> s)((var b : s), (op d : t)))

. (op __+__ : Int * Int -> Int)((op __-__ : Int *

Int -> Int)((var a : Nat), (var b : Nat)),

(op __-__ : Int * Int -> Int)((var c : Nat), (var d : Nat))) =

(op __-__ : Int * Int -> Int)((op __+__ : Nat *

Nat -> Nat)((var a : Nat), (var c : Nat)),

(op __+__ : Nat * Nat -> Nat)((var b : Nat), (var d : Nat)))

. (op __+__ : s * s -> s)((op __-__ : s * s -> s)((var a : s),

(var b : s)),

(op __-__ : s * s -> s)((op c : s), (op d : t))) =

(op __-__ : s * s -> s)((op __+__ : s * s -> s)((op a : s),

(op c : s)),

(op __+__ : s * s -> s)((var b : s), (op d : t)))

. (op __+__ : s * s -> s)((op __-__ : s * s -> s)((var a : s),

(var b : s)),

(op __-__ : s * s -> s)((op c : s), (op d : t))) =

(op __-__ : s * s -> s)((op __+__ : s * s -> s)((var a : s),

(op c : s)),

(op __+__ : s * s -> s)((var b : s), (op d : t)))

*** Error 142.26, ambiguous term

. (op __*__ : s * s -> s)((op __-__ : s * s -> s)((op a : s),

(var b : s)),

(op __-__ : s * s -> s)((op c : s), (op d : t))) =

(op __-__ : s * s -> s)((op __+__ : s * s -> s)((op __*__ : s *

s -> s)((op a : s), (op c : s)),

(op __*__ : s * s -> s)((var b : s),

(op d : t))),

(op __+__ : s * s -> s)((op __*__ : s * s -> s)((var b : s),

(op c : s)),

(op __*__ : s * s -> s)((op a : s),

(op d : t))))

. (op __*__ : s * s -> s)((op __-__ : s * s -> s)((op a : s),

(var b : s)),

(op __-__ : s * s -> s)((op c : s), (op d : t))) =

(op __-__ : s * s -> s)((op __+__ : s * s -> s)((op __*__ : s *

s -> s)((op a : s), (op c : s)),

(op __*__ : s * s -> s)((var b : s),

(op d : t))),

(op __+__ : s * s -> s)((op __*__ : s * s -> s)((var b : s),

(op c : s)),

(op __*__ : s * s -> s)((var a : s),

(op d : t))))

. (op __*__ : s * s -> s)((op __-__ : s * s -> s)((op a : s),

(var b : s)),

(op __-__ : s * s -> s)((op c : s), (op d : t))) =

(op __-__ : s * s -> s)((op __+__ : s * s -> s)((op __*__ : s *

s -> s)((var a : s), (op c : s)),

(op __*__ : s * s -> s)((var b : s),

(op d : t))),

(op __+__ : s * s -> s)((op __*__ : s * s -> s)((var b : s),

(op c : s)),

(op __*__ : s * s -> s)((op a : s),

(op d : t))))

. (op __*__ : s * s -> s)((op __-__ : s * s -> s)((op a : s),

(var b : s)),

(op __-__ : s * s -> s)((op c : s), (op d : t))) =

(op __-__ : s * s -> s)((op __+__ : s * s -> s)((op __*__ : s *

s -> s)((var a : s), (op c : s)),

(op __*__ : s * s -> s)((var b : s),

(op d : t))),

(op __+__ : s * s -> s)((op __*__ : s * s -> s)((var b : s),

(op c : s)),

(op __*__ : s * s -> s)((var a : s),

(op d : t))))

. (op __*__ : Int * Int -> Int)((op __-__ : Int *

Int -> Int)((var a : Nat), (var b : Nat)),

(op __-__ : Int * Int -> Int)((var c : Nat), (var d : Nat))) =

(op __-__ : Int * Int -> Int)((op __+__ : Nat *

Nat -> Nat)((op __*__ : Nat *

Nat -> Nat)((var a : Nat),

(var c : Nat)),

(op __*__ : Nat *

Nat -> Nat)((var b : Nat),

(var d : Nat))),

(op __+__ : Nat * Nat -> Nat)((op __*__ : Nat *

Nat -> Nat)((var b : Nat),

(var c : Nat)),

(op __*__ : Nat *

Nat -> Nat)((var a : Nat),

(var d : Nat))))

*** Error 230.35, ambiguous term

. (var x : Rat) = (var y : Rat)

. (var x : s) = (var y : s)

*** Error 242.12, ambiguous term

. (op __/__ : Rat * Rat ->? Rat)((var x : Rat), (var y : Rat)) =

(var z : Rat)

. (op __/__ : s * s -> s)((var x : s), (var y : s)) = (var z : s)

*** Error 273.5, ambiguous term

. (op a : Data1) = (op a : Data1)

. (op a : b) = (op a : b)

. (op a : s) = (op a : s)

. (op a : s) = (var a : s)

. (var a : s) = (op a : s)

*** Error 274.5, ambiguous term

. (op a : Data1) = (op a : Data1)

. (op a : b) = (op a : b)

. (op a : s) = (op a : s)

. (op a : s) = (var a : s)

. (var a : s) = (op a : s)

*** Error 276.5, ambiguous term

. (op a : Data1) = (op a : Data1)

. (op a : b) = (op a : b)

. (op a : s) = (op a : s)

. (op a : s) = (var a : s)

. (var a : s) = (op a : s)

*** Error 277.5, ambiguous term

. (op a : Data1) = (op a : Data1)

. (op a : b) = (op a : b)

. (op a : s) = (op a : s)

. (op a : s) = (var a : s)

. (var a : s) = (op a : s)

*** Error 279.10, ambiguous term

. (op a : Data1) = (op a : Data1)

. (op a : b) = (op a : b)

. (op a : s) = (op a : s)

. (op a : s) = (var a : s)

. (var a : s) = (op a : s)

*** Error 280.3, ambiguous term

. (op a : Data1) = (op a : Data1)

. (op a : b) = (op a : b)

. (op a : s) = (op a : s)

. (op a : s) = (var a : s)

. (var a : s) = (op a : s)

*** Error 282.9, ambiguous term

. (op a : Data1) = (op a : Data1)

. (op a : b) = (op a : b)

. (op a : s) = (op a : s)

. (op a : s) = (var a : s)

. (var a : s) = (op a : s)

*** Error 283.5, ambiguous term

. (op a : Data1) = (op a : Data1)

. (op a : b) = (op a : b)

. (op a : s) = (op a : s)

. (op a : s) = (var a : s)

. (var a : s) = (op a : s)

*** Error 316.3, ambiguous term

. (op a : Data1) = (op a : Data1)

. (op a : b) = (op a : b)

. (op a : s) = (op a : s)

. (op a : s) = (var a : s)

. (var a : s) = (op a : s)

*** Error 317.3, ambiguous term

. (op a : Data1) = (op a : Data1)

. (op a : b) = (op a : b)

. (op a : s) = (op a : s)

. (op a : s) = (var a : s)

. (var a : s) = (op a : s)

*** Error 320.5, ambiguous term

. (op a : Data1) = (op a : Data1)

. (op a : b) = (op a : b)

. (op a : s) = (op a : s)

. (op a : s) = (var a : s)

. (var a : s) = (op a : s)

*** Error 321.5, ambiguous term

. (op a : Data1) = (op a : Data1)

. (op a : b) = (op a : b)

. (op a : s) = (op a : s)

. (op a : s) = (var a : s)

. (var a : s) = (op a : s)

*** Error 342.5, ambiguous term

(op __@@__ : Nat * Nat -> Nat)((op 1 : Pos), (op 2 : Nat))

(op __@@__ : s * s -> s)((op 1 : s), (op 2 : s))

*** Error 342.20, no operation with 2 arguments found for '__E__'

*** Error 342.32, no operation with 2 arguments found for '__E__'

*** Error 342.45, no operation with 2 arguments found for '__:::__'

*** Error 343.14, no operation with 2 arguments found for '__E__'

*** Error 343.29, no operation with 2 arguments found for '__E__'

*** Error 343.45, no operation with 2 arguments found for '__E__'

*** Error 361.10, ambiguous term

. (op c : s * s -> s)((var x : s), (op a : s)) = (var x : s)

. (op c : s * s -> s)((var x : s), (var a : s)) = (var x : s)

*** Error 361.10, ambiguous term

. (op c : s * s -> s)((op a : s), (var x : s)) = (var x : s)

. (op c : s * s -> s)((var a : s), (var x : s)) = (var x : s)

*** Error 365.9, ambiguous term

. (op c : s * s ->? s)((var x : s), (op a : s)) = (var x : s)

. (op c : s * s ->? s)((var x : s), (var a : s)) = (var x : s)

*** Error 365.9, ambiguous term

. (op c : s * s ->? s)((op a : s), (var x : s)) = (var x : s)

. (op c : s * s ->? s)((var a : s), (var x : s)) = (var x : s)

*** Error 367.9, ambiguous term

. (op a : s) = (op a : s)

. (op a : s) = (var a : s)

*** Error 368.9, ambiguous term

. (op c : s * s * t -> s)((var x : s), (var y : s), (var z : t)) =

(op a : s)

. (op c : s * s * t -> s)((var x : s), (var y : s), (var z : t)) =

(var a : s)

*** Error 369.9, ambiguous term

. (op a :? s) = (op a : s)

. (op a :? s) = (var a : s)

*** Error 370.9, ambiguous term

. (op c : s * s * t ->? s)((var x : s), (var y : s),

(var z : t)) =

(op a : s)

. (op c : s * s * t ->? s)((var x : s), (var y : s),

(var z : t)) =

(var a : s)

*** Error 426.26, no predicate with 0 arguments found for 'e'

*** Error 427.12, no predicate with 0 arguments found for 'e'