Nuprl Definition : seteqweaken

seteqweaken(s2) ==
  λ_,moves. let u,v = moves[||moves|| - 2]
            in let u',v' = moves[||moves|| - 1]
               in if copath-length(u) <z copath-length(u') then <u', u'> else <v', v'> fi

Definitions occuring in Statement : copath-length: copath-length(p), play-len: ||moves||, play-item: moves[i], ifthenelse: if b then t else f fi , lt_int: i <z j, lambda: λx.A[x], spread: spread def, pair: <a, b>, subtract: n - m, natural_number: $n
Definitions occuring in definition : pair: <a, b>, copath-length: copath-length(p), lt_int: i <z j, ifthenelse: if b then t else f fi , natural_number: $n, play-len: ||moves||, subtract: n - m, play-item: moves[i], spread: spread def, lambda: λx.A[x]

Latex:
seteqweaken(s2) == \mlambda{}$_{}$,moves. let u,v = moves[||moves|| - 2] in let u',v' = moves[||moves|| - 1] in if copath-length(u) <z copath-length(u') then <u', u'> else <v', v'> fi Date html generated: 2018_07_29-AM-09_50_57 Last ObjectModification: 2018_07_11-AM-11_58_06 Theory : constructive!set!theory Home Index