User Tools

Site Tools


plt17:assignment_2

Differences

This shows you the differences between two versions of the page.

Link to this comparison view

Both sides previous revision Previous revision
plt17:assignment_2 [2017/12/05 14:45]
hossein [Task 1]
plt17:assignment_2 [2017/12/05 14:45] (current)
hossein [Task 3]
Line 31: Line 31:
 Prove the following theorem: if a variable does not appear free in a term, then substituting it with any other expression has no effect. ​ Prove the following theorem: if a variable does not appear free in a term, then substituting it with any other expression has no effect. ​
  
-''​Theorem subset_fresh : forall e1 e x, ~ (Free x e) -> subst e1 x e = e.''​+''​Theorem subset_fresh : forall e1 e x, ~ (free x e) -> subst e1 x e = e.''​
 ===== Task 4 ===== ===== Task 4 =====
  
plt17/assignment_2.txt ยท Last modified: 2017/12/05 14:45 by hossein