PrintForm
Definitions
formula
list
Sections
ClassicalProps(jlc)
Doc
At:
list
rank
append
homomorphism
1
2
1
1.
M:
Formula List
2.
u:
Formula
3.
v:
Formula List
4.
N:Formula List.
(v @ N) =
(v)+
(N)
5.
N:
Formula List
((u.v) @ N) =
(u.v)+
(N)
By:
With N (Analyze -2)
Generated subgoal:
1
4.
N:
Formula List
5.
(v @ N) =
(v)+
(N)
((u.v) @ N) =
(u.v)+
(N)
About:
(v @ N) = (v)+(N) 
((u.v) @ N) = (u.v)+(N) 
N:Formula List. (v @ N) = (v)+(N) ((u.v) @ N) = (u.v)+(N) (v @ N) = (v)+(N) ((u.v) @ N) = (u.v)+(N) 
