2. T : Type
3. v : T
4. x : Id
@i: x:T
@i: xinitially x = v realizes2 es.(vartype(i;x) 
r T)
& (
e:E. loc(e) = i 
Id 
first(e) (x when e) = v T) @i: x:T
@i: xinitially x = v realizes2 es.(vartype(i;x) r T)
& (e:E. loc(e) = i Id first(e) (x when e) = v T)| By: |
 Auto THEN DoSubsume THEN StrengthenSubtype in
RepeatFor 3 (Analyze 0) THEN Unfolds [`es-vartype`;`es-initially`;`w-es`] 0 THEN Reduce 0 THEN Analyze -1 THEN (let ops (let [`d-Loc`
(let ;`d-X`
(let ;`d-single-init`
(let ;`mk-d`
(let ;`d-m`
(let ;`mk-ma`
(let ;`ma-ds`
(let ;`ma-init`
(let ;`ma-single-init`
(let ;`fpf-val`
(let ;`fpf-dom`
(let ;`fpf-ap`
(let ;`fpf-cap`
(let ;`fpf-single`] in
(Repeat (Unfolds ops -1 THEN Reduce -1) THEN ExRepD THEN RepeatFor 2 (Thin -1) (THEN (AllHyps (  j.SimpleInstHyp i j THENA Complete Auto)
(THEN (AllHyps ( j.SimpleInstHyp x j THENA Complete T)
(THEN (AllHyps (( h.
((RWO Thm* d:EqDecider(A), i:A. (eqof(d)(i,i)) ~ true h THENA Complete Auto
((THEN ((Reduce h) (THEN (AllHyps (( h.
((RWO Thm* d:EqDecider(A), i:A. (eqof(d)(i,i)) ~ true h THENA Complete Auto
((THEN ((Reduce h) (THEN (Analyze 0 (THEN (Try Trivial) |
| 1 |
3. v : T 4. x : Id 5. w : World 6. p : 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 ,<[x],x.v>
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 , >
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.v>,,,,,,>
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.v>,,,,,,>
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.v>,,,,,,>
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.v>,,,,,,>
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.v>,,,,,,>
11. 2of(1of(2of(2of(else fi)))) 11. (x@0) 11. if deq-member(IdDeq;x@0;1of(1of(if eqof(IdDeq)(i@0,i)
11. if deq-member(IdDeq;x@0;1of(1of(if <<[x],x.T>,,<[x],x.v>,,,,,,>
11. if deq-member(IdDeq;x@0;1of(1of(else fi)))
11. if 2of(1of(if eqof(IdDeq)(i@0,i) <<[x],x.T>,,<[x],x.v>,,,,,,>
11. if 2of(1of(else fi))
11. if (x@0)
11. else Void fi
12. x@0:Id.
12. (eqof(IdDeq)(x,x@0)  false)
12.
12. s(i;0).x@0 = v if eqof(IdDeq)(x,x@0) false T else Void fi
13. a:Action(i).
13. isnull(a) (valtype(i;a) r <<[x],x.T>,,<[x],x.v>,,,,,,>.da(kind(a)))
14. x@0:Id. vartype(i;x@0) r if eqof(IdDeq)(x,x@0) false T else Top fi
15. vartype(i;x) r T
16. True s(i;0).x = v T
17. x@0:Id.
17. deq-member(IdDeq;x@0;1of(1of(2of(2of(if eqof(IdDeq)(x,i)
17. deq-member(IdDeq;x@0;1of(1of(2of(2of(if <<[x], x.T>,,<[x],x.v>,,,,,,>
17. deq-member(IdDeq;x@0;1of(1of(2of(2of(else fi))))) 17.
17. s(x;0).x@0 17. = 17. 2of(1of(2of(2of(if eqof(IdDeq)(x,i) <<[x],x.T>,,<[x],x.v>,,,,,,>
17. 2of(1of(2of(2of(else fi)))) 17. (x@0) 17. if deq-member(IdDeq;x@0;1of(1of(if eqof(IdDeq)(x,i)
17. if deq-member(IdDeq;x@0;1of(1of(if <<[x],x.T>,,<[x],x.v>,,,,,,>
17. if deq-member(IdDeq;x@0;1of(1of(else fi)))
17. if 2of(1of(if eqof(IdDeq)(x,i) <<[x],x.T>,,<[x],x.v>,,,,,,> else fi))
17. if (x@0)
17. else Void fi
18. a:Action(x).
18. isnull(a)
18.
18. (valtype(x;a) r if eqof(IdDeq)(x,i) <<[x],x.T>,,<[x],x.v>,,,,,,>
18. (valtype(x;a) r else fi.da(kind(a)))
19. x@0:Id.
19. vartype(x;x@0) r if deq-member(IdDeq;x@0;1of(1of(if eqof(IdDeq)(x,i)
19. vartype(x;x@0) r if deq-member(IdDeq;x@0;1of(1of(if <<[x],x.T>
19. vartype(x;x@0) r if deq-member(IdDeq;x@0;1of(1of(if ,
19. vartype(x;x@0) r if deq-member(IdDeq;x@0;1of(1of(if ,<[x],x.v>
19. vartype(x;x@0) r if deq-member(IdDeq;x@0;1of(1of(if ,
19. vartype(x;x@0) r if deq-member(IdDeq;x@0;1of(1of(if ,
19. vartype(x;x@0) r if deq-member(IdDeq;x@0;1of(1of(if ,
19. vartype(x;x@0) r if deq-member(IdDeq;x@0;1of(1of(if ,
19. vartype(x;x@0) r if deq-member(IdDeq;x@0;1of(1of(if ,
19. vartype(x;x@0) r if deq-member(IdDeq;x@0;1of(1of(if ,>
19. vartype(x;x@0) r if deq-member(IdDeq;x@0;1of(1of(else fi)))
19. vartype(x;x@0) r if 2of(1of(if eqof(IdDeq)(x,i)
19. vartype(x;x@0) r if 2of(1of(if <<[x],x.T>,,<[x],x.v>,,,,,,>
19. vartype(x;x@0) r if 2of(1of(else fi))
19. vartype(x;x@0) r if (x@0)
19. vartype(x;x@0) r else Top fi
20. vartype(i;x) r T
e:E. loc(e) = i Id first(e) (x when e) = v T | 29 steps |
About:
 |  |  |  |  |  |  |  |  |  |  |  |