Nuprl Definition : nonzero-cross-imp

nonzero-cross-imp(r;eq;a;b) ==
  case int_seg_decide(λi.if eq (a i) 0 then inr (λ%.let %4,%5 = % in Ax) 
                         if eq (b i) 0 then inr (λ%.let %5,%6 = % in Ax) 
                         else inl <λ%.Ax, λ%.Ax>
                         fi ;0;3)
   of inl(tr) =>
   let i,pr = tr 
   in eval i@0 = i in
      let _,_ = pr 
      in if eq (a i@0) 0 then Ax
         if int_seg_decide(λx.if eq (* (b i@0) (a x)) (* (a i@0) (b x)) then inr (λ%.Ax)  else inl Ax fi ;0;3)
           then case int_seg_decide(λj.if eq (* (b i@0) (a j)) (* (a i@0) (b j))
                                       then inr (λ%.Ax) 
                                       else inl (λ%.Ax)
                                       fi ;0;3)
                 of inl(x) =>
                 let j,_ = x 
                 in λx.if x=i@0 then a j else if x=j then -r (a i@0) else 0
                 | inr(x) =>
                 let j,_ = Ax 
                 in λx.if x=i@0 then a j else if x=j then -r (a i@0) else 0
         else Ax
         fi 
   | inr(_) =>
   λi.if i=non-zero-component(r;eq;3;b) then 1 else 0


Definitions occuring in Statement :  non-zero-component: non-zero-component(r;eq;k;a),  int_seg_decide: int_seg_decide(d;i;j),  callbyvalue: callbyvalue,  ifthenelse: if b then t else f fi ,  int_eq: if a=b then c else d,  apply: f a,  lambda: λx.A[x],  spread: spread def,  pair: <a, b>,  decide: case b of inl(x) => s[x] | inr(y) => t[y],  inr: inr x ,  inl: inl x,  natural_number: $n,  axiom: Ax,  rng_one: 1,  rng_times: *,  rng_minus: -r,  rng_zero: 0
Definitions occuring in definition :  apply: f a,  int_eq: if a=b then c else d,  lambda: λx.A[x],  axiom: Ax,  spread: spread def,  rng_zero: 0,  rng_minus: -r,  natural_number: $n,  inl: inl x,  inr: inr x ,  rng_times: *,  ifthenelse: if b then t else f fi ,  int_seg_decide: int_seg_decide(d;i;j),  decide: case b of inl(x) => s[x] | inr(y) => t[y],  callbyvalue: callbyvalue,  pair: <a, b>,  non-zero-component: non-zero-component(r;eq;k;a),  rng_one: 1
FDL editor aliases :  nonzero-cross-imp
Latex:
nonzero-cross-imp(r;eq;a;b)  ==
    case  int\_seg\_decide(\mlambda{}i.if  eq  (a  i)  0  then  inr  (\mlambda{}\%.let  \%4,\%5  =  \%  in  Ax) 
                                                  if  eq  (b  i)  0  then  inr  (\mlambda{}\%.let  \%5,\%6  =  \%  in  Ax) 
                                                  else  inl  <\mlambda{}\%.Ax,  \mlambda{}\%.Ax>
                                                  fi  ;0;3)
      of  inl(tr)  =>
      let  i,pr  =  tr 
      in  eval  i@0  =  i  in
            let  $_{}$,$_{}$  =  pr 
            in  if  eq  (a  i@0)  0  then  Ax
                  if  int\_seg\_decide(\mlambda{}x.if  eq  (*  (b  i@0)  (a  x))  (*  (a  i@0)  (b  x))
                                                            then  inr  (\mlambda{}\%.Ax) 
                                                            else  inl  Ax
                                                            fi  ;0;3)
                      then  case  int\_seg\_decide(\mlambda{}j.if  eq  (*  (b  i@0)  (a  j))  (*  (a  i@0)  (b  j))
                                                                              then  inr  (\mlambda{}\%.Ax) 
                                                                              else  inl  (\mlambda{}\%.Ax)
                                                                              fi  ;0;3)
                                  of  inl(x)  =>
                                  let  j,$_{}$  =  x 
                                  in  \mlambda{}x.if  x=i@0  then  a  j  else  if  x=j  then  -r  (a  i@0)  else  0
                                  |  inr(x)  =>
                                  let  j,$_{}$  =  Ax 
                                  in  \mlambda{}x.if  x=i@0  then  a  j  else  if  x=j  then  -r  (a  i@0)  else  0
                  else  Ax
                  fi 
      |  inr($_{}$)  =>
      \mlambda{}i.if  i=non-zero-component(r;eq;3;b)  then  1  else  0


Date html generated: 2020_05_20-AM-09_03_45
Last ObjectModification: 2019_11_27-PM-03_20_22

Theory : matrices


Home Index