Mercurial > hg > Members > kono > Proof > FirstOrder
changeset 19:55a0d814fce7 default tip
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Wed, 16 Dec 2020 16:16:43 +0900 |
| parents | 6cd5b63ecc38 |
| children | |
| files | Logic.agda simple-logic.agda |
| diffstat | 2 files changed, 2 insertions(+), 2 deletions(-) [+] |
line wrap: on
line diff
--- a/Logic.agda Sat Aug 22 13:34:12 2020 +0900 +++ b/Logic.agda Wed Dec 16 16:16:43 2020 +0900 @@ -36,7 +36,7 @@ (e ∧ e₁) [ xv / v ] = ( e [ xv / v ]) ∧ ( e₁ [ xv / v ]) (e ∨ e₁) [ xv / v ] = ( e [ xv / v ]) ∨ ( e₁ [ xv / v ]) (¬ e) [ xv / v ] = ¬ ( e [ xv / v ]) - (All x => e) [ xv / v ] = All x => ( e [ xv / v ]) + (All x => e) [ xv / v ] = All x => ( e [ xv / v ]) -- we should protect variable x from replacement (Exist x => e) [ xv / v ] = Exist x => ( e [ xv / v ]) m : Statement → Bool
--- a/simple-logic.agda Sat Aug 22 13:34:12 2020 +0900 +++ b/simple-logic.agda Wed Dec 16 16:16:43 2020 +0900 @@ -44,7 +44,7 @@ (x ∧ y) [ n / v ] = (x [ n / v ] ) ∧ (x [ n / v ]) (x ∨ y) [ n / v ] = (x [ n / v ] ) ∨ (x [ n / v ]) (¬ x) [ n / v ] = ¬ (x [ n / v ] ) -(all x => y) [ n / v ] = all x => (y [ n / v ]) +(all x => y) [ n / v ] = all x => (y [ n / v ]) -- we should protect variable x from replacement (∃ x => y) [ n / v ] = ∃ x => (y [ n / v ]) {-# TERMINATING #-}