(7steps total)
PrintForm
Definitions
Lemmas
graph
1
1
Sections
Graphs
Doc
At:
mapoutl
is
singleton
1
2
1.
A:
Type
2.
B:
Type
3.
L:
(A+B) List
4.
a:
A
5.
u:
A+B
6.
v:
(A+B) List
7.
mapoutl(v) = [a]
(
L1,L2:(A+B) List. v = (L1 @ [inl(a)] @ L2) & mapoutl(L1) = nil & mapoutl(L2) = nil)
mapoutl([u / v]) = [a]
(
L1,L2:(A+B) List. [u / v] = (L1 @ [inl(a) / L2]) & mapoutl(L1) = nil & mapoutl(L2) = nil)
By:
Analyze -3
THEN
Reduce 0
THEN
ThinTrivial
Generated subgoals:
1
5.
x:
A
6.
v:
(A+B) List
7.
mapoutl(v) = [a]
(
L1,L2:(A+B) List. v = (L1 @ [inl(a)] @ L2) & mapoutl(L1) = nil & mapoutl(L2) = nil)
8.
[x / mapoutl(v)] = [a]
L1,L2:(A+B) List. [inl(x) / v] = (L1 @ [inl(a) / L2]) & mapoutl(L1) = nil & mapoutl(L2) = nil
1
step
 
2
5.
y:
B
6.
v:
(A+B) List
7.
mapoutl(v) = [a]
8.
L1,L2:(A+B) List. v = (L1 @ [inl(a)] @ L2) & mapoutl(L1) = nil & mapoutl(L2) = nil
L1,L2:(A+B) List. [inr(y) / v] = (L1 @ [inl(a) / L2]) & mapoutl(L1) = nil & mapoutl(L2) = nil
1
step
About:
(7steps total)
PrintForm
Definitions
Lemmas
graph
1
1
Sections
Graphs
Doc