Wrong inference step in Envelope calculus

[stefborg]

When proving DL25FullPaperAuthor ⊑ DLCommunityMember in dl25example.owl.zip, I get the following proof:

[DL25FullPaperAuthor ⊑ ∃contributesTo.DL, ∃contributesTo.DL ⊑ DLCommunityMember]
--------------------- S(?C, ?D) :- S(?C, ?Cp), http://rulewerk.semantic-web.org/normalForm/subClassOf(?Cp, ?D) .
DL25FullPaperAuthor ⊑ DLCommunityMember

[DL25FullPaperAuthor ⊑ ∃contributesTo.DL25, DL25 ⊑ DL, ∃contributesTo.DL ⊑ ∃contributesTo.DL]
--------------------- S(?C, ?E) :- R(?C, ?R, ?D), S(?D, ?Dp), http://rulewerk.semantic-web.org/normalForm/subClassEx(?R, ?Dp, ?E) .
DL25FullPaperAuthor ⊑ ∃contributesTo.DL

[DL25FullPaperAuthor ⊑ ∃hasPaperAt.DL25, hasPaperAt ⊑ contributesTo]
--------------------- R(?C, ?S, ?D) :- R(?C, ?R, ?D), directSubProp(?R, ?S) .
DL25FullPaperAuthor ⊑ ∃contributesTo.DL25

[DL25FullPaperAuthor ⊑ ∃hasWorkshopPaperAt.DL25, hasWorkshopPaperAt ⊑ hasPaperAt]
--------------------- R(?C, ?S, ?D) :- R(?C, ?R, ?D), directSubProp(?R, ?S) .
DL25FullPaperAuthor ⊑ ∃hasPaperAt.DL25

[DL25FullPaperAuthor ⊑ DL25Author, DL25Author ⊑ ∃hasWorkshopPaperAt.DL25]
--------------------- S(?C, ?D) :- S(?C, ?Cp), http://rulewerk.semantic-web.org/normalForm/subClassOf(?Cp, ?D) .
DL25FullPaperAuthor ⊑ ∃hasWorkshopPaperAt.DL25

[]
--------------------- Asserted
DL25FullPaperAuthor ⊑ DL25Author

[]
--------------------- Asserted
DL25Author ⊑ ∃hasWorkshopPaperAt.DL25

[]
--------------------- Asserted
hasWorkshopPaperAt ⊑ hasPaperAt

[]
--------------------- Asserted
hasPaperAt ⊑ contributesTo

[]
--------------------- Asserted
DL25 ⊑ DL

[]
--------------------- http://rulewerk.semantic-web.org/normalForm/subClassEx(?R, ?B, ?Y), http://rulewerk.semantic-web.org/normalForm/class(?Y) :- http://rulewerk.semantic-web.org/normalForm/exists(?Y, ?R, ?B) .
∃contributesTo.DL ⊑ ∃contributesTo.DL

[]
--------------------- Asserted
∃contributesTo.DL ⊑ DLCommunityMember

But the step

[]
--------------------- http://rulewerk.semantic-web.org/normalForm/subClassEx(?R, ?B, ?Y), http://rulewerk.semantic-web.org/normalForm/class(?Y) :- http://rulewerk.semantic-web.org/normalForm/exists(?Y, ?R, ?B) .
∃contributesTo.DL ⊑ ∃contributesTo.DL

is not a valid step of the calculus, but just a normalization-related rule. This step should not be shown, and the second step from the proof should directly use ∃contributesTo.DL ⊑ DLCommunityMember instead of ∃contributesTo.DL ⊑ ∃contributesTo.DL.