{{theorem | A je RM \Leftrightarrow je oborem hodnot nějaké rostoucí úsekové ČRF

| RM=rngRM = rng rostoucí úsekové ČRF }}

Dk ::

 ⁣ \Rightarrow\,\!: Předpokládejme nejprve, že AA je RM. To znamená, že její char. fce χA(x)χ_A(x) je ORF.

:: Popíšeme fci f(i)f(i), která pro dané ii vrátí ii-tý nejmenší prvek množiny AA (počítáme od 0, tj. první prvek je vrácen pro i=0i = 0). :: Je-li AA konečná množina, není pro iAi ≥ |A| hodnota f(i)f(i) definována. Takto popsaná fce bude rostoucí i úseková. :: Intuitivní algoritmus, který bude počítat funkci f(i)f(i) je jednoduchý: :: Najdi nejmenší prvek množiny AA a poté ii-krát hledej nejmenší větší prvek. :: První cyklus while najde index nejmenšího (tedy 0-tého) prvku, který do množiny AA patří. :: Poté algoritmus ii-krát opakuje hledání následujícího prvku. :: Hledání následujícího prvku je obsaženo v druhém cyklu while. :: První inicializační cyklus si definujeme jako ČRF

ParseError: KaTeX parse error: Undefined control sequence: \[ at position 10: h(v) = μy\̲[̲χ_A(y) ≃ 1]

, všimněte si, že tato fce na svém parametru vůbec nezávisí, vždy najde nejmenší prvek množiny AA. :: Funkci uvnitř cyklu for si definujeme jako ČRF

ParseError: KaTeX parse error: Undefined control sequence: \[ at position 16: g(i, u, v) = μz\̲[̲(z > u) ∧ χ_A(z…

. :: Funkce gg dostává jako druhou hodnotu hodnotu z rekurze, tedy aktuální hodnotu naposledy nalezeného prvku, následně hledá nejmenší prvek množiny AA, který je větší než tento poslední nalezený prvek uložený v zz. :: Pomocí primitivní rekurze odvodíme funkci f=R2(h,g)f' = R_2(h, g) a poté stačí položit f(i)f(i,i)f(i) ≃ f' (i, i) :: (připomeňme si, že primitivní rekurze odvodí funkci alespoň dvou proměnných, proto funkci ff odvodíme takovouto oklikou).

 ⁣ \Leftarrow\,\!: Nyní předpokládejme, že A=rngfA = rng f, kde ff je rostoucí úseková ČRF.

:: Pokud ff není ORF, znamená to podle definice úsekové fce, že doména ff je konečná, a tedy je konečná i samotná množina AA a je tedy triviálně rekurzivní. :: Předpokládejme tedy, že ff je obecně rekurzivní, tedy všude definovaná fce, pro kterou platí, že f(i)f(i) vrátí ii-tý nejmenší prvek množiny AA. :: Char. fci můžeme nyní spočítat jednoduchým způsobem. Množina AA je nekonečná, a proto musí obsahovat prvek, který je větší nebo roven xx, ve skutečnosti platí, že ii-tý prvek musí být větší nebo roven ii, jinými slovy platí, že if(i)i ≤ f(i). :: Proto ve skutečnosti stačí hledat ixi ≤ x a mohli bychom se tedy obejít bez obecného cyklu while a nahradit jej cyklem for, toho využijeme při odvození fce χAχ_A. Definujme funkci

ParseError: KaTeX parse error: Undefined control sequence: \[ at position 14: g(x) = μi ≤ x\̲[̲f(i) ≥ x]

. :: Nyní platí, že xAx ∈A, právě když x=f(g(x))x = f(g(x)), přičemž rovnost je primitivně rekurzivní predikát, a proto je charakteristická fce χAχ_A obecně rekurzivní. :: Pokud je ff dokonce PRF, dostaneme, že i χ_A je PRF, neboť omezená minimalizace použitá v odvození fce gg je primitivně rekurzivní. V každém případě je-li ff ORF, je ORF i χAχ_A a AA je tedy RM.