Důkaz:

Nejprve provedeme transformaci na syntaktické úrovni, v dalším kroku pak ověříme její sémantickou korektnost.

Nechť .

• Je-li proces, pak pomocí algoritmu aplikovaného na dostaneneme systém definic CCS rozšířený o množinu definic relevantních procesu :
  
  
• Je-li síť, pak aplikací algoritmu na vstup dostaneme systém definic CCS rozšířený o množinu definic relevantních hierarchii sítě :

  
  

Zkonstruovali jsme systém CCS , v němž jsme proces CCS odpovídající transformovanému systému pojmenovali P. Nyní ukážeme, že tento proces CCS je sémanticky ekvivalentní původnímu systému GCCS . Přesněji řečeno systém může provést přechod pod nějakou akcí a změnit tak svůj stav na stav vyjádřený systémem právě tehdy, je-li odpovídající proces (agent) CCS P schopen provést pod touž akcí přechod do stavu vyjádřeného procesem (agentem) CCS , který vznikl transformací systému . Dokazujeme tedy tvrzení:

Důkaz směru vedeme indukcí vzhledem ke struktuře odvozovacího stromu sémantiky systému (v jistém smyslu tedy ke struktuře systému ). V důkazu se budeme odkazovat na pravidla sémantiky GCCS uvedené v předchozí kapitole.

• Pokud , pak nechť pro nějaké
  
  

  Podle pravidla (1) sémantiky GCCS platí . Dle indukčního předpokladu tedy platí pro odpovídající systém CCS v němž navíc platí: . Z algoritmu plyne, že výraz E má jeden z následujících tvarů

  1. , pak a pro dle sém. pravidla CCS pro prefix máme a tedy .
  2. a určitě pro nějaké vhodné k vyhovující podmínce . Pro dle indukčního předpokladu a pravidla CCS pro sumaci
     máme a tedy .
• Jestliže a pro nějaké
  
  

  
  
  
  
  

  1. 1. Je-li , pak dle pravidla (2) sémantiky GCCS platí . Připomeňme, že dle algoritmu platí , a , ( značí nedefinováno).
     2. Je-li , tak podle pravidla (3) (je-li splněna postranní podmínka, kde ; zejména je volný), také platí . Navíc dle postranní podmínky a algoritmu platí , a . Pokud nekoliduje se jménem volného portu rozhraní j-tého systému (pro j>i) v síti , pak . Jinak v případě kolize je a .

     V obou příp. máme , přičemž systémům a odpovídají dle algoritmu CCS procesy a .

     Z ind. předp. tedy dostáváme (ozn. ), kde je proces CCS popisující systém . Uvažme násl. instanci sém. pravidla pro paralelní kompozici CCS:
     
     Potom podle a z toho, že , a , nebo a dostáváme .

  2. Jestliže , (pro nějaké ) a je splněna postranní podmínka pravidla (4) sémantiky GCCS (tedy zejména je napojen na sběrnici ) dosazením a do tohoto pravidla dostáváme:
     
     

     Systémům a odpovídají dle algoritmu CCS procesy a . Pro akci není v této fázi definována, což plyne z premisy pravidla (4).

     Dle indukčního předpokladu platí (ozn.). Navíc podle algoritmu platí a .

     Uvažujme následující odvození sémantiky CCS pro (pomocí pravidel přejmenování a kompozice CCS):
     
     Pak z  a z toho, že a , dostáváme .

• Jestliže a platí:
  
  

  
  
  
  
  

  Je-li splněna postranní podmínka pravidla (5) sémantiky GCCS pro nějaká vhodná a , (zejména a jsou porty dvou různých podsystémů propojené vnitřní sběrnicí - označme ji ), pak dle tohoto pravidla dostáváme a , kde (resp. ) je systém, který vznikl provedením přechodu v i-tém (resp. j-tém) podsystému sítě .

  Systémům , , a odpovídají dle algoritmu procesy CCS , , a .

  Z ind. předp. máme a . Podle algoritmu platí následující tvrzení:

  • a
  • a
  • a

  Uvažme instanci sém. pravidla pro paralelní kompozici CCS (synchronizace):
  
  

  Celkem tedy z výše uvedených tvrzení dostáváme .

Důkaz směru vedeme indukcí ke struktuře odvozovacího stromu sémantiky výrazu definujícího proces CCS P. V důkazu využijeme faktu, že algoritmus transformace GCCS na CCS definuje jednoznačné přiřazení.

Předpokládejme pro nějaké . Jelikož definice CCS procesu P vznikla transformací systému GCCS , může být jednoho z násl. tvarů:

1. Je-li pro nějaké , pak podle pravidla sém. CCS pro prefix a pravidla pro definici CCS dostáváme . Podle alg. P vzniklo jednozn. transformací a jedn. transformací . Podle indukčního předpokladu máme . Celkem dle pravidla (1) sém. GCCS platí .
2. Je-li pro nějaké , pak podle pravidel sém. CCS pro sumaci a definici celkem Pro tedy máme . Podle alg. P vzniklo jednozn. transformací a jedn. transformací . Podle indukčního předpokladu stejně jako v předchozím případě platí .
3. Nechť pro nějaké a nechť index . Dále nechť (přejmenování propojením portu a sběrnice). Uvědomme si, že (odstranění nežádoucí synchronizace volných portů). Pak pokud provedeme podle pravidel sémantiky CCS následující odvození:

   
   
   

   Podle alg. P vzniklo transformací a transformací .
   Dle indukčního předpokladu máme . Celkem dle pravidla (2) (pokud ), podle pravidla (3) (pokud ) nebo jinak dle pravidla (4) sémantiky GCCS platí .

4. Nechť pro nějaké a . Dále nechť . Pak pokud (tedy ) provedeme podle pravidel sémantiky CCS následující odvození:

   
   
   

   Podle alg. P vzniklo transformací a transformací .
   Z indukčního předpokladu a máme . Celkem dle pravidla (5) sémantiky GCCS platí , kde .

Tím máme dokázáno, že výsledkem aplikace navrhovaných algoritmů na dobře definovaný systém GCCS je jemu sémanticky ekvivalentní CCS výraz.