NuITP (alpha 30) ProofProved


Goal

True = paired($1:Card, $2:Card) → alter($3:List $1:Card) = alter($3:List $1:Card $2:Card)

Script

set goal (paired(C1:Card,C2:Card) = True) → alter(L1:List C1:Card C2:Card) = alter(L1:List C1:Card) .
apply gnd! to 0 .
apply gsi* to 0.2.1 on $3 with GLISTL .
apply gsi* to 0.3.1 on $3 with GLISTL .

Rewriting Theory

fmod GILBREATH-ACU is
sorts Boolean Card List NeList .
subsort Card < NeList .
subsort NeList < List .
op False : -> Boolean [ ctor metadata "1" ] .
op True : -> Boolean [ ctor metadata "0" ] .
op __ : List List -> List [ assoc id: nil metadata "5" ] .
op __ : NeList NeList -> NeList [ assoc ctor id: nil metadata "5" ] .
op alter : List -> Boolean [ metadata "8" ] .
op black : -> Card [ ctor metadata "3" ] .
op even : List -> Boolean [ metadata "11" ] .
op neg : Card -> Card [ metadata "12" ] .
op nil : -> List [ ctor metadata "2" ] .
op opposite : List List -> Boolean [ metadata "7" ] .
op paired : Card Card -> Boolean [ metadata "6" ] .
op pairedList : List -> Boolean [ metadata "9" ] .
op red : -> Card [ ctor metadata "4" ] .
op rotate : List -> List [ metadata "13" ] .
op shuffle : List List List -> Boolean [ metadata "10" ] .
eq alter(C:Card) = True .
eq alter(nil) = True .
eq even(C:Card) = False .
eq even(nil) = True .
eq even(L1:List C1:Card L2:List C2:Card L3:List) = even(L1:List L2:List L3:List) .
eq neg(black) = red [ variant ] .
eq neg(red) = black [ variant ] .
eq opposite(L:List, nil) = False [ variant ] .
eq opposite(nil, L:List) = False [ variant ] .
eq opposite(C1:Card L1:List, C2:Card L2:List) = paired(C1:Card, C2:Card) [ variant ] .
eq paired(C:Card, C:Card) = False [ variant ] .
eq paired(black, red) = True [ variant ] .
eq paired(red, black) = True [ variant ] .
eq pairedList(C:Card) = False .
eq pairedList(nil) = True .
eq pairedList(C:Card C:Card L:List) = False .
eq rotate(nil) = nil [ variant ] .
eq rotate(C:Card L:List) = L:List C:Card [ variant ] .
eq shuffle(L1:List, C2:Card L2:List, nil) = False .
eq shuffle(nil, nil, nil) = True .
eq shuffle(nil, nil, C3:Card L3:List) = False .
eq shuffle(C1:Card L1:List, L2:List, nil) = False .
ceq alter(C1:Card C2:Card L:List) = False if paired(C1:Card, C2:Card) = False .
ceq alter(C1:Card C2:Card L:List) = alter(C2:Card L:List) if paired(C1:Card, C2:Card) = True .
ceq pairedList(C1:Card C2:Card L:List) = pairedList(L:List) if paired(C1:Card, C2:Card) = True .
ceq shuffle(nil, C2:Card L2:List, C3:Card L3:List) = False if paired(C2:Card, C3:Card) = True .
ceq shuffle(nil, C2:Card L2:List, C3:Card L3:List) = shuffle(nil, L2:List, L3:List) if paired(C2:Card, C3:Card) = False .
ceq shuffle(C1:Card L1:List, nil, C3:Card L3:List) = False if paired(C1:Card, C3:Card) = True .
ceq shuffle(C1:Card L1:List, nil, C3:Card L3:List) = shuffle(L1:List, nil, L3:List) if paired(C1:Card, C3:Card) = False .
ceq shuffle(C1:Card L1:List, C2:Card L2:List, C3:Card L3:List) = False if paired(C1:Card, C3:Card) = True /\ paired(C2:Card, C3:Card) = True .
ceq shuffle(C1:Card L1:List, C2:Card L2:List, C3:Card L3:List) = False if paired(C1:Card, C3:Card) = True /\ shuffle(C1:Card L1:List, L2:List, L3:List) = False .
ceq shuffle(C1:Card L1:List, C2:Card L2:List, C3:Card L3:List) = False if paired(C2:Card, C3:Card) = True /\ shuffle(L1:List, C2:Card L2:List, L3:List) = False .
ceq shuffle(C1:Card L1:List, C2:Card L2:List, C3:Card L3:List) = False if shuffle(L1:List, C2:Card L2:List, L3:List) = False /\ shuffle(C1:Card L1:List, L2:List, L3:List) = False .
ceq shuffle(C1:Card L1:List, C2:Card L2:List, C3:Card L3:List) = True if paired(C1:Card, C3:Card) = False /\ shuffle(L1:List, C2:Card L2:List, L3:List) = True .
ceq shuffle(C1:Card L1:List, C2:Card L2:List, C3:Card L3:List) = True if paired(C2:Card, C3:Card) = False /\ shuffle(C1:Card L1:List, L2:List, L3:List) = True .
endfm

Goals

Goal Id:  0
Generated By:  init
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
True = paired($1:Card, $2:Card) → alter($3:List $1:Card) = alter($3:List $1:Card $2:Card)
Goal Id:  0.1
Generated By:  GND
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
True = paired(black, black) → alter($3:List black) = alter($3:List black black)
Goal Id:  0.2
Generated By:  GND
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
True = paired(black, red) → alter($3:List black) = alter($3:List black red)
Goal Id:  0.3
Generated By:  GND
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
True = paired(red, black) → alter($3:List red) = alter($3:List red black)
Goal Id:  0.4
Generated By:  GND
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
True = paired(red, red) → alter($3:List red) = alter($3:List red red)
Goal Id:  0.1.1
Generated By:  EPS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.2.1
Generated By:  EPS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
alter($3:List black) = alter($3:List black red)
Goal Id:  0.3.1
Generated By:  EPS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
alter($3:List red) = alter($3:List red black)
Goal Id:  0.4.1
Generated By:  EPS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.2.1.1
Generated By:  GSI
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
alter(black black) = alter(black black red)
Goal Id:  0.2.1.2
Generated By:  GSI
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
alter(black) = alter(black red)
Goal Id:  0.2.1.3
Generated By:  GSI
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
alter(red black) = alter(red black red)
Goal Id:  0.2.1.4
Generated By:  GSI
Skolem Ops:
$4.NeList
Executable Hypotheses:
alter($4 black red) ⇒ alter($4 black)
Non-Executable Hypotheses:
None
Goal:
alter(black $4 black) = alter(black $4 black red)
Goal Id:  0.2.1.5
Generated By:  GSI
Skolem Ops:
$4.NeList
Executable Hypotheses:
alter($4 black red) ⇒ alter($4 black)
Non-Executable Hypotheses:
None
Goal:
alter(red $4 black) = alter(red $4 black red)
Goal Id:  0.3.1.1
Generated By:  GSI
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
alter(black red) = alter(black red black)
Goal Id:  0.3.1.2
Generated By:  GSI
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
alter(red) = alter(red black)
Goal Id:  0.3.1.3
Generated By:  GSI
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
alter(red red) = alter(red red black)
Goal Id:  0.3.1.4
Generated By:  GSI
Skolem Ops:
$4.NeList
Executable Hypotheses:
alter($4 red black) ⇒ alter($4 red)
Non-Executable Hypotheses:
None
Goal:
alter(black $4 red) = alter(black $4 red black)
Goal Id:  0.3.1.5
Generated By:  GSI
Skolem Ops:
$4.NeList
Executable Hypotheses:
alter($4 red black) ⇒ alter($4 red)
Non-Executable Hypotheses:
None
Goal:
alter(red $4 red) = alter(red $4 red black)
Goal Id:  0.2.1.1.1
Generated By:  EPS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.2.1.2.1
Generated By:  EPS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.2.1.3.1
Generated By:  EPS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.2.1.4.1
Generated By:  CAS
Skolem Ops:
$4.NeList
Executable Hypotheses:
$4 ⇒ black
Non-Executable Hypotheses:
None
Goal:
alter(black black black) = alter(black black black red)
Goal Id:  0.2.1.4.2
Generated By:  CAS
Skolem Ops:
$4.NeList
Executable Hypotheses:
$4 ⇒ red
Non-Executable Hypotheses:
None
Goal:
alter(black red black) = alter(black red black red)
Goal Id:  0.2.1.4.3
Generated By:  CAS
Skolem Ops:
$4.NeList
$5.NeList
Executable Hypotheses:
$4 ⇒ black $5
alter(black $5 black red) ⇒ alter(black $5 black)
Non-Executable Hypotheses:
None
Goal:
alter(black black $5 black) = alter(black black $5 black red)
Goal Id:  0.2.1.4.4
Generated By:  CAS
Skolem Ops:
$4.NeList
$5.NeList
Executable Hypotheses:
$4 ⇒ red $5
alter(red $5 black red) ⇒ alter(red $5 black)
Non-Executable Hypotheses:
None
Goal:
alter(black red $5 black) = alter(black red $5 black red)
Goal Id:  0.2.1.5.1
Generated By:  CAS
Skolem Ops:
$4.NeList
Executable Hypotheses:
$4 ⇒ black
Non-Executable Hypotheses:
None
Goal:
alter(red black black) = alter(red black black red)
Goal Id:  0.2.1.5.2
Generated By:  CAS
Skolem Ops:
$4.NeList
Executable Hypotheses:
$4 ⇒ red
Non-Executable Hypotheses:
None
Goal:
alter(red red black) = alter(red red black red)
Goal Id:  0.2.1.5.3
Generated By:  CAS
Skolem Ops:
$4.NeList
$5.NeList
Executable Hypotheses:
$4 ⇒ black $5
alter(black $5 black red) ⇒ alter(black $5 black)
Non-Executable Hypotheses:
None
Goal:
alter(red black $5 black) = alter(red black $5 black red)
Goal Id:  0.2.1.5.4
Generated By:  CAS
Skolem Ops:
$4.NeList
$5.NeList
Executable Hypotheses:
$4 ⇒ red $5
alter(red $5 black red) ⇒ alter(red $5 black)
Non-Executable Hypotheses:
None
Goal:
alter(red red $5 black) = alter(red red $5 black red)
Goal Id:  0.3.1.1.1
Generated By:  EPS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.3.1.2.1
Generated By:  EPS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.3.1.3.1
Generated By:  EPS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.3.1.4.1
Generated By:  CAS
Skolem Ops:
$4.NeList
Executable Hypotheses:
$4 ⇒ black
Non-Executable Hypotheses:
None
Goal:
alter(black black red) = alter(black black red black)
Goal Id:  0.3.1.4.2
Generated By:  CAS
Skolem Ops:
$4.NeList
Executable Hypotheses:
$4 ⇒ red
Non-Executable Hypotheses:
None
Goal:
alter(black red red) = alter(black red red black)
Goal Id:  0.3.1.4.3
Generated By:  CAS
Skolem Ops:
$4.NeList
$5.NeList
Executable Hypotheses:
$4 ⇒ black $5
alter(black $5 red black) ⇒ alter(black $5 red)
Non-Executable Hypotheses:
None
Goal:
alter(black black $5 red) = alter(black black $5 red black)
Goal Id:  0.3.1.4.4
Generated By:  CAS
Skolem Ops:
$4.NeList
$5.NeList
Executable Hypotheses:
$4 ⇒ red $5
alter(red $5 red black) ⇒ alter(red $5 red)
Non-Executable Hypotheses:
None
Goal:
alter(black red $5 red) = alter(black red $5 red black)
Goal Id:  0.3.1.5.1
Generated By:  CAS
Skolem Ops:
$4.NeList
Executable Hypotheses:
$4 ⇒ black
Non-Executable Hypotheses:
None
Goal:
alter(red black red) = alter(red black red black)
Goal Id:  0.3.1.5.2
Generated By:  CAS
Skolem Ops:
$4.NeList
Executable Hypotheses:
$4 ⇒ red
Non-Executable Hypotheses:
None
Goal:
alter(red red red) = alter(red red red black)
Goal Id:  0.3.1.5.3
Generated By:  CAS
Skolem Ops:
$4.NeList
$5.NeList
Executable Hypotheses:
$4 ⇒ black $5
alter(black $5 red black) ⇒ alter(black $5 red)
Non-Executable Hypotheses:
None
Goal:
alter(red black $5 red) = alter(red black $5 red black)
Goal Id:  0.3.1.5.4
Generated By:  CAS
Skolem Ops:
$4.NeList
$5.NeList
Executable Hypotheses:
$4 ⇒ red $5
alter(red $5 red black) ⇒ alter(red $5 red)
Non-Executable Hypotheses:
None
Goal:
alter(red red $5 red) = alter(red red $5 red black)
Goal Id:  0.2.1.4.1.1
Generated By:  EPS
Skolem Ops:
$4.NeList
Executable Hypotheses:
$4 ⇒ black
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.2.1.4.2.1
Generated By:  EPS
Skolem Ops:
$4.NeList
Executable Hypotheses:
$4 ⇒ red
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.2.1.4.3.1
Generated By:  EPS
Skolem Ops:
$4.NeList
$5.NeList
Executable Hypotheses:
$4 ⇒ black $5
alter(black $5 black red) ⇒ alter(black $5 black)
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.2.1.4.4.1
Generated By:  EPS
Skolem Ops:
$4.NeList
$5.NeList
Executable Hypotheses:
$4 ⇒ red $5
alter(red $5 black red) ⇒ alter(red $5 black)
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.2.1.5.1.1
Generated By:  EPS
Skolem Ops:
$4.NeList
Executable Hypotheses:
$4 ⇒ black
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.2.1.5.2.1
Generated By:  EPS
Skolem Ops:
$4.NeList
Executable Hypotheses:
$4 ⇒ red
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.2.1.5.3.1
Generated By:  EPS
Skolem Ops:
$4.NeList
$5.NeList
Executable Hypotheses:
$4 ⇒ black $5
alter(black $5 black red) ⇒ alter(black $5 black)
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.2.1.5.4.1
Generated By:  EPS
Skolem Ops:
$4.NeList
$5.NeList
Executable Hypotheses:
$4 ⇒ red $5
alter(red $5 black red) ⇒ alter(red $5 black)
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.3.1.4.1.1
Generated By:  EPS
Skolem Ops:
$4.NeList
Executable Hypotheses:
$4 ⇒ black
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.3.1.4.2.1
Generated By:  EPS
Skolem Ops:
$4.NeList
Executable Hypotheses:
$4 ⇒ red
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.3.1.4.3.1
Generated By:  EPS
Skolem Ops:
$4.NeList
$5.NeList
Executable Hypotheses:
$4 ⇒ black $5
alter(black $5 red black) ⇒ alter(black $5 red)
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.3.1.4.4.1
Generated By:  EPS
Skolem Ops:
$4.NeList
$5.NeList
Executable Hypotheses:
$4 ⇒ red $5
alter(red $5 red black) ⇒ alter(red $5 red)
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.3.1.5.1.1
Generated By:  EPS
Skolem Ops:
$4.NeList
Executable Hypotheses:
$4 ⇒ black
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.3.1.5.2.1
Generated By:  EPS
Skolem Ops:
$4.NeList
Executable Hypotheses:
$4 ⇒ red
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.3.1.5.3.1
Generated By:  EPS
Skolem Ops:
$4.NeList
$5.NeList
Executable Hypotheses:
$4 ⇒ black $5
alter(black $5 red black) ⇒ alter(black $5 red)
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.3.1.5.4.1
Generated By:  EPS
Skolem Ops:
$4.NeList
$5.NeList
Executable Hypotheses:
$4 ⇒ red $5
alter(red $5 red black) ⇒ alter(red $5 red)
Non-Executable Hypotheses:
None
Goal:
true

Proof Tree