File: SW.th

package info (click to toggle)
hol88 2.02.19940316-28
links: PTS
area: main
in suites: jessie, jessie-kfreebsd
size: 65,924 kB
ctags: 21,595
sloc: ml: 199,939; ansic: 9,666; sh: 7,118; makefile: 6,075; lisp: 2,747; yacc: 894; sed: 201; cpp: 87; awk: 5
file content (4 lines) | stat: -rw-r--r-- 55,998 bytes
parent folder | download | duplicates (11)

(SETQ %THEORYDATA '((PARENTS |plusm_subm| |hdi_tli| |myarith| |SWnew|) (TYPES) (NAMETYPES) (OPERATORS (LIVE_ASSUM |fun| (|fun| (|num|) (|bool|)) (|fun| (|num|) (|bool|))) (IMPL |fun| (|list| (%VARTYPE . *)) (|fun| (|num|) (|fun| (|fun| (|num|) (|list| (%VARTYPE . *))) (|fun| (|fun| (|num|) (|num|)) (|fun| (|num|) (|fun| (|fun| (|num|) (|fun| (|num|) (|bool|))) (|fun| (|fun| (|num|) (|num|)) (|fun| (|fun| (|num|) (|num|)) (|fun| (|fun| (|num|) (|bool|)) (|fun| (|num|) (|fun| (|fun| (|num|) (|list| (%VARTYPE . *))) (|fun| (|fun| (|num|) (|num|)) (|fun| (|num|) (|fun| (|fun| (|num|) (|bool|)) (|fun| (|fun| (|num|) (|sum| (|prod| (|num|) (%VARTYPE . *)) (|one|))) (|fun| (|fun| (|num|) (|sum| (|prod| (|num|) (%VARTYPE . *)) (|one|))) (|fun| (|fun| (|num|) (|sum| (|prod| (|num|) (%VARTYPE . *)) (|one|))) (|fun| (|fun| (|num|) (|sum| (|prod| (|num|) (%VARTYPE . *)) (|one|))) (|bool|))))))))))))))))))) (RECEIVER |fun| (|num|) (|fun| (|num|) (|fun| (|fun| (|num|) (|list| (%VARTYPE . *))) (|fun| (|fun| (|num|) (|num|)) (|fun| (|fun| (|num|) (|bool|)) (|fun| (|fun| (|num|) (|sum| (|prod| (|num|) (%VARTYPE . *)) (|one|))) (|fun| (|fun| (|num|) (|sum| (|prod| (|num|) (%VARTYPE . *)) (|one|))) (|bool|)))))))) (ABORT |fun| (|fun| (|num|) (|num|)) (|fun| (|fun| (|num|) (|bool|)) (|fun| (|num|) (|fun| (|num|) (|fun| (|num|) (|fun| (|fun| (|num|) (|num|)) (|fun| (|fun| (|num|) (|list| (%VARTYPE . *))) (|fun| (|fun| (|num|) (|sum| (|prod| (|num|) (%VARTYPE . *)) (|one|))) (|bool|))))))))) (SENDER |fun| (|num|) (|fun| (|num|) (|fun| (|fun| (|num|) (|list| (%VARTYPE . *))) (|fun| (|fun| (|num|) (|num|)) (|fun| (|fun| (|num|) (|fun| (|num|) (|bool|))) (|fun| (|fun| (|num|) (|num|)) (|fun| (|fun| (|num|) (|sum| (|prod| (|num|) (%VARTYPE . *)) (|one|))) (|fun| (|fun| (|num|) (|sum| (|prod| (|num|) (%VARTYPE . *)) (|one|))) (|bool|))))))))) (ACK_RECV |fun| (|fun| (|num|) (|sum| (|prod| (|num|) (%VARTYPE . *)) (|one|))) (|fun| (|num|) (|fun| (|num|) (|fun| (|fun| (|num|) (|list| (%VARTYPE . *))) (|fun| (|fun| (|num|) (|num|)) (|bool|)))))) (ACK_TRANS |fun| (|fun| (|num|) (|num|)) (|fun| (|num|) (|fun| (|fun| (|num|) (|bool|)) (|fun| (|fun| (|num|) (|sum| (|prod| (|num|) (%VARTYPE . *)) (|one|))) (|bool|))))) (DATA_RECV |fun| (|fun| (|num|) (|sum| (|prod| (|num|) (%VARTYPE . *)) (|one|))) (|fun| (|num|) (|fun| (|num|) (|fun| (|fun| (|num|) (|list| (%VARTYPE . *))) (|fun| (|fun| (|num|) (|num|)) (|bool|)))))) (IN_WINDOW |fun| (|sum| (|prod| (|num|) (%VARTYPE . *)) (|one|)) (|fun| (|num|) (|fun| (|num|) (|fun| (|num|) (|bool|))))) (DATA_TRANS |fun| (|fun| (|num|) (|list| (%VARTYPE . *))) (|fun| (|fun| (|num|) (|num|)) (|fun| (|num|) (|fun| (|num|) (|fun| (|fun| (|num|) (|fun| (|num|) (|bool|))) (|fun| (|fun| (|num|) (|num|)) (|fun| (|fun| (|num|) (|sum| (|prod| (|num|) (%VARTYPE . *)) (|one|))) (|bool|)))))))) (CHANNEL |fun| (|fun| (|num|) (|sum| (|prod| (|num|) (%VARTYPE . *)) (|one|))) (|fun| (|fun| (|num|) (|sum| (|prod| (|num|) (%VARTYPE . *)) (|one|))) (|bool|))) (INIT |fun| (|list| (%VARTYPE . *)) (|fun| (|num|) (|fun| (|fun| (|num|) (|list| (%VARTYPE . *))) (|fun| (|fun| (|num|) (|num|)) (|fun| (|fun| (|num|) (|list| (%VARTYPE . *))) (|fun| (|fun| (|num|) (|num|)) (|bool|))))))) (|message| |fun| (|sum| (|prod| (|num|) (%VARTYPE . *)) (|one|)) (%VARTYPE . *)) (|label| |fun| (|sum| (|prod| (|num|) (%VARTYPE . *)) (|one|)) (|num|)) (|new_packet| |fun| (|num|) (|fun| (%VARTYPE . *) (|sum| (|prod| (|num|) (%VARTYPE . *)) (|one|)))) (|good_packet| |fun| (|sum| (|prod| (|num|) (%VARTYPE . *)) (|one|)) (|bool|)) (|set_non_packet| |sum| (|prod| (|num|) (%VARTYPE . *)) (|one|))) (PAIRED-INFIXES) (CURRIED-INFIXES) (PREDICATES) (VERSION . "1.12 (Sun4/Allegro 4.0)") (STAMP . 2878467905))) 

(SETQ %THEOREMS '((SHARETYPES 10 (|q%9| |fun| (|num|) (|bool|)) (|,%8| |prod| (|num|) (|num|)) (|p%7| |fun| (|num|) (|fun| (|num|) (|bool|))) (|inC%6| |fun| (|num|) (|sum| (|prod| (|num|) (%VARTYPE . *)) (|one|))) (|s%5| |fun| (|num|) (|num|)) (|rem%4| |fun| (|num|) (|list| (%VARTYPE . *))) (|source%3| |list| (%VARTYPE . *)) (|,%2| |prod| (|num|) (%VARTYPE . *)) (|dd%1| %VARTYPE . *) (|set_non_packet%0| |sum| (|prod| (|num|) (%VARTYPE . *)) (|one|))) (AXIOM (LIVE_ASSUM PRED HOL_ASSERT COMB ((CONST HOL_DEFINITION) COMB ((CONST !) ABS ((VAR |aborted| %T . |q%9|) COMB ((CONST !) ABS ((VAR |maxT| |num|) COMB ((COMB ((CONST =) COMB ((COMB ((CONST LIVE_ASSUM) VAR |aborted|)) VAR |maxT|))) COMB ((CONST !) ABS ((VAR |t| |num|) COMB ((CONST ~) COMB ((VAR |aborted| %T . |q%9|) COMB ((COMB ((CONST +) VAR |t|)) COMB ((COMB ((CONST +) VAR |maxT|)) CONST |1|)))))) |bool|) |bool|)) |bool|)))) (IMPL PRED HOL_ASSERT COMB ((CONST HOL_DEFINITION) COMB ((CONST !) ABS ((VAR |source| %T . |source%3|) COMB ((CONST !) ABS ((VAR |maxseq| |num|) COMB ((CONST !) ABS ((VAR |rem| %T . |rem%4|) COMB ((CONST !) ABS ((VAR |s| %T . |s%5|) COMB ((CONST !) ABS ((VAR SW |num|) COMB ((CONST !) ABS ((VAR |p| %T . |p%7|) COMB ((CONST !) ABS ((VAR |i| %T . |s%5|) COMB ((CONST !) ABS ((VAR |c| %T . |s%5|) COMB ((CONST !) ABS ((VAR |aborted| %T . |q%9|) COMB ((CONST !) ABS ((VAR |maxT| |num|) COMB ((CONST !) ABS ((VAR |sink| %T . |rem%4|) COMB ((CONST !) ABS ((VAR |r| %T . |s%5|) COMB ((CONST !) ABS ((VAR RW |num|) COMB ((CONST !) ABS ((VAR |q| %T . |q%9|) COMB ((CONST !) ABS ((VAR |dataS| %T . |inC%6|) COMB ((CONST !) ABS ((VAR |dataR| %T . |inC%6|) COMB ((CONST !) ABS ((VAR |ackS| %T . |inC%6|) COMB ((CONST !) ABS ((VAR |ackR| %T . |inC%6|) COMB ((COMB ((CONST =) COMB ((COMB ((COMB ((COMB ((COMB ((COMB ((COMB ((COMB ((COMB ((COMB ((COMB ((COMB ((COMB ((COMB ((COMB ((COMB ((COMB ((COMB ((CONST IMPL) VAR |source| %T . |source%3|)) VAR |maxseq| |num|)) VAR |rem| %T . |rem%4|)) VAR |s| %T . |s%5|)) VAR SW |num|)) VAR |p| %T . |p%7|)) VAR |i| %T . |s%5|)) VAR |c| %T . |s%5|)) VAR |aborted| %T . |q%9|)) VAR |maxT| |num|)) VAR |sink| %T . |rem%4|)) VAR |r| %T . |s%5|)) VAR RW |num|)) VAR |q| %T . |q%9|)) VAR |dataS| %T . |inC%6|)) VAR |dataR| %T . |inC%6|)) VAR |ackS| %T . |inC%6|)) VAR |ackR| %T . |inC%6|) |bool|)) COMB ((COMB ((CONST |/\\|) COMB ((COMB ((COMB ((COMB ((COMB ((COMB ((CONST INIT) VAR |source| %T . |source%3|)) VAR |maxseq| |num|)) VAR |rem| %T . |rem%4|)) VAR |s| %T . |s%5|)) VAR |sink| %T . |rem%4|)) VAR |r| %T . |s%5|))) COMB ((COMB ((CONST |/\\|) COMB ((COMB ((COMB ((COMB ((COMB ((COMB ((COMB ((COMB ((CONST SENDER) VAR |maxseq| |num|)) VAR SW |num|)) VAR |rem| %T . |rem%4|)) VAR |s| %T . |s%5|)) VAR |p| %T . |p%7|)) VAR |i| %T . |s%5|)) VAR |dataS| %T . |inC%6|)) VAR |ackS| %T . |inC%6|))) COMB ((COMB ((CONST |/\\|) COMB ((COMB ((COMB ((COMB ((COMB ((COMB ((COMB ((COMB ((CONST ABORT) VAR |c| %T . |s%5|)) VAR |aborted| %T . |q%9|)) VAR |maxT| |num|)) VAR |maxseq| |num|)) VAR SW |num|)) VAR |s| %T . |s%5|)) VAR |rem| %T . |rem%4|)) VAR |ackS| %T . |inC%6|))) COMB ((COMB ((CONST |/\\|) COMB ((COMB ((CONST CHANNEL) VAR |dataS| %T . |inC%6|)) VAR |dataR| %T . |inC%6|))) COMB ((COMB ((CONST |/\\|) COMB ((COMB ((COMB ((COMB ((COMB ((COMB ((COMB ((CONST RECEIVER) VAR |maxseq| |num|)) VAR RW |num|)) VAR |sink| %T . |rem%4|)) VAR |r| %T . |s%5|)) VAR |q| %T . |q%9|)) VAR |ackR| %T . |inC%6|)) VAR |dataR| %T . |inC%6|))) COMB ((COMB ((CONST CHANNEL) VAR |ackR| %T . |inC%6|)) VAR |ackS| %T . |inC%6|))))))) |bool|)) |bool|)) |bool|)) |bool|)) |bool|)) |bool|)) |bool|)) |bool|)) |bool|)) |bool|)) |bool|)) |bool|)) |bool|)) |bool|)) |bool|)) |bool|)) |bool|)) |bool|)))) (RECEIVER PRED HOL_ASSERT COMB ((CONST HOL_DEFINITION) COMB ((CONST !) ABS ((VAR |maxseq| |num|) COMB ((CONST !) ABS ((VAR RW |num|) COMB ((CONST !) ABS ((VAR |sink| %T . |rem%4|) COMB ((CONST !) ABS ((VAR |r| %T . |s%5|) COMB ((CONST !) ABS ((VAR |q| %T . |q%9|) COMB ((CONST !) ABS ((VAR |ackR| %T . |inC%6|) COMB ((CONST !) ABS ((VAR |dataR| %T . |inC%6|) COMB ((COMB ((CONST =) COMB ((COMB ((COMB ((COMB ((COMB ((COMB ((COMB ((CONST RECEIVER) VAR |maxseq| |num|)) VAR RW |num|)) VAR |sink| %T . |rem%4|)) VAR |r| %T . |s%5|)) VAR |q| %T . |q%9|)) VAR |ackR| %T . |inC%6|)) VAR |dataR| %T . |inC%6|) |bool|)) COMB ((COMB ((CONST |/\\|) COMB ((COMB ((COMB ((COMB ((CONST ACK_TRANS) VAR |r| %T . |s%5|)) VAR |maxseq| |num|)) VAR |q| %T . |q%9|)) VAR |ackR| %T . |inC%6|))) COMB ((COMB ((COMB ((COMB ((COMB ((CONST DATA_RECV) VAR |dataR| %T . |inC%6|)) VAR RW |num|)) VAR |maxseq| |num|)) VAR |sink| %T . |rem%4|)) VAR |r| %T . |s%5|))) |bool|)) |bool|)) |bool|)) |bool|)) |bool|)) |bool|)) |bool|)))) (ABORT PRED HOL_ASSERT COMB ((CONST HOL_DEFINITION) COMB ((CONST !) ABS ((VAR |c| %T . |s%5|) COMB ((CONST !) ABS ((VAR |aborted| %T . |q%9|) COMB ((CONST !) ABS ((VAR |maxT| |num|) COMB ((CONST !) ABS ((VAR |maxseq| |num|) COMB ((CONST !) ABS ((VAR SW |num|) COMB ((CONST !) ABS ((VAR |s| %T . |s%5|) COMB ((CONST !) ABS ((VAR |rem| %T . |rem%4|) COMB ((CONST !) ABS ((VAR |ackS| %T . |inC%6|) COMB ((COMB ((CONST =) COMB ((COMB ((COMB ((COMB ((COMB ((COMB ((COMB ((COMB ((CONST ABORT) VAR |c| %T . |s%5|)) VAR |aborted| %T . |q%9|)) VAR |maxT| |num|)) VAR |maxseq| |num|)) VAR SW |num|)) VAR |s| %T . |s%5|)) VAR |rem| %T . |rem%4|)) VAR |ackS| %T . |inC%6|) |bool|)) COMB ((CONST !) ABS ((VAR |t| |num|) COMB ((COMB ((CONST |/\\|) COMB ((COMB ((CONST =) COMB ((VAR |c| %T . |s%5|) CONST |0|))) CONST |0|))) COMB ((COMB ((CONST |/\\|) COMB ((COMB ((CONST =) COMB ((VAR |c| %T . |s%5|) COMB ((COMB ((CONST +) VAR |t|)) CONST |1|)))) COMB ((COMB ((COMB ((CONST COND) COMB ((COMB ((COMB ((COMB ((CONST IN_WINDOW) COMB ((VAR |ackS| %T . |inC%6|) VAR |t|))) COMB ((VAR |s| %T . |s%5|) VAR |t|))) VAR SW |num|)) VAR |maxseq| |num|) |bool|)) CONST |0|)) COMB ((COMB ((CONST +) COMB ((VAR |c| %T . |s%5|) VAR |t|))) CONST |1|)) |num|))) COMB ((COMB ((CONST |/\\|) COMB ((COMB ((CONST =) COMB ((VAR |aborted| %T . |q%9|) CONST |0|))) CONST F))) COMB ((COMB ((CONST =) COMB ((VAR |aborted| %T . |q%9|) COMB ((COMB ((CONST +) VAR |t|)) CONST |1|)))) COMB ((COMB ((CONST |/\\|) COMB ((COMB ((CONST |\\/|) COMB ((COMB ((CONST >=) COMB ((VAR |c| %T . |s%5|) VAR |t|))) VAR |maxT|))) COMB ((VAR |aborted| %T . |q%9|) VAR |t|)))) COMB ((CONST ~) COMB ((CONST NULL) COMB ((VAR |rem| %T . |rem%4|) VAR |t|)))))))))) |bool|) |bool|)) |bool|)) |bool|)) |bool|)) |bool|)) |bool|)) |bool|)) |bool|)))) (SENDER PRED HOL_ASSERT COMB ((CONST HOL_DEFINITION) COMB ((CONST !) ABS ((VAR |maxseq| |num|) COMB ((CONST !) ABS ((VAR SW |num|) COMB ((CONST !) ABS ((VAR |rem| %T . |rem%4|) COMB ((CONST !) ABS ((VAR |s| %T . |s%5|) COMB ((CONST !) ABS ((VAR |p| %T . |p%7|) COMB ((CONST !) ABS ((VAR |i| %T . |s%5|) COMB ((CONST !) ABS ((VAR |dataS| %T . |inC%6|) COMB ((CONST !) ABS ((VAR |ackS| %T . |inC%6|) COMB ((COMB ((CONST =) COMB ((COMB ((COMB ((COMB ((COMB ((COMB ((COMB ((COMB ((CONST SENDER) VAR |maxseq| |num|)) VAR SW |num|)) VAR |rem| %T . |rem%4|)) VAR |s| %T . |s%5|)) VAR |p| %T . |p%7|)) VAR |i| %T . |s%5|)) VAR |dataS| %T . |inC%6|)) VAR |ackS| %T . |inC%6|) |bool|)) COMB ((COMB ((CONST |/\\|) COMB ((COMB ((COMB ((COMB ((COMB ((COMB ((COMB ((CONST DATA_TRANS) VAR |rem| %T . |rem%4|)) VAR |s| %T . |s%5|)) VAR SW |num|)) VAR |maxseq| |num|)) VAR |p| %T . |p%7|)) VAR |i| %T . |s%5|)) VAR |dataS| %T . |inC%6|))) COMB ((COMB ((COMB ((COMB ((COMB ((CONST ACK_RECV) VAR |ackS| %T . |inC%6|)) VAR SW |num|)) VAR |maxseq| |num|)) VAR |rem| %T . |rem%4|)) VAR |s| %T . |s%5|))) |bool|)) |bool|)) |bool|)) |bool|)) |bool|)) |bool|)) |bool|)) |bool|)))) (ACK_RECV PRED HOL_ASSERT COMB ((CONST HOL_DEFINITION) COMB ((CONST !) ABS ((VAR |ackS| %T . |inC%6|) COMB ((CONST !) ABS ((VAR SW |num|) COMB ((CONST !) ABS ((VAR |maxseq| |num|) COMB ((CONST !) ABS ((VAR |rem| %T . |rem%4|) COMB ((CONST !) ABS ((VAR |s| %T . |s%5|) COMB ((COMB ((CONST =) COMB ((COMB ((COMB ((COMB ((COMB ((CONST ACK_RECV) VAR |ackS| %T . |inC%6|)) VAR SW |num|)) VAR |maxseq| |num|)) VAR |rem| %T . |rem%4|)) VAR |s| %T . |s%5|) |bool|)) COMB ((CONST !) ABS ((VAR |t| |num|) COMB ((COMB ((COMB ((CONST COND) COMB ((COMB ((COMB ((COMB ((CONST IN_WINDOW) COMB ((VAR |ackS| %T . |inC%6|) VAR |t|))) COMB ((VAR |s| %T . |s%5|) VAR |t|))) VAR SW |num|)) VAR |maxseq| |num|) |bool|)) COMB ((COMB ((CONST |/\\|) COMB ((COMB ((CONST =) COMB ((VAR |s| %T . |s%5|) COMB ((COMB ((CONST +) VAR |t|)) CONST |1|)))) COMB ((CONST |plusm|) COMB ((COMB ((CONST |,|) COMB ((CONST |label|) COMB ((VAR |ackS| %T . |inC%6|) VAR |t|)) |num|)) COMB ((COMB ((CONST |,|) CONST |1|)) VAR |maxseq| |num|) %T . |,%8|))))) COMB ((COMB ((CONST =) COMB ((VAR |rem| %T . |rem%4|) COMB ((COMB ((CONST +) VAR |t|)) CONST |1|)))) COMB ((COMB ((CONST TLI) COMB ((CONST |subm|) COMB ((COMB ((CONST |,|) COMB ((CONST |plusm|) COMB ((COMB ((CONST |,|) COMB ((CONST |label|) COMB ((VAR |ackS| %T . |inC%6|) VAR |t|)) |num|)) COMB ((COMB ((CONST |,|) CONST |1|)) VAR |maxseq| |num|) %T . |,%8|)))) COMB ((COMB ((CONST |,|) COMB ((VAR |s| %T . |s%5|) VAR |t|))) VAR |maxseq| |num|) %T . |,%8|)))) COMB ((VAR |rem| %T . |rem%4|) VAR |t|)) %T . |source%3|)))) COMB ((COMB ((CONST |/\\|) COMB ((COMB ((CONST =) COMB ((VAR |s| %T . |s%5|) COMB ((COMB ((CONST +) VAR |t|)) CONST |1|)))) COMB ((VAR |s| %T . |s%5|) VAR |t|)))) COMB ((COMB ((CONST =) COMB ((VAR |rem| %T . |rem%4|) COMB ((COMB ((CONST +) VAR |t|)) CONST |1|)))) COMB ((VAR |rem| %T . |rem%4|) VAR |t|)))) |bool|)) |bool|) |bool|)) |bool|)) |bool|)) |bool|)) |bool|)))) (ACK_TRANS PRED HOL_ASSERT COMB ((CONST HOL_DEFINITION) COMB ((CONST !) ABS ((VAR |r| %T . |s%5|) COMB ((CONST !) ABS ((VAR |maxseq| |num|) COMB ((CONST !) ABS ((VAR |q| %T . |q%9|) COMB ((CONST !) ABS ((VAR |ackR| %T . |inC%6|) COMB ((COMB ((CONST =) COMB ((COMB ((COMB ((COMB ((CONST ACK_TRANS) VAR |r| %T . |s%5|)) VAR |maxseq| |num|)) VAR |q| %T . |q%9|)) VAR |ackR| %T . |inC%6|) |bool|)) COMB ((CONST !) ABS ((VAR |t| |num|) COMB ((CONST !) ABS ((VAR |dummy| %T . |dd%1|) COMB ((COMB ((COMB ((CONST COND) COMB ((VAR |q| %T . |q%9|) VAR |t|))) COMB ((COMB ((CONST =) COMB ((VAR |ackR| %T . |inC%6|) VAR |t|))) COMB ((COMB ((CONST |new_packet|) COMB ((CONST |subm|) COMB ((COMB ((CONST |,|) COMB ((VAR |r| %T . |s%5|) VAR |t|))) COMB ((COMB ((CONST |,|) CONST |1|)) VAR |maxseq| |num|) %T . |,%8|)))) VAR |dummy| %T . |dd%1|) %T . |set_non_packet%0|) |bool|)) COMB ((COMB ((CONST =) COMB ((VAR |ackR| %T . |inC%6|) VAR |t|))) CONST |set_non_packet| %T . |set_non_packet%0|) |bool|) |bool|)) |bool|)) |bool|) |bool|)) |bool|)) |bool|)) |bool|)))) (DATA_RECV PRED HOL_ASSERT COMB ((CONST HOL_DEFINITION) COMB ((CONST !) ABS ((VAR |dataR| %T . |inC%6|) COMB ((CONST !) ABS ((VAR RW |num|) COMB ((CONST !) ABS ((VAR |maxseq| |num|) COMB ((CONST !) ABS ((VAR |sink| %T . |rem%4|) COMB ((CONST !) ABS ((VAR |r| %T . |s%5|) COMB ((COMB ((CONST =) COMB ((COMB ((COMB ((COMB ((COMB ((CONST DATA_RECV) VAR |dataR| %T . |inC%6|)) VAR RW |num|)) VAR |maxseq| |num|)) VAR |sink| %T . |rem%4|)) VAR |r| %T . |s%5|) |bool|)) COMB ((COMB ((CONST |/\\|) COMB ((COMB ((CONST =) VAR RW |num|)) CONST |1|))) COMB ((CONST !) ABS ((VAR |t| |num|) COMB ((COMB ((COMB ((CONST COND) COMB ((COMB ((COMB ((COMB ((CONST IN_WINDOW) COMB ((VAR |dataR| %T . |inC%6|) VAR |t|))) COMB ((VAR |r| %T . |s%5|) VAR |t|))) VAR RW |num|)) VAR |maxseq| |num|) |bool|)) COMB ((COMB ((CONST |/\\|) COMB ((COMB ((CONST =) COMB ((VAR |r| %T . |s%5|) COMB ((COMB ((CONST +) VAR |t|)) CONST |1|)))) COMB ((CONST |plusm|) COMB ((COMB ((CONST |,|) COMB ((VAR |r| %T . |s%5|) VAR |t|))) COMB ((COMB ((CONST |,|) CONST |1|)) VAR |maxseq| |num|) %T . |,%8|))))) COMB ((COMB ((CONST =) COMB ((VAR |sink| %T . |rem%4|) COMB ((COMB ((CONST +) VAR |t|)) CONST |1|)))) COMB ((COMB ((CONST APPEND) COMB ((VAR |sink| %T . |rem%4|) VAR |t|))) COMB ((COMB ((CONST CONS) COMB ((CONST |message|) COMB ((VAR |dataR| %T . |inC%6|) VAR |t|)) %T . |dd%1|)) CONST NIL %T . |source%3|) %T . |source%3|) %T . |source%3|)))) COMB ((COMB ((CONST |/\\|) COMB ((COMB ((CONST =) COMB ((VAR |r| %T . |s%5|) COMB ((COMB ((CONST +) VAR |t|)) CONST |1|)))) COMB ((VAR |r| %T . |s%5|) VAR |t|)))) COMB ((COMB ((CONST =) COMB ((VAR |sink| %T . |rem%4|) COMB ((COMB ((CONST +) VAR |t|)) CONST |1|)))) COMB ((VAR |sink| %T . |rem%4|) VAR |t|)))) |bool|)))) |bool|)) |bool|)) |bool|)) |bool|)) |bool|)))) (IN_WINDOW PRED HOL_ASSERT COMB ((CONST HOL_DEFINITION) COMB ((CONST !) ABS ((VAR |p| %T . |set_non_packet%0|) COMB ((CONST !) ABS ((VAR |b| |num|) COMB ((CONST !) ABS ((VAR |ws| |num|) COMB ((CONST !) ABS ((VAR |maxseq| |num|) COMB ((COMB ((CONST =) COMB ((COMB ((COMB ((COMB ((CONST IN_WINDOW) VAR |p| %T . |set_non_packet%0|)) VAR |b| |num|)) VAR |ws| |num|)) VAR |maxseq| |num|) |bool|)) COMB ((COMB ((CONST |/\\|) COMB ((CONST |good_packet|) VAR |p| %T . |set_non_packet%0|))) COMB ((COMB ((CONST <) COMB ((CONST |subm|) COMB ((COMB ((CONST |,|) COMB ((CONST |label|) VAR |p| %T . |set_non_packet%0|) |num|)) COMB ((COMB ((CONST |,|) VAR |b| |num|)) VAR |maxseq| |num|) %T . |,%8|)))) VAR |ws|))) |bool|)) |bool|)) |bool|)) |bool|)))) (DATA_TRANS PRED HOL_ASSERT COMB ((CONST HOL_DEFINITION) COMB ((CONST !) ABS ((VAR |rem| %T . |rem%4|) COMB ((CONST !) ABS ((VAR |s| %T . |s%5|) COMB ((CONST !) ABS ((VAR SW |num|) COMB ((CONST !) ABS ((VAR |maxseq| |num|) COMB ((CONST !) ABS ((VAR |p| %T . |p%7|) COMB ((CONST !) ABS ((VAR |i| %T . |s%5|) COMB ((CONST !) ABS ((VAR |dataS| %T . |inC%6|) COMB ((COMB ((CONST =) COMB ((COMB ((COMB ((COMB ((COMB ((COMB ((COMB ((CONST DATA_TRANS) VAR |rem| %T . |rem%4|)) VAR |s| %T . |s%5|)) VAR SW |num|)) VAR |maxseq| |num|)) VAR |p| %T . |p%7|)) VAR |i| %T . |s%5|)) VAR |dataS| %T . |inC%6|) |bool|)) COMB ((COMB ((CONST |/\\|) COMB ((COMB ((CONST =) VAR SW |num|)) COMB ((COMB ((CONST -) VAR |maxseq|)) CONST |1|)))) COMB ((CONST !) ABS ((VAR |t| |num|) COMB ((COMB ((CONST |/\\|) COMB ((COMB ((CONST ==>) COMB ((COMB ((VAR |p| %T . |p%7|) VAR |t|)) COMB ((VAR |i| %T . |s%5|) VAR |t|)))) COMB ((COMB ((CONST |/\\|) COMB ((CONST ~) COMB ((CONST NULL) COMB ((COMB ((CONST TLI) COMB ((VAR |i| %T . |s%5|) VAR |t|))) COMB ((VAR |rem| %T . |rem%4|) VAR |t|)) %T . |source%3|)))) COMB ((COMB ((CONST <) COMB ((VAR |i| %T . |s%5|) VAR |t|))) VAR SW))))) COMB ((COMB ((COMB ((CONST COND) COMB ((COMB ((CONST |/\\|) COMB ((COMB ((VAR |p| %T . |p%7|) VAR |t|)) COMB ((VAR |i| %T . |s%5|) VAR |t|)))) COMB ((CONST ~) COMB ((CONST NULL) COMB ((VAR |rem| %T . |rem%4|) VAR |t|)))))) COMB ((COMB ((CONST =) COMB ((VAR |dataS| %T . |inC%6|) VAR |t|))) COMB ((COMB ((CONST |new_packet|) COMB ((CONST |plusm|) COMB ((COMB ((CONST |,|) COMB ((VAR |s| %T . |s%5|) VAR |t|))) COMB ((COMB ((CONST |,|) COMB ((VAR |i| %T . |s%5|) VAR |t|))) VAR |maxseq| |num|) %T . |,%8|)))) COMB ((COMB ((CONST HDI) COMB ((VAR |i| %T . |s%5|) VAR |t|))) COMB ((VAR |rem| %T . |rem%4|) VAR |t|)) %T . |dd%1|) %T . |set_non_packet%0|) |bool|)) COMB ((COMB ((CONST =) COMB ((VAR |dataS| %T . |inC%6|) VAR |t|))) CONST |set_non_packet| %T . |set_non_packet%0|) |bool|)))))) |bool|)) |bool|)) |bool|)) |bool|)) |bool|)) |bool|)) |bool|)))) (CHANNEL PRED HOL_ASSERT COMB ((CONST HOL_DEFINITION) COMB ((CONST !) ABS ((VAR |inC| %T . |inC%6|) COMB ((CONST !) ABS ((VAR |outC| %T . |inC%6|) COMB ((COMB ((CONST =) COMB ((COMB ((CONST CHANNEL) VAR |inC| %T . |inC%6|)) VAR |outC| %T . |inC%6|) |bool|)) COMB ((CONST !) ABS ((VAR |t| |num|) COMB ((COMB ((CONST |\\/|) COMB ((COMB ((CONST =) COMB ((VAR |outC| %T . |inC%6|) VAR |t|))) COMB ((VAR |inC| %T . |inC%6|) VAR |t|)))) COMB ((COMB ((CONST =) COMB ((VAR |outC| %T . |inC%6|) VAR |t|))) CONST |set_non_packet| %T . |set_non_packet%0|)))) |bool|) |bool|)) |bool|)))) (INIT PRED HOL_ASSERT COMB ((CONST HOL_DEFINITION) COMB ((CONST !) ABS ((VAR |source| %T . |source%3|) COMB ((CONST !) ABS ((VAR |maxseq| |num|) COMB ((CONST !) ABS ((VAR |rem| %T . |rem%4|) COMB ((CONST !) ABS ((VAR |s| %T . |s%5|) COMB ((CONST !) ABS ((VAR |sink| %T . |rem%4|) COMB ((CONST !) ABS ((VAR |r| %T . |s%5|) COMB ((COMB ((CONST =) COMB ((COMB ((COMB ((COMB ((COMB ((COMB ((CONST INIT) VAR |source| %T . |source%3|)) VAR |maxseq| |num|)) VAR |rem| %T . |rem%4|)) VAR |s| %T . |s%5|)) VAR |sink| %T . |rem%4|)) VAR |r| %T . |s%5|) |bool|)) COMB ((COMB ((CONST |/\\|) COMB ((COMB ((CONST <) CONST |1|)) VAR |maxseq|))) COMB ((COMB ((CONST |/\\|) COMB ((COMB ((CONST =) COMB ((VAR |rem| %T . |rem%4|) CONST |0|))) VAR |source| %T . |source%3|))) COMB ((COMB ((CONST |/\\|) COMB ((COMB ((CONST =) COMB ((VAR |s| %T . |s%5|) CONST |0|))) CONST |0|))) COMB ((COMB ((CONST |/\\|) COMB ((COMB ((CONST =) COMB ((VAR |sink| %T . |rem%4|) CONST |0|))) CONST NIL %T . |source%3|))) COMB ((COMB ((CONST =) COMB ((VAR |r| %T . |s%5|) CONST |0|))) CONST |0|)))))) |bool|)) |bool|)) |bool|)) |bool|)) |bool|)) |bool|)))) (|message| PRED HOL_ASSERT COMB ((CONST HOL_DEFINITION) COMB ((CONST !) ABS ((VAR |p| %T . |set_non_packet%0|) COMB ((COMB ((CONST =) COMB ((CONST |message|) VAR |p| %T . |set_non_packet%0|) %T . |dd%1|)) COMB ((CONST SND) COMB ((CONST OUTL) VAR |p| %T . |set_non_packet%0|) %T . |,%2|) %T . |dd%1|) |bool|)))) (|label| PRED HOL_ASSERT COMB ((CONST HOL_DEFINITION) COMB ((CONST !) ABS ((VAR |p| %T . |set_non_packet%0|) COMB ((COMB ((CONST =) COMB ((CONST |label|) VAR |p| %T . |set_non_packet%0|) |num|)) COMB ((CONST FST) COMB ((CONST OUTL) VAR |p| %T . |set_non_packet%0|) %T . |,%2|) |num|) |bool|)))) (|new_packet| PRED HOL_ASSERT COMB ((CONST HOL_DEFINITION) COMB ((CONST !) ABS ((VAR |ss| |num|) COMB ((CONST !) ABS ((VAR |dd| %T . |dd%1|) COMB ((COMB ((CONST =) COMB ((COMB ((CONST |new_packet|) VAR |ss| |num|)) VAR |dd| %T . |dd%1|) %T . |set_non_packet%0|)) COMB ((CONST INL) COMB ((COMB ((CONST |,|) VAR |ss| |num|)) VAR |dd| %T . |dd%1|) %T . |,%2|) %T . |set_non_packet%0|) |bool|)) |bool|)))) (|good_packet| PRED HOL_ASSERT COMB ((CONST HOL_DEFINITION) COMB ((CONST !) ABS ((VAR |p| %T . |set_non_packet%0|) COMB ((COMB ((CONST =) COMB ((CONST |good_packet|) VAR |p| %T . |set_non_packet%0|) |bool|)) COMB ((CONST ISL) VAR |p| %T . |set_non_packet%0|) |bool|) |bool|)))) (|set_non_packet| PRED HOL_ASSERT COMB ((CONST HOL_DEFINITION) COMB ((COMB ((CONST =) CONST |set_non_packet| %T . |set_non_packet%0|)) COMB ((CONST INR) CONST |one|) %T . |set_non_packet%0|)))) (FACT (LIST_OF_BINDERS PRED HOL_ASSERT COMB ((CONST BINDERS) VAR |arb| %T . |dd%1|) |bool|) (TOTAL_CORRECTNESS_THM PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |source| %T . |source%3|) COMB ((CONST !) ABS ((VAR |maxseq| |num|) COMB ((CONST !) ABS ((VAR |rem| %T . |rem%4|) COMB ((CONST !) ABS ((VAR |sink| %T . |rem%4|) COMB ((CONST !) ABS ((VAR |s| %T . |s%5|) COMB ((CONST !) ABS ((VAR |r| %T . |s%5|) COMB ((CONST !) ABS ((VAR SW |num|) COMB ((CONST !) ABS ((VAR RW |num|) COMB ((CONST !) ABS ((VAR |p| %T . |p%7|) COMB ((CONST !) ABS ((VAR |i| %T . |s%5|) COMB ((CONST !) ABS ((VAR |q| %T . |q%9|) COMB ((CONST !) ABS ((VAR |c| %T . |s%5|) COMB ((CONST !) ABS ((VAR |aborted| %T . |q%9|) COMB ((CONST !) ABS ((VAR |maxT| |num|) COMB ((CONST !) ABS ((VAR |dataS| %T . |inC%6|) COMB ((CONST !) ABS ((VAR |dataR| %T . |inC%6|) COMB ((CONST !) ABS ((VAR |ackS| %T . |inC%6|) COMB ((CONST !) ABS ((VAR |ackR| %T . |inC%6|) COMB ((COMB ((CONST ==>) COMB ((COMB ((CONST |/\\|) COMB ((COMB ((COMB ((COMB ((COMB ((COMB ((COMB ((COMB ((COMB ((COMB ((COMB ((COMB ((COMB ((COMB ((COMB ((COMB ((COMB ((COMB ((CONST IMPL) VAR |source| %T . |source%3|)) VAR |maxseq| |num|)) VAR |rem| %T . |rem%4|)) VAR |s| %T . |s%5|)) VAR SW |num|)) VAR |p| %T . |p%7|)) VAR |i| %T . |s%5|)) VAR |c| %T . |s%5|)) VAR |aborted| %T . |q%9|)) VAR |maxT| |num|)) VAR |sink| %T . |rem%4|)) VAR |r| %T . |s%5|)) VAR RW |num|)) VAR |q| %T . |q%9|)) VAR |dataS| %T . |inC%6|)) VAR |dataR| %T . |inC%6|)) VAR |ackS| %T . |inC%6|)) VAR |ackR| %T . |inC%6|))) COMB ((COMB ((CONST LIVE_ASSUM) VAR |aborted|)) VAR |maxT|)))) COMB ((CONST ?) ABS ((VAR |t| |num|) COMB ((COMB ((CONST =) COMB ((VAR |sink| %T . |rem%4|) VAR |t|))) VAR |source| %T . |source%3|) |bool|))))) |bool|)) |bool|)) |bool|)) |bool|)) |bool|)) |bool|)) |bool|)) |bool|)) |bool|)) |bool|)) |bool|)) |bool|)) |bool|)) |bool|)) |bool|)) |bool|)) |bool|)) |bool|) (LIVENESS PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |maxseq| |num|) COMB ((CONST !) ABS ((VAR |rem| %T . |rem%4|) COMB ((CONST !) ABS ((VAR |sink| %T . |rem%4|) COMB ((CONST !) ABS ((VAR |s| %T . |s%5|) COMB ((CONST !) ABS ((VAR |r| %T . |s%5|) COMB ((CONST !) ABS ((VAR SW |num|) COMB ((CONST !) ABS ((VAR |c| %T . |s%5|) COMB ((CONST !) ABS ((VAR |aborted| %T . |q%9|) COMB ((CONST !) ABS ((VAR |maxT| |num|) COMB ((CONST !) ABS ((VAR |p| %T . |p%7|) COMB ((CONST !) ABS ((VAR |i| %T . |s%5|) COMB ((CONST !) ABS ((VAR |ackS| %T . |inC%6|) COMB ((CONST !) ABS ((VAR |dataS| %T . |inC%6|) COMB ((CONST !) ABS ((VAR |source| %T . |source%3|) COMB ((COMB ((CONST ==>) COMB ((COMB ((CONST |/\\|) COMB ((COMB ((CONST LIVE_ASSUM) VAR |aborted|)) VAR |maxT|))) COMB ((COMB ((CONST |/\\|) COMB ((COMB ((COMB ((COMB ((COMB ((COMB ((CONST INIT) VAR |source| %T . |source%3|)) VAR |maxseq| |num|)) VAR |rem| %T . |rem%4|)) VAR |s| %T . |s%5|)) VAR |sink| %T . |rem%4|)) VAR |r| %T . |s%5|))) COMB ((COMB ((CONST |/\\|) COMB ((COMB ((COMB ((COMB ((COMB ((COMB ((COMB ((COMB ((CONST SENDER) VAR |maxseq| |num|)) VAR SW |num|)) VAR |rem| %T . |rem%4|)) VAR |s| %T . |s%5|)) VAR |p| %T . |p%7|)) VAR |i| %T . |s%5|)) VAR |dataS| %T . |inC%6|)) VAR |ackS| %T . |inC%6|))) COMB ((COMB ((COMB ((COMB ((COMB ((COMB ((COMB ((COMB ((CONST ABORT) VAR |c| %T . |s%5|)) VAR |aborted| %T . |q%9|)) VAR |maxT| |num|)) VAR |maxseq| |num|)) VAR SW |num|)) VAR |s| %T . |s%5|)) VAR |rem| %T . |rem%4|)) VAR |ackS| %T . |inC%6|)))))) COMB ((COMB ((CONST =) COMB ((VAR |rem| %T . |rem%4|) COMB ((COMB ((CONST *) VAR |maxT|)) COMB ((CONST LENGTH) COMB ((VAR |rem| %T . |rem%4|) CONST |0|)))))) CONST NIL %T . |source%3|)))) |bool|)) |bool|)) |bool|)) |bool|)) |bool|)) |bool|)) |bool|)) |bool|)) |bool|)) |bool|)) |bool|)) |bool|)) |bool|)) |bool|) (|decreasing_rem_lemma| PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |rem| %T . |rem%4|) COMB ((CONST !) ABS ((VAR |maxT| |num|) COMB ((COMB ((CONST ==>) COMB ((CONST !) ABS ((VAR |t| |num|) COMB ((COMB ((CONST |\\/|) COMB ((CONST NULL) COMB ((VAR |rem| %T . |rem%4|) COMB ((COMB ((CONST +) VAR |t|)) VAR |maxT|))))) COMB ((CONST ?) ABS ((VAR |x| |num|) COMB ((COMB ((CONST |/\\|) COMB ((COMB ((CONST =) COMB ((VAR |rem| %T . |rem%4|) COMB ((COMB ((CONST +) VAR |t|)) VAR |maxT|)))) COMB ((COMB ((CONST TLI) VAR |x| |num|)) COMB ((VAR |rem| %T . |rem%4|) VAR |t|)) %T . |source%3|))) COMB ((COMB ((CONST <) CONST |0|)) VAR |x|))))))))) COMB ((CONST !) ABS ((VAR |n| |num|) COMB ((COMB ((CONST <=) COMB ((CONST LENGTH) COMB ((VAR |rem| %T . |rem%4|) COMB ((COMB ((CONST *) VAR |maxT|)) VAR |n|))))) COMB ((COMB ((CONST -) COMB ((CONST LENGTH) COMB ((VAR |rem| %T . |rem%4|) CONST |0|)))) VAR |n|))))))) |bool|)) |bool|) (|Liveness| PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |maxseq| |num|) COMB ((CONST !) ABS ((VAR |rem| %T . |rem%4|) COMB ((CONST !) ABS ((VAR |sink| %T . |rem%4|) COMB ((CONST !) ABS ((VAR |s| %T . |s%5|) COMB ((CONST !) ABS ((VAR |r| %T . |s%5|) COMB ((CONST !) ABS ((VAR SW |num|) COMB ((CONST !) ABS ((VAR |c| %T . |s%5|) COMB ((CONST !) ABS ((VAR |aborted| %T . |q%9|) COMB ((CONST !) ABS ((VAR |maxT| |num|) COMB ((CONST !) ABS ((VAR |p| %T . |p%7|) COMB ((CONST !) ABS ((VAR |i| %T . |s%5|) COMB ((CONST !) ABS ((VAR |ackS| %T . |inC%6|) COMB ((CONST !) ABS ((VAR |dataS| %T . |inC%6|) COMB ((CONST !) ABS ((VAR |source| %T . |source%3|) COMB ((COMB ((CONST ==>) COMB ((COMB ((CONST |/\\|) COMB ((COMB ((COMB ((COMB ((COMB ((COMB ((CONST INIT) VAR |source| %T . |source%3|)) VAR |maxseq| |num|)) VAR |rem| %T . |rem%4|)) VAR |s| %T . |s%5|)) VAR |sink| %T . |rem%4|)) VAR |r| %T . |s%5|))) COMB ((COMB ((CONST |/\\|) COMB ((COMB ((COMB ((COMB ((COMB ((COMB ((COMB ((COMB ((CONST SENDER) VAR |maxseq| |num|)) VAR SW |num|)) VAR |rem| %T . |rem%4|)) VAR |s| %T . |s%5|)) VAR |p| %T . |p%7|)) VAR |i| %T . |s%5|)) VAR |dataS| %T . |inC%6|)) VAR |ackS| %T . |inC%6|))) COMB ((COMB ((COMB ((COMB ((COMB ((COMB ((COMB ((COMB ((CONST ABORT) VAR |c| %T . |s%5|)) VAR |aborted| %T . |q%9|)) VAR |maxT| |num|)) VAR |maxseq| |num|)) VAR SW |num|)) VAR |s| %T . |s%5|)) VAR |rem| %T . |rem%4|)) VAR |ackS| %T . |inC%6|))))) COMB ((CONST !) ABS ((VAR |t| |num|) COMB ((COMB ((CONST ==>) COMB ((CONST ~) COMB ((CONST NULL) COMB ((VAR |rem| %T . |rem%4|) COMB ((COMB ((CONST +) VAR |t|)) VAR |maxT|)))))) COMB ((COMB ((CONST |\\/|) COMB ((CONST ?) ABS ((VAR |x| |num|) COMB ((COMB ((CONST |/\\|) COMB ((COMB ((CONST =) COMB ((VAR |rem| %T . |rem%4|) COMB ((COMB ((CONST +) VAR |t|)) VAR |maxT|)))) COMB ((COMB ((CONST TLI) VAR |x| |num|)) COMB ((VAR |rem| %T . |rem%4|) VAR |t|)) %T . |source%3|))) COMB ((COMB ((CONST <) CONST |0|)) VAR |x|)))))) COMB ((VAR |aborted| %T . |q%9|) COMB ((COMB ((CONST +) VAR |t|)) COMB ((COMB ((CONST +) VAR |maxT|)) CONST |1|)))))))))) |bool|)) |bool|)) |bool|)) |bool|)) |bool|)) |bool|)) |bool|)) |bool|)) |bool|)) |bool|)) |bool|)) |bool|)) |bool|)) |bool|) (|Liveness_3| PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |maxseq| |num|) COMB ((CONST !) ABS ((VAR |rem| %T . |rem%4|) COMB ((CONST !) ABS ((VAR |sink| %T . |rem%4|) COMB ((CONST !) ABS ((VAR |s| %T . |s%5|) COMB ((CONST !) ABS ((VAR |r| %T . |s%5|) COMB ((CONST !) ABS ((VAR SW |num|) COMB ((CONST !) ABS ((VAR |c| %T . |s%5|) COMB ((CONST !) ABS ((VAR |aborted| %T . |q%9|) COMB ((CONST !) ABS ((VAR |maxT| |num|) COMB ((CONST !) ABS ((VAR |p| %T . |p%7|) COMB ((CONST !) ABS ((VAR |i| %T . |s%5|) COMB ((CONST !) ABS ((VAR |ackS| %T . |inC%6|) COMB ((CONST !) ABS ((VAR |dataS| %T . |inC%6|) COMB ((CONST !) ABS ((VAR |source| %T . |source%3|) COMB ((COMB ((CONST ==>) COMB ((COMB ((CONST |/\\|) COMB ((COMB ((COMB ((COMB ((COMB ((COMB ((CONST INIT) VAR |source| %T . |source%3|)) VAR |maxseq| |num|)) VAR |rem| %T . |rem%4|)) VAR |s| %T . |s%5|)) VAR |sink| %T . |rem%4|)) VAR |r| %T . |s%5|))) COMB ((COMB ((CONST |/\\|) COMB ((COMB ((COMB ((COMB ((COMB ((COMB ((COMB ((COMB ((CONST SENDER) VAR |maxseq| |num|)) VAR SW |num|)) VAR |rem| %T . |rem%4|)) VAR |s| %T . |s%5|)) VAR |p| %T . |p%7|)) VAR |i| %T . |s%5|)) VAR |dataS| %T . |inC%6|)) VAR |ackS| %T . |inC%6|))) COMB ((COMB ((COMB ((COMB ((COMB ((COMB ((COMB ((COMB ((CONST ABORT) VAR |c| %T . |s%5|)) VAR |aborted| %T . |q%9|)) VAR |maxT| |num|)) VAR |maxseq| |num|)) VAR SW |num|)) VAR |s| %T . |s%5|)) VAR |rem| %T . |rem%4|)) VAR |ackS| %T . |inC%6|))))) COMB ((CONST !) ABS ((VAR |n| |num|) COMB ((CONST !) ABS ((VAR |t| |num|) COMB ((COMB ((CONST |\\/|) COMB ((CONST ?) ABS ((VAR |x| |num|) COMB ((COMB ((CONST |/\\|) COMB ((COMB ((CONST =) COMB ((VAR |rem| %T . |rem%4|) COMB ((COMB ((CONST +) VAR |t|)) VAR |n|)))) COMB ((COMB ((CONST TLI) VAR |x| |num|)) COMB ((VAR |rem| %T . |rem%4|) VAR |t|)) %T . |source%3|))) COMB ((COMB ((CONST <) CONST |0|)) VAR |x|)))))) COMB ((COMB ((CONST |/\\|) COMB ((COMB ((CONST =) COMB ((VAR |rem| %T . |rem%4|) COMB ((COMB ((CONST +) VAR |t|)) VAR |n|)))) COMB ((VAR |rem| %T . |rem%4|) VAR |t|)))) COMB ((COMB ((CONST <=) VAR |n|)) COMB ((VAR |c| %T . |s%5|) COMB ((COMB ((CONST +) VAR |t|)) VAR |n|))))))) |bool|))))) |bool|)) |bool|)) |bool|)) |bool|)) |bool|)) |bool|)) |bool|)) |bool|)) |bool|)) |bool|)) |bool|)) |bool|)) |bool|)) |bool|) (|Liveness_2| PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |maxseq| |num|) COMB ((CONST !) ABS ((VAR |rem| %T . |rem%4|) COMB ((CONST !) ABS ((VAR |sink| %T . |rem%4|) COMB ((CONST !) ABS ((VAR |s| %T . |s%5|) COMB ((CONST !) ABS ((VAR SW |num|) COMB ((CONST !) ABS ((VAR |c| %T . |s%5|) COMB ((CONST !) ABS ((VAR |aborted| %T . |q%9|) COMB ((CONST !) ABS ((VAR |maxT| |num|) COMB ((CONST !) ABS ((VAR |ackS| %T . |inC%6|) COMB ((COMB ((CONST ==>) COMB ((COMB ((COMB ((COMB ((COMB ((COMB ((COMB ((COMB ((CONST ABORT) VAR |c| %T . |s%5|)) VAR |aborted| %T . |q%9|)) VAR |maxT| |num|)) VAR |maxseq| |num|)) VAR SW |num|)) VAR |s| %T . |s%5|)) VAR |rem| %T . |rem%4|)) VAR |ackS| %T . |inC%6|))) COMB ((CONST !) ABS ((VAR |t| |num|) COMB ((COMB ((CONST =) COMB ((COMB ((CONST |/\\|) COMB ((COMB ((CONST |\\/|) COMB ((COMB ((CONST >=) COMB ((VAR |c| %T . |s%5|) VAR |t|))) VAR |maxT|))) COMB ((VAR |aborted| %T . |q%9|) VAR |t|)))) COMB ((CONST ~) COMB ((CONST NULL) COMB ((VAR |rem| %T . |rem%4|) VAR |t|)))))) COMB ((VAR |aborted| %T . |q%9|) COMB ((COMB ((CONST +) VAR |t|)) CONST |1|))) |bool|))))) |bool|)) |bool|)) |bool|)) |bool|)) |bool|)) |bool|)) |bool|)) |bool|)) |bool|) (|Liveness_1| PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |maxseq| |num|) COMB ((CONST !) ABS ((VAR |rem| %T . |rem%4|) COMB ((CONST !) ABS ((VAR |sink| %T . |rem%4|) COMB ((CONST !) ABS ((VAR |s| %T . |s%5|) COMB ((CONST !) ABS ((VAR |r| %T . |s%5|) COMB ((CONST !) ABS ((VAR SW |num|) COMB ((CONST !) ABS ((VAR |c| %T . |s%5|) COMB ((CONST !) ABS ((VAR |aborted| %T . |q%9|) COMB ((CONST !) ABS ((VAR |maxT| |num|) COMB ((CONST !) ABS ((VAR |p| %T . |p%7|) COMB ((CONST !) ABS ((VAR |i| %T . |s%5|) COMB ((CONST !) ABS ((VAR |ackS| %T . |inC%6|) COMB ((CONST !) ABS ((VAR |dataS| %T . |inC%6|) COMB ((CONST !) ABS ((VAR |source| %T . |source%3|) COMB ((COMB ((CONST ==>) COMB ((COMB ((CONST |/\\|) COMB ((COMB ((COMB ((COMB ((COMB ((COMB ((CONST INIT) VAR |source| %T . |source%3|)) VAR |maxseq| |num|)) VAR |rem| %T . |rem%4|)) VAR |s| %T . |s%5|)) VAR |sink| %T . |rem%4|)) VAR |r| %T . |s%5|))) COMB ((COMB ((CONST |/\\|) COMB ((COMB ((COMB ((COMB ((COMB ((COMB ((COMB ((COMB ((CONST SENDER) VAR |maxseq| |num|)) VAR SW |num|)) VAR |rem| %T . |rem%4|)) VAR |s| %T . |s%5|)) VAR |p| %T . |p%7|)) VAR |i| %T . |s%5|)) VAR |dataS| %T . |inC%6|)) VAR |ackS| %T . |inC%6|))) COMB ((COMB ((COMB ((COMB ((COMB ((COMB ((COMB ((COMB ((CONST ABORT) VAR |c| %T . |s%5|)) VAR |aborted| %T . |q%9|)) VAR |maxT| |num|)) VAR |maxseq| |num|)) VAR SW |num|)) VAR |s| %T . |s%5|)) VAR |rem| %T . |rem%4|)) VAR |ackS| %T . |inC%6|))))) COMB ((CONST !) ABS ((VAR |t| |num|) COMB ((COMB ((CONST |\\/|) COMB ((COMB ((CONST |/\\|) COMB ((CONST ?) ABS ((VAR |x| |num|) COMB ((COMB ((CONST |/\\|) COMB ((COMB ((CONST =) COMB ((VAR |rem| %T . |rem%4|) COMB ((COMB ((CONST +) VAR |t|)) CONST |1|)))) COMB ((COMB ((CONST TLI) VAR |x| |num|)) COMB ((VAR |rem| %T . |rem%4|) VAR |t|)) %T . |source%3|))) COMB ((COMB ((CONST <) CONST |0|)) VAR |x|)))))) COMB ((COMB ((CONST =) COMB ((VAR |c| %T . |s%5|) COMB ((COMB ((CONST +) VAR |t|)) CONST |1|)))) CONST |0|)))) COMB ((COMB ((CONST |/\\|) COMB ((COMB ((CONST =) COMB ((VAR |rem| %T . |rem%4|) COMB ((COMB ((CONST +) VAR |t|)) CONST |1|)))) COMB ((VAR |rem| %T . |rem%4|) VAR |t|)))) COMB ((COMB ((CONST =) COMB ((VAR |c| %T . |s%5|) COMB ((COMB ((CONST +) VAR |t|)) CONST |1|)))) COMB ((COMB ((CONST +) COMB ((VAR |c| %T . |s%5|) VAR |t|))) CONST |1|))))))))) |bool|)) |bool|)) |bool|)) |bool|)) |bool|)) |bool|)) |bool|)) |bool|)) |bool|)) |bool|)) |bool|)) |bool|)) |bool|)) |bool|) (|SW_value| PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |rem| %T . |rem%4|) COMB ((CONST !) ABS ((VAR |s| %T . |s%5|) COMB ((CONST !) ABS ((VAR SW |num|) COMB ((CONST !) ABS ((VAR |maxseq| |num|) COMB ((CONST !) ABS ((VAR |p| %T . |p%7|) COMB ((CONST !) ABS ((VAR |i| %T . |s%5|) COMB ((CONST !) ABS ((VAR |dataS| %T . |inC%6|) COMB ((COMB ((CONST ==>) COMB ((COMB ((COMB ((COMB ((COMB ((COMB ((COMB ((CONST DATA_TRANS) VAR |rem| %T . |rem%4|)) VAR |s| %T . |s%5|)) VAR SW |num|)) VAR |maxseq| |num|)) VAR |p| %T . |p%7|)) VAR |i| %T . |s%5|)) VAR |dataS| %T . |inC%6|))) COMB ((COMB ((CONST =) VAR SW |num|)) COMB ((COMB ((CONST -) VAR |maxseq|)) CONST |1|))))) |bool|)) |bool|)) |bool|)) |bool|)) |bool|)) |bool|)) |bool|) (IMPL_LIVE_PARTS PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |source| %T . |source%3|) COMB ((CONST !) ABS ((VAR |maxseq| |num|) COMB ((CONST !) ABS ((VAR SW |num|) COMB ((CONST !) ABS ((VAR RW |num|) COMB ((CONST !) ABS ((VAR |rem| %T . |rem%4|) COMB ((CONST !) ABS ((VAR |sink| %T . |rem%4|) COMB ((CONST !) ABS ((VAR |s| %T . |s%5|) COMB ((CONST !) ABS ((VAR |r| %T . |s%5|) COMB ((CONST !) ABS ((VAR |p| %T . |p%7|) COMB ((CONST !) ABS ((VAR |i| %T . |s%5|) COMB ((CONST !) ABS ((VAR |q| %T . |q%9|) COMB ((CONST !) ABS ((VAR |c| %T . |s%5|) COMB ((CONST !) ABS ((VAR |aborted| %T . |q%9|) COMB ((CONST !) ABS ((VAR |maxT| |num|) COMB ((CONST !) ABS ((VAR |dataS| %T . |inC%6|) COMB ((CONST !) ABS ((VAR |dataR| %T . |inC%6|) COMB ((CONST !) ABS ((VAR |ackS| %T . |inC%6|) COMB ((CONST !) ABS ((VAR |ackR| %T . |inC%6|) COMB ((COMB ((CONST ==>) COMB ((COMB ((COMB ((COMB ((COMB ((COMB ((COMB ((COMB ((COMB ((COMB ((COMB ((COMB ((COMB ((COMB ((COMB ((COMB ((COMB ((COMB ((CONST IMPL) VAR |source| %T . |source%3|)) VAR |maxseq| |num|)) VAR |rem| %T . |rem%4|)) VAR |s| %T . |s%5|)) VAR SW |num|)) VAR |p| %T . |p%7|)) VAR |i| %T . |s%5|)) VAR |c| %T . |s%5|)) VAR |aborted| %T . |q%9|)) VAR |maxT| |num|)) VAR |sink| %T . |rem%4|)) VAR |r| %T . |s%5|)) VAR RW |num|)) VAR |q| %T . |q%9|)) VAR |dataS| %T . |inC%6|)) VAR |dataR| %T . |inC%6|)) VAR |ackS| %T . |inC%6|)) VAR |ackR| %T . |inC%6|))) COMB ((COMB ((CONST |/\\|) COMB ((COMB ((COMB ((COMB ((COMB ((COMB ((CONST INIT) VAR |source| %T . |source%3|)) VAR |maxseq| |num|)) VAR |rem| %T . |rem%4|)) VAR |s| %T . |s%5|)) VAR |sink| %T . |rem%4|)) VAR |r| %T . |s%5|))) COMB ((COMB ((CONST |/\\|) COMB ((COMB ((COMB ((COMB ((COMB ((COMB ((COMB ((COMB ((CONST SENDER) VAR |maxseq| |num|)) VAR SW |num|)) VAR |rem| %T . |rem%4|)) VAR |s| %T . |s%5|)) VAR |p| %T . |p%7|)) VAR |i| %T . |s%5|)) VAR |dataS| %T . |inC%6|)) VAR |ackS| %T . |inC%6|))) COMB ((COMB ((COMB ((COMB ((COMB ((COMB ((COMB ((COMB ((CONST ABORT) VAR |c| %T . |s%5|)) VAR |aborted| %T . |q%9|)) VAR |maxT| |num|)) VAR |maxseq| |num|)) VAR SW |num|)) VAR |s| %T . |s%5|)) VAR |rem| %T . |rem%4|)) VAR |ackS| %T . |inC%6|)))))) |bool|)) |bool|)) |bool|)) |bool|)) |bool|)) |bool|)) |bool|)) |bool|)) |bool|)) |bool|)) |bool|)) |bool|)) |bool|)) |bool|)) |bool|)) |bool|)) |bool|)) |bool|) (SAFETY_THM PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |source| %T . |source%3|) COMB ((CONST !) ABS ((VAR |maxseq| |num|) COMB ((CONST !) ABS ((VAR |rem| %T . |rem%4|) COMB ((CONST !) ABS ((VAR |s| %T . |s%5|) COMB ((CONST !) ABS ((VAR SW |num|) COMB ((CONST !) ABS ((VAR |p| %T . |p%7|) COMB ((CONST !) ABS ((VAR |i| %T . |s%5|) COMB ((CONST !) ABS ((VAR |c| %T . |s%5|) COMB ((CONST !) ABS ((VAR |aborted| %T . |q%9|) COMB ((CONST !) ABS ((VAR |maxT| |num|) COMB ((CONST !) ABS ((VAR |sink| %T . |rem%4|) COMB ((CONST !) ABS ((VAR |r| %T . |s%5|) COMB ((CONST !) ABS ((VAR RW |num|) COMB ((CONST !) ABS ((VAR |q| %T . |q%9|) COMB ((CONST !) ABS ((VAR |dataS| %T . |inC%6|) COMB ((CONST !) ABS ((VAR |dataR| %T . |inC%6|) COMB ((CONST !) ABS ((VAR |ackS| %T . |inC%6|) COMB ((CONST !) ABS ((VAR |ackR| %T . |inC%6|) COMB ((COMB ((CONST ==>) COMB ((COMB ((COMB ((COMB ((COMB ((COMB ((COMB ((COMB ((COMB ((COMB ((COMB ((COMB ((COMB ((COMB ((COMB ((COMB ((COMB ((COMB ((CONST IMPL) VAR |source| %T . |source%3|)) VAR |maxseq| |num|)) VAR |rem| %T . |rem%4|)) VAR |s| %T . |s%5|)) VAR SW |num|)) VAR |p| %T . |p%7|)) VAR |i| %T . |s%5|)) VAR |c| %T . |s%5|)) VAR |aborted| %T . |q%9|)) VAR |maxT| |num|)) VAR |sink| %T . |rem%4|)) VAR |r| %T . |s%5|)) VAR RW |num|)) VAR |q| %T . |q%9|)) VAR |dataS| %T . |inC%6|)) VAR |dataR| %T . |inC%6|)) VAR |ackS| %T . |inC%6|)) VAR |ackR| %T . |inC%6|))) COMB ((CONST !) ABS ((VAR |t| |num|) COMB ((COMB ((CONST =) COMB ((COMB ((CONST APPEND) COMB ((VAR |sink| %T . |rem%4|) VAR |t|))) COMB ((COMB ((CONST TLI) COMB ((CONST |subm|) COMB ((COMB ((CONST |,|) COMB ((VAR |r| %T . |s%5|) VAR |t|))) COMB ((COMB ((CONST |,|) COMB ((VAR |s| %T . |s%5|) VAR |t|))) VAR |maxseq| |num|) %T . |,%8|)))) COMB ((VAR |rem| %T . |rem%4|) VAR |t|)) %T . |source%3|) %T . |source%3|)) VAR |source| %T . |source%3|) |bool|))))) |bool|)) |bool|)) |bool|)) |bool|)) |bool|)) |bool|)) |bool|)) |bool|)) |bool|)) |bool|)) |bool|)) |bool|)) |bool|)) |bool|)) |bool|)) |bool|)) |bool|)) |bool|) (|Lemma4| PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |dataR| %T . |inC%6|) COMB ((CONST !) ABS ((VAR |dataS| %T . |inC%6|) COMB ((CONST !) ABS ((VAR |maxseq| |num|) COMB ((CONST !) ABS ((VAR |source| %T . |source%3|) COMB ((CONST !) ABS ((VAR |rem| %T . |rem%4|) COMB ((CONST !) ABS ((VAR |sink| %T . |rem%4|) COMB ((CONST !) ABS ((VAR |s| %T . |s%5|) COMB ((CONST !) ABS ((VAR |r| %T . |s%5|) COMB ((CONST !) ABS ((VAR SW |num|) COMB ((CONST !) ABS ((VAR RW |num|) COMB ((CONST !) ABS ((VAR |p| %T . |p%7|) COMB ((CONST !) ABS ((VAR |i| %T . |s%5|) COMB ((COMB ((CONST ==>) COMB ((COMB ((CONST |/\\|) COMB ((COMB ((COMB ((COMB ((COMB ((COMB ((CONST INIT) VAR |source| %T . |source%3|)) VAR |maxseq| |num|)) VAR |rem| %T . |rem%4|)) VAR |s| %T . |s%5|)) VAR |sink| %T . |rem%4|)) VAR |r| %T . |s%5|))) COMB ((COMB ((CONST |/\\|) COMB ((COMB ((COMB ((COMB ((COMB ((COMB ((COMB ((CONST DATA_TRANS) VAR |rem| %T . |rem%4|)) VAR |s| %T . |s%5|)) VAR SW |num|)) VAR |maxseq| |num|)) VAR |p| %T . |p%7|)) VAR |i| %T . |s%5|)) VAR |dataS| %T . |inC%6|))) COMB ((COMB ((CONST |/\\|) COMB ((COMB ((CONST CHANNEL) VAR |dataS| %T . |inC%6|)) VAR |dataR| %T . |inC%6|))) COMB ((COMB ((COMB ((COMB ((COMB ((CONST DATA_RECV) VAR |dataR| %T . |inC%6|)) VAR RW |num|)) VAR |maxseq| |num|)) VAR |sink| %T . |rem%4|)) VAR |r| %T . |s%5|)))))) COMB ((CONST !) ABS ((VAR |t| |num|) COMB ((COMB ((COMB ((CONST COND) COMB ((COMB ((COMB ((COMB ((CONST IN_WINDOW) COMB ((VAR |dataR| %T . |inC%6|) VAR |t|))) COMB ((VAR |r| %T . |s%5|) VAR |t|))) VAR RW |num|)) VAR |maxseq| |num|) |bool|)) COMB ((COMB ((CONST |/\\|) COMB ((COMB ((CONST =) COMB ((VAR |r| %T . |s%5|) COMB ((COMB ((CONST +) VAR |t|)) CONST |1|)))) COMB ((CONST |plusm|) COMB ((COMB ((CONST |,|) COMB ((VAR |r| %T . |s%5|) VAR |t|))) COMB ((COMB ((CONST |,|) CONST |1|)) VAR |maxseq| |num|) %T . |,%8|))))) COMB ((COMB ((CONST |/\\|) COMB ((COMB ((CONST =) COMB ((VAR |sink| %T . |rem%4|) COMB ((COMB ((CONST +) VAR |t|)) CONST |1|)))) COMB ((COMB ((CONST APPEND) COMB ((VAR |sink| %T . |rem%4|) VAR |t|))) COMB ((COMB ((CONST CONS) COMB ((COMB ((CONST HDI) COMB ((CONST |subm|) COMB ((COMB ((CONST |,|) COMB ((VAR |r| %T . |s%5|) VAR |t|))) COMB ((COMB ((CONST |,|) COMB ((VAR |s| %T . |s%5|) VAR |t|))) VAR |maxseq| |num|) %T . |,%8|)))) COMB ((VAR |rem| %T . |rem%4|) VAR |t|)) %T . |dd%1|)) CONST NIL %T . |source%3|) %T . |source%3|) %T . |source%3|))) COMB ((COMB ((CONST |/\\|) COMB ((CONST ~) COMB ((CONST NULL) COMB ((COMB ((CONST TLI) COMB ((CONST |subm|) COMB ((COMB ((CONST |,|) COMB ((VAR |r| %T . |s%5|) VAR |t|))) COMB ((COMB ((CONST |,|) COMB ((VAR |s| %T . |s%5|) VAR |t|))) VAR |maxseq| |num|) %T . |,%8|)))) COMB ((VAR |rem| %T . |rem%4|) VAR |t|)) %T . |source%3|)))) COMB ((COMB ((CONST <) COMB ((COMB ((CONST +) COMB ((CONST |subm|) COMB ((COMB ((CONST |,|) COMB ((VAR |r| %T . |s%5|) VAR |t|))) COMB ((COMB ((CONST |,|) COMB ((VAR |s| %T . |s%5|) VAR |t|))) VAR |maxseq| |num|) %T . |,%8|)))) CONST |1|))) VAR |maxseq|)))))) COMB ((COMB ((CONST |/\\|) COMB ((COMB ((CONST =) COMB ((VAR |r| %T . |s%5|) COMB ((COMB ((CONST +) VAR |t|)) CONST |1|)))) COMB ((VAR |r| %T . |s%5|) VAR |t|)))) COMB ((COMB ((CONST =) COMB ((VAR |sink| %T . |rem%4|) COMB ((COMB ((CONST +) VAR |t|)) CONST |1|)))) COMB ((VAR |sink| %T . |rem%4|) VAR |t|)))) |bool|))))) |bool|)) |bool|)) |bool|)) |bool|)) |bool|)) |bool|)) |bool|)) |bool|)) |bool|)) |bool|)) |bool|)) |bool|) (|Lemma3| PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |source| %T . |source%3|) COMB ((CONST !) ABS ((VAR |rem| %T . |rem%4|) COMB ((CONST !) ABS ((VAR |sink| %T . |rem%4|) COMB ((CONST !) ABS ((VAR SW |num|) COMB ((CONST !) ABS ((VAR |maxseq| |num|) COMB ((CONST !) ABS ((VAR |s| %T . |s%5|) COMB ((CONST !) ABS ((VAR |r| %T . |s%5|) COMB ((CONST !) ABS ((VAR |q| %T . |q%9|) COMB ((CONST !) ABS ((VAR |ackS| %T . |inC%6|) COMB ((CONST !) ABS ((VAR |ackR| %T . |inC%6|) COMB ((CONST !) ABS ((VAR |dataR| %T . |inC%6|) COMB ((COMB ((CONST ==>) COMB ((COMB ((CONST |/\\|) COMB ((COMB ((COMB ((COMB ((CONST ACK_TRANS) VAR |r| %T . |s%5|)) VAR |maxseq| |num|)) VAR |q| %T . |q%9|)) VAR |ackR| %T . |inC%6|))) COMB ((COMB ((CONST |/\\|) COMB ((COMB ((CONST CHANNEL) VAR |ackR| %T . |inC%6|)) VAR |ackS| %T . |inC%6|))) COMB ((COMB ((CONST |/\\|) COMB ((COMB ((COMB ((COMB ((COMB ((CONST ACK_RECV) VAR |ackS| %T . |inC%6|)) VAR SW |num|)) VAR |maxseq| |num|)) VAR |rem| %T . |rem%4|)) VAR |s| %T . |s%5|))) COMB ((COMB ((CONST |/\\|) COMB ((COMB ((COMB ((COMB ((COMB ((COMB ((CONST INIT) VAR |source| %T . |source%3|)) VAR |maxseq| |num|)) VAR |rem| %T . |rem%4|)) VAR |s| %T . |s%5|)) VAR |sink| %T . |rem%4|)) VAR |r| %T . |s%5|))) COMB ((COMB ((COMB ((COMB ((COMB ((CONST DATA_RECV) VAR |dataR| %T . |inC%6|)) VAR RW |num|)) VAR |maxseq| |num|)) VAR |sink| %T . |rem%4|)) VAR |r| %T . |s%5|))))))) COMB ((CONST !) ABS ((VAR |t| |num|) COMB ((COMB ((COMB ((CONST COND) COMB ((COMB ((COMB ((COMB ((CONST IN_WINDOW) COMB ((VAR |ackS| %T . |inC%6|) VAR |t|))) COMB ((VAR |s| %T . |s%5|) VAR |t|))) VAR SW |num|)) VAR |maxseq| |num|) |bool|)) COMB ((COMB ((CONST |/\\|) COMB ((COMB ((CONST =) COMB ((VAR |s| %T . |s%5|) COMB ((COMB ((CONST +) VAR |t|)) CONST |1|)))) COMB ((VAR |r| %T . |s%5|) VAR |t|)))) COMB ((COMB ((CONST =) COMB ((VAR |rem| %T . |rem%4|) COMB ((COMB ((CONST +) VAR |t|)) CONST |1|)))) COMB ((COMB ((CONST TLI) COMB ((CONST |subm|) COMB ((COMB ((CONST |,|) COMB ((VAR |r| %T . |s%5|) VAR |t|))) COMB ((COMB ((CONST |,|) COMB ((VAR |s| %T . |s%5|) VAR |t|))) VAR |maxseq| |num|) %T . |,%8|)))) COMB ((VAR |rem| %T . |rem%4|) VAR |t|)) %T . |source%3|)))) COMB ((COMB ((CONST |/\\|) COMB ((COMB ((CONST =) COMB ((VAR |s| %T . |s%5|) COMB ((COMB ((CONST +) VAR |t|)) CONST |1|)))) COMB ((VAR |s| %T . |s%5|) VAR |t|)))) COMB ((COMB ((CONST =) COMB ((VAR |rem| %T . |rem%4|) COMB ((COMB ((CONST +) VAR |t|)) CONST |1|)))) COMB ((VAR |rem| %T . |rem%4|) VAR |t|)))) |bool|))))) |bool|)) |bool|)) |bool|)) |bool|)) |bool|)) |bool|)) |bool|)) |bool|)) |bool|)) |bool|)) |bool|) (|Lemma2| PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |dataR| %T . |inC%6|) COMB ((CONST !) ABS ((VAR |dataS| %T . |inC%6|) COMB ((CONST !) ABS ((VAR |maxseq| |num|) COMB ((CONST !) ABS ((VAR SW |num|) COMB ((CONST !) ABS ((VAR RW |num|) COMB ((CONST !) ABS ((VAR |rem| %T . |rem%4|) COMB ((CONST !) ABS ((VAR |sink| %T . |rem%4|) COMB ((CONST !) ABS ((VAR |s| %T . |s%5|) COMB ((CONST !) ABS ((VAR |r| %T . |s%5|) COMB ((CONST !) ABS ((VAR |p| %T . |p%7|) COMB ((CONST !) ABS ((VAR |i| %T . |s%5|) COMB ((CONST !) ABS ((VAR |t| |num|) COMB ((COMB ((CONST ==>) COMB ((COMB ((CONST |/\\|) COMB ((COMB ((COMB ((COMB ((COMB ((COMB ((COMB ((CONST DATA_TRANS) VAR |rem| %T . |rem%4|)) VAR |s| %T . |s%5|)) VAR SW |num|)) VAR |maxseq| |num|)) VAR |p| %T . |p%7|)) VAR |i| %T . |s%5|)) VAR |dataS| %T . |inC%6|))) COMB ((COMB ((CONST |/\\|) COMB ((COMB ((CONST CHANNEL) VAR |dataS| %T . |inC%6|)) VAR |dataR| %T . |inC%6|))) COMB ((COMB ((CONST |/\\|) COMB ((COMB ((CONST =) VAR RW |num|)) CONST |1|))) COMB ((COMB ((CONST |/\\|) COMB ((COMB ((COMB ((COMB ((CONST IN_WINDOW) COMB ((VAR |dataR| %T . |inC%6|) VAR |t|))) COMB ((VAR |r| %T . |s%5|) VAR |t|))) VAR RW |num|)) VAR |maxseq| |num|))) COMB ((COMB ((CONST <) CONST |0|)) VAR |maxseq|))))))) COMB ((COMB ((CONST |/\\|) COMB ((COMB ((CONST =) COMB ((COMB ((CONST HDI) COMB ((CONST |subm|) COMB ((COMB ((CONST |,|) COMB ((VAR |r| %T . |s%5|) VAR |t|))) COMB ((COMB ((CONST |,|) COMB ((VAR |s| %T . |s%5|) VAR |t|))) VAR |maxseq| |num|) %T . |,%8|)))) COMB ((VAR |rem| %T . |rem%4|) VAR |t|)) %T . |dd%1|)) COMB ((CONST |message|) COMB ((VAR |dataR| %T . |inC%6|) VAR |t|)) %T . |dd%1|))) COMB ((COMB ((CONST |/\\|) COMB ((CONST ~) COMB ((CONST NULL) COMB ((COMB ((CONST TLI) COMB ((CONST |subm|) COMB ((COMB ((CONST |,|) COMB ((VAR |r| %T . |s%5|) VAR |t|))) COMB ((COMB ((CONST |,|) COMB ((VAR |s| %T . |s%5|) VAR |t|))) VAR |maxseq| |num|) %T . |,%8|)))) COMB ((VAR |rem| %T . |rem%4|) VAR |t|)) %T . |source%3|)))) COMB ((COMB ((CONST <) COMB ((COMB ((CONST +) COMB ((CONST |subm|) COMB ((COMB ((CONST |,|) COMB ((VAR |r| %T . |s%5|) VAR |t|))) COMB ((COMB ((CONST |,|) COMB ((VAR |s| %T . |s%5|) VAR |t|))) VAR |maxseq| |num|) %T . |,%8|)))) CONST |1|))) VAR |maxseq|)))))) |bool|)) |bool|)) |bool|)) |bool|)) |bool|)) |bool|)) |bool|)) |bool|)) |bool|)) |bool|)) |bool|)) |bool|) (|Lemma2C| PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |dataR| %T . |inC%6|) COMB ((CONST !) ABS ((VAR |dataS| %T . |inC%6|) COMB ((CONST !) ABS ((VAR |maxseq| |num|) COMB ((CONST !) ABS ((VAR SW |num|) COMB ((CONST !) ABS ((VAR RW |num|) COMB ((CONST !) ABS ((VAR |rem| %T . |rem%4|) COMB ((CONST !) ABS ((VAR |sink| %T . |rem%4|) COMB ((CONST !) ABS ((VAR |s| %T . |s%5|) COMB ((CONST !) ABS ((VAR |r| %T . |s%5|) COMB ((CONST !) ABS ((VAR |p| %T . |p%7|) COMB ((CONST !) ABS ((VAR |i| %T . |s%5|) COMB ((CONST !) ABS ((VAR |t| |num|) COMB ((COMB ((CONST ==>) COMB ((COMB ((CONST |/\\|) COMB ((COMB ((COMB ((COMB ((COMB ((COMB ((COMB ((CONST DATA_TRANS) VAR |rem| %T . |rem%4|)) VAR |s| %T . |s%5|)) VAR SW |num|)) VAR |maxseq| |num|)) VAR |p| %T . |p%7|)) VAR |i| %T . |s%5|)) VAR |dataS| %T . |inC%6|))) COMB ((COMB ((CONST |/\\|) COMB ((COMB ((CONST CHANNEL) VAR |dataS| %T . |inC%6|)) VAR |dataR| %T . |inC%6|))) COMB ((COMB ((CONST |/\\|) COMB ((COMB ((CONST =) VAR RW |num|)) CONST |1|))) COMB ((COMB ((CONST |/\\|) COMB ((COMB ((COMB ((COMB ((CONST IN_WINDOW) COMB ((VAR |dataR| %T . |inC%6|) VAR |t|))) COMB ((VAR |r| %T . |s%5|) VAR |t|))) VAR RW |num|)) VAR |maxseq| |num|))) COMB ((COMB ((CONST <) CONST |0|)) VAR |maxseq|))))))) COMB ((COMB ((CONST =) COMB ((VAR |i| %T . |s%5|) VAR |t|))) COMB ((CONST |subm|) COMB ((COMB ((CONST |,|) COMB ((VAR |r| %T . |s%5|) VAR |t|))) COMB ((COMB ((CONST |,|) COMB ((VAR |s| %T . |s%5|) VAR |t|))) VAR |maxseq| |num|) %T . |,%8|)))))) |bool|)) |bool|)) |bool|)) |bool|)) |bool|)) |bool|)) |bool|)) |bool|)) |bool|)) |bool|)) |bool|)) |bool|) (|Lemma2B| PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |dataR| %T . |inC%6|) COMB ((CONST !) ABS ((VAR |r| %T . |s%5|) COMB ((CONST !) ABS ((VAR RW |num|) COMB ((CONST !) ABS ((VAR |maxseq| |num|) COMB ((CONST !) ABS ((VAR |t| |num|) COMB ((COMB ((CONST ==>) COMB ((COMB ((CONST |/\\|) COMB ((COMB ((COMB ((COMB ((CONST IN_WINDOW) COMB ((VAR |dataR| %T . |inC%6|) VAR |t|))) COMB ((VAR |r| %T . |s%5|) VAR |t|))) VAR RW |num|)) VAR |maxseq| |num|))) COMB ((COMB ((CONST =) VAR RW |num|)) CONST |1|)))) COMB ((COMB ((CONST =) COMB ((CONST |subm|) COMB ((COMB ((CONST |,|) COMB ((CONST |label|) COMB ((VAR |dataR| %T . |inC%6|) VAR |t|)) |num|)) COMB ((COMB ((CONST |,|) COMB ((VAR |r| %T . |s%5|) VAR |t|))) VAR |maxseq| |num|) %T . |,%8|)))) CONST |0|)))) |bool|)) |bool|)) |bool|)) |bool|)) |bool|) (|Lemma2A| PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |dataS| %T . |inC%6|) COMB ((CONST !) ABS ((VAR |maxseq| |num|) COMB ((CONST !) ABS ((VAR |s| %T . |s%5|) COMB ((CONST !) ABS ((VAR |p| %T . |p%7|) COMB ((CONST !) ABS ((VAR |i| %T . |s%5|) COMB ((CONST !) ABS ((VAR |rem| %T . |rem%4|) COMB ((CONST !) ABS ((VAR |t| |num|) COMB ((COMB ((CONST ==>) COMB ((COMB ((CONST |/\\|) COMB ((COMB ((COMB ((COMB ((COMB ((COMB ((COMB ((CONST DATA_TRANS) VAR |rem| %T . |rem%4|)) VAR |s| %T . |s%5|)) VAR SW |num|)) VAR |maxseq| |num|)) VAR |p| %T . |p%7|)) VAR |i| %T . |s%5|)) VAR |dataS| %T . |inC%6|))) COMB ((COMB ((CONST |/\\|) COMB ((CONST |good_packet|) COMB ((VAR |dataS| %T . |inC%6|) VAR |t|)))) COMB ((COMB ((CONST <) CONST |0|)) VAR |maxseq|))))) COMB ((COMB ((CONST |/\\|) COMB ((COMB ((CONST =) COMB ((CONST |label|) COMB ((VAR |dataS| %T . |inC%6|) VAR |t|)) |num|)) COMB ((CONST |plusm|) COMB ((COMB ((CONST |,|) COMB ((VAR |s| %T . |s%5|) VAR |t|))) COMB ((COMB ((CONST |,|) COMB ((VAR |i| %T . |s%5|) VAR |t|))) VAR |maxseq| |num|) %T . |,%8|))))) COMB ((COMB ((CONST |/\\|) COMB ((COMB ((CONST =) COMB ((CONST |message|) COMB ((VAR |dataS| %T . |inC%6|) VAR |t|)) %T . |dd%1|)) COMB ((COMB ((CONST HDI) COMB ((VAR |i| %T . |s%5|) VAR |t|))) COMB ((VAR |rem| %T . |rem%4|) VAR |t|)) %T . |dd%1|))) COMB ((COMB ((CONST |/\\|) COMB ((COMB ((CONST <) COMB ((COMB ((CONST +) COMB ((VAR |i| %T . |s%5|) VAR |t|))) CONST |1|))) VAR |maxseq|))) COMB ((CONST ~) COMB ((CONST NULL) COMB ((COMB ((CONST TLI) COMB ((VAR |i| %T . |s%5|) VAR |t|))) COMB ((VAR |rem| %T . |rem%4|) VAR |t|)) %T . |source%3|)))))))) |bool|)) |bool|)) |bool|)) |bool|)) |bool|)) |bool|)) |bool|) (|Lemma1| PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |r| %T . |s%5|) COMB ((CONST !) ABS ((VAR |s| %T . |s%5|) COMB ((CONST !) ABS ((VAR |q| %T . |q%9|) COMB ((CONST !) ABS ((VAR SW |num|) COMB ((CONST !) ABS ((VAR |maxseq| |num|) COMB ((CONST !) ABS ((VAR |ackS| %T . |inC%6|) COMB ((CONST !) ABS ((VAR |ackR| %T . |inC%6|) COMB ((CONST !) ABS ((VAR |t| |num|) COMB ((COMB ((CONST ==>) COMB ((COMB ((CONST |/\\|) COMB ((COMB ((COMB ((COMB ((CONST ACK_TRANS) VAR |r| %T . |s%5|)) VAR |maxseq| |num|)) VAR |q| %T . |q%9|)) VAR |ackR| %T . |inC%6|))) COMB ((COMB ((CONST |/\\|) COMB ((COMB ((CONST CHANNEL) VAR |ackR| %T . |inC%6|)) VAR |ackS| %T . |inC%6|))) COMB ((COMB ((COMB ((COMB ((CONST IN_WINDOW) COMB ((VAR |ackS| %T . |inC%6|) VAR |t|))) COMB ((VAR |s| %T . |s%5|) VAR |t|))) VAR SW |num|)) VAR |maxseq| |num|))))) COMB ((COMB ((CONST =) COMB ((CONST |label|) COMB ((VAR |ackS| %T . |inC%6|) VAR |t|)) |num|)) COMB ((CONST |subm|) COMB ((COMB ((CONST |,|) COMB ((VAR |r| %T . |s%5|) VAR |t|))) COMB ((COMB ((CONST |,|) CONST |1|)) VAR |maxseq| |num|) %T . |,%8|)))))) |bool|)) |bool|)) |bool|)) |bool|)) |bool|)) |bool|)) |bool|)) |bool|) (|Lemma1A| PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |inC| %T . |inC%6|) COMB ((CONST !) ABS ((VAR |outC| %T . |inC%6|) COMB ((CONST !) ABS ((VAR |t| |num|) COMB ((COMB ((CONST ==>) COMB ((COMB ((CONST |/\\|) COMB ((COMB ((CONST CHANNEL) VAR |inC| %T . |inC%6|)) VAR |outC| %T . |inC%6|))) COMB ((CONST |good_packet|) COMB ((VAR |outC| %T . |inC%6|) VAR |t|))))) COMB ((COMB ((CONST =) COMB ((VAR |outC| %T . |inC%6|) VAR |t|))) COMB ((VAR |inC| %T . |inC%6|) VAR |t|))))) |bool|)) |bool|)) |bool|) (|INIT_maxseq_0| PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |source| %T . |source%3|) COMB ((CONST !) ABS ((VAR |maxseq| |num|) COMB ((CONST !) ABS ((VAR |rem| %T . |rem%4|) COMB ((CONST !) ABS ((VAR |sink| %T . |rem%4|) COMB ((CONST !) ABS ((VAR |s| %T . |s%5|) COMB ((CONST !) ABS ((VAR |r| %T . |s%5|) COMB ((COMB ((CONST ==>) COMB ((COMB ((COMB ((COMB ((COMB ((COMB ((CONST INIT) VAR |source| %T . |source%3|)) VAR |maxseq| |num|)) VAR |rem| %T . |rem%4|)) VAR |s| %T . |s%5|)) VAR |sink| %T . |rem%4|)) VAR |r| %T . |s%5|))) COMB ((COMB ((CONST <) CONST |0|)) VAR |maxseq|)))) |bool|)) |bool|)) |bool|)) |bool|)) |bool|)) |bool|) (|INIT_maxseq_1| PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |source| %T . |source%3|) COMB ((CONST !) ABS ((VAR |maxseq| |num|) COMB ((CONST !) ABS ((VAR |rem| %T . |rem%4|) COMB ((CONST !) ABS ((VAR |sink| %T . |rem%4|) COMB ((CONST !) ABS ((VAR |s| %T . |s%5|) COMB ((CONST !) ABS ((VAR |r| %T . |s%5|) COMB ((COMB ((CONST ==>) COMB ((COMB ((COMB ((COMB ((COMB ((COMB ((CONST INIT) VAR |source| %T . |source%3|)) VAR |maxseq| |num|)) VAR |rem| %T . |rem%4|)) VAR |s| %T . |s%5|)) VAR |sink| %T . |rem%4|)) VAR |r| %T . |s%5|))) COMB ((COMB ((CONST <) CONST |1|)) VAR |maxseq|)))) |bool|)) |bool|)) |bool|)) |bool|)) |bool|)) |bool|) (|r_in_range| PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |source| %T . |source%3|) COMB ((CONST !) ABS ((VAR |maxseq| |num|) COMB ((CONST !) ABS ((VAR |rem| %T . |rem%4|) COMB ((CONST !) ABS ((VAR |s| %T . |s%5|) COMB ((CONST !) ABS ((VAR |sink| %T . |rem%4|) COMB ((CONST !) ABS ((VAR |r| %T . |s%5|) COMB ((CONST !) ABS ((VAR RW |num|) COMB ((CONST !) ABS ((VAR |dataR| %T . |inC%6|) COMB ((COMB ((CONST ==>) COMB ((COMB ((CONST |/\\|) COMB ((COMB ((COMB ((COMB ((COMB ((COMB ((CONST INIT) VAR |source| %T . |source%3|)) VAR |maxseq| |num|)) VAR |rem| %T . |rem%4|)) VAR |s| %T . |s%5|)) VAR |sink| %T . |rem%4|)) VAR |r| %T . |s%5|))) COMB ((COMB ((COMB ((COMB ((COMB ((CONST DATA_RECV) VAR |dataR| %T . |inC%6|)) VAR RW |num|)) VAR |maxseq| |num|)) VAR |sink| %T . |rem%4|)) VAR |r| %T . |s%5|)))) COMB ((CONST !) ABS ((VAR |t| |num|) COMB ((COMB ((CONST <) COMB ((VAR |r| %T . |s%5|) VAR |t|))) VAR |maxseq|)))))) |bool|)) |bool|)) |bool|)) |bool|)) |bool|)) |bool|)) |bool|)) |bool|))))