species

subsentence = sentence | prenex subsentence

prenex = terms ZOhU #

sentence = [[jbocre: terms [jbocre: CU #|CU #]] bridi-tail

bridi-tail = selbri tail-terms | gek-sentence

gek-sentence = gek subsentence gik subsentence tail-terms

| tag KE # gek-sentence /KEhE#/

| NA # gek-sentence

tail-terms = terms /VAU#/

terms = term ...

term = FA sumti

| tag (sumti | /KU#/)

| NA KU #

| NUhI # gek terms /NUhU#/ gik terms /NUhU#/

sumti = quantifier KOhA xi number relative-clauses

| gek sumti gik sumti

selbri = tag selbri-1

selbri-1 = selbri-6 | NA # selbri

For each sentence, while there are terms in front of the selbri, starting from the first term, we export them to the prenex as follows.

If the term is of type "FA quantifier KOhA":

FA quantifier KOhA xi number relative-clauses [[jbocre: terms [jbocre: CU #|CU #]] bridi-tail: is reduced to "quantifier KOhA xi number relative-clauses zo'u FA KOhA [[jbocre: terms [jbocre: CU #|CU #]] bridi-tail" which is a subsentence (prenex sentence)

If the term is of type "tag (quantifier KOhA | /KU#/) | NA KU #" it is exported directly to the prenex:

(tag (quantifier KOhA /KU#/) | NA KU) [[jbocre: terms [jbocre: CU #|CU #]] bridi-tail: is reduced to "(tag (quantifier KOhA /KU#/) | NA KU) zo'u [[jbocre: terms [jbocre: CU #|CU #]] bridi-tail" which is a subsentence (prenex sentence)

If the term is of type "(FA | tag) gek sumti gik sumti", with logical gek:

(FA tag) gek sumti gik sumti [[jbocre: terms [jbocre: CU #|CU #]] bridi-tail: is reduced to tag zo'u gek sumti [[jbocre: terms [jbocre: CU #|CU #]] bridi-tail gik sumti [[jbocre: terms [jbocre: CU #|CU #]] bridi-tail which is a subsentence (prenex sentence)

Note: In the above rule, [[jbocre: terms [jbocre: CU #|CU #]] bridi-tail appears unchanged in the first connectand. In the second connectand, everything is copied unchanged except for unquantified KOhA terms, which move to the second connectand as FA tag KOhA xi number, dropping any relative clauses. Quantified terms may be copied unchanged, but the variable may be changed to a new one for clarity.

If the term is of type NUhI # gek terms /NUhU#/ gik terms /NUhU#/:

NUhI # gek terms /NUhU#/ gik terms /NUhU#/ [[jbocre: terms [jbocre: CU #|CU #]] bridi-tail: is reduced to gek terms [[jbocre: terms [jbocre: CU #|CU #]] bridi-tail gik terms [[jbocre: terms [jbocre: CU #|CU #]] bridi-tail which is a subsentence (prenex sentence)

The same caveat as in the previous case applies.