A továbbiakban legyenek és tetszőleges halmazok, és pedig az alábbi formában felírható halmazok:

ahol és . Amint az a fenti leírásból kiderül az az összes olyan halmaz -est tartalmazza, amelyeknek minden komponense az adott halmaz véges részhalmaza. Hasonlóan az elemei pedig az olyan halmaz -esek, amelyek -beli véges részhalmazokból állnak.

Definíció: TELJESEN DISZJUNKT FELBONTáS Azt mondjuk, hogy teljesen diszjunkt felbontása -nek, ha

Vegyük észre, hogy ha egydimenziós, akkor a teljesen diszjunkt felbontás megegyezik a diszjunkt felbontással, de többdimenziós esetben a teljesen diszjunkt felbontás egy jóval erősebb feltételt jelent.

Definíció: ELEMENKéNT FELDOLGOZHATó FüGGVéNY Legyen . Ha minden minden teljesen diszjunkt felbontására

akkor -et elemenként feldolgozhatónak nevezzük. Példa: Legyen egy teszőleges halmaz, , , . Ekkor elemenként feldolgozható, ui: tekintsük az halmazpár egy tetszőleges , teljesen diszjunkt felbontását. Ekkor a teljesen diszjunkt felbontás definíciója alapján:

Vizsgáljuk most meg az elemenként feldolgozhatóság két kritériumát:

Tehát a – kétváltozós – unió elemenként feldolgozható halmazfüggvény.

A továbbiakban tehát egy elemenként feldolgozható függvény helyettesítési értékének kiszámításával fogunk foglalkozni.

Mielőtt belekezdenénk a feladat specifikálásába és megoldásába bevezetünk két olyan halmazokra vonatkozó parciális értékadást, amelyeket aztán a megoldó programokban primitív műveletnek tekintünk.

10.4.1Egyváltozós-egyértékű eset

Először vizsgáljuk meg azt az esetet, amikor mind , mind egykomponensű, azaz . Ekkor az függvény egy halmazhoz egy másik halmazt rendel.

Oldjuk meg a feladatot ciklussal: az invariánsban azt fogalmazzuk meg, hogy az halmaz a még feldolgozandó elemeket, az halmaz pedig a már feldolgozott elemek szerinti képeinek unióját tartalmazza, azaz

Vizsgáljuk meg a ciklus levezetési szabályának feltételeit:

• -ból az fennállása esetén következik , ezért a ciklus elé az értékadás kerül.

• Az invariánsból esetén következik az utófeltétel, ám ez jó eséllyel nem egy megengedett feltétel (hiszen éppen -et akarjuk kiszámítani). Vegyük észre azonban, hogy elemenkénti feldolgozhatósága miatt esetén is teljesűl (az üres halmaznak két üres halmaz egy teljesen diszjunkt felbontása). Tehát a ciklusfeltétel: .

• Ha (a ciklusfeltétel szerint) nem üres, akkor termináló függvénynek válaszható számossága, azaz .

• számosságát úgy tudjuk csökkenteni, ha elhagyunk belőle egy – benne levő – elemet. Ezt megtehetjük az imént bevezetett parciális értékadással: .

• Írjuk fel a fenti parciális értékadás -re vonatkozó leggyengébb előfeltételét:

  Jól látható, hogy ez -ből nem következik. Vegyük azonban észre, hogy ha egy -beli elem, akkor és -nek egy teljesen diszjunkt felbontása, tehát elemenkénti feldolgozhatósága miatt:

  

  Így az értékadás már majdnem elegendő, hiszen

  .

  Ezt a feltételt összevetve -vel látható, hogy már csak az állítást kell teljesítenünk. Ezt viszont megtehetjük az értékkiválasztással, amelynek a fenti állításra vonatkozó leggyengébb előfeltétele .

Tétel: Ekkor az alábbi program megoldása a specifikált feladatnak:

Bizonyítás: A tétel a fenti levezetésből következik.

10.4.2Kétváltozós-egyértékű eset

Legyen elemenként feldolgozható függvény.

Tétel: Ekkor az alábbi program megoldása a specifikált feladatnak:

Bizonyítás: A tétel az egyváltozós esettel analóg módon levezethető, ha invariáns tulajdonságnak az alábbi állítást:

termináló függvénynek pedig -t választjuk. __

10.4.3Egyváltozós kétértékű eset

Legyen elemenként feldolgozható függvény.

Tétel: Ekkor az alábbi program megoldása a specifikált feladatnak:

Bizonyítás: A tétel levezetése az egyértékű esettől csak az invariáns tulajdonság megválasztásában tér el:

A termináló függvény marad, és a levezetés lépései is megegyeznek.__

10.4.4Általános változat

Legyenek rögzített természetes számok, elemenként feldolgozható függvény, és legyenek az függvények az komponensfüggvényei, azaz .

ahol az permutációja, ,

Az elágazás "ágainak" száma .

Bizonyítás: A tétel az alábbi invariáns tulajdonsággal és termináló függvénnyel formálisan levezethető (a levezetést annak bonyolultsága miatt elhagyjuk):

_