\lambda\delta home page

home	news	documentation	specification		implementation
foreword	milestones	version 2	version 2	(background - core - applications)	library	(static LDDL directory)
citations	visibility	version 1	version 1	(static HELM directory)	helena

Informal description: ""

{λ[a: nat ] . λ[b: nat ] . λ[c: nat ] . λ[d: nat ]} . <{({({(b) . (c)} . ts ) . ({(d) . (a)} . ts )} . ts ) . ({({(d) . (c)} . ts ) . ({(b) . (a)} . ts )} . ts )} . is > . {({({(b) . (c)} . ts ) . (d) . (a)} . assts2 ) . ({({(d) . (c) . (b) . (a)} . t2 ) . (a) . ({({(b) . (c)} . ts ) . (d)} . ts ) . ({({(d) . (c)} . ts ) . (b)} . ts )} . ists2 ) . ({({(d) . (c)} . ts ) . (b) . (a)} . assts1 ) . ({({(b) . (c)} . ts ) . ({(d) . (a)} . ts )} . ts ) . ({({({(b) . (c)} . ts ) . (d)} . ts ) . (a)} . ts ) . ({({({(d) . (c)} . ts ) . (b)} . ts ) . (a)} . ts ) . ({({(d) . (c)} . ts ) . ({(b) . (a)} . ts )} . ts ) . ( nat )} . tr3is

Validation parameters: sort hierarchy = "Z2", kernel options = ""