###### tags: `MP`
# MP lista 6

## Zadanie 1.

Przypomnij sobie definicję funkcji map. Następnie pokaż, że dla dowolnych funkcji
`f` i `g` oraz listy `xs` zachodzi `(map f (map g xs))` ~ `(map (lambda (x) (f (g x))) xs)`. Możesz założyć, że funkcje `f` i `g` poprawnie obliczają się do wartości dla
dowolnego argumentu.

### Dowód:

#### Definicja funkcji map

(define (map f xs)
  (if (empty? l)
      (list)
      (cons (f (first xs)) (map f (rest xs)))))

Pokażemy indukcyjnie:
1. Baza indukcji:
Gdy `xs` jest puste mamy:
L = `(map f (map g xs))` ~ `(map f (map g empty))` ~ (z def. map) ~ `(map f empty)` ~ `(empty)`
P = `(map (lambda (x) (f (g x))) xs)` ~ `(map (lambda (x) (f (g x))) empty)` ~ `(empty)`
Korzystając z definicji map otrzymujemy, że L ~ P.
2. Krok indukcyjny:
Załóżmy, że `(map f (map g xs))` ~ `(map (lambda (x) (f (g x))) xs)`, pokażemy `(map f (map g (cons x xs)))` ~ `(map (lambda (x) (f (g x))) (cons x xs))`.
L = `(map f (map g (cons x xs)))` ~ `(map f (cons (g x) (map g xs)))` ~ `(cons (f (g x)) (map f ((map g xs)))` ~ (ind) ~ `(cons (f (g x))(map (lambda (x) (f (g x))) xs))`.
P = `(map (lambda (x) (f (g x))) (cons x xs))` ~ `(cons (lambda (x) (f (g x)) x) (map (lambda (x) (f (g x))) xs))` ~ `(cons (f (g x))) (map (lambda (x) (f (g x))) xs))`, co jak widać jest tym samym co otrzymaliśmy z L, zatem L ~ P.

## Zadanie 2.

Pokaż, że funkcja `append` zawsze oblicza się do wartości, tzn. pokaż, że dla dowolnych list `xs` i `ys` istnieje lista `zs` taka, że `(append xs ys)` ~ `zs`.

### Definicja funkcji append

(define (append xs ys)
    (if (empty? xs)
        ys
        (cons (first xs)
            (append (rest xs) ys))))

### Dowód:

Weźmy dowolne listy `xs` i `ys`. Udowodnimy indukcyjnie (względem `xs`), że `(append xs ys)` oblicza się do wartości.

1. Baza indukcji
Jeśli `xs` jest `empty` to: `(append xs ys)` ~ `(append empty ys)` ~ (L1 z wykładu) ~ `ys`, co jest wartością.

2. Krok indukcyjny
Załóżmy, że istnieje `zs` ~ `(append xs ys)`, pokażemy, że istnieje `ts` ~ `(append (cons x xs) ys)`.
`(append (cons x xs) ys)` ~(cons x xs jest wartością) `(cons x (append xs ys))` ~ (zal. ind.) ~ `(cons x zs)`, zatem skoro `(cons a as)` jest wartością to udowodniliśmy to co trzeba.

## Zadanie 3.

Formuły w negacyjnej postaci normalnej to takie formuły rachunku zdań, w których wszystkie negacje znajdują się przy zmiennych zdaniowych. Dokładniej, formuły w negacyjnej postaci normalnej, składają się z koniunkcji, alternatywy i literałów, gdzie literały to zanegowane lub niezanegowane zmienne zdaniowe. Takie formuły można opisać następującym typem danych, sparametryzowanym typem opisującym zmienne.

( define-type ( NNF 'v )
( nnf-lit [ polarity : Boolean ] [ var : 'v ])
( nnf-conj [ l : ( NNF 'v ) ] [ r : ( NNF 'v ) ])
( nnf-disj [ l : ( NNF 'v ) ] [ r : ( NNF 'v ) ]) )

Flaga `polarity` w konstruktorze literału oznacza, czy zmienna jest zanegowana
(wartość `#f`), czy nie (wartość `#t`). Sformułuj zasadę indukcji dla typu `NNF`.

### Zasada indukcji:

Niech `nnf` to będzie formuła w `NNF`. Niech `P` będzie własnością taką, że:
1. Dla każdego `v` zachodzi:
* `P((nnf #t v))`
* `P((nnf #f v))`
3. Dla każdego `l`, `r` (będących formułami nnf) jeśli `P(l)` i `P(r)` to `P((nnf-conj l r))`
4. Dla każdego `l`, `r` (będących formułami nnf) jeśli `P(l)` i `P(r)` to `P((nnf-disj l r))`

Wówczas dla każdej formuły `nnf` typu `NNF` zachodzi `P(nnf)`.

## Zadanie 4.

Zdefiniuj funkcję `neg-nnf` typu `((NNF 'a) -> (NNF 'a))` negującą formułę w negacyjnej postaci normalnej. Następnie pokaż, że `(neg-nnf (neg-nnf fi))` ~ `fi` dla dowolnej formuły `fi`.

### Definicja funkcji:

(define (neg-nnf fi)
        (cond [(nnf-lit? fi) (if (equal? (nnf-lit-polarity fi) #t) 
                                      (nnf-lit #f (nnf-lit-var fi))
                                      (nnf-lit #t (nnf-lit-var fi)))]
              [(nnf-conj? fi) (nnf-disj (neg-nnf (nnf-conj-l fi))
                                    	(neg-nnf (nnf-conj-r fi)))]
              [(nnf-disj? fi) (nnf-conj (neg-nnf (nnf-disj-l fi))
                                        (neg-nnf (nnf-disj-r fi)))]))

### Dowód:

Dowód indukcyjny względem `fi`:
1. Jeśli `fi` jest literałem:
* Jeśli istnieje `v` takie, że `fi` ~ `(nnf-lit #t v)`
`(neg-nnf (neg-nnf fi))` ~ `(neg-nnf (neg-nnf (nnf-lit #t v)))` ~ `(neg-nnf (nnf-lit #f v))` ~ `(nnf-lit #t v))` ~ `fi`.
* Jeśli istnieje `v` takie, że `fi` ~ `(nnf-lit #f v)`
`(neg-nnf (neg-nnf fi))` ~ `(neg-nnf (neg-nnf (nnf-lit #f v)))` ~ `(neg-nnf (nnf-lit #t v))` ~ `(nnf-lit #f v))` ~ `fi`.
2. Jeśli `fi` ~ `(nnf-conj l r)` to:
Załóżmy, że `(neg-nnf (neg-nnf l))` ~ `l` oraz `(neg-nnf (neg-nnf r))` ~ `r`, pokażemy, że `(neg-nnf (neg-nnf fi))` ~ `fi`.
L = `(neg-nnf (neg-nnf fi))` ~ `(neg-nnf (neg-nnf (nnf-conj l r)))` ~ `(neg-nnf (nnf-disj (neg-nnf l)(neg-nnf r)))` ~ `(neg-nnf (nnf-disj (neg-nnf l)(neg-nnf r)))` ~ `(nnf-conj (neg-nnf (neg-nnf l)) (neg-nnf (neg-nnf r))) ` ~ `(nnf-conj l r)`
P = `fi` ~ `(nnf-conj l r)`.
3. Jeśli `fi` ~ `(nnf-disj l r)` to:
Załóżmy, że `(neg-nnf (neg-nnf l))` ~ `l` oraz `(neg-nnf (neg-nnf r))` ~ `r`, pokażemy, że `(neg-nnf (neg-nnf fi))` ~ `fi`.
L = `(neg-nnf (neg-nnf fi))` ~ `(neg-nnf (neg-nnf (nnf-disj l r)))` ~ `(neg-nnf (nnf-conj (neg-nnf l)(neg-nnf r)))` ~ `(neg-nnf (nnf-conj (neg-nnf l)(neg-nnf r)))` ~ `(nnf-disj (neg-nnf (neg-nnf l)) (neg-nnf (neg-nnf r))) ` ~ `(nnf-disj l r)`
P = `fi` ~ `(nnf-disj l r)`.

Stąd `fi` ~ `(neg-nnf (neg-nnf fi))`.

## Zadanie 5.

Zdefiniuj funkcję `eval-nnf` typu `(('a -> Boolean) (NNF 'a) -> Boolean)` interpretującą formułę w negacyjnej postaci normalnej, przy zadanym wartościowaniu zmiennych (funkcji typu `('a -> Boolean)`). Następnie pokaż, że dla dowolnej formuły `fi` i wartościowania `s` zachodzi `(eval-nnf s (neg-nnf fi))` ~ `(not (eval-nnf s fi))`. Możesz założyć, że funkcja s zawsze się zatrzymuje.

### Definicja:

(define (eval-nnf s fi)
  (cond [(nnf-lit? fi)
         (if (equal? (nnf-lit-polarity fi) #t) 
             (s (nnf-lit-var fi))
             (not (s (nnf-lit-var fi))))]
        [(nnf-conj? fi) (and (eval-nnf s (nnf-conj-l fi))
                                  (eval-nnf s (nnf-conj-r fi)))]
        [(nnf-disj? fi) (or (eval-nnf s (nnf-disj-l fi))
                                  (eval-nnf s (nnf-disj-r fi)))]))

### Lemat 5.1

Chcemy pokazać:
Dla dowolnych `x`, `y`, zachodzi `(not (and x y))` ~ `(or (not x) (not y))`, gdzie `x`, `y` są wartościami boolowskimi.

#### Dowód Lematu 5.1

Rozważmy 4 przypadki:
1. `x` ~ `#f` oraz `y` ~ `#f`
2. `x` ~ `#f` oraz `y` ~ `#t`
3. `x` ~ `#t` oraz `y` ~ `#f`
4. `x` ~ `#t` oraz `y` ~ `#t`
Zauważmy, że te przypadki są trywialne, więc Lemat jest prawdziwy dla dowolnych `x`, `y`.

### Lemat 5.2

Chcemy pokazać:
Dla dowolnych `x`, `y`, zachodzi `(not (or x y))` ~ `(and (not x) (not y))`, gdzie `x`, `y` są wartościami boolowskimi.

#### Dowód Lematu 5.2

Rozważmy 4 przypadki:
1. `x` ~ `#f` oraz `y` ~ `#f`
2. `x` ~ `#f` oraz `y` ~ `#t`
3. `x` ~ `#t` oraz `y` ~ `#f`
4. `x` ~ `#t` oraz `y` ~ `#t`
Zauważmy, że te przypadki są trywialne, więc Lemat 5.2 jest prawdziwy dla dowolnych `x`, `y`.

### Dowód:

Dowód indukcyjny względem fi:
Chcemy pokazać, że `(eval-nnf s (neg-nnf fi))` ~ `(not (eval-nnf s fi))`.

1. Jeśli `fi` jest literałem:
* Jeśli istnieje `v` takie, że `fi` ~ `(nnf-lit #t v)`
L = `(eval-nnf s (neg-nnf fi))` ~ `(eval-nnf s (neg-nnf (nnf-lit #t v)))` ~
`(eval-nnf s (nnf-lit #f v))` ~ `(not (s v))`
P = `(not (eval-nnf s fi))` ~ `(not (eval-nnf s (nnf-lit #t v)))` ~ `(not (s v))`
Zatem L ~ P.

* Jeśli istnieje `v` takie, że `(nnf-lit #f v)`
L = `(eval-nnf s (neg-nnf fi))` ~
`(eval-nnf s (neg-nnf (nnf-lit #f v)))` ~
`(eval-nnf s (nnf-lit #t v))` ~ `(s v)`
P = `(not (eval-nnf s fi))` ~
`(not (eval-nnf s (nnf-lit #f v)))` ~
`(not (not (s v)))` ~ `(s v)`.
Zatem L ~ P.

2. Jeśli `fi` ~ `(nnf-conj l r)` to:
Załóżmy, że `(eval-nnf s (neg-nnf l))` ~ `(not (eval-nnf s l))`
oraz `(eval-nnf s (neg-nnf r))` ~ `(not (eval-nnf s r))`,
pokażemy, że `(eval-nnf s (neg-nnf fi))` ~ `(not (eval-nnf s fi))`.

L = `(eval-nnf s (neg-nnf fi))` ~
`(eval-nnf s (neg-nnf (nnf-conj l r)))` ~
`(eval-nnf s (nnf-disj (neg-nnf l) (neg-nnf r)))` ~
`(or (eval-nnf s (neg-nnf l)) (eval-nnf s (neg-nnf r)))` ~
`(or (not (eval-nnf s l)) (not (eval-nnf s r)))`
P = `(not (eval-nnf s fi))` ~
`(not (eval-nnf s (nnf-conj l r)))` ~
`(not (and (eval-nnf s l)(eval-nnf s r)))` ~ (Lemat 5.1)
`(or (not (eval-nnf s l)) (not (eval-nnf s r)))`
Zatem L ~ P.

3. Jeśli `fi` ~ `(nnf-disj l r)` to:
Załóżmy, że `(eval-nnf s (neg-nnf l))` ~ `(not (eval-nnf s l))`
oraz `(eval-nnf s (neg-nnf r))` ~ `(not (eval-nnf s r))`,
pokażemy, że `(eval-nnf s (neg-nnf fi))` ~ `(not (eval-nnf s fi))`.

L = `(eval-nnf s (neg-nnf fi))` ~
`(eval-nnf s (neg-nnf (nnf-disj l r)))` ~
`(eval-nnf s (nnf-conj (neg-nnf l) (neg-nnf r)))` ~
`(and (eval-nnf s (neg-nnf l)) (eval-nnf s (neg-nnf r)))` ~
`(and (not (eval-nnf s l)) (not (eval-nnf s r)))`
P = `(not (eval-nnf s fi))` ~
`(not (eval-nnf s (nnf-disj l r)))` ~
`(not (or (eval-nnf s l)(eval-nnf s r)))` ~ (Lemat 5.2)
`(and (not (eval-nnf s l)) (not (eval-nnf s r)))`
Zatem L ~ P.

Stąd dla dowolnej formuły `fi` spełnione jest `(eval-nnf s (neg-nnf fi))` ~ `(not (eval-nnf s fi))`.

## Zadanie 6.

Formuły rachunku zdań możemy opisać następującym typem (definicja poniżej).
Zdefiniuj funkcję `to-nnf` transformującą formułę do równoważnej formuły w negacyjnej postaci normalnej. Możesz definiować funkcję pomocnicze, ale wszystkie funkcje (wzajemnie) rekurencyjne powinny używać rekursji strukturalnej.

### Definicja typu:

( define-type ( Formula 'v )
    ( var [ var : 'v ])
    ( neg [ f : ( Formula 'v ) ])
    ( conj [ l : ( Formula 'v ) ] [ r : ( Formula 'v ) ])
    ( disj [ l : ( Formula 'v ) ] [ r : ( Formula 'v ) ]) )

### Definicja funkcji:

(define (to-nnf fi)
  (cond [(var? fi) fi]
        [(conj? fi) (conj (to-nnf (conj-l fi))
                          (to-nnf (conj-r fi)))]
        [(disj? fi) 
	 (disj (to-nnf (disj-l fi))
    	       (to-nnf (disj-r fi)))]
        [(neg? fi) (cond [(var? (neg-f fi)) fi]
                         [(neg? (neg-f fi)) (to-nnf (neg-f (neg-f fi)))]
                         [(conj? (neg-f fi)) 
			   (disj (to-nnf (neg (conj-l (neg-f fi))))
                                (to-nnf (neg (conj-r (neg-f fi)))))]
                         [(disj? (neg-f fi)) 
			   (conj (to-nnf (neg (disj-l (neg-f fi))))
                                (to-nnf (neg (disj-r (neg-f fi)))))])]))

### Definicja fukcji II wersja:

(define (to-nnf fi)
  (cond [(var? fi) (nnf-lit #t (var-var fi))]
        [(conj? fi) (nnf-conj (to-nnf (conj-l fi))
                          (to-nnf (conj-r fi)))]
        [(disj? fi) (nnf-disj (to-nnf (disj-l fi))
                          (to-nnf (disj-r fi)))]
        [(neg? fi)(cond
                    [(var? (neg-f fi))
                     (nnf-lit #f (var-var (neg-f fi)))]
                    [(neg? (neg-f fi))
                     (to-nnf (neg-f (neg-f fi)))]
                    [(conj? (neg-f fi))
                     (nnf-disj (to-nnf (neg (conj-l (neg-f fi))))
                               (to-nnf (neg (conj-r (neg-f fi)))))]
                    [(disj? (neg-f fi))
                     (nnf-conj (to-nnf (neg (disj-l (neg-f fi))))
                               (to-nnf (neg (disj-r (neg-f fi)))))])]))

## Zadanie 7.

Zdefiniuj funkcję `eval-formula` interpretującą formuły z poprzedniego zadania. Następnie pokaż, że `(eval-nnf s (to-nnf fi))` ~ `(eval-formula s fi)`. Możesz założyć, że funkcja `s` zawsze się zatrzymuje.

### Definicja funkcji:

(define (eval-formula s fi)
  (cond [(var? fi) (s (var-var fi))]
        [(conj? fi) (and (eval-formula s (conj-l fi))
                         (eval-formula s (conj-r fi)))]
        [(disj? fi) (or (eval-formula s (disj-l fi))
                            (eval-formula s (disj-r fi)))]
        [(neg? fi) (not (eval-formula s fi))]))

### Dowód indukcyjny względem fi
1. `fi` ~ `(var x)`:
L = `(eval-nnf s (to-nnf fi))` ~
`(eval-nnf s (to-nnf (var x)))` ~
`(eval-nnf s (nnf-lit #t x))` ~
`(s x)`
P = `(eval-formula s fi)` ~
`(eval-formula s (var x)))` ~
`(s x)`
Zatem P ~ L.
2. `fi` ~ `(conj l r)`
Załóżmy, że `(eval-nnf s (to-nnf l))` ~ `(eval-formula s l)` oraz `(eval-nnf s (to-nnf r))` ~ `(eval-formula s r)`.
L = `(eval-nnf s (to-nnf fi))` ~
`(eval-nnf s (to-nnf (conj l r)))` ~
`(eval-nnf s (nnf-conj (to-nnf l)(to-nnf r)))` ~
`(and (eval-nnf s (to-nnf l))(eval-nnf s (to-nnf r))` ~
`(and (eval-formula s l)(eval-formula s r)` ~
P = `(eval-formula s fi)` ~
`(eval-formula s (conj l r))` ~
`(and (eval-formula s l)(eval-formula s r))` ~
Zatem P ~ L.
3. `fi` ~ `(disj l r)`
Załóżmy, że `(eval-nnf s (to-nnf l))` ~ `(eval-formula s l)` oraz `(eval-nnf s (to-nnf r))` ~ `(eval-formula s r)`.
L = `(eval-nnf s (to-nnf fi))` ~
`(eval-nnf s (to-nnf (disj l r)))` ~
`(eval-nnf s (nnf-disj (to-nnf l)(to-nnf r)))` ~
`(or (eval-nnf s (to-nnf l))(eval-nnf s (to-nnf r))` ~
`(or (eval-formula s l)(eval-formula s r)` ~
P = `(eval-formula s fi)` ~
`(eval-formula s (disj l r))` ~
`(or (eval-formula s l)(eval-formula s r))` ~
Zatem P ~ L.
4. `fi` ~ `(neg x)`
1. `x` ~ `(var v)`
L = `(eval-nnf s (to-nnf fi))` ~
`(eval-nnf s (to-nnf (neg (var v)))))` ~
`(eval-nnf s (nnf-lit #f v))` ~
`(not (s v))`
P = `(eval-formula s fi)` ~
`(eval-formula s (neg (var v)))` ~
`(not (eval-formula s v))` ~
`(not (s v))`
Zatem P = L
2. `x` ~ `(conj l r)`, zakładamy `P(l)` i `P(r)`.
L = `(eval-nnf s (to-nnf fi))` ~
`(eval-nnf s (to-nnf (neg (conj l r))))` ~
`(eval-nnf s (nnf-disj (to-nnf (neg l))(to-nnf (neg r))))` ~
`(eval-nnf s (nnf-disj (to-nnf (neg l))(to-nnf (neg r))))` ~
`(or (eval-nnf s (to-nnf (neg l)))(eval-nnf s (nnf-disj-r fi)))`
Teraz potrzebujemy założenia, że dla (neg l) oraz (neg r) jest spełnione. W związku z tym, że nie mamy tego co można zrobić?
Zauważmy, że jeśli drzewo formuły w korzeniu w `fi` miało wysokość `n` (najdłuższa odległość) to drzewo o korzeniu w `x` ma wysokość `n - 1`. Zatem skoro `x` to `(conj l r)` to formuły `l` i `r` mają wysokość co najwyżej `n - 2`, zatem `(neg l)` oraz `(neg r)` mają wysokość co najwyżej `n - 1`. Stąd na mocy indukcji strukturalnej po wysokości formuły możemy założyć, że `P((neg l))` oraz `P((neg r))` są spełnione, zatem:
L ~ `(or (eval-nnf s (to-nnf (neg l)))(eval-nnf s (nnf-disj-r fi)))` ~
`(or (eval-formula s (neg l))(eval-formula s (neg r)))` ~
`(or (not (eval-formula s l))(not (eval-formula s r)))` ~
P = `(eval-formula s fi)` ~
`(eval-formula s (neg (conj l r)))` ~
`(not (eval-formula s (conj l r)))` ~
`(not (and (eval-formula s l)(eval-formula s r)))` ~ (L 8.2)
`(or (not (eval-formula s l))(not (eval-formula s r)))`
Zatem L ~ P.
3. `x` ~ `(disj l r)` - podobnie jak conj
4. `x` ~ `(neg v)`
L = `(eval-nnf s (to-nnf fi))` ~
`(eval-nnf s (to-nnf (neg (neg v))))` ~
`(eval-nnf s (to-nnf v))` ~
`(eval-nnf s (nnf-lit #t v))` ~
`(s v)`
P = `(eval-formula s fi)` ~
`(eval-formula s (neg (neg v)))` ~
`(not (eval-formula s (neg v)))` ~
`(not (not (eval-formula s v)))` ~ (oczywiste że (not (not b)) ~ b)
`(eval-formula s v)` ~
`(s v)`
Zatem L ~ P.
Stąd na mocy indukcji działa (zauważmy, że jeśli w części używaliśmy założeń dla postruktury to indukcja po głębokości wyrażenia wystarczy wtedy też, więc to nie problem).

## Zadanie 8.
Zdefiniuj predykat `sorted?` : `((Listof Number) -> Boolean)` sprawdzający czy lista jest posortowana oraz funkcję `insert` : `(Number (Listof Number) -> (Listof Number))` wstawiającą element do listy posortowanej. Następnie udowodnij, że
jeśli `(sorted? xs)` ~ `#t` to `(sorted? (insert x xs))` ~ `#t`.

### Definicja sorted?

(define (sorted? xs)
  (cond [(empty? xs) #t]
        [(empty? (rest xs)) #t]
        [else (if (<= (first xs) (second xs))
                  (sorted? (rest xs))
                  #f)]))

### Definicja insert

(define (insert x xs)
  (if (empty? xs)
      (list x)
      (if (<= x (first xs))
          (cons x xs)
          (cons (first xs) (insert x (rest xs))))))

### Lemat 8.1
`(sorted? xs)` zwraca `#t` gdy lista `xs` jest posortowana, a `#f` w przeciwnym wypadku.

#### Dowód:
Pokażmy indukcyjnie:
1. Baza indukcji:
dla `xs` ~ `empty` oczywiście jest dobrze
dla `xs` jednoelementowego też
2. Krok indukcyjny:
Weźmy takie `x`, `xrest`, że `xs` ~ `(cons x xrest)`. Zakładamy, że `sorted` działa dla `xrest`, pokażemy że działa dla `(cons x xrest)`.
1. Jeśli `(sorted? xrest)` to `xrest` jest posortowana więc jeśli `x` jest mniejszy od `(first xrest)` to `(cons x xrest)` jest posortowane a `(sorted?)` zwróci prawdę, więc działa.
2. podobnie (jesli nie jest mniejszy to nie jest posortowane, jelsi wcześniej nieposortowane to całość też).
Stąd `sorted` działa.

### Lemat 8.2

Jeśli `x` < `y` oraz `(sorted? xs)` oraz `(sorted? (cons x xs))` to zachodzi:
`(sorted? (cons x (insert y xs))` ~ `(sorted? (insert y xs))`.
1. Jeśli `(sorted? (insert y xs))` to: (l = (insert y xs))
* jeśli x <= (first l) to skoro l jest posortowana to (cons x l) także, zatem `(sorted? (cons x (insert y xs))` zwróci prawdę (zgadza się).
2. Jeśli nieprawda, że `(sorted? (insert y xs))` to `(sorted? (cons x (insert y xs))` nie może zwrócić prawdy, (bo prawda tylko jak x <= (first l) oraz `(sorted? (insert y xs))`), zatem się zgadza.
Stąd niezależnie, czy `(sorted? (insert y xs))` jest prawdą, czy nie mamy:
`(sorted? (cons x (insert y xs))` ~ `(sorted? (insert y xs))`, co chceliśmy pokazać.

### Dowód indukcyjny po xs

Pokażemy, że jeśli `(sorted? xs)` ~ `#t` to `(sorted? (insert y xs))` ~ `#t`.
Załóżmy, że `(sorted? xs)` ~ `#t`.
1. Baza inducji:
Jeśli `xs` ~ `empty` to:
`(sorted? (insert x xs))` ~ `(sorted? (list x))` ~ `(sorted? (cons x empty))` ~ `#t`, co należało pokazać.
2. Krok indukcyjny:
Zakładamy, że:
* `(sorted? (cons x xs))` ~ `#t`
* jeśli `(sorted? xs)` ~ `#t` to `(sorted? (insert y xs))` ~ `#t`
Pokażemy, że: `(sorted? (insert y (cons x xs)))` ~ `#t`.
Zauważmy, że `(sorted? (cons x xs))` ~
1. `xs` ~ `empty`: `(sorted? (cons x xs))` ~ `#t`
2. W pozostałych przypadkach:
a. jeśli `(<= x (second xs)` to `(sorted? (cons x xs))` ~ `(sorted? xs)`
b. `#f`
Zatem skoro `(sorted? (cons x xs))` ~ `#t` to `(sorted? xs)` ~ `#t`. Zatem z założenia 2. mamy, że `(sorted? (insert y xs))` ~ `#t`.
Mamy 2 przypadki:
1. `y` <= `x`, wtedy:
`(sorted? (insert y (cons x xs)))` ~
`(sorted? (cons y (cons x xs)))` ~ (skoro y <= x)
`(sorted? (cons x xs))` ~ `#t` (z założeń).
2. `y` > `x`, wtedy:
`(sorted? (insert y (cons x xs)))` ~
`(sorted? (cons x (insert y xs))` ~ (skoro `(insert y xs)` jest pewną listą) i z L 8.2
`(sorted? (insert y xs))` ~ `#t`, co należało pokazać.

## Zadanie 7 nowe

Zdefiniuj funkcję eval-formula interpretującą formuły z poprzedniego zadania.
Następnie pokaż, że `(eval-nnf σ (to-nnf φ))` ≡ `(eval-formula σ φ)`. Możesz założyć, że funkcja `σ` zawsze się zatrzymuje.

### Lemat 7.1

Jeśli `(eval-nnf σ (to-nnf-neg φ))` ≡ `(not (eval-formula σ φ))` to `(eval-nnf σ (to-nnf (neg φ)))` ≡ `(eval-formula σ (neg φ))`

#### Dowód Lematu 7.1

L = `(eval-nnf σ (to-nnf (neg φ)))` ≡ `(eval-nnf σ (to-nnf-neg φ))` ≡ `(not (eval-formula σ φ))`
P = `(eval-formula σ (neg φ))` = `(not (eval-formula σ φ))` = L

### Dowód

#### Definicja funkcji:

(define (eval-formula s fi)
  (cond [(var? fi) (s (var-var fi))]
        [(conj? fi) (and (eval-formula s (conj-l fi))
                         (eval-formula s (conj-r fi)))]
        [(disj? fi) (or (eval-formula s (disj-l fi))
                            (eval-formula s (disj-r fi)))]
        [(neg? fi) (not (eval-formula s fi))]))

Dowód indukcyjny po `φ`:
Chcemy pokazać, że `(eval-nnf σ (to-nnf φ))` ≡ `(eval-formula σ φ)`.

1. `φ` ≡ `(var x)`:

L = `(eval-nnf σ (to-nnf φ))` ≡ `(eval-nnf σ (to-nnf (var x)))` ≡
`(eval-nnf σ (nnf-lit #t x))` ≡ `(σ x)`

P = `(eval-formula σ φ)` ≡ `(eval-formula σ (var x)))` ≡ `(σ x)` = L
2. `φ` ≡ `(conj l r)`
Załóżmy, że `(eval-nnf σ (to-nnf l))` ≡ `(eval-formula σ l)`
oraz `(eval-nnf σ (to-nnf r))` ≡ `(eval-formula σ r)`.

L = `(eval-nnf σ (to-nnf φ))` ≡ `(eval-nnf σ (to-nnf (conj l r)))` ≡
`(eval-nnf σ (nnf-conj (to-nnf l)(to-nnf r)))` ≡
`(and (eval-nnf σ (to-nnf l))(eval-nnf σ (to-nnf r))` ≡
`(and (eval-formula σ l)(eval-formula σ r)`

P = `(eval-formula σ φ)` ≡ `(eval-formula σ (conj l r))` ≡
`(and (eval-formula σ l)(eval-formula σ r))` = L
3. `φ` ≡ `(disj l r)`
Załóżmy, że `(eval-nnf σ (to-nnf l))` ≡ `(eval-formula σ l)` oraz `(eval-nnf σ (to-nnf r))` ≡ `(eval-formula σ r)`.

L = `(eval-nnf σ (to-nnf φ))` ≡
`(eval-nnf σ (to-nnf (disj l r)))` ≡
`(eval-nnf σ (nnf-disj (to-nnf l)(to-nnf r)))` ≡
`(or (eval-nnf σ (to-nnf l))(eval-nnf σ (to-nnf r))` ≡
`(or (eval-formula σ l)(eval-formula σ r)`

P = `(eval-formula σ φ)` ≡
`(eval-formula σ (disj l r))` ≡
`(or (eval-formula σ l)(eval-formula σ r))` = L
4. `φ` ≡ `(neg x)`
* `x` ≡ `(var v)`
L = `(eval-nnf σ (to-nnf φ))` ≡ `(eval-nnf σ (to-nnf (neg x)))` ≡
`(eval-nnf σ (to-nnf-neg x))` ≡ `(eval-nnf σ (to-nnf-neg (var v)))` ≡
`(eval-nnf σ (nnf-lit #f v)` ≡ `(not (σ v))`

P = `(eval-formula σ φ)` ≡ `(eval-formula σ (neg (var v)))` ≡
`(not (eval-formula σ v))` ≡ `(not (σ v))` = L
* `x` ≡ `(conj l r)`
Załóżmy, że `(eval-nnf σ (to-nnf-neg l))` ≡ `(not (eval-formula σ l))`
oraz `(eval-nnf σ (to-nnf-neg r))` ≡ `(not (eval-formula σ r))`.

L = `(eval-nnf σ (to-nnf φ))` ≡ `(eval-nnf σ (to-nnf (neg (conj l r))))` ≡
`(eval-nnf σ (to-nnf-neg (conj l r)))` ≡
`(eval-nnf σ (nnf-disj (to-nnf-neg l) (to-nnf-neg r)))` ≡
`(or (eval-nnf σ (to-nnf-neg l)) (eval-nnf σ (to-nnf-neg r)))` ≡
`(or (not (eval-formula σ l)) (not (eval-formula σ r)))`

P = `(eval-formula σ φ)` ≡ `(eval-formula σ (neg (conj l r)))` ≡
`(not (eval-formula σ (conj l r)))` ≡
`(not (and (eval-formula σ l)(eval-formula σ r)))` ≡
`(or (not (eval-formula σ l))(not (eval-formula σ r)))` = L

Udowodniliśmy, że
`(eval-nnf σ (to-nnf-neg (conj l r)))` ≡ `(not (eval-formula σ (conj l r)))`, ale z Lematu 7.1 otrzymujemy
`(eval-nnf σ (to-nnf (neg (conj l r))))` ≡ `(eval-formula σ (neg (conj l r)))`
* `x` ≡ `(disj l r)`
Załóżmy, że `(eval-nnf σ (to-nnf-neg l))` ≡ `(not (eval-formula σ l))`
oraz `(eval-nnf σ (to-nnf-neg r))` ≡ `(not (eval-formula σ r))`.

L = `(eval-nnf σ (to-nnf φ))` ≡ `(eval-nnf σ (to-nnf (neg (disj l r))))` ≡
`(eval-nnf σ (to-nnf-neg (disj l r)))` ≡
`(eval-nnf σ (nnf-conj (to-nnf-neg l) (to-nnf-neg r)))` ≡
`(and (eval-nnf σ (to-nnf-neg l)) (eval-nnf σ (to-nnf-neg r)))` ≡
`(and (not (eval-formula σ l)) (not (eval-formula σ r)))`

P = `(eval-formula σ φ)` ≡ `(eval-formula σ (neg (disj l r)))` ≡
`(not (eval-formula σ (disj l r)))` ≡
`(not (or (eval-formula σ l)(eval-formula σ r)))` ≡
`(and (not (eval-formula σ l))(not (eval-formula σ r)))` = L

Udowodniliśmy, że
`(eval-nnf σ (to-nnf-neg (disj l r)))` ≡ `(not (eval-formula σ (disj l r)))`, ale z Lematu 7.1 otrzymujemy
`(eval-nnf σ (to-nnf (neg (disj l r))))` ≡ `(eval-formula σ (neg (disj l r)))`
* `x` ≡ `(neg v)`
L = `(eval-nnf σ (to-nnf φ))` ≡ `(eval-nnf σ (to-nnf (neg (neg v))))` ≡
`(eval-nnf σ (to-nnf-neg (neg v)))` ≡ `(eval-nnf σ (to-nnf v))`

P = `(eval-formula σ φ)` ≡ `(eval-formula σ (neg (neg v)))` ≡
`(not (eval-formula σ (neg v)))` ≡ `(not (not (eval-formula σ v)))` ≡
`(eval-formula σ v)` = L

Zatem `(eval-nnf σ (to-nnf φ))` ≡ `(eval-formula σ φ)`