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