(9steps total)
PrintForm
Definitions
Lemmas
graph
1
1
Sections
Graphs
Doc
At:
mapoutl
is
append
1
2
1
1.
A:
Type
2.
B:
Type
3.
l1:
A List
4.
l2:
A List
5.
u:
A
6.
v:
A List
7.
L:(A+B) List. mapoutl(L) = (v @ l2)
(
L1,L2:(A+B) List. L = (L1 @ L2) & mapoutl(L1) = v & mapoutl(L2) = l2)
8.
L:
(A+B) List
nil = [u / (v @ l2)]
(
L1,L2:(A+B) List. nil = (L1 @ L2) & mapoutl(L1) = [u / v] & mapoutl(L2) = l2)
By:
ObviousConcl
Generated subgoals:
None
About:
(9steps total)
PrintForm
Definitions
Lemmas
graph
1
1
Sections
Graphs
Doc
L:(A+B) List.
mapoutl(L) = (v @ l2) 
(
L1,L2:(A+B) List. L = (L1 @ L2) & mapoutl(L1) = v & mapoutl(L2) = l2)
nil = [u / (v @ l2)] (L1,L2:(A+B) List. nil = (L1 @ L2) & mapoutl(L1) = [u / v] & mapoutl(L2) = l2)