Legyenek , , , és tetszőleges típusok. Legyen továbbá és , valamint , , és függvények.

Tekintsük az alábbi specifikációval adott feladatot:

Legyenek az és függvényeket kiszámító elemenként előállító programok az alábbiak: ____________________________________________________________ __________________________________________________ ____________ __________________________________________________

és tegyük fel, hogy az előállított és sorozatok rendezettek.

Legyen mint korábban, továbbá tegyük fel, hogy egy olyan kétváltozós egyértékű elemenként feldolgozható függvény, amely minden olyan halmazpárhoz, amelynek tagjai legfeljebb egy elemet tartalmaznak, pontosan egy elemű halmazt rendel hozzá.

Ekkor a függvénykompozíció helyettesítési értékének kiszámítására vonatkozó programozási tétel alapján a feladat megoldható a fenti két elemenként előállító, a kétváltozós egyértékű elemenként feldolgozó és az -at kiszámító elemenként felhasználó program szekvenciájaként. Vajon ebben az esetben is összeinvertálhatóak a fenti programok?

A válasz természetesen: igen, de a megoldás itt nem olyan egyszerű, mint az egyváltozós esetben volt. A probléma a szekvenciális file-oknál felmerülttel analóg: az elemet előállító program ( ill. ) az egyes elemeket ugyanúgy szolgáltatja mintha file-ból olvasnánk őket: csak akkor nézhetjük meg a következő elemet ha legeneráltatjuk. Ez sugallja azt a megoldást, hogy az és sorozatokat tekintsük az elemenként feldolgozásban absztrakt file-oknak. Az elemenként felhasználó program beinvertálása nem okoz gondot, ugyanúgy történik mint az egyváltozós esetben.

ahol az absztrakt műveletek megvalósításai: