n
x else f(i) fi
n,m:
, f:(n
m), x:m. f[n:=x] 
(n+1)mj == if i=j true ; false fii,j:
. (i=j) 
| No other cites to report in MarkB_generic | |
| fappend | Def f[n:=x](i) == if i=n x else f(i) fi |
| Thm* n,m:, f:(nm), x:m. f[n:=x] (n+1)m | |
| eq_int | Def i=j == if i=j true ; false fi |
| Thm* i,j:. (i=j) |
| Syntax: | f[n:=x] | has structure: | fappend(f; n; x) |
About:
 |  |  |  |  |  |  |
 |  |  |  |  |
 |