# Lab 6: Shorthand for Program Derivations

## Problem: Narrowing Down the Possibilities

**f1**
### types
* name = string
### Assumptions
* A name is equal to "Alice"
* B name is equal to "Bob"
* C name is equal to "Carol"
* D name is not equal to "Daniel"
* E name is not equal to "Emily"
### Exhaustive?
* the conditionals capture all possible versions of the variable name

**f2**
### types
* x = interger
* y = interger
### Assumptions
* A y > or = to 1
* B x > or = to 1
* C x = to -1
* D x < or = to -5 or y > or = to 3
* E x = to 0
* F x = to y
### Exhaustive?
* does not include x>-5 to x<-1 and y<1 when x =/= y

## Problem: Capture
**report**
### preconditions
* hw-avg = natural numbers
* quiz1 = natural numbers
* quiz2 = natural numbers
* quiz3 = natural numbers
### constraints
* hw-avg> 60 and hw-avg< 75
* or hw-avg> 75 and hw-avg< 90 where quiz2 > quiz1 or quiz3 > quiz2
### Innapropriate String?
* The function returns "progressing" rather than "needs help" if the hw-avg is above 75 but the quizes are below 60 and equal or in sequential order. For example (report 75 0 0 0) returns "progressing"
* This could be the intention, but it seems unlikely.

## Problem: Looking Ahead
**append**
### Claim (Nil Is An Identity on the Left): for any list l, (append '() $l$) $≡ l$.
let $l$ be an arbitrary list

    (append '() l)
--> (if (null? '())
        l
        (cons (car '()) (append (cdr '()) l))
--> (if #t
        l
        (cons (car '()) (append (cdr '()) l))
--> l

$l≡ l$
Thus, since $l$ was an arbitrary set, for any list l, (append '() $l$) $≡ l$.
☐
### Claim (Append is Not Commutative): there exists lists $l1$ and $l2$ such that (append $l1$ $l2$)≠(append $l2$ $l1$).

let $l1$ = '(1) and let $l2$ = '(2)

    (append '(1) '(2))
--> (if (null? '(1))
        '(2)
        (cons (car '(1)) (append (cdr '(1)) '(2))))
--> (if #f
        '(2)
        (cons (car '(1)) (append (cdr '(1)) '(2))))
-->(cons (car '(1)) (append (cdr '(1)) '(2)))
-->(cons (car '(1)) (append '() '(2)))
-->(cons 1 (append '() '(2)))
-->(cons 1 '(2)) <-using the identity result from above
-->'(1 2)

     (append '(2) '(1))
--> (if (null? '(2))
        '(1)
        (cons (car '(2)) (append (cdr '(2)) '(1))))
--> (if #f
        '(1)
        (cons (car '(2)) (append (cdr '(2)) '(1))))
-->(cons (car '(2)) (append (cdr '(2)) '(1)))
-->(cons (car '(2)) (append '() '(1)))
-->(cons  (append '() '(1)))
-->(cons '()' '(1)) <-using the identity result from above
-->'(2 1)   

'(1 2) ≠ '(2 1)
Thus, we have show a case of $l1$ and $l2$ such that (append $l1$ $l2$)≠(append $l2$ $l1$).
☐
### Claim (Nil Is An Identity on the Right): for any list l, (append l '()) ≡ l.
let l be an arbitrary list.

    (append l '())
--> (if (null? l)
        '()
        (cons (car l) (append (cdr l) '()))))

Here we will have 2 cases for l
Case 1: l is '().

    (append l '())
--> (if (null? l)
        '()
        (cons (car l) (append (cdr l) '()))))
--> (if (null? '())
        '()
        (cons (car l) (append (cdr l) '()))))
--> '()

Case 2: l is a list '(a l1) where a is and arbitrary value and l1 is an arbitrary list.

    (append l '())
--> (if (null? l)
        '()
        (cons (car l) (append (cdr l) '())))
--> (cons (car l) (append (cdr l) '()))
--> (cons a (append l1 '()))

Here in the second case we will have 2 cases for l1
Case 1: l1 is '().

    (append l1 '())
--> (if (null? l1)
        '()
        (cons (car l1) (append (cdr l1) '())))
--> (if (null? '())
        '()
        (cons (car l1) (append (cdr l1) '())))
--> '()

--> (cons a '()) put the result back into the original case 2 for l
--> '(a)

Case 2: l1 is a list '(b l2) where a is and arbitrary value and l1 is an arbitrary list.

    (append l1 '())
--> (if (null? l1)
        '()
        (cons (car l1) (append (cdr l1) '()))))
--> (cons (car l1) (append (cdr l1) '()))
--> (cons b (append l2 '()))

--> (cons a (cons b (append l2 '()))) put the result back into the orriginal case 2 for l

Here we can continue but the result is obvious. When l or its derivitives are null then the function will evaluate to '() and the cons function calls can finally be evaluated resulting in the original list l. The only way this would not happen is if the list l had infinitely many terms such that the append function would never evaluate.

### reflections
* The left-identity had a finite value '() evaluated in the if statement, so the claim could be directly evaluated through the call-by-value style.
* The right-identity had an arbitrary value evaluated in the if statement. This makes it harder to check the bahavior and one must look for patterns in the functions behavior.
* There needed to be apparent repettitive behavior that could be reasoned through to stop. If the behavior was either random or without a discernable pattern then it would need to be continued.