Check-in [556662b818]

Not logged in

Many hyperlinks are disabled.
Use anonymous login to enable hyperlinks.

Overview
Comment:Fixed a small logical mistake in a footnote.
Downloads: Tarball | ZIP archive | SQL archive
Timelines: family | ancestors | descendants | both | trunk
Files: files | file ages | folders
SHA1:556662b8186e98b187796f68ec9b6124c872d7bf
User & Date: andy 2015-04-15 14:31:52
Context
2015-04-15
14:32
Fixed module declarations/imports for the new argument pattern for `elaborate`. check-in: 207908bad1 user: andy tags: trunk
14:31
Fixed a small logical mistake in a footnote. check-in: 556662b818 user: andy tags: trunk
11:48
Added some extra arguments to the premise/conclusion hooks: index (for antecedants), path, and the actual term itself. check-in: f84190c56c user: andy tags: trunk
Changes
Hide Diffs Unified Diffs Ignore Whitespace Patch

Changes to report/arend-report.tex.

1948
1949
1950
1951
1952
1953
1954
1955
1956

1957

1958
1959
1960
1961
1962
1963
1964
\item $\mathsf{nat}(X) -> \mathsf{add}(X,z,X)$. This will require 
    induction on $\mathsf{nat}(X)$.

\item Commutativity of $\mathsf{add}$: $\mathsf{nat}(X) \land \mathsf{nat}(Y)
-> \mathsf{add}(X,Y,Z) \land \mathsf{add}(Y,X,Z') \land Z = Z'$.

\item Totality of $\mathsf{add}$: $\mathsf{nat}(X) \land \mathsf{nat}(Y) ->
    \mathsf{add}(X,Y,Z) \land \mathsf{nat}(Z)$.\marginnote{Note that in an 
    intuitionistic logic it is much more difficult to prove that $\mathsf{add}$ is

    \emph{functional}: i.e., that there exists \emph{exactly one} such $Z$.}


\item Transitivity of $>$: $\mathsf{nat}(X) \land \mathsf{nat}(Y) \land 
\mathsf{nat}(Z) \land X < Y \land Y < Z -> X < Z$.

\item Cons is idempotent: \\ 
$\mathsf{natlist}(L) \land \mathsf{elem}(N,L) \land
\mathsf{nat}(N') \land L' = cons(N',L) -> \mathsf{elem}(N,L')$







|
<
>
|
>







1948
1949
1950
1951
1952
1953
1954
1955

1956
1957
1958
1959
1960
1961
1962
1963
1964
1965
\item $\mathsf{nat}(X) -> \mathsf{add}(X,z,X)$. This will require 
    induction on $\mathsf{nat}(X)$.

\item Commutativity of $\mathsf{add}$: $\mathsf{nat}(X) \land \mathsf{nat}(Y)
-> \mathsf{add}(X,Y,Z) \land \mathsf{add}(Y,X,Z') \land Z = Z'$.

\item Totality of $\mathsf{add}$: $\mathsf{nat}(X) \land \mathsf{nat}(Y) ->
    \mathsf{add}(X,Y,Z) \land \mathsf{nat}(Z)$.


\item Functionality of $\mathsf{add}$: $\mathsf{nat}(X) \land \mathsf{nat}(Y) 
    \land \mathsf{add}(X,Y,Z_1) \land \mathsf{add}(X,Y,Z_2) -> Z_1 = Z_2$.

\item Transitivity of $>$: $\mathsf{nat}(X) \land \mathsf{nat}(Y) \land 
\mathsf{nat}(Z) \land X < Y \land Y < Z -> X < Z$.

\item Cons is idempotent: \\ 
$\mathsf{natlist}(L) \land \mathsf{elem}(N,L) \land
\mathsf{nat}(N') \land L' = cons(N',L) -> \mathsf{elem}(N,L')$