// TÉTEL: Kiválasztás //

            // SPECIFIKÁCIÓ //

            Be: honev ∈ S, 
                        honapok ∈ S[1..12] = ["január","február","március","április","május","június","július","augusztus","szeptember","október","november","december"]
            Ki: sorszam ∈ N
            Ef: ∃i ∈ [1..12]: (honev = honapok[i])
            Uf: sorszam = KIVÁLASZT(i>=1, honev = honapok[i])


            // VISSZAVEZETÉS //
            
            ind ~ sorszam
            (1 ~ 1)
            T(elemek[i]) ~ honev = honapok[i]


            //ALGORITMUS //
            
            ind := 1
            Ciklus amíg nem honev = honapok[i]
                ind := ind + 1
            Ciklus vége

            Forrás: 4. előadás 17. o.
            

            // TÉTEL: Megszámolás //

            // SPECIFIKÁCIÓ //

            Be: napdb ∈ N, homersekletek ∈ Z[1..napdb]
            Ki: fagyott ∈ N
            Ef: -
            Uf: fagyott = DARAB(i=1..napdb, homersekletek[i] <= 0)


            // VISSZAVEZETÉS //
            
            db ~ fagyott
            1..elemszám ~ 1..napdb
            T(elemek[i]) ~ homersekletek[i] <= 0


            //ALGORITMUS //
            
            Változó
                i: Egész
            fagyott := 0
            Ciklus i=1-től elemszám-ig
                Ha homersekletek[i] <= 0 akkor fagyott := fagyott + 1
            Ciklus vége

            Forrás: 3. előadás 70. o.
            

            // TÉTEL: Másolás //

            // SPECIFIKÁCIÓ //

            Be: vdb ∈ N, idok ∈ Ido[1..vdb], Ido=(ora:N x perc:N)
            Ki: percek ∈ N[1..vdb]
            Ef: vdb > 0 és ∀i ∈ [1..db]: (1 <= (idok[i].ora*60 + idok[i].perc) <= 600)
            Uf: percek = MÁSOL(i=1..vdb, idok[i].ora*60 + idok[i].perc)


            // VISSZAVEZETÉS //
            
            fvelemek ~ percek
            1..elemszám ~ 1..vdb
            f(elemek[i]) ~ idok[i].ora*60 + idok[i].perc


            //ALGORITMUS //
            
            Változó
                i: Egész
            Ciklus i=1-től vdb-ig
                percek[i] = idok[i].ora*60 + idok[i].perc
            Ciklus vége
            

            // TÉTEL: Eldöntés //

            // SPECIFIKÁCIÓ //

            Be: adb ∈ N, arak ∈ N[1..adb], budzse ∈ N
            Ki: van ∈ L
            Ef: -
            Uf: van = VAN(i=1..adb, arak[i] <= budzse)


            // VISSZAVEZETÉS //
            
            (van ~ van)
            1..elemszám ~ 1..adb
            T(elemek[i]) ~ arak[i] <= budzse


            //ALGORITMUS //
            
            Változó
                i: Egész
            i := 1
            Ciklus amíg i <= adb és nem arak[i] <= budzse
                i := i + 1
            Ciklus vége
            van := i <= adb
            

            // TÉTEL: Minimumkiválasztás //

            // SPECIFIKÁCIÓ //

            Be: napdb ∈ N, hom ∈ Z[1..napdb]
            Ki: minert ∈ Z
            Ef: napdb > 0
            Uf: (,minert) = MIN(i=1..napdb, hom[i])


            // VISSZAVEZETÉS //
            
            (minind ~ -)
            (minért ~ minert)
            1..elemszám ~ 1..napdb
            elemek[i] ~ hom[i]


            //ALGORITMUS //
            
            Változó
                i: Egész
            minert := hom[1]
            Ciklus i=2-től napdb-ig
                Ha hom[i] < minert akkor minert := hom[i]
            Ciklus vége

            Forrás: ~ 3. előadás 77. o.
            

            // TÉTEL: Kiválogatás //

            // SPECIFIKÁCIÓ //

            Be: tdb ∈ N, jegyek ∈ Jegy[1..tdb], Jegy=(nev:S x jegy:N)
            Ki: db ∈ N, kettesek ∈ S[1..db]
            Ef: ∀i ∈ [1..tdb]: (1 <= jegyek[i].jegy <= 5)
            Uf: (db, kettesek) = KIVÁLOGAT(i=1..tdb, jegyek[i].jegy = 2, jegyek[i].nev)


            // VISSZAVEZETÉS //
            
            (db ~ db)
            kivelemek ~ kettesek
            1..elemszám ~ 1..tdb
            T(elemek[i]) ~ jegyek[i].jegy = 2
            elemek[i] ~ jegyek[i].nev


            //ALGORITMUS //
            
            Változó
                i: Egész
            db := 0
            Ciklus i=1-től tdb-ig
                Ha jegyek[i].jegy = 2 akkor
                    db := db + 1
                    kettesek[db] := jegyek[i].nev
                Elágazás vége
            Ciklus vége

            Forrás: ~ 4. előadás 38. o.
            

            // TÉTEL: Mind eldöntés //

            // SPECIFIKÁCIÓ //

            Be: jegydb ∈ N, jegyek ∈ N[1..jegydb]
            Ki: kituno ∈ L
            Ef: jegydb >= 4 és ∀i ∈ [1..jegydb]: (1 <= jegyek[i] <= 5)
            Uf: kituno = MIND(i=1..jegydb, jegyek[i] = 5)


            // VISSZAVEZETÉS //
            
            mind ~ kituno
            1..elemszám ~ 1..jegydb
            T(elemek[i]) ~ jegyek[i] = 5


            //ALGORITMUS //
            
            Változó
                i: Egész
            i := 1
            Ciklus amíg i <= jegydb és jegyek[i] = 5
                i := i + 1
            Ciklus vége
            mind := i > jegydb
            

            // TÉTEL: Összegzés //

            // SPECIFIKÁCIÓ //

            Be: napdb ∈ N, kaloriak ∈ N[1..napdb]
            Ki: atlag ∈ R
            Ef: ∀i ∈ [1..napdb]: (kaloriak[i] >= 0)
            Uf: atlag = SZUM(i=1..napdb, kaloriak[i]) / napdb


            // VISSZAVEZETÉS //
            
            szum ~ atlag
            1..elemszám ~ 1..napdb
            elemek[i] ~ kaloriak[i]


            //ALGORITMUS //
            
            Változó
                i: Egész
            atlag := 0
            Ciklus i=1-től napdb-ig
                atlag := atlag + kaloriak[i]
            Ciklus vége
            atlag := atlag / napdb
            

            // TÉTEL: Keresés //

            // SPECIFIKÁCIÓ //

            Be: fdb ∈ N, filmek ∈ S[1..fdb]
            Ki: van ∈ L, ind ∈ N
            Ef: -
            Uf: (van, ind) = KERES(i=1..fdb, filmek[i] = "Jurassic World")


            // VISSZAVEZETÉS //
            
            (van ~ van)
            (ind ~ ind)
            1..elemszám ~ 1..fdb
            T(elemek[i]) ~ filmek[i] = "Jurassic World"


            //ALGORITMUS //
            
            ind := 1
            Ciklus amíg ind < fdb és nem filmek[i] = "Jurassic World"
                ind := ind + 1
            Ciklus vége
            van := ind <= fdb
            

            // TÉTEL: Maximumkiválasztás //

            // SPECIFIKÁCIÓ //

            Be: kdb ∈ N, oldalak ∈ N[1..kdb]
            Ki: maxind ∈ N, maxert ∈ N
            Ef: -
            Uf: (maxind, maxert) = MAX(i=1..kdb, oldalak[i])


            // VISSZAVEZETÉS //
            
            (maxind ~ maxind)
            (maxért ~ maxert)
            1..elemszám ~ 1..kdb
            elemek[i] ~ oldalak[i]


            //ALGORITMUS //
            
            Változó
                i: Egész
            maxind := 1
            maxert := oldalak[1]
            Ciklus i=2-től kdb-ig
                Ha oldalak[i] > maxert akkor
                    maxert := oldalak[i]
                    maxind := i
                Elágazás vége
            Ciklus vége