{-# LANGUAGE BangPatterns              #-}
{-# LANGUAGE EmptyCase                 #-}
{-# LANGUAGE EmptyDataDecls            #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE NoMonomorphismRestriction #-}
{-# LANGUAGE OverloadedStrings         #-}
{-# LANGUAGE PatternSynonyms           #-}
{-# LANGUAGE RankNTypes                #-}
{-# LANGUAGE ScopedTypeVariables       #-}

{-# OPTIONS_GHC -Wno-overlapping-patterns #-}

module MAlonzo.Code.Algorithmic.Properties where

import Data.Text qualified
import MAlonzo.Code.Agda.Builtin.Equality qualified
import MAlonzo.Code.Agda.Builtin.Sigma qualified
import MAlonzo.Code.Algorithmic qualified
import MAlonzo.Code.Type.BetaNormal qualified
import MAlonzo.Code.Utils qualified
import MAlonzo.RTE (AgdaAny, add64, addInt, coe, eq64, eqInt, erased, geqInt, lt64, ltInt, mul64,
                    mulInt, quot64, quotInt, rem64, remInt, sub64, subInt, word64FromNat,
                    word64ToNat)
import MAlonzo.RTE qualified

-- Algorithmic.Properties.lem-·⋆
d_lem'45''183''8902'_28 ::
  MAlonzo.Code.Utils.T_Kind_636 ->
  MAlonzo.Code.Utils.T_Kind_636 ->
  MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4 ->
  MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4 ->
  MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4 ->
  MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4 ->
  MAlonzo.Code.Algorithmic.T__'8866'__168 ->
  MAlonzo.Code.Algorithmic.T__'8866'__168 ->
  MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_lem'45''183''8902'_28 :: T_Kind_636
-> T_Kind_636
-> T__'8866'Nf'8902'__4
-> T__'8866'Nf'8902'__4
-> T__'8866'Nf'8902'__4
-> T__'8866'Nf'8902'__4
-> T__'8866'__168
-> T__'8866'__168
-> T__'8866'Nf'8902'__4
-> T__'8801'__12
-> T__'8801'__12
-> T__'8801'__12
-> T_Σ_14
d_lem'45''183''8902'_28 ~T_Kind_636
v0 ~T_Kind_636
v1 ~T__'8866'Nf'8902'__4
v2 ~T__'8866'Nf'8902'__4
v3 ~T__'8866'Nf'8902'__4
v4 ~T__'8866'Nf'8902'__4
v5 ~T__'8866'__168
v6 ~T__'8866'__168
v7 ~T__'8866'Nf'8902'__4
v8 ~T__'8801'__12
v9
                        ~T__'8801'__12
v10 ~T__'8801'__12
v11
  = T_Σ_14
du_lem'45''183''8902'_28
du_lem'45''183''8902'_28 :: MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_lem'45''183''8902'_28 :: T_Σ_14
du_lem'45''183''8902'_28
  = (Any -> Any -> T_Σ_14) -> Any -> Any -> T_Σ_14
forall a b. a -> b
coe
      Any -> Any -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 Any
forall a. a
erased
      ((Any -> Any -> T_Σ_14) -> Any -> Any -> Any
forall a b. a -> b
coe
         Any -> Any -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 Any
forall a. a
erased
         ((Any -> Any -> T_Σ_14) -> Any -> Any -> Any
forall a b. a -> b
coe Any -> Any -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 Any
forall a. a
erased Any
forall a. a
erased))
-- Algorithmic.Properties.lem-unwrap
d_lem'45'unwrap_54 ::
  MAlonzo.Code.Utils.T_Kind_636 ->
  MAlonzo.Code.Utils.T_Kind_636 ->
  MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4 ->
  MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4 ->
  MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4 ->
  MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4 ->
  MAlonzo.Code.Algorithmic.T__'8866'__168 ->
  MAlonzo.Code.Algorithmic.T__'8866'__168 ->
  MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_lem'45'unwrap_54 :: T_Kind_636
-> T_Kind_636
-> T__'8866'Nf'8902'__4
-> T__'8866'Nf'8902'__4
-> T__'8866'Nf'8902'__4
-> T__'8866'Nf'8902'__4
-> T__'8866'__168
-> T__'8866'__168
-> T__'8866'Nf'8902'__4
-> T__'8801'__12
-> T__'8801'__12
-> T__'8801'__12
-> T_Σ_14
d_lem'45'unwrap_54 ~T_Kind_636
v0 ~T_Kind_636
v1 ~T__'8866'Nf'8902'__4
v2 ~T__'8866'Nf'8902'__4
v3 ~T__'8866'Nf'8902'__4
v4 ~T__'8866'Nf'8902'__4
v5 ~T__'8866'__168
v6 ~T__'8866'__168
v7 ~T__'8866'Nf'8902'__4
v8 ~T__'8801'__12
v9 ~T__'8801'__12
v10
                   ~T__'8801'__12
v11
  = T_Σ_14
du_lem'45'unwrap_54
du_lem'45'unwrap_54 :: MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_lem'45'unwrap_54 :: T_Σ_14
du_lem'45'unwrap_54
  = (Any -> Any -> T_Σ_14) -> Any -> Any -> T_Σ_14
forall a b. a -> b
coe
      Any -> Any -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 Any
forall a. a
erased
      ((Any -> Any -> T_Σ_14) -> Any -> Any -> Any
forall a b. a -> b
coe
         Any -> Any -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 Any
forall a. a
erased
         ((Any -> Any -> T_Σ_14) -> Any -> Any -> Any
forall a b. a -> b
coe Any -> Any -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 Any
forall a. a
erased Any
forall a. a
erased))