\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: ""

{λ[sigma:Set] . λ[r:∀[x:sigma] . ∀[y:sigma] . Prop] . λ[refr1:∀[x:sigma] . (x) . (x) . r] . λ[symr1:∀[x:sigma] . ∀[y:sigma] . ∀[t:(y) . (x) . r] . (x) . (y) . r] . λ[trr1:∀[x:sigma] . ∀[y:sigma] . ∀[z:sigma] . ∀[t:(y) . (x) . r] . ∀[u:(z) . (y) . r] . (z) . (x) . r] . λ[s0:(sigma) . set ] . λ[ecs0:{(s0) . (trr1) . (symr1) . (refr1) . (r) . (sigma)} . anec ] . λ[t0:(sigma) . set ] . λ[ect0:{(t0) . (trr1) . (symr1) . (refr1) . (r) . (sigma)} . anec ] . λ[s:sigma] . λ[ses0:{(s0) . (s) . (sigma)} . esti ] . λ[t:sigma] . λ[tet0:{(t0) . (t) . (sigma)} . esti ] . λ[n:((t) . (s) . r) . not ]} . <{({(t) . (trr1) . (symr1) . (refr1) . (r) . (sigma)} . ecelt ) . (s0) . (sigma)} . disj > . {({(ses0) . (s) . (ecs0) . (s0) . (trr1) . (symr1) . (refr1) . (r) . (sigma)} . th2 ) . ({(n) . (t) . (s) . (trr1) . (symr1) . (refr1) . (r) . (sigma)} . th5 ) . (s0) . ({(s) . (trr1) . (symr1) . (refr1) . (r) . (sigma)} . ecelt ) . (λ[x:(sigma) . set ] . {({(t) . (trr1) . (symr1) . (refr1) . (r) . (sigma)} . ecelt ) . (x) . (sigma)} . disj ) . ((sigma) . set )} . isp1

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