(17steps total) PrintForm Definitions Lemmas mb event system 6 Sections EventSystems Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: frame-rule 2 1 2 1
1. i : Id
2. L : Knd List
3. x : Id
4. T : Type
5. w : World
6. FairFifo
7. FairFifo
8. i@0,x@0:Id.
8. vartype(i@0;x@0) r if deq-member(IdDeq;x@0;1of(1of(if eqof(IdDeq)(i@0,i)
8. vartype(i@0;x@0) r if deq-member(IdDeq;x@0;1of(1of(if <<[x],x.T>
8. vartype(i@0;x@0) r if deq-member(IdDeq;x@0;1of(1of(if ,
8. vartype(i@0;x@0) r if deq-member(IdDeq;x@0;1of(1of(if ,
8. vartype(i@0;x@0) r if deq-member(IdDeq;x@0;1of(1of(if ,
8. vartype(i@0;x@0) r if deq-member(IdDeq;x@0;1of(1of(if ,
8. vartype(i@0;x@0) r if deq-member(IdDeq;x@0;1of(1of(if ,
8. vartype(i@0;x@0) r if deq-member(IdDeq;x@0;1of(1of(if ,<[x],x.L>
8. vartype(i@0;x@0) r if deq-member(IdDeq;x@0;1of(1of(if ,
8. vartype(i@0;x@0) r if deq-member(IdDeq;x@0;1of(1of(if ,>
8. vartype(i@0;x@0) r if deq-member(IdDeq;x@0;1of(1of(else  fi)))
8. vartype(i@0;x@0) r if 2of(1of(if eqof(IdDeq)(i@0,i)
8. vartype(i@0;x@0) r if 2of(1of(if <<[x],x.T>,,,,,,<[x],x.L>,,>
8. vartype(i@0;x@0) r if 2of(1of(else  fi))
8. vartype(i@0;x@0) r if (x@0)
8. vartype(i@0;x@0) r else Top fi
9. i@0:Id, a:Action(i@0).
9. isnull(a)
9. 
9. (valtype(i@0;a) r if eqof(IdDeq)(i@0,i) <<[x],x.T>,,,,,,<[x],x.L>,,>
9. (valtype(i@0;a) r else  fi.da(kind(a)))
10. l:IdLnk, tg:Id.
10. (w.M(l,tg)) r if eqof(IdDeq)(source(l),i) <<[x],x.T>,,,,,,<[x],x.L>,,>
10. (w.M(l,tg)) r else  fi.da(rcv(l; tg))
11. i@0,x@0:Id.
11. deq-member(IdDeq;x@0;1of(1of(2of(2of(if eqof(IdDeq)(i@0,i)
11. deq-member(IdDeq;x@0;1of(1of(2of(2of(if <<[x],x.T>,,,,,,<[x],x.L>,,>
11. deq-member(IdDeq;x@0;1of(1of(2of(2of(else  fi)))))
11. 
11. s(i@0;0).x@0
11. =
11. 2of(1of(2of(2of(if eqof(IdDeq)(i@0,i) <<[x],x.T>,,,,,,<[x],x.L>,,>
11. 2of(1of(2of(2of(else  fi))))
11. (x@0)
12. i@0:Id, t:.
12. isnull(a(i@0;t))
12. 
12. (islocal(kind(a(i@0;t)))
12. (
12. (deq-member(IdDeq;act(kind(a(i@0;t)));1of(1of(2of(2of(2of(if eqof(IdDeq)
12. (deq-member(IdDeq;act(kind(a(i@0;t)));1of(1of(2of(2of(2of(if (i@0
12. (deq-member(IdDeq;act(kind(a(i@0;t)));1of(1of(2of(2of(2of(if ,i)
12. (deq-member(IdDeq;act(kind(a(i@0;t)));1of(1of(2of(2of(2of(if <<[x],x.T>
12. (deq-member(IdDeq;act(kind(a(i@0;t)));1of(1of(2of(2of(2of(if ,
12. (deq-member(IdDeq;act(kind(a(i@0;t)));1of(1of(2of(2of(2of(if ,
12. (deq-member(IdDeq;act(kind(a(i@0;t)));1of(1of(2of(2of(2of(if ,
12. (deq-member(IdDeq;act(kind(a(i@0;t)));1of(1of(2of(2of(2of(if ,
12. (deq-member(IdDeq;act(kind(a(i@0;t)));1of(1of(2of(2of(2of(if ,
12. (deq-member(IdDeq;act(kind(a(i@0;t)));1of(1of(2of(2of(2of(if ,<[x],x.L>
12. (deq-member(IdDeq;act(kind(a(i@0;t)));1of(1of(2of(2of(2of(if ,
12. (deq-member(IdDeq;act(kind(a(i@0;t)));1of(1of(2of(2of(2of(if ,>
12. (deq-member(IdDeq;act(kind(a(i@0;t)));1of(1of(2of(2of(2of(else  fi))))))
12. (
12. (2of(1of(2of(2of(2of(if eqof(IdDeq)(i@0,i) <<[x],x.T>,,,,,,<[x],x.L>,,>
12. (2of(1of(2of(2of(2of(else  fi)))))
12. ((act(kind(a(i@0;t)))
12. (,x.s(i@0;t).x
12. (,val(a(i@0;t))))
12. & (x@0:Id. 
12. & (deq-member(product-deq(Knd;Id;KindDeq;IdDeq);<kind(a(i@0;t))
12. & (deq-member(product-deq(Knd;Id;KindDeq;IdDeq);,x@0>;1of(1of(
12. & (deq-member(product-deq(Knd;Id;KindDeq;IdDeq);,x@0>;2of(2of(2of(2of(
12. & (deq-member(product-deq(Knd;Id;KindDeq;IdDeq);,x@0>;if eqof(IdDeq)(i@0,i)
12. & (deq-member(product-deq(Knd;Id;KindDeq;IdDeq);,x@0>;if <<[x],x.T>
12. & (deq-member(product-deq(Knd;Id;KindDeq;IdDeq);,x@0>;if ,
12. & (deq-member(product-deq(Knd;Id;KindDeq;IdDeq);,x@0>;if ,
12. & (deq-member(product-deq(Knd;Id;KindDeq;IdDeq);,x@0>;if ,
12. & (deq-member(product-deq(Knd;Id;KindDeq;IdDeq);,x@0>;if ,
12. & (deq-member(product-deq(Knd;Id;KindDeq;IdDeq);,x@0>;if ,
12. & (deq-member(product-deq(Knd;Id;KindDeq;IdDeq);,x@0>;if ,<[x],x.L>
12. & (deq-member(product-deq(Knd;Id;KindDeq;IdDeq);,x@0>;if ,
12. & (deq-member(product-deq(Knd;Id;KindDeq;IdDeq);,x@0>;if ,>
12. & (deq-member(product-deq(Knd;Id;KindDeq;IdDeq);,x@0>;else  fi)))))))
12. & (
12. & (s(i@0;t+1).x@0
12. & (=
12. & (2of(1of(2of(2of(2of(2of(if eqof(IdDeq)(i@0,i)
12. & (2of(1of(2of(2of(2of(2of(if <<[x],x.T>,,,,,,<[x],x.L>,,>
12. & (2of(1of(2of(2of(2of(2of(else  fi))))))
12. & ((<kind(a(i@0;t)),x@0>
12. & (,x.s(i@0;t).x
12. & (,val(a(i@0;t))))
12. & (l:IdLnk. 
12. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);<kind(a(i@0;t)),l>;1of(
12. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);<kind(a(i@0;t)),l>;1of(
12. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);<kind(a(i@0;t)),l>;2of(
12. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);<kind(a(i@0;t)),l>;2of(
12. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);<kind(a(i@0;t)),l>;2of(
12. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);<kind(a(i@0;t)),l>;2of(
12. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);<kind(a(i@0;t)),l>;2of(
12. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);<kind(a(i@0;t)),l>;if eqof(IdDeq)
12. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);<kind(a(i@0;t)),l>;if (i@0
12. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);<kind(a(i@0;t)),l>;if ,i)
12. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);<kind(a(i@0;t)),l>;if <<[x]
12. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);<kind(a(i@0;t)),l>;if <,x.
12. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);<kind(a(i@0;t)),l>;if <,T>
12. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);<kind(a(i@0;t)),l>;if ,
12. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);<kind(a(i@0;t)),l>;if ,
12. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);<kind(a(i@0;t)),l>;if ,
12. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);<kind(a(i@0;t)),l>;if ,
12. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);<kind(a(i@0;t)),l>;if ,
12. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);<kind(a(i@0;t)),l>;if ,<[x]
12. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);<kind(a(i@0;t)),l>;if ,,x.
12. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);<kind(a(i@0;t)),l>;if ,,L>
12. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);<kind(a(i@0;t)),l>;if ,
12. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);<kind(a(i@0;t)),l>;if ,>
12. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);<kind(a(i@0;t)),l>;else  fi))))))))
12. & (
12. & (withlnk(l;m(i@0;t))
12. & (=
12. & (if source(l) = i@0
12. & (if concat(map(tgf.map(x.
12. & (if <1of(tgf),x>;2of(tgf)
12. & (if <1of(tgf),x>;((x.s(i@0;t).x)
12. & (if <1of(tgf),x>;,val(a(i@0;t))));2of(1of(2of(2of(2of(2of(2of(
12. & (if <1of(tgf),x>;,val(a(i@0;t))));2of(1of(if eqof(IdDeq)(i@0,i)
12. & (if <1of(tgf),x>;,val(a(i@0;t))));2of(1of(if <<[x],x.T>
12. & (if <1of(tgf),x>;,val(a(i@0;t))));2of(1of(if ,
12. & (if <1of(tgf),x>;,val(a(i@0;t))));2of(1of(if ,
12. & (if <1of(tgf),x>;,val(a(i@0;t))));2of(1of(if ,
12. & (if <1of(tgf),x>;,val(a(i@0;t))));2of(1of(if ,
12. & (if <1of(tgf),x>;,val(a(i@0;t))));2of(1of(if ,
12. & (if <1of(tgf),x>;,val(a(i@0;t))));2of(1of(if ,<[x],x.L>
12. & (if <1of(tgf),x>;,val(a(i@0;t))));2of(1of(if ,
12. & (if <1of(tgf),x>;,val(a(i@0;t))));2of(1of(if ,>
12. & (if <1of(tgf),x>;,val(a(i@0;t))));2of(1of(else  fi)))))))
12. & (if <1of(tgf),x>;,val(a(i@0;t))));(<kind(a(i@0;t)),l>)))
12. & (else nil fi)
12. & (x@0:Id. 
12. & ((deq-member(IdDeq;x@0;1of(1of(2of(2of(2of(2of(2of(2of(if eqof(IdDeq)
12. & ((deq-member(IdDeq;x@0;1of(1of(2of(2of(2of(2of(2of(2of(if (i@0
12. & ((deq-member(IdDeq;x@0;1of(1of(2of(2of(2of(2of(2of(2of(if ,i)
12. & ((deq-member(IdDeq;x@0;1of(1of(2of(2of(2of(2of(2of(2of(if <<[x],x.T>
12. & ((deq-member(IdDeq;x@0;1of(1of(2of(2of(2of(2of(2of(2of(if ,
12. & ((deq-member(IdDeq;x@0;1of(1of(2of(2of(2of(2of(2of(2of(if ,
12. & ((deq-member(IdDeq;x@0;1of(1of(2of(2of(2of(2of(2of(2of(if ,
12. & ((deq-member(IdDeq;x@0;1of(1of(2of(2of(2of(2of(2of(2of(if ,
12. & ((deq-member(IdDeq;x@0;1of(1of(2of(2of(2of(2of(2of(2of(if ,
12. & ((deq-member(IdDeq;x@0;1of(1of(2of(2of(2of(2of(2of(2of(if ,<[x],x.L>
12. & ((deq-member(IdDeq;x@0;1of(1of(2of(2of(2of(2of(2of(2of(if ,
12. & ((deq-member(IdDeq;x@0;1of(1of(2of(2of(2of(2of(2of(2of(if ,>
12. & ((deq-member(IdDeq;x@0;1of(1of(2of(2of(2of(2of(2of(2of(else  fi)))))))))
12. & ((
12. & ((deq-member(KindDeq;kind(a(i@0;t));2of(1of(2of(2of(2of(2of(2of(2of(
12. & ((deq-member(KindDeq;kind(a(i@0;t));2of(1of(if eqof(IdDeq)(i@0,i)
12. & ((deq-member(KindDeq;kind(a(i@0;t));2of(1of(if <<[x],x.T>
12. & ((deq-member(KindDeq;kind(a(i@0;t));2of(1of(if ,
12. & ((deq-member(KindDeq;kind(a(i@0;t));2of(1of(if ,
12. & ((deq-member(KindDeq;kind(a(i@0;t));2of(1of(if ,
12. & ((deq-member(KindDeq;kind(a(i@0;t));2of(1of(if ,
12. & ((deq-member(KindDeq;kind(a(i@0;t));2of(1of(if ,
12. & ((deq-member(KindDeq;kind(a(i@0;t));2of(1of(if ,<[x],x.L>
12. & ((deq-member(KindDeq;kind(a(i@0;t));2of(1of(if ,
12. & ((deq-member(KindDeq;kind(a(i@0;t));2of(1of(if ,>
12. & ((deq-member(KindDeq;kind(a(i@0;t));2of(1of(else  fi))))))))
12. & ((deq-member(KindDeq;kind(a(i@0;t));(x@0)))
12. & (
12. & (s(i@0;t).x@0 = s(i@0;t+1).x@0)
12. & (l:IdLnk, tg:Id.
12. & ((deq-member(product-deq(IdLnk;Id;IdLnkDeq;IdDeq);<l
12. & ((deq-member(product-deq(IdLnk;Id;IdLnkDeq;IdDeq);,tg>;1of(1of(
12. & ((deq-member(product-deq(IdLnk;Id;IdLnkDeq;IdDeq);,tg>;2of(2of(2of(2of(
12. & ((deq-member(product-deq(IdLnk;Id;IdLnkDeq;IdDeq);,tg>;2of(2of(2of(
12. & ((deq-member(product-deq(IdLnk;Id;IdLnkDeq;IdDeq);,tg>;if eqof(IdDeq)
12. & ((deq-member(product-deq(IdLnk;Id;IdLnkDeq;IdDeq);,tg>;if (i@0
12. & ((deq-member(product-deq(IdLnk;Id;IdLnkDeq;IdDeq);,tg>;if ,i)
12. & ((deq-member(product-deq(IdLnk;Id;IdLnkDeq;IdDeq);,tg>;if <<[x],x.T>
12. & ((deq-member(product-deq(IdLnk;Id;IdLnkDeq;IdDeq);,tg>;if ,
12. & ((deq-member(product-deq(IdLnk;Id;IdLnkDeq;IdDeq);,tg>;if ,
12. & ((deq-member(product-deq(IdLnk;Id;IdLnkDeq;IdDeq);,tg>;if ,
12. & ((deq-member(product-deq(IdLnk;Id;IdLnkDeq;IdDeq);,tg>;if ,
12. & ((deq-member(product-deq(IdLnk;Id;IdLnkDeq;IdDeq);,tg>;if ,
12. & ((deq-member(product-deq(IdLnk;Id;IdLnkDeq;IdDeq);,tg>;if ,<[x],x.L>
12. & ((deq-member(product-deq(IdLnk;Id;IdLnkDeq;IdDeq);,tg>;if ,
12. & ((deq-member(product-deq(IdLnk;Id;IdLnkDeq;IdDeq);,tg>;if ,>
12. & ((deq-member(product-deq(IdLnk;Id;IdLnkDeq;IdDeq);,tg>;else  fi))))))))))
12. & ((
12. & ((deq-member(KindDeq;kind(a(i@0;t));2of(1of(2of(2of(2of(2of(2of(2of(2of(
12. & ((deq-member(KindDeq;kind(a(i@0;t));2of(1of(if eqof(IdDeq)(i@0,i)
12. & ((deq-member(KindDeq;kind(a(i@0;t));2of(1of(if <<[x],x.T>
12. & ((deq-member(KindDeq;kind(a(i@0;t));2of(1of(if ,
12. & ((deq-member(KindDeq;kind(a(i@0;t));2of(1of(if ,
12. & ((deq-member(KindDeq;kind(a(i@0;t));2of(1of(if ,
12. & ((deq-member(KindDeq;kind(a(i@0;t));2of(1of(if ,
12. & ((deq-member(KindDeq;kind(a(i@0;t));2of(1of(if ,
12. & ((deq-member(KindDeq;kind(a(i@0;t));2of(1of(if ,<[x],x.L>
12. & ((deq-member(KindDeq;kind(a(i@0;t));2of(1of(if ,
12. & ((deq-member(KindDeq;kind(a(i@0;t));2of(1of(if ,>
12. & ((deq-member(KindDeq;kind(a(i@0;t));2of(1of(else  fi)))))))))
12. & ((deq-member(KindDeq;kind(a(i@0;t));(<l,tg>)))
12. & (
12. & (w-tagged(tg; onlnk(l;m(i@0;t))) = nil)
13. vartype(i;x) r T
14. e1 : Id
15. e2 : 
16. isnull(a(e1;e2))  [not for witness]
17. e1 = i
  (s(e1;e2+1).x = s(e1;e2).x  T  (kind(a(e1;e2))  L))
  & ((kind(a(e1;e2))  L)  s(e1;e2+1).x = s(e1;e2).x  T)
By: AssertBY (isnull(a(i;e2)))
(SupposeNot THEN Assert False THEN Unhide THEN Analyze -1 THEN RevHypSubst -1 0)
THEN
InstHyp [i;e2] 12
THEN
RWO Thm* d:EqDecider(A), i:A. (eqof(d)(i,i)) ~ true -1
THEN
Reduce -1
THEN
SplitAndHyps
THEN
SimpleInstHyp x -2
THEN
ThinForallHyps
THEN
RWO Thm* d:EqDecider(A), i:A. (eqof(d)(i,i)) ~ true -1
THEN
Reduce -1
THEN
RWO Thm* eq:EqDecider(A), L:A List, x:A. deq-member(eq;x;L)  (x  L) -1
THEN
Reduce -1
THEN
TrySubsume

Generated subgoal:

1 8. vartype(i;x) r T
9. e1 : Id
10. e2 : 
11. isnull(a(e1;e2))  [not for witness]
12. e1 = i
13. isnull(a(i;e2))
14. islocal(kind(a(i;e2)))
14. 
14. deq-member(IdDeq;act(kind(a(i;e2)));1of())
14. 
14. 2of()(act(kind(a(i;e2))),x.s(i;e2).x,val(a(i;e2)))
15. (True  (kind(a(i;e2))  L))  s(i;e2).x = s(i;e2+1).x  T
  (s(e1;e2+1).x = s(e1;e2).x  T  (kind(a(e1;e2))  L))
  & ((kind(a(e1;e2))  L)  s(e1;e2+1).x = s(e1;e2).x  T)
10 steps

About:
pairproductlistconsnilbtrue
ifthenelseassertitvoidnatural_numberaddlambda
applyuniverseequalsqequaltopsubtype_relimpliesandfalse
all
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

(17steps total) PrintForm Definitions Lemmas mb event system 6 Sections EventSystems Doc