[isabelle] Simple



Hi,

how can i prove

set l1 ⊆ {Suc 0, 2, 3} ⟶ set l2 ⊆ {Suc 0, 2, 3, 4} ⟶ set (addlists l1 l2) ⊆ {Suc 0, 2, 3, 4, 5, 6, 7}

(by the way
fun  addlists :: "nat list => nat list => nat list" where
"addlists [] [] = []" |
"addlists (x#xs) [] = undefined" |
"addlists [] (x#xs) = undefined" |
"addlists (x#xs) (y#ys) = (x+y) # (addlists xs ys)"
)


Many thanks!
 		 	   		  


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.